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

2 files changed, 47 insertions, 7 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
 
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 5dd14974..0072ded7 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -255,8 +255,8 @@ function register_inaccessible(r) =
   else
     false
 
-val MEMr_tag = "read_tag"  : bits(64) -> bool effect { rmemt }
-val MEMw_tag = "write_tag" : (bits(64) , bool) -> unit effect { wmvt }
+val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
+val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
 
 val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { escape, rmem, rmemt }
 function MEMr_tagged (addr) =
@@ -360,7 +360,12 @@ function addrWrapper(addr, accessType, width) =
       to_bits(64, vAddr); /* XXX vAddr not truncated because top <= 2^64 and size > 0 */
   }
 
-val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape}
+$ifdef _MIPS_TLB_STUB
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape}
+$else
+val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, escape, undef}
+$endif
+
 function TranslatePC (vAddr) = {
   incrementCP0Count();
   let pcc = capRegToCapStruct(PCC);