Add Isabelle code generation for sequential CHERI model

4 files changed, 165 insertions, 0 deletions

diff --git a/test/isabelle/Cheri_sequential_code.thy b/test/isabelle/Cheri_sequential_code.thy
new file mode 100644
index 00000000..a7fc19ba
--- /dev/null
+++ b/test/isabelle/Cheri_sequential_code.thy
@@ -0,0 +1,64 @@
+theory Cheri_sequential_code
+  imports Cheri_sequential_lemmas "HOL-Library.Code_Char" "HOL-Library.Code_Target_Nat" "HOL-Library.Code_Target_Int"
+begin
+
+declare [[code abort: failwith]]
+
+code_datatype
+  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 whileS sorry
+
+fun prerr_endline' :: "String.literal \<Rightarrow> unit" where "prerr_endline' _ = ()"
+lemma [code]: "prerr_endline s = prerr_endline' (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 prerr_endline' \<rightharpoonup> (OCaml) "Pervasives.prerr'_endline"
+code_printing constant putchar' \<rightharpoonup> (OCaml) "Pervasives.print'_char"
+
+declare insert_code[code del]
+declare union_coset_filter[code del]
+
+lemma set_union_append[code]: "(set xs) \<union> (set ys) = set (xs @ ys)"
+  by auto
+
+lemma set_insert_Cons[code]: "insert x (set xs) = set (x # xs)"
+  by auto
+
+declare ast.case[code]
+
+fun write_char_mem :: "int \<Rightarrow> char \<Rightarrow> (regstate, unit, exception) monadS" where
+  "write_char_mem addr c =
+     bindS (write_mem_eaS BC_bitU_list Write_plain (bits_of_int 64 addr) 1) (\<lambda>_.
+     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 (\<lambda>seed. (False, seed)) 0)\<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 _))))"
+
+declare main_def[unfolded seqS_def, code]
+
+export_code main initial_state 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_sequential_export.ml"
+
+end
diff --git a/test/isabelle/Makefile b/test/isabelle/Makefile
index 43028fed..c66338ee 100644
--- a/test/isabelle/Makefile
+++ b/test/isabelle/Makefile
@@ -11,12 +11,17 @@ all: $(TGTS)
 	ocamlbuild -use-ocamlfind -pkg lem -pkg linksem -pkg num -pkg unix $@
 
 run_cheri.native: cheri_export.ml
+run_cheri_sequential.native: cheri_sequential_export.ml
 run_aarch64.native: aarch64_export.ml
 
 cheri_export.ml: Cheri_code.thy
 	make -C $(CHERI_DIR) Cheri.thy
 	isabelle build -c $(SESSION_DIRS) Sail-CHERI-Code
 
+cheri_sequential_export.ml: Cheri_sequential_code.thy
+	make -C $(CHERI_DIR) Cheri_sequential.thy
+	isabelle build -c $(SESSION_DIRS) Sail-CHERI-Sequential-Code
+
 aarch64_export.ml: Aarch64_code.thy
 	make -C $(AARCH64_DIR) Aarch64.thy
 	isabelle build -c $(SESSION_DIRS) Sail-AArch64-Code
diff --git a/test/isabelle/ROOT b/test/isabelle/ROOT
index 97544a58..28501b26 100644
--- a/test/isabelle/ROOT
+++ b/test/isabelle/ROOT
@@ -3,6 +3,11 @@ session "Sail-CHERI-Code" = "Sail-CHERI" +
   theories
     Cheri_code
 
+session "Sail-CHERI-Sequential-Code" = "Sail-CHERI-Sequential" +
+  options [document = false, quick_and_dirty]
+  theories
+    Cheri_sequential_code
+
 session "Sail-AArch64-Code" = "Sail-AArch64" +
   options [document = false, quick_and_dirty]
   theories
diff --git a/test/isabelle/run_cheri_sequential.ml b/test/isabelle/run_cheri_sequential.ml
new file mode 100644
index 00000000..9405713d
--- /dev/null
+++ b/test/isabelle/run_cheri_sequential.ml
@@ -0,0 +1,91 @@
+open Cheri_sequential_export;;
+
+
+
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Elf_loader;;
+
+let opt_file_arguments = ref ([] : string list)
+
+let options = Arg.align []
+
+let usage_msg = "Sail OCaml RTS options:"
+
+let () =
+  Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg
+
+let (>>) = State_monad.bindS
+
+let load_elf_segment seg =
+  let open Elf_interpreted_segment in
+  let bs = seg.elf64_segment_body in
+  let paddr = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_paddr) in
+  let base = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_base) in
+  let offset = Big_int.big_int_of_string (Nat_big_num.to_string seg.elf64_segment_offset) in
+  let writer i byte = Cheri_sequential_code.write_char_mem (Arith.plus_int (Arith.Int_of_integer paddr) i) byte in
+  prerr_endline "\nLoading Segment";
+  prerr_endline ("Segment offset: " ^ Big_int.string_of_big_int offset);
+  prerr_endline ("Segment base address: " ^ Big_int.string_of_big_int base);
+  prerr_endline ("Segment physical address: " ^ Big_int.string_of_big_int paddr);
+  print_segment seg;
+  State.iteriS writer (Byte_sequence.char_list_of_byte_sequence bs)
+
+let _ =
+  Random.self_init ();
+  let elf_segments = match !opt_file_arguments with
+    | f :: _ -> load_elf f
+    | _ -> []
+  in
+  (*State_monad.prerr_results*)
+    (Cheri_sequential_code.initial_state |>
+    (State.iterS load_elf_segment elf_segments >> (fun _ ->
+    (Cheri_sequential.main ()))));