Update CHERI code extraction from Isabelle

Also use zero-initialised memory.  Apparently some tests access unitialised
memory, and the default behaviour of the Lem shallow embedding is to fail in
this case.

2 files changed, 39 insertions, 16 deletions

diff --git a/test/isabelle/Cheri_code.thy b/test/isabelle/Cheri_code.thy
index 13884ad5..c0e8f9a7 100644
--- a/test/isabelle/Cheri_code.thy
+++ b/test/isabelle/Cheri_code.thy
@@ -5,32 +5,55 @@ begin
 declare [[code abort: failwith]]
 
 code_datatype
-  DADDIU DADDU DADDI DADD ADD ADDI ADDU ADDIU DSUBU DSUB SUB SUBU AND0 ANDI OR0 
+  DADDIU DADDU DADDI DADD ADD ADDI ADDU ADDIU DSUBU DSUB SUB SUBU AND0 ANDI OR0
   ORI NOR XOR0 XORI LUI DSLL DSLL32 DSLLV DSRA DSRA32 DSRAV DSRL DSRL32 DSRLV SLL
   SLLV SRA SRAV SRL SRLV SLT SLTI SLTU SLTIU MOVN MOVZ MFHI MFLO MTHI MTLO MUL
   MULT MULTU DMULT DMULTU MADD MADDU MSUB MSUBU DIV DIVU DDIV DDIVU J JAL JR JALR
-  BEQ BCMPZ SYSCALL_THREAD_START ImplementationDefinedStopFetching SYSCALL BREAK
-  WAIT TRAPREG TRAPIMM Load Store LWL LWR SWL SWR LDL LDR SDL SDR CACHE PREF SYNC
-  MFC0 HCF MTC0 TLBWI TLBWR TLBR TLBP RDHWR ERET CGetPerm CGetType CGetBase
-  CGetLen CGetTag CGetSealed CGetOffset CGetPCC CGetPCCSetOffset CGetCause
-  CSetCause CReadHwr CWriteHwr CAndPerm CToPtr CSub CPtrCmp CIncOffset
-  CIncOffsetImmediate CSetOffset CSetBounds CSetBoundsImmediate CSetBoundsExact
-  CClearTag CMOVX ClearRegs CFromPtr CBuildCap CCopyType CCheckPerm CCheckType
-  CTestSubset CSeal CCSeal CUnseal CCall CReturn CBX CBZ CJALR CLoad CStore CSC
-  CLC C2Dump RI CGetAddr
-
-termination whileM sorry
+  BEQ BCMPZ SYSCALL BREAK WAIT TRAPREG TRAPIMM Load Store LWL LWR SWL SWR LDL LDR
+  SDL SDR CACHE SYNC MFC0 HCF MTC0 TLBWI TLBWR TLBR TLBP RDHWR ERET CGetPerm
+  CGetType CGetBase CGetLen CGetTag CGetSealed CGetOffset CGetPCC
+  CGetPCCSetOffset CGetCause CSetCause CReadHwr CWriteHwr CAndPerm CToPtr CSub
+  CPtrCmp CIncOffset CIncOffsetImmediate CSetOffset CSetBounds
+  CSetBoundsImmediate CSetBoundsExact CClearTag CMOVX ClearRegs CFromPtr
+  CBuildCap CCopyType CCheckPerm CCheckType CTestSubset CSeal CCSeal CUnseal
+  CCall CReturn CBX CBZ CJALR CLoad CStore CSC CLC C2Dump RI CGetAddr
+
+(* Fake termination proofs of loops for code generation *)
+lemma whileM_dom: "whileM_dom (vars, cond, body)" sorry
+termination whileM using whileM_dom by auto
+lemma whileS_dom: "whileS_dom (vars, cond, body, s)" sorry
+termination whileS using whileS_dom by auto
+
+lemma liftS_whileM: "\<lbrakk>whileM vars cond body\<rbrakk>\<^sub>S = whileS vars (liftS \<circ> cond) (liftS \<circ> body)"
+  by (intro ext liftState_whileM[OF whileS_dom whileM_dom])
+
+(* Pre-lift main loop to state monad to gain some performance *)
+fun mainS :: "unit \<Rightarrow> (regstate, unit, exception) monadS" where
+  "mainS () = \<lbrakk>main ()\<rbrakk>\<^sub>S"
+
+schematic_goal liftS_main[symmetric, code]: "?m = mainS"
+  by (intro ext)
+     (simp add: main_def liftState_simp liftS_whileM comp_def del: whileM.simps whileS.simps
+           cong: bindS_cong if_cong)
+
+fun print_endline' :: "String.literal \<Rightarrow> unit" where "print_endline' _ = ()"
+lemma [code]: "print_endline s = print_endline' (String.implode s)" by auto
 
 fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()"
 lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto
 
+fun prerr_string' :: "String.literal \<Rightarrow> unit" where "prerr_string' _ = ()"
+lemma [code]: "prerr_string s = prerr_string' (String.implode s)" by auto
+
 fun putchar' :: "char \<Rightarrow> unit" where "putchar' _ = ()"
 lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto
 
 code_identifier code_module List \<rightharpoonup> (OCaml) "List0"
 code_printing constant String.implode \<rightharpoonup> (OCaml) "!(let l = _ in let res = Bytes.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> Bytes.set res i c; imp (i + 1) l in imp 0 l)"
 
+code_printing constant print_endline' \<rightharpoonup> (OCaml) "Pervasives.print'_endline"
 code_printing constant prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline"
+code_printing constant prerr_string' \<rightharpoonup> (OCaml) "Pervasives.prerr'_string"
 code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char"
 
 declare insert_code[code del]
@@ -50,12 +73,12 @@ fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exc
      bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\<lambda>_.
      returnS ()))"
 
-definition "initial_state \<equiv> init_state initial_regstate"
+definition "initial_state \<equiv> init_state initial_regstate\<lparr>memstate := (\<lambda>_. Some [B0, B0, B0, B0, B0, B0, B0, B0])\<rparr>"
 
 code_printing constant elf_entry \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Elf'_loader.elf'_entry _))"
 code_printing constant get_time_ns \<rightharpoonup> (OCaml) "(Arith.Int'_of'_integer (Big'_int.big'_int'_of'_int (Pervasives.int'_of'_float (1e9 *. Unix.gettimeofday _))))"
 
-export_code main initial_state liftState get_regval set_regval bindS returnS iteriS iterS
+export_code mainS initial_state liftState get_regval set_regval bindS returnS iteriS iterS
   write_char_mem integer_of_int int_of_integer "op + :: int \<Rightarrow> int \<Rightarrow> int" prerr_results
   in OCaml file "cheri_export.ml"
 
diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml
index 283e4283..c50d525d 100644
--- a/test/isabelle/run_cheri.ml
+++ b/test/isabelle/run_cheri.ml
@@ -64,7 +64,7 @@ let () =
   Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg
 
 let (>>) = Sail2_state_monad.bindS
-let liftS = Sail2_state_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval)
+(*let liftS = Sail2_state_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval)*)
 
 let load_elf_segment seg =
   let open Elf_interpreted_segment in
@@ -89,4 +89,4 @@ let _ =
   (* State_monad.prerr_results *)
     (Cheri_code.initial_state |>
     (Sail2_state.iterS load_elf_segment elf_segments >> (fun _ ->
-    liftS (Cheri.main ()))));
+    (Cheri_code.mainS ()))));