Give a better answer on overflow with two vectors of unknowns (i.e. unknown instead of 0)

2 files changed, 10 insertions, 7 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index aca430cb..b20aee1e 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -206,6 +206,7 @@ let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero)
 (* XXX interpret vectors as unsigned numbers for equality *)
 let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num Unsigned v; r]) ;;
 let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num Unsigned v]) ;;
+let eq_vec_vec (V_tuple [v;v2]) = eq (V_tuple [to_num Signed v; to_num Signed v2]);;
 
 let rec neg v = match v with
   | V_lit (L_aux arg la) -> 
@@ -220,6 +221,8 @@ end
 
 let neq = compose neg eq ;;
 
+let neq_vec = compose neg eq_vec_vec
+
 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)
@@ -261,7 +264,7 @@ let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
     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
+    let overflow = if (has_unknown l1 || has_unknown l2) then V_unknown else neq_vec (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 sign size (V_tuple [v1;v2])) (r1++r2)
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 9eb77dd1..4810f3df 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -155,10 +155,10 @@ let logfile_address_to_string a =
   logfile_memory_value_to_string bs'
   
 
-let bytes_to_string bytes = 
+(*let bytes_to_string bytes = 
   (String.concat ""
      (List.map (fun i -> hex_int_to_string i) 
-	(List.map (fun (Byte_lifted bs) -> bits_to_word8 bs) bytes)))
+	(List.map (fun (Byte_lifted bs) -> bits_to_word8 bs) bytes)))*)
 
 
 let bit_to_string = function
@@ -167,14 +167,14 @@ let bit_to_string = function
 
 
 
-let reg_value_to_string v = 
-  let l = List.length v.rv_bits in
+let reg_value_to_string v = "deprecated"
+(*  let l = List.length v.rv_bits in
   let start = string_of_int v.rv_start in
   if List.mem l [8;16;32;64;128] then
     let bytes = Interp_inter_imp.to_bytes v.rv_bits in
     "0x" ^ "_" ^ start ^ "'" ^ bytes_to_string bytes
   else (string_of_int l) ^ "_" ^ start ^ "'b" ^ 
-    collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")
+    collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")*)
 
 let ifield_to_string v =
   "0b"^ collapse_leading (List.fold_right (^) (List.map bit_to_string v) "")
@@ -346,7 +346,7 @@ let rec format_events = function
     "     Read_reg of " ^ (reg_name_to_string reg_name) ^ "\n" ^
     (format_events events)
   | (E_write_reg(reg_name, value))::events ->
-    "     Write_reg of " ^ (reg_name_to_string reg_name) ^ " writing " ^ (reg_value_to_string value) ^ "\n" ^
+    "     Write_reg of " ^ (reg_name_to_string reg_name) ^ " writing " ^ (register_value_to_string value) ^ "\n" ^
     (format_events events)
 ;;