diff --git a/macaw-ppc/macaw-ppc.cabal b/macaw-ppc/macaw-ppc.cabal index 55c4f3ab..b7ae3746 100644 --- 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, diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs index 4fb3ec48..204ab496 100644 --- 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.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 + S.BaseBVRepr w -> + M.Mux <$> pure (M.BVTypeRepr w) <*> addElt test <*> addElt t <*> addElt f + 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 :: (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 - M.Mux <$> pure M.BoolTypeRepr <*> addElt test <*> addElt t <*> addElt f -crucAppToExpr (S.BVIte w _ test t f) = AppExpr <$> do -- what is _ for? - 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 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 diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs index 1a1810bd..2319b3a0 100644 --- 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 |] - 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))) |] + 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.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" |] + S.BaseEq _bt bv1 bv2 -> do e1 <- addEltTH interps bv1 e2 <- addEltTH interps bv2 @@ -846,30 +859,32 @@ 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 - BooM.BoolMapTerms ts -> - let onEach e r = do - e >>= \e' -> do - n <- case r of - (t, BooM.Positive) -> addEltTH interps t - (t, BooM.Negative) -> do p <- addEltTH interps t - liftQ [| return (G.AppExpr (M.NotApp $(return p))) |] - 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 + case BooM.viewBoolMap bmap of + BooM.BoolMapUnit -> liftQ [| return (boolBase $(lift defVal)) |] + BooM.BoolMapDualUnit -> liftQ [| return (bNotBase $(lift defVal)) |] + BooM.BoolMapTerms ts -> + 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 [| (G.addExpr =<< return (G.AppExpr (M.NotApp $(return p)))) |] + j <- e + case op of + AndOp -> liftQ [| G.AppExpr <$> (M.AndApp <$> (G.addExpr =<< $(return j)) <*> $(return n)) |] + OrOp -> liftQ [| G.AppExpr <$> (M.OrApp <$> (G.addExpr =<< $(return j)) <*> $(return n)) |] diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 55688ea1..b2efc59a 100644 --- 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