accept trace constraints as input after final result

pate.cabal

@@ -161,6 +161,7 @@ library
                        Pate.Script,
                        Pate.Timeout,
                        Pate.TraceTree,
+                       Pate.TraceConstraint,
                        Pate.ExprMappable,
                        What4.ExprHelpers,
                        What4.PathCondition,

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."
          )

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
                      }

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
+  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

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

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

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