Iron out bugs in running new executable with branching; add new executable as well.

9 files changed, 162 insertions, 30 deletions

diff --git a/src/Makefile b/src/Makefile
index 93cad76c..896c0bf5 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;\
-	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=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
 	ln -fs _build/test/run_power.native run_power.native
 
 test_power: power
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 876685bd..b59b4144 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -38,7 +38,7 @@ end
 let extern_reg r slice = match (r,slice) with
   | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
   | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
-  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
+  | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field y x (i,i)
 end
 
 let rec extern_value mode for_mem v = match v with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c0237cbc..8400cf36 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -146,8 +146,8 @@ let to_vec ord len n =
   else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
 ;;
 
-let exts len v = match v with
-  | V_vector _ inc _  -> to_vec inc len (to_num true v)
+let exts (V_tuple[V_lit(L_aux (L_num len) _);v]) = match v with
+  | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num true v)
   | V_unknown -> V_unknown
 end
 ;;
@@ -278,6 +278,8 @@ let function_map = [
   ("minus_vec_range", arith_op_vec_range (-) 1);
   ("multiply", arith_op ( * ));
   ("multiply_vec", arith_op_vec ( * ) 2);
+  ("mult_range_vec", arith_op_range_vec ( * ) 2);
+  ("mult_vec_range", arith_op_vec_range ( * ) 2);
   ("mod", arith_op (mod));
   ("mod_vec", arith_op_vec (mod) 1);
   ("mod_vec_range", arith_op_vec_range (mod) 1);
@@ -289,7 +291,7 @@ let function_map = [
   ("is_one", is_one);
   ("to_num_inc", to_num false);
   ("to_num_dec", to_num false);
-  ("EXTS", exts 64);
+  ("EXTS", exts);
   ("to_vec_inc", to_vec_inc);
   ("to_vec_dec", to_vec_dec);
   ("bitwise_not", bitwise_not);
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index e845754d..211dd015 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -354,6 +354,7 @@ let doc_exp, doc_let =
       let opening = separate space [string "switch"; exp e; lbrace] in
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
+  | E_exit e -> separate space [string "exit"; exp e;]
   (* adding parens and loop for lower precedence *)
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index f8c05085..04b7eecc 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -137,7 +137,7 @@ let rec compact_exp (E_aux (e, l)) =
      wrap(E_field(compact_exp e, id))
  | E_assign (lexp, e) -> wrap(E_assign(lexp, compact_exp e))
  | E_block [] | E_nondet [] | E_cast (_, _) | E_internal_cast (_, _)
- | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ ->
+ | E_id _|E_lit _|E_vector_indexed (_, _)|E_record _|E_internal_exp _ | E_exit _->
      wrap e
 
 (* extract, compact and reverse expressions on the stack;
@@ -157,7 +157,7 @@ module Reg = struct
   let to_string id v = 
     sprintf "%s -> %s" id (val_to_string v)
   let find id m = 
-(*    eprintf "reg_find called with %s\n" id;*)
+(*    eprintf "reg_find called with %s\n" id; *)
     let v = find id m in
 (*    eprintf "%s -> %s\n" id (val_to_string v);*)
     v
diff --git a/src/test/hello4 b/src/test/hello4
new file mode 100755
index 00000000..962527fa
--- /dev/null
+++ b/src/test/hello4
diff --git a/src/test/power.sail b/src/test/power.sail
index bc184b67..c1295fa8 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -1,12 +1,10 @@
-val extern forall Nat 'n. bit['n] -> bit[64] effect pure EXTS
+val extern forall Nat 'm, Nat 'n. (implicit<'m>,bit['n]) -> bit['m] effect pure EXTS
 
 (* XXX binary coded decimal *)
 function forall Type 'a . 'a DEC_TO_BCD ( x ) = x
 function forall Type 'a . 'a BCD_TO_DEC ( x ) = x
 (* XXX carry out *)
 function bit carry_out ( x ) = bitzero
-(* XXX length *)
-function nat length ( x ) = 64
 (* XXX Storage control *)
 function forall Type 'a . 'a real_addr ( x ) = x
 (* XXX For stvxl and lvxl - what does that do? *)
@@ -299,27 +297,23 @@ val extern forall Nat 'n, Nat 'm. bit['n] -> bit['m] effect pure EXTZ
 val forall Nat 'n, Nat 'm, 'm <= 'n. (bit['n], [|'m|]) -> bit['m] effect pure Chop
 function forall Nat 'm. (bit['m]) Chop(x, y) = x[0..y]
 
-val forall Nat 'n, Nat 'm, Nat 'p, Nat 'q, Nat 'k, 'n <= 0, 0 <= 'm,
-  'n + 2** 'p = 0, 'm = 2** 'q, 'k = 'p + 'q.
-  (nat, [|'n|], [|'m|]) -> bit['k] effect { wreg } Clamp
+val forall Nat 'n, Nat 'm, Nat 'k, 'n <= 0, 0 <= 'm.
+  (implicit<'k>, int, [|'n|], [|'m|]) -> bit['k] effect { wreg } Clamp
 
-(*
-(*TODO: This is not the right type, Clamp needs the implicit additional parameter *)
-function forall Nat 'n, Nat 'm, Nat 'p, Nat 'q, Nat 'k, 'n <= 0, 0 <= 'm,
-  'n + 2** 'p = 0, 'm = 2** 'q, 'k = 'p + 'q. (bit['k])
-Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = {
+function forall Nat 'n, Nat 'm, Nat 'k, 'n <= 0, 0 <= 'm. (bit['k])
+Clamp((int) x, ([|'n|]) y, ([|'m|]) z) = {
   ([|'n:'m|]) result := 0;
   if (x<y) then {
     result := y;
-    VSCR.SAT := bitone;
+    VSCR.SAT := 1;
   } else if (x > z) then {
     result := z;
-    VSCR.SAT := bitone;
+    VSCR.SAT := 1;
   } else {
     result := x;
   };
   (bit['k]) result;
-}*)
+}
 
 (* XXX *)
 val extern bit[32] -> bit[32] effect pure RoundToSPIntCeil
@@ -341,6 +335,14 @@ register (bit[64]) CIA (* current instruction address *)
 
 val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw
 val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr_reserve
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> bool effect { wmem } MEMw_conditional
+
+val extern unit -> unit effect { barr } I_Sync
+val extern unit -> unit effect { barr } H_Sync (*corresponds to Sync in barrier kinds*)
+val extern unit -> unit effect { barr } LW_Sync
+val extern unit -> unit effect { barr } EIEIO_Sync
+
 
 (* XXX effect for trap? *)
 val extern unit -> unit effect pure trap
@@ -348,6 +350,19 @@ val extern unit -> unit effect pure trap
 register (bool) mode64bit
 register (bool) bigendianmode
 
+val bit[64] -> unit effect {rreg,wreg} set_overflow_cr0 
+function (unit) set_overflow_cr0(target_register) = {
+  (if mode64bit
+   then m := 0
+   else m := 32);
+  (if target_register[m..63] < 0
+  then c := 0b100
+  else if target_register[m..63] > 0 
+  then c := 0b010
+  else c := 0b001);
+  CR.CR0 := c:[XER.SO]
+}
+
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -366,7 +381,29 @@ function clause decode (0b010010 :
 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
+    if LK then LR := CIA + 4 else ()
+  }
+
+union ast member (bit[5], bit[5], bit[14], bit, bit) Bc
+
+function clause decode (0b010000 :
+(bit[5]) BO :
+(bit[5]) BI :
+(bit[14]) BD :
+[AA] :
+[LK] as instr) =
+  Bc (BO,BI,BD,AA,LK)
+
+function clause execute (Bc (BO, BI, BD, AA, LK)) =
+  {
+    if mode64bit then M := 0 else M := 32;
+    if ~ (BO[2]) then CTR := CTR - 1 else ();
+    ctr_ok := (BO[2] | (CTR[M .. 63] != 0) ^ BO[3]);
+    cond_ok := (BO[0] | CR[BI + 32] ^ ~ (BO[1]));
+    if ctr_ok & cond_ok
+    then if AA then NIA := EXTS (BD : 0b00) else NIA := CIA + EXTS (BD : 0b00)
+    else ();
+    if LK then LR := CIA + 4 else ()
   }
 
 union ast member (bit[5], bit[5], bit[2], bit) Bclr
@@ -383,11 +420,11 @@ function clause decode (0b010011 :
 function clause execute (Bclr (BO, BI, BH, LK)) =
   {
     if mode64bit then M := 0 else M := 32;
-    if ~ (BO[2]) then CTR := CTR - 1;
+    if ~ (BO[2]) then CTR := CTR - 1 else ();
     ctr_ok := (BO[2] | (CTR[M .. 63] != 0) ^ BO[3]);
     cond_ok := (BO[0] | CR[BI + 32] ^ ~ (BO[1]));
-    if ctr_ok & cond_ok then NIA := LR[0 .. 61] : 0b00;
-    if LK then LR := CIA + 4
+    if ctr_ok & cond_ok then NIA := LR[0 .. 61] : 0b00 else ();
+    if LK then LR := CIA + 4 else ()
   }
 
 union ast member (bit[5], bit[5], bit[16]) Lwz
@@ -498,6 +535,24 @@ 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) Subf
+
+function clause decode (0b011111 :
+(bit[5]) RT :
+(bit[5]) RA :
+(bit[5]) RB :
+[OE] :
+0b000101000 :
+[Rc] as instr) =
+  Subf (RT,RA,RB,OE,Rc)
+
+function clause execute (Subf (RT, RA, RB, OE, Rc)) =
+  {
+    (bit[64]) temp := ~ (GPR[RA]) + GPR[RB] + 1;
+    GPR[RT] := temp;
+    if Rc then set_overflow_cr0 (temp) else ()
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit, bit) Mullw
 
 function clause decode (0b011111 :
@@ -510,7 +565,40 @@ function clause decode (0b011111 :
   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]
+  {
+    (bit[64]) temp := (GPR[RA])[32 .. 63] * (GPR[RB])[32 .. 63];
+    GPR[RT] := temp;
+    if Rc then set_overflow_cr0 (temp) else ()
+  }
+
+union ast member (bit[3], bit, bit[5], bit[5]) Cmp
+
+function clause decode (0b011111 :
+(bit[3]) BF :
+(bit[1]) _ :
+[L] :
+(bit[5]) RA :
+(bit[5]) RB :
+0b0000000000 :
+(bit[1]) _ as instr) =
+  Cmp (BF,L,RA,RB)
+
+function clause execute (Cmp (BF, L, RA, RB)) =
+  {
+    (bit[64]) a := 0;
+    (bit[64]) b := 0;
+    if L == 0
+    then {
+      a := EXTS ((GPR[RA])[32 .. 63]);
+      b := EXTS ((GPR[RB])[32 .. 63])
+    }
+    else {
+      a := GPR[RA];
+      b := GPR[RB]
+    };
+    if a < b then c := 0b100 else if a > b then c := 0b010 else c := 0b001;
+    CR[4 * BF + 32..4 * BF + 35] := c : [XER.SO]
+  }
 
 union ast member (bit[5], bit[5], bit[5], bit) Or
 
@@ -541,16 +629,56 @@ function clause execute (Extsw (RS, RA, Rc)) =
     (GPR[RA])[0..31] := s ^^ 32
   }
 
+union ast member (bit[2]) Sync
+
+function clause decode (0b011111 :
+(bit[3]) _ :
+(bit[2]) L :
+(bit[5]) _ :
+(bit[5]) _ :
+0b1001010110 :
+(bit[1]) _ as instr) =
+  Sync (L)
+
+function clause execute (Sync (L)) =
+  switch L { case 0b00 -> { H_Sync (()) } case 0b01 -> { LW_Sync (()) } }
+
+union ast member (bit[5]) Mbar
+
+function clause decode (0b011111 :
+(bit[5]) MO :
+(bit[5]) _ :
+(bit[5]) _ :
+0b1101010110 :
+(bit[1]) _ as instr) =
+  Mbar (MO)
+
+function clause execute (Mbar (MO)) = ()
+
+
+typedef decode_failure = enumerate { no_matching_pattern; unsupported_instruction } 
+
+function clause decode _ = exit no_matching_pattern
 
 end decode
 end execute
 end ast
 
+val ast -> ast effect pure supported_instructions
+function ast supported_instructions ((ast) instr) = {
+  switch instr {
+    case (Mbar(_)) -> exit unsupported_instruction
+    case (Sync(0b10)) -> exit unsupported_instruction
+    case (Sync(0b11)) -> exit unsupported_instruction
+    case _ -> instr
+   }
+}
 
 (* fetch-decode-execute *)
 function unit fde () = {
   NIA := CIA + 4;
   instr := decode(MEMr(CIA, 4));
+  instr := supported_instructions(instr);
   execute(instr);
   CIA := NIA;
 }
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 5b570de7..56d2d051 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -92,6 +92,7 @@ let init_reg () =
     init "CTR" Big_int.zero_big_int 64;
     init "CR" Big_int.zero_big_int 32;
     init "LR" lr_init_value 64;
+    init "XER" Big_int.zero_big_int 64;
     "mode64bit", Bitvector([true],true,Big_int.zero_big_int);
   ]
 ;;
diff --git a/src/type_internal.ml b/src/type_internal.ml
index dcbfd0fd..e41a60d6 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1038,27 +1038,27 @@ let initial_typ_env =
 	      false,
      [Base(((mk_nat_params ["n"; "m"; "o";"p"]),
 	    (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
-	   External (Some "lt_vec"),
+	   External (Some "lt"),
 	   [LtEq(Specc(Parse_ast.Int("<",None)),
 	       {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nconst one})},
 	       {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e);
       Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_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")]) bit_t)),
-	   External (Some "lt"),[],pure_e);]));
+	   External (Some "lt_vec"),[],pure_e);]));
     (">",
      Overload(Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gt"),[],pure_e),
 	      false,
      [Base(((mk_nat_params ["n";"m";"o";"p"]), 
 	    (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)),
-	   External (Some "gt_vec"),
+	   External (Some "gt"),
 	   [GtEq(Specc(Parse_ast.Int(">",None)),
 		 {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},
 		 {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},{nexp=Nconst one})})],pure_e);
       Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_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")]) bit_t)), 
-	   External (Some "lt"),[],pure_e);]));
+	   External (Some "gt_vec"),[],pure_e);]));
     (*Unlikely to be the correct type; probably needs to be bit vectors*)
     ("<_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "ltu"),[],pure_e));
     (">_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),External (Some "gtu"),[],pure_e));