diff options
| -rw-r--r-- | cheri/ROOT | 5 | ||||
| -rw-r--r-- | test/isabelle/Cheri_sequential_code.thy | 64 | ||||
| -rw-r--r-- | test/isabelle/Makefile | 5 | ||||
| -rw-r--r-- | test/isabelle/ROOT | 5 | ||||
| -rw-r--r-- | test/isabelle/run_cheri_sequential.ml | 91 |
5 files changed, 0 insertions, 170 deletions
@@ -2,8 +2,3 @@ session "Sail-CHERI" = "Sail" + options [document = false] theories Cheri_lemmas - -session "Sail-CHERI-Sequential" = "Sail" + - options [document = false] - theories - Cheri_sequential_lemmas diff --git a/test/isabelle/Cheri_sequential_code.thy b/test/isabelle/Cheri_sequential_code.thy deleted file mode 100644 index a7fc19ba..00000000 --- a/test/isabelle/Cheri_sequential_code.thy +++ /dev/null @@ -1,64 +0,0 @@ -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 c66338ee..43028fed 100644 --- a/test/isabelle/Makefile +++ b/test/isabelle/Makefile @@ -11,17 +11,12 @@ 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 28501b26..97544a58 100644 --- a/test/isabelle/ROOT +++ b/test/isabelle/ROOT @@ -3,11 +3,6 @@ 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 deleted file mode 100644 index 9405713d..00000000 --- a/test/isabelle/run_cheri_sequential.ml +++ /dev/null @@ -1,91 +0,0 @@ -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 ())))); |