bug fixes to run test from Christopher's tests

5 files changed, 308 insertions, 31 deletions

diff --git a/src/Makefile b/src/Makefile
index 896c0bf5..647df7f8 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -34,7 +34,7 @@ power: sail interpreter
 	cd _build/test ;\
 	../../sail.native -lem_ast power.sail ;\
 	$(LEM) -ocaml -only_changed_output -lib ../lem_interp/ power.lem;\
-	env OCAMLRUNPARAM=l=10M ocamlfind ocamlopt -package num -package bitstring -package batteries -package uint -I $(LEMLIB) -I ../lem_interp/ -I ../elf_model/ -linkpkg $(LEMLIB)extract.cmxa ../pprint/src/PPrintLib.cmxa ../lem_interp/extract.cmxa elf_extract.cmxa power.ml run_power.ml -o run_power.native
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -package num -package bitstring -package batteries -package uint -I $(LEMLIB) -I ../lem_interp/ -I ../elf_model/ -linkpkg $(LEMLIB)extract.cmxa ../pprint/src/PPrintLib.cmxa ../lem_interp/extract.cmxa elf_extract.cmxa power.ml run_power.ml -o run_power.native
 	ln -fs _build/test/run_power.native run_power.native
 
 test_power: power
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 6febc709..4965deb8 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -398,30 +398,6 @@ let rec fupdate_record base updates =
 end
 
 
-val update_vector_slice : value -> value -> lmem -> lmem
-let rec update_vector_slice vector value mem = 
-  match (vector,value) with
-  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
-    foldr2 (fun vbox v mem -> match vbox with
-                                       | V_boxref n t -> update_mem mem n v end)
-      mem vs vals
-  | ((V_vector m inc vs),(V_vector_sparse n o inc2 vals d)) -> 
-    let (_,mem) = foldr (fun vbox (i,mem) ->
-                          match vbox with
-			    | V_boxref n t -> 
-			      (if inc then i+1 else i-1,
-				update_mem mem n (match List.lookup i vals with
-				  | Nothing -> d
-				  | Just v  -> v end))
-                          end) (m,mem) vs in 
-    mem
-  | ((V_vector m inc vs),v) ->
-    List.foldr (fun vbox mem -> match vbox with
-                                    | V_boxref n t -> update_mem mem n v end)
-      mem vs
-  | (V_track v1 r1, v) -> (update_vector_slice v1 value mem) 
-end
-
 val fupdate_sparse : (integer -> integer -> bool) -> list (integer*value) -> integer -> value -> list (integer*value)
 let rec fupdate_sparse compare vs n vexp =
   match vs with
@@ -444,6 +420,7 @@ let rec fupdate_vec v n vexp =
     | _ -> V_track (fupdate_vec v n vexp) r end)
   end
 
+
 val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
 let rec replace_is ls vs base start stop =
   match (ls,vs) with
@@ -451,7 +428,7 @@ let rec replace_is ls vs base start stop =
   | (ls,[]) -> ls
   | (l::ls,v::vs) -> 
     if base >= start then
-      if start >= stop then ls
+      if start >= stop then v::ls
       else v::(replace_is ls vs (base + 1) (start + 1) stop)
     else l::(replace_is ls (v::vs) (base+1) start stop)
   end
@@ -484,6 +461,35 @@ let rec fupdate_vector_slice vec replace start stop =
   | (vec, V_track vr rr) -> taint (fupdate_vector_slice vec vr start stop) rr
   end
 
+val update_vector_slice : value -> value -> integer -> integer -> lmem -> lmem
+let rec update_vector_slice vector value start stop mem = 
+  match (vector,value) with
+  | ((V_boxref n t), v) ->
+    update_mem mem n (fupdate_vector_slice (in_mem mem n) v start stop)    
+  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
+    let (V_vector m' _ vs') = slice_vector vector start stop in
+    foldr2 (fun vbox v mem -> match vbox with
+      | V_boxref n t -> update_mem mem n v end)
+      mem vs' vals
+  | ((V_vector m inc vs),(V_vector_sparse n o inc2 vals d)) -> 
+    let (V_vector m' _ vs') = slice_vector vector start stop in
+    let (_,mem) = foldr (fun vbox (i,mem) ->
+                          match vbox with
+			    | V_boxref n t -> 
+			      (if inc then i+1 else i-1,
+				update_mem mem n (match List.lookup i vals with
+				  | Nothing -> d
+				  | Just v  -> v end))
+                          end) (m,mem) vs' in 
+    mem
+  | ((V_vector m inc vs),v) ->
+    let (V_vector m' _ vs') = slice_vector vector start stop in
+    List.foldr (fun vbox mem -> match vbox with
+                                    | V_boxref n t -> update_mem mem n v end)
+      mem vs'
+  | (V_track v1 r1, v) -> (update_vector_slice v1 value start stop mem) 
+end
+
 val in_ctors : list (id * typ) -> id -> maybe typ
 let rec in_ctors ctors id =
   match ctors with
@@ -1776,10 +1782,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
       match tag with
 	| Tag_empty ->
 	  match in_lenv l_env id with
-	    | (V_boxref n t) -> 
+	    | ((V_boxref n t) as v) -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
+	      else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
 	    | V_unknown ->
 	      if is_top_level then
 		let (LMem c m) = l_mem in
@@ -1891,10 +1897,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
       match tag with
 	| Tag_empty ->
 	  match in_lenv l_env id with
-	    | V_boxref n t -> 
+	    | ((V_boxref n t) as v) -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+	      else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
 	    | V_unknown -> 	  
 	      if is_top_level 
               then begin
@@ -1992,7 +1998,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               | ((Value v,lm,le), Just lexp_builder) ->
                 (match (v,is_top_level) with
                 | (V_vector m inc vs,true) -> 
-                  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
+                  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
+		| (V_boxref _ _, true) -> 
+		  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
                 | (V_vector m inc vs,false) ->
                   ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
                 | _ -> ((Error l "Vector required",lm,le),Nothing) end)
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 8400cf36..9f807ee4 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -265,8 +265,14 @@ let rec vec_concat (V_tuple args) = match args with
   | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l true]) (*TODO, get the correct order*)
   end ;;
 
+let v_length v = match v with
+  | V_vector n d l -> V_lit (L_aux (L_num (integerFromNat (List.length l))) Unknown)
+  | V_unknown -> V_unknown
+end ;;
+
 let function_map = [
   ("ignore", ignore_sail);            
+  ("length", v_length);
   ("add", arith_op (+));
   ("add_vec", arith_op_vec (+) 1);
   ("add_vec_range", arith_op_vec_range (+) 1);
diff --git a/src/test/power.sail b/src/test/power.sail
index c1295fa8..ff0fe384 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -535,6 +535,19 @@ 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[16]) Addis
+
+function clause decode (0b001111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[16]) SI as instr) =
+  Addis (RT,RA,SI)
+
+function clause execute (Addis (RT, RA, SI)) =
+  if RA == 0
+  then GPR[RT] := EXTS (SI : 0b0000000000000000)
+  else GPR[RT] := GPR[RA] + EXTS (SI : 0b0000000000000000)
+
 union ast member (bit[5], bit[5], bit[5], bit, bit) Subf
 
 function clause decode (0b011111 :
@@ -600,6 +613,40 @@ function clause execute (Cmp (BF, L, RA, RB)) =
     CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
   }
 
+union ast member (bit[5], bit[5], bit[16]) Ori
+
+function clause decode (0b011000 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[16]) UI as instr) =
+  Ori (RS,RA,UI)
+
+function clause execute (Ori (RS, RA, UI)) =
+  GPR[RA] := (GPR[RS] | 0b000000000000000000000000000000000000000000000000 : UI)
+
+union ast member (bit[5], bit[5], bit[16]) Oris
+
+function clause decode (0b011001 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[16]) UI as instr) =
+  Oris (RS,RA,UI)
+
+function clause execute (Oris (RS, RA, UI)) =
+  GPR[RA] :=
+    (GPR[RS] | 0b00000000000000000000000000000000 : UI : 0b0000000000000000)
+
+union ast member (bit[5], bit[5], bit[16]) Xori
+
+function clause decode (0b011010 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[16]) UI as instr) =
+  Xori (RS,RA,UI)
+
+function clause execute (Xori (RS, RA, UI)) =
+  GPR[RA] := GPR[RS] ^ 0b000000000000000000000000000000000000000000000000 : UI
+
 union ast member (bit[5], bit[5], bit[5], bit) Or
 
 function clause decode (0b011111 :
@@ -629,6 +676,220 @@ function clause execute (Extsw (RS, RA, Rc)) =
     (GPR[RA])[0..31] := s ^^ 32
   }
 
+union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicr
+
+function clause decode (0b011110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+(bit[6]) me :
+0b001 :
+(bit[1]) _ :
+[Rc] as instr) =
+  Rldicr (RS,RA,instr[16 .. 20] : instr[30 .. 30],me,Rc)
+
+function clause execute (Rldicr (RS, RA, sh, me, Rc)) =
+  {
+    n := [sh[5]] : sh[0 .. 4];
+    r := ROTL (GPR[RS],n);
+    e := [me[5]] : me[0 .. 4];
+    m := MASK (0,e);
+    GPR[RA] := (r & m)
+  }
+
+union ast member (bit[5], bit[10]) Mtspr
+
+function clause decode (0b011111 :
+(bit[5]) RS :
+(bit[10]) spr :
+0b0111010011 :
+(bit[1]) _ as instr) =
+  Mtspr (RS,spr)
+
+function clause execute (Mtspr (RS, spr)) =
+  {
+    n := spr[5 .. 9] : spr[0 .. 4];
+    if n == 13
+    then trap ()
+    else if length (SPR[n]) == 64
+    then SPR[n] := GPR[RS]
+    else SPR[n] := (GPR[RS])[32 .. 63]
+  }
+
+union ast member (bit[5], bit[10]) Mfspr
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[10]) spr :
+0b0101010011 :
+(bit[1]) _ as instr) =
+  Mfspr (RT,spr)
+
+function clause execute (Mfspr (RT, spr)) =
+  {
+    n := spr[5 .. 9] : spr[0 .. 4];
+    if length (SPR[n]) == 64
+    then GPR[RT] := SPR[n]
+    else GPR[RT] := 0b00000000000000000000000000000000 : SPR[n]
+  }
+
+union ast member (bit[5], bit[8]) Mtcrf
+
+function clause decode (0b011111 :
+(bit[5]) RS :
+0b0 :
+(bit[8]) FXM :
+(bit[1]) _ :
+0b0010010000 :
+(bit[1]) _ as instr) =
+  Mtcrf (RS,FXM)
+
+function clause execute (Mtcrf (RS, FXM)) =
+  {
+    mask :=
+      (FXM[0] ^^ 4) :
+        (FXM[1] ^^ 4) :
+          (FXM[2] ^^ 4) :
+            (FXM[3] ^^ 4) :
+              (FXM[4] ^^ 4) : (FXM[5] ^^ 4) : (FXM[6] ^^ 4) : (FXM[7] ^^ 4);
+    CR :=
+      ((bit[32]) ((GPR[RS])[32 .. 63] & mask) |
+        (bit[32]) (CR & ~ ((bit[32]) mask)))
+  }
+
+union ast member (bit[5]) Mfcr
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+0b0 :
+(bit[9]) _ :
+0b0000010011 :
+(bit[1]) _ as instr) =
+  Mfcr (RT)
+
+function clause execute (Mfcr (RT)) =
+  GPR[RT] := 0b00000000000000000000000000000000 : CR
+
+union ast member (bit[5], bit[5], bit[16]) Lfd
+
+function clause decode (0b110010 :
+(bit[5]) FRT :
+(bit[5]) RA :
+(bit[16]) D as instr) =
+  Lfd (FRT,RA,D)
+
+function clause execute (Lfd (FRT, RA, D)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + EXTS (D);
+    FPR[FRT] := MEMr (EA,8)
+  }
+
+union ast member (bit[5], bit[5], bit[16]) Stfd
+
+function clause decode (0b110110 :
+(bit[5]) FRS :
+(bit[5]) RA :
+(bit[16]) D as instr) =
+  Stfd (FRS,RA,D)
+
+function clause execute (Stfd (FRS, RA, D)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + EXTS (D);
+    MEMw(EA,8) := FPR[FRS]
+  }
+
+union ast member (bit[5], bit) Mffs
+
+function clause decode (0b111111 :
+(bit[5]) FRT :
+(bit[5]) _ :
+(bit[5]) _ :
+0b1001000111 :
+[Rc] as instr) =
+  Mffs (FRT,Rc)
+
+function clause execute (Mffs (FRT, Rc)) = ()
+
+union ast member (bit[3], bit[3]) Mcrfs
+
+function clause decode (0b111111 :
+(bit[3]) BF :
+(bit[2]) _ :
+(bit[3]) BFA :
+(bit[2]) _ :
+(bit[5]) _ :
+0b0001000000 :
+(bit[1]) _ as instr) =
+  Mcrfs (BF,BFA)
+
+function clause execute (Mcrfs (BF, BFA)) = ()
+
+union ast member (bit[5], bit[5], bit[5]) Lvx
+
+function clause decode (0b011111 :
+(bit[5]) VRT :
+(bit[5]) RA :
+(bit[5]) RB :
+0b0001100111 :
+(bit[1]) _ as instr) =
+  Lvx (VRT,RA,RB)
+
+function clause execute (Lvx (VRT, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    VR[VRT] :=
+      MEMr
+        (EA & 0b1111111111111111111111111111111111111111111111111111111111110000,16)
+  }
+
+union ast member (bit[5], bit[5], bit[5]) Stvx
+
+function clause decode (0b011111 :
+(bit[5]) VRS :
+(bit[5]) RA :
+(bit[5]) RB :
+0b0011100111 :
+(bit[1]) _ as instr) =
+  Stvx (VRS,RA,RB)
+
+function clause execute (Stvx (VRS, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    MEMw(EA & 0b1111111111111111111111111111111111111111111111111111111111110000,16) :=
+      VR[VRS]
+  }
+
+union ast member (bit[5]) Mtvscr
+
+function clause decode (0b000100 :
+(bit[10]) _ :
+(bit[5]) VRB :
+0b11001000100 as instr) =
+  Mtvscr (VRB)
+
+function clause execute (Mtvscr (VRB)) = VSCR := (VR[VRB])[96 .. 127]
+
+union ast member (bit[5]) Mfvscr
+
+function clause decode (0b000100 :
+(bit[5]) VRT :
+(bit[10]) _ :
+0b11000000100 as instr) =
+  Mfvscr (VRT)
+
+function clause execute (Mfvscr (VRT)) =
+  VR[VRT] :=
+    0b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 :
+      VSCR
+
 union ast member (bit[2]) Sync
 
 function clause decode (0b011111 :
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 268a6a8f..dfb618a4 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -104,7 +104,9 @@ let init_reg () =
   List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
     (* XXX execute main() directly until we can handle the init phase *)
     init "CIA" (hex_to_big_int !mainaddr) 64;
+    init "GPR0" Big_int.zero_big_int 64;
     init "GPR1" Big_int.zero_big_int 64;
+    init "GPR2" Big_int.zero_big_int 64;
     init "GPR31" Big_int.zero_big_int 64;
     init "CTR" Big_int.zero_big_int 64;
     init "CR" Big_int.zero_big_int 32;