diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 12 | ||||
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 1 | ||||
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 40 |
3 files changed, 43 insertions, 10 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index f2fbcec2..efb1db7a 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -417,11 +417,11 @@ let detaint value = | v -> v end -let binary_taint thunk vall valr = +let rec binary_taint thunk vall valr = match (vall,valr) with - | (V_track vl rl,V_track vr rr) -> taint (thunk vl vr) (rl++rr) - | (V_track vl rl,vr) -> taint (thunk vl vr) rl - | (vl,V_track vr rr) -> taint (thunk vl vr) rr + | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++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 end @@ -1237,7 +1237,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let (by_e,env) = to_exp mode le by_val_whole in match by_val with | V_lit (L_aux (L_num by_num) bl) -> - if (from_num = to_num) + if ((is_inc && (from_num >= to_num)) || (from_num <= to_num)) then (Value(V_lit (L_aux L_unit l)),lm,le) else let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in @@ -1458,7 +1458,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) = let inc = n1 < n2 in V_vector n1 inc (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown) - | _ -> Assert_extra.failwith "Vector slice of non-vector" end) end) in + | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end) in (Value (binary_taint take_slice slice vvec), lm,le)) (fun a -> let rebuild v env = let (ie1,env) = to_exp mode env i1v in diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 3aef9d3b..648a61bd 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -180,6 +180,7 @@ let rec extern_mem_value mode v = match v with | Interp.V_vector fst inc bits -> (to_bytes (bitls_from_ibits bits), Nothing) | Interp.V_vector_sparse fst stop inc bits default -> extern_mem_value mode (Interp_lib.fill_in_sparse v) + | _ -> Assert_extra.failwith ("extern_mem_value received non-externable value " ^ (Interp.string_of_value v)) end let rec extern_ifield_value v = match v with diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 033057c3..7e573308 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -231,6 +231,14 @@ let exts (V_tuple[v1;v]) = end in binary_taint exts_help v1 v +let extz (V_tuple[v1;v]) = + let extz_help v1 v = match (v1,v) with + | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Unsigned v) + | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown + | (V_unknown,_) -> V_unknown + end in + binary_taint extz_help v1 v + let eq (V_tuple [x; y]) = let combo = binary_taint (fun v _ -> v) x y in retaint combo (V_lit (L_aux (if value_eq (detaint x) (detaint y) then L_one else L_zero) Unknown)) @@ -317,13 +325,13 @@ let rec arith_op_overflow_vec_bit op sign size (V_tuple [vl;vr]) = arith_op op (V_tuple [l1';(V_lit (L_aux (match bit with | L_one -> L_num 1 | L_zero -> L_num 0 end) li))]) in let correct_size_num = to_vec ord act_size n in let one_larger = to_vec ord (act_size +1) n in - let overflow = (match n with + let overflow = retaint n (match detaint n with | V_lit (L_aux (L_num n') ln) -> if (n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)) then V_lit (L_aux L_zero ln) else V_lit (L_aux L_one ln) end) in - V_tuple [correct_size_num;overflow;(match one_larger with V_vector _ _ (c::rst) -> c end)] + V_tuple [correct_size_num;overflow;(match detaint one_larger with V_vector _ _ (c::rst) -> c end)] | (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown] | (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown] end in @@ -399,7 +407,7 @@ let rec arith_op_vec_no0 op op_s sign size (V_tuple [vl;vr]) = if is_l2_unknown then V_unknown else (to_num sign vr)) in let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in let representable = - match n with + match detaint n with | V_lit (L_aux (L_num n') ln) -> let rep_size = (if op_s = "quot" then act_size/2 else act_size) in ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size))) @@ -420,7 +428,7 @@ let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple [vl;vr]) = if is_l2_unknown then V_unknown else (to_num sign vr)) in let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in let representable = - match n with + match detaint n with | V_lit (L_aux (L_num n') ln) -> let rep_size = (if op_s = "quot" then act_size/2 else act_size) in ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size))) @@ -445,6 +453,26 @@ let rec arith_op_vec_range_no0 op op_s sign size (V_tuple [vl;vr]) = end in binary_taint arith_help vl vr +let rec shift_op_vec op (V_tuple [vl;vr]) = + let arith_op_help vl vr = + match (vl,vr) with + | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) -> + (match op with + | "<<" -> + V_vector b ord + ((from_n_to_n n (integerFromNat ((length cs) - 1)) cs) ++(List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown)))) + | ">>" -> + V_vector b ord + ((List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs)) + | "<<<" -> + V_vector b ord + ((from_n_to_n n (integerFromNat ((length cs) -1)) cs) ++ (from_n_to_n 0 (n-1) cs)) end) + | (V_unknown,_) -> V_unknown + | (_,V_unknown) -> V_unknown + end in + binary_taint arith_op_help vl vr + + let rec compare_op op (V_tuple [vl;vr]) = let comp_help vl vr = match (vl,vr) with | (V_unknown,_) -> V_unknown @@ -541,6 +569,9 @@ let function_map = [ ("mult_range_vec_signed", arith_op_range_vec ( * ) Signed 2); ("mult_vec_range_signed", arith_op_vec_range ( * ) Signed 2); ("mult_overflow_vec_signed", arith_op_overflow_vec ( * ) Signed 2); + ("bitwise_leftshift", shift_op_vec "<<"); + ("bitwise_rightshift", shift_op_vec ">>"); + ("bitwise_rotate", shift_op_vec "<<<"); ("mod", arith_op_no0 (mod)); ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1); ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1); @@ -558,6 +589,7 @@ let function_map = [ ("to_num_inc", to_num Unsigned); ("to_num_dec", to_num Unsigned); ("EXTS", exts); + ("EXTZ", extz); ("to_vec_inc", to_vec_inc); ("to_vec_dec", to_vec_dec); ("bitwise_not", bitwise_not); |