diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 366 |
1 files changed, 177 insertions, 189 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index ed576d2d..88ce56e4 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -20,6 +20,9 @@ let make_interp_mode eager_eval tracking_values = let make_mode eager_eval tracking_values endian = <|internal_mode = make_interp_mode eager_eval tracking_values; endian = endian|>;; +let make_mode_exhaustive endian = + <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|>; + endian = endian |>;; let tracking_dependencies mode = mode.internal_mode.Interp.track_values let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;; let make_default_mode _ = <|internal_mode = make_interp_mode false false; endian = E_big_endian|>;; @@ -228,57 +231,6 @@ let rec slice_reg_value v start stop = (if inc then (stop - v.rv_start) else (v.rv_start - stop)) v.rv_bits); rv_start = (if inc then start else ((stop - start) + 1)) |> -(* -let append_value left right = - match (left,right) with - | (Bitvector bools1 inc fst, Bitvector bools2 _ _) -> Bitvector (bools1++bools2) inc fst - | (Bytevector bytes1, Bytevector bytes2) -> Bytevector (bytes1++bytes2) - | ((Bitvector _ _ _ as bit),(Bytevector _ as byte)) -> - (match (intern_value bit,intern_value byte) with - | (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> - (fst (extern_value (make_mode true false) false Nothing (Interp.V_vector a b (bits1++bits2)))) - | _ -> Unknown end) - | ((Bytevector _ as byte),(Bitvector _ _ _ as bit)) -> - (match (intern_value byte,intern_value bit) with - | (Interp.V_vector a b bits1,Interp.V_vector _ _ bits2) -> - (fst (extern_value (make_mode true false) true Nothing (Interp.V_vector a b (bits1++bits2)))) - | _ -> Unknown end) - | _ -> Unknown -end - -let add_to_address value num = - match value with - | Unknown -> Unknown - | Bitvector _ _ _ -> - fst(extern_value (make_mode true false) false Nothing - (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 - (Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)]))) - | Bytevector _ -> - fst(extern_value (make_mode true false) true Nothing - (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1 - (Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)]))) -end - - -let coerce_Bytevector_of_Bitvector (v: value) : value = - match v with - | Bitvector bs b i -> Bytevector (to_bytes bs) - | _ -> Assert_extra.failwith "coerce_Bytevector_of_Bitvector given non-Bitvector" - end - -let coerce_Bitvector_of_Bytevector (v: value) : value = - match v with - | Bytevector ws -> Bitvector - (List.concatMap - (fun w -> - List.reverse - (boolListFrombitSeq 8 (bitSeqFromNat w))) - ws) - true - 0 - | _ -> Assert_extra.failwith "coerce_Bitvector_of_Bitvector given non-Bytevector" - end -*) let initial_instruction_state top_level main args = let e_args = match args with @@ -287,7 +239,7 @@ let initial_instruction_state top_level main args = | args -> List.map fst (List.map (Interp.to_exp (make_interp_mode true false) Interp.eenv) (List.map intern_reg_value args)) end in Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) - top_level Interp.eenv Interp.emem Interp.Top + top_level Interp.eenv (Interp.emem "istate top level") Interp.Top let rec interp_to_value_helper arg err_str instr direction thunk = @@ -375,7 +327,7 @@ let decode_to_istate top_level value = mode (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) - top_env Interp.eenv Interp.emem Interp.Top) Nothing) in + top_env Interp.eenv (Interp.emem "decode top level") Interp.Top) Nothing) in match (instr_decoded,error) with | (Just instr, _) -> let instr_external = match instr with @@ -400,14 +352,14 @@ let decode_to_istate top_level value = (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) - top_env Interp.eenv Interp.emem Interp.Top) Nothing) in + top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in match (instr_decoded,error) with | (Just instr,_) -> (*let (arg,_) = Interp.to_exp mode Interp.eenv instr in*) Instr instr_external (IState (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) - top_env Interp.eenv Interp.emem Interp.Top) + top_env Interp.eenv (Interp.emem "execute") Interp.Top) top_level) | (Nothing, Just err) -> Decode_error err end @@ -444,120 +396,125 @@ let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instr [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms)) (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))]) (Interp_ast.Unknown,Nothing)) - top_env Interp.eenv Interp.emem Interp.Top) + top_env Interp.eenv (Interp.emem "execute") Interp.Top) top_level) let rec interp_to_outcome mode context thunk = let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in match thunk () with - | (Interp.Value _,lm,le) -> Done - | (Interp.Error l msg,lm,le) -> Error msg + | (Interp.Value _,lm,le) -> (Done,lm) + | (Interp.Error l msg,lm,le) -> (Error msg,lm) | (Interp.Action a next_state,lm,le) -> - match a with - | Interp.Read_reg reg_form slice -> - Read_reg (extern_reg reg_form slice) - (fun v -> - let v = (intern_reg_value v) in - let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in - IState (Interp.add_answer_to_stack next_state v) context) - | Interp.Write_reg reg_form slice value -> - let reg_name = extern_reg reg_form slice in - Write_reg reg_name (extern_reg_value reg_name value) (IState next_state context) - | Interp.Read_mem (Id_aux (Id i) _) value slice -> - match List.lookup i mem_reads with - | (Just (MR read_k f)) -> - let (location, length, tracking) = (f mode value) in - if (List.length location) = 8 - then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with - | Just bs -> Just (integer_of_byte_list bs) - | _ -> Nothing end in - Read_mem read_k (Address_lifted location address_int) length tracking - (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value mode direction v)) context) - else Error ("Memory address on read is not 64 bits") - | _ -> Error ("Memory " ^ i ^ " function with read kind not found") - end - | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> - match List.lookup i mem_writes with - | (Just (MW write_k f return)) -> - let (location, length, tracking) = (f mode loc_val) in - let (value, v_tracking) = (extern_mem_value mode write_val) in - if (List.length location) = 8 - then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with - | Just bs -> Just (integer_of_byte_list bs) - | _ -> Nothing end in - Write_mem write_k (Address_lifted location address_int) - length tracking value v_tracking - (fun b -> - match return with - | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) - | Just return_bool -> return_bool (IState next_state context) b end) - else Error "Memory address on write is not 64 bits" - | _ -> Error ("Memory " ^ i ^ " function with write kind not found") - end - | Interp.Write_ea (Id_aux (Id i) _) loc_val -> - match List.lookup i mem_write_eas with - | (Just (MEA write_k f)) -> - let (location, length, tracking) = (f mode loc_val) in - if (List.length location) = 8 - then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with - | Just bs -> Just (integer_of_byte_list bs) - | _ -> Nothing end in - Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context) - else Error "Memory address for write is not 64 bits" - | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end - | Interp.Write_memv (Id_aux (Id i) _) write_val -> - match List.lookup i mem_write_vals with - | (Just (MV return)) -> - let (value, v_tracking) = - match (Interp.detaint write_val) with - | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v)) - | _ -> (extern_mem_value mode write_val) end in - Write_memv value v_tracking - (fun b -> - match return with - | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) - | Just return_bool -> return_bool (IState next_state context) b end) - | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end - | Interp.Barrier (Id_aux (Id i) _) lval -> - match List.lookup i barriers with - | Just barrier -> - Barrier barrier (IState next_state context) - | _ -> Error ("Barrier " ^ i ^ " function not found") end - | Interp.Footprint (Id_aux (Id i) _) lval -> - Footprint (IState next_state context) - | Interp.Nondet exps tag -> - match tag with - | Tag_unknown -> - let possible_states = List.map (Interp.set_in_context next_state) exps in - Analysis_non_det (List.map (fun i -> IState i context) possible_states) (IState next_state context) - | _ -> - let nondet_states = List.map (Interp.set_in_context next_state) exps in - Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end - | Interp.Call_extern i value -> - match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with - | Nothing -> Error ("External function not available " ^ i) - | Just f -> - if (mode.internal_mode.Interp.eager_eval) - then interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value))) - else let new_v = f value in - Internal (Just i) + (match a with + | Interp.Read_reg reg_form slice -> + (Read_reg (extern_reg reg_form slice) + (fun v -> + let v = (intern_reg_value v) in + let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in + IState (Interp.add_answer_to_stack next_state v) context), lm) + | Interp.Write_reg reg_form slice value -> + let reg_name = extern_reg reg_form slice in + (Write_reg reg_name (extern_reg_value reg_name value) (IState next_state context),lm) + | Interp.Read_mem (Id_aux (Id i) _) value slice -> + (match List.lookup i mem_reads with + | (Just (MR read_k f)) -> + let (location, length, tracking) = (f mode value) in + if (List.length location) = 8 + then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in + Read_mem read_k (Address_lifted location address_int) length tracking + (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value mode direction v)) context) + else Error ("Memory address on read is not 64 bits") + | _ -> Error ("Memory " ^ i ^ " function with read kind not found") + end , lm) + | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> + (match List.lookup i mem_writes with + | (Just (MW write_k f return)) -> + let (location, length, tracking) = (f mode loc_val) in + let (value, v_tracking) = (extern_mem_value mode write_val) in + if (List.length location) = 8 + then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in + Write_mem write_k (Address_lifted location address_int) + length tracking value v_tracking + (fun b -> + match return with + | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) + | Just return_bool -> return_bool (IState next_state context) b end) + else Error "Memory address on write is not 64 bits" + | _ -> Error ("Memory " ^ i ^ " function with write kind not found") + end , lm) + | Interp.Write_ea (Id_aux (Id i) _) loc_val -> + (match List.lookup i mem_write_eas with + | (Just (MEA write_k f)) -> + let (location, length, tracking) = (f mode loc_val) in + if (List.length location) = 8 + then let address_int = match (maybe_all (List.map byte_of_byte_lifted location)) with + | Just bs -> Just (integer_of_byte_list bs) + | _ -> Nothing end in + Write_ea write_k (Address_lifted location address_int) length tracking (IState next_state context) + else Error "Memory address for write is not 64 bits" + | _ -> Error ("Memory " ^ i ^ " function to signal impending write, not found") end, lm) + | Interp.Write_memv (Id_aux (Id i) _) write_val -> + (match List.lookup i mem_write_vals with + | (Just (MV return)) -> + let (value, v_tracking) = + match (Interp.detaint write_val) with + | Interp.V_tuple[_;v] -> (extern_mem_value mode (Interp.retaint write_val v)) + | _ -> (extern_mem_value mode write_val) end in + Write_memv value v_tracking + (fun b -> + match return with + | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) + | Just return_bool -> return_bool (IState next_state context) b end) + | _ -> Error ("Memory " ^ i ^ " function with write value kind not found") end, lm) + | Interp.Barrier (Id_aux (Id i) _) lval -> + (match List.lookup i barriers with + | Just barrier -> + Barrier barrier (IState next_state context) + | _ -> Error ("Barrier " ^ i ^ " function not found") end, lm) + | Interp.Footprint (Id_aux (Id i) _) lval -> + (Footprint (IState next_state context), lm) + | Interp.Nondet exps tag -> + (match tag with + | Tag_unknown _ -> + let possible_states = List.map (Interp.set_in_context next_state) exps in + let cleared_possibles = List.map Interp.clear_stack_state possible_states in + Analysis_non_det (List.map (fun i -> IState i context) cleared_possibles) (IState next_state context) + | _ -> + let nondet_states = List.map (Interp.set_in_context next_state) exps in + Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end, lm) + | Interp.Call_extern i value -> + (match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with + | Nothing -> (Error ("External function not available " ^ i), lm) + | Just f -> + if (mode.internal_mode.Interp.eager_eval) + then interp_to_outcome mode context + (fun _ -> Interp.resume mode.internal_mode next_state (Just (f value))) + else let new_v = f value in + (Internal (Just i) (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v))) - (IState (Interp.add_answer_to_stack next_state new_v) context) - end - | Interp.Step l Nothing Nothing -> Internal Nothing Nothing (IState next_state context) - | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing (IState next_state context) - | Interp.Step l (Just name) (Just value) -> - Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context) - | Interp.Exit e -> - Escape (match e with - | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing - | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context) - end - end + (IState (Interp.add_answer_to_stack next_state new_v) context), lm) + end) + | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm) + | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm) + | Interp.Step l (Just name) (Just value) -> + (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm) + | Interp.Exit e -> + (Escape (match e with + | E_aux (E_lit (L_aux L_unit _)) _ -> Nothing + | _ -> Just (IState (Interp.set_in_context next_state e) context) end) (IState next_state context), + (snd (Interp.get_stack_state next_state))) + end ) + end let interp mode (IState interp_state context) = - interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) + match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with + | (o,_) -> o +end (*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*) (*TODO immediate: this will be impacted by need to change slicing *) @@ -592,6 +549,7 @@ let reg_size = function | Reg_f_slice i _ _ f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1 end +(*ie_loop returns a tuple of event list, and a tuple ofinternal interpreter memory, bool to indicate normal or exceptional termination*) let rec ie_loop mode register_values (IState interp_state context) = let (Context _ direction externs reads writes write_eas write_vals barriers) = context in let unknown_reg size = @@ -600,43 +558,73 @@ let rec ie_loop mode register_values (IState interp_state context) = rv_start_internal = (if direction = D_increasing then 0 else (size-1)); rv_dir = direction |> in let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in - match interp mode (IState interp_state context) with - | Done -> [] - | Error msg -> [E_error msg] - | Escape Nothing i_state -> [E_escape] + match interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode interp_state Nothing) with + | (Done,lm) -> ([],(lm,true)) + | (Error msg,lm) -> ([E_error msg],(lm,false)) + | (Escape Nothing i_state,lm) -> ([E_escape],(lm,false)) (*Do we want to record anything about the escape expression, which may be a function call*) - | Escape _ i_state -> [E_escape] - | Read_reg reg i_state_fun -> - let v = match register_values with + | (Escape _ i_state,lm) -> ([E_escape],(lm,false)) + | (Read_reg reg i_state_fun,_) -> + let v = (match register_values with | Nothing -> unknown_reg (reg_size reg) | Just(registers) -> match find_reg_name reg registers with | Nothing -> unknown_reg (reg_size reg) - | Just v -> v end end in - (E_read_reg reg)::(ie_loop mode register_values (i_state_fun v)) - | Write_reg reg value i_state-> - (E_write_reg reg value)::(ie_loop mode register_values i_state) - | Read_mem read_k loc length tracking i_state_fun -> - (E_read_mem read_k loc length tracking):: - (ie_loop mode register_values (i_state_fun (unknown_mem length))) - | Write_mem write_k loc length tracking value v_tracking i_state_fun -> - (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true)) - | Write_ea write_k loc length tracking i_state -> - (E_write_ea write_k loc length tracking)::(ie_loop mode register_values i_state) - | Write_memv value tracking i_state_fun -> - (E_write_memv value tracking)::(ie_loop mode register_values (i_state_fun true)) - | Barrier barrier_k i_state -> - (E_barrier barrier_k)::(ie_loop mode register_values i_state) - | Footprint i_state -> - E_footprint::(ie_loop mode register_values i_state) - | Internal _ _ next -> (ie_loop mode register_values next) - | Analysis_non_det possible_states i_state -> - (*TODO: need to merge the stores from the stacks/results somehow (so probably need to have a different loop)*) - (List.concat (List.map (ie_loop mode register_values) possible_states))++(ie_loop mode register_values i_state) + | Just v -> v end end) in + let (events,analysis_data) = ie_loop mode register_values (i_state_fun v) in + ((E_read_reg reg)::events,analysis_data) + | (Write_reg reg value i_state, _)-> + let (events,analysis_data) = ie_loop mode register_values i_state in + ((E_write_reg reg value)::events,analysis_data) + | (Read_mem read_k loc length tracking i_state_fun, _) -> + let (events,analysis_data) = ie_loop mode register_values (i_state_fun (unknown_mem length)) in + ((E_read_mem read_k loc length tracking)::events,analysis_data) + | (Write_mem write_k loc length tracking value v_tracking i_state_fun, _) -> + let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in + let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in + (*TODO: consider if lm and lm should be distinct and merged*) + ((E_write_mem write_k loc length tracking value v_tracking)::(events++events'),analysis_data) + | (Write_ea write_k loc length tracking i_state, _) -> + let (events,analysis_data) = ie_loop mode register_values i_state in + ((E_write_ea write_k loc length tracking)::events,analysis_data) + | (Write_memv value tracking i_state_fun, _) -> + let (events,analysis_data) = ie_loop mode register_values (i_state_fun true) in + let (events',analysis_data) = ie_loop mode register_values (i_state_fun false) in + (*TODO: consider if lm and lm should be merged*) + ((E_write_memv value tracking)::(events++events'),analysis_data) + | (Barrier barrier_k i_state, _) -> + let (events,analysis_data) = ie_loop mode register_values i_state in + ((E_barrier barrier_k)::events,analysis_data) + | (Footprint i_state, _) -> + let (events,analysis_data) = ie_loop mode register_values i_state in + (E_footprint::events,analysis_data) + | (Internal _ _ next, _) -> (ie_loop mode register_values next) + | (Analysis_non_det possible_istates i_state,_) -> + if possible_istates = [] + then ie_loop mode register_values i_state + else + let (possible_events,possible_states) = List.unzip(List.map (ie_loop mode register_values) possible_istates) in + let (unified_mem,update_mem) = List.foldr + (fun (lm,terminated_normally) (mem,update_mem) -> + if terminated_normally && update_mem + then (Interp.merge_lmems lm mem, true) + else if terminated_normally + then (lm, true) + else (mem, false)) + (List_extra.head possible_states) (List_extra.tail possible_states) in + let updated_i_state = + if update_mem + then match i_state with + | (IState interp_state context) -> IState (Interp.update_stack_state interp_state unified_mem) context end + else i_state in + let (events,analysis_data) = ie_loop mode register_values updated_i_state in + ((List.concat possible_events)++events, analysis_data) end ;; let interp_exhaustive register_values i_state = - let mode = make_mode true true E_big_endian in - ie_loop mode register_values i_state + let mode = make_mode_exhaustive E_big_endian in + match ie_loop mode register_values i_state with + | (events,_) -> events +end let rec rr_ie_loop mode i_state = let (IState _ (Context _ direction _ _ _ _ _ _)) = i_state in |