Make Lem export of CHERI(-256) typecheck

Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).

5 files changed, 15 insertions, 7 deletions

diff --git a/src/Makefile b/src/Makefile
index 53acec6a..4147b10c 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -78,11 +78,11 @@ ZARITH_LIB=$(ZARITH_DIR)/zarith.cmxa
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc
 
-MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 MIPS_SAILS:=$(MIPS_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
-MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+MIPS_NOTLB_SAILS_PRE:=$(SAIL_LIB_DIR)/prelude.sail $(SAIL_LIB_DIR)/prelude_wrappers.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(SAIL_DIR)/etc/regfp.sail $(MIPS_SAIL_DIR)/mips_regfp.sail
 
@@ -170,14 +170,14 @@ _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o cheri_notlb $(CHERI_NOTLB_SAILS)
 
-_build/cheri_embed_types.lem: $(CHERI_SAILS) ./sail.native
+_build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
 	../sail.native -lem_lib "Mips_extras_embed" -lem -o cheri $(CHERI_SAILS)
 
-_build/Cheri_embed_sequential.thy: _build/cheri_embed_types.lem
+_build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
 	cd _build ;\
-	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem ../../mips/mips_extras_embed_sequential.lem cheri_embed_types.lem cheri_embed_sequential.lem
+	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
 
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..fbe096c9 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -34,6 +34,8 @@ let adjust_start_index (start, v) = set_vector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_element v)
 let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false
+let cast_boolvec_bitvec (Vector bs start inc) =
+  Vector (List.map bool_to_bitU bs) start inc
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 10a56ad5..9bc81b3e 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -96,6 +96,8 @@ let adjust_start_index (start, v) = set_bitvector_start (start, v)
 
 let cast_vec_bool v = bitU_to_bool (extract_only_bit v)
 let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false)
+let cast_boolvec_bitvec (Vector bs start inc) =
+  vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eeec7440..e2cbb98a 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -11,6 +11,8 @@ type nn = natural
 val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
+let pow2 n = pow 2 n
+
 let bool_or (l, r) = (l || r)
 let bool_and (l, r) = (l && r)
 let bool_xor (l, r) = xor l r
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7671c26b..3d4f3083 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -843,8 +843,10 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e;])
     | E_assert (e1,e2) ->
-       let epp = separate space [string "assert'"; expY e1; expY e2] in
-       if aexp_needed then parens (align epp) else align epp
+       (* FIXME needs pretty-printing of E_constraint; ignore for now *)
+       string "()"
+       (* let epp = separate space [string "assert'"; expY e1; expY e2] in
+       if aexp_needed then parens (align epp) else align epp *)
     | E_app_infix (e1,id,e2) ->
        (* TODO: Should have been removed by the new type checker; check with Alasdair *)
        raise (Reporting_basic.err_unreachable l