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