From 5089d9ec81303ce50992084368d3d35f7169d230 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 11 May 2018 14:23:43 +0100 Subject: Add Isabelle code generation for sequential CHERI model --- test/isabelle/Cheri_sequential_code.thy | 64 +++++++++++++++++++++++ test/isabelle/Makefile | 5 ++ test/isabelle/ROOT | 5 ++ test/isabelle/run_cheri_sequential.ml | 91 +++++++++++++++++++++++++++++++++ 4 files changed, 165 insertions(+) create mode 100644 test/isabelle/Cheri_sequential_code.thy create mode 100644 test/isabelle/run_cheri_sequential.ml (limited to 'test/isabelle') 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 \ unit" where "prerr_endline' _ = ()" +lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto + +fun putchar' :: "char \ unit" where "putchar' _ = ()" +lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto + +code_identifier code_module List \ (OCaml) "List0" +code_printing constant String.implode \ (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' \ (OCaml) "Pervasives.prerr'_endline" +code_printing constant putchar' \ (OCaml) "Pervasives.print'_char" + +declare insert_code[code del] +declare union_coset_filter[code del] + +lemma set_union_append[code]: "(set xs) \ (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 \ char \ (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) (\_. + bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\_. + returnS ()))" + +definition "initial_state \ (init_state initial_regstate (\seed. (False, seed)) 0)\memstate := (\_. Some [B0, B0, B0, B0, B0, B0, B0, B0])\" + +code_printing constant elf_entry \ (OCaml) "(Arith.Int'_of'_integer (Elf'_loader.elf'_entry _))" +code_printing constant get_time_ns \ (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 \ int \ 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 ())))); -- cgit v1.2.3 From 3af9f9dfda3972f485cd98b2a2d110c16325b3a3 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 17 May 2018 15:31:11 +0100 Subject: Fix Isabelle->OCaml wrapper --- test/isabelle/run_cheri.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/isabelle') diff --git a/test/isabelle/run_cheri.ml b/test/isabelle/run_cheri.ml index e6d752b7..f51ef4dd 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 (>>) = State_monad.bindS -let liftS = State.liftState (Cheri_types.get_regval, Cheri_types.set_regval) +let liftS = State_lifting.liftState (Cheri_types.get_regval, Cheri_types.set_regval) let load_elf_segment seg = let open Elf_interpreted_segment in -- cgit v1.2.3 From f5672ea6a1e04ad1f2bee91ad86584b183d323b4 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 17 May 2018 16:37:47 +0100 Subject: Clean out old sequential files --- test/isabelle/Cheri_sequential_code.thy | 64 ----------------------- test/isabelle/Makefile | 5 -- test/isabelle/ROOT | 5 -- test/isabelle/run_cheri_sequential.ml | 91 --------------------------------- 4 files changed, 165 deletions(-) delete mode 100644 test/isabelle/Cheri_sequential_code.thy delete mode 100644 test/isabelle/run_cheri_sequential.ml (limited to 'test/isabelle') 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 \ unit" where "prerr_endline' _ = ()" -lemma [code]: "prerr_endline s = prerr_endline' (String.implode s)" by auto - -fun putchar' :: "char \ unit" where "putchar' _ = ()" -lemma [code]: "putchar c = putchar' (char_of_nat (nat c))" by auto - -code_identifier code_module List \ (OCaml) "List0" -code_printing constant String.implode \ (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' \ (OCaml) "Pervasives.prerr'_endline" -code_printing constant putchar' \ (OCaml) "Pervasives.print'_char" - -declare insert_code[code del] -declare union_coset_filter[code del] - -lemma set_union_append[code]: "(set xs) \ (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 \ char \ (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) (\_. - bindS (write_mem_valS BC_bitU_list (bits_of_nat 8 (nat_of_char c))) (\_. - returnS ()))" - -definition "initial_state \ (init_state initial_regstate (\seed. (False, seed)) 0)\memstate := (\_. Some [B0, B0, B0, B0, B0, B0, B0, B0])\" - -code_printing constant elf_entry \ (OCaml) "(Arith.Int'_of'_integer (Elf'_loader.elf'_entry _))" -code_printing constant get_time_ns \ (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 \ int \ 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 ())))); -- cgit v1.2.3