talos: added --save-problems argument and supporting code.

talos/app/CommandLine.hs

@@ -32,7 +32,8 @@ data Options =
           , optDDLEntry   :: Maybe String
           , optStrategy   :: Maybe [String]
           , optInvFile    :: Maybe FilePath
-          , optStatsFile  :: Maybe FilePath          
+          , optStatsFile  :: Maybe FilePath
+          , optProblemFilePfx :: Maybe FilePath          
           , optAnalysisKind :: Maybe String
           , optVerbosity :: Int
           , optNoLoops :: Bool
@@ -68,6 +69,12 @@ statsFileOpt = strOption
      <> metavar "FILE"
      <> help "Write statistics to FILE" )
 
+problemFileOpt :: Parser String
+problemFileOpt = strOption
+   ( long "save-problems"
+     <> metavar "FILE"
+     <> help "Write SMT problems to FILE<slice-id>" )
+
 statsKeyOpt :: Parser String
 statsKeyOpt = strOption
    ( long "stats-key"
@@ -78,7 +85,7 @@ statsKeyOpt = strOption
 smtLogOpt :: Parser FilePath
 smtLogOpt = strOption
    ( long "smt-log"
-     <> metavar "File"
+     <> metavar "FILE"
      <> help "Write smt log to FILE" )
 
 validateModelFlag :: Parser Bool
@@ -198,7 +205,8 @@ options = Options <$> solverOpt
                   <*> optional entryOpt
                   <*> optional (some strategyOpt)
                   <*> optional invFileOpt
-                  <*> optional statsFileOpt                  
+                  <*> optional statsFileOpt
+                  <*> optional problemFileOpt                  
                   <*> optional analysisKindOpt
                   <*> (length <$> many verbosityOpt)
                   <*> noLoopsOpt

talos/app/Main.hs

@@ -115,6 +115,7 @@ doSynthesis opts = do
       , logFile         = optLogOutput opts
       , debugKeys       = optDebugKeys opts
       , statsFile       = optStatsOutput opts
+      , problemFile     = optProblemFilePfx opts
       , statsKeys       = optStatsKeys opts
       }
 

talos/src/Talos.hs

@@ -15,22 +15,23 @@ module Talos (
 
 import qualified Colog.Core                   as Log
 import           Control.Monad                (forM_, unless, when)
+import           Control.Monad.IO.Class       (liftIO)
 import           Data.ByteString              (ByteString)
 import           Data.IORef                   (modifyIORef', newIORef,
                                                readIORef, writeIORef)
 import qualified Data.Map                     as Map
 import           Data.Maybe                   (fromMaybe, isJust)
 import           Data.String                  (fromString)
+import           Data.Text                    (Text)
+import qualified Data.Text                    as Text
 import           Data.Version
 import qualified SimpleSMT                    as SMT
 import qualified Streaming                    as S
 import           System.Exit                  (exitFailure)
-import           System.IO                    (IOMode (..), hFlush,
-                                               hPutStr, hPutStrLn, openFile,
-                                               stderr)
+import           System.IO                    (IOMode (..), hFlush, hPutStr,
+                                               hPutStrLn, openFile, stderr)
 import qualified Text.ParserCombinators.ReadP as RP
 import           Text.ParserCombinators.ReadP (readP_to_S)
-import qualified Data.Text as Text
 
 import           Daedalus.AST                 (nameScopeAsModScope)
 import           Daedalus.Core
@@ -45,12 +46,12 @@ import           Data.Functor.Of              (Of)
 import qualified Talos.Analysis               as A
 import           Talos.Analysis.AbsEnv        (AbsEnvTy (AbsEnvTy))
 import           Talos.Analysis.Monad         (makeDeclInvs)
-import           Talos.Monad                  (runTalosM, runTalosStream, LogKey, logKeyEnabled, getLogKey)
+import           Talos.Monad                  (LogKey, getLogKey, logKeyEnabled,
+                                               runTalosM, runTalosStream)
 import           Talos.Passes
+import           Talos.Path                   (ProvenanceMap)
 import           Talos.Strategy
-import           Talos.Path                  (ProvenanceMap)
 import qualified Talos.Synthesis              as T
-import Data.Text (Text)
 
 -- -- FIXME: move, maybe to GUID.hs?
 -- newtype FreshGUIDM a = FreshGUIDM { getFreshGUIDM :: State GUID a }
@@ -72,7 +73,7 @@ summarise inFile m_invFile m_entry verbosity noLoops absEnv = do
   putStrLn "Inverses"
   print (pp <$> Map.keys invs)
   putStrLn "Slices"
-  summs <- runTalosM md nguid mempty mempty (A.summarise p)
+  summs <- runTalosM md nguid mempty mempty mempty (A.summarise p)
 
   pure (bullets (map goF (Map.toList summs)))
   where
@@ -126,6 +127,7 @@ data SynthesisOptions = SynthesisOptions
   , debugKeys       :: [String]           -- ^ Keys for logging debug messages
   , statsFile       :: Maybe FilePath     -- ^ Output file for stats
   , statsKeys       :: [String]           -- ^ Keys for stats
+  , problemFile     :: Maybe FilePath     -- ^ Output file(s) for SMT problems
   , smtLogFile      :: Maybe FilePath     -- ^ SMT logging file  
   }
 
@@ -169,11 +171,12 @@ synthesise SynthesisOptions { .. } = do
 
   withLogStringFileMaybe logFile Log.logStringStdout $ \logact ->
     withLogStringFileMaybe statsFile mempty $ \statsact -> do
-    let strm = T.synthesise seed solver absty stratInsts mainRule
-        logact'   = Log.cmapMaybe logAction logact
-        statsact' = Log.cfilter (keyCFilter (map Text.pack statsKeys)) (Log.cmap ppStat statsact)
-
-    pure (runTalosStream md nguid statsact' logact' strm)
+      withLogStringFilePrefix problemFile mempty $ \problemact -> do
+        let strm = T.synthesise seed solver absty stratInsts mainRule
+            logact'    = Log.cmapMaybe logAction logact
+            statsact'  = Log.cfilter (keyCFilter (map Text.pack statsKeys)) (Log.cmap ppStat statsact)
+            problemact' = Log.cfilter (const True) problemact
+        pure (runTalosStream md nguid statsact' logact' problemact' strm)
 
   where
     -- We have a lazy stream which persists after the call returns, so
@@ -183,6 +186,13 @@ synthesise SynthesisOptions { .. } = do
       hdl <- openFile fn WriteMode
       f (Log.logStringHandle hdl <> Log.logFlush hdl)
 
+    withLogStringFilePrefix Nothing dflt f = f dflt
+    withLogStringFilePrefix (Just pfx) _dflt f = do
+      let mkName sid = pfx <> sid
+          -- FIXME: We ignore keys here.
+          act (_key, (sid, msg)) = liftIO (writeFile (mkName sid) msg)
+      f (Log.LogAction act)
+
     logAction (key, (lvl, msg))
       -- Always produce debug output if the key was requested
       | any (logKeyEnabled key) (map Text.pack debugKeys) = Just msg'
@@ -193,7 +203,8 @@ synthesise SynthesisOptions { .. } = do
         msg' = "[" <> show lvl <> "] " <> Text.unpack (getLogKey key) <> " " <> msg
 
     ppStat (key, stat) = Text.unpack (getLogKey key) <> " " <> Text.unpack stat
-
+
+
 -- Passes on only those keys that are prefixed by one of the argument
 -- keys
 keyCFilter :: [Text] -> (LogKey, a) -> Bool

talos/src/Talos/Monad.hs

@@ -42,6 +42,7 @@ data TalosMState  = TalosMState
   -- Logging and Statistics
   , tmStatAction :: !(Log.LogAction TalosM (LogKey, Statistic))
   , tmLogAction  :: !(Log.LogAction TalosM (LogKey, (LogLevel, String)))
+  , tmLogProblemAction :: !(Log.LogAction TalosM (LogKey, (String, String)))
     -- GUIDs
   , tmNextGUID  :: !GUID
   }
@@ -53,29 +54,33 @@ newtype TalosM a =
 runTalosStream :: Functor f => Module -> GUID ->
                   Log.LogAction TalosM (LogKey, Statistic) ->
                   Log.LogAction TalosM (LogKey, (LogLevel, String)) ->
+                  Log.LogAction TalosM (LogKey, (String, String)) ->
                   S.Stream f TalosM r ->
                   S.Stream f IO r
-runTalosStream md nguid statsact logact strm =
-  evalStateT (S.distribute (S.hoist getTalosM strm)) (emptyTalosMState md nguid statsact logact)
+runTalosStream md nguid statsact logact problemact strm =
+  evalStateT (S.distribute (S.hoist getTalosM strm)) (emptyTalosMState md nguid statsact logact problemact)
 
 runTalosM :: Module -> GUID ->
              Log.LogAction TalosM (LogKey, Statistic) ->
              Log.LogAction TalosM (LogKey, (LogLevel, String)) ->
+             Log.LogAction TalosM (LogKey, (String, String)) ->             
              TalosM a -> IO a
-runTalosM md nguid statsact logact m = evalStateT (getTalosM m) (emptyTalosMState md nguid statsact logact)
+runTalosM md nguid statsact logact problemact m = evalStateT (getTalosM m) (emptyTalosMState md nguid statsact logact problemact)
 
 emptyTalosMState :: Module -> GUID ->
                     Log.LogAction TalosM (LogKey, Statistic) ->
                     Log.LogAction TalosM (LogKey, (LogLevel, String)) ->
+                    Log.LogAction TalosM (LogKey, (String, String)) ->
                     TalosMState
-emptyTalosMState md nguid statsact logact = TalosMState
+emptyTalosMState md nguid statsact logact logproblemact = TalosMState
   { tmModule    = md
   -- Derived from the module
   , tmFunDefs   = funDefs
   , tmBFunDefs  = bfunDefs
   , tmIEnv      = env0
   , tmStatAction = statsact
   , tmLogAction  = logact
+  , tmLogProblemAction = logproblemact
   , tmNextGUID  = nguid
   }
   where
@@ -146,9 +151,14 @@ logMessage lvl key msg = liftTalosM $ do
   action <- TalosM $ gets tmLogAction
   action Log.<& (key, (lvl, msg))
 
+logProblem :: LiftTalosM m => LogKey -> String -> String -> m ()
+logProblem key sid msg = liftTalosM $ do
+  action <- TalosM $ gets tmLogProblemAction
+  action Log.<& (key, (sid, msg))
+
 debug, info, warning :: LiftTalosM m => LogKey -> String -> m ()
-debug   = logMessage Info 
-info    = logMessage Debug 
+debug   = logMessage Debug
+info    = logMessage Info 
 warning = logMessage Warning 
 
 -- -----------------------------------------------------------------------------

talos/src/Talos/Solver/SolverT.hs

@@ -21,7 +21,7 @@ module Talos.Solver.SolverT (
   getValue, getValues, getModel,
   -- * Context management
   SolverContext, SolverFrame, getContext, restoreContext,
-  freshContext, collapseContext, extendContext, instantiateSolverFrame,
+  freshContext, collapseContext, extendContext, instantiateSolverFrame, contextToSExprs,
   substSExpr,
   scoped,
   -- * Context management
@@ -209,6 +209,19 @@ collapseContext (SolverContext fs)
   where
     fs' = filter (not . nullSolverFrame) fs
 
+-- | This should match what was/will be sent to the solver.
+contextToSExprs :: SolverContext -> [SExpr]
+contextToSExprs (SolverContext frames) =
+  concatMap ( (++ [ S.List [S.const "push"] ]) . frameToSExprs ) frames
+
+frameToSExprs :: SolverFrame -> [SExpr]
+frameToSExprs sf = map go (toList $ frCommands sf)
+  where
+    go (QCAssert se) = S.fun "assert" [se]
+    go (QCDeclare v ty) = S.fun "declare-fun" [S.const v, S.List [], ty]
+    go (QCDefine  v ty body) = S.fun "define-fun" [S.const v,  S.List [], ty, body]
+
+
 -- | This makes all the variables in the solver frame fresh, so that
 -- we can use it multiple times.
 instantiateSolverFrame :: (Monad m, HasGUID m) =>

talos/src/Talos/Strategy.hs

@@ -38,29 +38,29 @@ allStrategies = [ randRestart, randMaybeT, randDFS, pathSymbolicStrat] {- , back
 parseStrategies :: [String] -> Either String [StrategyInstance]
 parseStrategies ss = M.parseStrategies ss allStrategies
 
-runStrategy :: SolverState -> StrategyInstance -> ProvenanceTag -> ExpSlice ->
+runStrategy :: SolverState -> StrategyInstance -> ProvenanceTag -> SliceId -> ExpSlice -> 
                StrategyM (([SelectedPath], Maybe StratGen), SolverState)
-runStrategy solvSt strat ptag sl = runSolverT (getStratGen (siFun strat ptag sl)) solvSt
+runStrategy solvSt strat ptag sid sl = runSolverT (getStratGen (siFun strat ptag sid sl)) solvSt
 
 -- Returns the result and wall-clock time (in ns)
-timeStrategy :: SolverState -> StrategyInstance -> ProvenanceTag -> ExpSlice ->
+timeStrategy :: SolverState -> StrategyInstance -> ProvenanceTag -> SliceId -> ExpSlice ->
                 StrategyM (([SelectedPath], Maybe StratGen, SolverState), Integer)
-timeStrategy solvSt strat ptag sl = timeIt $ do
-  ((rv, gen), solvSt') <- runStrategy solvSt strat ptag sl
+timeStrategy solvSt strat ptag sid sl = timeIt $ do
+  ((rv, gen), solvSt') <- runStrategy solvSt strat ptag sid sl
   rv'           <- liftIO $ evaluate $ force rv
   pure (rv', gen, solvSt')
 
-runStrategies :: LiftStrategyM m => SolverState -> [StrategyInstance] -> ProvenanceTag -> FName -> Name -> ExpSlice ->
+runStrategies :: LiftStrategyM m => SolverState -> [StrategyInstance] -> ProvenanceTag -> FName -> Name -> SliceId -> ExpSlice ->
                  m ([SelectedPath], Maybe StratGen, SolverState)
-runStrategies solvSt strats0 ptag fn x sl = liftStrategy $ go solvSt strats0
+runStrategies solvSt strats0 ptag fn x sid sl = liftStrategy $ go solvSt strats0
   where
     -- FIXME: There is probably a nicer way of doing this
     go s [] = pure ([], Nothing, s)
     go s (strat : strats) = do
       -- logMessage 1 $ "Trying strategy " ++ siName strat ++ " at " ++ showPP fn ++ "." ++ showPP x ++ " ... "
-      ((r, m_gen, s'), ns) <- timeStrategy s strat ptag sl
-      let dns = (fromIntegral ns :: Double)
-      let resReport = if null r then "failed" else "succeeded"
+      ((r, m_gen, s'), _ns) <- timeStrategy s strat ptag sid sl
+      -- let dns = (fromIntegral ns :: Double)
+      -- let resReport = if null r then "failed" else "succeeded"
       -- logMessage 1 $ printf "%s (%.3fms)\n" resReport (dns  / 1000000)
       if null r
         then go s' strats
@@ -104,7 +104,7 @@ findModel mc ptag fn x sid
     -- We haven't seen this slice before, so solve
   | otherwise = do
       sl <- getSlice sid
-      (r, _m_gen, solvSt') <- runStrategies (mcSolverState mc) (mcStratInstances mc) ptag fn x sl
+      (r, _m_gen, solvSt') <- runStrategies (mcSolverState mc) (mcStratInstances mc) ptag fn x sid sl
       pure $ if null r
              then (Nothing, mc)
              else nextModel (mc { mcSolverState = solvSt' })

talos/src/Talos/Strategy/BTRand.hs

@@ -24,7 +24,7 @@ import qualified Daedalus.Core.Semantics.Grammar as I
 import           Daedalus.Core.Type              (typeOf)
 import qualified Daedalus.Value                  as I
 
-import           Talos.Analysis.Exported         (ExpCallNode (..), ExpSlice)
+import           Talos.Analysis.Exported         (ExpCallNode (..), ExpSlice, SliceId)
 import           Talos.Analysis.Slice
 import           Talos.Monad                     (getIEnv)
 import           Talos.Strategy.DFST
@@ -56,7 +56,7 @@ randDFS =
         , siFun   = mkgen c
         }
 
-    mkgen c = \ptag sl -> StratGen $ lift $ do
+    mkgen c = \ptag _sid sl -> StratGen $ lift $ do
       rs <- go (cNModels c) [] ptag sl
       pure (rs, Nothing)
 
@@ -108,8 +108,8 @@ randRestart =
 restartBound :: Int
 restartBound = 1000
 
-randRestartStrat :: ProvenanceTag -> ExpSlice -> StratGen
-randRestartStrat ptag sl = trivialStratGen . lift $ go restartBound
+randRestartStrat :: ProvenanceTag -> SliceId -> ExpSlice -> StratGen
+randRestartStrat ptag _sid sl = trivialStratGen . lift $ go restartBound
   where
     go 0 = pure Nothing
     go n = do
@@ -139,8 +139,8 @@ randMaybeT =
     name  = "rand-restart-local-bt"
     descr = "Backtrack locally on failure, restart on (global) failure with random selection"
 
-randMaybeStrat :: ProvenanceTag -> ExpSlice -> StratGen
-randMaybeStrat ptag sl = trivialStratGen . lift $ go restartBound
+randMaybeStrat :: ProvenanceTag -> SliceId -> ExpSlice -> StratGen
+randMaybeStrat ptag _sid sl = trivialStratGen . lift $ go restartBound
   where
     go 0 = pure Nothing
     go n = do

talos/src/Talos/Strategy/Monad.hs

@@ -74,7 +74,7 @@ import           Talos.Solver.SolverT     (SolverT)
 -- Returns any new models, plus the option of getting more
 newtype StratGen = StratGen { getStratGen :: SolverT StrategyM ([SelectedPath], Maybe StratGen) }
 
-type StratFun = ProvenanceTag -> ExpSlice -> StratGen
+type StratFun = ProvenanceTag -> SliceId -> ExpSlice -> StratGen
 
 data StrategyInstance = StrategyInstance
   { siName  :: String

talos/src/Talos/Strategy/PathSymbolic.hs

@@ -45,6 +45,7 @@ import           Talos.Analysis.Slice
 import qualified Talos.Monad                             as T
 
 import           Talos.Lib                               (tByte)
+import           Talos.Monad                             (debug)
 import           Talos.Path
 import           Talos.Solver.SolverT                    (contextSize,
                                                           declareName,
@@ -115,9 +116,11 @@ configOpts = [ P.option "max-depth"  (field @"cMaxRecDepth") P.intP
 -- FIXME: define all types etc. eagerly
 symbolicFun :: Config ->
                ProvenanceTag ->
+               SliceId -> 
                ExpSlice ->
                StratGen
-symbolicFun config ptag sl = StratGen $ do
+symbolicFun config ptag sid sl = StratGen $ do
+  debug pathKey $ "Generating models for " <> showPP sid
   -- defined referenced types/functions
   reset -- FIXME
 
@@ -132,7 +135,7 @@ symbolicFun config ptag sl = StratGen $ do
     T.statS (pathKey <> "modelsize") sz
 
     let go ((_, pb), sm) = do
-          rs <- buildPaths (cNModels config) (cMaxUnsat config) sm pb
+          rs <- buildPaths (cNModels config) (cMaxUnsat config) sid sm pb
           T.info pathKey $ printf "Generated %d models" (length rs)
           pure (rs, Nothing) -- FIXME: return a generator here.
 

talos/src/Talos/Strategy/PathSymbolic/Assertion.hs

@@ -42,9 +42,11 @@ toSExpr assn =
     PSAssert ps -> PS.toSExpr ps
     BoolAssert b -> SMT.bool b
     BAssert  b  -> B.toSExpr (toSExpr <$> b)
-    EntailAssert ps assns ->
-      PS.toSExpr ps `SMT.implies` andMany (map toSExpr (toList assns))
-
+    EntailAssert ps assns
+      | PS.trivial ps -> rhs
+      | otherwise     -> PS.toSExpr ps `SMT.implies` rhs
+      where rhs = andMany (map toSExpr (toList assns))
+
 trivial :: Assertion -> Bool
 trivial assn =
   case assn of