Merge pull request #56 from GaloisInc/semiring_upd

Semiring upd
2024-12-18 03:21:49 +03:00 · 2019-07-19 13:33:37 -07:00 · 2019-07-19 13:33:37 -07:00 · 2d86fa7a5a
commit 2d86fa7a5a
parent 88343ea716 fb31de230f
4 changed files with 186 additions and 82 deletions
--- a/macaw-ppc/macaw-ppc.cabal
+++ b/macaw-ppc/macaw-ppc.cabal
@ -39,6 +39,7 @@ library
                       semmc,
                       semmc-ppc,
                       macaw-semmc,
+                       macaw-symbolic,
                       macaw-loader,
                       macaw-loader-ppc,
                       lens,
--- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs
+++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs
@ -9,9 +9,10 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}

 module Data.Macaw.PPC.Semantics.Base
  ( crucAppToExpr
@ -19,17 +20,23 @@ module Data.Macaw.PPC.Semantics.Base
  , interpretFormula
  ) where

+import qualified Data.Foldable as F
 import           Data.Proxy
 import           GHC.TypeLits

 import           Data.Parameterized.Classes
-import qualified What4.Expr.Builder as S
 import qualified What4.BaseTypes as S
+import qualified What4.Expr.BoolMap as BooM
+import qualified What4.Expr.Builder as S
+import qualified What4.Expr.WeightedSum as WSum
+import qualified What4.InterpretedFloatingPoint as SFP
+import qualified What4.SemiRing as SR

 import qualified SemMC.Architecture.PPC as SP
 import qualified SemMC.Architecture.PPC.Location as APPC
 import qualified Data.Macaw.CFG as M
 import qualified Data.Macaw.Types as M
+import qualified Data.Macaw.Symbolic as MS

 import Data.Parameterized.NatRepr ( knownNat
                                  , addNat
@ -44,21 +51,29 @@ import           Data.Macaw.PPC.PPCReg
 type family FromCrucibleBaseType (btp :: S.BaseType) :: M.Type where
  FromCrucibleBaseType (S.BaseBVType w) = M.BVType w
  FromCrucibleBaseType (S.BaseBoolType) = M.BoolType
+  FromCrucibleBaseType (S.BaseFloatType fpp) =
+    M.FloatType (MS.FromCrucibleFloatInfo (SFP.FloatPrecisionToInfo fpp))

-crucAppToExpr :: (M.ArchConstraints ppc) => S.App (S.Expr t) ctp -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
-crucAppToExpr S.TrueBool  = return $ ValueExpr (M.BoolValue True)
-crucAppToExpr S.FalseBool = return $ ValueExpr (M.BoolValue False)
-crucAppToExpr (S.NotBool bool) = (AppExpr . M.NotApp) <$> addElt bool
-crucAppToExpr (S.AndBool bool1 bool2) = AppExpr <$> do
-  M.AndApp <$> addElt bool1 <*> addElt bool2
-crucAppToExpr (S.XorBool bool1 bool2) = AppExpr <$> do
-  M.XorApp <$> addElt bool1 <*> addElt bool2
-crucAppToExpr (S.IteBool test t f) = AppExpr <$> do
+crucAppToExpr :: (M.ArchConstraints ppc) =>
+                 S.App (S.Expr t) ctp
+              -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
+crucAppToExpr (S.NotPred bool) = AppExpr . M.NotApp <$> addElt bool
+crucAppToExpr (S.ConjPred boolmap) = evalBoolMap AndOp True boolmap
+crucAppToExpr (S.DisjPred boolmap) = evalBoolMap OrOp False boolmap
+crucAppToExpr (S.BaseIte bt _ test t f) = AppExpr <$>
+  case bt of
+    S.BaseBoolRepr ->
      M.Mux <$> pure M.BoolTypeRepr <*> addElt test <*> addElt t <*> addElt f
-crucAppToExpr (S.BVIte w _ test t f) = AppExpr <$> do -- what is _ for?
+    S.BaseBVRepr w ->
      M.Mux <$> pure (M.BVTypeRepr w) <*> addElt test <*> addElt t <*> addElt f
-crucAppToExpr (S.BVEq bv1 bv2) = AppExpr <$> do
-  M.Eq <$> addElt bv1 <*> addElt bv2
+    S.BaseFloatRepr fpp ->
+      M.Mux
+      (M.FloatTypeRepr (MS.floatInfoFromCrucible $ SFP.floatPrecisionToInfoRepr fpp))
+      <$> addElt test <*> addElt t <*> addElt f
+    _ -> error "unsupported BaseITE repr for macaw PPC base semantics"
+crucAppToExpr (S.BaseEq _bt bv1 bv2) =
+  AppExpr <$> do M.Eq <$> addElt bv1 <*> addElt bv2
+
 crucAppToExpr (S.BVSlt bv1 bv2) = AppExpr <$> do
  M.BVSignedLt <$> addElt bv1 <*> addElt bv2
 crucAppToExpr (S.BVUlt bv1 bv2) = AppExpr <$> do
@ -95,18 +110,48 @@ crucAppToExpr (S.BVSelect idx n bv) = do
      -- Is there a way to just "know" that n = w?
      Just Refl <- return $ testEquality n w
      return $ ValueExpr bvVal
-crucAppToExpr (S.BVNeg w bv) = do
-  bvVal  <- addElt bv
-  bvComp <- addExpr (AppExpr (M.BVComplement w bvVal))
-  return $ AppExpr (M.BVAdd w bvComp (M.mkLit w 1))
 crucAppToExpr (S.BVTestBit idx bv) = AppExpr <$> do
  M.BVTestBit
    <$> addExpr (ValueExpr (M.BVValue (S.bvWidth bv) (fromIntegral idx)))
    <*> addElt bv
-crucAppToExpr (S.BVAdd repr bv1 bv2) = AppExpr <$> do
-  M.BVAdd <$> pure repr <*> addElt bv1 <*> addElt bv2
-crucAppToExpr (S.BVMul repr bv1 bv2) = AppExpr <$> do
-  M.BVMul <$> pure repr <*> addElt bv1 <*> addElt bv2
+
+crucAppToExpr (S.SemiRingSum sm) =
+    case WSum.sumRepr sm of
+      SR.SemiRingBVRepr SR.BVArithRepr w ->
+        let smul mul e = do x <- sval mul
+                            y <- eltToExpr e
+                            AppExpr <$> do M.BVMul w <$> addExpr x <*> addExpr y
+            sval v = return $ ValueExpr $ M.BVValue w v
+            add x y = AppExpr <$> do M.BVAdd w <$> addExpr x <*> addExpr y
+        in WSum.evalM add smul sval sm
+      SR.SemiRingBVRepr SR.BVBitsRepr w ->
+        let smul mul e = do x <- sval mul
+                            y <- eltToExpr e
+                            AppExpr <$> do M.BVAnd w <$> addExpr x <*> addExpr y
+            sval v = return $ ValueExpr $ M.BVValue w v
+            add x y = AppExpr <$> do M.BVXor w <$> addExpr x <*> addExpr y
+        in WSum.evalM add smul sval sm
+      _ -> error "unsupported SemiRingSum repr for macaw PPC base semantics"
+
+crucAppToExpr (S.SemiRingProd pd) =
+    case WSum.prodRepr pd of
+      SR.SemiRingBVRepr SR.BVArithRepr w ->
+        let pmul x y = AppExpr <$> do M.BVMul w <$> addExpr x <*> addExpr y
+            unit = return $ ValueExpr $ M.BVValue w 1
+        in WSum.prodEvalM pmul eltToExpr pd >>= maybe unit return
+      SR.SemiRingBVRepr SR.BVBitsRepr w ->
+        let pmul x y = AppExpr <$> do M.BVAnd w <$> addExpr x <*> addExpr y
+            unit = return $ ValueExpr $ M.BVValue w $ S.maxUnsigned w
+        in WSum.prodEvalM pmul eltToExpr pd >>= maybe unit return
+      _ -> error "unsupported SemiRingProd repr for macaw PPC base semantics"
+
+crucAppToExpr (S.BVOrBits pd) =
+    case WSum.prodRepr pd of
+      SR.SemiRingBVRepr _ w ->
+        let pmul x y = AppExpr <$> do M.BVOr w <$> addExpr x <*> addExpr y
+            unit = return $ ValueExpr $ M.BVValue w 0
+        in WSum.prodEvalM pmul eltToExpr pd >>= maybe unit return
+
 crucAppToExpr (S.BVShl repr bv1 bv2) = AppExpr <$> do
  M.BVShl <$> pure repr <*> addElt bv1 <*> addElt bv2
 crucAppToExpr (S.BVLshr repr bv1 bv2) = AppExpr <$> do
@ -117,17 +162,34 @@ crucAppToExpr (S.BVZext repr bv) = AppExpr <$> do
  M.UExt <$> addElt bv <*> pure repr
 crucAppToExpr (S.BVSext repr bv) = AppExpr <$> do
  M.SExt <$> addElt bv <*> pure repr
-crucAppToExpr (S.BVBitNot repr bv) = AppExpr <$> do
-  M.BVComplement <$> pure repr <*> addElt bv
-crucAppToExpr (S.BVBitAnd repr bv1 bv2) = AppExpr <$> do
-  M.BVAnd <$> pure repr <*> addElt bv1 <*> addElt bv2
-crucAppToExpr (S.BVBitOr repr bv1 bv2) = AppExpr <$> do
-  M.BVOr <$> pure repr <*> addElt bv1 <*> addElt bv2
-crucAppToExpr (S.BVBitXor repr bv1 bv2) = AppExpr <$> do
-  M.BVXor <$> pure repr <*> addElt bv1 <*> addElt bv2
+
 crucAppToExpr _ = error "crucAppToExpr: unimplemented crucible operation"


+data BoolMapOp = AndOp | OrOp
+
+evalBoolMap :: M.ArchConstraints ppc =>
+               BoolMapOp -> Bool -> BooM.BoolMap (S.Expr t)
+            -> Generator ppc ids s (Expr ppc ids 'M.BoolType)
+evalBoolMap op defVal bmap =
+  let bBase b = return $ ValueExpr (M.BoolValue b)
+      bNotBase = bBase . not
+  in case BooM.viewBoolMap bmap of
+       BooM.BoolMapUnit -> bBase defVal
+       BooM.BoolMapDualUnit -> bNotBase defVal
+       BooM.BoolMapTerms ts ->
+         let onEach e r = do
+               e >>= \e' -> do
+                 n <- case r of
+                        (t, BooM.Positive) -> eltToExpr t
+                        (t, BooM.Negative) -> do p <- eltToExpr t
+                                                 AppExpr <$> do M.NotApp <$> addExpr p
+                 case op of
+                   AndOp -> AppExpr <$> do M.AndApp <$> addExpr e' <*> addExpr n
+                   OrOp  -> AppExpr <$> do M.OrApp  <$> addExpr e' <*> addExpr n
+         in F.foldl onEach (bBase defVal) ts
+
+
 locToReg :: (1 <= APPC.ArchRegWidth ppc,
             M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
         => proxy ppc
@ -162,11 +224,16 @@ interpretFormula loc elt = do
      setRegVal reg (M.AssignedValue assignment)

 -- Convert a Crucible element into an expression.
-eltToExpr :: M.ArchConstraints ppc => S.Expr t ctp -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
-eltToExpr (S.BVExpr w val _) = return $ ValueExpr (M.BVValue w val)
+eltToExpr :: M.ArchConstraints ppc =>
+             S.Expr t ctp
+          -> Generator ppc ids s (Expr ppc ids (FromCrucibleBaseType ctp))
 eltToExpr (S.AppExpr appElt) = crucAppToExpr (S.appExprApp appElt)
+eltToExpr (S.SemiRingLiteral (SR.SemiRingBVRepr _ w) val _) =
+  return $ ValueExpr (M.BVValue w val)
 eltToExpr _ = undefined

 -- Add a Crucible element in the Generator monad.
-addElt :: M.ArchConstraints ppc => S.Expr t ctp -> Generator ppc ids s (M.Value ppc ids (FromCrucibleBaseType ctp))
+addElt :: M.ArchConstraints ppc =>
+          S.Expr t ctp
+       -> Generator ppc ids s (M.Value ppc ids (FromCrucibleBaseType ctp))
 addElt elt = eltToExpr elt >>= addExpr
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@ -631,7 +631,8 @@ addEltTH interps elt = do
            bindExpr elt [| return (M.BVValue $(natReprTH w) $(lift val)) |]
          | otherwise -> liftQ [| error "SemiRingLiteral Elts are not supported" |]
        S.StringExpr {} -> liftQ [| error "StringExpr elts are not supported" |]
-        S.BoolExpr b _loc -> liftQ [| return $ G.ValueExpr (M.BoolValue b) |]
+        S.BoolExpr b _loc -> bindExpr elt [| return (M.BoolValue $(lift b)) |]
+

 symFnName :: S.ExprSymFn t args ret -> String
 symFnName = T.unpack . Sy.solverSymbolAsText . S.symFnName
@ -795,18 +796,30 @@ defaultAppEvaluator elt interps = case elt of
    testE <- addEltTH interps test
    tE <- addEltTH interps t
    fE <- addEltTH interps f
-    tr <- case bt of
-            CT.BaseBoolRepr -> liftQ [| return M.BoolTypeRepr |]
+    case bt of
+      CT.BaseBoolRepr -> liftQ [| return
+                                  (G.AppExpr
+                                   (M.Mux M.BoolTypeRepr
+                                    $(return testE) $(return tE) $(return fE)))
+                                |]
+      CT.BaseBVRepr w -> liftQ [| return
+                                  (G.AppExpr
+                                   (M.Mux (M.BVTypeRepr $(natReprTH w))
+                                    $(return testE) $(return tE) $(return fE)))
+                                |]
+      CT.BaseFloatRepr fpp -> liftQ [| return
+                                       (G.AppExpr
+                                        (M.Mux (M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp))
+                                         $(return testE) $(return tE) $(return fE)))
+                                     |]
      CT.BaseNatRepr -> liftQ [| error "Macaw semantics for nat ITE unsupported" |]
      CT.BaseIntegerRepr -> liftQ [| error "Macaw semantics for integer ITE unsupported" |]
      CT.BaseRealRepr -> liftQ [| error "Macaw semantics for real ITE unsupported" |]
      CT.BaseStringRepr -> liftQ [| error "Macaw semantics for string ITE unsupported" |]
-            CT.BaseBVRepr w -> liftQ [| M.BVTypeRepr $(natReprTH w) |]
-            CT.BaseFloatRepr fpp -> liftQ [| M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp) |]
      CT.BaseComplexRepr -> liftQ [| error "Macaw semantics for complex ITE unsupported" |]
      CT.BaseStructRepr {} -> liftQ [| error "Macaw semantics for struct ITE unsupported" |]
      CT.BaseArrayRepr {} -> liftQ [| error "Macaw semantics for array ITE unsupported" |]
-    liftQ [| return (G.AppExpr (M.Mux $(return tr) $(return testE) $(return tE) $(return fE))) |]
+
  S.BaseEq _bt bv1 bv2 -> do
    e1 <- addEltTH interps bv1
    e2 <- addEltTH interps bv2
@ -846,29 +859,31 @@ defaultAppEvaluator elt interps = case elt of
  S.SemiRingSum sm ->
    case WSum.sumRepr sm of
      SR.SemiRingBVRepr SR.BVArithRepr w ->
-        let smul mul e = do x <- sval mul
-                            y <- addEltTH interps e
+        let smul mul e = do y <- addEltTH interps e
                            liftQ [| return
                                     (G.AppExpr
-                                      (M.BVMul $(natReprTH w) $(return x) $(return y)))
+                                      (M.BVMul $(natReprTH w)
+                                       (M.BVValue $(natReprTH w) $(lift mul))
+                                       $(return y)))
                                   |]
-            sval v = liftQ [| return (M.BVValue $(natReprTH w) $(lift v)) |]
-            add x y = liftQ [| return
-                               (G.AppExpr
-                                (M.BVAdd $(natReprTH w) $(return x) $(return y)))
+            sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift v))) |]
+            add x y = liftQ [| G.AppExpr <$> (M.BVAdd $(natReprTH w)
+                                              <$> (G.addExpr =<< $(return x))
+                                              <*> (G.addExpr =<< $(return y)))
                                |]
        in WSum.evalM add smul sval sm
      SR.SemiRingBVRepr SR.BVBitsRepr w ->
-        let smul mul e = do x <- sval mul
-                            y <- addEltTH interps e
+        let smul mul e = do y <- addEltTH interps e
                            liftQ [| return
                                     (G.AppExpr
-                                      (M.BVAnd $(natReprTH w) $(return x) $(return y)))
+                                      (M.BVAnd $(natReprTH w)
+                                       (M.BVValue $(natReprTH w) $(lift mul))
+                                       $(return y)))
                                   |]
-            sval v = liftQ [| return (M.BVValue $(natReprTH w) $(lift v)) |]
-            add x y = liftQ [| return
-                               (G.AppExpr
-                                (M.BVXor $(natReprTH w) $(return x) $(return y)))
+            sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift v))) |]
+            add x y = liftQ [| G.AppExpr <$> (M.BVXor $(natReprTH w)
+                                              <$> (G.addExpr =<< $(return x))
+                                              <*> (G.addExpr =<< $(return y)))
                                |]
        in WSum.evalM add smul sval sm
      _ -> liftQ [| error "unsupported SemiRingSum repr for macaw semmc TH" |]
@ -927,25 +942,44 @@ defaultAppEvaluator elt interps = case elt of
    liftQ [| return (G.AppExpr (M.SExt $(return e) $(natReprTH w))) |]
  _ -> error $ "unsupported Crucible elt:" ++ show elt

+
+----------------------------------------------------------------------
+
 data BoolMapOp = AndOp | OrOp

+
 evalBoolMap :: A.Architecture arch =>
               BoundVarInterpretations arch t fs
-            -> BoolMapOp -> Bool -> BooM.BoolMap (S.Expr t) -> MacawQ arch t fs Exp
+            -> BoolMapOp
+            -> Bool
+            -> BooM.BoolMap (S.Expr t)
+            -> MacawQ arch t fs Exp
 evalBoolMap interps op defVal bmap =
-  let bBase b = liftQ [| return $ G.ValueExpr (M.BoolValue b) |]
-      bNotBase = bBase . not
-  in case BooM.viewBoolMap bmap of
-       BooM.BoolMapUnit -> bBase defVal
-       BooM.BoolMapDualUnit -> bNotBase defVal
+  case BooM.viewBoolMap bmap of
+    BooM.BoolMapUnit ->     liftQ [| return (boolBase $(lift defVal)) |]
+    BooM.BoolMapDualUnit -> liftQ [| return (bNotBase $(lift defVal)) |]
    BooM.BoolMapTerms ts ->
-         let onEach e r = do
-               e >>= \e' -> do
-                 n <- case r of
-                        (t, BooM.Positive) -> addEltTH interps t
+         do d <- liftQ [| return (boolBase $(lift defVal)) |]
+            F.foldl (joinBool interps op) (return d) ts
+
+
+boolBase, bNotBase :: A.Architecture arch => Bool -> G.Expr arch t 'M.BoolType
+boolBase = G.ValueExpr . M.BoolValue
+bNotBase = boolBase . not
+
+joinBool :: A.Architecture arch =>
+            BoundVarInterpretations arch t fs
+         -> BoolMapOp
+         -> MacawQ arch t fs Exp
+         -> (S.Expr t SI.BaseBoolType, S.Polarity)
+         -> MacawQ arch t fs Exp
+joinBool interps op e r =
+  do n <- case r of
+            (t, BooM.Positive) -> do p <- addEltTH interps t
+                                     liftQ [| return $(return p) |]
            (t, BooM.Negative) -> do p <- addEltTH interps t
-                                                 liftQ [| return (G.AppExpr (M.NotApp $(return p))) |]
+                                     liftQ [| (G.addExpr =<< return (G.AppExpr (M.NotApp $(return p)))) |]
+     j <- e
     case op of
-                   AndOp -> liftQ [| return (G.AppExpr (M.AndApp $(return e') $(return n))) |]
-                   OrOp  -> liftQ [| return (G.AppExpr (M.OrApp $(return e') $(return n))) |]
-         in F.foldl onEach (bBase defVal) ts
+       AndOp -> liftQ [| G.AppExpr <$> (M.AndApp <$> (G.addExpr =<< $(return j)) <*> $(return n)) |]
+       OrOp  -> liftQ [| G.AppExpr <$> (M.OrApp  <$> (G.addExpr =<< $(return j)) <*> $(return n)) |]
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@ -20,7 +20,7 @@
 -- library.  There are two main portions of the API:
 --
 -- 1. Translation of Macaw IR into Crucible CFGs
-- 2. Symbolic execution of Crucible CFGs generated from MAcaw
+-- 2. Symbolic execution of Crucible CFGs generated from Macaw
 --
 -- There are examples of each use case in the relevant sections of the haddocks.
 --
@ -41,6 +41,7 @@
 --   do not necessarily hold for all machine code programs, but that do hold for
 --   (correct) C and C++ programs.  The current state of memory is held in a
 --   Crucible global value that is modified by all code.
+--
 -- * Each function takes a single argument (the full set of machine registers)
 --   and returns a single value (the full set of machine registers reflecting
 --   any modifications)
@ -77,6 +78,7 @@ module Data.Macaw.Symbolic
  , CG.crucArchRegTypes
  , PS.ToCrucibleType
  , PS.ToCrucibleFloatInfo
+  , PS.FromCrucibleFloatInfo
  , PS.floatInfoToCrucible
  , PS.floatInfoFromCrucible
  , PS.ArchRegContext