From 200df7e1e8d943811b40be7a7251f969fba8bd1e Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 24 Jan 2017 13:11:07 +0000 Subject: Remember to pass through collapse argument in else case in bit_lifteds_to_string --- src/lem_interp/printing_functions.ml | 2 +- src/lem_interp/run_with_elf_cheri128.ml | 1364 +++++++++++++++++++++++++++++++ 2 files changed, 1365 insertions(+), 1 deletion(-) create mode 100644 src/lem_interp/run_with_elf_cheri128.ml diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 760b0a35..202af6bb 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -150,7 +150,7 @@ let bit_lifteds_to_string ?(collapse=true) (bls: bit_lifted list) (show_length_a else "0x"^s else - simple_bit_lifteds_to_string bls show_length_and_start starto + simple_bit_lifteds_to_string ~collapse:collapse bls show_length_and_start starto let register_value_to_string rv = diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml new file mode 100644 index 00000000..99a6e681 --- /dev/null +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -0,0 +1,1364 @@ +open Printf ;; +open Format ;; +open Big_int ;; +open Interp_ast ;; +open Interp_interface ;; +open Interp_inter_imp ;; +open Run_interp_model ;; +open Sail_impl_base ;; +open Sail_interface ;; + +module StringMap = Map.Make(String) + +let file = ref "" ;; + +let rec foldli f acc ?(i=0) = function + | [] -> acc + | x::xs -> foldli f (f i acc x) ~i:(i+1) xs +;; + +let endian = ref E_big_endian ;; + +let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;; + +let data_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;; +let prog_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;; +let tag_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref);; +let reg = ref Reg.empty ;; +let input_buf = (ref [] : int list ref);; + +let add_mem byte addr mem = + assert(byte >= 0 && byte < 256); + (*Printf.printf "add_mem %s: 0x%02x\n" (Uint64.to_string_hex (Uint64.of_string (Nat_big_num.to_string addr))) byte;*) + let mem_byte = memory_byte_of_int byte in + let zero_byte = memory_byte_of_int 0 in + mem := Mem.add addr mem_byte !mem; + tag_mem := Mem.add addr zero_byte !tag_mem + +let get_reg reg name = + let reg_content = Reg.find name reg in reg_content + +let rec load_memory_segment' (bytes,addr) mem = + match bytes with + | [] -> () + | byte::bytes' -> + let data_byte = Char.code byte in + let addr' = Nat_big_num.succ addr in + begin add_mem data_byte addr mem; + load_memory_segment' (bytes',addr') mem + end + +let rec load_memory_segment (segment: Elf_interpreted_segment.elf64_interpreted_segment) mem = + let (Byte_sequence.Sequence bytes) = segment.Elf_interpreted_segment.elf64_segment_body in + let addr = segment.Elf_interpreted_segment.elf64_segment_paddr in + load_memory_segment' (bytes,addr) mem + + +let rec load_memory_segments segments = + begin match segments with + | [] -> () + | segment::segments' -> + let (x,w,r) = segment.Elf_interpreted_segment.elf64_segment_flags in + begin + load_memory_segment segment prog_mem; + load_memory_segments segments' + end + end + +let rec read_mem mem address length = + if length = 0 + then [] + else + let byte = + try Mem.find address mem with + | Not_found -> failwith "start address not found" + in + byte :: (read_mem mem (Nat_big_num.succ address) (length - 1)) + +let register_state_zero register_data rbn : register_value = + let (dir,width,start_index) = + try List.assoc rbn register_data with + | Not_found -> failwith ("register_state_zero lookup failed (" ^ rbn) + in register_value_zeros dir width start_index + +type model = PPC | AArch64 | MIPS +(* +let ppc_register_data_all = [ + (*Pseudo registers*) + ("CIA", (D_increasing, 64, 0)); + ("NIA", (D_increasing, 64, 0)); + ("mode64bit", (D_increasing, 1, 0)); + ("bigendianmode", (D_increasing, 1, 0)); + (* special registers *) + ("CR", (D_increasing, 32, 32)); + ("CTR", (D_increasing, 64, 0 )); + ("LR", (D_increasing, 64, 0 )); + ("XER", (D_increasing, 64, 0 )); + ("VRSAVE",(D_increasing, 32, 32)); + ("FPSCR", (D_increasing, 64, 0 )); + ("VSCR", (D_increasing, 32, 96)); + + (* general purpose registers *) + ("GPR0", (D_increasing, 64, 0 )); + ("GPR1", (D_increasing, 64, 0 )); + ("GPR2", (D_increasing, 64, 0 )); + ("GPR3", (D_increasing, 64, 0 )); + ("GPR4", (D_increasing, 64, 0 )); + ("GPR5", (D_increasing, 64, 0 )); + ("GPR6", (D_increasing, 64, 0 )); + ("GPR7", (D_increasing, 64, 0 )); + ("GPR8", (D_increasing, 64, 0 )); + ("GPR9", (D_increasing, 64, 0 )); + ("GPR10", (D_increasing, 64, 0 )); + ("GPR11", (D_increasing, 64, 0 )); + ("GPR12", (D_increasing, 64, 0 )); + ("GPR13", (D_increasing, 64, 0 )); + ("GPR14", (D_increasing, 64, 0 )); + ("GPR15", (D_increasing, 64, 0 )); + ("GPR16", (D_increasing, 64, 0 )); + ("GPR17", (D_increasing, 64, 0 )); + ("GPR18", (D_increasing, 64, 0 )); + ("GPR19", (D_increasing, 64, 0 )); + ("GPR20", (D_increasing, 64, 0 )); + ("GPR21", (D_increasing, 64, 0 )); + ("GPR22", (D_increasing, 64, 0 )); + ("GPR23", (D_increasing, 64, 0 )); + ("GPR24", (D_increasing, 64, 0 )); + ("GPR25", (D_increasing, 64, 0 )); + ("GPR26", (D_increasing, 64, 0 )); + ("GPR27", (D_increasing, 64, 0 )); + ("GPR28", (D_increasing, 64, 0 )); + ("GPR29", (D_increasing, 64, 0 )); + ("GPR30", (D_increasing, 64, 0 )); + ("GPR31", (D_increasing, 64, 0 )); + (* vector registers *) + ("VR0", (D_increasing, 128, 0 )); + ("VR1", (D_increasing, 128, 0 )); + ("VR2", (D_increasing, 128, 0 )); + ("VR3", (D_increasing, 128, 0 )); + ("VR4", (D_increasing, 128, 0 )); + ("VR5", (D_increasing, 128, 0 )); + ("VR6", (D_increasing, 128, 0 )); + ("VR7", (D_increasing, 128, 0 )); + ("VR8", (D_increasing, 128, 0 )); + ("VR9", (D_increasing, 128, 0 )); + ("VR10", (D_increasing, 128, 0 )); + ("VR11", (D_increasing, 128, 0 )); + ("VR12", (D_increasing, 128, 0 )); + ("VR13", (D_increasing, 128, 0 )); + ("VR14", (D_increasing, 128, 0 )); + ("VR15", (D_increasing, 128, 0 )); + ("VR16", (D_increasing, 128, 0 )); + ("VR17", (D_increasing, 128, 0 )); + ("VR18", (D_increasing, 128, 0 )); + ("VR19", (D_increasing, 128, 0 )); + ("VR20", (D_increasing, 128, 0 )); + ("VR21", (D_increasing, 128, 0 )); + ("VR22", (D_increasing, 128, 0 )); + ("VR23", (D_increasing, 128, 0 )); + ("VR24", (D_increasing, 128, 0 )); + ("VR25", (D_increasing, 128, 0 )); + ("VR26", (D_increasing, 128, 0 )); + ("VR27", (D_increasing, 128, 0 )); + ("VR28", (D_increasing, 128, 0 )); + ("VR29", (D_increasing, 128, 0 )); + ("VR30", (D_increasing, 128, 0 )); + ("VR31", (D_increasing, 128, 0 )); + (* floating-point registers *) + ("FPR0", (D_increasing, 64, 0 )); + ("FPR1", (D_increasing, 64, 0 )); + ("FPR2", (D_increasing, 64, 0 )); + ("FPR3", (D_increasing, 64, 0 )); + ("FPR4", (D_increasing, 64, 0 )); + ("FPR5", (D_increasing, 64, 0 )); + ("FPR6", (D_increasing, 64, 0 )); + ("FPR7", (D_increasing, 64, 0 )); + ("FPR8", (D_increasing, 64, 0 )); + ("FPR9", (D_increasing, 64, 0 )); + ("FPR10", (D_increasing, 64, 0 )); + ("FPR11", (D_increasing, 64, 0 )); + ("FPR12", (D_increasing, 64, 0 )); + ("FPR13", (D_increasing, 64, 0 )); + ("FPR14", (D_increasing, 64, 0 )); + ("FPR15", (D_increasing, 64, 0 )); + ("FPR16", (D_increasing, 64, 0 )); + ("FPR17", (D_increasing, 64, 0 )); + ("FPR18", (D_increasing, 64, 0 )); + ("FPR19", (D_increasing, 64, 0 )); + ("FPR20", (D_increasing, 64, 0 )); + ("FPR21", (D_increasing, 64, 0 )); + ("FPR22", (D_increasing, 64, 0 )); + ("FPR23", (D_increasing, 64, 0 )); + ("FPR24", (D_increasing, 64, 0 )); + ("FPR25", (D_increasing, 64, 0 )); + ("FPR26", (D_increasing, 64, 0 )); + ("FPR27", (D_increasing, 64, 0 )); + ("FPR28", (D_increasing, 64, 0 )); + ("FPR29", (D_increasing, 64, 0 )); + ("FPR30", (D_increasing, 64, 0 )); + ("FPR31", (D_increasing, 64, 0 )); +] + +let initial_stack_and_reg_data_of_PPC_elf_file e_entry all_data_memory = + (* set up initial registers, per 3.4.1 of 64-bit PowerPC ELF Application Binary Interface Supplement 1.9 *) + + let auxiliary_vector_space = Nat_big_num.of_string "17592186042368" (*"0xffffffff800"*) in + (* notionally there should be at least an AT_NULL auxiliary vector entry there, but our examples will never read it *) + + (* take start of stack roughly where running gdb on hello5 on bim says it is*) + let initial_GPR1_stack_pointer = Nat_big_num.of_string "17592186040320" (*"0xffffffff000"*) in + let initial_GPR1_stack_pointer_value = + Sail_impl_base.register_value_of_integer 64 0 Sail_impl_base.D_increasing initial_GPR1_stack_pointer in + (* ELF says we need an initial zero doubleword there *) + let initial_stack_data = + (* the code actually uses the stack, both above and below, so we map a bit more memory*) + (* this is a fairly big but arbitrary chunk *) + (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in + [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *) + (* this is the stack memory that test 1938 actually uses *) + [ ("initial_stack_data1", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128), + Lem_list.replicate 8 0 ); + ("initial_stack_data2", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 8), + Lem_list.replicate 8 0 ); + ("initial_stack_data3", Nat_big_num.add initial_GPR1_stack_pointer (Nat_big_num.of_int 16), + Lem_list.replicate 8 0 )] in + + (* read TOC from the second field of the function descriptor pointed to by e_entry*) + let initial_GPR2_TOC = + Sail_impl_base.register_value_of_address + (Sail_impl_base.address_of_byte_list + (List.map (fun b -> match b with Some b -> b | None -> failwith "Address had undefined") + (List.map byte_of_byte_lifted + (read_mem all_data_memory + (Nat_big_num.add (Nat_big_num.of_int 8) e_entry) 8)))) + Sail_impl_base.D_increasing in + (* these initial register values are all mandated to be zero, but that's handled by the generic zeroing below + let initial_GPR3_argc = (Nat_big_num.of_int 0) in + let initial_GPR4_argv = (Nat_big_num.of_int 0) in + let initial_GPR5_envp = (Nat_big_num.of_int 0) in + let initial_FPSCR = (Nat_big_num.of_int 0) in + *) + let initial_register_abi_data : (string * Sail_impl_base.register_value) list = + [ ("GPR1", initial_GPR1_stack_pointer_value); + ("GPR2", initial_GPR2_TOC); + (* + ("GPR3", initial_GPR3_argc); + ("GPR4", initial_GPR4_argv); + ("GPR5", initial_GPR5_envp); + ("FPSCR", initial_FPSCR); + *) + ] in + + (initial_stack_data, initial_register_abi_data) + + +let aarch64_reg bit_count name = (name, (D_decreasing, bit_count, bit_count - 1)) + +let aarch64_PC_data = [aarch64_reg 64 "_PC"] + +(* most of the PSTATE fields are aliases to other registers so they + don't appear here *) +let aarch64_PSTATE_data = [ + aarch64_reg 1 "PSTATE_nRW"; + aarch64_reg 1 "PSTATE_E"; + aarch64_reg 5 "PSTATE_M"; +] + +let aarch64_general_purpose_registers_data = [ + aarch64_reg 64 "R0"; + aarch64_reg 64 "R1"; + aarch64_reg 64 "R2"; + aarch64_reg 64 "R3"; + aarch64_reg 64 "R4"; + aarch64_reg 64 "R5"; + aarch64_reg 64 "R6"; + aarch64_reg 64 "R7"; + aarch64_reg 64 "R8"; + aarch64_reg 64 "R9"; + aarch64_reg 64 "R10"; + aarch64_reg 64 "R11"; + aarch64_reg 64 "R12"; + aarch64_reg 64 "R13"; + aarch64_reg 64 "R14"; + aarch64_reg 64 "R15"; + aarch64_reg 64 "R16"; + aarch64_reg 64 "R17"; + aarch64_reg 64 "R18"; + aarch64_reg 64 "R19"; + aarch64_reg 64 "R20"; + aarch64_reg 64 "R21"; + aarch64_reg 64 "R22"; + aarch64_reg 64 "R23"; + aarch64_reg 64 "R24"; + aarch64_reg 64 "R25"; + aarch64_reg 64 "R26"; + aarch64_reg 64 "R27"; + aarch64_reg 64 "R28"; + aarch64_reg 64 "R29"; + aarch64_reg 64 "R30"; +] + +let aarch64_SIMD_registers_data = [ + aarch64_reg 128 "V0"; + aarch64_reg 128 "V1"; + aarch64_reg 128 "V2"; + aarch64_reg 128 "V3"; + aarch64_reg 128 "V4"; + aarch64_reg 128 "V5"; + aarch64_reg 128 "V6"; + aarch64_reg 128 "V7"; + aarch64_reg 128 "V8"; + aarch64_reg 128 "V9"; + aarch64_reg 128 "V10"; + aarch64_reg 128 "V11"; + aarch64_reg 128 "V12"; + aarch64_reg 128 "V13"; + aarch64_reg 128 "V14"; + aarch64_reg 128 "V15"; + aarch64_reg 128 "V16"; + aarch64_reg 128 "V17"; + aarch64_reg 128 "V18"; + aarch64_reg 128 "V19"; + aarch64_reg 128 "V20"; + aarch64_reg 128 "V21"; + aarch64_reg 128 "V22"; + aarch64_reg 128 "V23"; + aarch64_reg 128 "V24"; + aarch64_reg 128 "V25"; + aarch64_reg 128 "V26"; + aarch64_reg 128 "V27"; + aarch64_reg 128 "V28"; + aarch64_reg 128 "V29"; + aarch64_reg 128 "V30"; + aarch64_reg 128 "V31"; +] + +let aarch64_special_purpose_registers_data = [ + aarch64_reg 32 "CurrentEL"; + aarch64_reg 32 "DAIF"; + aarch64_reg 32 "NZCV"; + aarch64_reg 64 "SP_EL0"; + aarch64_reg 64 "SP_EL1"; + aarch64_reg 64 "SP_EL2"; + aarch64_reg 64 "SP_EL3"; + aarch64_reg 32 "SPSel"; + aarch64_reg 32 "SPSR_EL1"; + aarch64_reg 32 "SPSR_EL2"; + aarch64_reg 32 "SPSR_EL3"; + aarch64_reg 64 "ELR_EL1"; + aarch64_reg 64 "ELR_EL2"; + aarch64_reg 64 "ELR_EL3"; +] + +let aarch64_general_system_control_registers_data = [ + aarch64_reg 64 "HCR_EL2"; + aarch64_reg 64 "ID_AA64MMFR0_EL1"; + aarch64_reg 64 "RVBAR_EL1"; + aarch64_reg 64 "RVBAR_EL2"; + aarch64_reg 64 "RVBAR_EL3"; + aarch64_reg 32 "SCR_EL3"; + aarch64_reg 32 "SCTLR_EL1"; + aarch64_reg 32 "SCTLR_EL2"; + aarch64_reg 32 "SCTLR_EL3"; + aarch64_reg 64 "TCR_EL1"; + aarch64_reg 32 "TCR_EL2"; + aarch64_reg 32 "TCR_EL3"; +] + +let aarch64_debug_registers_data = [ + aarch64_reg 32 "DBGPRCR_EL1"; + aarch64_reg 32 "OSDLR_EL1"; +] + +let aarch64_performance_monitors_registers_data = [] +let aarch64_generic_timer_registers_data = [] +let aarch64_generic_interrupt_controller_CPU_interface_registers_data = [] + +let aarch64_external_debug_registers_data = [ + aarch64_reg 32 "EDSCR"; +] + +let aarch32_general_system_control_registers_data = [ + aarch64_reg 32 "SCR"; +] + +let aarch32_debug_registers_data = [ + aarch64_reg 32 "DBGOSDLR"; + aarch64_reg 32 "DBGPRCR"; +] + +let aarch64_register_data_all = + aarch64_PC_data @ + aarch64_PSTATE_data @ + aarch64_general_purpose_registers_data @ + aarch64_SIMD_registers_data @ + aarch64_special_purpose_registers_data @ + aarch64_general_system_control_registers_data @ + aarch64_debug_registers_data @ + aarch64_performance_monitors_registers_data @ + aarch64_generic_timer_registers_data @ + aarch64_generic_interrupt_controller_CPU_interface_registers_data @ + aarch64_external_debug_registers_data @ + aarch32_general_system_control_registers_data @ + aarch32_debug_registers_data + +let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory = + let (reg_SP_EL0_direction, reg_SP_EL0_width, reg_SP_EL0_initial_index) = + List.assoc "SP_EL0" aarch64_register_data_all in + + (* we compiled a small program that prints out SP and run it a few + times on the Nexus9, these are the results: + 0x0000007fe7f903e0 + 0x0000007fdcdbf3f0 + 0x0000007fcbe1ba90 + 0x0000007fcf378280 + 0x0000007fdd54b8d0 + 0x0000007fd961bc10 + 0x0000007ff3be6350 + 0x0000007fd6bf6ef0 + 0x0000007fff7676f0 + 0x0000007ff2c34560 *) + let initial_SP_EL0 = Nat_big_num.of_string "549739036672" (*"0x0000007fff000000"*) in + let initial_SP_EL0_value = + Sail_impl_base.register_value_of_integer + reg_SP_EL0_width + reg_SP_EL0_initial_index + reg_SP_EL0_direction + initial_SP_EL0 + in + + (* ELF says we need an initial zero doubleword there *) + (* the code actually uses the stack, both above and below, so we map a bit more memory*) + let initial_stack_data = + (* this is a fairly big but arbitrary chunk: *) + (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in + [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *) + + [ ("initial_stack_data1", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 16), Lem_list.replicate 8 0); + ("initial_stack_data2", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 8), Lem_list.replicate 8 0) + ] + in + + let initial_register_abi_data : (string * Sail_impl_base.register_value) list = + [("SP_EL0", initial_SP_EL0_value)] + in + + (initial_stack_data, initial_register_abi_data) +*) + +let mips_register_data_all = [ + (*Pseudo registers*) + ("PC", (D_decreasing, 64, 63)); + ("branchPending", (D_decreasing, 1, 0)); + ("inBranchDelay", (D_decreasing, 1, 0)); + ("delayedPC", (D_decreasing, 64, 63)); + ("nextPC", (D_decreasing, 64, 63)); + (* General purpose registers *) + ("GPR00", (D_decreasing, 64, 63)); + ("GPR01", (D_decreasing, 64, 63)); + ("GPR02", (D_decreasing, 64, 63)); + ("GPR03", (D_decreasing, 64, 63)); + ("GPR04", (D_decreasing, 64, 63)); + ("GPR05", (D_decreasing, 64, 63)); + ("GPR06", (D_decreasing, 64, 63)); + ("GPR07", (D_decreasing, 64, 63)); + ("GPR08", (D_decreasing, 64, 63)); + ("GPR09", (D_decreasing, 64, 63)); + ("GPR10", (D_decreasing, 64, 63)); + ("GPR11", (D_decreasing, 64, 63)); + ("GPR12", (D_decreasing, 64, 63)); + ("GPR13", (D_decreasing, 64, 63)); + ("GPR14", (D_decreasing, 64, 63)); + ("GPR15", (D_decreasing, 64, 63)); + ("GPR16", (D_decreasing, 64, 63)); + ("GPR17", (D_decreasing, 64, 63)); + ("GPR18", (D_decreasing, 64, 63)); + ("GPR19", (D_decreasing, 64, 63)); + ("GPR20", (D_decreasing, 64, 63)); + ("GPR21", (D_decreasing, 64, 63)); + ("GPR22", (D_decreasing, 64, 63)); + ("GPR23", (D_decreasing, 64, 63)); + ("GPR24", (D_decreasing, 64, 63)); + ("GPR25", (D_decreasing, 64, 63)); + ("GPR26", (D_decreasing, 64, 63)); + ("GPR27", (D_decreasing, 64, 63)); + ("GPR28", (D_decreasing, 64, 63)); + ("GPR29", (D_decreasing, 64, 63)); + ("GPR30", (D_decreasing, 64, 63)); + ("GPR31", (D_decreasing, 64, 63)); + (* special registers for mul/div *) + ("HI", (D_decreasing, 64, 63)); + ("LO", (D_decreasing, 64, 63)); + (* control registers *) + ("CP0Status", (D_decreasing, 32, 31)); + ("CP0Cause", (D_decreasing, 32, 31)); + ("CP0EPC", (D_decreasing, 64, 63)); + ("CP0LLAddr", (D_decreasing, 64, 63)); + ("CP0LLBit", (D_decreasing, 1, 0)); + ("CP0Count", (D_decreasing, 32, 31)); + ("CP0Compare", (D_decreasing, 32, 31)); + ("CP0HWREna", (D_decreasing, 32, 31)); + ("CP0UserLocal", (D_decreasing, 64, 63)); + ("CP0BadVAddr", (D_decreasing, 64, 63)); + ("TLBProbe" ,(D_decreasing, 1, 0)); + ("TLBIndex" ,(D_decreasing, 6, 5)); + ("TLBRandom" ,(D_decreasing, 6, 5)); + ("TLBEntryLo0",(D_decreasing, 64, 63)); + ("TLBEntryLo1",(D_decreasing, 64, 63)); + ("TLBContext" ,(D_decreasing, 64, 63)); + ("TLBPageMask",(D_decreasing, 16, 15)); + ("TLBWired" ,(D_decreasing, 6, 5)); + ("TLBEntryHi" ,(D_decreasing, 64, 63)); + ("TLBXContext",(D_decreasing, 64, 63)); + + ("TLBEntry00" ,(D_decreasing, 117, 116)); + ("TLBEntry01" ,(D_decreasing, 117, 116)); + ("TLBEntry02" ,(D_decreasing, 117, 116)); + ("TLBEntry03" ,(D_decreasing, 117, 116)); + ("TLBEntry04" ,(D_decreasing, 117, 116)); + ("TLBEntry05" ,(D_decreasing, 117, 116)); + ("TLBEntry06" ,(D_decreasing, 117, 116)); + ("TLBEntry07" ,(D_decreasing, 117, 116)); + ("TLBEntry08" ,(D_decreasing, 117, 116)); + ("TLBEntry09" ,(D_decreasing, 117, 116)); + ("TLBEntry10" ,(D_decreasing, 117, 116)); + ("TLBEntry11" ,(D_decreasing, 117, 116)); + ("TLBEntry12" ,(D_decreasing, 117, 116)); + ("TLBEntry13" ,(D_decreasing, 117, 116)); + ("TLBEntry14" ,(D_decreasing, 117, 116)); + ("TLBEntry15" ,(D_decreasing, 117, 116)); + ("TLBEntry16" ,(D_decreasing, 117, 116)); + ("TLBEntry17" ,(D_decreasing, 117, 116)); + ("TLBEntry18" ,(D_decreasing, 117, 116)); + ("TLBEntry19" ,(D_decreasing, 117, 116)); + ("TLBEntry20" ,(D_decreasing, 117, 116)); + ("TLBEntry21" ,(D_decreasing, 117, 116)); + ("TLBEntry22" ,(D_decreasing, 117, 116)); + ("TLBEntry23" ,(D_decreasing, 117, 116)); + ("TLBEntry24" ,(D_decreasing, 117, 116)); + ("TLBEntry25" ,(D_decreasing, 117, 116)); + ("TLBEntry26" ,(D_decreasing, 117, 116)); + ("TLBEntry27" ,(D_decreasing, 117, 116)); + ("TLBEntry28" ,(D_decreasing, 117, 116)); + ("TLBEntry29" ,(D_decreasing, 117, 116)); + ("TLBEntry30" ,(D_decreasing, 117, 116)); + ("TLBEntry31" ,(D_decreasing, 117, 116)); + ("TLBEntry32" ,(D_decreasing, 117, 116)); + ("TLBEntry33" ,(D_decreasing, 117, 116)); + ("TLBEntry34" ,(D_decreasing, 117, 116)); + ("TLBEntry35" ,(D_decreasing, 117, 116)); + ("TLBEntry36" ,(D_decreasing, 117, 116)); + ("TLBEntry37" ,(D_decreasing, 117, 116)); + ("TLBEntry38" ,(D_decreasing, 117, 116)); + ("TLBEntry39" ,(D_decreasing, 117, 116)); + ("TLBEntry40" ,(D_decreasing, 117, 116)); + ("TLBEntry41" ,(D_decreasing, 117, 116)); + ("TLBEntry42" ,(D_decreasing, 117, 116)); + ("TLBEntry43" ,(D_decreasing, 117, 116)); + ("TLBEntry44" ,(D_decreasing, 117, 116)); + ("TLBEntry45" ,(D_decreasing, 117, 116)); + ("TLBEntry46" ,(D_decreasing, 117, 116)); + ("TLBEntry47" ,(D_decreasing, 117, 116)); + ("TLBEntry48" ,(D_decreasing, 117, 116)); + ("TLBEntry49" ,(D_decreasing, 117, 116)); + ("TLBEntry50" ,(D_decreasing, 117, 116)); + ("TLBEntry51" ,(D_decreasing, 117, 116)); + ("TLBEntry52" ,(D_decreasing, 117, 116)); + ("TLBEntry53" ,(D_decreasing, 117, 116)); + ("TLBEntry54" ,(D_decreasing, 117, 116)); + ("TLBEntry55" ,(D_decreasing, 117, 116)); + ("TLBEntry56" ,(D_decreasing, 117, 116)); + ("TLBEntry57" ,(D_decreasing, 117, 116)); + ("TLBEntry58" ,(D_decreasing, 117, 116)); + ("TLBEntry59" ,(D_decreasing, 117, 116)); + ("TLBEntry60" ,(D_decreasing, 117, 116)); + ("TLBEntry61" ,(D_decreasing, 117, 116)); + ("TLBEntry62" ,(D_decreasing, 117, 116)); + ("TLBEntry63" ,(D_decreasing, 117, 116)); + + ("UART_WDATA" ,(D_decreasing, 8, 7)); + ("UART_RDATA" ,(D_decreasing, 8, 7)); + ("UART_WRITTEN" ,(D_decreasing, 1, 0)); + ("UART_RVALID" ,(D_decreasing, 1, 0)); +] + +let cheri_register_data_all = mips_register_data_all @ [ + ("CapCause", (D_decreasing, 16, 15)); + ("PCC", (D_decreasing, 129, 128)); + ("nextPCC", (D_decreasing, 129, 128)); + ("delayedPCC", (D_decreasing, 129, 128)); + ("C00", (D_decreasing, 129, 128)); + ("C01", (D_decreasing, 129, 128)); + ("C02", (D_decreasing, 129, 128)); + ("C03", (D_decreasing, 129, 128)); + ("C04", (D_decreasing, 129, 128)); + ("C05", (D_decreasing, 129, 128)); + ("C06", (D_decreasing, 129, 128)); + ("C07", (D_decreasing, 129, 128)); + ("C08", (D_decreasing, 129, 128)); + ("C09", (D_decreasing, 129, 128)); + ("C10", (D_decreasing, 129, 128)); + ("C11", (D_decreasing, 129, 128)); + ("C12", (D_decreasing, 129, 128)); + ("C13", (D_decreasing, 129, 128)); + ("C14", (D_decreasing, 129, 128)); + ("C15", (D_decreasing, 129, 128)); + ("C16", (D_decreasing, 129, 128)); + ("C17", (D_decreasing, 129, 128)); + ("C18", (D_decreasing, 129, 128)); + ("C19", (D_decreasing, 129, 128)); + ("C20", (D_decreasing, 129, 128)); + ("C21", (D_decreasing, 129, 128)); + ("C22", (D_decreasing, 129, 128)); + ("C23", (D_decreasing, 129, 128)); + ("C24", (D_decreasing, 129, 128)); + ("C25", (D_decreasing, 129, 128)); + ("C26", (D_decreasing, 129, 128)); + ("C27", (D_decreasing, 129, 128)); + ("C28", (D_decreasing, 129, 128)); + ("C29", (D_decreasing, 129, 128)); + ("C30", (D_decreasing, 129, 128)); + ("C31", (D_decreasing, 129, 128)); +] + +let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory = + let initial_stack_data = [] in + let initial_cap_val_int = Nat_big_num.of_string "0x1fffe5a00000800000000000000000000" in (* hex((0x80000 << 64) + (45 << 105) + (0x7fff << 113) + (1 << 128)) *) + let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing initial_cap_val_int in + let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [ + ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000")); + ("PCC", initial_cap_val_reg); + ("nextPCC", initial_cap_val_reg); + ("delayedPCC", initial_cap_val_reg); + ("C00", initial_cap_val_reg); + ("C01", initial_cap_val_reg); + ("C02", initial_cap_val_reg); + ("C03", initial_cap_val_reg); + ("C04", initial_cap_val_reg); + ("C05", initial_cap_val_reg); + ("C06", initial_cap_val_reg); + ("C07", initial_cap_val_reg); + ("C08", initial_cap_val_reg); + ("C09", initial_cap_val_reg); + ("C10", initial_cap_val_reg); + ("C11", initial_cap_val_reg); + ("C12", initial_cap_val_reg); + ("C13", initial_cap_val_reg); + ("C14", initial_cap_val_reg); + ("C15", initial_cap_val_reg); + ("C16", initial_cap_val_reg); + ("C17", initial_cap_val_reg); + ("C18", initial_cap_val_reg); + ("C19", initial_cap_val_reg); + ("C20", initial_cap_val_reg); + ("C21", initial_cap_val_reg); + ("C22", initial_cap_val_reg); + ("C23", initial_cap_val_reg); + ("C24", initial_cap_val_reg); + ("C25", initial_cap_val_reg); + ("C26", initial_cap_val_reg); + ("C27", initial_cap_val_reg); + ("C28", initial_cap_val_reg); + ("C29", initial_cap_val_reg); + ("C30", initial_cap_val_reg); + ("C31", initial_cap_val_reg); + ] in + (initial_stack_data, initial_register_abi_data) + +let initial_reg_file reg_data init = + List.iter (fun (reg_name, _) -> reg := Reg.add reg_name (init reg_name) !reg) reg_data + +let initial_system_state_of_elf_file name = + + (* call ELF analyser on file *) + match Sail_interface.populate_and_obtain_global_symbol_init_info name with + | Error.Fail s -> failwith ("populate_and_obtain_global_symbol_init_info: " ^ s) + | Error.Success + (_, (elf_epi: Sail_interface.executable_process_image), + (symbol_map: Elf_file.global_symbol_init_info)) + -> + let (segments, e_entry, e_machine) = + begin match elf_epi with + | ELF_Class_32 _ -> failwith "cannot handle ELF_Class_32" + | ELF_Class_64 (segments,e_entry,e_machine) -> + (* remove all the auto generated segments (they contain only 0s) *) + let segments = + Lem_list.mapMaybe + (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) + segments + in + (segments,e_entry,e_machine) + end + in + + (* construct program memory and start address *) + begin + prog_mem := Mem.empty; + data_mem := Mem.empty; + tag_mem := Mem.empty; + load_memory_segments segments; + (* + debugf "prog_mem\n"; + Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !prog_mem; + debugf "data_mem\n"; + Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !data_mem; + *) + let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr, + initial_stack_data, initial_register_abi_data, register_data_all) = + match Nat_big_num.to_int e_machine with +(* | 21 (* EM_PPC64 *) -> + let startaddr = + let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in + match Abi_power64.abi_power64_compute_program_entry_point segments e_entry with + | Error.Fail s -> failwith "Failed computing entry point" + | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s) + in + let (initial_stack_data, initial_register_abi_data) = + initial_stack_and_reg_data_of_PPC_elf_file e_entry !data_mem in + + (Power.defs, + (Power_extras.read_memory_functions,Power_extras.memory_writes,[],[],Power_extras.barrier_functions), + Power_extras.power_externs, + PPC, + D_increasing, + startaddr, + initial_stack_data, + initial_register_abi_data, + ppc_register_data_all) + + | 183 (* EM_AARCH64 *) -> + let startaddr = + let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in + match Abi_aarch64_le.abi_aarch64_le_compute_program_entry_point segments e_entry with + | Error.Fail s -> failwith "Failed computing entry point" + | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s) + in + + let (initial_stack_data, initial_register_abi_data) = + initial_stack_and_reg_data_of_AAarch64_elf_file e_entry !data_mem in + + (ArmV8.defs, + (ArmV8_extras.aArch64_read_memory_functions, + ArmV8_extras.aArch64_memory_writes, + ArmV8_extras.aArch64_memory_eas, + ArmV8_extras.aArch64_memory_vals, + ArmV8_extras.aArch64_barrier_functions), + [], + AArch64, + D_decreasing, + startaddr, + initial_stack_data, + initial_register_abi_data, + aarch64_register_data_all) *) + | 8 (* EM_MIPS *) -> + let startaddr = + let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with + | Error.Fail s -> failwith "Failed computing entry point" + | Error.Success s -> s + in + let (initial_stack_data, initial_register_abi_data) = + initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in + + (Cheri128.defs, + (Mips_extras.read_memory_functions, + Mips_extras.memory_writes, + Mips_extras.memory_eas, + Mips_extras.memory_vals, + Mips_extras.barrier_functions), + [], + MIPS, + D_decreasing, + startaddr, + initial_stack_data, + initial_register_abi_data, + cheri_register_data_all) + + | _ -> failwith (Printf.sprintf "Sail sequential interpreter can't handle the e_machine value %s, only EM_PPC64, EM_AARCH64 and EM_MIPS are supported." (Nat_big_num.to_string e_machine)) + in + + (* pull the object symbols from the symbol table *) + let symbol_table : (string * Nat_big_num.num * int * word8 list (*their bytes*)) list = + let rec convert_symbol_table symbol_map = + begin match symbol_map with + | [] -> [] + | ((name: string), + ((typ: Nat_big_num.num), + (size: Nat_big_num.num (*number of bytes*)), + (address: Nat_big_num.num), + (mb: Byte_sequence.byte_sequence option (*present iff type=stt_object*)), + (binding: Nat_big_num.num))) + (* (mb: Byte_sequence_wrapper.t option (*present iff type=stt_object*)) )) *) + ::symbol_map' -> + if Nat_big_num.equal typ Elf_symbol_table.stt_object && not (Nat_big_num.equal size (Nat_big_num.of_int 0)) + then + ( + (* an object symbol - map *) + (*Printf.printf "*** size %d ***\n" (Nat_big_num.to_int size);*) + let bytes = + (match mb with + | None -> raise (Failure "this cannot happen") + | Some (Sequence bytes) -> + List.map (fun (c:char) -> Char.code c) bytes) in + (name, address, List.length bytes, bytes):: convert_symbol_table symbol_map' + ) + else + (* not an object symbol or of zero size - ignore *) + convert_symbol_table symbol_map' + end + in + (List.map (fun (n,a,bs) -> (n,a,List.length bs,bs)) initial_stack_data) @ convert_symbol_table symbol_map + in + + (* invert the symbol table to use for pp *) + let symbol_table_pp : ((Sail_impl_base.address * int) * string) list = + (* map symbol to (bindings, footprint), + if a symbol appears more then onece keep the one with higher + precedence (stb_global > stb_weak > stb_local) *) + let map = + List.fold_left + (fun map (name, (typ, size, address, mb, binding)) -> + if String.length name <> 0 && + (if String.length name = 1 then Char.code (String.get name 0) <> 0 else true) && + not (Nat_big_num.equal address (Nat_big_num.of_int 0)) + then + try + let (binding', _) = StringMap.find name map in + if Nat_big_num.equal binding' Elf_symbol_table.stb_local || + Nat_big_num.equal binding Elf_symbol_table.stb_global + then + StringMap.add name (binding, + (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map + else map + with Not_found -> + StringMap.add name (binding, + (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map + + else map + ) + StringMap.empty + symbol_map + in + + List.map (fun (name, (binding, fp)) -> (fp, name)) (StringMap.bindings map) + in + + + (* Now we examine the rest of the data memory, + removing the footprint of the symbols and chunking it into aligned chunks *) + + let rec remove_symbols_from_data_memory data_mem symbols = + match symbols with + | [] -> data_mem + | (name,address,size,bs)::symbols' -> + let data_mem' = + Mem.filter + (fun a v -> + not (Nat_big_num.greater_equal a address && + Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address))) + data_mem in + remove_symbols_from_data_memory data_mem' symbols' in + + let trimmed_data_memory : (Nat_big_num.num * memory_byte) list = + Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in + + (* make sure that's ordered increasingly.... *) + let trimmed_data_memory = + List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in + + let aligned a n = (* a mod n = 0 *) + let n_big = Nat_big_num.of_int n in + Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in + + let isplus a' a n = (* a' = a+n *) + Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in + + let rec chunk_data_memory dm = + match dm with + | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::(a4,b4)::(a5,b5)::(a6,b6)::(a7,b7)::dm' when + (aligned a0 8 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3 && + isplus a4 a0 4 && isplus a5 a0 5 && isplus a6 a0 6 && isplus a7 a0 7) -> + (a0,8,[b0;b1;b2;b3;b4;b5;b6;b7]) :: chunk_data_memory dm' + | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::dm' when + (aligned a0 4 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3) -> + (a0,4,[b0;b1;b2;b3]) :: chunk_data_memory dm' + | (a0,b0)::(a1,b1)::dm' when + (aligned a0 2 && isplus a1 a0 1) -> + (a0,2,[b0;b1]) :: chunk_data_memory dm' + | (a0,b0)::dm' -> + (a0,1,[b0]):: chunk_data_memory dm' + | [] -> [] in + + let initial_register_state = + fun rbn -> + try + List.assoc rbn initial_register_abi_data + with + Not_found -> + (register_state_zero register_data_all) rbn + in + + begin + (initial_reg_file register_data_all initial_register_state); + + (* construct initial system state *) + let initial_system_state = + (isa_defs, + isa_memory_access, + isa_externs, + isa_model, + model_reg_d, + startaddr, + (Sail_impl_base.address_of_integer startaddr)) + in + + (initial_system_state, symbol_table_pp) + end + end + +let eager_eval = ref true +let break_point = ref false +let break_instr = ref 0 +let max_cut_off = ref false +let max_instr = ref 0 +let raw_file = ref "" +let raw_at = ref 0 + +let args = [ + ("--file", Arg.Set_string file, "filename of elf binary to load in memory"); + ("--quiet", Arg.Clear Run_interp_model.interact_print, "do not display per-instruction actions"); + ("--silent", Arg.Tuple [Arg.Clear Run_interp_model.error_print; + Arg.Clear Run_interp_model.interact_print; + Arg.Clear Run_interp_model.result_print], + "do not dispaly error messages, per-instruction actions, or results"); + ("--no_result", Arg.Clear Run_interp_model.result_print, "do not display final register values"); + ("--interactive", Arg.Clear eager_eval , "interactive execution"); + ("--breakpoint", Arg.Int (fun i -> break_point := true; break_instr:= i), "run to instruction number i, then run interactively"); + ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop"); + ("--raw", Arg.Set_string raw_file, "filename of raw file to load in memory"); + ("--at", Arg.Set_int raw_at, "address to load raw file in memory"); +] + +let time_it action arg = + let start_time = Sys.time () in + ignore (action arg); + let finish_time = Sys.time () in + finish_time -. start_time + +(*TODO MIPS specific, should print final register values under all models*) +let rec debug_print_gprs start stop = + resultf "DEBUG MIPS REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "GPR%02d" start) !reg)); + if start < stop + then debug_print_gprs (start + 1) stop + else () + +let rec debug_print_capregs start stop = + resultf "DEBUG CAP REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "C%02d" start) !reg)); + if start < stop + then debug_print_capregs (start + 1) stop + else () + +let stop_condition_met model instr = + match model with + | PPC -> + (match instr with + | ("Sc", [("Lev", _, arg)]) -> + Nat_big_num.equal (integer_of_bit_list arg) (Nat_big_num.of_int 32) + | _ -> false) + | AArch64 -> (match instr with + | ("ImplementationDefinedStopFetching", _) -> true + | _ -> false) + | MIPS -> (match instr with + | ("HCF", _) -> + resultf "DEBUG MIPS PC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg)); + debug_print_gprs 0 31; + resultf "DEBUG CAP PCC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PCC" !reg)); + debug_print_capregs 0 31; + true + | _ -> false) + +let is_branch model instruction = + let (name,_,_) = instruction in + match (model , name) with + | (PPC, "B") -> true + | (PPC, "Bc") -> true + | (PPC, "Bclr") -> true + | (PPC, "Bcctr") -> true + | (PPC, _) -> false + | (AArch64, "BranchImmediate") -> true + | (AArch64, "BranchConditional") -> true + | (AArch64, "CompareAndBranch") -> true + | (AArch64, "TestBitAndBranch") -> true + | (AArch64, "BranchRegister") -> true + | (AArch64, _) -> false + | (MIPS, _) -> false (*todo,fill this in*) + +let option_int_of_option_integer i = match i with + | Some i -> Some (Nat_big_num.to_int i) + | None -> None + +let set_next_instruction_address model = + match model with + | PPC -> + let cia = Reg.find "CIA" !reg in + let cia_addr = address_of_register_value cia in + (match cia_addr with + | Some cia_addr -> + let nia_addr = add_address_nat cia_addr 4 in + let nia = register_value_of_address nia_addr Sail_impl_base.D_increasing in + reg := Reg.add "NIA" nia !reg + | _ -> failwith "CIA address contains unknown or undefined") + | AArch64 -> + let pc = Reg.find "_PC" !reg in + let pc_addr = address_of_register_value pc in + (match pc_addr with + | Some pc_addr -> + let n_addr = add_address_nat pc_addr 4 in + let n_pc = register_value_of_address n_addr D_decreasing in + reg := Reg.add "_PC" n_pc !reg + | _ -> failwith "_PC address contains unknown or undefined") + | MIPS -> + let pc_addr = address_of_register_value (Reg.find "PC" !reg) in + let branchPending = integer_of_register_value (Reg.find "branchPending" !reg) in + (match (pc_addr, option_int_of_option_integer branchPending) with + | (Some pc_val, Some 0) -> + (* normal -- increment PC *) + let n_addr = add_address_nat pc_val 4 in + let n_pc = register_value_of_address n_addr D_decreasing in + begin + reg := Reg.add "nextPC" n_pc !reg; + reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + end + | (Some pc_val, Some 1) -> + (* delay slot -- branch to delayed PC and clear branchPending *) + begin + reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; + reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; + reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg; + end + | (_, _) -> errorf "PC address contains unknown or undefined"; exit 1) + +let add1 = Nat_big_num.add (Nat_big_num.of_int 1) + +let get_addr_trans_regs _ = + (*resultf "PCC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PCC" !reg));*) + Some([ + (Sail_impl_base.Reg("PC", 63, 64, Sail_impl_base.D_decreasing), Reg.find "PC" !reg); + (Sail_impl_base.Reg("PCC", 128, 129, Sail_impl_base.D_decreasing), Reg.find "PCC" !reg); + (Sail_impl_base.Reg("C29", 128, 129, Sail_impl_base.D_decreasing), Reg.find "C29" !reg); + (Sail_impl_base.Reg("CP0Status", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Status" !reg); + (Sail_impl_base.Reg("CP0Cause", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Cause" !reg); + (Sail_impl_base.Reg("CP0Count", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Count" !reg); + (Sail_impl_base.Reg("CP0Compare", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Compare" !reg); + (Sail_impl_base.Reg("inBranchDelay", 0, 1, Sail_impl_base.D_decreasing), Reg.find "inBranchDelay" !reg); + (Sail_impl_base.Reg("TLBRandom", 5, 6, Sail_impl_base.D_decreasing), Reg.find "TLBRandom" !reg); + (Sail_impl_base.Reg("TLBWired", 5, 6, Sail_impl_base.D_decreasing), Reg.find "TLBWired" !reg); + (Sail_impl_base.Reg("TLBEntryHi", 63, 64, Sail_impl_base.D_decreasing), Reg.find "TLBEntryHi" !reg); + (Sail_impl_base.Reg("TLBEntry00", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry00" !reg); + (Sail_impl_base.Reg("TLBEntry01", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry01" !reg); + (Sail_impl_base.Reg("TLBEntry02", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry02" !reg); + (Sail_impl_base.Reg("TLBEntry03", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry03" !reg); + (Sail_impl_base.Reg("TLBEntry04", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry04" !reg); + (Sail_impl_base.Reg("TLBEntry05", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry05" !reg); + (Sail_impl_base.Reg("TLBEntry06", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry06" !reg); + (Sail_impl_base.Reg("TLBEntry07", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry07" !reg); + (Sail_impl_base.Reg("TLBEntry08", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry08" !reg); + (Sail_impl_base.Reg("TLBEntry09", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry09" !reg); + (Sail_impl_base.Reg("TLBEntry10", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry10" !reg); + (Sail_impl_base.Reg("TLBEntry11", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry11" !reg); + (Sail_impl_base.Reg("TLBEntry12", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry12" !reg); + (Sail_impl_base.Reg("TLBEntry13", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry13" !reg); + (Sail_impl_base.Reg("TLBEntry14", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry14" !reg); + (Sail_impl_base.Reg("TLBEntry15", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry15" !reg); + (Sail_impl_base.Reg("TLBEntry16", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry16" !reg); + (Sail_impl_base.Reg("TLBEntry17", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry17" !reg); + (Sail_impl_base.Reg("TLBEntry18", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry18" !reg); + (Sail_impl_base.Reg("TLBEntry19", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry19" !reg); + (Sail_impl_base.Reg("TLBEntry20", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry20" !reg); + (Sail_impl_base.Reg("TLBEntry21", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry21" !reg); + (Sail_impl_base.Reg("TLBEntry22", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry22" !reg); + (Sail_impl_base.Reg("TLBEntry23", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry23" !reg); + (Sail_impl_base.Reg("TLBEntry24", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry24" !reg); + (Sail_impl_base.Reg("TLBEntry25", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry25" !reg); + (Sail_impl_base.Reg("TLBEntry26", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry26" !reg); + (Sail_impl_base.Reg("TLBEntry27", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry27" !reg); + (Sail_impl_base.Reg("TLBEntry28", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry28" !reg); + (Sail_impl_base.Reg("TLBEntry29", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry29" !reg); + (Sail_impl_base.Reg("TLBEntry30", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry30" !reg); + (Sail_impl_base.Reg("TLBEntry31", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry31" !reg); + (Sail_impl_base.Reg("TLBEntry32", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry32" !reg); + (Sail_impl_base.Reg("TLBEntry33", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry33" !reg); + (Sail_impl_base.Reg("TLBEntry34", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry34" !reg); + (Sail_impl_base.Reg("TLBEntry35", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry35" !reg); + (Sail_impl_base.Reg("TLBEntry36", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry36" !reg); + (Sail_impl_base.Reg("TLBEntry37", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry37" !reg); + (Sail_impl_base.Reg("TLBEntry38", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry38" !reg); + (Sail_impl_base.Reg("TLBEntry39", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry39" !reg); + (Sail_impl_base.Reg("TLBEntry40", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry40" !reg); + (Sail_impl_base.Reg("TLBEntry41", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry41" !reg); + (Sail_impl_base.Reg("TLBEntry42", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry42" !reg); + (Sail_impl_base.Reg("TLBEntry43", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry43" !reg); + (Sail_impl_base.Reg("TLBEntry44", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry44" !reg); + (Sail_impl_base.Reg("TLBEntry45", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry45" !reg); + (Sail_impl_base.Reg("TLBEntry46", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry46" !reg); + (Sail_impl_base.Reg("TLBEntry47", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry47" !reg); + (Sail_impl_base.Reg("TLBEntry48", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry48" !reg); + (Sail_impl_base.Reg("TLBEntry49", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry49" !reg); + (Sail_impl_base.Reg("TLBEntry50", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry50" !reg); + (Sail_impl_base.Reg("TLBEntry51", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry51" !reg); + (Sail_impl_base.Reg("TLBEntry52", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry52" !reg); + (Sail_impl_base.Reg("TLBEntry53", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry53" !reg); + (Sail_impl_base.Reg("TLBEntry54", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry54" !reg); + (Sail_impl_base.Reg("TLBEntry55", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry55" !reg); + (Sail_impl_base.Reg("TLBEntry56", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry56" !reg); + (Sail_impl_base.Reg("TLBEntry57", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry57" !reg); + (Sail_impl_base.Reg("TLBEntry58", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry58" !reg); + (Sail_impl_base.Reg("TLBEntry59", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry59" !reg); + (Sail_impl_base.Reg("TLBEntry60", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry60" !reg); + (Sail_impl_base.Reg("TLBEntry61", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry61" !reg); + (Sail_impl_base.Reg("TLBEntry62", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry62" !reg); + (Sail_impl_base.Reg("TLBEntry63", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry63" !reg); + ]) + +let get_opcode pc_a = + List.map (fun b -> match b with + | Some b -> b + | None -> failwith "A byte in opcode contained unknown or undef") + (List.map byte_of_memory_byte + ([Mem.find pc_a !prog_mem; + Mem.find (add1 pc_a) !prog_mem; + Mem.find (add1 (add1 pc_a)) !prog_mem; + Mem.find (add1 (add1 (add1 pc_a))) !prog_mem])) + +let rec write_events = function + | [] -> () + | e::events -> + (match e with + | E_write_reg (Reg(id,_,_,_), value) -> reg := Reg.add id value !reg + | E_write_reg ((Reg_slice(id,_,_,range) as reg_n),value) + | E_write_reg ((Reg_field(id,_,_,_,range) as reg_n),value)-> + let old_val = Reg.find id !reg in + let new_val = fupdate_slice reg_n old_val value range in + reg := Reg.add id new_val !reg + | E_write_reg((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value) -> + let old_val = Reg.find id !reg in + let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in + reg := Reg.add id new_val !reg + | _ -> failwith "Only register write events expected"); + write_events events + +let fetch_instruction_opcode_and_update_ia model addr_trans = + match model with + | PPC -> + let cia = Reg.find "CIA" !reg in + let cia_addr = address_of_register_value cia in + (match cia_addr with + | Some cia_addr -> + let cia_a = integer_of_address cia_addr in + let opcode = (get_opcode cia_a) in + begin + reg := Reg.add "CIA" (Reg.find "NIA" !reg) !reg; + Opcode opcode + end + | None -> failwith "CIA address contains unknown or undefined") + | AArch64 -> + let pc = Reg.find "_PC" !reg in + let pc_addr = address_of_register_value pc in + (match pc_addr with + | Some pc_addr -> + let pc_a = integer_of_address pc_addr in + let opcode = (get_opcode pc_a) in + Opcode opcode + | None -> failwith "_PC address contains unknown or undefined") + | MIPS -> + begin + reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg; + let nextPC = Reg.find "nextPC" !reg in + let pc_addr = address_of_register_value nextPC in + (*let unused = interactf "PC: %s\n" (Printing_functions.register_value_to_string nextPC) in*) + (match pc_addr with + | Some pc_addr -> + let pc_a = match addr_trans (get_addr_trans_regs ()) pc_addr with + | Some a, Some events -> write_events (List.rev events); integer_of_address a + | Some a, None -> integer_of_address a + | None, Some events -> + write_events (List.rev events); + let nextPC = Reg.find "nextPC" !reg in + reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg; + let pc_addr = address_of_register_value nextPC in + (match pc_addr with + | Some pc_addr -> + (match addr_trans (get_addr_trans_regs ()) pc_addr with + | Some a, Some events -> write_events (List.rev events); integer_of_address a + | Some a, None -> integer_of_address a + | None, _ -> failwith "Address translation failed twice") + | None -> failwith "no nextPc address") + | _ -> failwith "No address and no events from translate address" + in + let opcode = (get_opcode pc_a) in + begin + reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg; + Opcode opcode + end + | None -> errorf "nextPC contains unknown or undefined"; exit 1) + end + | _ -> assert false + +let get_pc_address = function + | MIPS -> Reg.find "PC" !reg + | PPC -> Reg.find "CIA" !reg + | AArch64 -> Reg.find "_PC" !reg + + +let option_int_of_reg str = + option_int_of_option_integer (integer_of_register_value (Reg.find str !reg)) + +let rec fde_loop count context model mode track_dependencies addr_trans = + if !max_cut_off && count = !max_instr + then resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count + else begin + if !break_point && count = !break_instr then begin break_point := false; eager_eval := false end; + let pc_regval = get_pc_address model in + interactf "\n**** instruction %d from address %s ****\n" + count (Printing_functions.register_value_to_string pc_regval); + let pc_addr = address_of_register_value pc_regval in + let pc_val = match pc_addr with + | Some v -> v + | None -> failwith "pc contains undef or unknown" in + let m_paddr_int = match addr_trans (get_addr_trans_regs ()) pc_val with + | Some a, Some events -> write_events (List.rev events); Some (integer_of_address a) + | Some a, None -> Some (integer_of_address a) + | None, Some events -> write_events (List.rev events); None + | None, None -> failwith "address translation failed and no writes" in + match m_paddr_int with + | Some pc -> + let inBranchDelay = option_int_of_reg "inBranchDelay" in + (match inBranchDelay with + | Some 0 -> + let npc_addr = add_address_nat pc_val 4 in + let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in + reg := Reg.add "nextPC" npc_reg !reg; + | Some 1 -> + reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; + reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; + | _ -> failwith "invalid value of inBranchDelay"); + let opcode = Opcode (get_opcode pc) in + let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with + | Instr(instruction,istate) -> + interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction); + (instruction,istate) + | Decode_error d -> + (match d with + | Interp_interface.Unsupported_instruction_error instr -> + errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr) + | Interp_interface.Not_an_instruction_error op -> + (match op with + | Opcode bytes -> + errorf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes)) + | Internal_error s -> errorf "\n**** Internal error on decode: %s ****\n" s); exit 1 + in + if stop_condition_met model instruction + then resultf "\nSUCCESS program terminated after %d instructions\n" count + else + begin + match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with + | false, _,_, _ -> errorf "FAILURE\n"; exit 1 + | true, mode, track_dependencies, (my_reg, my_mem, my_tags) -> + reg := my_reg; + prog_mem := my_mem; + tag_mem := my_tags; + + (try + let (pending, _, _) = (Unix.select [(Unix.stdin)] [] [] 0.0) in + (if (pending != []) then + let char = (input_byte stdin) in ( + errorf "Input %x\n" char; + input_buf := (!input_buf) @ [char])); + with + | _ -> ()); + + let uart_rvalid = option_int_of_reg "UART_RVALID" in + (match uart_rvalid with + | Some 0 -> + (match !input_buf with + | x :: xs -> ( + reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg; + reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg; + input_buf := xs; + ) + | [] -> ()) + | _-> ()); + + let uart_written = option_int_of_reg "UART_WRITTEN" in + (match uart_written with + | Some 1 -> + (let uart_data = option_int_of_reg "UART_WDATA" in + match uart_data with + | Some b -> (printf "%c" (Char.chr b); printf "%!") + | None -> (errorf "UART_WDATA was undef" ; exit 1)) + | _ -> ()); + reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + + reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg; + reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg; + reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg; + fde_loop (count + 1) context model (Some mode) (ref track_dependencies) addr_trans + end + | None -> begin + reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg; + reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; + reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg; + reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg; + fde_loop (count + 1) context model mode track_dependencies addr_trans + end + end + +let rec load_raw_file' mem addr chan = + let byte = input_byte chan in + (add_mem byte addr mem; + load_raw_file' mem (Nat_big_num.succ addr) chan) + +let rec load_raw_file mem addr chan = + try + load_raw_file' mem addr chan + with + | End_of_file -> () + +let run () = + Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ; + if !file = "" then begin + Arg.usage args ""; + exit 1; + end; + if !break_point then eager_eval := true; + + let ((isa_defs, + (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4), + isa_externs, + isa_model, + model_reg_d, + startaddr, + startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in + + let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in + (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not, + endian mode, and translate function name + *) + let addr_trans = translate_address context E_big_endian "TranslateAddress" in + if String.length(!raw_file) != 0 then + load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file); + reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg; + (* entry point: unit -> unit fde *) + let name = Filename.basename !file in + let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) addr_trans) () in + resultf "Execution time for file %s: %f seconds\n" name t;; + +(* Turn off line-buffering of standard input to allow responsive console input *) +if Unix.isatty (Unix.stdin) then begin + let tattrs = Unix.tcgetattr (Unix.stdin) in + Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false}) +end ;; + +run () ;; -- cgit v1.2.3 From 65175633755ee5c96e159356d5243ba48be4dbd5 Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Tue, 24 Jan 2017 13:24:46 +0000 Subject: add "interpreter" to make all --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 51a51042..038249f6 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ .PHONY: all sail language clean archs -all: sail +all: sail interpreter apply_header: headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail` -- cgit v1.2.3 From 01ed1c4a495cffcc0a0ca12f3019220f25d1cf66 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 24 Jan 2017 14:23:05 +0000 Subject: first pass at cheri128 sail. --- cheri/Makefile | 8 +- cheri/cheri_insts_128.sail | 973 +++++++++++++++++++++++++++++++++++++++++++ cheri/cheri_prelude_128.sail | 569 +++++++++++++++++++++++++ mips/mips_prelude.sail | 5 +- src/Makefile | 14 + 5 files changed, 1566 insertions(+), 3 deletions(-) create mode 100644 cheri/cheri_insts_128.sail create mode 100644 cheri/cheri_prelude_128.sail diff --git a/cheri/Makefile b/cheri/Makefile index 200ddd5a..4e9a397a 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -1,7 +1,12 @@ EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^ //;1d;$$d' > inst_$1.sail extract: cheri_insts.sail - $(call EXTRACT_INST,CGetX) + $(call EXTRACT_INST,CGetPerms) + $(call EXTRACT_INST,CGetType) + $(call EXTRACT_INST,CGetBase) + $(call EXTRACT_INST,CGetOffset) + $(call EXTRACT_INST,CGetTag) + $(call EXTRACT_INST,CGetSealed) $(call EXTRACT_INST,CGetPCC) $(call EXTRACT_INST,CGetPCCSetOffset) $(call EXTRACT_INST,CGetCause) @@ -13,6 +18,7 @@ extract: cheri_insts.sail $(call EXTRACT_INST,CIncOffset) $(call EXTRACT_INST,CSetOffset) $(call EXTRACT_INST,CSetBounds) + $(call EXTRACT_INST,CSetBoundsExact) $(call EXTRACT_INST,CClearTag) $(call EXTRACT_INST,ClearRegs) $(call EXTRACT_INST,CFromPtr) diff --git a/cheri/cheri_insts_128.sail b/cheri/cheri_insts_128.sail new file mode 100644 index 00000000..b671b515 --- /dev/null +++ b/cheri/cheri_insts_128.sail @@ -0,0 +1,973 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2016 Robert M. Norton *) +(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* 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. *) +(*========================================================================*) + +(* Operations that extract parts of a capability into GPR *) + +union ast member (regno, regno) CGetPerm +union ast member (regno, regno) CGetType +union ast member (regno, regno) CGetBase +union ast member (regno, regno) CGetLen +union ast member (regno, regno) CGetTag +union ast member (regno, regno) CGetSealed +union ast member (regno, regno) CGetOffset + +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetPerm(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetType(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetBase(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(CGetLen(rd, cb)) +(* NB CGetCause Handled separately *) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetTag(rd, cb)) +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetSealed(rd, cb)) +function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *) + +function clause execute (CGetPerm(rd, cb)) = +{ + (* START_CGetPerms *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(getCapPerms(capVal)); + (* END_CGetPerms *) +} + +function clause execute (CGetType(rd, cb)) = +{ + (* START_CGetType *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.otype); + (* END_CGetType *) +} + +function clause execute (CGetBase(rd, cb)) = +{ + (* START_CGetBase *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := getCapBase(capVal); + (* END_CGetBase *) +} + +function clause execute (CGetOffset(rd, cb)) = +{ + (* START_CGetOffset *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := getCapOffset(capVal); + (* END_CGetOffset *) +} + +function clause execute (CGetLen(rd, cb)) = +{ + (* START_CGetLen *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + let len65 = getCapLength(capVal) in + let len64 = if len65 > MAX_U64 then + (bit[64]) MAX_U64 else len65[63..0] in + wGPR(rd) := len64; + (* END_CGetLen *) +} + +function clause execute (CGetTag(rd, cb)) = +{ + (* START_CGetTag *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.tag); + (* END_CGetTag *) +} + +function clause execute (CGetSealed(rd, cb)) = +{ + (* START_CGetSealed *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + let capVal = readCapReg(cb) in + wGPR(rd) := EXTZ(capVal.sealed); + (* END_CGetSealed *) +} + +union ast member regno CGetPCC +function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd)) +function clause execute (CGetPCC(cd)) = +{ + (* START_CGetPCC *) + checkCP2usable(); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else + let pcc = (capRegToCapStruct(PCC)) in + let (success, pcc2) = setCapOffset(pcc, PC) in + {assert (success, None); (* guaranteed to be in-bounds *) + writeCapReg(cd, pcc2)}; + (* END_CGetPCC *) +} + + +union ast member (regno, regno) CGetPCCSetOffset +function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs)) +function clause execute (CGetPCCSetOffset(cd, rs)) = +{ + (* START_CGetPCCSetOffset *) + checkCP2usable(); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else + let pcc = (capRegToCapStruct(PCC)) in + let rs_val = rGPR(rs) in + let (success, newPCC) = setCapOffset(pcc, rs_val) in + if (success) then + writeCapReg(cd, newPCC) + else + writeCapReg(cd, int_to_cap(rs_val)); + (* END_CGetPCCSetOffset *) +} +(* Get and Set CP2 cause register *) + +union ast member regno CGetCause +function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd)) +function clause execute (CGetCause(rd)) = +{ + (* START_CGetCause *) + checkCP2usable(); + if not (pcc_access_system_regs ()) then + raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) + else + wGPR(rd) := EXTZ(CapCause) + (* END_CGetCause *) +} + +union ast member (regno) CSetCause +function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt)) +function clause execute (CSetCause((regno) rt)) = +{ + (* START_CSetCause *) + checkCP2usable(); + if not (pcc_access_system_regs ()) then + raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) + else + { + (bit[64]) rt_val := rGPR(rt); + CapCause.ExcCode := rt_val[15..8]; + CapCause.RegNum := rt_val[7..0]; + } + (* END_CSetCause *) +} + +union ast member regregreg CAndPerm +function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt)) +function clause execute(CAndPerm(cd, cb, rt)) = +{ + (* START_CAndPerm *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := rGPR(rt); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else + let perms = getCapPerms(cb_val) in + let newCap = setCapPerms(cb_val, (perms & rt_val[30..0])) in + writeCapReg(cd, newCap); + (* END_CAndPerm *) +} + + + +union ast member regregreg CToPtr +function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct)) +function clause execute(CToPtr(rd, cb, ct)) = +{ + (* START_CToPtr *) + checkCP2usable(); + ct_val := readCapReg(ct); + cb_val := readCapReg(cb); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if (register_inaccessible(ct)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) + else if not (ct_val.tag) then + raise_c2_exception(CapEx_TagViolation, ct) + else + { + wGPR(rd) := if not (cb_val.tag) then + ((bit[64]) 0) + else + (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val))) + } + (* END_CToPtr *) +} + + + +union ast member regregreg CSub +function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b001010) = Some(CSub(rd, cb, ct)) +function clause execute(CSub(rd, cb, ct)) = +{ + (* START_CSub *) + checkCP2usable(); + ct_val := readCapReg(ct); + cb_val := readCapReg(cb); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if (register_inaccessible(ct)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) + else + { + wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val)) + } + (* END_CSub *) +} + +union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b001) = Some(CPtrCmp(rd, cb, ct, CNE)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b010) = Some(CPtrCmp(rd, cb, ct, CLT)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b011) = Some(CPtrCmp(rd, cb, ct, CLE)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU)) +function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ)) + +function clause execute(CPtrCmp(rd, cb, ct, op)) = +{ + (* START_CPtrCmp *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if (register_inaccessible(ct)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) + else + { + cb_val := readCapReg(cb); + ct_val := readCapReg(ct); + equal := false; + ltu := false; + lts := false; + if (cb_val.tag != ct_val.tag) then + { + if not (cb_val.tag) then + { + ltu := true; + lts := true; + } + } + else + { + cursor1 := getCapCursor(cb_val); + cursor2 := getCapCursor(ct_val); + equal := (cursor1 == cursor2); + ltu := (cursor1 < cursor2); + lts := (((bit[64])cursor1) <_s ((bit[64])cursor2)); + }; + wGPR(rd) := EXTZ(switch (op) { + case CEQ -> [equal] + case CNE -> [not (equal)] + case CLT -> [lts] + case CLE -> [lts | equal] + case CLTU -> [ltu] + case CLEU -> [lts | equal] + case CEXEQ -> [cb_val == ct_val] + }) + } + (* END_CPtrCmp *) +} + +union ast member regregreg CIncOffset +function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt)) +function clause execute (CIncOffset(cd, cb, rt)) = +{ + (* START_CIncOffset *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := rGPR(rt); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then + raise_c2_exception(CapEx_SealViolation, cb) + else + let (success, newCap) = incCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) + (* END_CIncOffset *) +} + +union ast member regregreg CSetOffset +function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt)) +function clause execute (CSetOffset(cd, cb, rt)) = +{ + (* START_CSetOffset *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := rGPR(rt); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if ((cb_val.tag) & (cb_val.sealed)) then + raise_c2_exception(CapEx_SealViolation, cb) + else + let (success, newCap) = setCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(cb_val.address + rt_val)) + (* END_CSetOffset *) +} + +union ast member regregreg CSetBounds +function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt)) +function clause execute (CSetBounds(cd, cb, rt)) = +{ + (* START_CSetBounds *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := unsigned(rGPR(rt)); + cursor := getCapCursor(cb_val); + base := unsigned(getCapBase(cb_val)); + top := unsigned(getCapTop(cb_val)); + newTop := cursor + rt_val; + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if (cursor < base) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if (newTop > top) then + raise_c2_exception(CapEx_LengthViolation, cb) + else + let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in + writeCapReg(cd, newCap) (* ignore exact *) + (* END_CSetBounds *) +} + + +union ast member regregreg CSetBoundsExact +function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cb, rt)) +function clause execute (CSetBoundsExact(cd, cb, rt)) = +{ + (* START_CSetBoundsExact *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := unsigned(rGPR(rt)); + cursor := getCapCursor(cb_val); + base := unsigned(getCapBase(cb_val)); + top := unsigned(getCapTop(cb_val)); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if (cursor < base) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((cursor + rt_val) > top) then + raise_c2_exception(CapEx_LengthViolation, cb) + else + let (exact, newCap) = setCapBounds(cb_val, (bit[64]) base, (bit[65]) top) in + if not (exact) then + raise_c2_exception(CapEx_InexactBounds, cb) + else + writeCapReg(cd, newCap) + (* END_CSetBoundsExact *) +} + +union ast member (regno, regno) CClearTag +function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb)) +function clause execute (CClearTag(cd, cb)) = +{ + (* START_CClearTag *) + checkCP2usable(); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else + { + cb_val := readCapReg(cb); + writeCapReg(cd, {cb_val with tag = false}); + } + (* END_CClearTag *) +} + +union ast member (ClearRegSet, bit[16]) ClearRegs +function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) (* ClearLo *) +function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm)) (* ClearHi *) +function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm)) (* CClearLo *) +function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm)) (* CClearHi *) +function clause execute (ClearRegs(regset, mask)) = +{ + (* START_ClearRegs *) + if ((regset == CLo) | (regset == CHi)) then + checkCP2usable(); + if (regset == CHi) then + foreach (i from 0 to 15) + let r = ((bit[5]) (i+16)) in + if (mask[i] & register_inaccessible(r)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, r); + foreach (i from 0 to 15) + if (mask[i]) then + switch (regset) { + case GPLo -> wGPR((bit[5])i) := 0 + case GPHi -> wGPR((bit[5])(i+16)) := 0 + case CLo -> writeCapReg((bit[5]) i) := null_cap + case CHi -> writeCapReg((bit[5]) (i+16)) := null_cap + } + (* END_ClearRegs *) +} + +union ast member regregreg CFromPtr +function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt)) +function clause execute (CFromPtr(cd, cb, rt)) = +{ + (* START_CFromPtr *) + checkCP2usable(); + cb_val := readCapReg(cb); + rt_val := rGPR(rt); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if (rt == 0) then + writeCapReg(cd, null_cap) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else + let (success, newCap) = setCapOffset(cb_val, rt_val) in + if (success) then + writeCapReg(cd, newCap) + else + writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) + (* END_CFromPtr *) +} + +union ast member (regno, regno) CCheckPerm +function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt)) +function clause execute (CCheckPerm(cs, rt)) = +{ + (* START_CCheckPerm *) + checkCP2usable(); + cs_val := readCapReg(cs); + cs_perms := EXTZ(getCapPerms(cs_val)); + rt_perms := rGPR(rt); + if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if not (cs_val.tag) then + raise_c2_exception(CapEx_TagViolation, cs) + else if ((cs_perms & rt_perms) != rt_perms) then + raise_c2_exception(CapEx_UserDefViolation, cs) + else + () + (* END_CCheckPerm *) +} + +union ast member (regno, regno) CCheckType +function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb)) +function clause execute (CCheckType(cs, cb)) = +{ + (* START_CCheckType *) + checkCP2usable(); + cs_val := readCapReg(cs); + cb_val := readCapReg(cb); + if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cs_val.tag) then + raise_c2_exception(CapEx_TagViolation, cs) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if not (cs_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cs) + else if not (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if ((cs_val.otype) != (cb_val.otype)) then + raise_c2_exception(CapEx_TypeViolation, cs) + else + () + (* END_CCheckType *) +} + +union ast member regregreg CSeal +function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct)) +function clause execute (CSeal(cd, cs, ct)) = +{ + (* START_CSeal *) + checkCP2usable(); + cs_val := readCapReg(cs); + ct_val := readCapReg(ct); + ct_cursor := getCapCursor(ct_val); + ct_top := unsigned(getCapTop(ct_val)); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if (register_inaccessible(ct)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) + else if not (cs_val.tag) then + raise_c2_exception(CapEx_TagViolation, cs) + else if not (ct_val.tag) then + raise_c2_exception(CapEx_TagViolation, ct) + else if (cs_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cs) + else if (ct_val.sealed) then + raise_c2_exception(CapEx_SealViolation, ct) + else if not (ct_val.permit_seal) then + raise_c2_exception(CapEx_PermitSealViolation, ct) + else if (ct_cursor >= ct_top) then + raise_c2_exception(CapEx_LengthViolation, ct) + else if (ct_cursor > max_otype) then + raise_c2_exception(CapEx_LengthViolation, ct) + else + let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in + if not (success) then + raise_c2_exception(CapEx_InexactBounds, cs) + else + writeCapReg(cd, newCap) + (* END_CSeal *) +} + +union ast member regregreg CUnseal +function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct)) +function clause execute (CUnseal(cd, cs, ct)) = +{ + (* START_CUnseal *) + checkCP2usable(); + cs_val := readCapReg(cs); + ct_val := readCapReg(ct); + ct_cursor := getCapCursor(ct_val); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if (register_inaccessible(ct)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) + else if not (cs_val.tag) then + raise_c2_exception(CapEx_TagViolation, cs) + else if not (ct_val.tag) then + raise_c2_exception(CapEx_TagViolation, ct) + else if not (cs_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cs) + else if (ct_val.sealed) then + raise_c2_exception(CapEx_SealViolation, ct) + else if (ct_cursor != unsigned(cs_val.otype)) then + raise_c2_exception(CapEx_TypeViolation, ct) + else if not (ct_val.permit_seal) then + raise_c2_exception(CapEx_PermitSealViolation, ct) + else if (ct_cursor >= unsigned(getCapTop(ct_val))) then + raise_c2_exception(CapEx_LengthViolation, ct) + else + writeCapReg(cd, {cs_val with + sealed=false; + otype=0; + global=(cs_val.global & ct_val.global) + }) + (* END_CUnseal *) +} + +union ast member (regno, regno) CCall +function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb)) +function clause execute (CCall(cs, cb)) = +{ + (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *) + (* START_CCall *) + checkCP2usable(); + cs_val := readCapReg(cs); + cb_val := readCapReg(cb); + if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cs_val.tag) then + raise_c2_exception(CapEx_TagViolation, cs) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if not (cs_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cs) + else if not (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if ((cs_val.otype) != (cb_val.otype)) then + raise_c2_exception(CapEx_TypeViolation, cs) + else if not (cs_val.permit_execute) then + raise_c2_exception(CapEx_PermitExecuteViolation, cs) + else if (cb_val.permit_execute) then + raise_c2_exception(CapEx_PermitExecuteViolation, cb) + else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then + raise_c2_exception(CapEx_LengthViolation, cs) + else + raise_c2_exception(CapEx_CallTrap, cs); + (* END_CCall *) +} + +union ast member unit CReturn +function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn) +function clause execute (CReturn) = +{ + (* START_CReturn *) + checkCP2usable(); + raise_c2_exception_noreg(CapEx_ReturnTrap) + (* END_CReturn *) +} + +union ast member (regno, bit[16], bool) CBX +function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *) +function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, false)) (* CBTS *) + +function clause execute (CBX(cb, imm, invert)) = +{ + (* START_CBx *) + checkCP2usable(); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if (((readCapReg(cb)).tag) ^ invert) then + { + let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in + delayedPC := PC + offset; + branchPending := 1; + } + (* END_CBx *) +} + +union ast member (regno, regno, bool) CJALR +function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(cd, cb, true)) (* CJALR *) +function clause decode (0b010010 : 0b01000 : 0b00000 : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(0b00000, cb, false)) (* CJR *) +function clause execute(CJALR(cd, cb, link)) = +{ + (* START_CJALR *) + checkCP2usable(); + cb_val := readCapReg(cb); + cb_ptr := getCapCursor(cb_val); + cb_top := unsigned(getCapTop(cb_val)); + if (link & register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if not (cb_val.permit_execute) then + raise_c2_exception(CapEx_PermitExecuteViolation, cb) + else if not (cb_val.global) then + raise_c2_exception(CapEx_GlobalViolation, cb) + else if (cb_ptr + 4 > cb_top) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((cb_ptr mod 4) != 0) then + SignalException(AdEL) + else + { + if (link) then + let pcc = capRegToCapStruct(PCC) in + let (success, linkCap) = setCapOffset(pcc, PC+8) in + if (success) then + writeCapReg(cd, linkCap) + else + assert(false, None); + delayedPC := getCapOffset(cb_val); + delayedPCC := capStructToCapReg(cb_val); + branchPending := 1; + } + (* END_CJALR *) +} + +union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) (* CLBU *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b00) = Some(CLoad(rd, cb, rt, offset, true, B, false)) (* CLB *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) (* CLHU *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b01) = Some(CLoad(rd, cb, rt, offset, true, H, false)) (* CLH *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) (* CLWU *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b10) = Some(CLoad(rd, cb, rt, offset, true, W, false)) (* CLW *) +function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) (* CLD *) + +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) (* CLLBU *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, B, true)) (* CLLB *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) (* CLLHU *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, H, true)) (* CLLH *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) (* CLLWU *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, W, true)) (* CLLW *) +function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) (* CLLD *) + +function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = +{ + (* START_CLoad *) + checkCP2usable(); + cb_val := readCapReg(cb); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if not (cb_val.permit_load) then + raise_c2_exception(CapEx_PermitLoadViolation, cb) + else + { + size := wordWidthBytes(width); + cursor := getCapCursor(cb_val); + vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); + vAddr64:= (bit[64]) vAddr; + if ((vAddr + size) > unsigned(getCapTop(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if (vAddr < unsigned(getCapBase(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if not (isAddressAligned(vAddr64, width)) then + SignalExceptionBadAddr(AdEL, vAddr64) + else + { + pAddr := (TLBTranslate(vAddr64, LoadData)); + widthBytes := wordWidthBytes(width); + memResult := if (linked) then + { + CP0LLBit := 0b1; + CP0LLAddr := pAddr; + MEMr_reserve(pAddr, widthBytes); + } + else + MEMr(pAddr, widthBytes); + if (signext) then + wGPR(rd) := EXTS(memResult) + else + wGPR(rd) := EXTZ(memResult) + } + } + (* END_CLoad *) +} + +union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore +function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) (* CSB *) +function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) (* CSH *) +function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) (* CSW *) +function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) (* CSD *) + +function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) (* CSCB *) +function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) (* CSCH *) +function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) (* CSCW *) +function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) (* CSCD *) + +function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = +{ + (* START_CStore *) + checkCP2usable(); + cb_val := readCapReg(cb); + if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if not (cb_val.permit_store) then + raise_c2_exception(CapEx_PermitStoreViolation, cb) + else + { + size := wordWidthBytes(width); + cursor := getCapCursor(cb_val); + vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); + vAddr64:= (bit[64]) vAddr; + if ((vAddr + size) > unsigned(getCapTop(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if (vAddr < unsigned(getCapBase(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if not (isAddressAligned(vAddr64, width)) then + SignalExceptionBadAddr(AdES, vAddr64) + else + { + pAddr := (TLBTranslate(vAddr64, StoreData)); + rs_val := rGPR(rs); + if (conditional) then + { + success := if (CP0LLBit[0]) then + switch(width) + { + case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]) + case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]) + case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]) + case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val) + } + else + false; + wGPR(rd) := EXTZ([success]); + } + else + switch(width) + { + case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0] + case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0] + case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0] + case D -> MEMw_wrapper(pAddr, 8) := rs_val + } + } + } + (* END_CStore *) +} + +union ast member (regno, regno, regno, regno, bit[11], bool) CSC +function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, 0b00000, offset, false)) +function clause decode (0b010010 : 0b10000 : (regno) cs : (regno) cb: (regno) rd : 0b00 : 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true)) +function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = +{ + (* START_CSC *) + checkCP2usable(); + cs_val := readCapReg(cs); + cb_val := readCapReg(cb); + if (register_inaccessible(cs)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if not (cb_val.permit_store_cap) then + raise_c2_exception(CapEx_PermitStoreCapViolation, cb) + else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then + raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb) + else + { + cursor := getCapCursor(cb_val); + vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); + vAddr64:= (bit[64]) vAddr; + if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if (vAddr < unsigned(getCapBase(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((vAddr mod cap_size) != 0) then + SignalExceptionBadAddr(AdES, vAddr64) + else + { + let (pAddr, noStoreCap) = (TLBTranslateC(vAddr64, StoreData)) in + if (cs_val.tag & noStoreCap) then + raise_c2_exception(CapEx_TLBNoStoreCap, cs) + else if (conditional) then + { + success := if (CP0LLBit[0]) then + MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val)) + else + false; + wGPR(rd) := EXTZ([success]); + } + else + MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val)); + } + } + (* END_CSC *) +} + +union ast member (regno, regno, regno, bit[11], bool) CLC +function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset, false)) +function clause decode (0b010010 : 0b10000 : (regno) cd : (regno) cb: 0b0000000 : 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true)) +function clause execute (CLC(cd, cb, rt, offset, linked)) = +{ + (* START_CLC *) + checkCP2usable(); + cb_val := readCapReg(cb); + if (register_inaccessible(cd)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) + else if (register_inaccessible(cb)) then + raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) + else if not (cb_val.tag) then + raise_c2_exception(CapEx_TagViolation, cb) + else if (cb_val.sealed) then + raise_c2_exception(CapEx_SealViolation, cb) + else if not (cb_val.permit_load_cap) then + raise_c2_exception(CapEx_PermitLoadCapViolation, cb) + else + { + cursor := getCapCursor(cb_val); + vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset)); + vAddr64:= (bit[64]) vAddr; + if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if (vAddr < unsigned(getCapBase(cb_val))) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((vAddr mod cap_size) != 0) then + SignalExceptionBadAddr(AdEL, vAddr64) + else + { + let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in + let (tag, mem) = (if (linked) + then + { + CP0LLBit := 0b1; + CP0LLAddr := pAddr; + MEMr_tagged_reserve(pAddr); + } + else + (MEMr_tagged(pAddr))) + in + (CapRegs[cd]) := memBitsToCapBits(tag & not (suppressTag), mem); + } + } + (* END_CLC *) +} + +union ast member (regno) C2Dump +function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt)) +function clause execute (C2Dump (rt)) = + () (* Currently a NOP *) diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail new file mode 100644 index 00000000..323682b7 --- /dev/null +++ b/cheri/cheri_prelude_128.sail @@ -0,0 +1,569 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2016 Robert M. Norton *) +(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* 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. *) +(*========================================================================*) + +(* 265-bit capability is really 257 bits including tag *) +typedef CapReg = bit[129] + +register CapReg PCC +register CapReg nextPCC +register CapReg delayedPCC +register CapReg C00 (* aka default data capability, DDC *) +register CapReg C01 +register CapReg C02 +register CapReg C03 +register CapReg C04 +register CapReg C05 +register CapReg C06 +register CapReg C07 +register CapReg C08 +register CapReg C09 +register CapReg C10 +register CapReg C11 +register CapReg C12 +register CapReg C13 +register CapReg C14 +register CapReg C15 +register CapReg C16 +register CapReg C17 +register CapReg C18 +register CapReg C19 +register CapReg C20 +register CapReg C21 +register CapReg C22 +register CapReg C23 +register CapReg C24 (* aka return code capability, RCC *) +register CapReg C25 +register CapReg C26 (* aka invoked data capability, IDC *) +register CapReg C27 (* aka kernel reserved capability 1, KR1C *) +register CapReg C28 (* aka kernel reserved capability 2, KR2C *) +register CapReg C29 (* aka kernel code capability, KCC *) +register CapReg C30 (* aka kernel data capability, KDC *) +register CapReg C31 (* aka exception program counter capability, EPCC *) + +let (vector <0, 32, inc, (register)>) CapRegs = + [ C00, C01, C02, C03, C04, C05, C06, C07, C08, C09, C10, + C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, + C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31 + ] + +let num_uperms = 4 + + +typedef CapStruct = const struct { + bool tag; + bit[4] uperms; + bool access_system_regs; + bool perm_reserved9; + bool perm_reserved8; + bool permit_seal; + bool permit_store_local_cap; + bool permit_store_cap; + bool permit_load_cap; + bool permit_store; + bool permit_load; + bool permit_execute; + bool global; + bit[2] reserved; + bit[6] E; + bool sealed; + bit[20] B; + bit[20] T; + bit[24] otype; + bit[64] address; +} + +let (CapStruct) null_cap = { + tag = false; + uperms = 0; + access_system_regs = false; + perm_reserved9 = false; + perm_reserved8 = false; + permit_seal = false; + permit_store_local_cap = false; + permit_store_cap = false; + permit_load_cap = false; + permit_store = false; + permit_load = false; + permit_execute = false; + global = false; + reserved = 0; + E = 48; (* encoded as 0 in memory due to xor *) + sealed = false; + B = 0; + T = 0; + otype = 0; + address = 0; +} + +let (nat) max_otype = 0xffffff +def Nat cap_size_t = 16 (* cap size in bytes *) +let ([:cap_size_t:]) cap_size = 16 +let have_cp2 = true + +function CapStruct capRegToCapStruct((CapReg) c) = + let (bool) s = c[104] in + let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in + let (bit[20]) T = if s then c[83..76] : 0x000 else c[83..64] in + let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in + { + tag = c[128]; + uperms = c[127..124]; + access_system_regs = c[123]; + perm_reserved9 = c[122]; + perm_reserved8 = c[121]; + permit_seal = c[120]; + permit_store_local_cap = c[119]; + permit_store_cap = c[118]; + permit_load_cap = c[117]; + permit_store = c[116]; + permit_load = c[115]; + permit_execute = c[114]; + global = c[113]; + reserved = c[112..111]; + E = c[110..105]; + sealed = s; + B = B; + T = T; + otype = otype; + address = c[63..0]; + } + + +function (CapStruct) readCapReg((regno) n) = + capRegToCapStruct(CapRegs[n]) + +function (bit[11]) getCapHardPerms((CapStruct) cap) = + ([cap.access_system_regs] + : [cap.perm_reserved9] + : [cap.perm_reserved8] + : [cap.permit_seal] + : [cap.permit_store_local_cap] + : [cap.permit_store_cap] + : [cap.permit_load_cap] + : [cap.permit_store] + : [cap.permit_load] + : [cap.permit_execute] + : [cap.global]) + +function (bit[31]) getCapPerms((CapStruct) cap) = + let (bit[15]) perms = EXTS(getCapHardPerms(cap)) in (* NB access_system copied into 14-11 *) + (0x000 (* uperms 30-19 *) + : cap.uperms + : perms) + +function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = + { cap with + uperms = perms[18..15]; +(* perm_reserved11_14 = (cap.perm_reserved11_14 & (perms[14..11]));*) + access_system_regs = perms[10]; + perm_reserved9 = perms[9]; + perm_reserved8 = perms[8]; + permit_seal = perms[7]; + permit_store_local_cap = perms[6]; + permit_store_cap = perms[5]; + permit_load_cap = perms[4]; + permit_store = perms[3]; + permit_load = perms[2]; + permit_execute = perms[1]; + global = perms[0]; + } + +function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = + if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then + (true, {cap with sealed=true; otype=otype}) + else + (false, undefined) + +function (bit[128]) capStructToMemBits((CapStruct) cap) = + let (bit[20]) b = if cap.sealed then (cap.B)[23..12] : (cap.otype)[23..12] else cap.B in + let (bit[20]) t = if cap.sealed then (cap.T)[23..12] : (cap.otype)[11..0] else cap.T in + ( cap.uperms + : getCapHardPerms(cap) + : cap.reserved + : cap.E + : [cap.sealed] + : b + : t + : cap.address + ) + +function (CapReg) capStructToCapReg((CapStruct) cap) = + ([cap.tag] : capStructToMemBits(cap)) + +(* Reverse of above used when reading from memory *) +function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) = + ([tag] + : b + ) + +function unit writeCapReg((regno) n, (CapStruct) cap) = + { + CapRegs[n] := capStructToCapReg(cap) + } + + +function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = + switch (a_mid < R, bound < R) { + case (False, False) -> 0 + case (False, True) -> 1 + case (True, False) -> -1 + case (True, True) -> 0 + } + +function bit[64] getCapBase((CapStruct) c) = + let ([|63|]) E = unsigned(c.E) in + let (bool) s = c.sealed in + let (bit[20]) B = c.B in + let (bit[64]) a = c.address in + let (bit[20]) R = B - 0x00100 in (* wraps *) + let (bit[20]) a_mid = a[(E + 19)..E] in + let (int) correction = a_top_correction(a_mid, R, B) in + let a_top = a[63..(E+20)] in + let (bit[64]) base = EXTZ((a_top + correction) : B) in + base << E + +function bit[65] getCapTop((CapStruct) c) = + let ([|63|]) E = unsigned(c.E) in + let (bool) s = c.sealed in + let (bit[20]) B = c.B in + let (bit[20]) T = c.T in + let (bit[64]) a = c.address in + let (bit[20]) R = B - 0x00100 in (* wraps *) + let (bit[20]) a_mid = a[(E + 19)..E] in + let (int) correction = a_top_correction(a_mid, R, T) in + let a_top = a[63..(E+20)] in + let (bit[65]) top1 = EXTZ((a_top + correction) : T) in + top1 << E + +function bit[64] getCapOffset((CapStruct) c) = + let base = getCapBase(c) in + c.address - base + +function bit[65] getCapLength((CapStruct) c) = getCapTop(c) - (0b0 : getCapBase(c)) + +function nat getCapCursor((CapStruct) cap) = unsigned(cap.address) + +function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = + let oldBase = getCapBase(c) in + let oldTop = getCapTop(c) in + let (bit[64]) newAddress = oldBase + offset in + let newCap = { c with address = newAddress } in + let newBase = getCapBase(newCap) in + let newTop = getCapTop(newCap) in + let representable = (oldBase == newBase) & (oldTop == newTop) in + (representable, newCap) + +function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) = + let oldBase = getCapBase(c) in + let oldTop = getCapTop(c) in + let (bit[64]) newAddress = c.address + delta in + let newCap = { c with address = newAddress } in + let newBase = getCapBase(newCap) in + let newTop = getCapTop(newCap) in + let representable = (oldBase == newBase) & (oldTop == newTop) in + (representable, newCap) + +(** FUNCTION:integer HighestSetBit(bits(N) x) *) + +function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = { + let N = (length(x)) in { + ([|('N + -1)|]) result := 0; + (bool) break := false; + foreach (i from (N - 1) downto 0) + if ~(break) & x[i] == 1 then { + result := i; + break := true; + }; + + if break then Some(result) else None; +}} + +function (bit[6]) computeE ((bit[65]) rlength) = + let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in + switch (msb) { + case (Some(b)) -> (bit[6]) b (* hw rounds up to multiple of 4 *) + case None -> 0 + } + +function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) = + (* {cap with base=base; length=(bit[64]) length; offset=0} *) + let (bit[6]) e = computeE(top - (0b0 : base)) in + let (bit[20]) B = base[(19+e)..e] in + let (bit[20]) T = top[(19+e)..e] in + let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in + let newCap = {cap with E=e; B=B; T=T2} in + let newBase = getCapBase(newCap) in + let newTop = getCapTop(newCap) in + let exact = (base == newBase) & (top == newTop) in + (exact, newCap) + +function CapStruct int_to_cap ((bit[64]) offset) = + {null_cap with address = offset} + +typedef CapEx = enumerate { + CapEx_None; + CapEx_LengthViolation; + CapEx_TagViolation; + CapEx_SealViolation; + CapEx_TypeViolation; + CapEx_CallTrap; + CapEx_ReturnTrap; + CapEx_TSSUnderFlow; + CapEx_UserDefViolation; + CapEx_TLBNoStoreCap; + CapEx_InexactBounds; + CapEx_GlobalViolation; + CapEx_PermitExecuteViolation; + CapEx_PermitLoadViolation; + CapEx_PermitStoreViolation; + CapEx_PermitLoadCapViolation; + CapEx_PermitStoreCapViolation; + CapEx_PermitStoreLocalCapViolation; + CapEx_PermitSealViolation; + CapEx_AccessSystemRegsViolation; +} + +typedef CPtrCmpOp = enumerate { + CEQ; + CNE; + CLT; + CLE; + CLTU; + CLEU; + CEXEQ; +} + +typedef ClearRegSet = enumerate { +GPLo; +GPHi; +CLo; +CHi; +} + +function (bit[8]) CapExCode((CapEx) ex) = + switch(ex) { + case CapEx_None -> 0x00 + case CapEx_LengthViolation -> 0x01 + case CapEx_TagViolation -> 0x02 + case CapEx_SealViolation -> 0x03 + case CapEx_TypeViolation -> 0x04 + case CapEx_CallTrap -> 0x05 + case CapEx_ReturnTrap -> 0x06 + case CapEx_TSSUnderFlow -> 0x07 + case CapEx_UserDefViolation -> 0x08 + case CapEx_TLBNoStoreCap -> 0x09 + case CapEx_InexactBounds -> 0x0a + case CapEx_GlobalViolation -> 0x10 + case CapEx_PermitExecuteViolation -> 0x11 + case CapEx_PermitLoadViolation -> 0x12 + case CapEx_PermitStoreViolation -> 0x13 + case CapEx_PermitLoadCapViolation -> 0x14 + case CapEx_PermitStoreCapViolation -> 0x15 + case CapEx_PermitStoreLocalCapViolation -> 0x16 + case CapEx_PermitSealViolation -> 0x17 + case CapEx_AccessSystemRegsViolation -> 0x18 + } + +typedef CapCauseReg = register bits [15:0] { + 15..8: ExcCode; + 7..0: RegNum; +} + +register CapCauseReg CapCause + +function forall Type 'o . 'o SignalException ((Exception) ex) = + { + C31 := PCC; + (*C31.offset := PC; XXX fix this *) + nextPCC := C29; (* KCC *) + delayedPCC := C29; (* always write delayedPCC together whether PCC so + that non-capability branches don't override PCC *) + SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29))); + } + +function unit ERETHook() = + { + nextPCC := C31; + delayedPCC := C31; (* always write delayedPCC together whether PCC so + that non-capability branches don't override PCC *) + } + +function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = + { + (CapCause.ExcCode) := CapExCode(capEx); + (CapCause.RegNum) := regnum; + let mipsEx = + if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) + then C2Trap else C2E in + SignalException(mipsEx); + } + +function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = + raise_c2_exception8(capEx, 0b000 : regnum) + +function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = + raise_c2_exception8(capEx, 0xff) + +function bool pcc_access_system_regs () = + let pcc = capRegToCapStruct(PCC) in + (pcc.access_system_regs) + +function bool register_inaccessible((regno) r) = + let is_sys_reg = switch(r) { + case 0b11011 -> true + case 0b11100 -> true + case 0b11101 -> true + case 0b11110 -> true + case 0b11111 -> true + case _ -> false + } in + if is_sys_reg then + not (pcc_access_system_regs ()) + else + false + +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve + +val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag +val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional + + +function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = +{ + (* assumes addr is cap. aligned *) + let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in + (tag[0], mem) +} + +function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = +{ + (* assumes addr is cap. aligned *) + let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in + (tag[0], mem) +} + +function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = +{ + (* assumes addr is cap. aligned *) + MEMea_tag(addr, cap_size); + MEMval_tag(addr, cap_size, 0b0000000 : [tag] : data); +} + +function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = +{ + (* assumes addr is cap. aligned *) + MEMea_tag_conditional(addr, cap_size); + MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : data); +} + +function unit effect {wmem} MEMw_wrapper(addr, size, data) = + if (addr == 0x000000007f000000) then + { + UART_WDATA := data[31..24]; + UART_WRITTEN := 1; + } + else + { + (* On cheri non-capability writes must clear the corresponding tag + XXX this is vestigal and only works on sequential modle -- tag clearing + should probably be done in memory model. *) + TAGw((addr[63..4] : 0b0000), 0x00); + MEMea(addr,size); + MEMval(addr, size, data); + } + +function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = + { + (* On cheri non-capability writes must clear the corresponding tag*) + MEMea_conditional(addr, size); + success := MEMval_conditional(addr,size,data); + if (success) then + (* XXX as above TAGw is vestigal and must die *) + TAGw((addr[63..4] : 0b0000), 0x00); + success; + } + +function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = + { + capno := 0b00000; + cap := readCapReg(capno); + if (~(cap.tag)) then + (raise_c2_exception(CapEx_TagViolation, capno)) + else if (cap.sealed) then + (raise_c2_exception(CapEx_SealViolation, capno)); + switch (accessType) { + case Instruction -> if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)) + case LoadData -> if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)) + case StoreData -> if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno)) + }; + cursor := getCapCursor(cap); + vAddr := cursor + unsigned(addr); + size := wordWidthBytes(width); + base := unsigned(getCapBase(cap)); + top := unsigned(getCapTop(cap)); + if ((vAddr + size) > top) then + (raise_c2_exception(CapEx_LengthViolation, capno)) + else if (vAddr < (base)) then + (raise_c2_exception(CapEx_LengthViolation, capno)) + else + (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *) + } + +function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { + incrementCP0Count(); + let pcc = capRegToCapStruct(PCC) in + let base = unsigned(getCapBase(pcc)) in + let top = unsigned(getCapTop(pcc)) in + let absPC = (unsigned(vAddr)) in + if ((absPC mod 4) != 0) then (* bad PC alignment *) + (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *) + else if ((absPC + 4) > top) then + (raise_c2_exception_noreg(CapEx_LengthViolation)) + else + TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) +} + +function unit checkCP2usable () = + { + if (~((CP0Status.CU)[2])) then + { + (CP0Cause.CE) := 0b10; + (SignalException(CpU)); + } + } + diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 80350af1..8975193c 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -89,8 +89,9 @@ let ([:64:]) TLBNumEntries = 64 typedef TLBIndexT = (bit[6]) let (TLBIndexT) TLBIndexMax = 0b111111 -let MAX_VA = unsigned(0xffffffffff) -let MAX_PA = unsigned(0xfffffffff) +let MAX_U64 = unsigned(0xffffffffffffffff) +let MAX_VA = unsigned(0xffffffffff) +let MAX_PA = unsigned(0xfffffffff) typedef TLBEntry = register bits [116 : 0] { 116 .. 101: pagemask; diff --git a/src/Makefile b/src/Makefile index fb71396d..594f5c15 100644 --- a/src/Makefile +++ b/src/Makefile @@ -42,6 +42,8 @@ CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts_128.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail + elf: make -C $(ELFDIR) @@ -56,6 +58,10 @@ _build/run_with_elf_cheri.ml: lem_interp/run_with_elf_cheri.ml mkdir -p _build cp $< $@ +_build/run_with_elf_cheri128.ml: lem_interp/run_with_elf_cheri128.ml + mkdir -p _build + cp $< $@ + _build/mips.lem: $(MIPS_SAILS) ./sail.native mkdir -p _build cd _build ;\ @@ -76,6 +82,11 @@ _build/cheri.lem: $(CHERI_SAILS) ./sail.native cd _build ;\ ../sail.native -lem_ast -o cheri $(CHERI_SAILS) +_build/cheri128.lem: $(CHERI128_SAILS) ./sail.native + mkdir -p _build + cd _build ;\ + ../sail.native -lem_ast -o cheri128 $(CHERI128_SAILS) + _build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native mkdir -p _build cd _build ;\ @@ -111,6 +122,9 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native +run_cheri128.native: _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native + mips_notlb: _build/mips_notlb.ml _build/mips_embed_types.lem _build/mips_extras.ml true -- cgit v1.2.3 From 951560776eed6964ea95dab2c33433515d687afa Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 24 Jan 2017 16:58:21 +0000 Subject: force unsigned comparison in cgetlen overflow check. --- cheri/cheri_insts_128.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cheri/cheri_insts_128.sail b/cheri/cheri_insts_128.sail index b671b515..1d2b37fb 100644 --- a/cheri/cheri_insts_128.sail +++ b/cheri/cheri_insts_128.sail @@ -108,7 +108,7 @@ function clause execute (CGetLen(rd, cb)) = else let capVal = readCapReg(cb) in let len65 = getCapLength(capVal) in - let len64 = if len65 > MAX_U64 then + let len64 = if unsigned(len65) > MAX_U64 then (bit[64]) MAX_U64 else len65[63..0] in wGPR(rd) := len64; (* END_CGetLen *) -- cgit v1.2.3 From ccfab66f9b4cc0acefb63e79fd7e9d56aa79d66a Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 24 Jan 2017 19:34:37 +0000 Subject: functionality for comparing handwritten analysis function with exhaustive interpreter --- src/lem_interp/interp_inter_imp.lem | 82 +++++++++++++++++++++++++++++++++++++ src/lem_interp/sail_impl_base.lem | 41 +++++++++++++++++++ 2 files changed, 123 insertions(+) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index cbd56240..75e695eb 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1215,3 +1215,85 @@ let interp_instruction_analysis end in (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind) + +let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment = + fst (instruction_analysis context endianness analysis_function + reg_info (Just environment) instruction) + + + +val print_and_fail_of_inequal : forall 'a. Show 'a => + (string -> unit) -> + (instruction -> string) -> + (string * 'a) -> (string * 'a) -> unit +let print_and_fail_if_inequal + (print_endline,pp_instruction,instruction) + (name1,xs1) (name2,xs2) = + if xs1 = xs2 then () + else + let () = print_endline (name1^": "^show xs1) in + let () = print_endline (name2^": "^show xs2) in + failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction) + +let interp_compare_analyses + print_endline + pp_instruction + (non_pseudo_registers : set reg_name -> set reg_name) + context + endianness + interp_exhaustive + instruction + nia_reg + ism + environment + analysis_function + reg_info = + let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = + interp_instruction_analysis interp_exhaustive instruction nia_reg ism + environment in + let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) = + (Set.fromList regs_in1, + Set.fromList regs_out1, + Set.fromList regs_feeding_address1, + Set.fromList nias1) in + let (regs_in1S,regs_out1S,regs_feeding_addres1S) = + (non_pseudo_registers regs_in1S, + non_pseudo_registers regs_out1S, + non_pseudo_registers regs_feeding_address1S) in + + let (regs_in2,regs_out2,regs_feeding_address2,nias2,dia2,inst_kind2) = + interp_handwritten_instruction_analysis + context endianness instruction analysis_function reg_info environment in + let (regs_in2S,regs_out2S,regs_feeding_address2S,nias2S) = + (Set.fromList regs_in2, + Set.fromList regs_out2, + Set.fromList regs_feeding_address2, + Set.fromList nias2) in + let (regs_in2S,regs_out2S,regs_feeding_addres2S) = + (non_pseudo_registers regs_in2S, + non_pseudo_registers regs_out2S, + non_pseudo_registers regs_feeding_address2S) in + + let aux = (print_endline,pp_instruction,instruction) in + let () = (print_and_fail_if_inequal aux) + ("regs_in exhaustive",regs_in1S) + ("regs_in hand",regs_in2S) in + let () = (print_and_fail_if_inequal aux) + ("regs_out exhaustive",regs_out1S) + ("regs_out hand",regs_out2S) in + let () = (print_and_fail_if_inequal aux) + ("regs_feeding_address exhaustive",regs_feeding_address1S) + ("regs_feeding_address hand",regs_feeding_address2S) in + let () = (print_and_fail_if_inequal aux) + ("nias exhaustive",nias1S) + ("nias hand",nias2S) in + let () = (print_and_fail_if_inequal aux) + ("dia exhaustive",dia1) + ("dia hand",dia2) in + let () = (print_and_fail_if_inequal aux) + ("inst_kind exhaustive",inst_kind1) + ("inst_kind hand",inst_kind2) in + + (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) + + diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 76ac1797..3f38f521 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -398,6 +398,18 @@ type write_kind = (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release +instance (Show write_kind) + let show = function + | Write_plain -> "Write_plain" + | Write_tag -> "Write_tag" + | Write_tag_conditional -> "Write_tag_conditional" + | Write_conditional -> "Write_conditional" + | Write_release -> "Write_release" + | Write_exclusive -> "Write_exclusive" + | Write_exclusive_release -> "Write_exclusive_release" + end +end + type barrier_kind = (* Power barriers *) Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync @@ -407,6 +419,23 @@ type barrier_kind = (* MIPS barriers *) | Barrier_MIPS_SYNC +instance (Show barrier_kind) + let show = function + | Barrier_Sync -> "Barrier_Sync" + | Barrier_LwSync -> "Barrier_LwSync" + | Barrier_Eieio -> "Barrier_Eieio" + | Barrier_Isync -> "Barrier_Isync" + | Barrier_DMB -> "Barrier_DMB" + | Barrier_DMB_ST -> "Barrier_DMB_ST" + | Barrier_DMB_LD -> "Barrier_DMB_LD" + | Barrier_DSB -> "Barrier_DSB" + | Barrier_DSB_ST -> "Barrier_DSB_ST" + | Barrier_DSB_LD -> "Barrier_DSB_LD" + | Barrier_ISB -> "Barrier_ISB" + | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" + end +end + type instruction_kind = | IK_barrier of barrier_kind | IK_mem_read of read_kind @@ -419,6 +448,18 @@ they just have particular nias (and will be IK_simple *) | IK_simple +instance (Show instruction_kind) + let show = function + | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) + | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) + | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) + | IK_cond_branch -> "IK_cond_branch" + | IK_simple -> "IK_simple" + end +end + + + let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with | (Read_plain, Read_plain) -> EQ -- cgit v1.2.3