diff options
| author | Jon French <jf451@cam.ac.uk> | 2019-03-12 11:11:24 +0000 |
|---|---|---|
| committer | Jon French <jf451@cam.ac.uk> | 2019-03-12 11:11:24 +0000 |
| commit | 954a462605c14f3fb0d6283422b0e10560920195 (patch) | |
| tree | f6a38dd8ee0a14b3c171f1683800a49118cca6b7 | |
| parent | cef40e8d67063ec999efae89581feadb2d3d8278 (diff) | |
| download | sail-riscv-954a462605c14f3fb0d6283422b0e10560920195.zip sail-riscv-954a462605c14f3fb0d6283422b0e10560920195.tar.gz sail-riscv-954a462605c14f3fb0d6283422b0e10560920195.tar.bz2 | |
Makefile: generate toFromInterp and marshalled defs for RMEM
| -rw-r--r-- | Makefile | 24 |
1 files changed, 16 insertions, 8 deletions
@@ -237,22 +237,30 @@ generated_definitions/coq/riscv.vo: generated_definitions/coq/riscv_types.vo han generated_definitions/coq/riscv_duopod.vo: generated_definitions/coq/riscv_duopod_types.vo handwritten_support/riscv_extras.vo -riscv_rmem: generated_definitions/lem-for-rmem/riscv.lem -riscv_rmem: generated_definitions/lem-for-rmem/riscv_sequential.lem -riscv_rmem: generated_definitions/tofrominterp-for-rmem/riscv_toFromInterp2.ml +echo_rmem_srcs: + echo $(SAIL_RMEM_SRCS) + +riscv_rmem: generated_definitions/for-rmem/riscv.lem +riscv_rmem: generated_definitions/for-rmem/riscv_sequential.lem +riscv_rmem: generated_definitions/for-rmem/riscv_toFromInterp2.ml +riscv_rmem: generated_definitions/for-rmem/riscv.defs .PHONY: riscv_rmem -generated_definitions/lem-for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras -generated_definitions/lem-for-rmem/riscv_sequential.lem: SAIL_FLAGS += -lem_lib Riscv_extras_sequential -lem_sequential -generated_definitions/lem-for-rmem/%.lem: $(SAIL_RMEM_SRCS) +generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras +generated_definitions/for-rmem/riscv_sequential.lem: SAIL_FLAGS += -lem_lib Riscv_extras_sequential -lem_sequential +generated_definitions/for-rmem/%.lem: $(SAIL_RMEM_SRCS) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them $(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o $(notdir $(basename $@)) $^ -generated_definitions/tofrominterp-for-rmem/riscv_toFromInterp2.ml: $(SAIL_RMEM_SRCS) +generated_definitions/for-rmem/riscv_toFromInterp2.ml: $(SAIL_RMEM_SRCS) mkdir -p $(dir $@) $(SAIL) $(SAIL_FLAGS) -tofrominterp -tofrominterp_lem -tofrominterp_output_dir $(dir $@) -o riscv $^ +generated_definitions/for-rmem/riscv.defs: $(SAIL_RMEM_SRCS) + mkdir -p $(dir $@) + $(SAIL) $(SAIL_FLAGS) -marshal -o $(basename $@) $^ + # we exclude prelude.sail here, most code there should move to sail lib #LOC_FILES:=$(SAIL_SRCS) main.sail #include $(SAIL_DIR)/etc/loc.mk @@ -260,7 +268,7 @@ generated_definitions/tofrominterp-for-rmem/riscv_toFromInterp2.ml: $(SAIL_RMEM_ clean: -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* - -rm -rf generated_definitions/lem-for-rmem/* + -rm -rf generated_definitions/for-rmem/* -rm -f c_emulator/riscv_sim c_emulator/riscv_rvfi -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim ocaml_emulator/tracecmp -rm -f *.gcno *.gcda |