Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI

1 files changed, 39 insertions, 4 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index c7f72557..6fa738a7 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -7,16 +7,51 @@ CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri
 SAIL:=$(SAIL_DIR)/sail
 SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail
 
-CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+MIPS_PRE:=$(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail
+MIPS_TLB:=$(MIPS_SAIL_DIR)/mips_tlb.sail
+MIPS_TLB_STUB:=$(MIPS_SAIL_DIR)/mips_tlb_stub.sail
+MIPS_INSTS:=$(MIPS_SAIL_DIR)/mips_insts.sail
+MIPS_EPILOGUE:=$(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail
+CHERI128_PRE:=$(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail
+CHERI_INSTS:=$(CHERI_SAIL_DIR)/cheri_insts.sail
 
-CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
+CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_PRE) $(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)
+CHERI_MAIN:=$(CHERI_SAIL_DIR)/main.sail
 
-cheri: $(CHERI_SAILS)
+cheri: $(CHERI_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml -o $@ $^
 
-cheri128: $(CHERI128_SAILS)
+cheri128: $(CHERI128_SAILS) $(CHERI_MAIN)
 	$(SAIL) -ocaml -o $@ $^
 
+# TODO Using bit lists for now in Lem generation; for machine words,
+# monomorphisation is needed due to some variable length bitvectors, e.g. in
+# CLoad as of commit b34c3fb, in the TLB translation, and in compressed
+# capability functions
+
+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)
+	$(SAIL) -lem -o cheri -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri_types.lem: cheri.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
+
+cheri128.lem: $(CHERI128_SAILS)
+	$(SAIL) -lem -o cheri128 -lem_lib Mips_extras -undefined_gen -memo_z3 $^
+cheri128_types.lem: cheri128.lem
+
+C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem
+	lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
+
 clean:
 	rm -rf cheri cheri128 _sbuild inst_*.sail