[semmc-ppc] Fix updateXER bug, generate PPC32 semantics for ADDOo

I also tested the semantics using the fuzzer and they pass 10k+
tests. Also, if I change the semantics slightly the tests fail, so
this is pretty convincing :)

semmc-ppc/data/32/base/ADD4Oo.sem

@@ -0,0 +1,128 @@
+;; ADDO. (XO-form, OE=1, RC=1)
+(let
+ ((false
+  (bvne #b0 #b0)))
+ ((operands
+  ((rT . 'Gprc)
+   (rB . 'Gprc)
+   (rA . 'Gprc)))
+  (in
+   ('XER 'CR rA rB 'IP))
+  (defs
+   (('CR
+    ((_ call "df.cmpImm")
+     (bvslt
+      (bvadd rA rB)
+      #x00000000)
+     (bvsgt
+      (bvadd rA rB)
+      #x00000000)
+     #b000
+     (concat
+      (bvor
+       ((_ extract 31 31)
+        'XER)
+       (ite
+        (ite
+         (andp
+          (bvslt rA #x00000000)
+          (bvslt rB #x00000000))
+         (notp
+          (bvslt
+           (bvadd rA rB)
+           #x00000000))
+         (ite
+          (andp
+           (bvsge rA #x00000000)
+           (bvsge rB #x00000000))
+          (notp
+           (bvsge
+            (bvadd rA rB)
+            #x00000000))
+          (false)))
+        #b1
+        #b0))
+      ((_ extract 30 0)
+       (concat
+        ((_ extract 31 31)
+         'XER)
+        (concat
+         (ite
+          (ite
+           (andp
+            (bvslt rA #x00000000)
+            (bvslt rB #x00000000))
+           (notp
+            (bvslt
+             (bvadd rA rB)
+             #x00000000))
+           (ite
+            (andp
+             (bvsge rA #x00000000)
+             (bvsge rB #x00000000))
+            (notp
+             (bvsge
+              (bvadd rA rB)
+              #x00000000))
+            (false)))
+          #b1
+          #b0)
+         ((_ extract 29 0)
+          'XER)))))
+     'CR))
+    ('XER
+     (concat
+      (bvor
+       ((_ extract 31 31)
+        'XER)
+       (ite
+        (ite
+         (andp
+          (bvslt rA #x00000000)
+          (bvslt rB #x00000000))
+         (notp
+          (bvslt
+           (bvadd rA rB)
+           #x00000000))
+         (ite
+          (andp
+           (bvsge rA #x00000000)
+           (bvsge rB #x00000000))
+          (notp
+           (bvsge
+            (bvadd rA rB)
+            #x00000000))
+          (false)))
+        #b1
+        #b0))
+      ((_ extract 30 0)
+       (concat
+        ((_ extract 31 31)
+         'XER)
+        (concat
+         (ite
+          (ite
+           (andp
+            (bvslt rA #x00000000)
+            (bvslt rB #x00000000))
+           (notp
+            (bvslt
+             (bvadd rA rB)
+             #x00000000))
+           (ite
+            (andp
+             (bvsge rA #x00000000)
+             (bvsge rB #x00000000))
+            (notp
+             (bvsge
+              (bvadd rA rB)
+              #x00000000))
+            (false)))
+          #b1
+          #b0)
+         ((_ extract 29 0)
+          'XER))))))
+    (rT
+     (bvadd rA rB))
+    ('IP
+     (bvadd 'IP #x00000004))))))

semmc-ppc/src/SemMC/Architecture/PPC/Base/Core.hs

@@ -390,13 +390,13 @@ updateXER xb xerExp newBit
 -- have to in order to interface with crucible/macaw.  The bit numbering in PPC
 -- is somewhat odd compared to other architectures.
 lowBits64 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-lowBits64 n = extract 63 (63 - n + 1)
+lowBits64 n = extract' 63 (63 - n + 1)
 
 lowBits32 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-lowBits32 n = extract 31 (31 - n + 1)
+lowBits32 n = extract' 31 (31 - n + 1)
 
 lowBits128 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-lowBits128 n = extract 127 (127 - n + 1)
+lowBits128 n = extract' 127 (127 - n + 1)
 
 -- | A wrapper around the two low bit extractors parameterized by bit size (it
 -- selects the appropriate extractor based on architecture size)
@@ -409,19 +409,19 @@ lowBits n e
 
 lowBits' :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
 lowBits' n e
-  | nBits >= n = extract (nBits - 1) (nBits - n) e
+  | nBits >= n = extract' (nBits - 1) (nBits - n) e
   | otherwise = error ("Unexpected small slice: " ++ show n ++ " from " ++ show e)
   where
     nBits = exprBVSize e
 
 highBits64 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-highBits64 n = extract (n - 1) 0
+highBits64 n = extract' (n - 1) 0
 
 highBits32 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-highBits32 n = extract (n - 1) 0
+highBits32 n = extract' (n - 1) 0
 
 highBits128 :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
-highBits128 n = extract (n - 1) 0
+highBits128 n = extract' (n - 1) 0
 
 highBits :: (HasCallStack, ?bitSize :: BitSize) => Int -> Expr 'TBV -> Expr 'TBV
 highBits n e
@@ -433,7 +433,7 @@ highBits n e
 -- | Take the @n@ high bits of the given value
 highBits' :: (HasCallStack) => Int -> Expr 'TBV -> Expr 'TBV
 highBits' n e
-  | exprBVSize e >= n = extract (n - 1) 0 e
+  | exprBVSize e >= n = extract' (n - 1) 0 e
   | otherwise = error ("Unexpected small slice: " ++ show n ++ " from " ++ show e)
 
 -- Uninterpreted function helpers