From cc46b5a2366cd73d34117590448f6779fac4d312 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 17 Aug 2017 13:41:21 +0100 Subject: added RISC-V load-acquire --- src/lem_interp/sail_impl_base.lem | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index cda6702c..1642bc81 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -426,6 +426,8 @@ type read_kind = | Read_reserve (* AArch64 reads *) | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream + (* RISC-V reads *) + | Read_RISCV_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire instance (Show read_kind) let show = function -- cgit v1.2.3 From 9a26a0440f4d3c63ea19976c44cd39edb8149b2a Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Sat, 19 Aug 2017 10:34:04 +0100 Subject: RISC-V store-release --- src/lem_interp/sail_impl_base.lem | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 1642bc81..caec3838 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -437,6 +437,9 @@ instance (Show read_kind) | Read_exclusive -> "Read_exclusive" | Read_exclusive_acquire -> "Read_exclusive_acquire" | Read_stream -> "Read_stream" + | Read_RISCV_acquire -> "Read_RISCV_acquire" + | Read_RISCV_reserved -> "Read_RISCV_reserved" + | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" end end @@ -447,6 +450,8 @@ type write_kind = | Write_conditional (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release + (* RISC-V *) + | Write_RISCV_release | Write_RISCV_conditional | Write_RISCV_conditional_release instance (Show write_kind) let show = function @@ -455,6 +460,9 @@ instance (Show write_kind) | Write_release -> "Write_release" | Write_exclusive -> "Write_exclusive" | Write_exclusive_release -> "Write_exclusive_release" + | Write_RISCV_release -> "Write_RISCV_release" + | Write_RISCV_conditional -> "Write_RISCV_conditional" + | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" end end @@ -488,6 +496,9 @@ instance (Show barrier_kind) | Barrier_ISB -> "Barrier_ISB" | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" + | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" + | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" end end -- cgit v1.2.3 From 78a35c575021679b5e512539598d47603a6822f0 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 22 Aug 2017 11:09:47 +0100 Subject: adapt state.lem to RISCV additions --- src/gen_lib/state.lem | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src') diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 430ee562..2e29d19a 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -60,6 +60,9 @@ let read_mem dir read_kind addr sz state = | Sail_impl_base.Read_exclusive -> true | Sail_impl_base.Read_exclusive_acquire -> true | Sail_impl_base.Read_stream -> false + | Sail_impl_base.Read_RISCV_acquire -> false + | Sail_impl_base.Read_RISCV_reserved -> true + | Sail_impl_base.Read_RISCV_reserved_acquire -> true end in if is_exclusive -- cgit v1.2.3 From 6cc248cc27d9133e23da1454f115176f0799a572 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Tue, 22 Aug 2017 14:16:01 +0100 Subject: added RISC-V "fence w,w" and "fence.i"; fixed the interpreter nias analysis; --- src/lem_interp/interp_inter_imp.lem | 49 ++++++++++++++++++++++++++++++++++--- src/lem_interp/sail_impl_base.lem | 4 +++ 2 files changed, 49 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index fda9d5dd..6a9a77a1 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1267,6 +1267,10 @@ let nias_of_instruction else [NIA_successor] | _ -> [ NIA_successor ] end + | ("PPCGEN_ism", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"PPCGEN_ism\", \"" ^ s ^ "\")") in + [ NIA_successor ] (* AARch64 label branch (i.e. address must be known) although these instructions take the address as an offset from PC, in here @@ -1301,7 +1305,10 @@ let nias_of_instruction | (Reg name _ _ _) -> name = n_reg | _ -> false end] - + | ("AArch64HandSail", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"AArch64HandSail\", \"" ^ s ^ "\")") in + [ NIA_successor ] (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *) @@ -1334,18 +1341,52 @@ let nias_of_instruction | (Reg name _ _ _) -> name = n_reg | _ -> false end] + | ("AArch64GenSail", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"AArch64GenSail\", \"" ^ s ^ "\")") in + [ NIA_successor ] (** end of hacky *) | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias + | ("AArch64LitmusSail", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"AArch64LitmusSail\", \"" ^ s ^ "\")") in + [ NIA_successor ] | ("MIPS_ism", "B") -> fail + | ("MIPS_ism", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"MIPS_ism\", \"" ^ s ^ "\")") in + [ NIA_successor ] - | (s1,s2) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in + | ("RISCV_ism", "JAL") -> nias + | ("RISCV_ism", "JALR") -> + let rs1_integer = + match instruction_fields with + | [_; (_, _, rs1); _] -> integer_of_bit_list rs1 + | _ -> fail + end + in + let () = ensure (0 <= rs1_integer && rs1_integer <= 31) + "expected register number from 0 to 31" + in + if rs1_integer = 0 then nias + else + let rs1_reg = "x" ^ (String_extra.stringFromInteger rs1_integer) in + [NIA_register r | forall (r MEM regs_in) + | match r with + | (Reg name _ _ _) -> name = rs1_reg + | _ -> false + end] + | ("RISCV_ism", "BTYPE") -> NIA_successor :: nias + | ("RISCV_ism", s) -> + let () = ensure (not unknown_nia_address) + ("unexpected unknown/undefined address in nia_values 4 (\"RISCV_ism\", \"" ^ s ^ "\")") in [ NIA_successor ] + + | (s1, s2) -> failwith ("unexpected (thread_ism, instruction_name): (" ^ s1 ^ ", " ^ s2 ^ ")") end let interp_instruction_analysis diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index caec3838..ebf0db4a 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -479,6 +479,8 @@ type barrier_kind = | Barrier_RISCV_rw_rw | Barrier_RISCV_r_rw | Barrier_RISCV_rw_w + | Barrier_RISCV_w_w + | Barrier_RISCV_i instance (Show barrier_kind) @@ -499,6 +501,8 @@ instance (Show barrier_kind) | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" + | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" + | Barrier_RISCV_I -> "Barrier_RISCV_i" end end -- cgit v1.2.3 From d8c238ddac07ed8bf828596ff68198d0c63758f5 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 22 Aug 2017 14:39:20 +0100 Subject: and fix that other places --- src/gen_lib/state.lem | 37 +++++++++++++++---------------------- 1 file changed, 15 insertions(+), 22 deletions(-) (limited to 'src') diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 2e29d19a..2ea1247e 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -47,25 +47,27 @@ let set_reg state reg bitv = <| state with regstate = Map.insert reg bitv state.regstate |> +let is_exclusive = function + | Sail_impl_base.Read_plain -> false + | Sail_impl_base.Read_reserve -> true + | Sail_impl_base.Read_acquire -> false + | Sail_impl_base.Read_exclusive -> true + | Sail_impl_base.Read_exclusive_acquire -> true + | Sail_impl_base.Read_stream -> false + | Sail_impl_base.Read_RISCV_acquire -> false + | Sail_impl_base.Read_RISCV_reserved -> true + | Sail_impl_base.Read_RISCV_reserved_acquire -> true +end + + val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU) let read_mem dir read_kind addr sz state = let addr = integer_of_address (address_of_bitv addr) in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in let value = Sail_values.internal_mem_value dir memory_value in - let is_exclusive = match read_kind with - | Sail_impl_base.Read_plain -> false - | Sail_impl_base.Read_reserve -> true - | Sail_impl_base.Read_acquire -> false - | Sail_impl_base.Read_exclusive -> true - | Sail_impl_base.Read_exclusive_acquire -> true - | Sail_impl_base.Read_stream -> false - | Sail_impl_base.Read_RISCV_acquire -> false - | Sail_impl_base.Read_RISCV_reserved -> true - | Sail_impl_base.Read_RISCV_reserved_acquire -> true - end in - if is_exclusive + if is_exclusive read_kind then [(Left value, <| state with last_exclusive_operation_was_load = true |>)] else [(Left value, state)] @@ -79,17 +81,8 @@ let read_tag dir read_kind addr state = | Just t -> t | Nothing -> B0 end in - let is_exclusive = match read_kind with - | Sail_impl_base.Read_plain -> false - | Sail_impl_base.Read_reserve -> true - | Sail_impl_base.Read_acquire -> false - | Sail_impl_base.Read_exclusive -> true - | Sail_impl_base.Read_exclusive_acquire -> true - | Sail_impl_base.Read_stream -> false - end in - (* TODO Should reading a tag set the exclusive flag? *) - if is_exclusive + if is_exclusive read_kind then [(Left tag, <| state with last_exclusive_operation_was_load = true |>)] else [(Left tag, state)] -- cgit v1.2.3 From 888b0f2bd01b8a2e026d6a081e85ffe2df3ed16c Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 24 Aug 2017 10:06:34 +0100 Subject: added barrier-kind for x86 MFENCE; fixed some compare functions; --- src/lem_interp/sail_impl_base.lem | 168 ++++++++++++++++++++++---------------- 1 file changed, 96 insertions(+), 72 deletions(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index ebf0db4a..b52eb58f 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -481,6 +481,8 @@ type barrier_kind = | Barrier_RISCV_rw_w | Barrier_RISCV_w_w | Barrier_RISCV_i + (* X86 *) + | Barrier_X86_MFENCE instance (Show barrier_kind) @@ -503,6 +505,7 @@ instance (Show barrier_kind) | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" | Barrier_RISCV_I -> "Barrier_RISCV_i" + | Barrier_X86_MFENCE -> "Barrier_X86_MFENCE" end end @@ -546,48 +549,42 @@ end let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with - | (Read_plain, Read_plain) -> EQ - | (Read_plain, Read_reserve) -> LT - | (Read_plain, Read_acquire) -> LT - | (Read_plain, Read_exclusive) -> LT - | (Read_plain, Read_exclusive_acquire) -> LT - | (Read_plain, Read_stream) -> LT - - | (Read_reserve, Read_plain) -> GT - | (Read_reserve, Read_reserve) -> EQ - | (Read_reserve, Read_acquire) -> LT - | (Read_reserve, Read_exclusive) -> LT - | (Read_reserve, Read_exclusive_acquire) -> LT - | (Read_reserve, Read_stream) -> LT - - | (Read_acquire, Read_plain) -> GT - | (Read_acquire, Read_reserve) -> GT - | (Read_acquire, Read_acquire) -> EQ - | (Read_acquire, Read_exclusive) -> LT - | (Read_acquire, Read_exclusive_acquire) -> LT - | (Read_acquire, Read_stream) -> LT - - | (Read_exclusive, Read_plain) -> GT - | (Read_exclusive, Read_reserve) -> GT - | (Read_exclusive, Read_acquire) -> GT - | (Read_exclusive, Read_exclusive) -> EQ - | (Read_exclusive, Read_exclusive_acquire) -> LT - | (Read_exclusive, Read_stream) -> LT - - | (Read_exclusive_acquire, Read_plain) -> GT - | (Read_exclusive_acquire, Read_reserve) -> GT - | (Read_exclusive_acquire, Read_acquire) -> GT - | (Read_exclusive_acquire, Read_exclusive) -> GT + | (Read_plain, Read_plain) -> EQ + | (Read_plain, _) -> LT + | (_, Read_plain) -> GT + + | (Read_reserve, Read_reserve) -> EQ + | (Read_reserve, _) -> LT + | (_, Read_reserve) -> GT + + | (Read_acquire, Read_acquire) -> EQ + | (Read_acquire, _) -> LT + | (_, Read_acquire) -> GT + + | (Read_exclusive, Read_exclusive) -> EQ + | (Read_exclusive, _) -> LT + | (_, Read_exclusive) -> GT + | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ - | (Read_exclusive_acquire, Read_stream) -> GT - - | (Read_stream, Read_plain) -> GT - | (Read_stream, Read_reserve) -> GT - | (Read_stream, Read_acquire) -> GT - | (Read_stream, Read_exclusive) -> GT - | (Read_stream, Read_exclusive_acquire) -> GT - | (Read_stream, Read_stream) -> EQ -end + | (Read_exclusive_acquire, _) -> LT + | (_, Read_exclusive_acquire) -> GT + + | (Read_stream, Read_stream) -> EQ + | (Read_stream, _) -> LT + | (_, Read_stream) -> GT + + | (Read_RISCV_acquire, Read_RISCV_acquire) -> EQ + | (Read_RISCV_acquire, _) -> LT + | (_, Read_RISCV_acquire) -> GT + + | (Read_RISCV_reserved, Read_RISCV_reserved) -> EQ + | (Read_RISCV_reserved, _) -> LT + | (_, Read_RISCV_reserved) -> GT + + | (Read_RISCV_reserved_acquire, Read_RISCV_reserved_acquire) -> EQ + (*| (Read_RISCV_reserved_acquire, _) -> LT + | (_, Read_RISCV_reserved_acquire) -> GT*) + end let inline {ocaml} read_kindCompare = defaultCompare let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT @@ -610,36 +607,39 @@ end let ~{ocaml} write_kindCompare wk1 wk2 = match (wk1, wk2) with - | (Write_plain, Write_plain) -> EQ - | (Write_plain, Write_conditional) -> LT - | (Write_plain, Write_release) -> LT - | (Write_plain, Write_exclusive) -> LT - | (Write_plain, Write_exclusive_release) -> LT - - | (Write_conditional, Write_plain) -> GT - | (Write_conditional, Write_conditional) -> EQ - | (Write_conditional, Write_release) -> LT - | (Write_conditional, Write_exclusive) -> LT - | (Write_conditional, Write_exclusive_release) -> LT - - | (Write_release, Write_plain) -> GT - | (Write_release, Write_conditional) -> GT - | (Write_release, Write_release) -> EQ - | (Write_release, Write_exclusive) -> LT - | (Write_release, Write_exclusive_release) -> LT - - | (Write_exclusive, Write_plain) -> GT - | (Write_exclusive, Write_conditional) -> GT - | (Write_exclusive, Write_release) -> GT - | (Write_exclusive, Write_exclusive) -> EQ - | (Write_exclusive, Write_exclusive_release) -> LT - - | (Write_exclusive_release, Write_plain) -> GT - | (Write_exclusive_release, Write_conditional) -> GT - | (Write_exclusive_release, Write_release) -> GT - | (Write_exclusive_release, Write_exclusive) -> GT + | (Write_plain, Write_plain) -> EQ + | (Write_plain, _) -> LT + | (_, Write_plain) -> GT + + | (Write_conditional, Write_conditional) -> EQ + | (Write_conditional, _) -> LT + | (_, Write_conditional) -> GT + + + | (Write_release, Write_release) -> EQ + | (Write_release, _) -> LT + | (_, Write_release) -> GT + + | (Write_exclusive, Write_exclusive) -> EQ + | (Write_exclusive, _) -> LT + | (_, Write_exclusive) -> GT + | (Write_exclusive_release, Write_exclusive_release) -> EQ -end + | (Write_exclusive_release, _) -> LT + | (_, Write_exclusive_release) -> GT + + | (Write_RISCV_release, Write_RISCV_release) -> EQ + | (Write_RISCV_release, _) -> LT + | (_, Write_RISCV_release) -> GT + + | (Write_RISCV_conditional, Write_RISCV_conditional) -> EQ + | (Write_RISCV_conditional, _) -> LT + | (_, Write_RISCV_conditional) -> GT + + | (Write_RISCV_conditional_release, Write_RISCV_conditional_release) -> EQ + (*| (Write_RISCV_conditional_release, _) -> LT + | (_, Write_RISCV_conditional_release) -> GT*) + end let inline {ocaml} write_kindCompare = defaultCompare let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT @@ -660,6 +660,7 @@ instance (Ord write_kind) let (>=) = write_kindGreaterEq end + let ~{ocaml} barrier_kindCompare bk1 bk2 = match (bk1, bk2) with | (Barrier_Sync, Barrier_Sync) -> EQ @@ -711,9 +712,32 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (_, Barrier_TM_COMMIT) -> GT | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ - (* | (Barrier_MIPS_SYNC, _) -> LT - | (_, Barrier_MIPS_SYNC) -> GT *) + | (Barrier_MIPS_SYNC, _) -> LT + | (_, Barrier_MIPS_SYNC) -> GT + + | (Barrier_RISCV_rw_rw, Barrier_RISCV_rw_rw) -> EQ + | (Barrier_RISCV_rw_rw, _) -> LT + | (_, Barrier_RISCV_rw_rw) -> GT + + | (Barrier_RISCV_r_rw, Barrier_RISCV_r_rw) -> EQ + | (Barrier_RISCV_r_rw, _) -> LT + | (_, Barrier_RISCV_r_rw) -> GT + + | (Barrier_RISCV_rw_w, Barrier_RISCV_rw_w) -> EQ + | (Barrier_RISCV_rw_w, _) -> LT + | (_, Barrier_RISCV_rw_w) -> GT + + | (Barrier_RISCV_w_w, Barrier_RISCV_w_w) -> EQ + | (Barrier_RISCV_w_w, _) -> LT + | (_, Barrier_RISCV_w_w) -> GT + + | (Barrier_RISCV_i, Barrier_RISCV_i) -> EQ + | (Barrier_RISCV_i, _) -> LT + | (_, Barrier_RISCV_i) -> GT + | (Barrier_X86_MFENCE, Barrier_X86_MFENCE) -> EQ + (*| (Barrier_X86_MFENCE, _) -> LT + | (_, Barrier_X86_MFENCE) -> GT*) end let inline {ocaml} barrier_kindCompare = defaultCompare -- cgit v1.2.3 From 3721093caa882173526ab7ba03ccaa3226e2a94f Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 24 Aug 2017 10:09:00 +0100 Subject: typo --- src/lem_interp/sail_impl_base.lem | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index b52eb58f..60beffb4 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -504,7 +504,7 @@ instance (Show barrier_kind) | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" - | Barrier_RISCV_I -> "Barrier_RISCV_i" + | Barrier_RISCV_i -> "Barrier_RISCV_i" | Barrier_X86_MFENCE -> "Barrier_X86_MFENCE" end end -- cgit v1.2.3 From 1dd42197633a1b608303187fac8cc7f5b30ec22e Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 24 Aug 2017 10:11:22 +0100 Subject: typo --- src/lem_interp/sail_impl_base.lem | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 60beffb4..65ae87c2 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -482,7 +482,7 @@ type barrier_kind = | Barrier_RISCV_w_w | Barrier_RISCV_i (* X86 *) - | Barrier_X86_MFENCE + | Barrier_x86_MFENCE instance (Show barrier_kind) @@ -505,7 +505,7 @@ instance (Show barrier_kind) | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" | Barrier_RISCV_i -> "Barrier_RISCV_i" - | Barrier_X86_MFENCE -> "Barrier_X86_MFENCE" + | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" end end @@ -735,9 +735,9 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = | (Barrier_RISCV_i, _) -> LT | (_, Barrier_RISCV_i) -> GT - | (Barrier_X86_MFENCE, Barrier_X86_MFENCE) -> EQ - (*| (Barrier_X86_MFENCE, _) -> LT - | (_, Barrier_X86_MFENCE) -> GT*) + | (Barrier_x86_MFENCE, Barrier_x86_MFENCE) -> EQ + (*| (Barrier_x86_MFENCE, _) -> LT + | (_, Barrier_x86_MFENCE) -> GT*) end let inline {ocaml} barrier_kindCompare = defaultCompare -- cgit v1.2.3 From d9e3c14533806986f7c6ce843148cf1973f9711b Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 30 Aug 2017 14:44:28 +0100 Subject: typeclass instance Ord(opcode) --- src/lem_interp/sail_impl_base.lem | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 65ae87c2..3886f919 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -110,7 +110,7 @@ type address = Address of list byte (* of length 8 *) * integer type opcode = Opcode of list byte (* of length 4 *) (** typeclass instantiations *) - + let ~{ocaml} bitCompare (b1:bit) (b2:bit) = match (b1,b2) with | (Bitc_zero, Bitc_zero) -> EQ @@ -214,6 +214,36 @@ instance (Ord byte) let (>=) = byteGreaterEq end + + + + +let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) = + compare o1 o2 +let {ocaml} opcodeCompare = defaultCompare + +let ~{ocaml} opcodeLess b1 b2 = opcodeCompare b1 b2 = LT +let ~{ocaml} opcodeLessEq b1 b2 = opcodeCompare b1 b2 <> GT +let ~{ocaml} opcodeGreater b1 b2 = opcodeCompare b1 b2 = GT +let ~{ocaml} opcodeGreaterEq b1 b2 = opcodeCompare b1 b2 <> LT + +let inline {ocaml} opcodeLess = defaultLess +let inline {ocaml} opcodeLessEq = defaultLessEq +let inline {ocaml} opcodeGreater = defaultGreater +let inline {ocaml} opcodeGreaterEq = defaultGreaterEq + +instance (Ord opcode) + let compare = opcodeCompare + let (<) = opcodeLess + let (<=) = opcodeLessEq + let (>) = opcodeGreater + let (>=) = opcodeGreaterEq +end + + + + + let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2 (* this cannot be defaultCompare for OCaml because addresses contain big ints *) -- cgit v1.2.3 From 07fad742df72ff6e7bfb948c1c353a2cf12f5e28 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 31 Aug 2017 15:08:10 +0100 Subject: added RISC-V AMOs --- src/lem_interp/interp_inter_imp.lem | 39 ++++++++++++++++++++++++++++++++++++- src/lem_interp/sail_impl_base.lem | 25 ++++++++++++------------ 2 files changed, 51 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 6a9a77a1..411ad3fc 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1416,6 +1416,41 @@ let interp_instruction_analysis if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then inst_kind + + else if + (forall (inst_kind' MEM (inst_kind :: inst_kinds)). + match inst_kind' with + | IK_mem_read _ -> true + | IK_mem_write _ -> true + | IK_mem_rmw _ -> false + | IK_barrier _ -> false + | IK_cond_branch -> false + | IK_trans _ -> false + | IK_simple -> false + end) && + (exists (inst_kind' MEM (inst_kind :: inst_kinds)). + match inst_kind' with + | IK_mem_read _ -> true + | _ -> false + end) && + (exists (inst_kind' MEM (inst_kind :: inst_kinds)). + match inst_kind' with + | IK_mem_write _ -> true + | _ -> false + end) + then + match + List.partition + (function IK_mem_read _ -> true | _ -> false end) + (inst_kind :: inst_kinds) + with + | ((IK_mem_read r) :: rs, (IK_mem_write w) :: ws) -> + let () = ensure (forall (r' MEM rs). r' = IK_mem_read r) "more than one kind of read" in + let () = ensure (forall (w' MEM ws). w' = IK_mem_write w) "more than one kind of write" in + IK_mem_rmw (r, w) + | _ -> fail + end + (* the TSTART instruction can also be aborted so it will have two kinds of events *) else if (exists (inst_kind' MEM (inst_kind :: inst_kinds)). inst_kind' = IK_trans Transaction_start) && @@ -1424,7 +1459,9 @@ let interp_instruction_analysis || inst_kind' = IK_trans Transaction_abort) then IK_trans Transaction_start - else failwith "multiple instruction kinds" + + else + failwith "multiple instruction kinds" end in (regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind) diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 3886f919..721c0226 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -552,26 +552,27 @@ instance (Show trans_kind) end type instruction_kind = - | IK_barrier of barrier_kind - | IK_mem_read of read_kind + | IK_barrier of barrier_kind + | IK_mem_read of read_kind | IK_mem_write of write_kind -(* SS reinstating cond_branches -at present branches are not distinguished in the instruction_kind; -they just have particular nias (and will be IK_simple *) - | IK_cond_branch -(* | IK_uncond_branch *) - | IK_trans of trans_kind + | IK_mem_rmw of (read_kind * write_kind) + | IK_cond_branch + (* unconditional branches are not distinguished in the instruction_kind; + they just have particular nias (and will be IK_simple *) + (* | IK_uncond_branch *) + | IK_trans of trans_kind | 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_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_trans trans_kind -> "IK_trans " ^ (show trans_kind) - | IK_simple -> "IK_simple" + | IK_mem_rmw (r, w) -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w) + | IK_cond_branch -> "IK_cond_branch" + | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) + | IK_simple -> "IK_simple" end end -- cgit v1.2.3 From f83c3d00f60a2507dfa5c3f31de6ddfc08eee610 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Thu, 31 Aug 2017 17:25:30 +0100 Subject: add EnumerationType type class: if a type is a member you get Ord membership and Set membership for free --- src/lem_interp/sail_impl_base.lem | 361 ++++++++++---------------------------- 1 file changed, 89 insertions(+), 272 deletions(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 721c0226..c577c44b 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -42,6 +42,29 @@ open import Pervasives_extra + + +class ( EnumerationType 'a ) + val toNat : 'a -> nat +end + + +val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering +let ~{ocaml} enumeration_typeCompare e1 e2 = + compare (toNat e1) (toNat e2) +let inline {ocaml} enumeration_typeCompare = defaultCompare + + +default_instance forall 'a. EnumerationType 'a => (Ord 'a) + let compare = enumeration_typeCompare + let (<) r1 r2 = (enumeration_typeCompare r1 r2) = LT + let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT + let (>) r1 r2 = (enumeration_typeCompare r1 r2) = GT + let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT +end + + + (* maybe isn't a member of type Ord - this should be in the Lem standard library*) instance forall 'a. Ord 'a => (Ord (maybe 'a)) let compare = maybeCompare compare @@ -111,65 +134,21 @@ type opcode = Opcode of list byte (* of length 4 *) (** typeclass instantiations *) -let ~{ocaml} bitCompare (b1:bit) (b2:bit) = - match (b1,b2) with - | (Bitc_zero, Bitc_zero) -> EQ - | (Bitc_one, Bitc_one) -> EQ - | (Bitc_zero, _) -> LT - | (_,_) -> GT + +instance (EnumerationType bit) + let toNat = function + | Bitc_zero -> 0 + | Bitc_one -> 1 end -let inline {ocaml} bitCompare = defaultCompare - -let ~{ocaml} bitLess b1 b2 = bitCompare b1 b2 = LT -let ~{ocaml} bitLessEq b1 b2 = bitCompare b1 b2 <> GT -let ~{ocaml} bitGreater b1 b2 = bitCompare b1 b2 = GT -let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT - -let inline {ocaml} bitLess = defaultLess -let inline {ocaml} bitLessEq = defaultLessEq -let inline {ocaml} bitGreater = defaultGreater -let inline {ocaml} bitGreaterEq = defaultGreaterEq - -instance (Ord bit) - let compare = bitCompare - let (<) = bitLess - let (<=) = bitLessEq - let (>) = bitGreater - let (>=) = bitGreaterEq end -let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) = - match (bl1,bl2) with - | (Bitl_zero, Bitl_zero) -> EQ - | (Bitl_zero,_) -> LT - | (Bitl_one, Bitl_zero) -> GT - | (Bitl_one, Bitl_one) -> EQ - | (Bitl_one, _) -> LT - | (Bitl_undef,Bitl_zero) -> GT - | (Bitl_undef,Bitl_one) -> GT - | (Bitl_undef,Bitl_undef) -> EQ - | (Bitl_undef,_) -> LT - | (Bitl_unknown,Bitl_unknown) -> EQ - | (Bitl_unknown,_) -> GT +instance (EnumerationType bit_lifted) + let toNat = function + | Bitl_zero -> 0 + | Bitl_one -> 1 + | Bitl_undef -> 2 + | Bitl_unknown -> 3 end -let inline {ocaml} bit_liftedCompare = defaultCompare - -let ~{ocaml} bit_liftedLess b1 b2 = bit_liftedCompare b1 b2 = LT -let ~{ocaml} bit_liftedLessEq b1 b2 = bit_liftedCompare b1 b2 <> GT -let ~{ocaml} bit_liftedGreater b1 b2 = bit_liftedCompare b1 b2 = GT -let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT - -let inline {ocaml} bit_liftedLess = defaultLess -let inline {ocaml} bit_liftedLessEq = defaultLessEq -let inline {ocaml} bit_liftedGreater = defaultGreater -let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq - -instance (Ord bit_lifted) - let compare = bit_liftedCompare - let (<) = bit_liftedLess - let (<=) = bit_liftedLessEq - let (>) = bit_liftedGreater - let (>=) = bit_liftedGreaterEq end let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2 @@ -578,233 +557,71 @@ end -let ~{ocaml} read_kindCompare rk1 rk2 = - match (rk1, rk2) with - | (Read_plain, Read_plain) -> EQ - | (Read_plain, _) -> LT - | (_, Read_plain) -> GT - - | (Read_reserve, Read_reserve) -> EQ - | (Read_reserve, _) -> LT - | (_, Read_reserve) -> GT - - | (Read_acquire, Read_acquire) -> EQ - | (Read_acquire, _) -> LT - | (_, Read_acquire) -> GT - - | (Read_exclusive, Read_exclusive) -> EQ - | (Read_exclusive, _) -> LT - | (_, Read_exclusive) -> GT - - | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ - | (Read_exclusive_acquire, _) -> LT - | (_, Read_exclusive_acquire) -> GT - - | (Read_stream, Read_stream) -> EQ - | (Read_stream, _) -> LT - | (_, Read_stream) -> GT - - | (Read_RISCV_acquire, Read_RISCV_acquire) -> EQ - | (Read_RISCV_acquire, _) -> LT - | (_, Read_RISCV_acquire) -> GT - - | (Read_RISCV_reserved, Read_RISCV_reserved) -> EQ - | (Read_RISCV_reserved, _) -> LT - | (_, Read_RISCV_reserved) -> GT - - | (Read_RISCV_reserved_acquire, Read_RISCV_reserved_acquire) -> EQ - (*| (Read_RISCV_reserved_acquire, _) -> LT - | (_, Read_RISCV_reserved_acquire) -> GT*) +instance (EnumerationType read_kind) + let toNat = function + | Read_plain -> 0 + | Read_reserve -> 1 + | Read_acquire -> 2 + | Read_exclusive -> 3 + | Read_exclusive_acquire -> 4 + | Read_stream -> 5 + | Read_RISCV_acquire -> 6 + | Read_RISCV_reserved -> 7 + | Read_RISCV_reserved_acquire -> 8 end -let inline {ocaml} read_kindCompare = defaultCompare - -let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT -let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT -let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT -let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT - -let inline {ocaml} read_kindLess = defaultLess -let inline {ocaml} read_kindLessEq = defaultLessEq -let inline {ocaml} read_kindGreater = defaultGreater -let inline {ocaml} read_kindGreaterEq = defaultGreaterEq - -instance (Ord read_kind) - let compare = read_kindCompare - let (<) = read_kindLess - let (<=) = read_kindLessEq - let (>) = read_kindGreater - let (>=) = read_kindGreaterEq end -let ~{ocaml} write_kindCompare wk1 wk2 = - match (wk1, wk2) with - | (Write_plain, Write_plain) -> EQ - | (Write_plain, _) -> LT - | (_, Write_plain) -> GT - - | (Write_conditional, Write_conditional) -> EQ - | (Write_conditional, _) -> LT - | (_, Write_conditional) -> GT - - - | (Write_release, Write_release) -> EQ - | (Write_release, _) -> LT - | (_, Write_release) -> GT - - | (Write_exclusive, Write_exclusive) -> EQ - | (Write_exclusive, _) -> LT - | (_, Write_exclusive) -> GT - - | (Write_exclusive_release, Write_exclusive_release) -> EQ - | (Write_exclusive_release, _) -> LT - | (_, Write_exclusive_release) -> GT - - | (Write_RISCV_release, Write_RISCV_release) -> EQ - | (Write_RISCV_release, _) -> LT - | (_, Write_RISCV_release) -> GT - - | (Write_RISCV_conditional, Write_RISCV_conditional) -> EQ - | (Write_RISCV_conditional, _) -> LT - | (_, Write_RISCV_conditional) -> GT - - | (Write_RISCV_conditional_release, Write_RISCV_conditional_release) -> EQ - (*| (Write_RISCV_conditional_release, _) -> LT - | (_, Write_RISCV_conditional_release) -> GT*) +instance (EnumerationType write_kind) + let toNat = function + | Write_plain -> 0 + | Write_conditional -> 1 + | Write_release -> 2 + | Write_exclusive -> 3 + | Write_exclusive_release -> 4 + | Write_RISCV_release -> 5 + | Write_RISCV_conditional -> 6 + | Write_RISCV_conditional_release -> 7 end -let inline {ocaml} write_kindCompare = defaultCompare - -let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT -let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT -let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT -let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT - -let inline {ocaml} write_kindLess = defaultLess -let inline {ocaml} write_kindLessEq = defaultLessEq -let inline {ocaml} write_kindGreater = defaultGreater -let inline {ocaml} write_kindGreaterEq = defaultGreaterEq - -instance (Ord write_kind) - let compare = write_kindCompare - let (<) = write_kindLess - let (<=) = write_kindLessEq - let (>) = write_kindGreater - let (>=) = write_kindGreaterEq end - -let ~{ocaml} barrier_kindCompare bk1 bk2 = - match (bk1, bk2) with - | (Barrier_Sync, Barrier_Sync) -> EQ - | (Barrier_Sync, _) -> LT - | (_, Barrier_Sync) -> GT - - | (Barrier_LwSync, Barrier_LwSync) -> EQ - | (Barrier_LwSync, _) -> LT - | (_, Barrier_LwSync) -> GT - - | (Barrier_Eieio, Barrier_Eieio) -> EQ - | (Barrier_Eieio, _) -> LT - | (_, Barrier_Eieio) -> GT - - | (Barrier_Isync, Barrier_Isync) -> EQ - | (Barrier_Isync, _) -> LT - | (_, Barrier_Isync) -> GT - - | (Barrier_DMB, Barrier_DMB) -> EQ - | (Barrier_DMB, _) -> LT - | (_, Barrier_DMB) -> GT - - | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ - | (Barrier_DMB_ST, _) -> LT - | (_, Barrier_DMB_ST) -> GT - - | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ - | (Barrier_DMB_LD, _) -> LT - | (_, Barrier_DMB_LD) -> GT - - | (Barrier_DSB, Barrier_DSB) -> EQ - | (Barrier_DSB, _) -> LT - | (_, Barrier_DSB) -> GT - - | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ - | (Barrier_DSB_ST, _) -> LT - | (_, Barrier_DSB_ST) -> GT - - | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ - | (Barrier_DSB_LD, _) -> LT - | (_, Barrier_DSB_LD) -> GT - - | (Barrier_ISB, Barrier_ISB) -> EQ - | (Barrier_ISB, _) -> LT - | (_, Barrier_ISB) -> GT - - | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ - | (Barrier_TM_COMMIT, _) -> LT - | (_, Barrier_TM_COMMIT) -> GT - - | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ - | (Barrier_MIPS_SYNC, _) -> LT - | (_, Barrier_MIPS_SYNC) -> GT - - | (Barrier_RISCV_rw_rw, Barrier_RISCV_rw_rw) -> EQ - | (Barrier_RISCV_rw_rw, _) -> LT - | (_, Barrier_RISCV_rw_rw) -> GT - - | (Barrier_RISCV_r_rw, Barrier_RISCV_r_rw) -> EQ - | (Barrier_RISCV_r_rw, _) -> LT - | (_, Barrier_RISCV_r_rw) -> GT - - | (Barrier_RISCV_rw_w, Barrier_RISCV_rw_w) -> EQ - | (Barrier_RISCV_rw_w, _) -> LT - | (_, Barrier_RISCV_rw_w) -> GT - - | (Barrier_RISCV_w_w, Barrier_RISCV_w_w) -> EQ - | (Barrier_RISCV_w_w, _) -> LT - | (_, Barrier_RISCV_w_w) -> GT - - | (Barrier_RISCV_i, Barrier_RISCV_i) -> EQ - | (Barrier_RISCV_i, _) -> LT - | (_, Barrier_RISCV_i) -> GT - - | (Barrier_x86_MFENCE, Barrier_x86_MFENCE) -> EQ - (*| (Barrier_x86_MFENCE, _) -> LT - | (_, Barrier_x86_MFENCE) -> GT*) +instance (EnumerationType barrier_kind) + let toNat = function + | Barrier_Sync -> 0 + | Barrier_LwSync -> 1 + | Barrier_Eieio ->2 + | Barrier_Isync -> 3 + | Barrier_DMB -> 4 + | Barrier_DMB_ST -> 5 + | Barrier_DMB_LD -> 6 + | Barrier_DSB -> 7 + | Barrier_DSB_ST -> 8 + | Barrier_DSB_LD -> 9 + | Barrier_ISB -> 10 + | Barrier_TM_COMMIT -> 11 + | Barrier_MIPS_SYNC -> 12 + | Barrier_RISCV_rw_rw -> 13 + | Barrier_RISCV_r_rw -> 14 + | Barrier_RISCV_rw_w -> 15 + | Barrier_RISCV_w_w -> 16 + | Barrier_RISCV_i -> 17 + | Barrier_x86_MFENCE -> 18 end -let inline {ocaml} barrier_kindCompare = defaultCompare - -let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT -let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT -let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT -let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT - -let inline {ocaml} barrier_kindLess = defaultLess -let inline {ocaml} barrier_kindLessEq = defaultLessEq -let inline {ocaml} barrier_kindGreater = defaultGreater -let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq - -instance (Ord barrier_kind) - let compare = barrier_kindCompare - let (<) = barrier_kindLess - let (<=) = barrier_kindLessEq - let (>) = barrier_kindGreater - let (>=) = barrier_kindGreaterEq end - type event = -| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) -| E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name) -| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) -| E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) -| E_excl_res -| E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name) -| E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) -| E_barrier of barrier_kind -| E_footprint -| E_read_reg of reg_name -| E_write_reg of reg_name * register_value -| E_escape -| E_error of string + | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) + | E_read_memt of read_kind * address_lifted * nat * maybe (list reg_name) + | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) + | E_write_ea of write_kind * address_lifted * nat * maybe (list reg_name) + | E_excl_res + | E_write_memv of maybe address_lifted * memory_value * maybe (list reg_name) + | E_write_memvt of maybe address_lifted * (bit_lifted * memory_value) * maybe (list reg_name) + | E_barrier of barrier_kind + | E_footprint + | E_read_reg of reg_name + | E_write_reg of reg_name * register_value + | E_escape + | E_error of string let eventCompare e1 e2 = -- cgit v1.2.3 From 75022d46352525305b4c06b4988bf2df15f9f29e Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Sun, 3 Sep 2017 15:05:23 +0100 Subject: added RISC-V strong-acquire/release --- src/gen_lib/sail_values.lem | 3 +++ src/gen_lib/state.lem | 2 ++ src/lem_interp/sail_impl_base.lem | 24 ++++++++++++++++++------ 3 files changed, 23 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 49f37381..121f6cc8 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -956,3 +956,6 @@ let diafp_to_dia reginfo = function | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v) | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r) end + +let max = uncurry max +let min = uncurry min diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 2ea1247e..ac5cb869 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -55,8 +55,10 @@ let is_exclusive = function | Sail_impl_base.Read_exclusive_acquire -> true | Sail_impl_base.Read_stream -> false | Sail_impl_base.Read_RISCV_acquire -> false + | Sail_impl_base.Read_RISCV_strong_acquire -> false | Sail_impl_base.Read_RISCV_reserved -> true | Sail_impl_base.Read_RISCV_reserved_acquire -> true + | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true end diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index c577c44b..48ddd10e 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -436,7 +436,9 @@ type read_kind = (* AArch64 reads *) | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream (* RISC-V reads *) - | Read_RISCV_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire + | Read_RISCV_acquire | Read_RISCV_strong_acquire + | Read_RISCV_reserved | Read_RISCV_reserved_acquire + | Read_RISCV_reserved_strong_acquire instance (Show read_kind) let show = function @@ -447,8 +449,10 @@ instance (Show read_kind) | Read_exclusive_acquire -> "Read_exclusive_acquire" | Read_stream -> "Read_stream" | Read_RISCV_acquire -> "Read_RISCV_acquire" + | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire" | Read_RISCV_reserved -> "Read_RISCV_reserved" | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" + | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" end end @@ -460,7 +464,9 @@ type write_kind = (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release (* RISC-V *) - | Write_RISCV_release | Write_RISCV_conditional | Write_RISCV_conditional_release + | Write_RISCV_release | Write_RISCV_strong_release + | Write_RISCV_conditional | Write_RISCV_conditional_release + | Write_RISCV_conditional_strong_release instance (Show write_kind) let show = function @@ -470,8 +476,10 @@ instance (Show write_kind) | Write_exclusive -> "Write_exclusive" | Write_exclusive_release -> "Write_exclusive_release" | Write_RISCV_release -> "Write_RISCV_release" + | Write_RISCV_strong_release -> "Write_RISCV_strong_release" | Write_RISCV_conditional -> "Write_RISCV_conditional" | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" + | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" end end @@ -566,8 +574,10 @@ instance (EnumerationType read_kind) | Read_exclusive_acquire -> 4 | Read_stream -> 5 | Read_RISCV_acquire -> 6 - | Read_RISCV_reserved -> 7 - | Read_RISCV_reserved_acquire -> 8 + | Read_RISCV_strong_acquire -> 7 + | Read_RISCV_reserved -> 8 + | Read_RISCV_reserved_acquire -> 9 + | Read_RISCV_reserved_strong_acquire -> 10 end end @@ -579,8 +589,10 @@ instance (EnumerationType write_kind) | Write_exclusive -> 3 | Write_exclusive_release -> 4 | Write_RISCV_release -> 5 - | Write_RISCV_conditional -> 6 - | Write_RISCV_conditional_release -> 7 + | Write_RISCV_strong_release -> 6 + | Write_RISCV_conditional -> 7 + | Write_RISCV_conditional_release -> 8 + | Write_RISCV_conditional_strong_release -> 9 end end -- cgit v1.2.3 From a97cd6081df6a76c9daa34c773d82f21f5d014c8 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 15 Sep 2017 11:50:54 +0100 Subject: reinstate deep/shallow conversion --- src/gen_lib/deep_shallow_convert.lem | 116 ++++++++++++--------- src/lem_interp/sail_impl_base.lem | 2 + src/pretty_print.mli | 2 +- src/pretty_print_lem.ml | 191 +++++++++++++++++------------------ src/process_file.ml | 13 ++- 5 files changed, 176 insertions(+), 148 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 23c34222..4af6eb2f 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -6,20 +6,20 @@ open import Sail_values class (ToFromInterpValue 'a) - val toInterpValue : 'a -> Interp.value - val fromInterpValue : Interp.value -> 'a + val toInterpValue : 'a -> Interp_ast.value + val fromInterpValue : Interp_ast.value -> 'a end let toInterValueBool = function - | true -> Interp.V_lit (L_aux (L_one) Unknown) - | false -> Interp.V_lit (L_aux (L_zero) Unknown) + | true -> Interp_ast.V_lit (L_aux (L_one) Unknown) + | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown) end let rec fromInterpValueBool v = match v with - | Interp.V_lit (L_aux (L_true) _) -> true - | Interp.V_lit (L_aux (L_false) _) -> false - | Interp.V_lit (L_aux (L_one) _) -> true - | Interp.V_lit (L_aux (L_zero) _) -> false - | Interp.V_tuple [v] -> fromInterpValueBool v + | Interp_ast.V_lit (L_aux (L_true) _) -> true + | Interp_ast.V_lit (L_aux (L_false) _) -> false + | Interp_ast.V_lit (L_aux (L_one) _) -> true + | Interp_ast.V_lit (L_aux (L_zero) _) -> false + | Interp_ast.V_tuple [v] -> fromInterpValueBool v | v -> failwith ("fromInterpValue bool: unexpected value. " ^ Interp.debug_print_value v) end @@ -29,10 +29,10 @@ instance (ToFromInterpValue bool) end -let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown) +let toInterpValueUnit () = Interp_ast.V_lit (L_aux (L_unit) Unknown) let rec fromInterpValueUnit v = match v with - | Interp.V_lit (L_aux (L_unit) _) -> () - | Interp.V_tuple [v] -> fromInterpValueUnit v + | Interp_ast.V_lit (L_aux (L_unit) _) -> () + | Interp_ast.V_tuple [v] -> fromInterpValueUnit v | v -> failwith ("fromInterpValue unit: unexpected value. " ^ Interp.debug_print_value v) end @@ -44,8 +44,8 @@ end let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown) let rec fromInterpValueInteger v = match v with - | Interp.V_lit (L_aux (L_num i) _) -> i - | Interp.V_tuple [v] -> fromInterpValueInteger v + | Interp_ast.V_lit (L_aux (L_num i) _) -> i + | Interp_ast.V_tuple [v] -> fromInterpValueInteger v | v -> failwith ("fromInterpValue integer: unexpected value. " ^ Interp.debug_print_value v) end @@ -57,8 +57,8 @@ end let toInterpValueString s = V_lit (L_aux (L_string s) Unknown) let rec fromInterpValueString v = match v with - | Interp.V_lit (L_aux (L_string s) _) -> s - | Interp.V_tuple [v] -> fromInterpValueString v + | Interp_ast.V_lit (L_aux (L_string s) _) -> s + | Interp_ast.V_tuple [v] -> fromInterpValueString v | v -> failwith ("fromInterpValue integer: unexpected value. " ^ Interp.debug_print_value v) end @@ -69,17 +69,17 @@ end let toInterpValueBitU = function - | I -> Interp.V_lit (L_aux (L_one) Unknown) - | O -> Interp.V_lit (L_aux (L_zero) Unknown) - | Undef -> Interp.V_lit (L_aux (L_undef) Unknown) + | I -> Interp_ast.V_lit (L_aux (L_one) Unknown) + | O -> Interp_ast.V_lit (L_aux (L_zero) Unknown) + | Undef -> Interp_ast.V_lit (L_aux (L_undef) Unknown) end let rec fromInterpValueBitU v = match v with - | Interp.V_lit (L_aux (L_one) _) -> I - | Interp.V_lit (L_aux (L_zero) _) -> O - | Interp.V_lit (L_aux (L_undef) _) -> Undef - | Interp.V_lit (L_aux (L_true) _) -> I - | Interp.V_lit (L_aux (L_false) _) -> O - | Interp.V_tuple [v] -> fromInterpValueBitU v + | Interp_ast.V_lit (L_aux (L_one) _) -> B1 + | Interp_ast.V_lit (L_aux (L_zero) _) -> B0 + | Interp_ast.V_lit (L_aux (L_undef) _) -> BU + | Interp_ast.V_lit (L_aux (L_true) _) -> B1 + | Interp_ast.V_lit (L_aux (L_false) _) -> B0 + | Interp_ast.V_tuple [v] -> fromInterpValueBitU v | v -> failwith ("fromInterpValue bitU: unexpected value. " ^ Interp.debug_print_value v) end @@ -383,29 +383,31 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a)) end -module SI = Interp -module SIA = Interp_ast - - let read_kindToInterpValue = function | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ()) - | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) - | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) end let rec read_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain - | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag - | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream + | V_ctor (Id_aux (Id "Read_RISCV_acquire") _) _ _ v -> Read_RISCV_acquire + | V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") _) _ _ v -> Read_RISCV_strong_acquire + | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved + | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire + | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire | V_tuple [v] -> read_kindFromInterpValue v | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^ Interp.debug_print_value v) @@ -418,21 +420,27 @@ end let write_kindToInterpValue = function | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ()) - | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) - | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) + | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ()) + | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ()) + | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ()) + | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ()) + | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ()) end let rec write_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain - | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag - | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release + | V_ctor (Id_aux (Id "Write_RISCV_release") _) _ _ v -> Write_RISCV_release + | V_ctor (Id_aux (Id "Write_RISCV_strong_release") _) _ _ v -> Write_RISCV_strong_release + | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional + | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release + | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release | V_tuple [v] -> write_kindFromInterpValue v | v -> failwith ("fromInterpValue write_kind: unexpected value " ^ Interp.debug_print_value v) @@ -455,7 +463,14 @@ let barrier_kindToInterpValue = function | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) - | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) + | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) + | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) + | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ()) + | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ()) + | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ()) + | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ()) + | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ()) + | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ()) end let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync @@ -469,7 +484,14 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB + | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC + | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw + | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw + | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w + | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w + | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i + | V_ctor (Id_aux (Id "Barrier_x86_MFENCE") _) _ _ v -> Barrier_x86_MFENCE | V_tuple [v] -> barrier_kindFromInterpValue v | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^ Interp.debug_print_value v) @@ -503,18 +525,18 @@ instance (ToFromInterpValue instruction_kind) end let regfpToInterpValue = function - | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) - | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v) + | RFull v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RSlice v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RSliceBit v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) + | RField v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v) end let rec regfpFromInterpValue v = match v with - | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) - | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v) - | SI.V_tuple [v] -> regfpFromInterpValue v + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") _) _ _ v -> RFull (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v) + | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") _) _ _ v -> RField (fromInterpValue v) + | Interp_ast.V_tuple [v] -> regfpFromInterpValue v | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v) end diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 48ddd10e..e6169762 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -428,6 +428,8 @@ end (* Data structures for building up instructions *) +(* careful: changes in the read/write/barrier kinds have to be + reflected in deep_shallow_convert *) type read_kind = (* common reads *) | Read_plain diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 9a002454..034db664 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -52,7 +52,7 @@ val pat_to_string : tannot pat -> string val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit -val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit +val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit val pp_format_annot_ascii : tannot -> string diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 9758b2de..cf8fda59 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -50,7 +50,7 @@ open Pretty_print_common * PPrint-based sail-to-lem pprinter ****************************************************************************) -let print_to_from_interp_value = ref false +let print_to_from_interp_value = ref true let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar @@ -805,8 +805,8 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_lem_type id]) - (doc_typschm_lem regtypes typschm) + (doc_op equals (concat [string "type"; space; doc_id_lem_type id]) + (doc_typschm_lem regtypes typschm),empty) | TD_record(id,nm,typq,fs,_) -> let f_pp (typ,fid) = let fname = if prefix_recordtype @@ -814,19 +814,19 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with else doc_id_lem_type fid in concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals + (doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) - (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))) + (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))),empty) | TD_variant(id,nm,typq,ar,_) -> (match id with - | Id_aux ((Id "read_kind"),_) -> empty - | Id_aux ((Id "write_kind"),_) -> empty - | Id_aux ((Id "barrier_kind"),_) -> empty - | Id_aux ((Id "trans_kind"),_) -> empty - | Id_aux ((Id "instruction_kind"),_) -> empty - | Id_aux ((Id "regfp"),_) -> empty - | Id_aux ((Id "niafp"),_) -> empty - | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "read_kind"),_) -> (empty,empty) + | Id_aux ((Id "write_kind"),_) -> (empty,empty) + | Id_aux ((Id "barrier_kind"),_) -> (empty,empty) + | Id_aux ((Id "trans_kind"),_) -> (empty,empty) + | Id_aux ((Id "instruction_kind"),_) -> (empty,empty) + | Id_aux ((Id "regfp"),_) -> (empty,empty) + | Id_aux ((Id "niafp"),_) -> (empty,empty) + | Id_aux ((Id "diafp"),_) -> (empty,empty) | _ -> let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in let typ_pp = @@ -835,9 +835,9 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq ar_doc) in let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in + separate space [string "Interp_ast.Id_aux"; + parens (string "Interp_ast.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "Interp_ast.Unknown"] in let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let fromInterpValuePP = @@ -849,18 +849,18 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with match tu with | Tu_ty_id (ty,cid) -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid; parens (string "fromInterpValue v")] | Tu_id cid -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid]) ar) ^/^ - ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ + ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit @@ -879,43 +879,40 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with | Tu_ty_id (ty,cid) -> (separate space) [pipe;doc_id_lem_ctor cid;string "v";arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + string "Interp_ast.C_Union"; parens (string "toInterpValue v")] | Tu_id cid -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - string "SI.C_Union"; + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + string "Interp_ast.C_Union"; parens (string "toInterpValue ()")]) ar) ^/^ string "end") in let fromToInterpValuePP = + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - if !print_to_from_interp_value then - toInterpValuePP ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline - else empty) + (typ_pp ^^ hardline,fromToInterpValuePP ^^ hardline)) | TD_enum(id,nm,enums,_) -> (match id with - | Id_aux ((Id "read_kind"),_) -> empty - | Id_aux ((Id "write_kind"),_) -> empty - | Id_aux ((Id "barrier_kind"),_) -> empty - | Id_aux ((Id "trans_kind"),_) -> empty - | Id_aux ((Id "instruction_kind"),_) -> empty - | Id_aux ((Id "regfp"),_) -> empty - | Id_aux ((Id "niafp"),_) -> empty - | Id_aux ((Id "diafp"),_) -> empty + | Id_aux ((Id "read_kind"),_) -> (empty,empty) + | Id_aux ((Id "write_kind"),_) -> (empty,empty) + | Id_aux ((Id "barrier_kind"),_) -> (empty,empty) + | Id_aux ((Id "trans_kind"),_) -> (empty,empty) + | Id_aux ((Id "instruction_kind"),_) -> (empty,empty) + | Id_aux ((Id "regfp"),_) -> (empty,empty) + | Id_aux ((Id "niafp"),_) -> (empty,empty) + | Id_aux ((Id "diafp"),_) -> (empty,empty) | _ -> let rec range i j = if i > j then [] else i :: (range (i+1) j) in let nats = range 0 in @@ -926,9 +923,9 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let make_id pat id = - separate space [string "SIA.Id_aux"; - parens (string "SIA.Id " ^^ string_lit (doc_id id)); - if pat then underscore else string "SIA.Unknown"] in + separate space [string "Interp_ast.Id_aux"; + parens (string "Interp_ast.Id " ^^ string_lit (doc_id id)); + if pat then underscore else string "Interp_ast.Unknown"] in let fromInterpValuePP = (prefix 2 1) (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"]) @@ -936,7 +933,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ((separate_map (break 1)) (fun (cid) -> (separate space) - [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; + [pipe;string "Interp_ast.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow;doc_id_lem_ctor cid] ) enums @@ -944,7 +941,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ( (align ((prefix 3 1) - (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow]) + (separate space [pipe;string ("Interp_ast.V_lit (Interp_ast.L_aux (Interp_ast.L_num n) _)");arrow]) (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^ ( ((separate_map (break 1)) @@ -960,7 +957,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with ) ) ^/^ - ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ + ((separate space) [pipe;string "Interp_ast.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit @@ -978,25 +975,23 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with (fun (cid,number) -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; - string "SI.V_ctor"; + string "Interp_ast.V_ctor"; parens (make_id false cid); - parens (string "SIA.T_id " ^^ string_lit (doc_id id)); - parens (string ("SI.C_Enum " ^ string_of_int number)); + parens (string "Interp_ast.T_id " ^^ string_lit (doc_id id)); + parens (string ("Interp_ast.C_Enum " ^ string_of_int number)); parens (string "toInterpValue ()")]) (List.combine enums (nats ((List.length enums) - 1)))) ^/^ string "end") in let fromToInterpValuePP = + toInterpValuePP ^^ hardline ^^ hardline ^^ + fromInterpValuePP ^^ hardline ^^ hardline ^^ ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in - typ_pp ^^ hardline ^^ hardline ^^ - if !print_to_from_interp_value - then toInterpValuePP ^^ hardline ^^ hardline ^^ - fromInterpValuePP ^^ hardline ^^ hardline ^^ - fromToInterpValuePP ^^ hardline - else empty) + (typ_pp ^^ hardline, + fromToInterpValuePP ^^ hardline)) | TD_register(id,n1,n2,rs) -> match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> @@ -1010,11 +1005,11 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with let dir_b = i1 < i2 in let dir = string (if dir_b then "true" else "false") in let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in - (doc_op equals) + ((doc_op equals) (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) (string "Register" ^^ space ^^ align (separate space [string "regname"; doc_int size; doc_int i1; dir; - break 0 ^^ brackets (align doc_rids)])) + break 0 ^^ brackets (align doc_rids)])),empty) (*^^ hardline ^^ separate_map hardline doc_rfield rs *) @@ -1147,26 +1142,29 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) = let rec doc_def_lem regtypes def = match def with - | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty) - | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty) - | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty) + | DEF_spec v_spec -> ((doc_spec_lem regtypes v_spec,empty),empty) + | DEF_type t_def -> + let (typdefs,fromtodefs) = doc_typdef_lem regtypes t_def in + ((group typdefs ^/^ hardline,fromtodefs),empty) + | DEF_reg_dec dec -> ((group (doc_dec_lem dec),empty),empty) - | DEF_default df -> (empty,empty) - | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline) - | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline) + | DEF_default df -> ((empty,empty),empty) + | DEF_fundef f_def -> ((empty,empty),group (doc_fundef_lem regtypes f_def) ^/^ hardline) + | DEF_val lbind -> ((empty,empty),group (doc_let_lem regtypes lbind) ^/^ hardline) | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" - | DEF_kind _ -> (empty,empty) + | DEF_kind _ -> ((empty,empty),empty) - | DEF_comm (DC_comm s) -> (empty,comment (string s)) + | DEF_comm (DC_comm s) -> ((empty,empty),comment (string s)) | DEF_comm (DC_comm_struct d) -> - let (typdefs,vdefs) = doc_def_lem regtypes d in - (empty,comment (typdefs ^^ hardline ^^ vdefs)) + let ((typdefs,tofromdefs),vdefs) = doc_def_lem regtypes d in + ((empty,empty),comment (typdefs ^^ hardline ^^ tofromdefs ^^ hardline ^^ vdefs)) let doc_defs_lem regtypes (Defs defs) = let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in - (separate empty typdefs,separate empty valdefs) + let (typdefs,tofromdefs) = List.split typdefs in + (separate empty typdefs,separate empty tofromdefs, separate empty valdefs) let find_regtypes (Defs defs) = List.fold_left @@ -1180,38 +1178,33 @@ let find_regtypes (Defs defs) = let typ_to_t env = Type_check.typ_to_t env false false -let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = +let pp_defs_lem + (types_file,types_modules) + (prompt_file,prompt_modules) + (state_file,state_modules) + (tofrom_file,tofrom_modules) + d top_line = + let pp_aux file modules defs = + (print file) + (concat + [string "(*" ^^ (string top_line) ^^ string "*)";hardline; + (separate_map hardline) + (fun lib -> separate space [string "open import";string lib]) modules;hardline; + defs]); + in + + let regtypes = find_regtypes d in - let (typdefs,valdefs) = doc_defs_lem regtypes d in - (print types_file) - (concat - [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) types_modules;hardline; - if !print_to_from_interp_value - then - concat - [(separate_map hardline) - (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; - string "open import Deep_shallow_convert"; - hardline; - hardline; - string "module SI = Interp"; hardline; - string "module SIA = Interp_ast"; hardline; - hardline] - else empty; - typdefs]); - (print prompt_file) - (concat - [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline; - hardline; - valdefs]); - (print state_file) + let (typdefs,tofromdefs,valdefs) = doc_defs_lem regtypes d in + + pp_aux types_file types_modules typdefs; + pp_aux prompt_file prompt_modules valdefs; + pp_aux state_file state_modules valdefs; + + (print tofrom_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; - (separate_map hardline) - (fun lib -> separate space [string "open import";string lib]) state_modules;hardline; - hardline; - valdefs]); + (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) tofrom_modules;hardline; + (separate_map hardline) (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"];hardline; + string "open import Deep_shallow_convert"; + hardline;tofromdefs]) diff --git a/src/process_file.ml b/src/process_file.ml index 273979cf..39a8bf58 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -172,18 +172,23 @@ let output1 libpath out_arg filename defs = | Lem_out None -> let generated_line = generated_line filename in let types_module = (f' ^ "_embed_types") in + let tofrom_module = (f' ^ "_toFromInterp") in let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embed_types.lem") in let ((o',_, _) as ext_o') = open_output_with_check_unformatted (f' ^ "_embed.lem") in let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in + let ((o''',_, _) as ext_o''') = + open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in (Pretty_print.pp_defs_lem (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; String.capitalize types_module]) (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; String.capitalize types_module]) + (o''',["Pervasives_extra";"Sail_impl_base";"Sail_values"; + String.capitalize types_module]) defs generated_line); close_output_with_check ext_o; close_output_with_check ext_o'; @@ -191,22 +196,28 @@ let output1 libpath out_arg filename defs = | Lem_out (Some lib) -> let generated_line = generated_line filename in let types_module = (f' ^ "_embed_types") in + let tofrom_module = (f' ^ "_toFromInterp") in let ((o,_, _) as ext_o) = open_output_with_check_unformatted (f' ^ "_embed_types.lem") in let ((o',_, _) as ext_o') = open_output_with_check_unformatted (f' ^ "_embed.lem") in let ((o'',_, _) as ext_o'') = open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in + let ((o''',_, _) as ext_o''') = + open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in (Pretty_print.pp_defs_lem (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; "Sail_values";String.capitalize types_module;lib]) (o'',["Pervasives_extra";"Sail_impl_base";"State"; "Sail_values";String.capitalize types_module;lib ^ "_sequential"]) + (o''',["Pervasives_extra";"Sail_impl_base"; + "Sail_values";String.capitalize types_module;lib]) defs generated_line); close_output_with_check ext_o; close_output_with_check ext_o'; - close_output_with_check ext_o'' + close_output_with_check ext_o''; + close_output_with_check ext_o''' | Ocaml_out None -> let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; -- cgit v1.2.3 From 3a4358d34cca39d61da4a21953be2a55f0a0a89e Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 15 Sep 2017 18:26:16 +0100 Subject: x86: implement regfp analysis function (no control flow yet) --- src/lem_interp/interp_inter_imp.lem | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 411ad3fc..6ee13d60 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -587,7 +587,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Barrier_DSB_ST" -> Barrier_DSB_ST | "Barrier_DSB_LD" -> Barrier_DSB_LD | "Barrier_ISB" -> Barrier_ISB - | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC + | "Barrier_MIPS_SYNC" -> Barrier_MIPS_SYNC + | "Barrier_x86_MFENCE" -> Barrier_x86_MFENCE end) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> -- cgit v1.2.3 From c3b5af179dde8d0b2c272eb851ebdb59764468d0 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 19 Sep 2017 19:45:36 +0300 Subject: fix --- src/gen_lib/deep_shallow_convert.lem | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 4af6eb2f..42a65c49 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -69,9 +69,9 @@ end let toInterpValueBitU = function - | I -> Interp_ast.V_lit (L_aux (L_one) Unknown) - | O -> Interp_ast.V_lit (L_aux (L_zero) Unknown) - | Undef -> Interp_ast.V_lit (L_aux (L_undef) Unknown) + | B1 -> Interp_ast.V_lit (L_aux (L_one) Unknown) + | B0 -> Interp_ast.V_lit (L_aux (L_zero) Unknown) + | BU -> Interp_ast.V_lit (L_aux (L_undef) Unknown) end let rec fromInterpValueBitU v = match v with | Interp_ast.V_lit (L_aux (L_one) _) -> B1 @@ -391,10 +391,10 @@ let read_kindToInterpValue = function | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ()) - | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) - | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) - | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) - | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) + | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) + | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_RISCV_reserved_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) end let rec read_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain -- cgit v1.2.3 From a02e52919de565fc3fba82723b48200fbf034ff9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Wed, 20 Sep 2017 15:38:14 +0100 Subject: add support for x86 lock prefix (also remove unused Read/Write_tag kind in etc/regfp.sail. --- src/lem_interp/sail_impl_base.lem | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index e6169762..e39c4421 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -441,6 +441,7 @@ type read_kind = | Read_RISCV_acquire | Read_RISCV_strong_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire | Read_RISCV_reserved_strong_acquire + | Read_X86_locked instance (Show read_kind) let show = function @@ -455,6 +456,7 @@ instance (Show read_kind) | Read_RISCV_reserved -> "Read_RISCV_reserved" | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" + | Read_X86_locked -> "Read_X86_locked" end end @@ -469,6 +471,7 @@ type write_kind = | Write_RISCV_release | Write_RISCV_strong_release | Write_RISCV_conditional | Write_RISCV_conditional_release | Write_RISCV_conditional_strong_release + | Write_X86_locked instance (Show write_kind) let show = function @@ -482,6 +485,7 @@ instance (Show write_kind) | Write_RISCV_conditional -> "Write_RISCV_conditional" | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" + | Write_X86_locked -> "Write_X86_locked" end end @@ -580,6 +584,7 @@ instance (EnumerationType read_kind) | Read_RISCV_reserved -> 8 | Read_RISCV_reserved_acquire -> 9 | Read_RISCV_reserved_strong_acquire -> 10 + | Read_X86_locked -> 11 end end @@ -595,6 +600,7 @@ instance (EnumerationType write_kind) | Write_RISCV_conditional -> 7 | Write_RISCV_conditional_release -> 8 | Write_RISCV_conditional_strong_release -> 9 + | Write_X86_locked -> 10 end end -- cgit v1.2.3 From 83adaea79d0ae53ff898985fdd359fbca7773de3 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 21 Sep 2017 09:51:41 +0100 Subject: added a comment to the x86 lock'd read and write --- src/lem_interp/sail_impl_base.lem | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index e39c4421..6957bb95 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -441,7 +441,8 @@ type read_kind = | Read_RISCV_acquire | Read_RISCV_strong_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire | Read_RISCV_reserved_strong_acquire - | Read_X86_locked + (* x86 reads *) + | Read_X86_locked (* the read part of a lock'd instruction (rmw) *) instance (Show read_kind) let show = function @@ -471,7 +472,8 @@ type write_kind = | Write_RISCV_release | Write_RISCV_strong_release | Write_RISCV_conditional | Write_RISCV_conditional_release | Write_RISCV_conditional_strong_release - | Write_X86_locked + (* x86 writes *) + | Write_X86_locked (* the write part of a lock'd instruction (rmw) *) instance (Show write_kind) let show = function -- cgit v1.2.3 From 2148a88c9e9d16e07be1439ddc36ed69c31ee74c Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 21 Sep 2017 10:52:23 +0100 Subject: wib --- src/gen_lib/state.lem | 1 + 1 file changed, 1 insertion(+) (limited to 'src') diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index ac5cb869..88e29522 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -59,6 +59,7 @@ let is_exclusive = function | Sail_impl_base.Read_RISCV_reserved -> true | Sail_impl_base.Read_RISCV_reserved_acquire -> true | Sail_impl_base.Read_RISCV_reserved_strong_acquire -> true + | Sail_impl_base.Read_X86_locked -> true end -- cgit v1.2.3 From 72e597901e710f1549d387d9c1326b04be42e9d2 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Tue, 26 Sep 2017 12:23:46 +0100 Subject: fixes --- src/gen_lib/deep_shallow_convert.lem | 40 ++++++++++++++++++++---------------- 1 file changed, 22 insertions(+), 18 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 42a65c49..86365b78 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -385,16 +385,17 @@ end let read_kindToInterpValue = function | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ()) - | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) - | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) - | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) - | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) - | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) - | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ()) - | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) - | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) - | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ()) + | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ()) + | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ()) + | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ()) + | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ()) + | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ()) + | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ()) + | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ()) + | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ()) | Read_RISCV_reserved_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ()) + | Read_X86_locked -> V_ctor (Id_aux (Id "Read_X86_locked") Unknown) (T_id "read_kind") (C_Enum 11) (toInterpValue ()) end let rec read_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain @@ -408,6 +409,7 @@ let rec read_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire + | V_ctor (Id_aux (Id "Read_X86_locked") _) _ _ v -> Read_X86_locked | V_tuple [v] -> read_kindFromInterpValue v | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^ Interp.debug_print_value v) @@ -420,15 +422,16 @@ end let write_kindToInterpValue = function | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ()) - | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) - | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) - | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) - | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) - | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ()) - | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ()) - | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ()) - | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ()) - | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ()) + | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ()) + | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ()) + | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ()) + | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ()) + | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ()) + | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ()) + | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ()) + | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ()) + | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ()) + | Write_X86_locked -> V_ctor (Id_aux (Id "Write_X86_locked") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ()) end let rec write_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain @@ -441,6 +444,7 @@ let rec write_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release + | V_ctor (Id_aux (Id "Write_X86_locked") _) _ _ v -> Write_X86_locked | V_tuple [v] -> write_kindFromInterpValue v | v -> failwith ("fromInterpValue write_kind: unexpected value " ^ Interp.debug_print_value v) -- cgit v1.2.3 From efa98fb796fdab5486193f792adf999826fde7b4 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 29 Sep 2017 17:02:38 +0100 Subject: fix deep_shallow_convert, stop using interp_interface.instruction for most things, SF and CP bugfixing --- src/gen_lib/deep_shallow_convert.lem | 29 ++++++++++++++++++-- src/lem_interp/interp.lem | 4 +-- src/lem_interp/interp_inter_imp.lem | 53 ++++++++++++++++++------------------ src/lem_interp/interp_interface.lem | 10 +++++-- src/lem_interp/sail_impl_base.lem | 2 -- 5 files changed, 62 insertions(+), 36 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 86365b78..5a0dd99e 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -15,10 +15,10 @@ let toInterValueBool = function | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown) end let rec fromInterpValueBool v = match v with - | Interp_ast.V_lit (L_aux (L_true) _) -> true - | Interp_ast.V_lit (L_aux (L_false) _) -> false | Interp_ast.V_lit (L_aux (L_one) _) -> true + | Interp_ast.V_lit (L_aux (L_true) _) -> true | Interp_ast.V_lit (L_aux (L_zero) _) -> false + | Interp_ast.V_lit (L_aux (L_false) _) -> false | Interp_ast.V_tuple [v] -> fromInterpValueBool v | v -> failwith ("fromInterpValue bool: unexpected value. " ^ Interp.debug_print_value v) @@ -78,7 +78,7 @@ let rec fromInterpValueBitU v = match v with | Interp_ast.V_lit (L_aux (L_zero) _) -> B0 | Interp_ast.V_lit (L_aux (L_undef) _) -> BU | Interp_ast.V_lit (L_aux (L_true) _) -> B1 - | Interp_ast.V_lit (L_aux (L_false) _) -> B0 + | Interp_ast.V_lit (L_aux (L_false) _) -> B0 | Interp_ast.V_tuple [v] -> fromInterpValueBitU v | v -> failwith ("fromInterpValue bitU: unexpected value. " ^ Interp.debug_print_value v) @@ -506,18 +506,41 @@ instance (ToFromInterpValue barrier_kind) end +let trans_kindToInterpValue = function + | Transaction_start -> V_ctor (Id_aux (Id "Transaction_start") Unknown) (T_id "trans_kind") (C_Enum 0) (toInterpValue ()) + | Transaction_commit -> V_ctor (Id_aux (Id "Transaction_commit") Unknown) (T_id "trans_kind") (C_Enum 1) (toInterpValue ()) + | Transaction_abort -> V_ctor (Id_aux (Id "Transaction_abort") Unknown) (T_id "trans_kind") (C_Enum 2) (toInterpValue ()) + end +let rec trans_kindFromInterpValue v = match v with + | V_ctor (Id_aux (Id "Transaction_start") _) _ _ v -> Transaction_start + | V_ctor (Id_aux (Id "Transaction_commit") _) _ _ v -> Transaction_commit + | V_ctor (Id_aux (Id "Transaction_abort") _) _ _ v -> Transaction_abort + | V_tuple [v] -> trans_kindFromInterpValue v + | v -> failwith ("fromInterpValue trans_kind: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue trans_kind) + let toInterpValue = trans_kindToInterpValue + let fromInterpValue = trans_kindFromInterpValue +end + + let instruction_kindToInterpValue = function | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) + | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) end let rec instruction_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) + | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v) | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v) | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple | V_tuple [v] -> instruction_kindFromInterpValue v | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^ diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 58874fa6..f00458b7 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1424,8 +1424,8 @@ let rec match_pattern t_level (P_aux p (_, annot)) value_whole = | V_ctor (Id_aux cid _) t ckind v -> if id = cid then (match (pats,detaint v) with - | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv) - | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,eenv) + | ([],(V_lit (L_aux L_unit _))) -> (true,false,eenv) + | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,false,eenv) | ([p],_) -> match_pattern t_level p v | _ -> (false,false,eenv) end) else (false,false,eenv) diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 6ee13d60..52acae1e 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -469,7 +469,7 @@ let translate_address top_level end_flag thunk_name registers address = let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (address_error,events) = - interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction + interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume int_mode @@ -504,17 +504,16 @@ let intern_instruction direction (name,parms) = Interp_ast.V_ctor (Interp.id_of_string name) (T_id "ast") Interp_ast.C_Union (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms)) -let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction = +let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers (instruction : Interp_ast.value) = let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in let mode = make_mode true false debug in let int_mode = mode.internal_mode in - let intern_val = intern_instruction direction instruction in - let val_str = Interp.string_of_value intern_val in - let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in + let val_str = Interp.string_of_value instruction in + let (arg,_) = Interp.to_exp int_mode Interp.eenv instruction in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (analysis_or_error,events) = - interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction + interp_to_value_helper debug Nothing Ivh_analysis val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume int_mode @@ -680,7 +679,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in let (instr_decoded_error,events) = - interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false + interp_to_value_helper debug (Just value) Ivh_decode val_str (V_list []) internal_direction registers [] false (fun _ -> Interp.resume mode (Interp.Thunk_frame @@ -688,9 +687,9 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in match (instr_decoded_error) with | Ivh_value instr -> - let instr_external = interp_value_to_instr_external top_level instr in + (* let instr_external = interp_value_to_instr_external top_level instr in*) let (instr_decoded_error,events) = - interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction + interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr (*instr_external*) internal_direction registers [] false (fun _ -> Interp.resume mode @@ -699,7 +698,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro (Interp_ast.Unknown, Nothing)) top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in match (instr_decoded_error) with - | Ivh_value _ -> IDE_instr instr_external instr + | Ivh_value _ -> IDE_instr instr (*instr_external*) | Ivh_value_after_exn v -> Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now" | Ivh_error err -> IDE_decode_error err @@ -713,9 +712,9 @@ end let decode_to_istate (top_level:context) registers (value:opcode) : i_state_or_error = let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in match decode_to_instruction top_level registers value with - | IDE_instr instr instrv -> + | IDE_instr instr -> let mode = make_interpreter_mode true false in - let (arg,_) = Interp.to_exp mode Interp.eenv instrv in + let (arg,_) = Interp.to_exp mode Interp.eenv instr in Instr instr (IState (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) @@ -750,11 +749,11 @@ let instr_external_to_interp_value top_level instr = Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) (T_id "ast") Interp_ast.C_Union parmsV -val instruction_to_istate : context -> instruction -> instruction_state -let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state = +val instruction_to_istate : context -> Interp_ast.value -> instruction_state +let instruction_to_istate (top_level:context) (instr:Interp_ast.value) : instruction_state = let mode = make_interpreter_mode true false in let (Context top_env _ _ _ _ _ _ _ _ _ _) = top_level in - let ast_node = fst (Interp.to_exp mode Interp.eenv (instr_external_to_interp_value top_level instr)) in + let ast_node = fst (Interp.to_exp mode Interp.eenv instr) in (IState (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [ast_node]) @@ -1092,7 +1091,7 @@ and state_to_outcome_s pp_instruction_state mode state = (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state)) ) -val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit +val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> Interp_ast.value -> Sail_impl_base.outcome_s unit let initial_outcome_s_of_instruction pp_instruction_state context mode instruction = let state = instruction_to_istate context instruction in state_to_outcome_s pp_instruction_state mode state @@ -1222,14 +1221,15 @@ let nia_address_of_event nia_reg (event: event) : maybe (maybe address) = | _ -> Nothing end -let nias_of_instruction +let nias_of_instruction + top_level thread_ism (nia_address: list (maybe address)) (* Nothing for unknown/undef*) (regs_in: list reg_name) - (instruction: instruction) + (instruction: Interp_ast.value) : list nia = - let (instruction_name, instruction_fields) = instruction in + let (instruction_name, instruction_fields) = interp_value_to_instr_external top_level instruction in let unknown_nia_address = List.elem Nothing nia_address in @@ -1390,7 +1390,9 @@ let nias_of_instruction | (s1, s2) -> failwith ("unexpected (thread_ism, instruction_name): (" ^ s1 ^ ", " ^ s2 ^ ")") end + let interp_instruction_analysis + top_level (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) instruction nia_reg ism environment = @@ -1403,7 +1405,7 @@ let interp_instruction_analysis let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in - let nias = nias_of_instruction ism nia_address regs_in instruction in + let nias = nias_of_instruction top_level ism nia_address regs_in instruction in let dia = DIA_none in (* FIX THIS! *) @@ -1478,29 +1480,28 @@ val print_and_fail_of_inequal : forall 'a. Show 'a => (instruction -> string) -> (string * 'a) -> (string * 'a) -> unit let print_and_fail_if_inequal - (print_endline,pp_instruction,instruction) + (print_endline,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) + failwith (name1^" and "^ name2^" inequal for instruction: \n" ^ Interp.string_of_value instruction) let interp_compare_analyses print_endline - pp_instruction (non_pseudo_registers : set reg_name -> set reg_name) context endianness interp_exhaustive - instruction + (instruction : Interp_ast.value) 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 + interp_instruction_analysis context interp_exhaustive instruction nia_reg ism environment in let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) = (Set.fromList regs_in1, @@ -1525,7 +1526,7 @@ let interp_compare_analyses non_pseudo_registers regs_out2S, non_pseudo_registers regs_feeding_address2S) in - let aux = (print_endline,pp_instruction,instruction) in + let aux = (print_endline,instruction) in let () = (print_and_fail_if_inequal aux) ("regs_in exhaustive",regs_in1S) ("regs_in hand",regs_in2S) in diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index dcc9f537..07d9e2b3 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -104,6 +104,10 @@ end and the potential static effects from the funcl clause for this instruction Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values *) + + +type instruction_field_value = list bit + type instruction = (string * list (string * instr_parm_typ * instruction_field_value)) let {coq} instructionEqual i1 i2 = match (i1,i2) with @@ -117,7 +121,7 @@ let inline ~{coq} instructionInequal = unsafe_structural_inequality type v_kind = Bitv | Bytev type decode_error = - | Unsupported_instruction_error of instruction + | Unsupported_instruction_error of Interp_ast.value | Not_an_instruction_error of opcode | Internal_error of string @@ -264,12 +268,12 @@ val initial_instruction_state : context -> string -> list register_value -> inst (* string is a function name, list of value are the parameters to that function *) type instruction_or_decode_error = - | IDE_instr of instruction * Interp_ast.value + | IDE_instr of Interp_ast.value | IDE_decode_error of decode_error (** propose to remove the following type and use the above instead *) type i_state_or_error = - | Instr of instruction * instruction_state + | Instr of Interp_ast.value * instruction_state | Decode_error of decode_error diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 6957bb95..4f07f574 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -106,8 +106,6 @@ type register_value = <| type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*) -type instruction_field_value = list bit - type byte = Byte of list bit (* of length 8 *) (*MSB first everywhere*) type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer -- cgit v1.2.3 From 9f58a1bbaadd0a679413a8cb424acfb6255f8eca Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Fri, 29 Sep 2017 17:55:48 +0100 Subject: fix those build errors --- src/lem_interp/run_with_elf.ml | 10 +++++++--- src/lem_interp/run_with_elf_cheri.ml | 6 ++++-- src/lem_interp/run_with_elf_cheri128.ml | 6 ++++-- 3 files changed, 15 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 2a1783db..98b98a03 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1198,12 +1198,16 @@ let rec fde_loop count context model mode track_dependencies addr_trans = 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); + let instruction = interp_value_to_instr_external context instruction in + 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.Unsupported_instruction_error instruction -> + let instruction = interp_value_to_instr_external context instruction in + errorf "\n**** Encountered unsupported instruction %s ****\n" + (Printing_functions.instruction_to_string instruction) | Interp_interface.Not_an_instruction_error op -> (match op with | Opcode bytes -> diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index e773bf5b..b879f702 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1290,12 +1290,14 @@ let rec fde_loop count context model mode track_dependencies addr_trans = let opcode = Opcode (get_opcode pc) in let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with | Instr(instruction,istate) -> + let instruction = interp_value_to_instr_external context instruction in 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.Unsupported_instruction_error instruction -> + let instruction = interp_value_to_instr_external context instruction in + errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instruction) | Interp_interface.Not_an_instruction_error op -> (match op with | Opcode bytes -> diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index cd2e7312..3ad507bc 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1290,12 +1290,14 @@ let rec fde_loop count context model mode track_dependencies addr_trans = let opcode = Opcode (get_opcode pc) in let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with | Instr(instruction,istate) -> + let instruction = interp_value_to_instr_external context instruction in 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.Unsupported_instruction_error instruction -> + let instruction = interp_value_to_instr_external context instruction in + errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instruction) | Interp_interface.Not_an_instruction_error op -> (match op with | Opcode bytes -> -- cgit v1.2.3 From dd733219d795bd59516c54717e798ced9c378d33 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 6 Oct 2017 14:47:23 +0100 Subject: move nias_of_instruction into RMEM so that it can use shallow embedding ast and not obsolete interp_interface one. --- src/lem_interp/interp_inter_imp.lem | 180 ++---------------------------------- 1 file changed, 7 insertions(+), 173 deletions(-) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 52acae1e..c0d2ea4a 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1221,180 +1221,13 @@ let nia_address_of_event nia_reg (event: event) : maybe (maybe address) = | _ -> Nothing end -let nias_of_instruction - top_level - thread_ism - (nia_address: list (maybe address)) (* Nothing for unknown/undef*) - (regs_in: list reg_name) - (instruction: Interp_ast.value) - : list nia - = - let (instruction_name, instruction_fields) = interp_value_to_instr_external top_level instruction in - - let unknown_nia_address = List.elem Nothing nia_address in - - let nias = [NIA_concrete_address addr | forall (addr MEM (List.mapMaybe id nia_address)) | true] in - - (* it's a fact of the Power2.06B instruction pseudocode that in the B and Bc - cases there should be no Unknown values in nia_values, while in the Bclr - and Bcctr cases nia_values will just be Unknown and the semantics should - match the comments in the machineDefTypes definition of nia *) - (* All our other analysis is on the pseudocode directly, which is arguably - pleasingly robust. We could replace the nias pattern match on - instruction_name with something in that style if the exhaustive interpreter - announced register dependencies to register writes (easy) and if it could - check the form of the register writes to LR and CTR matches the - machineDefTypes nia definition *) - match (thread_ism, instruction_name) with - | ("PPCGEN_ism", "B") -> - let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values 1" in - nias - | ("PPCGEN_ism", "Bc") -> - let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values 2" in - NIA_successor :: nias - | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ] - | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ] - | ("PPCGEN_ism", "Sc") -> - let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values 3" in - match instruction_fields with - | [(_, _, lev)] -> - (* LEV field is 7 bits long, pad it with false at beginning *) - if lev = [Bitc_zero;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one;Bitc_one] - (* (Interp_inter_imp.integer_of_byte_list (Interp_inter_imp.to_bytes (false :: bl))) = 63 *) - then [] - else [NIA_successor] - | _ -> [ NIA_successor ] - end - | ("PPCGEN_ism", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"PPCGEN_ism\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - (* AARch64 label branch (i.e. address must be known) although - these instructions take the address as an offset from PC, in here - we see the absolute address as it was extracted from the micro ops - just before write to PC *) - | ("AArch64HandSail", "BranchImmediate") -> nias - | ("AArch64HandSail", "BranchConditional") -> NIA_successor :: nias - | ("AArch64HandSail", "CompareAndBranch") -> NIA_successor :: nias - | ("AArch64HandSail", "TestBitAndBranch") -> NIA_successor :: nias - - (* AArch64 calculated address branch *) - | ("AArch64HandSail", "BranchRegister") -> - (* do some parsing of the ast fields to figure out which register holds - the branching address i.e. find n in "BR ". The ast constructor - from armV8.sail: (reg_index,BranchType) BranchRegister; *) - let n_integer = - match instruction_fields with - | [(_, _, n); _] -> integer_of_bit_list n - | _ -> fail - end - in - let () = ensure (0 <= n_integer && n_integer <= 31) - "expected register number from 0 to 31" - in - if n_integer = 31 then - nias (* BR XZR *) - else - (* look for Xn (which we actually call Rn) in regs_in *) - let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in - [NIA_register r | forall (r MEM regs_in) - | match r with - | (Reg name _ _ _) -> name = n_reg - | _ -> false - end] - | ("AArch64HandSail", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"AArch64HandSail\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *) - - | ("AArch64GenSail", "BranchImmediate") -> nias - | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias - | ("AArch64GenSail", "CompareAndBranch") -> NIA_successor :: nias - | ("AArch64GenSail", "TestBitAndBranch") -> NIA_successor :: nias - - (* AArch64 calculated address branch *) - | ("AArch64GenSail", "branch_unconditional_register") -> - (* do some parsing of the ast fields to figure out which register holds - the branching address i.e. find n in "BR ". The ast constructor - from armV8.sail: (reg_index,BranchType) BranchRegister; *) - let n_integer = - match instruction_fields with - | [(_, _, n); _] -> integer_of_bit_list n - | _ -> fail - end - in - let () = ensure (0 <= n_integer && n_integer <= 31) - "expected register number from 0 to 31" - in - if n_integer = 31 then - nias (* BR XZR *) - else - (* look for Xn (which we actually call Rn) in regs_in *) - let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in - [NIA_register r | forall (r MEM regs_in) - | match r with - | (Reg name _ _ _) -> name = n_reg - | _ -> false - end] - | ("AArch64GenSail", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"AArch64GenSail\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - (** end of hacky *) - - | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias - | ("AArch64LitmusSail", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"AArch64LitmusSail\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - - | ("MIPS_ism", "B") -> fail - | ("MIPS_ism", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"MIPS_ism\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - | ("RISCV_ism", "JAL") -> nias - | ("RISCV_ism", "JALR") -> - let rs1_integer = - match instruction_fields with - | [_; (_, _, rs1); _] -> integer_of_bit_list rs1 - | _ -> fail - end - in - let () = ensure (0 <= rs1_integer && rs1_integer <= 31) - "expected register number from 0 to 31" - in - if rs1_integer = 0 then nias - else - let rs1_reg = "x" ^ (String_extra.stringFromInteger rs1_integer) in - [NIA_register r | forall (r MEM regs_in) - | match r with - | (Reg name _ _ _) -> name = rs1_reg - | _ -> false - end] - | ("RISCV_ism", "BTYPE") -> NIA_successor :: nias - | ("RISCV_ism", s) -> - let () = ensure (not unknown_nia_address) - ("unexpected unknown/undefined address in nia_values 4 (\"RISCV_ism\", \"" ^ s ^ "\")") in - [ NIA_successor ] - - | (s1, s2) -> failwith ("unexpected (thread_ism, instruction_name): (" ^ s1 ^ ", " ^ s2 ^ ")") - end - - let interp_instruction_analysis top_level (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) - instruction nia_reg ism environment = + instruction + nia_reg + (nias_function : (list (maybe address) -> list reg_name -> list nia)) + ism environment = let es = interp_exhaustive environment in @@ -1405,7 +1238,7 @@ let interp_instruction_analysis let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in - let nias = nias_of_instruction top_level ism nia_address regs_in instruction in + let nias = nias_function nia_address regs_in in let dia = DIA_none in (* FIX THIS! *) @@ -1496,12 +1329,13 @@ let interp_compare_analyses interp_exhaustive (instruction : Interp_ast.value) nia_reg + (nias_function : (list (maybe address) -> list reg_name -> list nia)) ism environment analysis_function reg_info = let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) = - interp_instruction_analysis context interp_exhaustive instruction nia_reg ism + interp_instruction_analysis context interp_exhaustive instruction nia_reg nias_function ism environment in let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) = (Set.fromList regs_in1, -- cgit v1.2.3 From 97b808681f951a962cdb3c087d79aee5556a7089 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 9 Oct 2017 16:14:08 +0100 Subject: add translation of IK_mem_rmw interp_inter_imp. TODO: could we get rid of this and use shallow embedding conversion? --- src/lem_interp/interp_inter_imp.lem | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index c0d2ea4a..1c993ba0 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -571,6 +571,21 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> NIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return nia of expected type" end in + let readk_to_readk = function + | "Read_plain" -> Read_plain + | "Read_reserve" -> Read_reserve + | "Read_acquire" -> Read_acquire + | "Read_exclusive" -> Read_exclusive + | "Read_exclusive_acquire" -> Read_exclusive_acquire + | "Read_stream" -> Read_stream + | r -> failwith ("unknown read kind: " ^ r) end in + let writek_to_writek = function + | "Write_plain" -> Write_plain + | "Write_conditional" -> Write_conditional + | "Write_release" -> Write_release + | "Write_exclusive" -> Write_exclusive + | "Write_exclusive_release" -> Write_exclusive_release + | w -> failwith ("unknown write kind: " ^ w) end in let ik_to_ik = function | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) -> @@ -591,23 +606,14 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis end) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _ (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) -> - IK_mem_read (match r with - | "Read_plain" -> Read_plain - | "Read_reserve" -> Read_reserve - | "Read_acquire" -> Read_acquire - | "Read_exclusive" -> Read_exclusive - | "Read_exclusive_acquire" -> Read_exclusive_acquire - | "Read_stream" -> Read_stream - end) + IK_mem_read(readk_to_readk r) | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _ (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) -> - IK_mem_write (match w with - | "Write_plain" -> Write_plain - | "Write_conditional" -> Write_conditional - | "Write_release" -> Write_release - | "Write_exclusive" -> Write_exclusive - | "Write_exclusive_release" -> Write_exclusive_release - end) + IK_mem_write(writek_to_writek w) + | Interp_ast.V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ + (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; + (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> + IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> IK_cond_branch | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> -- cgit v1.2.3 From 93dfd61038583eac852e5e3ea66c46817a610bbe Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Mon, 9 Oct 2017 16:38:03 +0100 Subject: add translations for missing read/write kinds. --- src/lem_interp/interp_inter_imp.lem | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src') diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 1c993ba0..8199f271 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -578,6 +578,12 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Read_exclusive" -> Read_exclusive | "Read_exclusive_acquire" -> Read_exclusive_acquire | "Read_stream" -> Read_stream + | "Read_RISCV_acquire" -> Read_RISCV_acquire + | "Read_RISCV_strong_acquire" -> Read_RISCV_strong_acquire + | "Read_RISCV_reserved" -> Read_RISCV_reserved + | "Read_RISCV_reserved_acquire" -> Read_RISCV_reserved_acquire + | "Read_RISCV_reserved_strong_acquire" -> Read_RISCV_reserved_strong_acquire + | "Read_X86_locked" -> Read_X86_locked | r -> failwith ("unknown read kind: " ^ r) end in let writek_to_writek = function | "Write_plain" -> Write_plain @@ -585,6 +591,12 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | "Write_release" -> Write_release | "Write_exclusive" -> Write_exclusive | "Write_exclusive_release" -> Write_exclusive_release + | "Write_RISCV_release" -> Write_RISCV_release + | "Write_RISCV_strong_release" -> Write_RISCV_strong_release + | "Write_RISCV_conditional" -> Write_RISCV_conditional + | "Write_RISCV_conditional_release" -> Write_RISCV_conditional_release + | "Write_RISCV_conditional_strong_release" -> Write_RISCV_conditional_strong_release + | "Write_X86_locked" -> Write_X86_locked | w -> failwith ("unknown write kind: " ^ w) end in let ik_to_ik = function | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _ -- cgit v1.2.3 From 29182cd14e228529b3e26ef901e927bde8d27345 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 24 Oct 2017 15:44:10 +0100 Subject: fix default cap value on cheri128 following previous changes -- E stored in registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length. --- src/gen_lib/sail_values.ml | 27 +++++++++++++++++---------- src/lem_interp/run_with_elf_cheri128.ml | 2 +- 2 files changed, 18 insertions(+), 11 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index d160e84a..213acea1 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -889,18 +889,25 @@ let shift_op_vec_int op (l,r) = let len = Array.length array in (match op with | "<<" -> - let left = Array.sub array r (len - r) in - let right = Array.make r Vzero in - let result = Array.append left right in - Vvector(result, start, ord) + if (r <= len) then + let left = Array.sub array r (len - r) in + let right = Array.make r Vzero in + let result = Array.append left right in + Vvector(result, start, ord) + else + Vvector(Array.make len Vzero, start, ord) | ">>" -> - let left = Array.make r Vzero in - let right = Array.sub array 0 (len - r) in - let result = Array.append left right in - Vvector(result, start, ord) + if (r <= len) then + let left = Array.make r Vzero in + let right = Array.sub array 0 (len - r) in + let result = Array.append left right in + Vvector(result, start, ord) + else + Vvector(Array.make len Vzero, start, ord) | "<<<" -> - let left = Array.sub array r (len - r) in - let right = Array.sub array 0 r in + let rmod = r mod len in + let left = Array.sub array rmod (len - rmod) in + let right = Array.sub array 0 rmod in let result = Array.append left right in Vvector(result, start, ord) | _ -> assert false) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 3ad507bc..f4f319ea 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -665,7 +665,7 @@ let cheri_register_data_all = mips_register_data_all @ [ 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 "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *) + let initial_cap_val_int = Nat_big_num.of_string "0x1fffe6000000100000000000000000000" in (* hex((0x10000 << 64) + (48 << 105) + (0x7fff << 113) + (1 << 128)) T=0x10000 E=48 perms=0x7fff tag=1 *) 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")); -- cgit v1.2.3 From a35692d69681683c2bffe7c824ad230b88679ed9 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Tue, 31 Oct 2017 16:09:46 +0000 Subject: cheri: throw an exception if there is an attempt to access C26/IDC in the delay slot of a ccall selector 1 call. --- src/lem_interp/run_with_elf_cheri.ml | 2 ++ src/lem_interp/run_with_elf_cheri128.ml | 2 ++ 2 files changed, 4 insertions(+) (limited to 'src') diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index b879f702..b50cb01d 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -493,6 +493,7 @@ let mips_register_data_all = [ ("PC", (D_decreasing, 64, 63)); ("branchPending", (D_decreasing, 1, 0)); ("inBranchDelay", (D_decreasing, 1, 0)); + ("inCCallDelay", (D_decreasing, 1, 0)); ("delayedPC", (D_decreasing, 64, 63)); ("nextPC", (D_decreasing, 64, 63)); (* General purpose registers *) @@ -1072,6 +1073,7 @@ let set_next_instruction_address model = 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; + reg := Reg.add "inCCallDelay" (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 *) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index f4f319ea..148b29ae 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -493,6 +493,7 @@ let mips_register_data_all = [ ("PC", (D_decreasing, 64, 63)); ("branchPending", (D_decreasing, 1, 0)); ("inBranchDelay", (D_decreasing, 1, 0)); + ("inCCallDelay", (D_decreasing, 1, 0)); ("delayedPC", (D_decreasing, 64, 63)); ("nextPC", (D_decreasing, 64, 63)); (* General purpose registers *) @@ -1072,6 +1073,7 @@ let set_next_instruction_address model = 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; + reg := Reg.add "inCCallDelay" (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 *) -- cgit v1.2.3 From 8e5d44d17c71cf946e65e15de8df42de2af4c652 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Wed, 1 Nov 2017 14:17:08 +0000 Subject: added RISC-V "fence r,r" --- src/gen_lib/deep_shallow_convert.lem | 10 ++++++---- src/lem_interp/sail_impl_base.lem | 11 +++++++---- 2 files changed, 13 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 5a0dd99e..76880dbd 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -471,10 +471,11 @@ let barrier_kindToInterpValue = function | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ()) | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ()) - | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ()) - | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ()) - | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ()) - | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ()) + | Barrier_RISCV_r_r -> V_ctor (Id_aux (Id "Barrier_RISCV_r_r") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ()) + | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ()) + | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ()) + | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ()) + | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 19) (toInterpValue ()) end let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync @@ -492,6 +493,7 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw + | V_ctor (Id_aux (Id "Barrier_RISCV_r_r") _) _ _ v -> Barrier_RISCV_r_r | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 4f07f574..c0ec8548 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -501,6 +501,7 @@ type barrier_kind = (* RISC-V barriers *) | Barrier_RISCV_rw_rw | Barrier_RISCV_r_rw + | Barrier_RISCV_r_r | Barrier_RISCV_rw_w | Barrier_RISCV_w_w | Barrier_RISCV_i @@ -525,6 +526,7 @@ instance (Show barrier_kind) | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" + | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" | Barrier_RISCV_i -> "Barrier_RISCV_i" @@ -621,10 +623,11 @@ instance (EnumerationType barrier_kind) | Barrier_MIPS_SYNC -> 12 | Barrier_RISCV_rw_rw -> 13 | Barrier_RISCV_r_rw -> 14 - | Barrier_RISCV_rw_w -> 15 - | Barrier_RISCV_w_w -> 16 - | Barrier_RISCV_i -> 17 - | Barrier_x86_MFENCE -> 18 + | Barrier_RISCV_r_r -> 15 + | Barrier_RISCV_rw_w -> 16 + | Barrier_RISCV_w_w -> 17 + | Barrier_RISCV_i -> 18 + | Barrier_x86_MFENCE -> 19 end end -- cgit v1.2.3 From d91841f80740b210c673d3138f77b9d4d5684102 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 2 Nov 2017 14:06:24 +0000 Subject: reset inCCallDelay in code that is not dead. --- src/lem_interp/run_with_elf_cheri.ml | 1 + src/lem_interp/run_with_elf_cheri128.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'src') diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index b50cb01d..8f7d5505 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1285,6 +1285,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = 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; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 148b29ae..311d6f69 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1285,6 +1285,7 @@ let rec fde_loop count context model mode track_dependencies addr_trans = 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; + reg := Reg.add "inCCallDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg; | Some 1 -> reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg; reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg; -- cgit v1.2.3 From 5d59b0c1a477c2d9e1abcfc6fb1b51dff32bd9b5 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 2 Nov 2017 14:47:30 +0000 Subject: remove a lot of dead code form run_with_elf_cheri* --- src/lem_interp/run_with_elf_cheri.ml | 568 ------------------------------- src/lem_interp/run_with_elf_cheri128.ml | 570 -------------------------------- 2 files changed, 1138 deletions(-) (limited to 'src') diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 8f7d5505..7750c16c 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -124,369 +124,6 @@ let register_state_zero register_data rbn : register_value = 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*) @@ -749,50 +386,6 @@ let initial_system_state_of_elf_file name = 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 @@ -889,50 +482,6 @@ let initial_system_state_of_elf_file name = 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 -> @@ -1022,69 +571,10 @@ let stop_condition_met model instr = 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; - reg := Reg.add "inCCallDelay" (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 _ = @@ -1194,68 +684,10 @@ let rec write_events = function | _ -> 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)) diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 311d6f69..6dca80f4 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -124,369 +124,6 @@ let register_state_zero register_data rbn : register_value = 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*) @@ -749,50 +386,6 @@ let initial_system_state_of_elf_file name = 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 @@ -888,52 +481,6 @@ let initial_system_state_of_elf_file name = 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 @@ -1022,69 +569,10 @@ let stop_condition_met model instr = 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; - reg := Reg.add "inCCallDelay" (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 _ = @@ -1194,68 +682,10 @@ let rec write_events = function | _ -> 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)) -- cgit v1.2.3