1#
2# Copyright 2016, Data61, CSIRO
3#
4# This software may be distributed and modified according to the terms of
5# the BSD 2-Clause license. Note that NO WARRANTY is provided.
6# See "LICENSE_BSD2.txt" for details.
7#
8# @TAG(DATA61_BSD)
9#
10
11# note this makefile will not work entirely correctly if invoked in the local
12# directory; make really needs to be invoked in the parent directory, or
13# further up still
14
15STP_PFX := $(realpath $(dir $(lastword $(MAKEFILE_LIST))))
16
17ISABELLE_HOME ?= $(STP_PFX)/../../../isabelle
18
19ifndef STP_INCLUDED
20STP_INCLUDED=true
21
22ARM_DIR=$(STP_PFX)/ARM
23ARM_HYP_DIR=$(STP_PFX)/ARM_HYP
24X64_DIR=$(STP_PFX)/X64
25RISCV64_DIR=$(STP_PFX)/RISCV64
26ARCH_DIRS=$(ARM_DIR) $(ARM_HYP_DIR) $(X64_DIR) $(RISCV64_DIR)
27
28STPARSER_ARM=$(ARM_DIR)/c-parser
29STPARSER_ARM_HYP=$(ARM_HYP_DIR)/c-parser
30STPARSER_X64=$(X64_DIR)/c-parser
31STPARSER_RISCV64=$(RISCV64_DIR)/c-parser
32STPARSERS=$(STPARSER_ARM) $(STPARSER_ARM_HYP) $(STPARSER_X64) $(STPARSER_RISCV64)
33
34TOKENIZER_ARM=$(ARM_DIR)/tokenizer
35TOKENIZER_ARM_HYP=$(ARM_HYP_DIR)/tokenizer
36TOKENIZER_X64=$(X64_DIR)/tokenizer
37TOKENIZER_RISCV64=$(RISCV64_DIR)/tokenizer
38TOKENIZERS=$(TOKENIZER_ARM) $(TOKENIZER_ARM_HYP) $(TOKENIZER_X64) $(TOKENIZER_RISCV64)
39
40.PHONY: all cparser_tools stp_all standalone-cparser standalone-tokenizer
41
42all: stp_all
43
44standalone-cparser stp_all: $(STPARSERS)
45standalone-tokenizer stp_all: $(TOKENIZERS)
46
47include $(STP_PFX)/../Makefile
48
49# This is only used for ARM_HYP and ARM since the former is a copy of the latter
50UMM_HEAP_ARM_HYP=$(realpath $(STP_PFX)/../umm_heap)/ARM_HYP
51UMM_HEAP_ARM=$(realpath $(STP_PFX)/../umm_heap/ARM)
52
53$(UMM_HEAP_ARM_HYP)/% : $(UMM_HEAP_ARM)/%
54	mkdir -p $(UMM_HEAP_ARM_HYP)
55	cp -p $< $@
56
57STP_CLEAN_TARGETS := $(STPARSERS) $(TOKENIZERS) $(STP_PFX)/c-parser.o $(STP_PFX)/table.ML
58
59$(STP_PFX)/table.ML: $(ISABELLE_HOME)/src/Pure/General/table.ML
60	sed -e '/ML.pretty-printing/,/final.declarations/d' < $< > $@
61
62$(ARCH_DIRS):
63	mkdir -p $@
64
65
66ifeq ($(SML_COMPILER),mlton)
67#
68# compilation if the compiler is mlton
69#
70
71ARM_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM'
72ARM_HYP_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM_HYP'
73X64_MLB_PATH := -mlb-path-var 'L4V_ARCH X64'
74RISCV64_MLB_PATH := -mlb-path-var 'L4V_ARCH RISCV64'
75
76PARSER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
77PARSER_DEPS_ARM_HYP := $(shell mlton $(ARM_HYP_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
78PARSER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
79PARSER_DEPS_RISCV64 := $(shell mlton $(RISCV64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
80
81TOKENIZER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
82TOKENIZER_DEPS_ARM_HYP := $(shell mlton $(ARM_HYP_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
83TOKENIZER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
84TOKENIZER_DEPS_RISCV64 := $(shell mlton $(RISCV64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
85
86$(STPARSER_ARM): $(PARSER_DEPS_ARM) | $(ARM_DIR)
87	mlton $(ARM_MLB_PATH) -output $@ $<
88
89$(STPARSER_ARM_HYP): $(PARSER_DEPS_ARM_HYP) | $(ARM_HYP_DIR)
90	mlton $(ARM_HYP_MLB_PATH) -output $@ $<
91
92$(STPARSER_X64): $(PARSER_DEPS_X64) | $(X64_DIR)
93	mlton $(X64_MLB_PATH) -output $@ $<
94
95$(STPARSER_RISCV64): $(PARSER_DEPS_RISCV64) | $(RISCV64_DIR)
96	mlton $(RISCV64_MLB_PATH) -output $@ $<
97
98$(TOKENIZER_ARM): $(TOKENIZER_DEPS_ARM) | $(ARM_DIR)
99	mlton $(ARM_MLB_PATH) -output $@ $<
100
101$(TOKENIZER_ARM_HYP): $(TOKENIZER_DEPS_ARM_HYP) | $(ARM_HYP_DIR)
102	mlton $(ARM_HYP_MLB_PATH) -output $@ $<
103
104$(TOKENIZER_X64): $(TOKENIZER_DEPS_X64) | $(X64_DIR)
105	mlton $(X64_MLB_PATH) -output $@ $<
106
107$(TOKENIZER_RISCV64): $(TOKENIZER_DEPS_RISCV64) | $(RISCV64_DIR)
108	mlton $(RISCV64_MLB_PATH) -output $@ $<
109
110else ifeq ($(SML_COMPILER),poly)
111#
112# compilation with polyml may be bit-rotted
113#
114
115PARSER0_DEPS := $(shell perl -e 'use Cwd "abs_path"; while (<>) { if (/ml$$|sig$$/i && !/^ *mlton/) { tr/ //d; print abs_path("$(STP_PFX)/$$_"); }}' < $(STP_PFX)/c-parser.mlb)
116PARSER_DEPS := $(PARSER0_DEPS) $(realpath $(STP_PFX)/c-parser.mlb) $(STP_PFX)/table.ML
117
118TOKENIZER0_DEPS := $(shell perl -e 'use Cwd "abs_path"; while (<>) { if (/ml$$|sig$$/i && !/^ *mlton/) { tr/ //d; print abs_path("$(STP_PFX)/$$_"); }}' < $(STP_PFX)/tokenizer.mlb)
119TOKENIZER_DEPS := $(TOKENIZER0_DEPS) $(realpath $(STP_PFX)/tokenzier.mlb) $(STP_PFX)/table.ML
120
121$(STPARSER): $(STP_PFX)/c-parser.o $(LIBPOLYML)
122	$(POLYCC) -o $@ $<
123
124$(STP_PFX)/c-parser.o: $(STP_PFX)/poly-cparser.ML $(PARSER_DEPS)
125	STP_PFX=$(STP_PFX) $(POLY) < $<
126
127$(STP_PFX)/tokenizer: $(STP_PFX)/tokenizer.o $(LIBPOLYML)
128	$(POLYCC) -o $@ $<
129
130$(STP_PFX)/tokenizer.o: $(STP_PFX)/poly-tokenizer.ML $(TOKENIZER_DEPS)
131	STP_PFX=$(STP_PFX) $(POLY) < $<
132
133
134.PHONY: stp_deps
135stp_deps:
136	@echo $(PARSER_DEPS)
137
138else
139$(error Can only cope with SML_COMPILER as "poly" or "mlton"; got $(SML_COMPILER))
140
141endif
142
143
144clean: stp_clean
145
146stp_clean:
147	-/bin/rm -f $(STP_CLEAN_TARGETS)
148	-/bin/rm -fr $(UMM_HEAP_ARM_HYP)
149
150endif
151