More work on interpreter and Power model

4 files changed, 40 insertions, 21 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
diff --git a/src/test/power.sail b/src/test/power.sail
index 64a487e6..fc90c654 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -1,27 +1,27 @@
-(* XXX types are wrong *)
-val extern forall Type 'a, Type 'b, Type 'c . ( 'a * 'b ) -> 'c effect pure (deinfix + ) = "add"
-val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix mod ) = "mod"
-val extern forall Type 'a, Type 'b, Type 'c .
-  ( 'a * 'b ) -> 'c effect pure (deinfix : ) = "vec_concat"
-val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"
-val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec"
-val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc"
-val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
-
-val extern forall Type 'a . ( 'a * 'a ) -> bit effect pure (deinfix == ) = "eq"
-val extern forall Type 'a . ( 'a * 'a ) -> bit effect pure (deinfix != ) = "neq"
-
-val extern forall Type 'a . 'a -> 'a effect pure (deinfix ~ ) = "bitwise-not"
-val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix ^ ) = "bitwise-xor"
-val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix || ) = "bitwise-or"
-val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix & ) = "bitwise-and"
-
-val extern bit -> bool effect pure is_one = "is_one"
 
 (* XXX sign extension *)
 function forall Type 'a . 'a exts ( x ) = x
 
-register (vector<0, 16, inc, (vector<0, 63, inc, bit>)> ) GPR
+register (vector <0, 63, inc, bit>) GPR0
+register (vector <0, 63, inc, bit>) GPR1
+register (vector <0, 63, inc, bit>) GPR2
+register (vector <0, 63, inc, bit>) GPR3
+register (vector <0, 63, inc, bit>) GPR4
+register (vector <0, 63, inc, bit>) GPR5
+register (vector <0, 63, inc, bit>) GPR6
+register (vector <0, 63, inc, bit>) GPR7
+register (vector <0, 63, inc, bit>) GPR8
+register (vector <0, 63, inc, bit>) GPR9
+register (vector <0, 63, inc, bit>) GPR10
+register (vector <0, 63, inc, bit>) GPR11
+register (vector <0, 63, inc, bit>) GPR12
+register (vector <0, 63, inc, bit>) GPR13
+register (vector <0, 63, inc, bit>) GPR14
+register (vector <0, 63, inc, bit>) GPR15
+
+let (vector <0, 16, inc, (register<(vector<0, 63, inc, bit>)>) >) GPR =
+  [ GPR0, GPR1, GPR2, GPR3, GPR4, GPR5, GPR6, GPR7, GPR8, GPR9, GPR10,
+  GPR11, GPR12, GPR13, GPR14, GPR15 ]
 
 register (bit[64]) NIA (* next instruction address *)
 register (bit[64]) CIA (* current instruction address *)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index e395b09b..da60aa13 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -203,6 +203,7 @@ let initial_typ_env =
     ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "add"),[],pure_e));
     ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e));
     ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e));
+    ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e));
     (*Type incomplete*)
     (":",Some(([("a",{k=K_Typ});("b",{k=K_Typ});("c",{k=K_Typ})],
 	       {t= Tfn ({t=Ttup([{t=Tvar "a"};{t=Tvar "b"}])},{t=Tvar "c"},pure_e)}),External (Some "vec_concat"),[],pure_e));