diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 81 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/run_interp_model.ml | 99 |
4 files changed, 83 insertions, 103 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index da617824..b1ee613d 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -837,30 +837,33 @@ let rec to_exp mode env v : (exp tannot * lenv) = | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env) end -val env_to_let : interp_mode -> lenv -> (exp tannot) -> (exp tannot) -let rec env_to_let_help mode env = match env with - | [] -> [] +val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv) +let rec env_to_let_help mode env taint_env = match env with + | [] -> ([],taint_env) | (i,v)::env -> let t = (val_typ v) in let tan = (val_annot t) in - let (e,_) = to_exp <| mode with track_values = false |> eenv v in - (((P_aux (P_id i) (Unknown,tan)),e),t)::(env_to_let_help mode env) + let (e,taint_env) = to_exp mode taint_env v in + let (rest,taint_env) = env_to_let_help mode env taint_env in + ((((P_aux (P_id i) (Unknown,tan)),e),t)::rest, taint_env) end -let env_to_let mode (LEnv _ env) (E_aux e annot) = - match env_to_let_help mode env with - | [] -> E_aux e annot - | [((p,e),t)] -> E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot - | pts -> let ts = List.map snd pts in - let pes = List.map fst pts in - let ps = List.map fst pes in - let es = List.map snd pes in - let t = T_tup ts in - let tan = val_annot t in - E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan)) - (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan)) - (E_aux e annot)) - annot +let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env = + match env_to_let_help mode env taint_env with + | ([],taint_env) -> (E_aux e annot,taint_env) + | ([((p,e),t)],tain_env) -> + (E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot,taint_env) + | (pts,taint_env) -> + let ts = List.map snd pts in + let pes = List.map fst pts in + let ps = List.map fst pes in + let es = List.map snd pes in + let t = T_tup ts in + let tan = val_annot t in + (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan)) + (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan)) + (E_aux e annot)) + annot, taint_env) end (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *) @@ -897,7 +900,7 @@ let rec match_pattern (P_aux p _) value_whole = if matched_p then (matched_p,used_unknown,(LEnv bi ((id,value_whole)::bounds))) else (false,false,eenv) - | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information, but that's looking less useful *) + | P_typ typ pat -> match_pattern pat value_whole (* Might like to destructure against the type to get information, but that's looking less useful *) | P_id id -> (true, false, (LEnv 0 [(id,value_whole)])) | P_app (Id_aux id _) pats -> match value with @@ -1324,13 +1327,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (fun v lm le -> match find_case pats v with | [] -> (Error l ("No matching patterns in case for value " ^ (string_of_value v)),lm,le) - | [(env,used_unknown,exp)] -> + | [(env,_,exp)] -> if mode.eager_eval then interp_main mode t_level (union_env env l_env) lm exp else debug_out Nothing Nothing exp t_level lm (union_env env l_env) | multi_matches -> - let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in - interp_main mode t_level l_env lm (E_aux (E_block lets) (l,annot)) + let (lets,taint_env) = + List.foldr (fun (env,_,exp) (rst,taint_env) -> + let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in + interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)) end) (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env)))) | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> @@ -1715,7 +1720,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | [] -> (Error l ("No matching pattern for function " ^ name ^ " on value " ^ (string_of_value v)),l_mem,l_env) - | [(env,used_unknown,exp)] -> + | [(env,_,exp)] -> resolve_outcome (if mode.eager_eval then (interp_main mode t_level env emem exp) @@ -1726,9 +1731,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack))) | multi_matches -> - let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in - interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)) - end) + let (lets,taint_env) = + List.foldr (fun (env,_,exp) (rst,taint_env) -> + let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in + interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)) + end) | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end) | Tag_empty -> @@ -1788,8 +1795,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le) else if has_wmem_effect effects then - (*TODO This is wrong, need to split up value or unsplit generally*) - (Action (Write_mem (id_of_string name_ext) v Nothing v) + let (wv,v) = + match v with + | V_tuple params_list -> + let reved = List.reverse params_list in + (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in + (Action (Write_mem (id_of_string name_ext) v Nothing wv) (Hole_frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l, intern_annot annot)) t_level le lm Top),lm,le) else @@ -2090,8 +2101,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level ( t_level l_env l_mem stack))), l_mem,l_env), Nothing) | (e,lm,le) -> ((e,lm,le),Nothing) end) | multi_matches -> - let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in - (interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)), Nothing) + let (lets,taint_env) = + List.foldr (fun (env,_,exp) (rst,taint_env) -> + let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in + (interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)), Nothing) end) | Nothing -> ((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end) @@ -2473,7 +2486,7 @@ let interp mode external_functions defs exp = let rec resume_with_env mode stack value = match (stack,value) with - | (Top,_) -> (Error Unknown "Top hit without expression to evaluate",eenv) + | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv) | (Hole_frame id exp t_level env mem Top,Just value) -> match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,e) -> (o,e) end | (Hole_frame id exp t_level env mem stack,Just value) -> @@ -2503,9 +2516,11 @@ let rec resume_with_env mode stack value = let rec resume mode stack value = match (stack,value) with - | (Top,_) -> Error Unknown "Top hit without expression to evaluate" + | (Top,_) -> Error Unknown "Top hit without expression to evaluate in resume" | (Hole_frame id exp t_level env mem Top,Just value) -> match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,_) -> o end + | (Hole_frame id exp t_level env mem Top,Nothing) -> + Error Unknown "Top hole frame hit wihtout a value in resume" | (Hole_frame id exp t_level env mem stack,Just value) -> match resume mode stack (Just value) with | Value v -> diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 690f8bcf..da87842d 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -437,7 +437,7 @@ let rec interp_to_outcome mode context thunk = length tracking value v_tracking (fun b -> match return with - | Nothing -> (IState next_state context) + | 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") diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index ee141275..4b9cd8b4 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -579,7 +579,9 @@ let mask direction (V_tuple [vsize;v]) = retaint v (match (detaint v,detaint vsi let current_size = List.length l in V_vector (if is_inc(d) then 0 else (n-1)) d (drop (current_size - n) l) | (V_unknown,V_lit (L_aux (L_num n) _)) -> - V_vector 0 direction (List.replicate (natFromInteger n) V_unknown) + let nat_n = natFromInteger n in + let start_num = if is_inc(direction) then 0 else nat_n -1 in + V_vector start_num direction (List.replicate nat_n V_unknown) end) let library_functions direction = [ diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index 57f3f7c1..d865bcf9 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -3,13 +3,12 @@ open Interp_ast ;; open Interp_interface ;; open Interp_inter_imp ;; -open Big_int ;; open Printing_functions ;; module Reg = struct include Map.Make(struct type t = string let compare = compare end) let to_string id v = - sprintf "%s -> %s" id (val_to_string v) + sprintf "%s -> %s" id (register_value_to_string v) let find id m = (* eprintf "reg_find called with %s\n" id; *) let v = find id m in @@ -17,13 +16,14 @@ module Reg = struct v end ;; -let compare_bytes v1 v2 = +let compare_addresses v1 v2 = let rec comp v1s v2s = match (v1s,v2s) with | ([],[]) -> 0 | (v1::v1s,v2::v2s) -> match compare v1 v2 with | 0 -> comp v1s v2s | ans -> ans in + let l1 = List.length v1 in let l2 = List.length v2 in if l1 > l2 then 1 @@ -32,8 +32,8 @@ let compare_bytes v1 v2 = module Mem = struct include Map.Make(struct - type t = word8 list - let compare v1 v2 = compare_bytes v1 v2 + type t = address_lifted + let compare v1 v2 = compare_addresses v1 v2 end) let find idx m = (* eprintf "mem_find called with %s\n" (val_to_string (Bytevector idx));*) @@ -45,32 +45,22 @@ module Mem = struct add key valu m let to_string loc v = - sprintf "[%s] -> %x" (val_to_string (Bytevector loc)) v + sprintf "[%s] -> %s" (memory_value_to_string (memory_value_of_address_lifted loc)) (memory_value_to_string v) end ;; -let rec slice bitvector (start,stop) = - match bitvector with - | Bitvector(bools, inc, fst) -> - Bitvector ((Interp.from_n_to_n (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)) bools), - inc, - (if inc then start else (add_big_int (sub_big_int stop start) unit_big_int))) - - | 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 -;; +let slice register_vector (start,stop) = slice_reg_value register_vector start stop + +let big_num_unit = Nat_big_num.of_int 1 let rec list_update index start stop e vals = match vals with | [] -> [] | x :: xs -> - if eq_big_int index stop + if Nat_big_num.equal index stop then e :: xs - else if ge_big_int index start - then e :: (list_update (add_big_int index unit_big_int) start stop e xs) - else x :: (list_update (add_big_int index unit_big_int) start stop e xs) -;; + else if Nat_big_num.greater_equal index start + then e :: (list_update (Nat_big_num.add index big_num_unit) start stop e xs) + else x :: (list_update (Nat_big_num.add index big_num_unit) start stop e xs) let rec list_update_list index start stop es vals = match vals with @@ -79,56 +69,29 @@ let rec list_update_list index start stop es vals = match es with | [] -> xs | e::es -> - if eq_big_int index stop + if Nat_big_num.equal index stop then e::xs - else if ge_big_int index start - then e :: (list_update_list (add_big_int index unit_big_int) start stop es xs) - else x :: (list_update_list (add_big_int index unit_big_int) start stop (e::es) xs) -;; + else if Nat_big_num.greater_equal index start + then e :: (list_update_list (Nat_big_num.add index big_num_unit) start stop es xs) + else x :: (list_update_list (Nat_big_num.add index big_num_unit) start stop (e::es) xs) -let fupdate_slice original e (start,stop) = - match original with - | Bitvector(bools,inc,fst) -> - (match e with - | Bitvector ([b],_,_) -> - Bitvector((list_update zero_big_int - (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)) b bools), inc, fst) - | Bitvector(bs,_,_) -> - Bitvector((list_update_list zero_big_int - (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 -> (*Can this happen?*) - (match e with - | 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 -;; +let fupdate_slice original e (start,stop) = assert false -let combine_slices (start, stop) (inner_start,inner_stop) = (add_big_int start inner_start, add_big_int start inner_stop) - -let increment bytes = - let adder byte (carry_out, bytes) = - let new_byte = carry_out + byte in - if new_byte > 255 then (1,0::bytes) else (0,new_byte::bytes) - in (snd (List.fold_right adder bytes (1,[]))) -;; -let unit_lit = (L_aux(L_unit,Interp_ast.Unknown)) +let increment address = address (*Need to increment this *) +let combine_slices (start, stop) (inner_start,inner_stop) = + (start + inner_start, start + inner_stop) +let unit_lit = (L_aux(L_unit,Interp_ast.Unknown)) let rec perform_action ((reg, mem) as env) = function (* registers *) - | Read_reg0((Reg0 id), _) -> (Some(Reg.find id reg), env) + | Read_reg0(Reg0(id,_), _) -> (Some(Reg.find id reg), env) | Read_reg0(Reg_slice(id, range), _) | Read_reg0(Reg_field(id, _, range), _) -> (Some(slice (Reg.find id reg) range), env) | Read_reg0(Reg_f_slice(id, _, range, mini_range), _) -> (Some(slice (slice (Reg.find id reg) range) mini_range),env) - | Write_reg0(Reg0 id, value, _) -> (None, (Reg.add id value reg,mem)) + | Write_reg0(Reg0(id,_), value, _) -> (None, (Reg.add id value reg,mem)) | Write_reg0(Reg_slice(id,range),value, _) | Write_reg0(Reg_field(id,_,range),value,_)-> let old_val = Reg.find id reg in @@ -138,20 +101,20 @@ 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(_,location, length, _,_) -> let rec reading location length = - if eq_big_int length zero_big_int + if length = 0 then [] - else (Mem.find location mem)::(reading (increment location) (sub_big_int length unit_big_int)) in - (Some (Bytevector(reading location length)), env) - | Write_mem0(_,(Bytevector location), length, _, (Bytevector bytes),_,_) -> + else (Mem.find location mem)::(reading (increment location) (length - 1)) in + (Some (reading location length), env) + | Write_mem0(_,location, length, _, bytes,_,_) -> let rec writing location length bytes mem = - if eq_big_int length zero_big_int + if length = 0 then mem else match bytes with | [] -> mem | b::bytes -> - writing (increment location) (sub_big_int length unit_big_int) bytes (Mem.add location b mem) in + writing (increment location) (length - 1) bytes (Mem.add location b mem) in (None,(reg,writing location length bytes mem)) | _ -> (None, env) ;; |