summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
-rw-r--r--src/lem_interp/interp_lib.lem88
-rw-r--r--src/lem_interp/run_interp_model.ml42
3 files changed, 105 insertions, 27 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8265fd5e..a2d59943 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -44,7 +44,7 @@ let extern_value mode for_mem v = match v with
if for_mem
then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
else (Bitvector (from_bits bits) inc fst, Nothing)
- | Interp.V_track (Interp.V_vector fst inc bits) regs ->
+ | Interp.V_track (Interp.V_vector fst inc bits) regs ->
if for_mem
then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst,
if (mode.Interp.track_values)
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 8d13bcb0..990382ff 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -80,32 +80,45 @@ let bitwise_not_bit v =
| L_one -> (V_lit (L_aux L_zero loc)) end in
match v with
| V_lit lit -> lit_not lit
+ | V_unknown -> V_unknown
| V_track (V_lit lit) r -> V_track (lit_not lit) r
end;;
let bitwise_binop_bit op (V_tuple [x; y]) = match (x,y) with
| (V_track x rx,V_track y ry) ->
- V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) (rx ++ ry)
+ taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) (rx ++ ry)
| (V_track x rx,y) ->
- V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) rx
+ taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) rx
| (x,V_track y ry) ->
- V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) ry
+ taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) ry
+ | (V_unknown,_) -> V_unknown
+ | (_,V_unknown) -> V_unknown
| _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
end ;;
-let bitwise_binop op (V_tuple [v1;v2]) =
+let rec bitwise_binop op (V_tuple [v1;v2]) =
match (v1,v2) with
| (V_vector idx inc v, V_vector idx' inc' v') ->
(* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
V_vector idx inc (List.map apply (List.zip v v'))
+ | (V_track v1 r1, V_track v2 r2) ->
+ taint (bitwise_binop op (V_tuple [v1;v2])) (r1 ++ r2)
+ | (V_track v1 r1,v2) ->
+ taint (bitwise_binop op (V_tuple [v1;v2])) r1
+ | (v1,V_track v2 r2) ->
+ taint (bitwise_binop op (V_tuple [v1;v2])) r2
+ | (V_unknown,_) -> V_unknown
+ | (_,V_unknown) -> V_unknown
end ;;
(* BitSeq expects LSB first.
* By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
* hence MSB first.
* http://en.wikipedia.org/wiki/Bit_numbering *)
-let to_num signed (V_vector idx inc l) =
+let rec to_num signed v =
+ match v with
+ | (V_vector idx inc l) ->
(* Word library in Lem expects bitseq with LSB first *)
(*TODO: Kathy think more
We thought a reverse was needed due to above comments only in inc case.
@@ -115,7 +128,10 @@ let to_num signed (V_vector idx inc l) =
let l = (*if inc then reverse l else l*) reverse l in
(* Make sure the last bit is a zero to force unsigned numbers *)
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
- V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
+ V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
+ | V_unknown -> V_unknown
+ | V_track v r -> taint (to_num signed v) r
+end ;;
(*TODO As with above, consider the reverse here in both cases, where we're again always interpreting with the MSB on the left *)
let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
@@ -145,31 +161,73 @@ let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
let neq = compose neg eq ;;
-let arith_op op (V_tuple args) = match args with
+let rec arith_op op (V_tuple args) = match args with
+ | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
+ | [V_track v1 r1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1;v2] -> taint (arith_op op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
- | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
end ;;
-let arith_op_vec op (V_tuple args) = match args with
+let rec arith_op_vec op (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
let (l1',l2') = (to_num false l1,to_num false l2) in
let n = arith_op op (V_tuple [l1';l2']) in
to_vec ord (List.length cs) n
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_vec op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1;v2] ->
+ taint (arith_op_vec op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_vec op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
end ;;
-let arith_op_range_vec op (V_tuple args) = match args with
+let rec arith_op_range_vec op (V_tuple args) = match args with
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_range_vec op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1; v2] ->
+ taint (arith_op_range_vec op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_range_vec op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
| [n; (V_vector _ ord cs as l2)] ->
arith_op_vec op (V_tuple [(to_vec ord (List.length cs) n);l2])
end ;;
-let arith_op_vec_range op (V_tuple args) = match args with
+let rec arith_op_vec_range op (V_tuple args) = match args with
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_vec_range op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1; v2] ->
+ taint (arith_op_vec_range op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_vec_range op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
| [(V_vector _ ord cs as l1);n] ->
- arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
+ arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
-
-let arith_op_range_vec_range op (V_tuple args) = match args with
+let rec arith_op_range_vec_range op (V_tuple args) = match args with
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_range_vec_range op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1; v2] ->
+ taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
| [n;(V_vector _ ord _ as l2)] ->
arith_op op (V_tuple [n;(to_num ord l2)])
end ;;
-let arith_op_vec_range_range op (V_tuple args) = match args with
+let rec arith_op_vec_range_range op (V_tuple args) = match args with
+ | [V_track v1 r1;V_track v2 r2] ->
+ taint (arith_op_vec_range_range op (V_tuple [v1;v2])) (r1++r2)
+ | [V_track v1 r1; v2] ->
+ taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r1
+ | [v1;V_track v2 r2] ->
+ taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r2
+ | [V_unknown;_] -> V_unknown
+ | [_;V_unknown] -> V_unknown
| [(V_vector _ ord _ as l1);n] ->
arith_op op (V_tuple [(to_num ord l1);n])
end ;;
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 9591b918..5d461b52 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -59,9 +59,12 @@ let val_to_string v = match v with
let reg_name_to_string = function
| Reg0 s -> s
- | Reg_slice(s,(first,second)) -> s (*contemplate putting slice here*)
+ | Reg_slice(s,(first,second)) ->
+ s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
| Reg_field(s,f,_) -> s ^ "." ^ f
- | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f
+ | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+
+let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
let rec val_to_string_internal = function
| Interp.V_boxref(n, t) -> sprintf "boxref %d" n
@@ -305,6 +308,7 @@ let run
?(reg=Reg.empty)
?(mem=Mem.empty)
?(eager_eval=true)
+ ?(track_dependencies= ref false)
?mode
(name, spec) =
let get_loc (E_aux(_, (l, _))) = loc_to_string l in
@@ -314,7 +318,8 @@ let run
let usage = "Usage:
step go to next action [default]
next go to next break point
- run complete current execution,
+ run complete current execution
+ track begin/end tracking register dependencies
bt print call stack
cont print continuation of the top stack frame
reg print content of environment
@@ -341,6 +346,9 @@ let run
(* print not-compacted continuation *)
print_exp (top_frame_exp stack);
interact mode env stack
+ | "track" | "t" ->
+ track_dependencies := not(!track_dependencies);
+ interact mode env stack
| "show_casts" ->
Pretty_interp.ignore_casts := false;
interact mode env stack
@@ -357,10 +365,10 @@ let run
let rec loop mode env = function
| Done ->
debugf "%s: %s\n" (grey name) (blue "done");
- (true, mode, env)
+ (true, mode, !track_dependencies, env)
| Error0 s ->
debugf "%s: %s: %s\n" (grey name) (red "error") s;
- (false, mode, env)
+ (false, mode, !track_dependencies, env)
| action ->
let step ?(force=false) stack =
let top_exp = top_frame_exp stack in
@@ -386,13 +394,25 @@ let run
| Read_mem0(kind, location, length, dependencies, next_thunk) ->
(match return with
| Some(value) ->
- (*TODO: show length, conditionally show dependencies *)
show "read_mem" (val_to_string location) right (val_to_string value);
+ (match dependencies with
+ | None -> ()
+ | Some(deps) ->
+ show "read_mem address depended on" (dependencies_to_string deps) "" "");
let next = next_thunk value in
(step next, env', next)
| None -> assert false)
| Write_mem0(kind,location, 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) -> ();
+ | (Some(deps),None) ->
+ show "write_mem address depended on" (dependencies_to_string deps) "" "";
+ | (None,Some(deps)) ->
+ show "write_mem value depended on" (dependencies_to_string deps) "" "";
+ | (Some(deps),Some(vdeps)) ->
+ show "write_mem address depended on" (dependencies_to_string deps) "" "";
+ show "write_mem value depended on" (dependencies_to_string vdeps) "" "";);
let next = next_thunk true in
(step next,env',next)
| Barrier0(bkind,next) ->
@@ -406,21 +426,21 @@ let run
let choose_order = List.sort (fun (_,i1) (_,i2) -> compare i1 i2)
(List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
show "nondeterministic evaluation begun" "" "" "";
- let (_,_,env') = List.fold_right (fun (next,_) (_,_,env') ->
- loop mode env' (interp0 (make_mode (mode=Run) false) next)) choose_order (false,mode,env'); in
+ let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') ->
+ loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) choose_order (false,mode,!track_dependencies,env'); in
show "nondeterministic evaluation ended" "" "" "";
(step next,env',next)
(* | Exit e ->
show "exiting current evaluation" "" "" "";
step (),env', (set_in_context s e)*)
in
- loop mode' env' (interp0 (make_mode (mode' = Run) false) next) in
+ loop mode' env' (interp0 (make_mode (mode' = Run) !track_dependencies) next) in
let mode = match mode with
| None -> if eager_eval then Run else Step
| Some m -> m in
let context = build_context spec in
let initial_state = initial_instruction_state context main_func parameters in
- let imode = make_mode eager_eval false in
+ let imode = make_mode eager_eval !track_dependencies in
let top_exp = top_frame_exp initial_state in
debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp top_exp);
try
@@ -429,5 +449,5 @@ let run
with e ->
let trace = Printexc.get_backtrace () in
debugf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace;
- false, mode, (reg, mem)
+ (false, mode, !track_dependencies, (reg, mem))
;;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 09:52:23 +0000