diff options
Diffstat (limited to 'src/lem_interp/interp.lem')
| -rw-r--r-- | src/lem_interp/interp.lem | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index d0899674..ef5743bf 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -56,7 +56,7 @@ type value = | V_unknown (* Distinct from undefined, used by memory system *) | V_register of reg_form (* Value to store register access, when not actively reading or writing *) | 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 *) + | V_track of value * (set reg_form) (* Used when memory system wants to track what register(s) a value came from *) let rec {ocaml} string_of_reg_form r = match r with | Reg id _ _ -> get_id id @@ -431,16 +431,15 @@ let list_nth l n = List_extra.nth l n val list_length : forall 'a . list 'a -> integer let list_length l = integerFromNat (List.length l) -val taint: value -> list reg_form -> value +val taint: value -> set reg_form -> value let rec taint value regs = - match regs with - | [] -> value - | _ -> - match value with - | V_track value rs -> taint value (regs ++ rs) - | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals) - | _ -> V_track value regs -end end + if Set.null regs + then value + else match value with + | V_track value rs -> taint value (regs union rs) + | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals) + | _ -> V_track value regs +end val retaint: value -> value -> value let retaint orig updated = @@ -459,7 +458,7 @@ end (* the inner lambda is to make Isabelle happier about overlapping patterns *) let rec binary_taint thunk = fun vall valr -> match (vall,valr) with - | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++rr) + | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl union rr) | (V_track vl rl,vr) -> taint (binary_taint thunk vl vr) rl | (vl,V_track vr rr) -> taint (binary_taint thunk vl vr) rr | (vl,vr) -> thunk vl vr @@ -1367,7 +1366,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = | (V_track _ rs, V_lit _) -> to_exp mode env (taint (V_lit diff) rs) | (V_lit _, V_track _ rs) -> to_exp mode env (taint (V_lit diff) rs) | (V_track _ r1, V_track _ r2) -> - (to_exp mode env (taint (V_lit diff) (r1 ++ r2))) end in + (to_exp mode env (taint (V_lit diff) (r1 union r2))) end in let e = (E_aux (E_block [(E_aux |