From 1d03a7b3b6b706e80af5757930e6342c56c01c9e Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 2 Jul 2019 11:09:16 -0700 Subject: [PATCH 1/2] [base] update ParsedIte/ParsedBranch reference in comment. --- base/src/Data/Macaw/Discovery.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/base/src/Data/Macaw/Discovery.hs b/base/src/Data/Macaw/Discovery.hs index ab9aba82..a9bb95f6 100644 --- a/base/src/Data/Macaw/Discovery.hs +++ b/base/src/Data/Macaw/Discovery.hs @@ -962,7 +962,7 @@ parseFetchAndExecute ctx initRegs stmts initAbsState finalRegs = do withArchConstraints ainfo $ do -- Try to figure out what control flow statement we have. case () of - -- The block ends with a Mux, so we turn this into a `ParsedIte` statement. + -- The block ends with a Mux, so we turn this into a `ParsedBranch` statement. _ | Just (Mux _ c t f) <- valueAsApp (finalRegs^.boundValue ip_reg) , Just trueTgtAddr <- valueAsSegmentOff mem t -- Check that true branch is an allowed intra-procedural branch target From 9fbcbe510facd31217ef93e3d4fca6bdfd90d021 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Tue, 2 Jul 2019 11:16:42 -0700 Subject: [PATCH 2/2] [macaw-semmc] update TH semantics instantiation for What4 semiring changes. --- macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 182 ++++++++++++++++--------- 1 file changed, 118 insertions(+), 64 deletions(-) diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs index ad9c0637..1a1810bd 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs @@ -7,9 +7,9 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeApplications #-} -- | Architecture-independent translation of semmc semantics (via SimpleBuilder) -- into macaw IR. -- @@ -39,9 +39,10 @@ import qualified Control.Concurrent.Async as Async import qualified Data.Functor.Const as C import Data.Functor.Product -import Data.Proxy ( Proxy(..) ) +import qualified Data.Foldable as F import qualified Data.List as L import qualified Data.Map as Map +import Data.Proxy ( Proxy(..) ) import Data.Semigroup ((<>)) import qualified Data.Text as T import Language.Haskell.TH @@ -60,9 +61,12 @@ import Data.Parameterized.Some ( Some(..) ) import qualified Data.Parameterized.TraversableFC as FC import qualified Lang.Crucible.Backend.Simple as S import qualified What4.BaseTypes as CT +import qualified What4.Expr.BoolMap as BooM import qualified What4.Expr.Builder as S +import qualified What4.Expr.WeightedSum as WSum import qualified What4.Interface as SI import qualified What4.InterpretedFloatingPoint as SI +import qualified What4.SemiRing as SR import qualified What4.Symbol as Sy import qualified Dismantle.Instruction as D @@ -607,8 +611,6 @@ addEltTH interps elt = do Just e -> return e Nothing -> case elt of - S.BVExpr w val _loc -> - bindExpr elt [| return (M.BVValue $(natReprTH w) $(lift val)) |] S.AppExpr appElt -> do translatedExpr <- appToExprTH (S.appExprApp appElt) interps bindExpr elt [| G.addExpr =<< $(return translatedExpr) |] @@ -624,8 +626,12 @@ addEltTH interps elt = do S.NonceAppExpr n -> do translatedExpr <- evalNonceAppTH interps (S.nonceExprApp n) bindExpr elt (return translatedExpr) - S.SemiRingLiteral {} -> liftQ [| error "SemiRingLiteral Elts are not supported" |] + S.SemiRingLiteral srTy val _ + | (SR.SemiRingBVRepr _ w) <- srTy -> + 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) |] symFnName :: S.ExprSymFn t args ret -> String symFnName = T.unpack . Sy.solverSymbolAsText . S.symFnName @@ -780,30 +786,28 @@ defaultAppEvaluator :: (A.Architecture arch) -> BoundVarInterpretations arch t fs -> MacawQ arch t fs Exp defaultAppEvaluator elt interps = case elt of - S.TrueBool -> liftQ [| return $ G.ValueExpr (M.BoolValue True) |] - S.FalseBool -> liftQ [| return $ G.ValueExpr (M.BoolValue False) |] - S.NotBool bool -> do + S.NotPred bool -> do e <- addEltTH interps bool liftQ [| return (G.AppExpr (M.NotApp $(return e))) |] - S.AndBool bool1 bool2 -> do - e1 <- addEltTH interps bool1 - e2 <- addEltTH interps bool2 - liftQ [| return (G.AppExpr (M.AndApp $(return e1) $(return e2))) |] - S.XorBool bool1 bool2 -> do - e1 <- addEltTH interps bool1 - e2 <- addEltTH interps bool2 - liftQ [| return (G.AppExpr (M.XorApp $(return e1) $(return e2))) |] - S.IteBool test t f -> do + S.ConjPred boolmap -> evalBoolMap interps AndOp True boolmap + S.DisjPred boolmap -> evalBoolMap interps OrOp False boolmap + S.BaseIte bt _ test t f -> do testE <- addEltTH interps test tE <- addEltTH interps t fE <- addEltTH interps f - liftQ [| return (G.AppExpr (M.Mux M.BoolTypeRepr $(return testE) $(return tE) $(return fE))) |] - S.BVIte w _ test t f -> do - testE <- addEltTH interps test - tE <- addEltTH interps t - fE <- addEltTH interps f - liftQ [| return (G.AppExpr (M.Mux (M.BVTypeRepr $(natReprTH w)) $(return testE) $(return tE) $(return fE))) |] - S.BVEq bv1 bv2 -> do + 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))) |] + S.BaseEq _bt bv1 bv2 -> do e1 <- addEltTH interps bv1 e2 <- addEltTH interps bv2 liftQ [| return (G.AppExpr (M.Eq $(return e1) $(return e2))) |] @@ -833,22 +837,76 @@ defaultAppEvaluator elt interps = case elt of Just Refl -> return (G.ValueExpr $(return e)) Nothing -> error "Invalid reprs for BVSelect translation" |] - S.BVNeg w bv -> do - bvValExp <- addEltTH interps bv - liftQ [| let repW = $(natReprTH w) - in G.AppExpr <$> (M.BVAdd repW <$> G.addExpr (G.AppExpr (M.BVComplement repW $(return bvValExp))) <*> pure (M.mkLit repW 1)) - |] S.BVTestBit idx bv -> do bvValExp <- addEltTH interps bv - liftQ [| G.AppExpr <$> (M.BVTestBit <$> G.addExpr (G.ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx))) <*> pure $(return bvValExp)) |] - S.BVAdd w bv1 bv2 -> do - e1 <- addEltTH interps bv1 - e2 <- addEltTH interps bv2 - liftQ [| return (G.AppExpr (M.BVAdd $(natReprTH w) $(return e1) $(return e2))) |] - S.BVMul w bv1 bv2 -> do - e1 <- addEltTH interps bv1 - e2 <- addEltTH interps bv2 - liftQ [| return (G.AppExpr (M.BVMul $(natReprTH w) $(return e1) $(return e2))) |] + liftQ [| G.AppExpr <$> (M.BVTestBit <$> + G.addExpr (G.ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx))) <*> + pure $(return bvValExp)) |] + + 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 + liftQ [| return + (G.AppExpr + (M.BVMul $(natReprTH w) $(return x) $(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))) + |] + in WSum.evalM add smul sval sm + SR.SemiRingBVRepr SR.BVBitsRepr w -> + let smul mul e = do x <- sval mul + y <- addEltTH interps e + liftQ [| return + (G.AppExpr + (M.BVAnd $(natReprTH w) $(return x) $(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))) + |] + in WSum.evalM add smul sval sm + _ -> liftQ [| error "unsupported SemiRingSum repr for macaw semmc TH" |] + + S.SemiRingProd pd -> + case WSum.prodRepr pd of + SR.SemiRingBVRepr SR.BVArithRepr w -> + let pmul x y = liftQ + [| return + (G.AppExpr + (M.BVMul $(natReprTH w) $(return x) $(return y))) + |] + unit = liftQ [| return $ M.BVValue $(natReprTH w) 1 |] + convert = addEltTH interps + in WSum.prodEvalM pmul convert pd >>= maybe unit return + SR.SemiRingBVRepr SR.BVBitsRepr w -> + let pmul x y = liftQ + [| return + (G.AppExpr + (M.BVAnd $(natReprTH w) $(return x) $(return y))) + |] + unit = liftQ [| return (M.BVValue $(natReprTH w) $(lift $ SI.maxUnsigned w)) |] + convert = addEltTH interps + in WSum.prodEvalM pmul convert pd >>= maybe unit return + _ -> liftQ [| error "unsupported SemiRingProd repr for macaw semmc TH" |] + + S.BVOrBits pd -> + case WSum.prodRepr pd of + SR.SemiRingBVRepr _ w -> + let pmul x y = liftQ + [| return + (G.AppExpr + (M.BVOr $(natReprTH w) $(return x) $(return y))) + |] + unit = liftQ [| return $ M.BVValue $(natReprTH w) 0 |] + convert = addEltTH interps + in WSum.prodEvalM pmul convert pd >>= maybe unit return + S.BVShl w bv1 bv2 -> do e1 <- addEltTH interps bv1 e2 <- addEltTH interps bv2 @@ -867,31 +925,27 @@ defaultAppEvaluator elt interps = case elt of S.BVSext w bv -> do e <- addEltTH interps bv liftQ [| return (G.AppExpr (M.SExt $(return e) $(natReprTH w))) |] - S.BVBitNot w bv -> do - e <- addEltTH interps bv - liftQ [| return (G.AppExpr (M.BVComplement $(natReprTH w) $(return e))) |] - S.BVBitAnd w bv1 bv2 -> do - e1 <- addEltTH interps bv1 - e2 <- addEltTH interps bv2 - liftQ [| return (G.AppExpr (M.BVAnd $(natReprTH w) $(return e1) $(return e2))) |] - S.BVBitOr w bv1 bv2 -> do - e1 <- addEltTH interps bv1 - e2 <- addEltTH interps bv2 - liftQ [| return (G.AppExpr (M.BVOr $(natReprTH w) $(return e1) $(return e2))) |] - S.BVBitXor w bv1 bv2 -> do - e1 <- addEltTH interps bv1 - e2 <- addEltTH interps bv2 - liftQ [| return (G.AppExpr (M.BVXor $(natReprTH w) $(return e1) $(return e2))) |] - S.FloatIte fpp cond fp1 fp2 -> do - c <- addEltTH interps cond - e1 <- addEltTH interps fp1 - e2 <- addEltTH interps fp2 - liftQ [| - return $ G.AppExpr $ M.Mux - (M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp)) - $(return c) - $(return e1) - $(return e2) - |] _ -> 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 +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