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..da0fb5bf 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/TraceConstraint.hs b/src/Pate/TraceConstraint.hs new file mode 100644 index 00000000..4edabe16 --- /dev/null +++ b/src/Pate/TraceConstraint.hs @@ -0,0 +1,151 @@ +{-# 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 + , 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:" ++ show (W4.exprType var)) + +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 + 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 + GTs -> goNot W4.bvSle + GTu -> goNot W4.bvUle + GEs -> goNot W4.bvSlt + GEu -> goNot W4.bvUlt + NEQ -> goNot W4.isEq + _ -> 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 = [] + +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 :: [[JSON.Value]]) <- runJSON $ JSON.parseJSON v + let nds = zip ndEnvs nodes + 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 + + +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] \ 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..87823be7 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,115 @@ 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, JSON.Value) + , 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.." (Map.toAscList (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 <- getTraceFootprint scope bundle + 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 (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 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) + 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 +983,8 @@ data FinalEquivCond sym arch = FinalEquivCond _finEqCondPred :: W4.Pred sym , _finEqCondTraceTrue :: CE.TraceEvents sym arch , _finEqCondTraceFalse :: CE.TraceEvents sym arch + -- small hack to include the footprint serialized according to the expression environment + , _finEqFootprints :: PPa.PatchPairC (CE.TraceFootprint sym arch, JSON.Value) } @@ -915,8 +996,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..= (TF.fmapF (\(Const(_,v)) -> Const v) fps) ] instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "toplevel_result" where diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs index bfb18b54..92d3c16f 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) @@ -69,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 @@ -243,6 +250,43 @@ 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)))] + } + +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 => + 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_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 trace_pair <- PPa.w4SerializePair p $ \(TraceEventsOne rop evs) -> diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index dc010544..5fcff5f6 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 @@ -56,6 +57,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 @@ -86,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 @@ -108,6 +112,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(..)) @@ -120,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 @@ -473,6 +480,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 -> @@ -489,21 +510,30 @@ 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) - -- 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 + + tr <- tryWithAsms + [ (ptrAsserts_pred, PEE.RequiresInvalidPointerOps) + ] $ \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' -- | Compute a counter-example for a given predicate getTraceFromModel :: diff --git a/src/What4/JSON.hs b/src/What4/JSON.hs index 97d1d3a6..f942c84b 100644 --- a/src/What4/JSON.hs +++ b/src/What4/JSON.hs @@ -24,20 +24,35 @@ module What4.JSON , W4SerializableFC , SerializableExprs , w4ToJSON + , w4ToJSONEnv , object , w4SerializeString , (.=) , (.==) , (.=~) + , ExprEnv + , mergeEnvs + , W4Deserializable(..) + , jsonToW4 + , readJSON + , (.:) + , SymDeserializable(..) + , symDeserializable ) where import Control.Monad.State (MonadState (..), State, modify, evalState, runState) import qualified Data.Map.Ordered as OMap +import Data.List ( stripPrefix ) +import Data.Maybe ( mapMaybe, catMaybes ) 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 +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 +77,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 +86,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 +97,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 +122,41 @@ 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))) + +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 -> IO (ExprEnv sym) +cacheToEnv _sym (ExprCache m) = (ExprEnv . Map.fromList . catMaybes) <$> mapM go (Map.keys m) + where + go (Some e) + | Nothing <- W4.asConcrete e + = 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 + 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 + 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 @@ -130,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 @@ -142,16 +209,22 @@ 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 -> do + let tp_sexpr = W4S.serializeBaseType (W4.exprType 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' + 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 +320,113 @@ 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_ :: W4.IsExprBuilder sym => JSON.Value -> W4DS sym a + + 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 () + +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 + +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 + 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 } + +instance W4Deserializable sym (Some (ToDeserializable sym)) where + w4Deserialize_ v = fmap (\(Some x) -> Some (ToDeserializable x)) $ 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 = 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) + +-- | 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. + SymDeserializable sym (W4.SymExpr sym) +symDeserializable = unsafeCoerce r + where + r :: SymDeserializable sym (ToDeserializable sym) + r = SymDeserializable \ No newline at end of file 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) 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