diff options
| author | Brian Campbell | 2018-05-17 13:05:18 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-17 13:05:18 +0100 |
| commit | 97b978eb392bda9b66b22ee0bb2ec65b1407cb86 (patch) | |
| tree | 7a4b097344f333c58a0e1a302f53a29a444308a5 /cheri/Makefile | |
| parent | c37130ba4ac69be6a298476b24b1f93811df4bb4 (diff) | |
Clean up CHERI HOL generation a little too
Diffstat (limited to 'cheri/Makefile')
| -rw-r--r-- | cheri/Makefile | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 1f3e5179..42c7ef86 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -17,6 +17,7 @@ CHERI128_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude CHERI_INSTS:=$(CHERI_SAIL_DIR)/cheri_insts.sail CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) +CHERI_MONO_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(SAIL_LIB_DIR)/mono_rewrites.sail $(MIPS_TLB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) CHERI128_NO_TLB_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(MIPS_TLB_STUB) $(CHERI128_PRE) $(MIPS_INSTS) $(CHERI_INSTS) $(MIPS_EPILOGUE) @@ -59,15 +60,10 @@ cheri_no_tlb.lem: $(CHERI_NO_TLB_SAILS) $(SAIL) -lem -o cheri_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_no_tlb_types.lem: cheri_no_tlb.lem -cheri.lem: $(CHERI_SAILS) $(CHERI_MAIN) +cheri.lem: $(CHERI_MONO_SAILS) $(CHERI_MAIN) $(SAIL) -lem -o cheri -auto_mono -mono_rewrites -lem_mwords -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri_types.lem: cheri.lem -cheri_sequential.lem: $(CHERI_SAILS) $(CHERI_MAIN) - $(SAIL) -lem -o cheri_sequential -auto_mono -mono_rewrites -lem_mwords -lem_sequential -lem_lib Mips_extras_sequential -undefined_gen -memo_z3 $^ -cheri_sequential_types.lem: cheri_sequential.lem -Cheri_sequential.thy cheri_sequentialScript.sml: $(MIPS_SAIL_DIR)/mips_extras_sequential.lem - cheri128_no_tlb.lem: $(CHERI128_NO_TLB_SAILS) $(SAIL) -lem -o cheri128_no_tlb -lem_lib Mips_extras -undefined_gen -memo_z3 $^ cheri128_no_tlb_types.lem: cheri128_no_tlb.lem @@ -83,5 +79,10 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem %Script.sml: %.lem %_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem lem -hol -outdir . -lib $(SAIL_DIR)/lib/hol -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^ +%Theory.uo: %Script.sml + Holmake $@ + clean: rm -rf cheri cheri_trace cheri128 cheri128_trace _sbuild inst_*.sail cheri.c sail_latex sail_latexcc + rm -f cheriScript.sml cheri_typesScript.sml mips_extrasScript.sml + -Holmake cleanAll |