From 879d6b253f502d450535b7c0cfee2de76ceac132 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 2 Aug 2024 16:46:14 -0700 Subject: [PATCH 1/8] add identifier-based what4 deserialization provides an additional interface for serializing expression-containing types using abstract identifiers, producing a binding environment that can be used during deserialization --- src/What4/JSON.hs | 195 +++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 183 insertions(+), 12 deletions(-) diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 97d1d3a6..b0f68bcd 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -34,10 +34,15 @@ module What4.JSON import Control.Monad.State (MonadState (..), State, modify, evalState, runState) import qualified Data.Map.Ordered as OMap +import Data.List ( stripPrefix ) +import Data.Maybe ( mapMaybe ) import Data.Map (Map) import Data.Text (Text) import Data.Data (Proxy(..), Typeable) import qualified Data.Aeson as JSON +import qualified Data.Aeson.Types as JSON +import qualified Data.BitVector.Sized as BVS +import qualified Numeric as N import Data.Parameterized.Some (Some(..)) @@ -62,6 +67,8 @@ import qualified Lang.Crucible.Utils.MuxTree as MT import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.TraversableFC as TFC import qualified Data.Parameterized.SetF as SetF +import qualified Data.Parameterized.SetF as SetF +import Data.Parameterized.Classes import Data.Functor.Const import Control.Monad.Trans.Reader hiding (asks,ask) import qualified Data.IORef as IO @@ -69,6 +76,10 @@ import Control.Monad.Reader import Control.Exception (tryJust) import What4.Utils.Process (filterAsync) import qualified What4.ExprHelpers as WEH +import Control.Monad.Except +import Control.Applicative +import GHC.Natural +import Unsafe.Coerce (unsafeCoerce) newtype ExprCache sym = ExprCache (Map (Some (W4.SymExpr sym)) JSON.Value) @@ -76,6 +87,7 @@ newtype ExprCache sym = ExprCache (Map (Some (W4.SymExpr sym)) JSON.Value) data W4SEnv sym = W4SEnv { w4sCache :: IO.IORef (ExprCache sym) , w4sSym :: sym + , w4sUseIdents :: Bool } newtype W4S sym a = W4S (ReaderT (W4SEnv sym) IO a) @@ -100,9 +112,30 @@ w4ToJSON :: forall sym a. SerializableExprs sym => W4Serializable sym a => sym - w4ToJSON sym a = do cacheRef <- IO.newIORef (ExprCache Map.empty) W4S f <- return $ w4Serialize @sym a - let env = W4SEnv cacheRef sym + let env = W4SEnv cacheRef sym False runReaderT f env +newtype ExprEnv sym = ExprEnv (Map Integer (Some (W4.SymExpr sym))) + +-- | Extract expressions with annotations +cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> ExprEnv sym +cacheToEnv sym (ExprCache m) = ExprEnv $ Map.fromList $ mapMaybe go (Map.keys m) + where + go (Some e) + | Nothing <- W4.asConcrete e + , Just ann <- W4.getAnnotation sym e + = Just (fromIntegral $ hashF ann, Some e) + go _ = Nothing + +w4ToJSONEnv :: forall sym a. (W4.IsExprBuilder sym, SerializableExprs sym) => W4Serializable sym a => sym -> a -> IO (JSON.Value, ExprEnv sym) +w4ToJSONEnv sym a = do + cacheRef <- IO.newIORef (ExprCache Map.empty) + W4S f <- return $ w4Serialize @sym a + let env = W4SEnv cacheRef sym True + v <- runReaderT f env + c <- IO.readIORef cacheRef + return $ (v, cacheToEnv sym c) + class W4SerializableF sym (f :: k -> Type) where withSerializable :: Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a @@ -142,16 +175,24 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) Just{} -> return $ JSON.String (T.pack (show (W4.printSymExpr e'))) _ -> do sym <- asks w4sSym - e <- liftIO $ WEH.stripAnnotations sym e' - mv <- trySerialize $ do - let result = W4S.serializeExprWithConfig (W4S.Config True True) e - let var_env = map (\(Some bv, t) -> (show (W4B.bvarName bv), t)) $ OMap.toAscList $ W4S.resFreeVarEnv result - let fn_env = map (\(W4S.SomeExprSymFn fn, t) -> (show (W4B.symFnName fn), t)) $ OMap.toAscList $ W4S.resSymFnEnv result - let sexpr = W4S.resSExpr result - return $ JSON.object [ "symbolic" JSON..= JSON.String (W4D.printSExpr mempty sexpr), "vars" JSON..= var_env, "fns" JSON..= fn_env ] - case mv of - Left er -> return $ JSON.object [ "symbolic_serialize_err" JSON..= er] - Right v -> return v + asks w4sUseIdents >>= \case + True -> case W4.getAnnotation sym e' of + Just ann -> do + let tp_sexpr = W4S.serializeBaseType (W4.exprType e') + let (ident :: Integer) = fromIntegral $ hashF ann + return $ JSON.object [ "symbolic_ident" JSON..= ident, "type" JSON..= JSON.String (W4D.printSExpr mempty tp_sexpr) ] + Nothing -> return $ JSON.object [ "symbolic_serialize_err" JSON..= ("Missing expression annotation" :: String)] + False -> do + e <- liftIO $ WEH.stripAnnotations sym e' + mv <- trySerialize $ do + let result = W4S.serializeExprWithConfig (W4S.Config True True) e + let var_env = map (\(Some bv, t) -> (show (W4B.bvarName bv), t)) $ OMap.toAscList $ W4S.resFreeVarEnv result + let fn_env = map (\(W4S.SomeExprSymFn fn, t) -> (show (W4B.symFnName fn), t)) $ OMap.toAscList $ W4S.resSymFnEnv result + let sexpr = W4S.resSExpr result + return $ JSON.object [ "symbolic" JSON..= JSON.String (W4D.printSExpr mempty sexpr), "vars" JSON..= var_env, "fns" JSON..= fn_env ] + case mv of + Left er -> return $ JSON.object [ "symbolic_serialize_err" JSON..= er] + Right v -> return v modify $ \(ExprCache s') -> ExprCache (Map.insert (Some e') v s') return v @@ -247,4 +288,134 @@ instance forall sym e. (W4SerializableF sym e) => W4SerializableF sym (SetF.SetF instance forall sym f tp. (W4Serializable sym f) => W4Serializable sym (Const f tp) where w4Serialize (Const f) = w4Serialize f -instance forall sym f. (W4Serializable sym f) => W4SerializableF sym (Const f) \ No newline at end of file +instance forall sym f. (W4Serializable sym f) => W4SerializableF sym (Const f) + + +data W4DSEnv sym where + W4DSEnv :: W4.IsExprBuilder sym => { + w4dsEnv :: ExprEnv sym + , w4dsSym :: sym + } -> W4DSEnv sym + +newtype W4DS sym a = W4DS (ExceptT String (ReaderT (W4DSEnv sym) IO) a) + deriving (Monad, Applicative, Functor, MonadReader (W4DSEnv sym), MonadIO, Alternative, MonadError String) + +instance MonadFail (W4DS sym) where + fail msg = throwError msg + +class W4Deserializable sym a where + w4Deserialize :: JSON.Value -> W4DS sym a + +jsonToW4 :: (W4Deserializable sym a, W4.IsExprBuilder sym) => sym -> ExprEnv sym -> JSON.Value -> IO (Either String a) +jsonToW4 sym env v = do + let wenv = W4DSEnv env sym + let W4DS f = (w4Deserialize v) + runReaderT (runExceptT f) wenv + +fromJSON :: JSON.FromJSON a => JSON.Value -> W4DS sym a +fromJSON v = case JSON.fromJSON v of + JSON.Success a -> return a + JSON.Error msg -> fail msg + +liftParser :: (b -> JSON.Parser a) -> b -> W4DS sym a +liftParser f v = case JSON.parse f v of + JSON.Success a -> return a + JSON.Error msg -> fail msg + +(.:) :: JSON.FromJSON a => JSON.Object -> JSON.Key -> W4DS sym a +(.:) o = liftParser ((JSON..:) o) + + +newtype ToDeserializable sym tp = ToDeserializable { _unDS :: W4.SymExpr sym tp } + +instance W4Deserializable sym (Some (ToDeserializable sym)) where + w4Deserialize v = fmap (\(Some x) -> Some (ToDeserializable x)) $ ask >>= \W4DSEnv{} -> asks w4dsSym >>= \sym -> do + (i :: Integer) <- fromJSON v + Some <$> (liftIO $ W4.intLit sym i) + <|> do + (b :: Bool) <- fromJSON v + Some <$> (return $ if b then W4.truePred sym else W4.falsePred sym) + <|> do + JSON.String s0 <- return v + Just s1 <- return $ stripPrefix "0x" (T.unpack s0) + ((i :: Integer,s2):_) <- return $ N.readHex s1 + Just s3 <- return $ stripPrefix ":[" s2 + ((w :: Natural,_s4):_) <- return $ readsPrec 0 s3 + Just (Some repr) <- return $ W4.someNat w + Just W4.LeqProof <- return $ W4.isPosNat repr + Some <$> (liftIO $ W4.bvLit sym repr (BVS.mkBV repr i)) + <|> do + JSON.Object o <- return v + (ident :: Integer) <- o .: "symbolic_ident" + ExprEnv env <- asks w4dsEnv + Just (Some e) <- return $ Map.lookup ident env + return $ Some e + +instance forall tp sym. KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (ToDeserializable sym tp) where + w4Deserialize v = ask >>= \W4DSEnv{} -> do + Some (ToDeserializable e :: ToDeserializable sym tp') <- w4Deserialize v + case testEquality (knownRepr @_ @_ @tp) (W4.exprType e) of + Just Refl -> return $ ToDeserializable e + Nothing -> fail $ "Unexpected type: " ++ show (W4.exprType e) + +newtype SymDeserializable sym f = SymDeserializable (forall tp a. ((KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (f tp)) => a) -> a) + +symDeserializable :: + forall sym. + sym -> + SymDeserializable sym (W4.SymExpr sym) +symDeserializable _sym = unsafeCoerce r + where + r :: SymDeserializable sym (ToDeserializable sym) + r = SymDeserializable (\a -> a) + +{- +class (TestEquality g, KnownRepr g k) => W4DeserializableF sym (f :: k -> Type) where + withDeserializable :: Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a + + default withDeserializable :: W4Deserializable sym (f tp) => Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a + withDeserializable _ _ _ x = x + + w4DeserializeF :: forall tp. JSON.Value -> W4DS sym (f tp) + w4DeserializeF x = withDeserializable (Proxy :: Proxy sym) (Proxy :: Proxy f) (Proxy :: Proxy tp) (w4Deserialize x) +-} + +{- +data WrappedBuilder sym = + WrappedBuilder { wSym :: sym, wEnv :: MapF (W4.SymAnnotation sym) (W4.SymExpr sym)} + +data WSymExpr sym tp where + WSymExpr :: W4.SymAnnotation sym tp -> WSymExpr sym tp + WConc :: W4.ConcreteVal tp -> WSymExpr sym tp + + +instance JSON.FromJSON (Some (W4.SymAnnotation sym)) => JSON.FromJSON (Some (WSymExpr sym)) where + parseJSON v = do + JSON.Object o <- return v + go o + where + go o = do + Some (ann :: W4.SymAnnotation sym tp) <- o JSON..: "ann" + return $ Some (WSymExpr ann) + <|> do + (i :: Integer) <- o JSON..: "conc_int" + return $ Some $ WConc (W4.ConcreteInteger i) + <|> do + (i :: Bool) <- o JSON..: "conc_bool" + return $ Some $ WConc (W4.ConcreteBool i) + <|> fail "Unsupported value" + + +instance JSON.ToJSON (W4.SymAnnotation sym tp) => JSON.ToJSON (WSymExpr sym tp) where + toJSON = + + + +instance forall sym sym'. (sym ~ WrappedBuilder sym', W4.IsExprBuilder sym', W4Deserializable sym (Some (W4.SymAnnotation sym'))) => W4Deserializable sym (Some (WSymExpr sym)) where + w4Deserialize v = do + Some (ann :: W4.SymAnnotation sym' tp') <- w4Deserialize v + sym <- asks w4dsSym + case MapF.lookup ann (wEnv sym) of + Just e -> return $ Some $ WSymExpr e + Nothing -> fail "Missing annotation" +-} From 7230cd7befb1ecd130f0a8c249b51fb282339e57 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Mon, 5 Aug 2024 16:40:18 -0700 Subject: [PATCH 2/8] use expression hash for identifiers --- src/What4/JSON.hs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index b0f68bcd..93c6c2b8 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -123,8 +123,7 @@ cacheToEnv sym (ExprCache m) = ExprEnv $ Map.fromList $ mapMaybe go (Map.keys m) where go (Some e) | Nothing <- W4.asConcrete e - , Just ann <- W4.getAnnotation sym e - = Just (fromIntegral $ hashF ann, Some e) + = Just (fromIntegral $ hashF e, Some e) go _ = Nothing w4ToJSONEnv :: forall sym a. (W4.IsExprBuilder sym, SerializableExprs sym) => W4Serializable sym a => sym -> a -> IO (JSON.Value, ExprEnv sym) @@ -176,12 +175,10 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) _ -> do sym <- asks w4sSym asks w4sUseIdents >>= \case - True -> case W4.getAnnotation sym e' of - Just ann -> do - let tp_sexpr = W4S.serializeBaseType (W4.exprType e') - let (ident :: Integer) = fromIntegral $ hashF ann - return $ JSON.object [ "symbolic_ident" JSON..= ident, "type" JSON..= JSON.String (W4D.printSExpr mempty tp_sexpr) ] - Nothing -> return $ JSON.object [ "symbolic_serialize_err" JSON..= ("Missing expression annotation" :: String)] + True -> do + let tp_sexpr = W4S.serializeBaseType (W4.exprType e') + let (ident :: Integer) = fromIntegral $ hashF e' + return $ JSON.object [ "symbolic_ident" JSON..= ident, "type" JSON..= JSON.String (W4D.printSExpr mempty tp_sexpr) ] False -> do e <- liftIO $ WEH.stripAnnotations sym e' mv <- trySerialize $ do From 897f49b4269ee4ac869e034432f605b847bbc8a3 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Mon, 5 Aug 2024 16:41:16 -0700 Subject: [PATCH 3/8] compute trace footprint from sequence --- .../StrongestPosts/CounterExample.hs | 34 +++++++++ src/Pate/Verification/Widening.hs | 72 +++++++++++++++---- src/What4/JSON.hs | 1 + src/What4/SymSequence.hs | 37 +++++----- 4 files changed, 114 insertions(+), 30 deletions(-) diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs index bfb18b54..27f9356b 100644 --- a/src/Pate/Verification/StrongestPosts/CounterExample.hs +++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs @@ -28,6 +28,8 @@ module Pate.Verification.StrongestPosts.CounterExample , groundTraceEvent , groundTraceEventSequence , groundRegOp + , TraceFootprint(..) + , mkFootprint ) where @@ -61,6 +63,8 @@ import Lang.Crucible.Simulator.SymSequence import qualified Lang.Crucible.Types as CT import qualified Data.Parameterized.TraversableF as TF import qualified What4.Concrete as W4 +import qualified What4.SymSequence as W4 + import Data.Functor.Const import qualified Data.Parameterized.Map as MapF import Data.Maybe (mapMaybe) @@ -243,6 +247,36 @@ data TraceEventsOne sym arch (bin :: PB.WhichBinary) = TraceEventsOne , traceEventGroups :: [TraceEventGroup sym arch] } +-- | Partial symbolic spec for the initial state +data TraceFootprint sym arch = TraceFootprint + { fpInitialRegs :: MT.RegOp sym arch + , fpMem :: [(MM.ArchSegmentOff arch, (MT.MemOp sym (MM.ArchAddrWidth arch)))] + } + +mkFootprint :: + forall sym arch. + W4.IsExprBuilder sym => + sym -> + MT.RegOp sym arch -> + SymSequence sym (MT.TraceEvent sym arch) -> + IO (TraceFootprint sym arch) +mkFootprint sym init_regs s = do + init_mems <- W4.concatSymSequence sym go (\_ a b -> return $ a ++ b) (\a b -> return $ a ++ b) [] s + return $ TraceFootprint init_regs init_mems + where + go :: MT.TraceEvent sym arch -> IO [(MM.ArchSegmentOff arch, (MT.MemOp sym (MM.ArchAddrWidth arch)))] + go = \case + MT.TraceMemEvent instr (MT.MemOpEvent mop@(MT.MemOp ptr _ _ _ _ _)) + | [(Just (instr1, _), _)] <- MT.viewMuxTree instr + , CLM.LLVMPointer reg off <- ptr + , Just{} <- W4.asNat reg + , Just{} <- W4.asConcrete off + -> return $ [(instr1, mop)] + _ -> return [] + +instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceFootprint sym arch) where + w4Serialize fp = W4S.object [ "fp_initial_regs" .= fpInitialRegs fp, "fp_mem" .= fpMem fp] + instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceEvents sym arch) where w4Serialize (TraceEvents p pre post) = do trace_pair <- PPa.w4SerializePair p $ \(TraceEventsOne rop evs) -> diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index dc010544..7f28b0c7 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -108,6 +108,8 @@ import qualified Pate.Verification.AbstractDomain as PAD import Pate.Verification.AbstractDomain ( WidenLocs(..) ) import Pate.TraceTree import qualified What4.ExprHelpers as WEH +import qualified What4.JSON as W4S + import Lang.Crucible.Simulator.SymSequence import qualified Pate.Monad.Context as PMC import Data.Functor.Const (Const(..)) @@ -473,6 +475,20 @@ addRefinementChoice nd gr0 = withTracing @"message" ("Modify Proof Node: " ++ sh choice "Clear work list (unsafe!)" $ \_ gr4 -> return $ emptyWorkList gr4 +tryWithAsms :: + [(W4.Pred sym, PEE.InnerEquivalenceError arch)] -> + (SymGroundEvalFn sym -> EquivM_ sym arch a) -> + EquivM sym arch a +tryWithAsms ((asm, err):asms) f = do + mresult <- withSatAssumption (PAs.fromPred asm) $ tryWithAsms asms f + case mresult of + Just a -> return a + Nothing -> emitWarning err >> tryWithAsms asms f +tryWithAsms [] f = withSym $ \sym -> goalSat "tryWithAsms" (W4.truePred sym) $ \res -> case res of + Unsat _ -> throwHere PEE.InvalidSMTModel + Unknown -> throwHere PEE.InconclusiveSAT + Sat evalFn -> f evalFn + getSomeGroundTrace :: PS.SimScope sym arch v -> SimBundle sym arch v -> @@ -491,19 +507,49 @@ getSomeGroundTrace scope bundle preD postCond = withSym $ \sym -> do PAs.fromPred <$> (liftIO $ W4.isEq sym zero stackbase) ptrAsserts_pred <- PAs.toPred sym (stacks_zero <> ptrAsserts) - -- first we try to see if we can make a model that doesn't - -- involve any invalid pointer operations - mevs <- goalSat "getCounterExample" ptrAsserts_pred $ \res -> case res of - Unsat _ -> emitWarning PEE.RequiresInvalidPointerOps >> return Nothing - Unknown -> emitWarning PEE.RequiresInvalidPointerOps >> return Nothing - Sat evalFn -> Just <$> getTraceFromModel scope evalFn bundle preD postCond - case mevs of - Just evs -> return evs - -- otherwise, just try to get any model - Nothing -> goalSat "getCounterExample" (W4.truePred sym) $ \res -> case res of - Unsat _ -> throwHere PEE.InvalidSMTModel - Unknown -> throwHere PEE.InconclusiveSAT - Sat evalFn -> getTraceFromModel scope evalFn bundle preD postCond + trace_constraint <- getTraceConstraint scope bundle + + tryWithAsms + [ (ptrAsserts_pred, PEE.RequiresInvalidPointerOps) + , (trace_constraint, PEE.UnsatisfiableAssumptions) + ] $ \evalFn -> + getTraceFromModel scope evalFn bundle preD postCond + +getTraceFootprint :: + forall sym arch v. + PS.SimScope sym arch v -> + SimBundle sym arch v -> + EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch)) +getTraceFootprint _scope bundle = withSym $ \sym -> PPa.forBinsC $ \bin -> do + out <- PPa.get bin (PS.simOut bundle) + in_ <- PPa.get bin (PS.simIn bundle) + let in_regs = PS.simInRegs in_ + let rop = MT.RegOp (MM.regStateMap in_regs) + let mem = PS.simOutMem out + let s = (MT.memFullSeq @_ @arch mem) + s' <- PEM.mapExpr sym concretizeWithSolver s + liftIO $ CE.mkFootprint sym rop s' + +getTraceConstraint :: + forall sym arch v. + PS.SimScope sym arch v -> + SimBundle sym arch v -> + EquivM sym arch (W4.Pred sym) +getTraceConstraint scope bundle = withSym $ \sym -> do + fps <- getTraceFootprint scope bundle + PPa.joinPatchPred (\a b -> liftIO $ W4.andPred sym a b) $ \bin -> withTracing @"binary" (Some bin) $ do + fp <- PPa.getC bin fps + (v',_eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp + emitTraceLabel @"trace_footprint" v' fp + -- FIXME: todo: get constraint from user + return $ W4.truePred sym + +instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where + type TraceNodeType '(sym,arch) "trace_footprint" = CE.TraceFootprint sym arch + type TraceNodeLabel "trace_footprint" = JSON.Value + prettyNode json _ = PP.viaShow json + nodeTags = [(Summary, \_ _ -> "TODO"), (Simplified, \_ _ -> "TODO")] + jsonNode _ json _ = return json -- | Compute a counter-example for a given predicate getTraceFromModel :: diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 93c6c2b8..04f55cae 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -24,6 +24,7 @@ module What4.JSON , W4SerializableFC , SerializableExprs , w4ToJSON + , w4ToJSONEnv , object , w4SerializeString , (.=) diff --git a/src/What4/SymSequence.hs b/src/What4/SymSequence.hs index f8af0755..8bb3eeb7 100644 --- a/src/What4/SymSequence.hs +++ b/src/What4/SymSequence.hs @@ -635,31 +635,33 @@ reverseSeq sym s_outer = evalWithFreshCache go s_outer -- using the provided combine and mux operations and -- empty value. concatSymSequence :: - forall sym m c. + forall sym m a b. IsExprBuilder sym => IO.MonadIO m => sym -> - (Pred sym -> c -> c -> m c) {-^ mux for 'c' -} -> - (c -> c -> m c) {-^ combining 'c' values -} -> - c {-^ empty c -} -> - SymSequence sym c -> - m c -concatSymSequence _sym f g c_init s_outer = getConst <$> evalWithFreshCache go s_outer + (a -> m b) {-^ produce atomic 'b' value from sequence element 'a' -} -> + (Pred sym -> b -> b -> m b) {-^ mux for 'b' -} -> + (b -> b -> m b) {-^ combining 'b' values -} -> + b {-^ empty 'b' -} -> + SymSequence sym a -> + m b +concatSymSequence _sym h f g c_init s_outer = getConst <$> evalWithFreshCache go s_outer where - go :: (SymSequence sym c -> m ((Const c) c)) -> SymSequence sym c -> m ((Const c) c) + go :: (SymSequence sym a -> m ((Const b) a)) -> SymSequence sym a -> m ((Const b) a) go rec s = fmap Const $ case s of SymSequenceNil -> return $ c_init - SymSequenceCons _ c1 sa -> do - Const c2 <- rec sa - g c1 c2 + SymSequenceCons _ a1 sa -> do + Const b2 <- rec sa + b1 <- h a1 + g b1 b2 SymSequenceAppend _ sa1 sa2 -> do - Const c1 <- rec sa1 - Const c2 <- rec sa2 - g c1 c2 + Const b1 <- rec sa1 + Const b2 <- rec sa2 + g b1 b2 SymSequenceMerge _ p' saT saF -> do - Const cT <- rec saT - Const cF <- rec saF - f p' cT cF + Const bT <- rec saT + Const bF <- rec saF + f p' bT bF -- | Pointwise comparison of two sequences. When they are (semantically) not -- the same length, the resulting predicate is False. Otherwise it is @@ -685,6 +687,7 @@ compareSymSeq sym sa sb f = do nil_b <- IO.liftIO $ isNilSymSequence sym suf_b matching_head <- concatSymSequence sym + return (\p a b -> IO.liftIO $ baseTypeIte sym p a b) (\a b -> IO.liftIO $ andPred sym a b) (truePred sym) From eafbecb0e0b239907f499aef4a316837e9f80338 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 6 Aug 2024 14:37:46 -0700 Subject: [PATCH 4/8] print footprint trace JSON as utf8-encoded --- src/Pate/Verification/Widening.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 7f28b0c7..33aa4056 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -56,6 +56,8 @@ import Data.Parameterized.Classes() import Data.Parameterized.NatRepr import Data.Parameterized.Some import qualified Data.Parameterized.Map as MapF +import qualified Data.Text.Lazy.Encoding as Text +import qualified Data.Text.Encoding.Error as Text import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4B @@ -547,7 +549,7 @@ getTraceConstraint scope bundle = withSym $ \sym -> do instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where type TraceNodeType '(sym,arch) "trace_footprint" = CE.TraceFootprint sym arch type TraceNodeLabel "trace_footprint" = JSON.Value - prettyNode json _ = PP.viaShow json + prettyNode json _ = PP.pretty $ Text.decodeUtf8With Text.lenientDecode $ JSON.encode json nodeTags = [(Summary, \_ _ -> "TODO"), (Simplified, \_ _ -> "TODO")] jsonNode _ json _ = return json From f49be5409f7c0553342779f8bf62c081ba506660 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 7 Aug 2024 16:27:17 -0700 Subject: [PATCH 5/8] accept trace constraints as input after final result --- pate.cabal | 1 + src/Pate/CLI.hs | 6 ++ src/Pate/Config.hs | 3 + src/Pate/PatchPair.hs | 20 +++- src/Pate/TraceTree.hs | 27 ++++- src/Pate/Verification/StrongestPosts.hs | 131 ++++++++++++++++++------ src/Pate/Verification/Widening.hs | 49 ++++----- src/What4/JSON.hs | 37 ++++++- 8 files changed, 208 insertions(+), 66 deletions(-) diff --git a/pate.cabal b/pate.cabal index 120c48f1..6d0a9793 100644 --- a/pate.cabal +++ b/pate.cabal @@ -161,6 +161,7 @@ library Pate.Script, Pate.Timeout, Pate.TraceTree, + Pate.TraceConstraint, Pate.ExprMappable, What4.ExprHelpers, What4.PathCondition, diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs index 0c5745b7..399466e9 100644 --- a/src/Pate/CLI.hs +++ b/src/Pate/CLI.hs @@ -97,6 +97,7 @@ mkRunConfig archLoader opts rcfg mtt = let , PC.cfgStackScopeAssume = not $ noAssumeStackScope opts , PC.cfgIgnoreWarnings = ignoreWarnings opts , PC.cfgAlwaysClassifyReturn = alwaysClassifyReturn opts + , PC.cfgTraceConstraints = traceConstraints opts } cfg = PL.RunConfig { PL.archLoader = archLoader @@ -150,6 +151,7 @@ data CLIOptions = CLIOptions , ignoreWarnings :: [String] , alwaysClassifyReturn :: Bool , preferTextInput :: Bool + , traceConstraints :: Bool } deriving (Eq, Ord, Show) printAtVerbosity @@ -474,4 +476,8 @@ cliOptions = OA.info (OA.helper <*> parser) <*> OA.switch ( OA.long "prefer-text-input" <> OA.help "Prefer taking text input over multiple choice menus where possible." + ) + <*> OA.switch + ( OA.long "add-trace-constraints" + <> OA.help "Prompt to add additional constraints when generating traces." ) \ No newline at end of file diff --git a/src/Pate/Config.hs b/src/Pate/Config.hs index 9cfcf94d..a0c66b0e 100644 --- a/src/Pate/Config.hs +++ b/src/Pate/Config.hs @@ -290,6 +290,8 @@ data VerificationConfig validRepr = , cfgPreferTextInput :: Bool -- ^ modifies some menus to take string input instead of providing -- a menu selection + , cfgTraceConstraints :: Bool + -- ^ flag to determine if the user should be prompted to add constraints to traces } @@ -317,4 +319,5 @@ defaultVerificationCfg = , cfgIgnoreWarnings = [] , cfgAlwaysClassifyReturn = False , cfgPreferTextInput = False + , cfgTraceConstraints = False } diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index 41a8b102..f594bcc0 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -101,6 +101,7 @@ import qualified What4.JSON as W4S import What4.JSON import Control.Monad.State.Strict (StateT (..), put) import qualified Control.Monad.State.Strict as CMS +import Control.Applicative ( (<|>) ) -- | A pair of values indexed based on which binary they are associated with (either the -- original binary or the patched binary). @@ -612,4 +613,21 @@ w4SerializePair ppair f = case ppair of return $ JSON.object ["patched" JSON..= p_v] instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (PatchPair f) where - w4Serialize ppair = w4SerializePair ppair w4SerializeF \ No newline at end of file + w4Serialize ppair = w4SerializePair ppair w4SerializeF + + +instance (forall bin. PB.KnownBinary bin => W4Deserializable sym (f bin)) => W4Deserializable sym (PatchPair f) where + w4Deserialize v = do + JSON.Object o <- return v + let + case_pair = do + (vo :: f PB.Original) <- o .: "original" + (vp :: f PB.Patched) <- o .: "patched" + return $ PatchPair vo vp + case_orig = do + (vo :: f PB.Original) <- o .: "original" + return $ PatchPairOriginal vo + case_patched = do + (vp :: f PB.Patched) <- o .: "patched" + return $ PatchPairPatched vp + case_pair <|> case_orig <|> case_patched \ No newline at end of file diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index 95b10317..94aadbf2 100644 --- a/src/Pate/TraceTree.hs +++ b/src/Pate/TraceTree.hs @@ -120,6 +120,7 @@ module Pate.TraceTree ( , waitingForChoiceInput , chooseInput , chooseInputFromList + , chooseInput_ ) where import GHC.TypeLits ( Symbol, KnownSymbol ) @@ -1050,7 +1051,7 @@ instance PP.Pretty InputChoiceError where data InputChoice (k :: l) nm where InputChoice :: (IsTraceNode k nm) => - { inputChoiceParse :: String -> Either InputChoiceError (TraceNodeLabel nm, TraceNodeType k nm) + { inputChoiceParse :: String -> IO (Either InputChoiceError (TraceNodeLabel nm, TraceNodeType k nm)) , inputChoicePut :: TraceNodeLabel nm -> TraceNodeType k nm -> IO Bool -- returns false if input has already been provided , inputChoiceValue :: IO (Maybe (TraceNodeLabel nm, TraceNodeType k nm)) } -> InputChoice k nm @@ -1063,7 +1064,7 @@ waitingForChoiceInput ic = inputChoiceValue ic >>= \case giveChoiceInput :: InputChoice k nm -> String -> IO (Maybe InputChoiceError) giveChoiceInput ic input = waitingForChoiceInput ic >>= \case False -> return $ Just InputChoiceAlreadyMade - True -> case inputChoiceParse ic input of + True -> inputChoiceParse ic input >>= \case Right (lbl, v) -> inputChoicePut ic lbl v >>= \case True -> return Nothing False -> return $ Just InputChoiceAlreadyMade @@ -1097,12 +1098,28 @@ chooseInputFromList :: m (Maybe a) chooseInputFromList treenm opts = do let parseInput s = case findIndex (\(s',_) -> s == s') opts of - Just idx -> Right (s, idx) - Nothing -> Left (InputChoiceError "Invalid input. Valid options:" (map fst opts)) + Just idx -> return $ Right (s, idx) + Nothing -> return $ Left (InputChoiceError "Invalid input. Valid options:" (map fst opts)) chooseInput @"opt_index" treenm parseInput >>= \case Just (_, idx) -> return $ Just $ (snd (opts !! idx)) Nothing -> return Nothing +chooseInput_ :: + forall nm_choice k m e. + IsTreeBuilder k e m => + IsTraceNode k nm_choice => + Default (TraceNodeLabel nm_choice) => + IO.MonadUnliftIO m => + String -> + (String -> IO (Either InputChoiceError (TraceNodeType k nm_choice))) -> + m (Maybe (TraceNodeType k nm_choice)) +chooseInput_ treenm parseInput = do + let parse s = parseInput s >>= \case + Left err -> return $ Left err + Right a -> return $ Right (def,a) + fmap snd <$> chooseInput @nm_choice treenm parse + + -- | Take user input as a string. Returns 'Nothing' in the case where the trace tree -- is not running interactively. Otherwise, blocks the current thread until -- valid input is provided. @@ -1112,7 +1129,7 @@ chooseInput :: IsTraceNode k nm_choice => IO.MonadUnliftIO m => String -> - (String -> Either InputChoiceError (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) -> + (String -> IO (Either InputChoiceError (TraceNodeLabel nm_choice, TraceNodeType k nm_choice))) -> m (Maybe (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) chooseInput treenm parseInput = do builder <- getTreeBuilder diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index ddbf5e66..5bf35097 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -109,6 +109,7 @@ import qualified Pate.SimulatorRegisters as PSR import qualified Pate.Verification.StrongestPosts.CounterExample as CE import qualified Pate.Register.Traversal as PRt import Pate.Discovery.PLT (extraJumpClassifier, ExtraJumps(..), ExtraJumpTarget(..)) +import qualified Pate.TraceConstraint as PTC import Pate.TraceTree import qualified Pate.Verification.Validity as PVV @@ -860,37 +861,104 @@ clearTrivialCondition nd condK pg = case getCondition pg nd ConditionEquiv of return pg1 Nothing -> return pg -showFinalResult :: PairGraph sym arch -> EquivM sym arch () +-- | Context needed to re-generate traces when adding trace constraints +data IntermediateEqCond sym arch v = + IntermediateEqCond + { ieqBundle :: SimBundle sym arch v + , ieqFootprints:: PPa.PatchPairC (CE.TraceFootprint sym arch) + , ieqEnv :: W4S.ExprEnv sym + , ieqAsms :: PAS.AssumptionSet sym + , ieqCond :: W4.Pred sym + , ieqDom :: AbstractDomain sym arch v + } + +data EqCondCollector sym arch = EqCondCollector + { eqCondFinals :: Map.Map (GraphNode arch) (FinalEquivCond sym arch) + , eqCondInterims :: Map.Map (GraphNode arch) (PS.SimSpec sym arch (IntermediateEqCond sym arch)) + , eqCondConstraints :: PTC.TraceConstraintMap sym arch + } + +getExprEnvs :: EqCondCollector sym arch -> Map.Map (GraphNode arch) (W4S.ExprEnv sym) +getExprEnvs st = fmap (\spec -> PS.viewSpecBody spec ieqEnv) (eqCondInterims st) + +showFinalResult :: forall sym arch. PairGraph sym arch -> EquivM sym arch () showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do - subTree @"node" "Observable Counter-examples" $ do - forM_ (Map.toList (pairGraphObservableReports pg0)) $ \(nd,report) -> - subTrace (GraphNode nd) $ - emitTrace @"observable_result" (CE.ObservableCheckCounterexample report) - eq_conds <- fmap catMaybes $ subTree @"node" "Assumed Equivalence Conditions" $ do - - forM (getAllNodes pg0) $ \nd -> do + st <- go (EqCondCollector Map.empty Map.empty (PTC.TraceConstraintMap Map.empty)) + add_constraints <- asks (PCfg.cfgTraceConstraints . envConfig) + case add_constraints of + True -> + let loop st_ = chooseBool "Regenerate result with new trace constraints?" >>= \case + True -> do + tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (getExprEnvs st_) + go (st_ {eqCondConstraints = tcs}) >>= loop + False -> return () + in loop st + False -> return () + + where + mkEqCond :: + EqCondCollector sym arch -> + GraphNode arch -> + NodeBuilderT '(sym,arch) "node" (EquivM_ sym arch) (EqCondCollector sym arch) + mkEqCond rs nd = do pg <- lift $ clearTrivialCondition nd ConditionEquiv pg0 - case getCondition pg nd ConditionEquiv of - Just cond_spec -> subTrace nd $ do - s <- withFreshScope (graphNodeBlocks nd) $ \scope -> do - (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec - (tr, _) <- withGraphNode scope nd pg $ \bundle d -> do - cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond - eqCond_pred <- PEC.toPred sym cond_simplified - (mtraceT, mtraceF) <- getTracesForPred scope bundle d eqCond_pred - case (mtraceT, mtraceF) of - (Just traceT, Just traceF) -> do - cond_pretty <- PSi.applySimpStrategy PSi.prettySimplifier eqCond_pred - return $ (Just (FinalEquivCond cond_pretty traceT traceF), pg) - _ -> return (Nothing, pg) - return $ (Const (fmap (nd,) tr)) - return $ PS.viewSpec s (\_ -> getConst) - Nothing -> return Nothing - let result = pairGraphComputeVerdict pg0 - emitTrace @"equivalence_result" result - let eq_conds_map = Map.fromList eq_conds - let toplevel_result = FinalResult result (pairGraphObservableReports pg0) eq_conds_map - emitTrace @"toplevel_result" toplevel_result + let PTC.TraceConstraintMap tcm = eqCondConstraints rs + + + let + rest :: forall v. PS.SimScope sym arch v -> IntermediateEqCond sym arch v -> EquivM_ sym arch (Maybe (FinalEquivCond sym arch)) + rest scope (IntermediateEqCond bundle fps _ _ cond d) = withSym $ \sym -> do + trace_constraint <- case Map.lookup nd tcm of + Just tc -> IO.liftIO $ PTC.constraintToPred sym tc + Nothing -> return $ W4.truePred sym + mres <- withSatAssumption (PAS.fromPred trace_constraint) $ do + (mtraceT, mtraceF) <- getTracesForPred scope bundle d cond + case (mtraceT, mtraceF) of + (Just traceT, Just traceF) -> do + cond_pretty <- PSi.applySimpStrategy PSi.prettySimplifier cond + return $ Just (FinalEquivCond cond_pretty traceT traceF fps) + _ -> return Nothing + case mres of + Just res -> return res + Nothing -> emitWarning PEE.UnsatisfiableAssumptions >> return Nothing + + case Map.lookup nd (eqCondInterims rs) of + Just ieqcspec -> subTrace nd $ PS.viewSpec ieqcspec $ \scope ieqc -> withAssumptionSet (ieqAsms ieqc) $ do + rest scope ieqc >>= \case + Just fcond -> return (rs { eqCondFinals = Map.insert nd fcond (eqCondFinals rs) }) + Nothing -> return rs + Nothing -> case getCondition pg nd ConditionEquiv of + Just cond_spec -> subTrace nd $ withSym $ \sym -> do + spec <- withFreshScope (graphNodeBlocks nd) $ \scope -> fmap PS.WithScope $ do + (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec + fmap fst $ withGraphNode scope nd pg $ \bundle d -> do + cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond + eqCond_pred <- PEC.toPred sym cond_simplified + (fps, eenv) <- getTraceFootprint scope bundle + asms <- currentAsm + let ieqc = IntermediateEqCond bundle fps eenv asms eqCond_pred d + let interims = Map.insert nd (PS.mkSimSpec scope ieqc) (eqCondInterims rs) + rest scope ieqc >>= \case + Just fcond -> return (rs { eqCondFinals = Map.insert nd fcond (eqCondFinals rs), eqCondInterims = interims }, pg) + Nothing -> return (rs { eqCondInterims = interims }, pg) + return $ PS.viewSpecBody spec PS.unWS + Nothing -> return rs + + go :: EqCondCollector sym arch -> EquivM sym arch (EqCondCollector sym arch) + go rs = do + subTree @"node" "Observable Counter-examples" $ do + forM_ (Map.toList (pairGraphObservableReports pg0)) $ \(nd,report) -> + subTrace (GraphNode nd) $ + emitTrace @"observable_result" (CE.ObservableCheckCounterexample report) + + rs' <- subTree @"node" "Assumed Equivalence Conditions" $ + foldM mkEqCond (rs { eqCondFinals = Map.empty }) (getAllNodes pg0) + let result = pairGraphComputeVerdict pg0 + emitTrace @"equivalence_result" result + + let toplevel_result = FinalResult result (pairGraphObservableReports pg0) (eqCondFinals rs') + emitTrace @"toplevel_result" toplevel_result + return rs' data FinalResult sym arch = FinalResult { @@ -904,6 +972,7 @@ data FinalEquivCond sym arch = FinalEquivCond _finEqCondPred :: W4.Pred sym , _finEqCondTraceTrue :: CE.TraceEvents sym arch , _finEqCondTraceFalse :: CE.TraceEvents sym arch + , _finEqFootprints :: PPa.PatchPairC (CE.TraceFootprint sym arch) } @@ -915,8 +984,8 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalR W4S.object [ "eq_status" W4S..= st, "observable_counterexamples" W4S..= obs, "eq_conditions" W4S..= conds ] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalEquivCond sym arch) where - w4Serialize (FinalEquivCond p trT trF) = do - W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF ] + w4Serialize (FinalEquivCond p trT trF fps) = do + W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF, "trace_footprint" W4S..= fps ] instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "toplevel_result" where diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 33aa4056..bdc32d70 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -33,6 +33,7 @@ module Pate.Verification.Widening , getTraceFromModel , addToEquivCondition , strengthenPredicate + , getTraceFootprint ) where import GHC.Stack @@ -88,6 +89,7 @@ import qualified Pate.Proof.Instances () import qualified Pate.ExprMappable as PEM import qualified Pate.Solver as PSo import qualified Pate.Verification.Simplify as PSi +import qualified Pate.TraceConstraint as PTC import Pate.Monad import Pate.Monad.PairGraph @@ -124,6 +126,7 @@ import qualified Prettyprinter as PP import qualified What4.Expr.GroundEval as W4 import qualified Lang.Crucible.Utils.MuxTree as MT import Pate.Verification.Domain (universalDomain) +import qualified Data.Parameterized.TraversableF as TF -- | Generate a fresh abstract domain value for the given graph node. -- This should represent the most information we can ever possibly @@ -507,44 +510,36 @@ getSomeGroundTrace scope bundle preD postCond = withSym $ \sym -> do let stackbase = PS.unSE $ PS.simStackBase (PS.simInState in_) zero <- liftIO $ W4.bvLit sym CT.knownRepr (BVS.mkBV CT.knownRepr 0) PAs.fromPred <$> (liftIO $ W4.isEq sym zero stackbase) - + ptrAsserts_pred <- PAs.toPred sym (stacks_zero <> ptrAsserts) - trace_constraint <- getTraceConstraint scope bundle - tryWithAsms + tr <- tryWithAsms [ (ptrAsserts_pred, PEE.RequiresInvalidPointerOps) - , (trace_constraint, PEE.UnsatisfiableAssumptions) ] $ \evalFn -> getTraceFromModel scope evalFn bundle preD postCond + return tr + getTraceFootprint :: forall sym arch v. PS.SimScope sym arch v -> SimBundle sym arch v -> - EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch)) -getTraceFootprint _scope bundle = withSym $ \sym -> PPa.forBinsC $ \bin -> do - out <- PPa.get bin (PS.simOut bundle) - in_ <- PPa.get bin (PS.simIn bundle) - let in_regs = PS.simInRegs in_ - let rop = MT.RegOp (MM.regStateMap in_regs) - let mem = PS.simOutMem out - let s = (MT.memFullSeq @_ @arch mem) - s' <- PEM.mapExpr sym concretizeWithSolver s - liftIO $ CE.mkFootprint sym rop s' - -getTraceConstraint :: - forall sym arch v. - PS.SimScope sym arch v -> - SimBundle sym arch v -> - EquivM sym arch (W4.Pred sym) -getTraceConstraint scope bundle = withSym $ \sym -> do - fps <- getTraceFootprint scope bundle - PPa.joinPatchPred (\a b -> liftIO $ W4.andPred sym a b) $ \bin -> withTracing @"binary" (Some bin) $ do - fp <- PPa.getC bin fps - (v',_eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp + EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch), W4S.ExprEnv sym) +getTraceFootprint _scope bundle = withSym $ \sym -> do + fps <- PPa.forBinsC $ \bin -> withTracing @"binary" (Some bin) $ do + out <- PPa.get bin (PS.simOut bundle) + in_ <- PPa.get bin (PS.simIn bundle) + let in_regs = PS.simInRegs in_ + let rop = MT.RegOp (MM.regStateMap in_regs) + let mem = PS.simOutMem out + let s = (MT.memFullSeq @_ @arch mem) + s' <- PEM.mapExpr sym concretizeWithSolver s + fp <- liftIO $ CE.mkFootprint sym rop s' + (v',eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp emitTraceLabel @"trace_footprint" v' fp - -- FIXME: todo: get constraint from user - return $ W4.truePred sym + return (fp, eenv) + env <- PPa.joinPatchPred (\(_, a) (_, b) -> return $ W4S.mergeEnvs a b) $ \bin -> (PPa.getC bin fps) + return $ (TF.fmapF (\(Const(a,_)) -> Const a) fps, env) instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where type TraceNodeType '(sym,arch) "trace_footprint" = CE.TraceFootprint sym arch diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 04f55cae..fb9adf9a 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -30,6 +30,11 @@ module What4.JSON , (.=) , (.==) , (.=~) + , ExprEnv + , mergeEnvs + , W4Deserializable(..) + , jsonToW4 + , (.:) ) where import Control.Monad.State (MonadState (..), State, modify, evalState, runState) @@ -38,6 +43,7 @@ import qualified Data.Map.Ordered as OMap import Data.List ( stripPrefix ) import Data.Maybe ( mapMaybe ) import Data.Map (Map) +import qualified Data.Map.Merge.Strict as Map import Data.Text (Text) import Data.Data (Proxy(..), Typeable) import qualified Data.Aeson as JSON @@ -118,6 +124,15 @@ w4ToJSON sym a = do newtype ExprEnv sym = ExprEnv (Map Integer (Some (W4.SymExpr sym))) +mergeEnvs :: TestEquality (W4.SymExpr sym) => ExprEnv sym -> ExprEnv sym -> ExprEnv sym +mergeEnvs (ExprEnv env1) (ExprEnv env2) = ExprEnv ( + Map.merge + Map.preserveMissing + Map.preserveMissing + (Map.zipWithMatched (\_ (Some e1) (Some e2) -> (case testEquality e1 e2 of Just Refl -> Some e1; Nothing -> error $ "Unexpected term hash clash"))) + env1 + env2) + -- | Extract expressions with annotations cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> ExprEnv sym cacheToEnv sym (ExprCache m) = ExprEnv $ Map.fromList $ mapMaybe go (Map.keys m) @@ -304,6 +319,13 @@ instance MonadFail (W4DS sym) where class W4Deserializable sym a where w4Deserialize :: JSON.Value -> W4DS sym a + default w4Deserialize :: JSON.FromJSON a => JSON.Value -> W4DS sym a + w4Deserialize v = fromJSON v + +instance W4Deserializable sym Integer +instance W4Deserializable sym Bool +instance W4Deserializable sym () + jsonToW4 :: (W4Deserializable sym a, W4.IsExprBuilder sym) => sym -> ExprEnv sym -> JSON.Value -> IO (Either String a) jsonToW4 sym env v = do let wenv = W4DSEnv env sym @@ -320,9 +342,20 @@ liftParser f v = case JSON.parse f v of JSON.Success a -> return a JSON.Error msg -> fail msg -(.:) :: JSON.FromJSON a => JSON.Object -> JSON.Key -> W4DS sym a -(.:) o = liftParser ((JSON..:) o) +(.:) :: W4Deserializable sym a => JSON.Object -> JSON.Key -> W4DS sym a +(.:) o k = do + (v :: JSON.Value) <- liftParser ((JSON..:) o) k + w4Deserialize v + +instance (W4Deserializable sym a, W4Deserializable sym b) => W4Deserializable sym (a, b) where + w4Deserialize v = do + JSON.Object o <- return v + v1 <- o .: "fst" + v2 <- o .: "snd" + return (v1,v2) +instance W4Deserializable sym f => W4Deserializable sym (Const f x) where + w4Deserialize v = Const <$> w4Deserialize v newtype ToDeserializable sym tp = ToDeserializable { _unDS :: W4.SymExpr sym tp } From f19bd49d3e7cfcf7a34b3bc7cf816e4303d67c4a Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Aug 2024 12:16:54 -0700 Subject: [PATCH 6/8] work-in-progress for constraint deserialization --- src/Pate/PatchPair.hs | 2 +- src/Pate/TraceConstraint.hs | 178 ++++++++++++++++++++++++ src/Pate/Verification/StrongestPosts.hs | 2 +- src/What4/JSON.hs | 88 ++++-------- 4 files changed, 206 insertions(+), 64 deletions(-) create mode 100644 src/Pate/TraceConstraint.hs diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index f594bcc0..da0fb5bf 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -617,7 +617,7 @@ instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (PatchPair f) where instance (forall bin. PB.KnownBinary bin => W4Deserializable sym (f bin)) => W4Deserializable sym (PatchPair f) where - w4Deserialize v = do + w4Deserialize_ v = do JSON.Object o <- return v let case_pair = do diff --git a/src/Pate/TraceConstraint.hs b/src/Pate/TraceConstraint.hs new file mode 100644 index 00000000..b362724f --- /dev/null +++ b/src/Pate/TraceConstraint.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GADTs #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} + +module Pate.TraceConstraint + ( + TraceConstraint(..) + , readDeserializable + , constraintToPred + , TraceConstraintMap(..) + , readConstraintMap + ) where + +import Prelude hiding (EQ) + +import qualified Control.Monad.IO.Unlift as IO +import Control.Monad ( forM ) +import Control.Monad.Except +import Control.Monad.Trans +import qualified Data.Aeson as JSON +import qualified Data.Aeson.Types as JSON + +import qualified Data.Text.Lazy.Encoding as Text +import qualified Data.Text.Encoding.Error as Text +import qualified Data.Kind as DK +import Data.String +import Data.Map ( Map ) +import qualified Data.Map as Map + +import qualified Prettyprinter as PP + +import qualified What4.Interface as W4 +import qualified What4.Concrete as W4 + +import qualified Pate.Arch as PA +import qualified Pate.PatchPair as PPa +import Pate.Verification.PairGraph.Node +import Pate.TraceTree +import qualified What4.JSON as W4S +import What4.JSON ( (.:) ) +import Data.Parameterized.Some (Some(..)) +import qualified Data.BitVector.Sized as BVS +import qualified Numeric as Num + +newtype TraceIdentifier = TraceIdentifier String + deriving (Eq, Ord, IsString) + +data ConstraintOp = LTs | LTu | GTs | GTu | LEs | LEu | GEs | GEu | NEQ | EQ + deriving (Show, Read) + +data TraceConstraint sym = forall tp. TraceConstraint + { tcVar :: W4.SymExpr sym tp + , tcOp :: ConstraintOp + , tcConst :: W4.ConcreteVal tp + } + +instance forall sym. W4S.W4Deserializable sym (TraceConstraint sym) where + w4Deserialize_ v | W4S.SymDeserializable{} <- W4S.symDeserializable @sym = do + JSON.Object o <- return v + (Some (var :: W4.SymExpr sym tp)) <- o .: "var" + (opJSON :: JSON.Value) <- o .: "op" + (op :: ConstraintOp) <- W4S.readJSON opJSON + case W4.exprType var of + W4.BaseBVRepr w -> do + (cS :: String) <- o .: "const" + ((c :: Integer),""):_ <- return $ Num.readDec cS + case (BVS.mkBVUnsigned w c) of + Just bv -> return $ TraceConstraint var op (W4.ConcreteBV w bv) + Nothing -> fail "Unexpected integer size" + _ -> fail "Unsupported expression type" + +{- +instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch) "trace_constraint" where + type TraceNodeType '(sym,arch) "trace_constraint" = TraceConstraint sym + prettyNode _ _ = PP.pretty ("TODO" :: String) + nodeTags = mkTags @'(sym,arch) @"trace_constraint" [Summary, Simplified] +-} + +constraintToPred :: + forall sym. + W4.IsExprBuilder sym => + sym -> + TraceConstraint sym -> + IO (W4.Pred sym) +constraintToPred sym (TraceConstraint var op c) = case W4.exprType var of + W4.BaseBVRepr w -> do + let W4.ConcreteBV _ bv = c + bvSym <- W4.bvLit sym w bv + let go :: (forall w. 1 W4.<= w => sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> IO (W4.Pred sym) + go f = f sym var bvSym + case op of + LTs -> go W4.bvSlt + LTu -> go W4.bvUlt + LEs -> go W4.bvSle + LEu -> go W4.bvUle + EQ -> go W4.isEq + _ -> fail "err" + + _ -> fail "Unexpected constraint " + + + +newtype TraceConstraintMap sym arch = + TraceConstraintMap (Map (GraphNode arch) (TraceConstraint sym)) + + +instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch :: DK.Type) "trace_constraint_map" where + type TraceNodeType '(sym,arch) "trace_constraint_map" = TraceConstraintMap sym arch + prettyNode _ _ = PP.pretty ("TODO" :: String) + nodeTags = mkTags @'(sym,arch) @"trace_constraint_map" [Summary, Simplified] + +readConstraintMap :: + W4.IsExprBuilder sym => + IsTreeBuilder '(sym,arch) e m => + IO.MonadUnliftIO m => + PA.ValidArch arch => + sym -> + String {- ^ input prompt -} -> + [(GraphNode arch,W4S.ExprEnv sym)] -> + m (TraceConstraintMap sym arch) +readConstraintMap sym msg ndEnvs = do + let parse s = case JSON.eitherDecode (fromString s) of + Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err] + Right (v :: JSON.Value) -> runExceptT $ do + nodes <- runJSON $ do + JSON.Object o <- return v + (nodes :: [JSON.Value]) <- o JSON..: "trace_constraints" + return nodes + let nds = zip ndEnvs nodes + fmap (TraceConstraintMap . Map.fromList) $ forM nds $ \((nd, env), constraint_json) -> do + (lift $ W4S.jsonToW4 sym env constraint_json) >>= \case + Left err -> throwError $ InputChoiceError "Failed to parse value" [err] + Right a -> return (nd, a) + chooseInput_ @"trace_constraint_map" msg parse >>= \case + Nothing -> IO.liftIO $ fail "Unexpected trace map read" + Just a -> return a + + +runJSON :: JSON.Parser a -> ExceptT InputChoiceError IO a +runJSON p = ExceptT $ case JSON.parse (\() -> p) () of + JSON.Success a -> return $ Right a + JSON.Error err -> return $ Left $ InputChoiceError "Failed to parse value" [err] + + + +-- FIXME: Move +readDeserializable :: + forall nm_choice sym k e m. + W4S.W4Deserializable sym (TraceNodeLabel nm_choice, TraceNodeType k nm_choice) => + W4.IsExprBuilder sym => + IsTreeBuilder k e m => + IsTraceNode k nm_choice => + IO.MonadUnliftIO m => + sym -> + W4S.ExprEnv sym -> + String -> + m (Maybe (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) +readDeserializable sym env msg = do + let parse s = case JSON.eitherDecode (fromString s) of + Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err] + Right (v :: JSON.Value) -> W4S.jsonToW4 sym env v >>= \case + Left err -> return $ Left $ InputChoiceError "Failed to parse value" [err] + Right a -> return $ Right a + chooseInput @nm_choice msg parse diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 5bf35097..7aa66c09 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -889,7 +889,7 @@ showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do True -> let loop st_ = chooseBool "Regenerate result with new trace constraints?" >>= \case True -> do - tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (getExprEnvs st_) + tcs <- PTC.readConstraintMap sym "Waiting for constraints.." (Map.toAscList (getExprEnvs st_)) go (st_ {eqCondConstraints = tcs}) >>= loop False -> return () in loop st diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index fb9adf9a..2a13bc03 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -34,7 +34,10 @@ module What4.JSON , mergeEnvs , W4Deserializable(..) , jsonToW4 + , readJSON , (.:) + , SymDeserializable(..) + , symDeserializable ) where import Control.Monad.State (MonadState (..), State, modify, evalState, runState) @@ -317,11 +320,16 @@ instance MonadFail (W4DS sym) where fail msg = throwError msg class W4Deserializable sym a where - w4Deserialize :: JSON.Value -> W4DS sym a + w4Deserialize_ :: W4.IsExprBuilder sym => JSON.Value -> W4DS sym a - default w4Deserialize :: JSON.FromJSON a => JSON.Value -> W4DS sym a - w4Deserialize v = fromJSON v + default w4Deserialize_ :: (W4.IsExprBuilder sym, JSON.FromJSON a) => JSON.Value -> W4DS sym a + w4Deserialize_ v = fromJSON v +w4Deserialize :: W4Deserializable sym a => JSON.Value -> W4DS sym a +w4Deserialize v = ask >>= \W4DSEnv{} -> w4Deserialize_ v + +instance W4Deserializable sym JSON.Value +instance W4Deserializable sym String instance W4Deserializable sym Integer instance W4Deserializable sym Bool instance W4Deserializable sym () @@ -342,25 +350,31 @@ liftParser f v = case JSON.parse f v of JSON.Success a -> return a JSON.Error msg -> fail msg +readJSON :: forall a sym. Read a => JSON.Value -> W4DS sym a +readJSON v = do + (vS :: String) <- fromJSON v + (a :: a,""):_ <- return $ readsPrec 0 vS + return a + (.:) :: W4Deserializable sym a => JSON.Object -> JSON.Key -> W4DS sym a (.:) o k = do (v :: JSON.Value) <- liftParser ((JSON..:) o) k w4Deserialize v instance (W4Deserializable sym a, W4Deserializable sym b) => W4Deserializable sym (a, b) where - w4Deserialize v = do + w4Deserialize_ v = do JSON.Object o <- return v v1 <- o .: "fst" v2 <- o .: "snd" return (v1,v2) instance W4Deserializable sym f => W4Deserializable sym (Const f x) where - w4Deserialize v = Const <$> w4Deserialize v + w4Deserialize_ v = Const <$> w4Deserialize v newtype ToDeserializable sym tp = ToDeserializable { _unDS :: W4.SymExpr sym tp } instance W4Deserializable sym (Some (ToDeserializable sym)) where - w4Deserialize v = fmap (\(Some x) -> Some (ToDeserializable x)) $ ask >>= \W4DSEnv{} -> asks w4dsSym >>= \sym -> do + w4Deserialize_ v = fmap (\(Some x) -> Some (ToDeserializable x)) $ asks w4dsSym >>= \sym -> do (i :: Integer) <- fromJSON v Some <$> (liftIO $ W4.intLit sym i) <|> do @@ -383,70 +397,20 @@ instance W4Deserializable sym (Some (ToDeserializable sym)) where return $ Some e instance forall tp sym. KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (ToDeserializable sym tp) where - w4Deserialize v = ask >>= \W4DSEnv{} -> do + w4Deserialize_ v = do Some (ToDeserializable e :: ToDeserializable sym tp') <- w4Deserialize v case testEquality (knownRepr @_ @_ @tp) (W4.exprType e) of Just Refl -> return $ ToDeserializable e Nothing -> fail $ "Unexpected type: " ++ show (W4.exprType e) -newtype SymDeserializable sym f = SymDeserializable (forall tp a. ((KnownRepr W4.BaseTypeRepr tp => W4Deserializable sym (f tp)) => a) -> a) +-- | Small hack to pretend that W4.SymExpr has a W4Deserializable instance, which haskell's +-- type class mechanism doesn't support because W4.SymExpr is a type family +data SymDeserializable sym f = W4Deserializable sym (Some f) => SymDeserializable symDeserializable :: forall sym. - sym -> SymDeserializable sym (W4.SymExpr sym) -symDeserializable _sym = unsafeCoerce r +symDeserializable = unsafeCoerce r where r :: SymDeserializable sym (ToDeserializable sym) - r = SymDeserializable (\a -> a) - -{- -class (TestEquality g, KnownRepr g k) => W4DeserializableF sym (f :: k -> Type) where - withDeserializable :: Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a - - default withDeserializable :: W4Deserializable sym (f tp) => Proxy sym -> p f -> q tp -> (W4Deserializable sym (f tp) => a) -> a - withDeserializable _ _ _ x = x - - w4DeserializeF :: forall tp. JSON.Value -> W4DS sym (f tp) - w4DeserializeF x = withDeserializable (Proxy :: Proxy sym) (Proxy :: Proxy f) (Proxy :: Proxy tp) (w4Deserialize x) --} - -{- -data WrappedBuilder sym = - WrappedBuilder { wSym :: sym, wEnv :: MapF (W4.SymAnnotation sym) (W4.SymExpr sym)} - -data WSymExpr sym tp where - WSymExpr :: W4.SymAnnotation sym tp -> WSymExpr sym tp - WConc :: W4.ConcreteVal tp -> WSymExpr sym tp - - -instance JSON.FromJSON (Some (W4.SymAnnotation sym)) => JSON.FromJSON (Some (WSymExpr sym)) where - parseJSON v = do - JSON.Object o <- return v - go o - where - go o = do - Some (ann :: W4.SymAnnotation sym tp) <- o JSON..: "ann" - return $ Some (WSymExpr ann) - <|> do - (i :: Integer) <- o JSON..: "conc_int" - return $ Some $ WConc (W4.ConcreteInteger i) - <|> do - (i :: Bool) <- o JSON..: "conc_bool" - return $ Some $ WConc (W4.ConcreteBool i) - <|> fail "Unsupported value" - - -instance JSON.ToJSON (W4.SymAnnotation sym tp) => JSON.ToJSON (WSymExpr sym tp) where - toJSON = - - - -instance forall sym sym'. (sym ~ WrappedBuilder sym', W4.IsExprBuilder sym', W4Deserializable sym (Some (W4.SymAnnotation sym'))) => W4Deserializable sym (Some (WSymExpr sym)) where - w4Deserialize v = do - Some (ann :: W4.SymAnnotation sym' tp') <- w4Deserialize v - sym <- asks w4dsSym - case MapF.lookup ann (wEnv sym) of - Just e -> return $ Some $ WSymExpr e - Nothing -> fail "Missing annotation" --} + r = SymDeserializable \ No newline at end of file From b59897d76b1fd5f8c981d8d6bb765e59c635af73 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Aug 2024 16:45:53 -0700 Subject: [PATCH 7/8] finalize trace constraint parsing: * takes an ordered list of lists of triples: var-op-const * identifiers are now somewhat more stable, as they are computed as an offset from some initial hash * don't include trace footprints in tracetree by default - these are part of the toplevel output currently - can still be inspected via the "debug" tag * support "negated" comparison ops (i.e. GE, GT, NEQ) --- src/Pate/TraceConstraint.hs | 61 ++++++------------- src/Pate/Verification/StrongestPosts.hs | 8 ++- .../StrongestPosts/CounterExample.hs | 12 +++- src/Pate/Verification/Widening.hs | 19 +----- src/What4/JSON.hs | 30 ++++++--- tests/integration/packet/packet.exp | 38 ++++++++++-- 6 files changed, 95 insertions(+), 73 deletions(-) diff --git a/src/Pate/TraceConstraint.hs b/src/Pate/TraceConstraint.hs index b362724f..4edabe16 100644 --- a/src/Pate/TraceConstraint.hs +++ b/src/Pate/TraceConstraint.hs @@ -18,8 +18,7 @@ module Pate.TraceConstraint ( - TraceConstraint(..) - , readDeserializable + TraceConstraint , constraintToPred , TraceConstraintMap(..) , readConstraintMap @@ -81,14 +80,7 @@ instance forall sym. W4S.W4Deserializable sym (TraceConstraint sym) where case (BVS.mkBVUnsigned w c) of Just bv -> return $ TraceConstraint var op (W4.ConcreteBV w bv) Nothing -> fail "Unexpected integer size" - _ -> fail "Unsupported expression type" - -{- -instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch) "trace_constraint" where - type TraceNodeType '(sym,arch) "trace_constraint" = TraceConstraint sym - prettyNode _ _ = PP.pretty ("TODO" :: String) - nodeTags = mkTags @'(sym,arch) @"trace_constraint" [Summary, Simplified] --} + _ -> fail ("Unsupported expression type:" ++ show (W4.exprType var)) constraintToPred :: forall sym. @@ -102,14 +94,19 @@ constraintToPred sym (TraceConstraint var op c) = case W4.exprType var of bvSym <- W4.bvLit sym w bv let go :: (forall w. 1 W4.<= w => sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> IO (W4.Pred sym) go f = f sym var bvSym + let goNot :: (forall w. 1 W4.<= w => sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) -> IO (W4.Pred sym) + goNot f = f sym var bvSym >>= W4.notPred sym case op of LTs -> go W4.bvSlt LTu -> go W4.bvUlt LEs -> go W4.bvSle LEu -> go W4.bvUle EQ -> go W4.isEq - _ -> fail "err" - + GTs -> goNot W4.bvSle + GTu -> goNot W4.bvUle + GEs -> goNot W4.bvSlt + GEu -> goNot W4.bvUlt + NEQ -> goNot W4.isEq _ -> fail "Unexpected constraint " @@ -121,7 +118,7 @@ newtype TraceConstraintMap sym arch = instance forall sym arch. IsTraceNode '(sym :: DK.Type,arch :: DK.Type) "trace_constraint_map" where type TraceNodeType '(sym,arch) "trace_constraint_map" = TraceConstraintMap sym arch prettyNode _ _ = PP.pretty ("TODO" :: String) - nodeTags = mkTags @'(sym,arch) @"trace_constraint_map" [Summary, Simplified] + nodeTags = [] readConstraintMap :: W4.IsExprBuilder sym => @@ -136,15 +133,13 @@ readConstraintMap sym msg ndEnvs = do let parse s = case JSON.eitherDecode (fromString s) of Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err] Right (v :: JSON.Value) -> runExceptT $ do - nodes <- runJSON $ do - JSON.Object o <- return v - (nodes :: [JSON.Value]) <- o JSON..: "trace_constraints" - return nodes + (nodes :: [[JSON.Value]]) <- runJSON $ JSON.parseJSON v let nds = zip ndEnvs nodes - fmap (TraceConstraintMap . Map.fromList) $ forM nds $ \((nd, env), constraint_json) -> do - (lift $ W4S.jsonToW4 sym env constraint_json) >>= \case - Left err -> throwError $ InputChoiceError "Failed to parse value" [err] - Right a -> return (nd, a) + fmap (TraceConstraintMap . Map.fromList . concat) $ + forM nds $ \((nd, env), constraints_json) -> forM constraints_json $ \constraint_json -> + (lift $ W4S.jsonToW4 sym env constraint_json) >>= \case + Left err -> throwError $ InputChoiceError "Failed to parse value" [err] + Right a -> return (nd, a) chooseInput_ @"trace_constraint_map" msg parse >>= \case Nothing -> IO.liftIO $ fail "Unexpected trace map read" Just a -> return a @@ -153,26 +148,4 @@ readConstraintMap sym msg ndEnvs = do runJSON :: JSON.Parser a -> ExceptT InputChoiceError IO a runJSON p = ExceptT $ case JSON.parse (\() -> p) () of JSON.Success a -> return $ Right a - JSON.Error err -> return $ Left $ InputChoiceError "Failed to parse value" [err] - - - --- FIXME: Move -readDeserializable :: - forall nm_choice sym k e m. - W4S.W4Deserializable sym (TraceNodeLabel nm_choice, TraceNodeType k nm_choice) => - W4.IsExprBuilder sym => - IsTreeBuilder k e m => - IsTraceNode k nm_choice => - IO.MonadUnliftIO m => - sym -> - W4S.ExprEnv sym -> - String -> - m (Maybe (TraceNodeLabel nm_choice, TraceNodeType k nm_choice)) -readDeserializable sym env msg = do - let parse s = case JSON.eitherDecode (fromString s) of - Left err -> return $ Left $ InputChoiceError "Failed to decode JSON" [err] - Right (v :: JSON.Value) -> W4S.jsonToW4 sym env v >>= \case - Left err -> return $ Left $ InputChoiceError "Failed to parse value" [err] - Right a -> return $ Right a - chooseInput @nm_choice msg parse + JSON.Error err -> return $ Left $ InputChoiceError "Failed to parse value" [err] \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 7aa66c09..47b094ac 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -934,7 +934,13 @@ showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do fmap fst $ withGraphNode scope nd pg $ \bundle d -> do cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond eqCond_pred <- PEC.toPred sym cond_simplified - (fps, eenv) <- getTraceFootprint scope bundle + fps <- getTraceFootprint scope bundle + eenv <- PPa.joinPatchPred (\a b -> return $ W4S.mergeEnvs a b) $ \bin -> do + fp <- PPa.getC bin fps + (v, env) <- liftIO $ W4S.w4ToJSONEnv sym fp + -- only visible with debug tag + emitTraceLabel @"trace_footprint" v fp + return env asms <- currentAsm let ieqc = IntermediateEqCond bundle fps eenv asms eqCond_pred d let interims = Map.insert nd (PS.mkSimSpec scope ieqc) (eqCondInterims rs) diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs index 27f9356b..92d3c16f 100644 --- a/src/Pate/Verification/StrongestPosts/CounterExample.hs +++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs @@ -73,6 +73,9 @@ import What4.JSON import Pate.Equivalence (StatePostCondition) import qualified Pate.Binary as PB import GHC.Stack (HasCallStack) +import qualified Data.Aeson as JSON +import qualified Data.Text.Lazy.Encoding as Text +import qualified Data.Text.Encoding.Error as Text -- | A totality counterexample represents a potential control-flow situation that represents -- desynchronization of the original and patched program. The first tuple represents @@ -253,6 +256,13 @@ data TraceFootprint sym arch = TraceFootprint , fpMem :: [(MM.ArchSegmentOff arch, (MT.MemOp sym (MM.ArchAddrWidth arch)))] } +instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where + type TraceNodeType '(sym,arch) "trace_footprint" = TraceFootprint sym arch + type TraceNodeLabel "trace_footprint" = JSON.Value + prettyNode json _ = PP.pretty $ Text.decodeUtf8With Text.lenientDecode $ JSON.encode json + nodeTags = mkTags @'(sym,arch) @"trace_footprint" ["debug"] + jsonNode _ json _ = return json + mkFootprint :: forall sym arch. W4.IsExprBuilder sym => @@ -275,7 +285,7 @@ mkFootprint sym init_regs s = do _ -> return [] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceFootprint sym arch) where - w4Serialize fp = W4S.object [ "fp_initial_regs" .= fpInitialRegs fp, "fp_mem" .= fpMem fp] + w4Serialize fp = W4S.object [ "fp_mem" .= fpMem fp, "fp_initial_regs" .= fpInitialRegs fp] instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (TraceEvents sym arch) where w4Serialize (TraceEvents p pre post) = do diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index bdc32d70..5fcff5f6 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -524,9 +524,8 @@ getTraceFootprint :: forall sym arch v. PS.SimScope sym arch v -> SimBundle sym arch v -> - EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch), W4S.ExprEnv sym) -getTraceFootprint _scope bundle = withSym $ \sym -> do - fps <- PPa.forBinsC $ \bin -> withTracing @"binary" (Some bin) $ do + EquivM sym arch (PPa.PatchPairC (CE.TraceFootprint sym arch)) +getTraceFootprint _scope bundle = withSym $ \sym -> PPa.forBinsC $ \bin -> do out <- PPa.get bin (PS.simOut bundle) in_ <- PPa.get bin (PS.simIn bundle) let in_regs = PS.simInRegs in_ @@ -534,19 +533,7 @@ getTraceFootprint _scope bundle = withSym $ \sym -> do let mem = PS.simOutMem out let s = (MT.memFullSeq @_ @arch mem) s' <- PEM.mapExpr sym concretizeWithSolver s - fp <- liftIO $ CE.mkFootprint sym rop s' - (v',eenv) <- liftIO $ W4S.w4ToJSONEnv sym fp - emitTraceLabel @"trace_footprint" v' fp - return (fp, eenv) - env <- PPa.joinPatchPred (\(_, a) (_, b) -> return $ W4S.mergeEnvs a b) $ \bin -> (PPa.getC bin fps) - return $ (TF.fmapF (\(Const(a,_)) -> Const a) fps, env) - -instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "trace_footprint" where - type TraceNodeType '(sym,arch) "trace_footprint" = CE.TraceFootprint sym arch - type TraceNodeLabel "trace_footprint" = JSON.Value - prettyNode json _ = PP.pretty $ Text.decodeUtf8With Text.lenientDecode $ JSON.encode json - nodeTags = [(Summary, \_ _ -> "TODO"), (Simplified, \_ _ -> "TODO")] - jsonNode _ json _ = return json + liftIO $ CE.mkFootprint sym rop s' -- | Compute a counter-example for a given predicate getTraceFromModel :: diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 2a13bc03..f942c84b 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -44,7 +44,7 @@ import Control.Monad.State (MonadState (..), State, modify, evalState, import qualified Data.Map.Ordered as OMap import Data.List ( stripPrefix ) -import Data.Maybe ( mapMaybe ) +import Data.Maybe ( mapMaybe, catMaybes ) import Data.Map (Map) import qualified Data.Map.Merge.Strict as Map import Data.Text (Text) @@ -137,13 +137,15 @@ mergeEnvs (ExprEnv env1) (ExprEnv env2) = ExprEnv ( env2) -- | Extract expressions with annotations -cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> ExprEnv sym -cacheToEnv sym (ExprCache m) = ExprEnv $ Map.fromList $ mapMaybe go (Map.keys m) +cacheToEnv :: W4.IsExprBuilder sym => sym -> ExprCache sym -> IO (ExprEnv sym) +cacheToEnv _sym (ExprCache m) = (ExprEnv . Map.fromList . catMaybes) <$> mapM go (Map.keys m) where go (Some e) | Nothing <- W4.asConcrete e - = Just (fromIntegral $ hashF e, Some e) - go _ = Nothing + = do + ident <- mkIdent e + return $ Just (ident, Some e) + go _ = return Nothing w4ToJSONEnv :: forall sym a. (W4.IsExprBuilder sym, SerializableExprs sym) => W4Serializable sym a => sym -> a -> IO (JSON.Value, ExprEnv sym) w4ToJSONEnv sym a = do @@ -152,7 +154,8 @@ w4ToJSONEnv sym a = do let env = W4SEnv cacheRef sym True v <- runReaderT f env c <- IO.readIORef cacheRef - return $ (v, cacheToEnv sym c) + eenv <- cacheToEnv sym c + return $ (v, eenv) class W4SerializableF sym (f :: k -> Type) where withSerializable :: Proxy sym -> p f -> q tp -> (W4Serializable sym (f tp) => a) -> a @@ -181,6 +184,19 @@ trySerialize (W4S f) = do Left err -> return $ Left (show err) Right x -> return $ Right x +firstHashRef :: IO.IORef (Maybe Integer) +firstHashRef = unsafePerformIO (IO.newIORef Nothing) + +-- | Makes hashes slightly more stable by fixing the first requested +-- identifier and deriving all subsequent identifiers as offsets from it +mkIdent :: HashableF t => t tp -> IO Integer +mkIdent v = do + let (ident :: Integer) = fromIntegral $ hashF v + let f = \case + Just i -> (Just i, ident - i) + Nothing -> (Just ident, 0) + IO.atomicModifyIORef firstHashRef f + instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) where w4Serialize e' = do ExprCache s <- get @@ -196,7 +212,7 @@ instance sym ~ W4B.ExprBuilder t fs scope => W4Serializable sym (W4B.Expr t tp) asks w4sUseIdents >>= \case True -> do let tp_sexpr = W4S.serializeBaseType (W4.exprType e') - let (ident :: Integer) = fromIntegral $ hashF e' + ident <- liftIO $ mkIdent e' return $ JSON.object [ "symbolic_ident" JSON..= ident, "type" JSON..= JSON.String (W4D.printSExpr mempty tp_sexpr) ] False -> do e <- liftIO $ WEH.stripAnnotations sym e' diff --git a/tests/integration/packet/packet.exp b/tests/integration/packet/packet.exp index be269004..6cfe432f 100755 --- a/tests/integration/packet/packet.exp +++ b/tests/integration/packet/packet.exp @@ -18,7 +18,7 @@ # Also note this example is mentioned in the README.rst and used in the User Manual. # Major changes here likely warrant an update of the corresponding User Manual content. -spawn ./pate.sh --original tests/integration/packet/exe/packet.exe --patched tests/integration/packet/exe/packet.patched.exe -s parse_packet +spawn ./pate.sh --original tests/integration/packet/exe/packet.exe --patched tests/integration/packet/exe/packet.patched.exe -s parse_packet --add-trace-constraints set timeout 480 @@ -42,6 +42,17 @@ expect "0: Finish and view final result" expect "?>" send "0\r" +expect "Regenerate result with new trace constraints?" +expect "0: True" +send "0\r" +expect "Waiting for constraints.." +send "input \"\[ \[ { \\\"var\\\" : { \\\"symbolic_ident\\\" : -6 }, \\\"op\\\" : \\\"NEQ\\\", \\\"const\\\" : \\\"128\\\"} \] \]\"\r" + +expect "Regenerate result with new trace constraints?" +expect "1: False" +send "1\r" + + expect "15: Final Result" expect ">" send "15\r" @@ -51,19 +62,38 @@ expect "2: Binaries are conditionally, observably equivalent" expect ">" send "0\r" + + # Inspect the specific equivalence condition expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]" expect ">" send "0\r" -expect "3: let -- segment1+0x664.. in not v40591" +expect -re {3: let -- segment1\+0x664.. in not v(\d)+} expect ">" send "3\r" -expect "v40591 = and (eq 0x80:\\\[8\\\] v40584) (not (eq v40587 (bvSum v40584 0x80:\\\[8\\\])))" -expect "in not v40591" +expect -re {v((\d)+) = and \(eq 0x80:\[8\] v((\d)+)\) \(not \(eq v((\d)+) \(bvSum v((\d)+) 0x80:\[8\]\)\)\)} +expect -re {in not v((\d)+)} +expect ">" + +send "up\r" expect ">" +send "up\r" +expect ">" +send "up\r" +expect "5: Assumed Equivalence Conditions" +expect ">" +send "5\r" + +expect "0: segment1+0x644 \\\[ via: \"parse_packet\" (segment1+0x554) \\\]" +expect ">" +send "0\r" + +# constraint has made the equivalence condition satisified +expect "0: true" + send "\x04" ; # Ctrl-D (EOF) # remove EOF from expect_before, now that we're expecting it From aece8f68053dbea2bc67cbaefefb22149a5f8331 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 9 Aug 2024 12:13:51 -0700 Subject: [PATCH 8/8] use identifier-based serialization for trace footprint in the toplevel result --- src/Pate/Verification/StrongestPosts.hs | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 47b094ac..87823be7 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -865,7 +865,7 @@ clearTrivialCondition nd condK pg = case getCondition pg nd ConditionEquiv of data IntermediateEqCond sym arch v = IntermediateEqCond { ieqBundle :: SimBundle sym arch v - , ieqFootprints:: PPa.PatchPairC (CE.TraceFootprint sym arch) + , ieqFootprints:: PPa.PatchPairC (CE.TraceFootprint sym arch, JSON.Value) , ieqEnv :: W4S.ExprEnv sym , ieqAsms :: PAS.AssumptionSet sym , ieqCond :: W4.Pred sym @@ -935,14 +935,19 @@ showFinalResult pg0 = withTracing @"final_result" () $ withSym $ \sym -> do cond_simplified <- PSi.applySimpStrategy PSi.deepPredicateSimplifier cond eqCond_pred <- PEC.toPred sym cond_simplified fps <- getTraceFootprint scope bundle - eenv <- PPa.joinPatchPred (\a b -> return $ W4S.mergeEnvs a b) $ \bin -> do + vs <- PPa.forBinsC $ \bin -> do fp <- PPa.getC bin fps (v, env) <- liftIO $ W4S.w4ToJSONEnv sym fp -- only visible with debug tag emitTraceLabel @"trace_footprint" v fp - return env + return (v, env) + eenv <- PPa.joinPatchPred (\a b -> return $ W4S.mergeEnvs a b) $ \bin -> snd <$> (PPa.getC bin vs) + fpvs <- PPa.forBinsC $ \bin -> do + fp <- PPa.getC bin fps + (v,_) <- PPa.getC bin vs + return (fp,v) asms <- currentAsm - let ieqc = IntermediateEqCond bundle fps eenv asms eqCond_pred d + let ieqc = IntermediateEqCond bundle fpvs eenv asms eqCond_pred d let interims = Map.insert nd (PS.mkSimSpec scope ieqc) (eqCondInterims rs) rest scope ieqc >>= \case Just fcond -> return (rs { eqCondFinals = Map.insert nd fcond (eqCondFinals rs), eqCondInterims = interims }, pg) @@ -978,7 +983,8 @@ data FinalEquivCond sym arch = FinalEquivCond _finEqCondPred :: W4.Pred sym , _finEqCondTraceTrue :: CE.TraceEvents sym arch , _finEqCondTraceFalse :: CE.TraceEvents sym arch - , _finEqFootprints :: PPa.PatchPairC (CE.TraceFootprint sym arch) + -- small hack to include the footprint serialized according to the expression environment + , _finEqFootprints :: PPa.PatchPairC (CE.TraceFootprint sym arch, JSON.Value) } @@ -991,7 +997,7 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalR instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalEquivCond sym arch) where w4Serialize (FinalEquivCond p trT trF fps) = do - W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF, "trace_footprint" W4S..= fps ] + W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF, "trace_footprint" W4S..= (TF.fmapF (\(Const(_,v)) -> Const v) fps) ] instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "toplevel_result" where