diff options
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 27 | ||||
| -rw-r--r-- | src/type_internal.ml | 6 |
2 files changed, 32 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 696e0547..860f76d7 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -242,6 +242,32 @@ let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with | [V_unknown;_] -> V_tuple [V_unknown;V_unknown] | [_;V_unknown] -> V_tuple [V_unknown;V_unknown] end ;; +let rec arith_op_overflow_vec_bit op sign size (V_tuple args) = match args with + | [(V_vector b ord cs as l1);(V_lit (L_aux L_one li))] -> + let l1' = to_num sign l1 in + let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 1) li))]) in + let correct_size_num = to_vec ord ((List.length cs) * size) n in + let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in + let overflow = neq (V_tuple [correct_size_num;one_larger]) in + V_tuple [correct_size_num;overflow] + | [(V_vector b ord cs as l1);(V_lit (L_aux L_zero li))] -> + let l1' = to_num sign l1 in + let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 0) li))]) in + let correct_size_num = to_vec ord ((List.length cs) * size) n in + let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in + let overflow = neq (V_tuple [correct_size_num;one_larger]) in + V_tuple [correct_size_num;overflow] + | [V_track v1 r1;V_track v2 r2] -> + taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2) + | [V_track v1 r1;v2] -> + taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r1 + | [v1;V_track v2 r2] -> + taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r2 + | [V_unknown;_] -> V_tuple [V_unknown;V_unknown] + | [_;V_unknown] -> V_tuple [V_unknown;V_unknown] +end ;; + + let rec arith_op_range_vec op sign size (V_tuple args) = match args with | [V_track v1 r1;V_track v2 r2] -> taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) (r1++r2) @@ -441,6 +467,7 @@ let function_map = [ ("add_vec_vec_range_signed", arith_op_vec_vec_range (+) Signed); ("add_vec_bit_signed", arith_op_vec_bit (+) Signed 1); ("add_overflow_vec_signed", arith_op_overflow_vec (+) Signed 1); + ("add_overflow_vec_bit_signed", arith_op_overflow_vec_bit (+) Signed 1); ("minus", arith_op (-)); ("minus_vec", arith_op_vec (-) Unsigned 1); ("minus_vec_range", arith_op_vec_range (-) Unsigned 1); diff --git a/src/type_internal.ml b/src/type_internal.ml index 2ae210da..e2399d88 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -964,7 +964,11 @@ let initial_typ_env = Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t]) (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))), - External (Some "add_vec_bit"), [], pure_e); + External (Some "add_vec_bit_signed"), [], pure_e); + Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t]) + (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")); bit_t]))), + External (Some "add_overflow_vec_bit_signed"), [], pure_e); Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), (mk_pure_fun (mk_tup [bit_t; mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))), |