diff options
| -rw-r--r-- | src/lem_interp/extract.mllib | 3 | ||||
| -rw-r--r-- | src/lem_interp/instruction_extractor.lem | 8 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 90 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 29 | ||||
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 32 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 32 |
7 files changed, 64 insertions, 132 deletions
diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib index 6230c0e8..ebca3114 100644 --- a/src/lem_interp/extract.mllib +++ b/src/lem_interp/extract.mllib @@ -1,9 +1,10 @@ Interp_ast +Interp_utilities +Instruction_extractor Interp Interp_lib Interp_interface Interp_inter_imp -Instruction_extractor Pretty_interp Run_interp diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index 5474566d..e47a5252 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -1,6 +1,6 @@ open import Interp_ast +open import Interp_utilities open import Pervasives -import Interp type typ = | Bit @@ -11,7 +11,7 @@ type instruction = | Instr of string * list (string * typ) * list base_effect | Skipped -val extract_instructions : string -> string -> defs Interp.tannot -> list instruction +val extract_instructions : string -> string -> defs tannot -> list instruction let extract_parm (E_aux e (_,tannot)) = match e with @@ -54,8 +54,8 @@ let rec extract_effects instrs execute = end let extract_instructions decode_name execute_name defs = - let (Just decoder) = Interp.find_function defs (Id_aux (Id decode_name) Unknown) in - let (Just executer) = Interp.find_function defs (Id_aux (Id execute_name) Unknown) in + let (Just decoder) = find_function defs (Id_aux (Id decode_name) Unknown) in + let (Just executer) = find_function defs (Id_aux (Id execute_name) Unknown) in let instr_no_effects = extract_from_decode decoder in let instructions = extract_effects instr_no_effects executer in instructions diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 6edebc49..a436d652 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -5,14 +5,9 @@ import List_extra (* For 'nth' and 'head' where we know that they cannot fail *) open import String_extra (* for 'show' to convert nat to string) *) open import Interp_ast +open import Interp_utilities -type tannot = maybe (t * tag * list nec * effect) - -let get_exp_l (E_aux e (l,annot)) = l - -val pure : effect -let pure = Effect_aux(Effect_set []) Unknown -let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown +type tannot = Interp_utilities.tannot val intern_annot : tannot -> tannot let intern_annot annot = @@ -24,38 +19,10 @@ let intern_annot annot = let val_annot typ = Just(typ,Tag_empty,[],pure) -(* Workaround Lem's inability to scrap my (type classes) boilerplate. - * Implementing only Eq, and only for literals - hopefully this will - * be enough, but we should in principle implement ordering for everything in - * Interp_ast *) - -val lit_eq: lit -> lit -> bool -let lit_eq (L_aux left _) (L_aux right _) = - match (left, right) with - | (L_unit, L_unit) -> true - | (L_zero, L_zero) -> true - | (L_one, L_one) -> true - | (L_true, L_true) -> true - | (L_false, L_false) -> true - | (L_num n, L_num m) -> n = m - | (L_hex h, L_hex h') -> h = h' - | (L_bin b, L_bin b') -> b = b' - | (L_undef, L_undef) -> true - | (L_string s, L_string s') -> s = s' - | (_, _) -> false -end - -instance (Eq lit) - let (=) = lit_eq - let (<>) n1 n2 = not (lit_eq n1 n2) -end - (* This is different from OCaml: it will drop elements from the longest list. *) let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l') let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l') -let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end - type reg_form = | Reg of id * tannot | SubReg of id * reg_form * index_range @@ -76,12 +43,6 @@ type value = | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *) | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *) -let rec list_to_string format sep lst = match lst with - | [] -> "" - | [last] -> format last - | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest) -end - let rec string_of_value v = match v with | V_boxref nat t -> "$#" ^ (show nat) ^ "$" | V_lit (L_aux lit _) -> @@ -228,36 +189,6 @@ let rec to_aliases (Defs defs) = end end -val has_rmem_effect : list base_effect -> bool -val has_barr_effect : list base_effect -> bool -val has_wmem_effect : list base_effect -> bool -let rec has_effect which efcts = - match efcts with - | [] -> false - | (BE_aux e _)::efcts -> - match (which,e) with - | (BE_rreg,BE_rreg) -> true - | (BE_wreg,BE_wreg) -> true - | (BE_rmem,BE_rmem) -> true - | (BE_wmem,BE_wmem) -> true - | (BE_barr,BE_barr) -> true - | (BE_undef,BE_undef) -> true - | (BE_unspec,BE_unspec) -> true - | (BE_nondet,BE_nondet) -> true - | _ -> has_effect which efcts - end - end -let has_rmem_effect = has_effect BE_rmem -let has_barr_effect = has_effect BE_barr -let has_wmem_effect = has_effect BE_wmem - -let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t -let get_effects (Typ_aux t _) = - match t with - | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff - | _ -> [] - end - val to_data_constructors : defs tannot -> list (id * typ) let rec to_data_constructors (Defs defs) = match defs with @@ -760,23 +691,6 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) = annot end -val find_type_def : defs tannot -> id -> maybe (type_def tannot) -val find_function : defs tannot -> id -> maybe (list (funcl tannot)) - -let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) = - List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls - -let rec find_function (Defs defs) id = - match defs with - | [] -> Nothing - | def::defs -> - match def with - | DEF_fundef f -> match get_funcls id f with - | [] -> find_function (Defs defs) id - | funcs -> Just funcs end - | _ -> find_function (Defs defs) id - end end - (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) val match_pattern : pat tannot -> value -> bool * bool * lenv let rec match_pattern (P_aux p _) value_whole = diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 14a286cb..a69ea430 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -27,7 +27,7 @@ end let intern_value v = match v with | Bitvector bs inc fst -> Interp.V_vector fst inc (to_bits bs) - | Bytevector bys inc fst -> Interp.V_vector fst inc + | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.reverse (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))) | Unknown -> Interp.V_unknown @@ -43,11 +43,11 @@ end let extern_value mode for_mem v = match v with | Interp.V_vector fst inc bits -> if for_mem - then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing) + then (Bytevector (List.reverse (to_bytes (from_bits bits))), Nothing) else (Bitvector (from_bits bits) inc fst, Nothing) | Interp.V_track (Interp.V_vector fst inc bits) regs -> if for_mem - then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, + then (Bytevector (List.reverse (to_bytes (from_bits bits))), if (mode.Interp.track_values) then (Just (List.map (fun r -> extern_reg r Nothing) regs)) else Nothing) @@ -103,7 +103,7 @@ let rec interp_to_value_helper thunk = end | Interp.Action (Interp.Exit (E_aux e _)) _ -> match e with - | E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just Unsupported_instruction_error) + | E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error ("",[],[]))) | E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error) end | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode")) @@ -133,6 +133,7 @@ let decode_to_istate top_level value = Instr (Interp.Thunk_frame (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing)) top_level Interp.eenv Interp.emem Interp.Top) + ("",[],[]) | (Nothing, Just err) -> err end | (Nothing, Just err) -> err @@ -156,7 +157,7 @@ let rec interp_to_outcome mode thunk = match List.lookup i memory_functions with | (Just (Just read_k,_,f)) -> let (location, length, tracking) = (f mode value) in - Read_mem read_k location length tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v)) + Read_mem read_k location tracking length Nothing (fun v -> Interp.add_answer_to_stack next_state (intern_value v)) | _ -> Error ("Memory " ^ i ^ " function with read kind not found") end | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val -> @@ -164,7 +165,7 @@ let rec interp_to_outcome mode thunk = | (Just (_,Just write_k,f)) -> let (location, length, tracking) = (f mode loc_val) in let (value, val_tracking) = (extern_value mode true write_val) in - Write_mem write_k location length tracking value val_tracking (fun b -> next_state) + Write_mem write_k location tracking length Nothing value val_tracking (fun b -> next_state) | _ -> Error ("Memory " ^ i ^ " function with write kind not found") end | Interp.Barrier (Id_aux (Id i) _) lval -> @@ -200,10 +201,10 @@ let rec ie_loop mode i_state = (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown)) | Write_reg reg value i_state-> (E_write_reg reg value)::(ie_loop mode i_state) - | Read_mem read_k loc length tracking i_state_fun -> - (E_read_mem read_k loc length tracking)::(ie_loop mode (i_state_fun Unknown)) - | Write_mem write_k loc length l_track value v_track i_state_fun -> - (E_write_mem write_k loc length l_track value v_track)::(ie_loop mode (i_state_fun true)) + | Read_mem read_k loc tracking length ltracking i_state_fun -> + (E_read_mem read_k loc tracking length ltracking)::(ie_loop mode (i_state_fun Unknown)) + | Write_mem write_k loc track length l_track value v_track i_state_fun -> + (E_write_mem write_k loc track length l_track value v_track)::(ie_loop mode (i_state_fun true)) | Internal _ _ next -> (ie_loop mode next) end ;; @@ -219,12 +220,12 @@ let rec rr_ie_loop mode i_state = | Write_reg reg value i_state-> let (events,outcome) = (rr_ie_loop mode i_state) in (((E_write_reg reg value)::events), outcome) - | Read_mem read_k loc length tracking i_state_fun -> + | Read_mem read_k loc tracking length ltracking i_state_fun -> let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in - (((E_read_mem read_k loc length tracking)::events),outcome) - | Write_mem write_k loc length l_track value v_track i_state_fun -> + (((E_read_mem read_k loc tracking length ltracking)::events),outcome) + | Write_mem write_k loc track length l_track value v_track i_state_fun -> let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in - (((E_write_mem write_k loc length l_track value v_track)::events),outcome) + (((E_write_mem write_k loc track length l_track value v_track)::events),outcome) | Internal _ _ next -> (rr_ie_loop mode next) end ;; diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 2051233d..68e57b47 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -1,4 +1,5 @@ import Interp +open import Interp_ast open import Pervasives open import Num @@ -22,7 +23,7 @@ type value = some special registers, with no clear mapping to bits. Should we permit Record of (string * Bitvector) values as well? *) -| Bytevector of list word8 * bool * integer (* For memory accesses : see above *) +| Bytevector of list word8 (* For memory accesses *) | Unknown (*To add: an abstract value representing an unknown but named memory address?*) @@ -35,10 +36,11 @@ type reg_name = | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *) type outcome = -(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *) -| Read_mem of read_kind * value * integer * maybe (list reg_name) * (value -> instruction_state) +(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values, + integer is size to read, followed by registers that were used in computing that size *) +| Read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * (value -> instruction_state) (* Request to write memory, first value and dependent registers is location, second is the value to write *) -| Write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) +| Write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state) (* Request a memory barrier *) | Barrier of barrier_kind * instruction_state (* Request to read register, will track dependency when mode.track_values *) @@ -49,16 +51,19 @@ type outcome = | Nondet_choice of list instruction_state * instruction_state (* Stop for incremental stepping, function can be used to display function call data *) | Internal of maybe string * maybe (unit -> string) * instruction_state +(* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler *) +| Escape of maybe instruction_state | Done | Error of string type event = -| E_read_mem of read_kind * value * integer * maybe (list reg_name) -| E_write_mem of write_kind * value * integer * maybe (list reg_name) * value * maybe (list reg_name) +| E_read_mem of read_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) +| E_write_mem of write_kind * value * maybe (list reg_name) * integer * maybe (list reg_name) * value * maybe (list reg_name) | E_barrier of barrier_kind | E_read_reg of reg_name | E_write_reg of reg_name * value | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*) +(*should there be a representation for escape down here?*) (*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*) (* Functions to build up the initial state for interpretation *) @@ -66,9 +71,20 @@ val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come val initial_instruction_state : context -> string -> list value -> instruction_state (* string is a function name, list of value are the parameters to that function *) +(*Type representint the constructor parameters in instruction_form, other is a type not representable externally*) +type instr_parm_typ = + | Bit (*A single bit, represented as a one element Bitvector as a value*) + | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *) + | Bvector of maybe integer (* A bitvector type, with length when statically known *) + +(*A representation of the AST node for each instruction in the spec, with concrete values from this call, 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_form = (string * list (string * instr_parm_typ * value) * list base_effect) + type i_state_or_error = - | Instr of instruction_state - | Unsupported_instruction_error + | Instr of instruction_state * instruction_form + | Unsupported_instruction_error of instruction_form | Not_an_instruction_error | Internal_error of string diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index a9c22b6c..a54dc6e1 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -49,7 +49,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu let val_to_string v = match v with | Bitvector(bools, _, _) -> "0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools)) - | Bytevector(words, _, _)-> + | Bytevector words-> "0x" ^ (String.concat "" (List.map (function | 10 -> "A" diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index fbb06eed..60258504 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -50,7 +50,7 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu let val_to_string v = match v with | Bitvector(bools, inc, fst)-> let l = List.length bools in (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools)) - | Bytevector(words, inc, fst)-> + | Bytevector words -> let l = List.length words in (string_of_int l) ^ " bytes --" ^ (String.concat "" @@ -191,7 +191,7 @@ module Mem = struct add key valu m let to_string loc v = - sprintf "[%s] -> %x" (val_to_string (Bytevector(loc, true, zero_big_int))) v + sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v end ;; let rec slice bitvector (start,stop) = @@ -202,8 +202,8 @@ let rec slice bitvector (start,stop) = inc, (if inc then zero_big_int else (add_big_int (sub_big_int stop start) unit_big_int))) - | Bytevector(bytes, inc, fst) -> - Bytevector((Interp.from_n_to_n start stop bytes),inc,fst) (*This is wrong, need to explode and re-encode, but maybe never happens?*) + | Bytevector bytes -> + Bytevector((Interp.from_n_to_n start stop bytes)) (*This is wrong, need to explode and re-encode, but maybe never happens?*) | Unknown0 -> Unknown0 ;; @@ -245,12 +245,12 @@ let fupdate_slice original e (start,stop) = (if inc then (sub_big_int start fst) else (sub_big_int fst start)) (if inc then (sub_big_int stop fst) else (sub_big_int fst stop)) bs bools), inc, fst) | _ -> Unknown0) - | Bytevector(bytes,inc,fst) -> (*Can this happen?*) + | Bytevector bytes -> (*Can this happen?*) (match e with - | Bytevector([byte],_,_) -> - Bytevector((list_update zero_big_int start stop byte bytes),inc,fst) - | Bytevector(bs,_,_) -> - Bytevector((list_update_list zero_big_int start stop bs bytes),inc,fst) + | Bytevector [byte] -> + Bytevector (list_update zero_big_int start stop byte bytes) + | Bytevector bs -> + Bytevector (list_update_list zero_big_int start stop bs bytes) | _ -> Unknown0) | Unknown0 -> Unknown0 ;; @@ -272,10 +272,10 @@ let rec format_events = function " Failed with message : " ^ s ^ "\n" | (E_error s)::events -> " Failed with message : " ^ s ^ " but continued on erroneously\n" - | (E_read_mem(read_kind, location, length, dep))::events -> + | (E_read_mem(read_kind, location,depl, length, dep))::events -> " Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^ (format_events events) - | (E_write_mem(write_kind,location, length, dep, value, vdep))::events -> + | (E_write_mem(write_kind,location,depl, length, dep, value, vdep))::events -> " Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^ (format_events events) | ((E_barrier b_kind)::events) -> @@ -306,13 +306,13 @@ let rec perform_action ((reg, mem) as env) = function let old_val = Reg.find id reg in let new_val = fupdate_slice old_val value (combine_slices range mini_range) in (None,(Reg.add id new_val reg,mem)) - | Read_mem0(_,Bytevector(location,_,_), length, _,_) -> + | Read_mem0(_,(Bytevector location),_, length, _,_) -> let rec reading location length = if eq_big_int length zero_big_int then [] else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in - (Some (Bytevector((List.rev (reading location length)), true, zero_big_int)), env) (*TODO: how to get order back here? *) - | Write_mem0(_,(Bytevector(location,_,_)), length, _, (Bytevector(bytes,_,_)),_,_) -> + (Some (Bytevector((List.rev (reading location length)))), env) + | Write_mem0(_,(Bytevector location),_, length, _, (Bytevector bytes),_,_) -> let rec writing location length bytes mem = if eq_big_int length zero_big_int then mem @@ -440,7 +440,7 @@ let run | Write_reg0(reg,value,next) -> show "write_reg" (reg_name_to_string reg) left (val_to_string value); (step next, env', next) - | Read_mem0(kind, location, length, dependencies, next_thunk) -> + | Read_mem0(kind, location, ldeps, length, dependencies, next_thunk) -> (match return with | Some(value) -> show "read_mem" (val_to_string location) right (val_to_string value); @@ -451,7 +451,7 @@ let run let next = next_thunk value in (step next, env', next) | None -> assert false) - | Write_mem0(kind,location, length, dependencies, value, val_dependencies, next_thunk) -> + | Write_mem0(kind,location, ldeps, length, dependencies, value, val_dependencies, next_thunk) -> show "write_mem" (val_to_string location) left (val_to_string value); (match (dependencies,val_dependencies) with | (None,None) -> (); |