add command line argument for setting undef values to all zero or all one. Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work.

2 files changed, 11 insertions, 2 deletions

diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 0386c981..e967eb1c 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -74,6 +74,7 @@ let args = [
   ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
   ("--trace", Arg.Set trace_writes, "trace all register writes"); (* trace_writes is in sail_values.ml *)
   ("--quiet", Arg.Clear interact_print, "suppress trace of PC");
+  ("--undef", Arg.String (fun s -> undef_val := bit_of_string s), "value to use for undef (u,0,1)");
 ]
 
 module type ISA_model = sig
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 1516c503..7e6f0ae7 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -11,6 +11,8 @@ type _bool = vbit
 type _string = string
 type _nat = number
 
+let undef_val = ref Vundef
+
 type value =
   | Vvector of vbit array * int * bool
   | VvectorR of value array * int * bool
@@ -25,6 +27,12 @@ let string_of_bit = function
   | Vzero  -> "0"
   | Vundef -> "u"
 
+let bit_of_string = function
+  | "1" -> Vone
+  | "0" -> Vzero
+  | "u" -> Vundef
+  | _ -> failwith "invalid bit value"
+
 let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) 
 
 let string_of_value = function
@@ -509,13 +517,13 @@ let to_vec_inc = to_vec_inc_big
 let to_vec_dec = to_vec_dec_big
 
 let to_vec_undef_int ord len = 
-  let array = Array.make len Vundef in
+  let array = Array.make len !undef_val in
   let start = if ord then 0 else len-1 in
   Vvector(array, start, ord)
 
 let to_vec_undef_big ord len = 
   let len = int_of_big_int len in
-  let array = Array.make len Vundef in
+  let array = Array.make len !undef_val in
   let start = if ord then 0 else len-1 in
   Vvector(array, start, ord)