fixes

6 files changed, 249 insertions, 78 deletions

diff --git a/src/gen_lib/power_extras.lem b/src/gen_lib/power_extras.lem
index 2883c810..b43c6403 100644
--- a/src/gen_lib/power_extras.lem
+++ b/src/gen_lib/power_extras.lem
@@ -26,6 +26,9 @@ let rec countLeadingZeros (Interp.V_tuple v) = ((match v with
 let MEMr (addr,l) = read_memory (unsigned addr) l
 let MEMr_reserve (addr,l) = read_memory (unsigned addr) l
 
+let MEMw_EA (addr,l) = write_writeEA (unsigned addr) l
+let MEMw_EA_conditional (addr,l) = write_writeEA (unsigned addr) l
+                                        
 let MEMw (addr,l,value) = write_memory (unsigned addr) l value
 let MEMw_conditional (addr,l,value) = write_memory (unsigned addr) l value >> return true
 
@@ -41,6 +44,6 @@ let trap () = exit ()
  * as an effect *)
 
 val countLeadingZeroes : vector bit * integer -> integer
-let countLeadingZeroes (V bits _ _ ,n)  = 
+let countLeadingZeroes (Vector bits _ _ ,n)  = 
   let (_,bits) = List.splitAt (natFromInteger n) bits in
   integerFromNat (List.length (takeWhile ((=) O) bits))
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 1382fd1d..738a0b20 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,4 +1,4 @@
-open import Pervasives_extra
+open import Pervasves_extra
 open import Vector
 open import Arch
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 0f6aa5ee..3914bdef 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -23,6 +23,8 @@ let bitwise_not_bit = function
   end
 
 let (~) = bitwise_not_bit
+
+val pow : integer -> integer -> integer
 let pow m n = m ** (natFromInteger n)
 
 
@@ -496,3 +498,29 @@ let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n)
 let mask (n,Vector bits start dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
+
+
+
+
+(* this is for a temporary workaround int/nat/integer/natural issues*)
+
+class (subInteger 'a)
+  val toInteger : 'a -> integer
+end
+
+
+instance (subInteger integer)
+  let toInteger = id
+end
+
+instance (subInteger int)
+  let toInteger = integerFromInt
+end
+
+instance (subInteger nat)
+  let toInteger = integerFromNat
+end
+
+instance (subInteger natural)
+  let toInteger = integerFromNatural
+end
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8b81b83f..9a06b0ba 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -516,7 +516,6 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                         | "Barrier_DSB_ST" -> DSB_ST
                         | "Barrier_DSB_LD" -> DSB_LD
                         | "Barrier_ISB" ->    ISB
-                        | "Barrier_Sync" ->   Sync
                         end)
          | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
            (Interp.V_ctor (Id_aux (Id r) _) _ _ _) ->
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4503555a..cd0392b0 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2099,7 +2099,7 @@ let effectful (Effect_aux (eff,_)) =
        (fun (BE_aux (eff,_)) ->
          match eff with
          | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv
-         | BE_barr | BE_depend | BE_undef | BE_nondet | BE_escape -> true
+         | BE_barr | BE_depend | BE_nondet | BE_escape -> true
          | _ -> false)
        effs
 
@@ -2169,8 +2169,7 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a =
   | L_true  -> "I"
   | L_num i ->
      let ipp = string_of_int i in
-     (if i < 0 then "((0"^ipp^") )"
-      else "("^ipp^" : i)")
+     if i < 0 then "((0"^ipp^") : i)" else "("^ipp^" : i)"
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
diff --git a/src/test/power.sail b/src/test/power.sail
index b3e14b5a..6f3eeecc 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -486,6 +486,12 @@ function forall Nat 'n. (bit['n]) zero_or_undef ((bit['n]) x) = {
   out
 }
 
+(* announce write address for plain write *)
+val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA
+
+(* announce write address for write conditional *)
+val extern forall Nat 'N, 'N IN {1,2,4,8,16}. (bit[64] (*address*), [:'N:] (*size*)) -> unit effect {eamem} MEMw_EA_cond
+
 scattered function unit execute
 scattered typedef ast = const union
 
@@ -516,7 +522,7 @@ function clause decode (0b010000 :
 function clause execute (Bc (BO, BI, BD, AA, LK)) =
   {
     if mode64bit then M := 0 else M := 32;
-    ctr_temp := CTR;
+    (bit[64]) ctr_temp := CTR;
     if ~(BO[2])
     then {
       ctr_temp := ctr_temp - 1;
@@ -545,7 +551,7 @@ function clause decode (0b010011 :
 function clause execute (Bclr (BO, BI, BH, LK)) =
   {
     if mode64bit then M := 0 else M := 32;
-    ctr_temp := CTR;
+    (bit[64]) ctr_temp := CTR;
     if ~(BO[2])
     then {
       ctr_temp := ctr_temp - 1;
@@ -1136,6 +1142,7 @@ function clause execute (Stb (RS, RA, D)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(D);
+    MEMw_EA(EA,1);
     MEMw(EA,1) := (GPR[RS])[56 .. 63]
   }
 
@@ -1155,6 +1162,7 @@ function clause execute (Stbx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,1);
     MEMw(EA,1) := (GPR[RS])[56 .. 63]
   }
 
@@ -1170,6 +1178,7 @@ function clause execute (Stbu (RS, RA, D)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + EXTS(D);
+    MEMw_EA(EA,1);
     GPR[RA] := EA;
     MEMw(EA,1) := (GPR[RS])[56 .. 63]
   }
@@ -1188,6 +1197,7 @@ function clause execute (Stbux (RS, RA, RB)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + GPR[RB];
+    MEMw_EA(EA,1);
     GPR[RA] := EA;
     MEMw(EA,1) := (GPR[RS])[56 .. 63]
   }
@@ -1206,6 +1216,7 @@ function clause execute (Sth (RS, RA, D)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(D);
+    MEMw_EA(EA,2);
     MEMw(EA,2) := (GPR[RS])[48 .. 63]
   }
 
@@ -1225,6 +1236,7 @@ function clause execute (Sthx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,2);
     MEMw(EA,2) := (GPR[RS])[48 .. 63]
   }
 
@@ -1240,6 +1252,7 @@ function clause execute (Sthu (RS, RA, D)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + EXTS(D);
+    MEMw_EA(EA,2);
     GPR[RA] := EA;
     MEMw(EA,2) := (GPR[RS])[48 .. 63]
   }
@@ -1258,6 +1271,7 @@ function clause execute (Sthux (RS, RA, RB)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + GPR[RB];
+    MEMw_EA(EA,2);
     GPR[RA] := EA;
     MEMw(EA,2) := (GPR[RS])[48 .. 63]
   }
@@ -1276,6 +1290,7 @@ function clause execute (Stw (RS, RA, D)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(D);
+    MEMw_EA(EA,4);
     MEMw(EA,4) := (GPR[RS])[32 .. 63]
   }
 
@@ -1295,6 +1310,7 @@ function clause execute (Stwx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,4);
     MEMw(EA,4) := (GPR[RS])[32 .. 63]
   }
 
@@ -1310,6 +1326,7 @@ function clause execute (Stwu (RS, RA, D)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + EXTS(D);
+    MEMw_EA(EA,4);
     GPR[RA] := EA;
     MEMw(EA,4) := (GPR[RS])[32 .. 63]
   }
@@ -1328,6 +1345,7 @@ function clause execute (Stwux (RS, RA, RB)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + GPR[RB];
+    MEMw_EA(EA,4);
     GPR[RA] := EA;
     MEMw(EA,4) := (GPR[RS])[32 .. 63]
   }
@@ -1347,6 +1365,7 @@ function clause execute (Std (RS, RA, DS)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(DS : 0b00);
+    MEMw_EA(EA,8);
     MEMw(EA,8) := GPR[RS]
   }
 
@@ -1366,6 +1385,7 @@ function clause execute (Stdx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,8);
     MEMw(EA,8) := GPR[RS]
   }
 
@@ -1382,6 +1402,7 @@ function clause execute (Stdu (RS, RA, DS)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + EXTS(DS : 0b00);
+    MEMw_EA(EA,8);
     GPR[RA] := EA;
     MEMw(EA,8) := GPR[RS]
   }
@@ -1400,6 +1421,7 @@ function clause execute (Stdux (RS, RA, RB)) =
   {
     (bit[64]) EA := 0;
     EA := GPR[RA] + GPR[RB];
+    MEMw_EA(EA,8);
     GPR[RA] := EA;
     MEMw(EA,8) := GPR[RS]
   }
@@ -1445,19 +1467,14 @@ function clause execute (Stq (RSp, RA, DS)) =
   {
     (bit[64]) b := 0;
     (bit[64]) EA := 0;
-    {
-      (bit[64]) EA := 0;
-      (bit[64]) b := 0;
-      if RA == 0 then b := 0 else b := GPR[RA];
-      EA := b + EXTS(DS : 0b00);
-      (bit[128]) mem := 0;
-      mem[0..63] := GPR[RSp];
-      mem[64..127] := GPR[RSp + 1];
-      if ~(bigendianmode) then mem := byte_reverse(mem) else ();
-      MEMw(EA,16) := mem
-    };
+    if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(DS : 0b00);
-    MEMw(EA,8) := RSp
+    MEMw_EA(EA,16);
+    (bit[128]) mem := 0;
+    mem[0..63] := GPR[RSp];
+    mem[64..127] := GPR[RSp + 1];
+    if ~(bigendianmode) then mem := byte_reverse(mem) else ();
+    MEMw(EA,16) := mem
   }
 
 union ast member (bit[5], bit[5], bit[5]) Lhbrx
@@ -1497,6 +1514,7 @@ function clause execute (Sthbrx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,2);
     MEMw(EA,2) := (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55]
   }
 
@@ -1538,6 +1556,7 @@ function clause execute (Stwbrx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,4);
     MEMw(EA,4) :=
       (GPR[RS])[56 .. 63] : (GPR[RS])[48 .. 55] : (GPR[RS])[40 .. 47] : (GPR[RS])[32 .. 39]
   }
@@ -1583,6 +1602,7 @@ function clause execute (Stdbrx (RS, RA, RB)) =
     (bit[64]) EA := 0;
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + GPR[RB];
+    MEMw_EA(EA,8);
     MEMw(EA,8) :=
       (GPR[RS])[56 .. 63] :
         (GPR[RS])[48 .. 55] :
@@ -1630,6 +1650,7 @@ function clause execute (Stmw (RS, RA, D)) =
     if RA == 0 then b := 0 else b := GPR[RA];
     EA := b + EXTS(D);
     size := ([|32|]) (32 - RS) * 4;
+    MEMw_EA(EA,size);
     (bit[994]) buffer := [0 = 0,993 = 0; default=0];
     i := 0;
     foreach (r from RS to 31 by 1 in inc)
@@ -1740,6 +1761,7 @@ function clause execute (Stswi (RS, RA, NB)) =
     ([|31|]) r := 0;
     r := RS - 1;
     ([|32|]) size := if NB == 0 then 32 else NB;
+    MEMw_EA(EA,size);
     (bit[256]) membuffer := [0 = 0,255 = 0; default=0];
     j := 0;
     i := 32;
@@ -1775,6 +1797,7 @@ function clause execute (Stswx (RS, RA, RB)) =
     i := 32;
     ([|128|]) n_top := XER[57 .. 63];
     recalculate_dependency(());
+    MEMw_EA(EA,n_top);
     (bit[512]) membuffer := [0 = 0,511 = 0; default=0];
     j := 0;
     foreach (n from n_top to 1 by 1 in dec)
@@ -1829,7 +1852,7 @@ function clause execute (Add (RT, RA, RB, OE, Rc)) =
       GPR[RT] := temp;
       if Rc
       then {
-        xer_so := XER.SO;
+        (bit) xer_so := XER.SO;
         if OE & overflow then xer_so := overflow else ();
         set_overflow_cr0(temp,xer_so)
       }
@@ -1857,7 +1880,7 @@ function clause execute (Subf (RT, RA, RB, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -1930,7 +1953,7 @@ function clause execute (Addc (RT, RA, RB, OE, Rc)) =
       GPR[RT] := temp;
       if Rc
       then {
-        xer_so := XER.SO;
+        (bit) xer_so := XER.SO;
         if OE & overflow then xer_so := overflow else ();
         set_overflow_cr0(temp,xer_so)
       }
@@ -1960,7 +1983,7 @@ function clause execute (Subfc (RT, RA, RB, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -1990,7 +2013,7 @@ function clause execute (Adde (RT, RA, RB, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -2020,7 +2043,7 @@ function clause execute (Subfe (RT, RA, RB, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -2050,7 +2073,7 @@ function clause execute (Addme (RT, RA, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -2080,7 +2103,7 @@ function clause execute (Subfme (RT, RA, OE, Rc)) =
         GPR[RT] := temp;
         if Rc
         then {
-          xer_so := XER.SO;
+          (bit) xer_so := XER.SO;
           if OE & overflow then xer_so := overflow else ();
           set_overflow_cr0(temp,xer_so)
         }
@@ -2106,7 +2129,7 @@ function clause execute (Addze (RT, RA, OE, Rc)) =
       GPR[RT] := temp;
       if Rc
       then {
-        xer_so := XER.SO;
+        (bit) xer_so := XER.SO;
         if OE & overflow then xer_so := overflow else ();
         set_overflow_cr0(temp,xer_so)
       }
@@ -2132,7 +2155,7 @@ function clause execute (Subfze (RT, RA, OE, Rc)) =
       GPR[RT] := temp;
       if Rc
       then {
-        xer_so := XER.SO;
+        (bit) xer_so := XER.SO;
         if OE & overflow then xer_so := overflow else ();
         set_overflow_cr0(temp,xer_so)
       }
@@ -2191,7 +2214,7 @@ function clause execute (Mullw (RT, RA, RB, OE, Rc)) =
       GPR[RT] := prod;
       if Rc
       then {
-        xer_so := XER.SO;
+        (bit) xer_so := XER.SO;
         if OE & overflow then xer_so := overflow else ();
         set_overflow_cr0(prod,xer_so)
       }
@@ -2223,7 +2246,7 @@ function clause execute (Mulhw (RT, RA, RB, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if mode64bit
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
       else set_overflow_cr0(prod,xer_so)
@@ -2249,7 +2272,7 @@ function clause execute (Mulhwu (RT, RA, RB, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if mode64bit
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
       else set_overflow_cr0(prod,xer_so)
@@ -2283,7 +2306,7 @@ function clause execute (Divw (RT, RA, RB, OE, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if mode64bit | overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -2319,7 +2342,7 @@ function clause execute (Divwu (RT, RA, RB, OE, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if mode64bit | overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -2355,7 +2378,7 @@ function clause execute (Divwe (RT, RA, RB, OE, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if mode64bit | overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -2391,7 +2414,7 @@ function clause execute (Divweu (RT, RA, RB, OE, Rc)) =
     (GPR[RT])[0..31] := undefined;
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if mode64bit | overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -2424,7 +2447,7 @@ function clause execute (Mulld (RT, RA, RB, OE, Rc)) =
     GPR[RT] := prod[64 .. 127];
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       set_overflow_cr0(prod[64 .. 127],xer_so)
     }
@@ -2549,7 +2572,7 @@ function clause execute (Divde (RT, RA, RB, OE, Rc)) =
     if OE then set_SO_OV(overflow) else ();
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -2585,7 +2608,7 @@ function clause execute (Divdeu (RT, RA, RB, OE, Rc)) =
     if OE then set_SO_OV(overflow) else ();
     if Rc
     then {
-      xer_so := XER.SO;
+      (bit) xer_so := XER.SO;
       if OE & overflow then xer_so := overflow else ();
       if overflow
       then CR.CR0 := [undefined,undefined,undefined,xer_so]
@@ -3288,6 +3311,75 @@ function clause execute (Rlwimi (RS, RA, SH, MB, ME, Rc)) =
     if Rc then set_overflow_cr0(temp,XER.SO) else ()
   }
 
+union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldicl
+
+function clause decode (0b011110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+(bit[6]) mb :
+0b000 :
+(bit[1]) _ :
+[Rc] as instr) =
+  Some(Rldicl(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
+
+function clause execute (Rldicl (RS, RA, sh, mb, Rc)) =
+  {
+    n := [sh[5]] : sh[0 .. 4];
+    r := ROTL(GPR[RS],n);
+    b := [mb[5]] : mb[0 .. 4];
+    m := MASK(b,63);
+    (bit[64]) temp := (r & m);
+    GPR[RA] := temp;
+    if Rc then set_overflow_cr0(temp,XER.SO) else ()
+  }
+
+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) =
+  Some(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);
+    (bit[64]) temp := (r & m);
+    GPR[RA] := temp;
+    if Rc then set_overflow_cr0(temp,XER.SO) else ()
+  }
+
+union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldic
+
+function clause decode (0b011110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+(bit[6]) mb :
+0b010 :
+(bit[1]) _ :
+[Rc] as instr) =
+  Some(Rldic(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
+
+function clause execute (Rldic (RS, RA, sh, mb, Rc)) =
+  {
+    n := [sh[5]] : sh[0 .. 4];
+    r := ROTL(GPR[RS],n);
+    b := [mb[5]] : mb[0 .. 4];
+    m := MASK(b,(bit[6]) (~(n)));
+    (bit[64]) temp := (r & m);
+    GPR[RA] := temp;
+    if Rc then set_overflow_cr0(temp,XER.SO) else ()
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit[6], bit) Rldcl
 
 function clause decode (0b011110 :
@@ -3332,6 +3424,29 @@ function clause execute (Rldcr (RS, RA, RB, me, Rc)) =
     if Rc then set_overflow_cr0(temp,XER.SO) else ()
   }
 
+union ast member (bit[5], bit[5], bit[6], bit[6], bit) Rldimi
+
+function clause decode (0b011110 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+(bit[6]) mb :
+0b011 :
+(bit[1]) _ :
+[Rc] as instr) =
+  Some(Rldimi(RS,RA,instr[16 .. 20] : instr[30 .. 30],mb,Rc))
+
+function clause execute (Rldimi (RS, RA, sh, mb, Rc)) =
+  {
+    n := [sh[5]] : sh[0 .. 4];
+    r := ROTL(GPR[RS],n);
+    b := [mb[5]] : mb[0 .. 4];
+    m := MASK(b,(bit[6]) (~(n)));
+    (bit[64]) temp := (r & m | GPR[RA] & ~(m));
+    GPR[RA] := temp;
+    if Rc then set_overflow_cr0(temp,XER.SO) else ()
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit) Slw
 
 function clause decode (0b011111 :
@@ -3466,6 +3581,29 @@ function clause execute (Srd (RS, RA, RB, Rc)) =
     if Rc then set_overflow_cr0(temp,XER.SO) else ()
   }
 
+union ast member (bit[5], bit[5], bit[6], bit) Sradi
+
+function clause decode (0b011111 :
+(bit[5]) RS :
+(bit[5]) RA :
+(bit[5]) _ :
+0b110011101 :
+(bit[1]) _ :
+[Rc] as instr) =
+  Some(Sradi(RS,RA,instr[16 .. 20] : instr[30 .. 30],Rc))
+
+function clause execute (Sradi (RS, RA, sh, Rc)) =
+  {
+    n := [sh[5]] : sh[0 .. 4];
+    r := ROTL(GPR[RS],64 - n);
+    m := MASK(n,63);
+    s := (GPR[RS])[0];
+    (bit[64]) temp := (r & m | s ^^ 64 & ~(m));
+    GPR[RA] := temp;
+    if Rc then set_overflow_cr0(temp,XER.SO) else ();
+    XER.CA := if n >_u (bit[6]) 0 then s & ~((r & ~(m)) == 0) else 0
+  }
+
 union ast member (bit[5], bit[5], bit[5], bit) Srad
 
 function clause decode (0b011111 :
@@ -3716,38 +3854,6 @@ function clause execute (Mcrxr (BF)) =
     XER[32..35] := 0b0000
   }
 
-union ast member (bit[5], bit[5]) Mtdcrux
-
-function clause decode (0b011111 :
-(bit[5]) RS :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0110100011 :
-(bit[1]) _ as instr) =
-  Some(Mtdcrux(RS,RA))
-
-function clause execute (Mtdcrux (RS, RA)) =
-  {
-    DCRN := GPR[RA];
-    DCR[DCRN] := GPR[RS]
-  }
-
-union ast member (bit[5], bit[5]) Mfdcrux
-
-function clause decode (0b011111 :
-(bit[5]) RT :
-(bit[5]) RA :
-(bit[5]) _ :
-0b0100100011 :
-(bit[1]) _ as instr) =
-  Some(Mfdcrux(RT,RA))
-
-function clause execute (Mfdcrux (RT, RA)) =
-  {
-    DCRN := GPR[RA];
-    GPR[RT] := DCR[DCRN]
-  }
-
 union ast member (bit[5], bit[5], bit[5], bit) Dlmzb
 
 function clause decode (0b011111 :
@@ -4243,7 +4349,16 @@ function clause decode (0b011111 :
 0b1 as instr) =
   Some(Stbcx(RS,RA,RB))
 
-function clause execute (Stbcx (RS, RA, RB)) = ()
+function clause execute (Stbcx (RS, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    (bit[64]) EA := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    MEMw_EA_cond(EA,1);
+    status := MEMw_conditional(EA,1,(GPR[RS])[56 .. 63]);
+    CR0 := 0b00 : [status] : [XER.SO]
+  }
 
 union ast member (bit[5], bit[5], bit[5]) Sthcx
 
@@ -4255,7 +4370,16 @@ function clause decode (0b011111 :
 0b1 as instr) =
   Some(Sthcx(RS,RA,RB))
 
-function clause execute (Sthcx (RS, RA, RB)) = ()
+function clause execute (Sthcx (RS, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    (bit[64]) EA := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    MEMw_EA_cond(EA,2);
+    status := MEMw_conditional(EA,2,(GPR[RS])[48 .. 63]);
+    CR0 := 0b00 : [status] : [XER.SO]
+  }
 
 union ast member (bit[5], bit[5], bit[5]) Stwcx
 
@@ -4267,7 +4391,16 @@ function clause decode (0b011111 :
 0b1 as instr) =
   Some(Stwcx(RS,RA,RB))
 
-function clause execute (Stwcx (RS, RA, RB)) = ()
+function clause execute (Stwcx (RS, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    (bit[64]) EA := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    MEMw_EA_cond(EA,4);
+    status := MEMw_conditional(EA,4,(GPR[RS])[32 .. 63]);
+    CR0 := 0b00 : [status] : [XER.SO]
+  }
 
 union ast member (bit[5], bit[5], bit[5], bit) Ldarx
 
@@ -4298,7 +4431,16 @@ function clause decode (0b011111 :
 0b1 as instr) =
   Some(Stdcx(RS,RA,RB))
 
-function clause execute (Stdcx (RS, RA, RB)) = ()
+function clause execute (Stdcx (RS, RA, RB)) =
+  {
+    (bit[64]) b := 0;
+    (bit[64]) EA := 0;
+    if RA == 0 then b := 0 else b := GPR[RA];
+    EA := b + GPR[RB];
+    MEMw_EA_cond(EA,8);
+    status := MEMw_conditional(EA,8,GPR[RS]);
+    CR0 := 0b00 : [status] : [XER.SO]
+  }
 
 union ast member (bit[2]) Sync
 
@@ -4374,8 +4516,8 @@ val ast -> bit effect pure illegal_instructions_pred
 function bit illegal_instructions_pred ((ast) instr) = {
      switch instr {
         case (Bcctr(BO,BI,BH,LK)) -> ~(BO[2])
-        case (Lbzu(RT,RA,D)) -> (RA == 0) | (RA == RT)
-        case (Lbzux(RT,RA,_)) ->(RA == 0) | (RA == RT)
+        case (Lbzu(RT,RA,D)) -> (RA == 0) | (RA == RT) 
+        case (Lbzux(RT,RA,_)) ->(RA == 0) | (RA == RT) 
         case (Lhzu(RT,RA,D)) -> (RA == 0) | (RA == RT)
         case (Lhzux(RT,RA,RB)) -> (RA == 0) | (RA == RT)
         case (Lhau(RT,RA,D)) -> (RA == 0) | (RA == RT)