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.lem4
-rw-r--r--src/lem_interp/interp_lib.lem151
2 files changed, 82 insertions, 73 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index da6b27f4..31a75b73 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -150,11 +150,11 @@ let add_to_address value num =
| Unknown -> Unknown
| Bitvector _ _ _ ->
fst(extern_value (make_mode true false) false Nothing
- (Interp_lib.arith_op_vec_range (+) 1
+ (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1
(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
| Bytevector _ ->
fst(extern_value (make_mode true false) true Nothing
- (Interp_lib.arith_op_vec_range (+) 1
+ (Interp_lib.arith_op_vec_range (+) Interp_lib.Unsigned 1
(Interp.V_tuple [(intern_value value);Interp.V_lit (L_aux (L_num num) Interp_ast.Unknown)])))
end
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 6c6bbb46..696e0547 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -198,109 +198,109 @@ let rec arith_op op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
-let rec arith_op_vec op size (V_tuple args) = match args with
+let rec arith_op_vec op sign size (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
- let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+ let (l1',l2') = (to_num sign l1,to_num sign l2) in
let n = arith_op op (V_tuple [l1';l2']) in
to_vec ord ((List.length cs) * size) n
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1;v2] ->
- taint (arith_op_vec op size (V_tuple [v1;v2])) r1
+ taint (arith_op_vec op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec op size (V_tuple [v1;v2])) r2
+ taint (arith_op_vec op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
-let rec arith_op_vec_vec_range op (V_tuple args) = match args with
+let rec arith_op_vec_vec_range op sign (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
- let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+ let (l1',l2') = (to_num sign l1,to_num sign l2) in
arith_op op (V_tuple [l1';l2'])
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1;v2] ->
- taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_vec_range op (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
-let rec arith_op_overflow_vec op size (V_tuple args) = match args with
+let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
- let (l1',l2') = (to_num Signed l1,to_num Signed l2) in
+ let (l1',l2') = (to_num sign l1,to_num sign l2) in
let n = arith_op op (V_tuple [l1';l2']) 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 op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1;v2] ->
- taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r1
+ taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_overflow_vec op size (V_tuple [v1;v2])) r2
+ taint (arith_op_overflow_vec 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 size (V_tuple args) = match args with
+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 size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_range_vec op size (V_tuple [v1;v2])) r1
+ taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_range_vec op size (V_tuple [v1;v2])) r2
+ taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [n; (V_vector _ ord cs as l2)] ->
- arith_op_vec op size (V_tuple [(to_vec ord (List.length cs) n);l2])
+ arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);l2])
end ;;
-let rec arith_op_vec_range op size (V_tuple args) = match args with
+let rec arith_op_vec_range op sign size (V_tuple args) = match args with
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec_range op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_vec_range op size (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_range op size (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [(V_vector _ ord cs as l1);n] ->
- arith_op_vec op size (V_tuple [l1;(to_vec ord (List.length cs) n)])
+ arith_op_vec op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
-let rec arith_op_range_vec_range op (V_tuple args) = match args with
+let rec arith_op_range_vec_range op sign (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)
+ taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r1
+ taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r2
+ taint (arith_op_range_vec_range op sign (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 Unsigned l2)])
end ;;
-let rec arith_op_vec_range_range op (V_tuple args) = match args with
+let rec arith_op_vec_range_range op sign (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)
+ taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_range_range op sign (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 Unsigned l1);n])
+ arith_op op (V_tuple [(to_num sign l1);n])
end ;;
-let rec arith_op_vec_bit op size (V_tuple args) = match args with
+let rec arith_op_vec_bit op sign size (V_tuple args) = match args with
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec_bit op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_vec_bit op size (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_bit op size (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [(V_vector _ ord cs as l1);V_lit (L_aux bit _)] ->
- let l1' = to_num Unsigned l1 in
+ let l1' = to_num sign l1 in
let n = arith_op op (V_tuple
[l1';
V_lit
@@ -320,31 +320,31 @@ let rec arith_op_no0 op (V_tuple args) = match args with
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
-let rec arith_op_vec_no0 op size (V_tuple args) = match args with
+let rec arith_op_vec_no0 op sign size (V_tuple args) = match args with
| [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
- let (l1',l2') = (to_num Unsigned l1,to_num Unsigned l2) in
+ let (l1',l2') = (to_num sign l1,to_num sign l2) in
let n = arith_op_no0 op (V_tuple [l1';l2']) in
to_vec ord ((List.length cs) * size) n
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1;v2] ->
- taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_no0 op size (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_no0 op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
end ;;
-let rec arith_op_vec_range_no0 op size (V_tuple args) = match args with
+let rec arith_op_vec_range_no0 op sign size (V_tuple args) = match args with
| [V_track v1 r1;V_track v2 r2] ->
- taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) (r1++r2)
+ taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) (r1++r2)
| [V_track v1 r1; v2] ->
- taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r1
+ taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) r1
| [v1;V_track v2 r2] ->
- taint (arith_op_vec_range_no0 op size (V_tuple [v1;v2])) r2
+ taint (arith_op_vec_range_no0 op sign size (V_tuple [v1;v2])) r2
| [V_unknown;_] -> V_unknown
| [_;V_unknown] -> V_unknown
| [(V_vector _ ord cs as l1);n] ->
- arith_op_vec_no0 op size (V_tuple [l1;(to_vec ord (List.length cs) n)])
+ arith_op_vec_no0 op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
end ;;
let rec compare_op op (V_tuple args) = match args with
@@ -424,32 +424,41 @@ let function_map = [
("ignore", ignore_sail);
("length", v_length);
("add", arith_op (+));
- ("add_vec", arith_op_vec (+) 1);
- ("add_vec_range", arith_op_vec_range (+) 1);
- ("add_vec_range_range", arith_op_vec_range_range (+));
- ("add_range_vec", arith_op_range_vec (+) 1);
- ("add_range_vec_range", arith_op_range_vec_range (+));
- ("add_vec_vec_range", arith_op_vec_vec_range (+));
- ("add_vec_bit", arith_op_vec_bit (+) 1);
- ("add_overload_vec", arith_op_overflow_vec (+) 1);
+ ("add_vec", arith_op_vec (+) Unsigned 1);
+ ("add_vec_range", arith_op_vec_range (+) Unsigned 1);
+ ("add_vec_range_range", arith_op_vec_range_range (+) Unsigned);
+ ("add_range_vec", arith_op_range_vec (+) Unsigned 1);
+ ("add_range_vec_range", arith_op_range_vec_range (+) Unsigned);
+ ("add_vec_vec_range", arith_op_vec_vec_range (+) Unsigned);
+ ("add_vec_bit", arith_op_vec_bit (+) Unsigned 1);
+ ("add_overflow_vec", arith_op_overflow_vec (+) Unsigned 1);
+ ("add_signed", arith_op (+));
+ ("add_vec_signed", arith_op_vec (+) Signed 1);
+ ("add_vec_range_signed", arith_op_vec_range (+) Signed 1);
+ ("add_vec_range_range_signed", arith_op_vec_range_range (+) Signed);
+ ("add_range_vec_signed", arith_op_range_vec (+) Signed 1);
+ ("add_range_vec_range_signed", arith_op_range_vec_range (+) Signed);
+ ("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);
("minus", arith_op (-));
- ("minus_vec", arith_op_vec (-) 1);
- ("minus_vec_range", arith_op_vec_range (-) 1);
- ("minus_range_vec", arith_op_range_vec (-) 1);
- ("minus_vec_range_range", arith_op_vec_range_range (-));
- ("minus_range_vec_range", arith_op_range_vec_range (-));
- ("minus_vec_bit", arith_op_vec_bit (-) 1);
- ("minus_overload_vec", arith_op_overflow_vec (-) 1);
+ ("minus_vec", arith_op_vec (-) Unsigned 1);
+ ("minus_vec_range", arith_op_vec_range (-) Unsigned 1);
+ ("minus_range_vec", arith_op_range_vec (-) Unsigned 1);
+ ("minus_vec_range_range", arith_op_vec_range_range (-) Unsigned);
+ ("minus_range_vec_range", arith_op_range_vec_range (-) Unsigned);
+ ("minus_vec_bit", arith_op_vec_bit (-) Unsigned 1);
+ ("minus_overload_vec", arith_op_overflow_vec (-) Unsigned 1);
("multiply", arith_op ( * ));
- ("multiply_vec", arith_op_vec ( * ) 2);
- ("mult_range_vec", arith_op_range_vec ( * ) 2);
- ("mult_vec_range", arith_op_vec_range ( * ) 2);
- ("mult_overload_vec", arith_op_overflow_vec ( * ) 2);
+ ("multiply_vec", arith_op_vec ( * ) Unsigned 2);
+ ("mult_range_vec", arith_op_range_vec ( * ) Unsigned 2);
+ ("mult_vec_range", arith_op_vec_range ( * ) Unsigned 2);
+ ("mult_overload_vec", arith_op_overflow_vec ( * ) Unsigned 2);
("mod", arith_op_no0 (mod));
- ("mod_vec", arith_op_vec_no0 (mod) 1);
- ("mod_vec_range", arith_op_vec_range_no0 (mod) 1);
+ ("mod_vec", arith_op_vec_no0 (mod) Unsigned 1);
+ ("mod_vec_range", arith_op_vec_range_no0 (mod) Unsigned 1);
("quot", arith_op_no0 (/));
- ("quot_vec", arith_op_vec_no0 (/) 1);
+ ("quot_vec", arith_op_vec_no0 (/) Unsigned 1);
("eq", eq);
("eq_vec_range", eq_vec_range);
("eq_range_vec", eq_range_vec);
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-15 21:19:48 +0000