Merge branch 'master' of https://gitlab-ext.galois.com/macaw/macaw-semmc

.gitmodules

@@ -19,3 +19,6 @@
 [submodule "submodules/macaw"]
 	path = submodules/macaw
 	url = git@github.com:GaloisInc/macaw.git
+[submodule "submodules/s-cargot"]
+	path = submodules/s-cargot
+	url = git@github.com:aisamanra/s-cargot.git

macaw-ppc/src/Data/Macaw/PPC/Arch.hs

@@ -25,7 +25,9 @@ module Data.Macaw.PPC.Arch (
 
 import           GHC.TypeLits
 
+import           Control.Lens ( (^.) )
 import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import           Data.Parameterized.Classes ( knownRepr )
 import qualified Data.Parameterized.NatRepr as NR
 import qualified Data.Parameterized.TraversableFC as FC
 import qualified Data.Parameterized.TraversableF as TF
@@ -75,7 +77,7 @@ data PPCStmt ppc (v :: MT.Type -> *) where
   Attn :: PPCStmt ppc v
   Sync :: PPCStmt ppc v
   Isync :: PPCStmt ppc v
-  -- These are cache hints
+  -- These are data cache hints
   Dcba   :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
   Dcbf   :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
   Dcbi   :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
@@ -84,6 +86,9 @@ data PPCStmt ppc (v :: MT.Type -> *) where
   Dcbzl  :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
   Dcbt   :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 5) -> PPCStmt ppc v
   Dcbtst :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 5) -> PPCStmt ppc v
+  -- Instruction cache hints
+  Icbi :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> PPCStmt ppc v
+  Icbt :: v (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc))) -> v (MT.BVType 4) -> PPCStmt ppc v
 
 instance TF.FunctorF (PPCStmt ppc) where
   fmapF = TF.fmapFDefault
@@ -105,6 +110,8 @@ instance TF.TraversableF (PPCStmt ppc) where
       Dcbzl ea -> Dcbzl <$> go ea
       Dcbt ea th -> Dcbt <$> go ea <*> go th
       Dcbtst ea th -> Dcbtst <$> go ea <*> go th
+      Icbi ea -> Icbi <$> go ea
+      Icbt ea ct -> Icbt <$> go ea <*> go ct
 
 instance MC.IsArchStmt (PPCStmt ppc) where
   ppArchStmt pp stmt =
@@ -120,6 +127,8 @@ instance MC.IsArchStmt (PPCStmt ppc) where
       Dcbzl ea -> PP.text "ppc_dcbzl" PP.<+> pp ea
       Dcbt ea th -> PP.text "ppc_dcbt" PP.<+> pp ea PP.<+> pp th
       Dcbtst ea th -> PP.text "ppc_dcbtst" PP.<+> pp ea PP.<+> pp th
+      Icbi ea -> PP.text "ppc_icbi" PP.<+> pp ea
+      Icbt ea ct -> PP.text "ppc_icbt" PP.<+> pp ea PP.<+> pp ct
 
 type instance MC.ArchStmt PPC64.PPC = PPCStmt PPC64.PPC
 type instance MC.ArchStmt PPC32.PPC = PPCStmt PPC32.PPC
@@ -144,39 +153,43 @@ data PPCPrimFn ppc f tp where
        -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
        -> f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
        -> PPCPrimFn ppc f (MT.BVType (MC.RegAddrWidth (MC.ArchReg ppc)))
+
   FPIsQNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
   FPIsSNaN :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPAdd :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
-  FPAddRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPSub :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
-  FPSubRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPMul :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
-  FPMulRoundedUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPDiv :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
-  FPLt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
-  FPEq :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f MT.BoolType
   FPCvt :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f (MT.FloatType flt')
-  FPCvtRoundsUp :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> !(MT.FloatInfoRepr flt') -> PPCPrimFn ppc f MT.BoolType
+
-  FPFromBV :: !(f (MT.BVType n)) -> !(MT.FloatInfoRepr flt) -> PPCPrimFn ppc f (MT.FloatType flt)
+  -- | Uninterpreted floating point functions
-  TruncFPToSignedBV :: (1 <= n) => MT.FloatInfoRepr flt -> f (MT.FloatType flt) -> NR.NatRepr n -> PPCPrimFn ppc f (MT.BVType n)
+  FP1 :: !String -- ^ the name of the function
-  FPAbs :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
+      -> !(f (MT.BVType 128)) -- ^ arg 1
-  FPNeg :: !(MT.FloatInfoRepr flt) -> !(f (MT.FloatType flt)) -> PPCPrimFn ppc f (MT.FloatType flt)
+      -> !(f (MT.BVType 32)) -- ^ current fpscr
+      -> PPCPrimFn ppc f (MT.BVType 160)
+  FP2 :: !String
+      -> !(f (MT.BVType 128))
+      -> !(f (MT.BVType 128))
+      -> !(f (MT.BVType 32))
+      -> PPCPrimFn ppc f (MT.BVType 160)
+  FP3 :: !String
+      -> !(f (MT.BVType 128))
+      -> !(f (MT.BVType 128))
+      -> !(f (MT.BVType 128))
+      -> !(f (MT.BVType 32))
+      -> PPCPrimFn ppc f (MT.BVType 160)
 
   -- | Uninterpreted vector functions
-  Vec1 :: String -- ^ the name of the function
+  Vec1 :: !String -- ^ the name of the function
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 32)
+       -> !(f (MT.BVType 32))
        -> PPCPrimFn ppc f (MT.BVType 160)
   Vec2 :: String -- ^ the name of the function
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 32)
+       -> !(f (MT.BVType 32))
        -> PPCPrimFn ppc f (MT.BVType 160)
   Vec3 :: String -- ^ the name of the function
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 128)
+       -> !(f (MT.BVType 128))
-       -> f (MT.BVType 32)
+       -> !(f (MT.BVType 32))
        -> PPCPrimFn ppc f (MT.BVType 160)
 
 instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (MC.Value ppc ids)) MT.TypeRepr where
@@ -187,23 +200,12 @@ instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => MT.HasRepr (PPCPrimFn ppc (M
 
       FPIsQNaN _ _ -> MT.BoolTypeRepr
       FPIsSNaN _ _ -> MT.BoolTypeRepr
-      FPAdd rep _ _ -> MT.floatTypeRepr rep
-      FPAddRoundedUp _ _ _ -> MT.BoolTypeRepr
-      FPSub rep _ _ -> MT.floatTypeRepr rep
-      FPSubRoundedUp _ _ _ -> MT.BoolTypeRepr
-      FPMul rep _ _ -> MT.floatTypeRepr rep
-      FPMulRoundedUp _ _ _ -> MT.BoolTypeRepr
-      FPDiv rep _ _ -> MT.floatTypeRepr rep
-      FPLt _ _ _ -> MT.BoolTypeRepr
-      FPEq _ _ _ -> MT.BoolTypeRepr
       FPCvt _ _ rep -> MT.floatTypeRepr rep
-      FPCvtRoundsUp _ _ _ -> MT.BoolTypeRepr
-      FPFromBV _ rep -> MT.floatTypeRepr rep
-      TruncFPToSignedBV _ _ rep -> MT.BVTypeRepr rep
-      FPAbs rep _ -> MT.floatTypeRepr rep
-      FPNeg rep _ -> MT.floatTypeRepr rep
 
-      -- FIXME: Is this right?
+      FP1 _    _ _      -> MT.BVTypeRepr MT.knownNat
+      FP2 _    _ _ _    -> MT.BVTypeRepr MT.knownNat
+      FP3 _    _ _ _ _  -> MT.BVTypeRepr MT.knownNat
+
       Vec1 _   _ _      -> MT.BVTypeRepr MT.knownNat
       Vec2 _   _ _ _    -> MT.BVTypeRepr MT.knownNat
       Vec3 _   _ _ _ _  -> MT.BVTypeRepr MT.knownNat
@@ -218,21 +220,10 @@ ppcPrimFnHasSideEffects pf =
     SDiv {} -> False
     FPIsQNaN {} -> False
     FPIsSNaN {} -> False
-    FPAdd {} -> False
-    FPAddRoundedUp {} -> False
-    FPSub {} -> False
-    FPSubRoundedUp {} -> False
-    FPMul {} -> False
-    FPMulRoundedUp {} -> False
-    FPDiv {} -> False
-    FPLt {} -> False
-    FPEq {} -> False
     FPCvt {} -> False
-    FPCvtRoundsUp {} -> False
+    FP1 {} -> False
-    FPFromBV {} -> False
+    FP2 {} -> False
-    TruncFPToSignedBV {} -> False
+    FP3 {} -> False
-    FPAbs {} -> False
-    FPNeg {} -> False
     Vec1 {} -> False
     Vec2 {} -> False
     Vec3 {} -> False
@@ -254,51 +245,18 @@ rewritePrimFn f =
     FPIsSNaN info v -> do
       tgt <- FPIsSNaN info <$> rewriteValue v
       evalRewrittenArchFn tgt
-    FPAdd rep v1 v2 -> do
-      tgt <- FPAdd rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPAddRoundedUp rep v1 v2 -> do
-      tgt <- FPAddRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPSub rep v1 v2 -> do
-      tgt <- FPSub rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPSubRoundedUp rep v1 v2 -> do
-      tgt <- FPSubRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPMul rep v1 v2 -> do
-      tgt <- FPMul rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPMulRoundedUp rep v1 v2 -> do
-      tgt <- FPMulRoundedUp rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPDiv rep v1 v2 -> do
-      tgt <- FPDiv rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPLt rep v1 v2 -> do
-      tgt <- FPLt rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
-    FPEq rep v1 v2 -> do
-      tgt <- FPEq rep <$> rewriteValue v1 <*> rewriteValue v2
-      evalRewrittenArchFn tgt
     FPCvt rep1 v rep2 -> do
       tgt <- FPCvt rep1 <$> rewriteValue v <*> pure rep2
       evalRewrittenArchFn tgt
-    FPCvtRoundsUp rep1 v rep2 -> do
+    FP1 name op fpscr -> do
-      tgt <- FPCvtRoundsUp rep1 <$> rewriteValue v <*> pure rep2
+      tgtFn <- FP1 name <$> rewriteValue op <*> rewriteValue fpscr
-      evalRewrittenArchFn tgt
+      evalRewrittenArchFn tgtFn
-    FPFromBV bv rep -> do
+    FP2 name op1 op2 fpscr -> do
-      tgt <- FPFromBV <$> rewriteValue bv <*> pure rep
+      tgtFn <- FP2 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue fpscr
-      evalRewrittenArchFn tgt
+      evalRewrittenArchFn tgtFn
-    TruncFPToSignedBV info v rep -> do
+    FP3 name op1 op2 op3 fpscr -> do
-      tgt <- TruncFPToSignedBV info <$> rewriteValue v <*> pure rep
+      tgtFn <- FP3 name <$> rewriteValue op1 <*> rewriteValue op2 <*> rewriteValue op3 <*> rewriteValue fpscr
-      evalRewrittenArchFn tgt
+      evalRewrittenArchFn tgtFn
-    FPAbs rep v -> do
-      tgt <- FPAbs rep <$> rewriteValue v
-      evalRewrittenArchFn tgt
-    FPNeg rep v -> do
-      tgt <- FPNeg rep <$> rewriteValue v
-      evalRewrittenArchFn tgt
     Vec1 name op vscr -> do
       tgtFn <- Vec1 name <$> rewriteValue op <*> rewriteValue vscr
       evalRewrittenArchFn tgtFn
@@ -316,21 +274,10 @@ ppPrimFn pp f =
     SDiv _ lhs rhs -> ppBinary "ppc_sdiv" <$> pp lhs <*> pp rhs
     FPIsQNaN _info v -> ppUnary "ppc_fp_isqnan" <$> pp v
     FPIsSNaN _info v -> ppUnary "ppc_fp_issnan" <$> pp v
-    FPAdd _rep v1 v2 -> ppBinary "ppc_fp_add" <$> pp v1 <*> pp v2
-    FPAddRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_add_roundedup" <$> pp v1 <*> pp v2
-    FPSub _rep v1 v2 -> ppBinary "ppc_fp_sub" <$> pp v1 <*> pp v2
-    FPSubRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_sub_roundedup" <$> pp v1 <*> pp v2
-    FPMul _rep v1 v2 -> ppBinary "ppc_fp_mul" <$> pp v1 <*> pp v2
-    FPMulRoundedUp _rep v1 v2 -> ppBinary "ppc_fp_mul_roundedup" <$> pp v1 <*> pp v2
-    FPDiv _rep v1 v2 -> ppBinary "ppc_fp_div" <$> pp v1 <*> pp v2
-    FPLt _rep v1 v2 -> ppBinary "ppc_fp_lt" <$> pp v1 <*> pp v2
-    FPEq _rep v1 v2 -> ppBinary "ppc_fp_eq" <$> pp v1 <*> pp v2
     FPCvt _rep1 v _rep2 -> ppUnary "ppc_fp_cvt" <$> pp v
-    FPCvtRoundsUp _rep1 v _rep2 -> ppUnary "ppc_fp_cvt_roundedup" <$> pp v
+    FP1 n r1 fpscr -> ppBinary ("ppc_fp1 " ++ n) <$> pp r1 <*> pp fpscr
-    FPFromBV bv _rep -> ppUnary "ppc_fp_frombv" <$> pp bv
+    FP2 n r1 r2 fpscr -> pp3 ("ppc_fp2 " ++ n) <$> pp r1 <*> pp r2 <*> pp fpscr
-    TruncFPToSignedBV _info v _rep -> ppUnary "ppc_fp_trunc_to_signed_bv" <$> pp v
+    FP3 n r1 r2 r3 fpscr -> pp4 ("ppc_fp3 " ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp fpscr
-    FPAbs _rep v -> ppUnary "ppc_fp_abs" <$> pp v
-    FPNeg _rep v -> ppUnary "ppc_fp_neg" <$> pp v
     Vec1 n r1 vscr -> ppBinary ("ppc_vec1 " ++ n) <$> pp r1 <*> pp vscr
     Vec2 n r1 r2 vscr -> pp3 ("ppc_vec2" ++ n) <$> pp r1 <*> pp r2 <*> pp vscr
     Vec3 n r1 r2 r3 vscr -> pp4 ("ppc_vec3" ++ n) <$> pp r1 <*> pp r2 <*> pp r3 <*> pp vscr
@@ -356,21 +303,10 @@ instance FC.TraversableFC (PPCPrimFn ppc) where
       SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
       FPIsQNaN info v -> FPIsQNaN info <$> go v
       FPIsSNaN info v -> FPIsSNaN info <$> go v
-      FPAdd rep v1 v2 -> FPAdd rep <$> go v1 <*> go v2
-      FPAddRoundedUp rep v1 v2 -> FPAddRoundedUp rep <$> go v1 <*> go v2
-      FPSub rep v1 v2 -> FPSub rep <$> go v1 <*> go v2
-      FPSubRoundedUp rep v1 v2 -> FPSubRoundedUp rep <$> go v1 <*> go v2
-      FPMul rep v1 v2 -> FPMul rep <$> go v1 <*> go v2
-      FPMulRoundedUp rep v1 v2 -> FPMulRoundedUp rep <$> go v1 <*> go v2
-      FPDiv rep v1 v2 -> FPDiv rep <$> go v1 <*> go v2
-      FPLt rep v1 v2 -> FPLt rep <$> go v1 <*> go v2
-      FPEq rep v1 v2 -> FPEq rep <$> go v1 <*> go v2
       FPCvt rep1 v rep2 -> FPCvt rep1 <$> go v <*> pure rep2
-      FPCvtRoundsUp rep1 v rep2 -> FPCvtRoundsUp rep1 <$> go v <*> pure rep2
+      FP1 name op fpscr -> FP1 name <$> go op <*> go fpscr
-      FPFromBV bv rep -> FPFromBV <$> go bv <*> pure rep
+      FP2 name op1 op2 fpscr -> FP2 name <$> go op1 <*> go op2 <*> go fpscr
-      TruncFPToSignedBV info v rep -> TruncFPToSignedBV info <$> go v <*> pure rep
+      FP3 name op1 op2 op3 fpscr -> FP3 name <$> go op1 <*> go op2 <*> go op3 <*> go fpscr
-      FPAbs rep v -> FPAbs rep <$> go v
-      FPNeg rep v -> FPNeg rep <$> go v
       Vec1 name op vscr -> Vec1 name <$> go op <*> go vscr
       Vec2 name op1 op2 vscr -> Vec2 name <$> go op1 <*> go op2 <*> go vscr
       Vec3 name op1 op2 op3 vscr -> Vec3 name <$> go op1 <*> go op2 <*> go op3 <*> go vscr
@@ -404,60 +340,100 @@ memrrToEffectiveAddress memrr = do
   b <- G.addExpr (G.AppExpr (MC.Mux (MT.BVTypeRepr repr) isr0 zero base))
   G.addExpr (G.AppExpr (MC.BVAdd repr b offset))
 
+-- | A helper to increment the IP by 4, meant to be used to implement
+-- arch-specific statements that need to update the IP (i.e., all but syscalls).
+incrementIP :: (PPCArchConstraints ppc) => G.Generator ppc ids s ()
+incrementIP = do
+  rs <- G.getRegs
+  let ipVal = rs ^. MC.boundValue PPC_IP
+  e <- G.addExpr (G.AppExpr (MC.BVAdd knownRepr ipVal (MC.BVValue knownRepr 0x4)))
+  G.setRegVal PPC_IP e
+
 -- | Manually-provided semantics for instructions whose full semantics cannot be
 -- expressed in our semantics format.
 --
 -- This includes instructions with special side effects that we don't have a way
 -- to talk about in the semantics; especially useful for architecture-specific
 -- terminator statements.
+--
+-- NOTE: For SC and TRAP (which we treat as system calls), we don't need to
+-- update the IP here, as the update is handled in the abstract interpretation
+-- of system calls in 'postPPCTermStmtAbsState'.
 ppcInstructionMatcher :: (PPCArchConstraints ppc) => D.Instruction -> Maybe (G.Generator ppc ids s ())
 ppcInstructionMatcher (D.Instruction opc operands) =
   case opc of
-    D.SC -> Just (G.finishWithTerminator (MC.ArchTermStmt PPCSyscall))
+    D.SC -> Just $ G.finishWithTerminator (MC.ArchTermStmt PPCSyscall)
-    D.TRAP -> Just (G.finishWithTerminator (MC.ArchTermStmt PPCTrap))
+    D.TRAP -> Just $ G.finishWithTerminator (MC.ArchTermStmt PPCTrap)
-    D.ATTN -> Just (G.addStmt (MC.ExecArchStmt Attn))
+    D.ATTN -> Just $ do
-    D.SYNC -> Just (G.addStmt (MC.ExecArchStmt Sync))
+      incrementIP
-    D.ISYNC -> Just (G.addStmt (MC.ExecArchStmt Isync))
+      G.addStmt (MC.ExecArchStmt Attn)
+    D.SYNC -> Just $ do
+      incrementIP
+      G.addStmt (MC.ExecArchStmt Sync)
+    D.ISYNC -> Just $ do
+      incrementIP
+      G.addStmt (MC.ExecArchStmt Isync)
     D.DCBA ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcba ea))
     D.DCBF ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcbf ea))
     D.DCBI ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcbi ea))
     D.DCBST ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcbst ea))
     D.DCBZ ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcbz ea))
     D.DCBZL ->
       case operands of
         D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           G.addStmt (MC.ExecArchStmt (Dcbzl ea))
     D.DCBT ->
       case operands of
         D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           th <- O.extractValue imm
           G.addStmt (MC.ExecArchStmt (Dcbt ea th))
     D.DCBTST ->
       case operands of
         D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do
+          incrementIP
           ea <- memrrToEffectiveAddress memrr
           th <- O.extractValue imm
           G.addStmt (MC.ExecArchStmt (Dcbtst ea th))
+    D.ICBI ->
+      case operands of
+        D.Memrr memrr D.:< D.Nil -> Just $ do
+          incrementIP
+          ea <- memrrToEffectiveAddress memrr
+          G.addStmt (MC.ExecArchStmt (Icbi ea))
+    D.ICBT ->
+      case operands of
+        D.Memrr memrr D.:< D.U4imm imm D.:< D.Nil -> Just $ do
+          incrementIP
+          ea <- memrrToEffectiveAddress memrr
+          ct <- O.extractValue imm
+          G.addStmt (MC.ExecArchStmt (Icbt ea ct))
     _ -> Nothing

macaw-ppc/src/Data/Macaw/PPC/Eval.hs

@@ -100,21 +100,10 @@ absEvalArchFn _ _r f =
     UDiv {} -> MA.TopV
     FPIsQNaN {} -> MA.TopV
     FPIsSNaN {} -> MA.TopV
-    FPAdd {} -> MA.TopV
-    FPAddRoundedUp {} -> MA.TopV
-    FPSub {} -> MA.TopV
-    FPSubRoundedUp {} -> MA.TopV
-    FPMul {} -> MA.TopV
-    FPMulRoundedUp {} -> MA.TopV
-    FPDiv {} -> MA.TopV
-    FPLt {} -> MA.TopV
-    FPEq {} -> MA.TopV
     FPCvt {} -> MA.TopV
-    FPCvtRoundsUp {} -> MA.TopV
+    FP1 {} -> MA.TopV
-    FPFromBV {} -> MA.TopV
+    FP2 {} -> MA.TopV
-    TruncFPToSignedBV {} -> MA.TopV
+    FP3 {} -> MA.TopV
-    FPAbs {} -> MA.TopV
-    FPNeg {} -> MA.TopV
     Vec1 {} -> MA.TopV
     Vec2 {} -> MA.TopV
     Vec3 {} -> MA.TopV

macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs

@@ -61,6 +61,39 @@ ppcNonceAppEval bvi nonceApp =
     S.FnApp symFn args -> do
       let fnName = symFnName symFn
       case fnName of
+        "ppc_fp1" -> return $ do
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some fpscr] -> do
+              case getOpName op of
+                Just name -> do
+                  valA <- addEltTH bvi frA
+                  valFpscr <- addEltTH bvi fpscr
+                  liftQ [| addArchExpr $ FP1 $(lift name) $(return valA) $(return valFpscr) |]
+                Nothing -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
+            _ -> fail $ "Invalid argument list for ppc.fp1: " ++ showF args
+        "ppc_fp2" -> return $ do
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some frB, Some fpscr] -> do
+              case getOpName op of
+                Just name -> do
+                  valA <- addEltTH bvi frA
+                  valB <- addEltTH bvi frB
+                  valFpscr <- addEltTH bvi fpscr
+                  liftQ [| addArchExpr $ FP2 $(lift name) $(return valA) $(return valB) $(return valFpscr) |]
+                Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
+            _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
+        "ppc_fp3" -> return $ do
+          case FC.toListFC Some args of
+            [Some op, Some frA, Some frB, Some frC, Some fpscr] -> do
+              case getOpName op of
+                Just name -> do
+                  valA <- addEltTH bvi frA
+                  valB <- addEltTH bvi frB
+                  valC <- addEltTH bvi frC
+                  valFpscr <- addEltTH bvi fpscr
+                  liftQ [| addArchExpr $ FP3 $(lift name) $(return valA) $(return valB) $(return valC) $(return valFpscr) |]
+                Nothing -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
+            _ -> fail $ "Invalid argument list for ppc.fp2: " ++ showF args
         "ppc_vec1" -> return $ do
           case FC.toListFC Some args of
             [Some op, Some rA, Some vscr] -> do
@@ -70,7 +103,7 @@ ppcNonceAppEval bvi nonceApp =
                   valVscr <- addEltTH bvi vscr
                   liftQ [| addArchExpr $ Vec1 $(lift name) $(return valA) $(return valVscr) |]
                 Nothing -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
-            _ -> fail $ "Invalid argument list for ppc.vec2: " ++ showF args
+            _ -> fail $ "Invalid argument list for ppc.vec1: " ++ showF args
         "ppc_vec2" -> return $ do
           case FC.toListFC Some args of
             [Some op, Some rA, Some rB, Some vscr] -> do
@@ -160,18 +193,6 @@ floatingPointTH bvi fnName args =
         "single_to_double" -> do
           fpval <- addEltTH bvi a
           liftQ [| addArchExpr (FPCvt M.SingleFloatRepr $(return fpval) M.DoubleFloatRepr) |]
-        "abs" -> do
-          -- Note that fabs is only defined for doubles; the operation is the
-          -- same for single and double precision on PPC, so there is only a
-          -- single instruction.
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPAbs M.DoubleFloatRepr $(return fpval)) |]
-        "negate64" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPNeg M.DoubleFloatRepr $(return fpval)) |]
-        "negate32" -> do
-          fpval <- addEltTH bvi a
-          liftQ [| addArchExpr (FPNeg M.SingleFloatRepr $(return fpval)) |]
         "is_qnan32" -> do
           fpval <- addEltTH bvi a
           liftQ [| addArchExpr (FPIsQNaN M.SingleFloatRepr $(return fpval)) |]
@@ -187,63 +208,9 @@ floatingPointTH bvi fnName args =
         _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
     [Some a, Some b] ->
       case fnName of
-        "add64" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPAdd M.DoubleFloatRepr $(return valA) $(return valB)) |]
-        "add32" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPAdd M.SingleFloatRepr $(return valA) $(return valB)) |]
-        "sub64" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPSub M.DoubleFloatRepr $(return valA) $(return valB)) |]
-        "sub32" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPSub M.SingleFloatRepr $(return valA) $(return valB)) |]
-        "mul64" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valB)) |]
-        "mul32" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valB)) |]
-        "div64" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPDiv M.DoubleFloatRepr $(return valA) $(return valB)) |]
-        "div32" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          liftQ [| addArchExpr (FPDiv M.SingleFloatRepr $(return valA) $(return valB)) |]
-        "lt" -> do
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          -- All comparisons are done as 64-bit comparisons in PPC
-          liftQ [| addArchExpr (FPLt M.DoubleFloatRepr $(return valA) $(return valB)) |]
         _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
     [Some a, Some b, Some c] ->
       case fnName of
-        "muladd64" -> do
-          -- FIXME: This is very wrong - we need a separate constructor for it
-          -- a * c + b
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          valC <- addEltTH bvi c
-          liftQ [| do prodVal <- addArchExpr (FPMul M.DoubleFloatRepr $(return valA) $(return valC))
-                      addArchExpr (FPAdd M.DoubleFloatRepr prodVal $(return valB))
-                 |]
-        "muladd32" -> do
-          -- a * c + b
-          valA <- addEltTH bvi a
-          valB <- addEltTH bvi b
-          valC <- addEltTH bvi c
-          liftQ [| do prodVal <- addArchExpr (FPMul M.SingleFloatRepr $(return valA) $(return valC))
-                      addArchExpr (FPAdd M.SingleFloatRepr prodVal $(return valB))
-                 |]
         _ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName)
     _ -> fail ("Unsupported floating point intrinsic: " ++ fnName)
 

macaw-ppc/tests/PPC64InstructionCoverage.hs

@@ -38,7 +38,7 @@ testMacaw elf =
     let otherEntryAddrs :: [MM.MemAddr 64]
         otherEntryAddrs = E.tocEntryAddrsForElf (Proxy @PPC64.PPC) elf
     let otherEntries = mapMaybe (MM.asSegmentOff mem) otherEntryAddrs
-    let di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap (entryPoint:otherEntries) []
+    let di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem M.empty (entryPoint:otherEntries) []
     let allFoundBlockAddrs :: S.Set Word64
         allFoundBlockAddrs =
           S.fromList [ fromIntegral (fromJust (MM.asAbsoluteAddr (MM.relativeSegmentAddr (MD.pblockAddr pbr))))

macaw-ppc/tests/PPC64Tests.hs

@@ -82,7 +82,7 @@ testDiscovery expectedFilename elf =
         otherEntryAddrs :: [MM.MemAddr 64]
         otherEntryAddrs = E.tocEntryAddrsForElf (Proxy @PPC64.PPC) elf
         otherEntries = mapMaybe (MM.asSegmentOff mem) otherEntryAddrs
-        di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem MD.emptySymbolAddrMap (entryPoint:otherEntries) []
+        di = MD.cfgFromAddrs (RO.ppc64_linux_info tocBase) mem M.empty (entryPoint:otherEntries) []
     expectedString <- readFile expectedFilename
     case readMaybe expectedString of
       -- Above: Read in the ExpectedResult from the contents of the file

stack.yaml

@@ -3,20 +3,26 @@ flags:
     old-locale: false
 packages:
 - macaw-semmc/
+- macaw-arm/
 - macaw-ppc/
 - submodules/semmc/semmc
 - submodules/semmc/semmc-ppc
+- submodules/semmc/semmc-arm
 - submodules/dismantle/dismantle-tablegen
 - submodules/dismantle/dismantle-ppc
+- submodules/dismantle/dismantle-arm
+- submodules/dismantle/dismantle-thumb
 - submodules/macaw/base
 - submodules/parameterized-utils
 - submodules/crucible/crucible
 - submodules/crucible/galois-matlab
 - submodules/dwarf
 - submodules/elf-edit
+- submodules/s-cargot
 extra-deps:
+- BoundedChan-1.0.3.0
 - IntervalMap-0.5.2.0
-- Cabal-2.0.0.2
+- Only-0.1
 - QuickCheck-2.10.0.1
 - StateVar-1.1.0.4
 - adjunctions-4.3
@@ -24,10 +30,11 @@ extra-deps:
 - ansi-wl-pprint-0.6.8.1
 - async-2.1.1.1
 - attoparsec-0.13.2.0
+- auto-update-0.1.4
 - base-compat-0.9.3
 - base-orphans-0.6
+- base16-bytestring-0.1.1.6
 - bifunctors-5.4.2
-- binary-0.8.5.1
 - bimap-0.3.3
 - blaze-builder-0.4.0.2
 - blaze-textual-0.2.1.0
@@ -35,18 +42,22 @@ extra-deps:
 - cabal-doctest-1.0.2
 - call-stack-0.1.0
 - case-insensitive-1.2.0.10
+- cereal-0.5.4.0
 - clock-0.7.2
 - comonad-5.0.2
+- conduit-1.2.12.1
+- conduit-extra-1.1.17
 - constraints-0.9.1
-- containers-0.5.10.2
 - contravariant-1.4
 - direct-sqlite-2.3.21
 - distributive-0.5.3
+- easy-file-0.2.1
 - exceptions-0.8.3
 - fail-4.9.0.0
+- fast-logger-2.4.10
 - fgl-5.6.0.0
 - filemanip-0.3.6.3
-- fingertree-0.1.1.0
+- finite-typelits-0.1.3.0
 - free-4.12.4
 - generic-deriving-1.11.2
 - hashable-1.2.6.1
@@ -55,14 +66,19 @@ extra-deps:
 - io-streams-1.4.1.0
 - kan-extensions-5.0.2
 - lens-4.15.4
+- lifted-base-0.2.3.11
 - located-base-0.1.1.1
 - math-functions-0.2.1.0
 - megaparsec-6.1.1
+- mmorph-1.1.0
+- monad-control-1.0.2.2
 - monad-logger-0.3.25.1
+- monad-loops-0.4.3
 - mtl-2.2.1
 - mwc-random-0.13.6.0
 - network-2.6.3.2
-- Only-0.1
+- old-locale-1.0.0.7
+- old-time-1.1.0.3
 - optparse-applicative-0.14.0.0
 - parallel-3.2.1.1
 - parsec-3.1.11
@@ -77,60 +93,40 @@ extra-deps:
 - regex-tdfa-1.2.2
 - regex-tdfa-text-1.0.0.3
 - resourcet-1.1.9
-- s-cargot-0.1.2.0
+# - s-cargot-0.1.2.0
 - scientific-0.3.5.1
 - semigroupoids-5.2.1
 - semigroups-0.18.3
-- smtLib-1.0.8
 - split-0.2.3.2
 - sqlite-simple-0.4.14.0
 - stm-2.4.4.1
+- stm-chans-3.0.0.4
+- streaming-commons-0.1.18
 - tagged-0.8.5
 - tasty-0.11.2.5
 - tasty-ant-xml-1.1.0
 - tasty-expected-failure-0.11.0.4
-- tasty-hunit-0.9.2
+- tasty-hunit-0.10.0.1
 - tasty-quickcheck-0.8.4
 - temporary-1.2.1.1
 - text-1.2.2.2
 - tf-random-0.5
 - th-abstraction-0.2.5.0
 - time-locale-compat-0.1.1.3
+- transformers-base-0.4.4
 - transformers-compat-0.5.1.4
 - unbounded-delays-0.1.1.0
 - unix-compat-0.4.3.1
+- unix-time-0.3.7
 - unliftio-0.1.0.0
 - unliftio-core-0.1.0.0
 - unordered-containers-0.2.8.0
 - utf8-string-1.0.1.1
 - vector-0.12.0.1
+- vector-sized-0.6.1.0
 - vector-th-unbox-0.2.1.6
 - void-0.7.2
 - xml-1.3.14
 - zlib-0.6.1.2
 - zlib-bindings-0.1.1.5
-
-- conduit-1.2.12.1
-- conduit-extra-1.1.17
-- fast-logger-2.4.10
-- lifted-base-0.2.3.11
-- mmorph-1.1.0
-- monad-control-1.0.2.2
-- monad-loops-0.4.3
-- old-locale-1.0.0.7
-- stm-chans-3.0.0.4
-- transformers-base-0.4.4
-
-- auto-update-0.1.4
-- easy-file-0.2.1
-- streaming-commons-0.1.18
-- unix-time-0.3.7
-
-- old-time-1.1.0.3
-
-- base16-bytestring-0.1.1.6
-- cereal-0.5.4.0
-
-
-
 resolver: ghc-8.2.1

submodules/crucible

@@ -1 +1 @@
-Subproject commit 1f580c71e05efbcd79828430234964829edebab5
+Subproject commit 256e47fab36245dd9ad3d987edc165bf3d4a4766

submodules/dismantle

@@ -1 +1 @@
-Subproject commit 183e26883166a865e3d07de881a6971ba25c5cf8
+Subproject commit 5934a45ffc1f84843482d5b5d6ff3ffab258b732

submodules/macaw

@@ -1 +1 @@
-Subproject commit eebc94cbe808e3b0ecfb036990a242b33a13658b
+Subproject commit 278b079a4963fa9ad70905a55fa07b6935b48788

submodules/parameterized-utils

@@ -1 +1 @@
-Subproject commit 7c76b811a321a548af7d4fcf46390daf979f39b1
+Subproject commit 3a58997813693ffbb3b8dd11a24f24ec05c4d1ee

submodules/s-cargot

@@ -0,0 +1 @@
+Subproject commit 68e8eb150f334ec81eac813f76e80c9a8dd4cc7f

submodules/semmc

@@ -1 +1 @@
-Subproject commit de3cef59472041fbfd69494978a8de28716d3f5f
+Subproject commit fcb75a23bb0d07aae42a53e89f6f9da76f7d78e9