More work on interpreter and Power model

2 files changed, 19 insertions, 1 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index efccc9bb..8a0083a7 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -61,6 +61,14 @@ let rec add (V_tuple args) = match args with
       let len = List.length l in
       add (V_tuple [v; (if d then to_vec_inc else to_vec_dec) len n])
   (* assume other literals are L_bin or L_hex, ie. vectors *)
+  | [(V_lit (L_aux L_zero _) as l); x] ->
+      add (V_tuple [V_vector 0 true [l]; x])
+  | [(V_lit (L_aux L_one _) as l); x] ->
+      add (V_tuple [V_vector 0 true [l]; x])
+  | [x; (V_lit (L_aux L_zero _) as l)] ->
+      add (V_tuple [x; V_vector 0 true [l]])
+  | [x; (V_lit (L_aux L_one _) as l)] ->
+      add (V_tuple [x; V_vector 0 true [l]])
   | [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
   | [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
   end ;;
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index b519a2cb..c9222463 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -30,7 +30,7 @@ let loc_to_string = function
       " to line " ^ (string_of_int tline) ^ " character " ^ (string_of_int tchar)
 ;;
 
-let bitvec_to_string l = "0b" ^ (String.concat "" (List.map (function
+let bitvec_to_string l = "0b" ^ (String.concat "" (List.rev_map (function
   | V_lit(L_aux(L_zero, _)) -> "0"
   | V_lit(L_aux(L_one, _)) -> "1"
   | _ -> assert false) l))
@@ -101,6 +101,16 @@ let id_compare i1 i2 =
 
 module Reg = struct
   include Map.Make(struct type t = id let compare = id_compare end)
+
+  let zero_vec =
+    V_vector (zero_big_int, true, Array.to_list (Array.make 64
+    (V_lit(L_aux(L_zero, Unknown)))))
+
+  let find id reg =
+    try find id reg
+    with Not_found ->
+      (* default to a 64-bit big-endian vector of zero bits *)
+      zero_vec
 end ;;
 
 module Mem = struct