Changes to get another (slightly larger) executable running;

adding executable as a test as well

6 files changed, 136 insertions, 31 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 990382ff..c04ff73d 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -169,43 +169,43 @@ 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 (V_tuple args) = match args with
+let rec arith_op_vec op size (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
     let (l1',l2') = (to_num false l1,to_num false l2) in
     let n = arith_op op (V_tuple [l1';l2']) in
-    to_vec ord (List.length cs) n
+    to_vec ord ((List.length cs) * size) n
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec op size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1;v2] ->
-    taint (arith_op_vec op (V_tuple [v1;v2])) r1
+    taint (arith_op_vec op size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] ->
-    taint (arith_op_vec op (V_tuple [v1;v2])) r2
+    taint (arith_op_vec op size (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
 end ;;
-let rec arith_op_range_vec op (V_tuple args) = match args with
+let rec arith_op_range_vec op size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_range_vec op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_range_vec op size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_range_vec op (V_tuple [v1;v2])) r1
+    taint (arith_op_range_vec op size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_range_vec op (V_tuple [v1;v2])) r2
+    taint (arith_op_range_vec op 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 (V_tuple [(to_vec ord (List.length cs) n);l2])
+    arith_op_vec op size (V_tuple [(to_vec ord (List.length cs) n);l2])
 end ;;
-let rec arith_op_vec_range op (V_tuple args) = match args with
+let rec arith_op_vec_range op size (V_tuple args) = match args with
   | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range op (V_tuple [v1;v2])) (r1++r2)
+    taint (arith_op_vec_range op size (V_tuple [v1;v2])) (r1++r2)
   | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range op (V_tuple [v1;v2])) r1
+    taint (arith_op_vec_range op size (V_tuple [v1;v2])) r1
   | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range op (V_tuple [v1;v2])) r2
+    taint (arith_op_vec_range op 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 (V_tuple [l1;(to_vec ord (List.length cs) n)])
+    arith_op_vec op 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
   | [V_track v1 r1;V_track v2 r2] ->
@@ -244,6 +244,11 @@ let compare_op_vec op (V_tuple args) = match args with
     compare_op op (V_tuple[l1';l2'])
 end ;;
 
+let rec duplicate (V_tuple args) = match args with
+  | [(V_lit _ as v);(V_lit (L_aux (L_num n) _))] ->
+    (V_vector 0 true (List.replicate (natFromInteger n) v))
+end
+
 let rec vec_concat (V_tuple args) = match args with
   | [V_vector n d l; V_vector n' d' l'] ->
       (* XXX d = d' ? droping n' ? *)
@@ -255,16 +260,18 @@ let rec vec_concat (V_tuple args) = match args with
 let function_map = [
   ("ignore", ignore_sail);            
   ("add", arith_op (+));
-  ("add_vec", arith_op_vec (+));
-  ("add_vec_range", arith_op_vec_range (+));
+  ("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 (+));
+  ("add_range_vec", arith_op_range_vec (+) 1);
   ("add_range_vec_range", arith_op_range_vec_range (+));
   ("minus", arith_op (-));
-  ("minus_vec", arith_op_vec (-));
+  ("minus_vec", arith_op_vec (-) 1);
+  ("multiply", arith_op ( * ));
+  ("multiply_vec", arith_op_vec ( * ) 2);
   ("mod", arith_op (mod));
-  ("mod_vec", arith_op_vec (mod));
-  ("mod_vec_range", arith_op_vec_range (mod));
+  ("mod_vec", arith_op_vec (mod) 1);
+  ("mod_vec_range", arith_op_vec_range (mod) 1);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
@@ -288,6 +295,7 @@ let function_map = [
   ("gt", compare_op (>));
   ("lt_vec", compare_op_vec (<));
   ("gt_vec", compare_op_vec (>));
+  ("duplicate", duplicate);
 ] ;;
 
 let eval_external name v = match List.lookup name function_map with
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 9921d9f4..72568c1c 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -221,8 +221,9 @@ let rec list_update index start stop e vals =
 let bool_to_byte = function | true -> 0 | false -> 1
 let bitvector_to_bool = function
   | Bitvector([b],_,_) -> b
+  | Bitvector(bs,_,_) -> false (*TODO fupdate slice got a vector of stuff, not just one new value.*)
   | Bytevector([0],_,_) -> false
-  | Bytevector([1],_,_) -> true
+  | Bytevector(_,_,_) | Unknown0 -> true
 ;;
 
 let fupdate_slice original e (start,stop) =
diff --git a/src/parser.mly b/src/parser.mly
index e805b4b5..6d019af4 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -172,6 +172,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
 %token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
 
+
 %start file nonempty_exp_list
 %type <Parse_ast.defs> defs
 %type <Parse_ast.atyp> typ
@@ -923,13 +924,13 @@ patsexp:
     { peloc (Pat_exp($1,$3)) }
 
 letbind:
-/*  | Let_ atomic_pat Eq atomic_exp
-    { lbloc (LB_val_implicit($2,$4)) }*/
+  | Let_ atomic_pat Eq atomic_exp
+    { lbloc (LB_val_implicit($2,$4)) }
   | Let_ typquant atomic_typ atomic_pat Eq exp
     { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
-  /* This is ambiguous causing 4 shift/reduce and 5 reduce/reduce conflicts because the parser can't tell until the end of typ whether it was parsing a type or a pattern, and this seem to be too late. Solutions are to have a different keyword for this and the above solution besides let (while still absolutely having a keyword here) */
-  | Let_ atomic_typ atomic_pat Eq exp
-    { lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) } 
+/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this
+  | Let_ Lparen typ Rparen atomic_pat Eq exp 
+    { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */
 
 funcl:
   | id atomic_pat Eq exp
diff --git a/src/test/hello3 b/src/test/hello3
new file mode 100644
index 00000000..bb0df93e
--- /dev/null
+++ b/src/test/hello3
diff --git a/src/test/power.sail b/src/test/power.sail
index 75238732..bc184b67 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -355,6 +355,20 @@ val bit[32] -> ast effect pure decode
 
 scattered function ast decode
 
+union ast member (bit[24], bit, bit) B
+
+function clause decode (0b010010 :
+(bit[24]) LI :
+[AA] :
+[LK] as instr) =
+  B (LI,AA,LK)
+
+function clause execute (B (LI, AA, LK)) =
+  {
+    if AA then NIA := EXTS (LI : 0b00) else NIA := CIA + EXTS (LI : 0b00);
+    if LK then LR := CIA + 4
+  }
+
 union ast member (bit[5], bit[5], bit[2], bit) Bclr
 
 function clause decode (0b010011 :
@@ -392,6 +406,23 @@ function clause execute (Lwz (RT, RA, D)) =
     GPR[RT] := 0b00000000000000000000000000000000 : MEMr (EA,4)
   }
 
+union ast member (bit[5], bit[5], bit[14]) Ld
+
+function clause decode (0b111010 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[14]) DS :
+0b00 as instr) =
+  Ld (RT,RA,DS)
+
+function clause execute (Ld (RT, RA, DS)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + EXTS (DS : 0b00);
+    GPR[RT] := MEMr (EA,8)
+  }
+
 union ast member (bit[5], bit[5], bit[16]) Stw
 
 function clause decode (0b100100 :
@@ -423,6 +454,39 @@ function clause execute (Stwu (RS, RA, D)) =
     GPR[RA] := EA
   }
 
+union ast member (bit[5], bit[5], bit[14]) Std
+
+function clause decode (0b111110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[14]) DS :
+0b00 as instr) =
+  Std (RS,RA,DS)
+
+function clause execute (Std (RS, RA, DS)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + EXTS (DS : 0b00);
+    MEMw(EA,8) := GPR[RS]
+  }
+
+union ast member (bit[5], bit[5], bit[14]) Stdu
+
+function clause decode (0b111110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[14]) DS :
+0b01 as instr) =
+  Stdu (RS,RA,DS)
+
+function clause execute (Stdu (RS, RA, DS)) =
+  {
+    EA := GPR[RA] + EXTS (DS : 0b00);
+    MEMw(EA,8) := GPR[RS];
+    GPR[RA] := EA
+  }
+
 union ast member (bit[5], bit[5], bit[16]) Addi
 
 function clause decode (0b001110 :
@@ -434,6 +498,20 @@ function clause decode (0b001110 :
 function clause execute (Addi (RT, RA, SI)) =
   if RA == 0 then GPR[RT] := EXTS (SI) else GPR[RT] := GPR[RA] + EXTS (SI)
 
+union ast member (bit[5], bit[5], bit[5], bit, bit) Mullw
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[5]) RB :
+[OE] :
+0b011101011 :
+[Rc] as instr) =
+  Mullw (RT,RA,RB,OE,Rc)
+
+function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
+  GPR[RT] := (GPR[RA])[32 .. 63] * (GPR[RB])[32 .. 63]
+
 union ast member (bit[5], bit[5], bit[5], bit) Or
 
 function clause decode (0b011111 :
@@ -446,6 +524,23 @@ function clause decode (0b011111 :
 
 function clause execute (Or (RS, RA, RB, Rc)) = GPR[RA] := (GPR[RS] | GPR[RB])
 
+union ast member (bit[5], bit[5], bit) Extsw
+
+function clause decode (0b011111 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+0b1111011010 :
+[Rc] as instr) =
+  Extsw (RS,RA,Rc)
+
+function clause execute (Extsw (RS, RA, Rc)) =
+  {
+    s := (GPR[RS])[32];
+    (GPR[RA])[32..63] := (GPR[RS])[32 .. 63];
+    (GPR[RA])[0..31] := s ^^ 32
+  }
+
 
 end decode
 end execute
diff --git a/src/type_internal.ml b/src/type_internal.ml
index d619b2e9..7928358e 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -900,15 +900,15 @@ let initial_typ_env =
                   Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
                         (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");
                                               mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")])
-                        (* could also use 2*n instead of n+n *)
-                        (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nadd (mk_nv "n", mk_nv "n"))))),
+                           (* could also use 2*n instead of n+n *)
+                           (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nadd (mk_nv "n", mk_nv "n"))))),
                         External (Some "multiply_vec"), [],pure_e);
 
                    Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),
                          (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p");
                                                mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")])
-                        (* could also use 2*m instead of m+m *)
-                        (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))),
+                            (* could also use 2*m instead of m+m *)
+                            (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))),
                         External (Some "mult_range_vec"),
                        [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e);
                    Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]),