Merge pull request #428 from GaloisInc/dm/traceconstraints

support additional constraints when generating traces

* add `--add-trace-constraints` flag that allows for generating additional traces with constraints for the final equivalence conditions
  - Defines a trace constraint datatype in Pate.TraceConstraint that is simply: expression, comparison, constant
* add alternative what4 serializer that uses expression identifiers (based on what4 hashes/nonces) in lieu of serialized expressions
* add deserialization infrastructure for expressions-containing types, using the expression environment from the identifier-based serializer

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/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]

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