diff options
| -rw-r--r-- | src/gen_lib/prompt.lem | 34 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.lem | 13 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 27 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 58 |
4 files changed, 99 insertions, 33 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index a9aa3218..e1e8658e 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -88,20 +88,18 @@ type outcome 'e 'a = * on when mode.track_values, integer is size to read, followed by registers that were used in * computing that size *) (* address_lifted should go away: doesn't make sense to allow for undefined bits in addresses *) - | Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) * - (memory_value -> outcome 'e 'a) + | Read_mem of read_kind * address_lifted * nat * (memory_value -> outcome 'e 'a) (* Request to write memory, first value and dependent registers is location, second is the value * to write *) - | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * - maybe (list reg_name) * (bool -> outcome 'e 'a) + | Write_mem of write_kind * address_lifted * nat * memory_value * (bool -> outcome 'e 'a) (* Tell the system a write is imminent, at address lifted tanted by register list, of size nat *) - | Write_ea of write_kind * address_lifted * nat * maybe (list reg_name) * outcome 'e 'a + | Write_ea of write_kind * address_lifted * nat * outcome 'e 'a (* Request to write memory at last signaled address. Memory value should be 8* the size given in * ea signal *) - | Write_memv of memory_value * maybe (list reg_name) * (bool -> outcome 'e 'a) + | Write_memv of memory_value * (bool -> outcome 'e 'a) (* Request a memory barrier *) (* outcome 'a used to be (unit -> outcome 'a), but since the code is purely functional we don't @@ -136,16 +134,16 @@ let return a = Done a val (>>=) : forall 'e 'a 'b. M 'e 'a -> ('a -> M 'e 'b) -> M 'e 'b let rec (>>=) m f = match m with | Done a -> f a - | Read_mem rk addr sz rs k -> Read_mem rk addr sz rs (fun v -> (k v) >>= f) - | Write_mem wk addr sz rs v rs2 k -> Write_mem wk addr sz rs v rs2 (fun b -> (k b) >>= f) - | Write_ea wk addr sz rs k -> Write_ea wk addr sz rs (k >>= f) - | Write_memv v rs k -> Write_memv v rs (fun b -> (k b) >>= f) - | Barrier bk k -> Barrier bk (k >>= f) - | Footprint k -> Footprint (k >>= f) - | Read_reg reg k -> Read_reg reg (fun v -> (k v) >>= f) - | Write_reg reg v k -> Write_reg reg v (k >>= f) - | Nondet_choice () -> Nondet_choice () - | Escape e -> Escape e + | Read_mem rk addr sz k -> Read_mem rk addr sz (fun v -> (k v) >>= f) + | Write_mem wk addr sz v k -> Write_mem wk addr sz v (fun b -> (k b) >>= f) + | Write_ea wk addr sz k -> Write_ea wk addr sz (k >>= f) + | Write_memv v k -> Write_memv v (fun b -> (k b) >>= f) + | Barrier bk k -> Barrier bk (k >>= f) + | Footprint k -> Footprint (k >>= f) + | Read_reg reg k -> Read_reg reg (fun v -> (k v) >>= f) + | Write_reg reg v k -> Write_reg reg v (k >>= f) + | Nondet_choice () -> Nondet_choice () + | Escape e -> Escape e end val (>>) : forall 'e 'b. M 'e unit -> M 'e 'b -> M 'e 'b @@ -181,12 +179,12 @@ let registerValueFromBitv (Vector bits start is_inc) reg = val read_memory : forall 'e. read_kind -> integer -> integer -> M 'e (vector bit) let read_memory rk addr sz = let sz = natFromInteger sz in - Read_mem rk addr sz Nothing (compose Done bitvFromBytes) + Read_mem rk addr sz (compose Done bitvFromBytes) val write_memory : forall 'e. write_kind -> integer -> integer -> vector bit -> M 'e bool let write_memory wk addr sz (Vector v _ _) = let sz = natFromInteger sz in - Write_mem wk addr sz Nothing (byte_chunks sz v) Nothing Done + Write_mem wk addr sz (byte_chunks sz v) Done val read_reg_range : forall 'e. register -> (integer * integer) -> M 'e (vector bit) let read_reg_range reg (i,j) = diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 6de5b853..46c3a10c 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -454,20 +454,21 @@ let lteq_range_vec = compare_op_range_vec (<=) true let gteq_range_vec = compare_op_range_vec (>=) true let eq (l,r) = bool_to_bit (l = r) +let eq_range (l,r) = bool_to_bit (l = r) +let eq_vec (l,r) = bool_to_bit (l = r) +let eq_bit (l,r) = bool_to_bit (l = r) let eq_vec_range (l,r) = eq (to_num false l,r) let eq_range_vec (l,r) = eq (l, to_num false r) let eq_vec_vec (l,r) = eq (to_num true l, to_num true r) -(* -let neq (l,r) = bitwise_not_bit (eq (l,r)) *) + +let neq (l,r) = bitwise_not_bit (eq (l,r)) +let neq_bit (l,r) = bitwise_not_bit (eq_bit (l,r)) +let neq_range (l,r) = bitwise_not_bit (eq_range (l,r)) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r)) let neq_vec_range (l,r) = bitwise_not_bit (eq_vec_range (l,r)) let neq_range_vec (l,r) = bitwise_not_bit (eq_range_vec (l,r)) -(* temporarily *) -val neq : forall 'a 'b. 'a * 'b -> bit -let neq _ = O - val make_indexed_vector : forall 'a. list (integer * 'a) -> 'a -> integer -> integer -> vector 'a let make_indexed_vector entries default start length = let length = natFromInteger length in diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 9a06b0ba..483968ca 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -476,6 +476,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis Interp.V_list regs2; Interp.V_list regs3; Interp.V_list nias; + dia; ik] -> let reg_to_reg_name v = match v with | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) -> @@ -500,7 +501,24 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis Reg_field n start direction f (extern_slice direction start span) | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end in - let get_nia v = address_of_memory_value end_flag (fst (extern_mem_value mode v)) in + let get_addr v = match address_of_memory_value end_flag (fst (extern_mem_value mode v)) with + | Just addr -> addr + | Nothing -> failwith "get_nia encountered invalid address" end in + let dia_to_dia = function + | Interp.V_ctor (Id_aux (Id "DIA_none") _) _ _ _ -> DIA_none + | Interp.V_ctor (Id_aux (Id "DIA_concrete") _) _ _ address -> + DIA_concrete_address (get_addr address) + | Interp.V_ctor (Id_aux (Id "DIA_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) + | _ -> failwith "Register footprint analysis did not return dia of expected type" end in + let nia_to_nia = function + | Interp.V_ctor (Id_aux (Id "NIA_successor") _) _ _ _-> NIA_successor + | Interp.V_ctor (Id_aux (Id "NIA_concrete_address") _) _ _ address -> + NIA_concrete_address (get_addr address) + | Interp.V_ctor (Id_aux (Id "NIA_LR") _) _ _ _ -> NIA_LR + | Interp.V_ctor (Id_aux (Id "NIA_CTR") _) _ _ _ -> NIA_CTR + | Interp.V_ctor (Id_aux (Id "NIA_register") _) _ _ reg -> + NIA_register (reg_to_reg_name reg) + | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let ik_to_ik = function | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _ (Interp.V_ctor (Id_aux (Id b) _) _ _ _) -> @@ -544,13 +562,14 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" end in - let (regs1,regs2,regs3,nias,ik) = + let (regs1,regs2,regs3,nias,dia,ik) = (List.map reg_to_reg_name regs1, List.map reg_to_reg_name regs2, List.map reg_to_reg_name regs3, - List.map get_nia nias, + List.map nia_to_nia nias, + dia_to_dia dia, ik_to_ik ik) in - ((regs1,regs2,regs3,nias,ik), events) + ((regs1,regs2,regs3,nias,dia,ik), events) | _ -> Assert_extra.failwith "Analysis did not return a four-tuple of lists" end) | Ivh_value_after_exn _ -> Assert_extra.failwith "Instruction analysis failed" | Ivh_error err -> match err with diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index cc0bef06..2e649ec1 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -413,7 +413,6 @@ instance (Show read_kind) end end - type write_kind = (* common writes *) Write_plain @@ -1179,10 +1178,6 @@ val translate_address : context -> end_flag -> string -> maybe (list (reg_name * register_value)) -> address -> maybe address * maybe (list event) -val instruction_analysis : - context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) - -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list address) - val byte_list_of_memory_value : end_flag -> memory_value -> maybe (list byte) let byte_list_of_memory_value endian mv = let mv = if endian = E_big_endian then mv else List.reverse mv in @@ -1405,3 +1400,56 @@ instance (Show byte_lifted) let show = stringFromByte_lifted end +(* possible next instruction address options *) +type nia = + | NIA_successor + | NIA_concrete_address of address + | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *) + | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *) + | NIA_register of reg_name (* the address will be in a register, + corresponds to AArch64 BLR, BR, RET + instructions *) + +let niaCompare n1 n2 = match (n1,n2) with + | (NIA_successor,NIA_successor) -> EQ + | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 + | (NIA_LR,NIA_LR) -> EQ + | (NIA_CTR,NIA_CTR) -> EQ + | (NIA_register r1,NIA_register r2) -> compare r1 r2 + + | (NIA_successor,_) -> LT + | (NIA_concrete_address _,_) -> LT + | (NIA_LR,_) -> LT + | (NIA_CTR,_) -> LT + | (_,_) -> GT + end + +instance (Ord nia) + let compare = niaCompare + let (<) n1 n2 = (niaCompare n1 n2) = LT + let (<=) n1 n2 = (niaCompare n1 n2) <> GT + let (>) n1 n2 = (niaCompare n1 n2) = GT + let (>=) n1 n2 = (niaCompare n1 n2) <> LT +end + +let stringFromNia = function + | NIA_successor -> "NIA_successor" + | NIA_concrete_address a -> "NIA_concrete_address " ^ show a + | NIA_LR -> "NIA_LR" + | NIA_CTR -> "NIA_CTR" + | NIA_register r -> "NIA_register " ^ show r +end + +instance (Show nia) + let show = stringFromNia +end + +type dia = + | DIA_none + | DIA_concrete_address of address + | DIA_register of reg_name + + +val instruction_analysis : + context -> end_flag -> string -> (string -> (nat * nat * direction * (nat * nat))) + -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind) |