diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 0daef001fa..b7a032ddc8 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -2,6 +2,7 @@ module Main (main) where import Prelude.Kore +import qualified Control.Lens as Lens import Control.Monad.Catch ( MonadMask , SomeException @@ -10,11 +11,13 @@ import Control.Monad.Catch , throwM ) import Control.Monad.Extra as Monad -import qualified Data.Char as Char import Data.Default ( def ) import qualified Data.Foldable as Foldable +import Data.Generics.Product + ( field + ) import Data.Limit ( Limit (..) , maybeLimit @@ -35,6 +38,7 @@ import qualified Data.Text.IO as Text ( putStrLn , readFile ) +import qualified GHC.Generics as GHC import Options.Applicative ( InfoMod , Parser @@ -160,6 +164,14 @@ import qualified Kore.Syntax.Definition as Definition.DoNotUse import Kore.Unparser ( unparse ) +import Options.SMT + ( KoreSolverOptions (..) + , Solver (..) + , ensureSmtPreludeExists + , parseKoreSolverOptions + , unparseKoreSolverOptions + , writeKoreSolverFiles + ) import Pretty ( Doc , Pretty (..) @@ -172,7 +184,6 @@ import Prof ) import SMT ( MonadSMT - , TimeOut (..) ) import qualified SMT import Stats @@ -192,7 +203,7 @@ data KoreSearchOptions = -- ^ The maximum bound on the number of search matches , searchType :: !SearchType -- ^ The type of search to perform - } + } deriving (GHC.Generic) parseKoreSearchOptions :: Parser KoreSearchOptions parseKoreSearchOptions = @@ -262,23 +273,6 @@ applyKoreSearchOptions koreSearchOptions@(Just koreSearchOpts) koreExecOpts = ONE -> Limit 1 _ -> Unlimited --- | Available SMT solvers -data Solver = Z3 | None - deriving (Eq, Ord, Show) - deriving (Enum, Bounded) - -parseSolver :: Parser Solver -parseSolver = - option (snd <$> readSum longName options) - $ metavar "SOLVER" - <> long longName - <> help ("SMT solver for checking constraints: " <> knownOptions) - <> value Z3 - where - longName = "smt" - knownOptions = intercalate ", " (map fst options) - options = [ (map Char.toLower $ show s, s) | s <- [minBound .. maxBound] ] - -- | Main options record data KoreExecOptions = KoreExecOptions { definitionFileName :: !FilePath @@ -289,19 +283,17 @@ data KoreExecOptions = KoreExecOptions -- ^ Name for file to contain the output pattern , mainModuleName :: !ModuleName -- ^ The name of the main module in the definition - , smtTimeOut :: !SMT.TimeOut - , smtPrelude :: !(Maybe FilePath) - , smtSolver :: !Solver , breadthLimit :: !(Limit Natural) , depthLimit :: !(Limit Natural) , strategy :: !(String, [RewriteRule RewritingVariableName] -> Strategy (Prim (RewriteRule RewritingVariableName))) + , koreSolverOptions :: !KoreSolverOptions , koreLogOptions :: !KoreLogOptions , koreSearchOptions :: !(Maybe KoreSearchOptions) , koreProveOptions :: !(Maybe KoreProveOptions) , koreMergeOptions :: !(Maybe KoreMergeOptions) , rtsStatistics :: !(Maybe FilePath) , bugReport :: !BugReport - } + } deriving (GHC.Generic) -- | Command Line Argument Parser parseKoreExecOptions :: TimeSpec -> Parser KoreExecOptions @@ -332,35 +324,17 @@ parseKoreExecOptions startTime = ) ) <*> parseMainModuleName - <*> option readSMTTimeOut - ( metavar "SMT_TIMEOUT" - <> long "smt-timeout" - <> help "Timeout for calls to the SMT solver, in milliseconds" - <> value defaultTimeOut - ) - <*> optional - ( strOption - ( metavar "SMT_PRELUDE" - <> long "smt-prelude" - <> help "Path to the SMT prelude file" - ) - ) - <*> parseSolver <*> parseBreadthLimit <*> parseDepthLimit <*> parseStrategy + <*> parseKoreSolverOptions <*> parseKoreLogOptions (ExeName "kore-exec") startTime <*> pure Nothing <*> optional parseKoreProveOptions <*> optional parseKoreMergeOptions <*> optional parseRtsStatistics <*> parseBugReport - SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig - readSMTTimeOut = do - i <- auto - if i <= 0 - then readerError "smt-timeout must be a positive integer." - else return $ SMT.TimeOut $ Limit i + parseBreadthLimit = Limit <$> breadth <|> pure Unlimited parseDepthLimit = Limit <$> depth <|> pure Unlimited parseStrategy = @@ -375,6 +349,7 @@ parseKoreExecOptions startTime = [ ("any", priorityAnyStrategy) , ("all", priorityAllStrategy) ] + breadth = option auto ( metavar "BREADTH" @@ -387,6 +362,7 @@ parseKoreExecOptions startTime = <> long "depth" <> help "Execute up to DEPTH steps." ) + parseMainModuleName = GlobalMain.parseModuleName "MODULE" @@ -446,12 +422,10 @@ koreExecSh patternFileName outputFileName mainModuleName - (TimeOut timeout) - smtPrelude - smtSolver breadthLimit depthLimit strategy + koreSolverOptions koreLogOptions koreSearchOptions koreProveOptions @@ -474,10 +448,6 @@ koreExecSh , patternFileName $> "--pattern pgm.kore" , outputFileName $> "--output result.kore" , pure $ "--module " <> unpack (getModuleName mainModuleName) - , (\limit -> unwords ["--smt-timeout", show limit]) - <$> maybeLimit Nothing Just timeout - , smtPrelude $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] - , pure $ "--smt " <> fmap Char.toLower (show smtSolver) , (\limit -> unwords ["--breadth", show limit]) <$> maybeLimit Nothing Just breadthLimit , (\limit -> unwords ["--depth", show limit]) @@ -486,6 +456,7 @@ koreExecSh , rtsStatistics $> unwords ["--rts-statistics", defaultRtsStatisticsFilePath] ] + , unparseKoreSolverOptions koreSolverOptions , unparseKoreLogOptions koreLogOptions , maybe mempty unparseKoreSearchOptions koreSearchOptions , maybe mempty unparseKoreProveOptions koreProveOptions @@ -497,9 +468,6 @@ defaultDefinitionFilePath KoreExecOptions { koreProveOptions } | isJust koreProveOptions = "vdefinition.kore" | otherwise = "definition.kore" -defaultSmtPreludeFilePath :: FilePath -defaultSmtPreludeFilePath = "prelude.smt2" - defaultRtsStatisticsFilePath :: FilePath defaultRtsStatisticsFilePath = "rts-statistics.json" @@ -527,7 +495,7 @@ writeOptionsAndKoreFiles opts@KoreExecOptions { definitionFileName , patternFileName - , smtPrelude + , koreSolverOptions , koreSearchOptions , koreProveOptions , koreMergeOptions @@ -545,8 +513,7 @@ writeOptionsAndKoreFiles (reportDirectory defaultDefinitionFilePath opts) Foldable.for_ patternFileName $ flip copyFile (reportDirectory "pgm.kore") - Foldable.for_ smtPrelude - $ flip copyFile (reportDirectory defaultSmtPreludeFilePath) + writeKoreSolverFiles koreSolverOptions reportDirectory Foldable.for_ koreSearchOptions (writeKoreSearchFiles reportDirectory) Foldable.for_ koreMergeOptions @@ -569,18 +536,10 @@ main = do parserInfoModifiers Foldable.for_ (localOptions options) mainWithOptions --- | Ensure that the SMT prelude file exists, if specified. -ensureSmtPreludeExists :: Maybe FilePath -> IO () -ensureSmtPreludeExists = - Foldable.traverse_ $ \filePath -> - Monad.whenM - (not <$> doesFileExist filePath) - (error $ "SMT prelude file does not exist: " <> filePath) - mainWithOptions :: KoreExecOptions -> IO () mainWithOptions execOptions = do - let KoreExecOptions { koreLogOptions, bugReport, smtPrelude } = execOptions - ensureSmtPreludeExists smtPrelude + let KoreExecOptions { koreLogOptions, koreSolverOptions, bugReport } = execOptions + ensureSmtPreludeExists koreSolverOptions exitCode <- withBugReport Main.exeName bugReport $ \tmpDir -> do writeOptionsAndKoreFiles tmpDir execOptions @@ -841,7 +800,7 @@ execute -> Main r execute options mainModule worker = clockSomethingIO "Executing" - $ case smtSolver of + $ case solver of Z3 -> withZ3 None -> withoutSMT where @@ -854,11 +813,13 @@ execute options mainModule worker = ) worker withoutSMT = SMT.runNoSMT worker - KoreExecOptions { smtTimeOut, smtPrelude, smtSolver } = options + KoreSolverOptions { timeOut, resetInterval, prelude, solver } = + Lens.view (field @"koreSolverOptions") options config = SMT.defaultConfig - { SMT.timeOut = smtTimeOut - , SMT.preludeFile = smtPrelude + { SMT.timeOut = timeOut + , SMT.resetInterval = resetInterval + , SMT.prelude = prelude } loadPattern :: LoadedModule -> Maybe FilePath -> Main (TermLike VariableName) diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs index 6db4ca2e6a..e19ddbe50d 100644 --- a/kore/app/repl/Main.hs +++ b/kore/app/repl/Main.hs @@ -11,29 +11,22 @@ import Options.Applicative ( InfoMod , Parser , argument - , auto , flag , fullDesc , header , help , long , metavar - , option , progDesc - , readerError , short , str , strOption - , value ) import System.Exit ( exitFailure , exitWith ) -import Data.Limit - ( Limit (..) - ) import Kore.BugReport import Kore.Exec ( proveWithRepl @@ -58,6 +51,10 @@ import Kore.Step.SMT.Lemma import Kore.Syntax.Module ( ModuleName (..) ) +import Options.SMT + ( KoreSolverOptions (..) + , parseKoreSolverOptions + ) import qualified SMT import System.Clock ( Clock (Monotonic) @@ -73,17 +70,11 @@ data KoreModule = KoreModule , moduleName :: !ModuleName } --- | SMT Timeout and (optionally) a custom prelude path. -data SmtOptions = SmtOptions - { timeOut :: !SMT.TimeOut - , prelude :: !(Maybe FilePath) - } - -- | Options for the kore repl. data KoreReplOptions = KoreReplOptions { definitionModule :: !KoreModule , proveOptions :: !KoreProveOptions - , smtOptions :: !SmtOptions + , smtOptions :: !KoreSolverOptions , replMode :: !ReplMode , scriptModeOutput :: !ScriptModeOutput , replScript :: !ReplScript @@ -97,7 +88,7 @@ parseKoreReplOptions startTime = KoreReplOptions <$> parseMainModule <*> parseKoreProveOptions - <*> parseSmtOptions + <*> parseKoreSolverOptions <*> parseReplMode <*> parseScriptModeOutput <*> parseReplScript @@ -116,23 +107,6 @@ parseKoreReplOptions startTime = "module" "Kore main module name." - parseSmtOptions :: Parser SmtOptions - parseSmtOptions = - SmtOptions - <$> option readSMTTimeOut - ( metavar "SMT_TIMEOUT" - <> long "smt-timeout" - <> help "Timeout for calls to the SMT solver, in miliseconds" - <> value defaultTimeOut - ) - <*> optional - ( strOption - ( metavar "SMT_PRELUDE" - <> long "smt-prelude" - <> help "Path to the SMT prelude file" - ) - ) - parseReplMode :: Parser ReplMode parseReplMode = flag @@ -163,14 +137,6 @@ parseKoreReplOptions startTime = ) ) - SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig - - readSMTTimeOut = do - i <- auto - if i <= 0 - then readerError "smt-timeout must be a positive integer." - else return $ SMT.TimeOut $ Limit i - parseOutputFile :: Parser OutputFile parseOutputFile = OutputFile @@ -230,7 +196,8 @@ mainWithOptions smtConfig = SMT.defaultConfig { SMT.timeOut = smtTimeOut - , SMT.preludeFile = smtPrelude + , SMT.resetInterval = smtResetInterval + , SMT.prelude = smtPrelude } when @@ -290,5 +257,8 @@ mainWithOptions smtTimeOut :: SMT.TimeOut smtTimeOut = timeOut smtOptions - smtPrelude :: Maybe FilePath + smtResetInterval :: SMT.ResetInterval + smtResetInterval = resetInterval smtOptions + + smtPrelude :: SMT.Prelude smtPrelude = prelude smtOptions diff --git a/kore/src/Options/SMT.hs b/kore/src/Options/SMT.hs new file mode 100644 index 0000000000..9e8205c531 --- /dev/null +++ b/kore/src/Options/SMT.hs @@ -0,0 +1,182 @@ +{- | +Copyright : (c) Runtime Verification, 2020 +License : NCSA +-} + +module Options.SMT + ( KoreSolverOptions (..) + , Solver (..) + , parseKoreSolverOptions + , unparseKoreSolverOptions + , defaultSmtPreludeFilePath + , writeKoreSolverFiles + , ensureSmtPreludeExists + ) where + +import Prelude.Kore + +import Control.Monad.Extra as Monad +import qualified Data.Char as Char +import qualified Data.Foldable as Foldable +import Data.List + ( intercalate + ) +import Options.Applicative + ( Parser + , auto + , help + , long + , metavar + , option + , readerError + , str + , strOption + , value + ) +import qualified Options.Applicative as Options +import System.Directory + ( copyFile + , doesFileExist + ) +import System.FilePath + ( () + ) + +import Data.Limit + ( Limit (..) + , maybeLimit + ) +import SMT hiding + ( Solver + , not + ) + +-- | Command line options for the SMT solver. +data KoreSolverOptions = KoreSolverOptions + { timeOut :: !TimeOut + , resetInterval :: !ResetInterval + , prelude :: !Prelude + , solver :: !Solver + } + +parseKoreSolverOptions :: Parser KoreSolverOptions +parseKoreSolverOptions = + KoreSolverOptions + <$> parseTimeOut + <*> parseResetInterval + <*> parsePrelude + <*> parseSolver + where + parseTimeOut = + option readTimeOut + ( metavar "SMT_TIMEOUT" + <> long "smt-timeout" + <> help "Timeout for calls to the SMT solver, in milliseconds" + <> value defaultTimeOut + ) + + parseResetInterval = + option readResetInterval + ( metavar "SMT_RESET_INTERVAL" + <> long "smt-reset-interval" + <> help "Reset the solver after this number of queries" + <> value defaultResetInterval + ) + + parsePrelude = + Prelude + <$> optional + ( strOption + ( metavar "SMT_PRELUDE" + <> long "smt-prelude" + <> help "Path to the SMT prelude file" + ) + ) + + SMT.Config { timeOut = defaultTimeOut } = SMT.defaultConfig + SMT.Config { resetInterval = defaultResetInterval } = SMT.defaultConfig + + readPositiveInteger ctor optionName = do + readInt <- auto + when (readInt <= 0) err + return . ctor $ readInt + where + err = + readerError + . unwords + $ [optionName, "must be a positive integer."] + + readTimeOut = readPositiveInteger (SMT.TimeOut . Limit) "smt-timeout" + readResetInterval = + readPositiveInteger SMT.ResetInterval "smt-reset-interval" + +unparseKoreSolverOptions :: KoreSolverOptions -> [String] +unparseKoreSolverOptions + KoreSolverOptions + { timeOut = TimeOut unwrappedTimeOut + , resetInterval + , prelude = Prelude unwrappedPrelude + , solver + } + = + catMaybes + [ (\limit -> unwords ["--smt-timeout", show limit]) + <$> maybeLimit Nothing Just unwrappedTimeOut + , pure $ unwords ["--smt-reset-interval", show resetInterval] + , unwrappedPrelude + $> unwords ["--smt-prelude", defaultSmtPreludeFilePath] + , pure $ "--smt " <> fmap Char.toLower (show solver) + ] + +-- | Available SMT solvers. +data Solver = Z3 | None + deriving (Eq, Ord, Show) + deriving (Enum, Bounded) + +parseSolver :: Parser Solver +parseSolver = + option (snd <$> readSum longName options) + $ metavar "SOLVER" + <> long longName + <> help ("SMT solver for checking constraints: " <> knownOptions) + <> value Z3 + where + longName = "smt" + knownOptions = intercalate ", " (map fst options) + options = [ (map Char.toLower $ show s, s) | s <- [minBound .. maxBound] ] + +readSum :: String -> [(String, value)] -> Options.ReadM (String, value) +readSum longName options = do + opt <- str + case lookup opt options of + Just val -> pure (opt, val) + _ -> readerError (unknown opt ++ known) + where + knownOptions = intercalate ", " (map fst options) + unknown opt = "Unknown " ++ longName ++ " '" ++ opt ++ "'. " + known = "Known " ++ longName ++ "s are: " ++ knownOptions ++ "." + +defaultSmtPreludeFilePath :: FilePath +defaultSmtPreludeFilePath = "prelude.smt2" + +writeKoreSolverFiles :: KoreSolverOptions -> FilePath -> IO () +writeKoreSolverFiles + KoreSolverOptions { prelude = Prelude unwrappedPrelude } + reportFile + = + Foldable.for_ unwrappedPrelude + $ flip copyFile (reportFile defaultSmtPreludeFilePath) + +-- | Ensure that the SMT prelude file exists, if specified. +ensureSmtPreludeExists :: KoreSolverOptions -> IO () +ensureSmtPreludeExists + KoreSolverOptions + { prelude = SMT.Prelude unwrappedPrelude } + = + Foldable.traverse_ + (\filePath -> + Monad.whenM + (not <$> doesFileExist filePath) + (error $ "SMT prelude file does not exist: " <> filePath) + ) + unwrappedPrelude diff --git a/kore/src/SMT.hs b/kore/src/SMT.hs index bf7e2cec59..f37f2cfa93 100644 --- a/kore/src/SMT.hs +++ b/kore/src/SMT.hs @@ -15,6 +15,8 @@ module SMT , Config (..) , defaultConfig , TimeOut (..) + , ResetInterval (..) + , Prelude (..) , Result (..) , Constructor (..) , ConstructorArgument (..) @@ -343,14 +345,15 @@ unshareSolverHandle action = do {- | Increase the 'queryCounter' and indicate if the solver should be reset. -} -incrementQueryCounter :: Monad monad => StateT SolverHandle monad Bool -incrementQueryCounter = do +incrementQueryCounter + :: Monad monad => ResetInterval -> StateT SolverHandle monad Bool +incrementQueryCounter (ResetInterval resetInterval) = do Lens.modifying (field @"queryCounter") (+ 1) counter <- Lens.use (field @"queryCounter") -- Due to an issue with the SMT solver, we need to reinitialise it after a -- number of runs, specified here. This number can be adjusted based on -- experimentation. - pure (counter >= 100) + pure (toInteger counter >= resetInterval) instance MonadSMT SMT where withSolver action = @@ -359,7 +362,10 @@ instance MonadSMT SMT where Exception.finally action (do withSolver' pop - needReset <- modifySolverHandle incrementQueryCounter + resetInterval' <- extractResetInterval + needReset <- + modifySolverHandle + (incrementQueryCounter resetInterval') when needReset reinit ) @@ -422,19 +428,29 @@ instance MonadSMT m => MonadSMT (ExceptT e m) newtype TimeOut = TimeOut { getTimeOut :: Limit Integer } deriving (Eq, Ord, Read, Show) +-- | Reset interval for solver. +newtype ResetInterval = + ResetInterval { getResetInterval :: Integer } + deriving (Eq, Ord, Read, Show) + +-- | Optional filepath for the SMT prelude. +newtype Prelude = Prelude { getPrelude :: Maybe FilePath } + -- | Solver configuration data Config = Config - { executable :: FilePath + { executable :: !FilePath -- ^ solver executable file name - , arguments :: [String] + , arguments :: ![String] -- ^ default command-line arguments to solver - , preludeFile :: Maybe FilePath + , prelude :: !Prelude -- ^ prelude of definitions to initialize solver - , logFile :: Maybe FilePath + , logFile :: !(Maybe FilePath) -- ^ optional log file name - , timeOut :: TimeOut + , timeOut :: !TimeOut -- ^ query time limit + , resetInterval :: !ResetInterval + -- ^ reset solver after this number of queries } -- | Default configuration using the Z3 solver. @@ -446,16 +462,19 @@ defaultConfig = [ "-smt2" -- use SMT-LIB2 format , "-in" -- read from standard input ] - , preludeFile = Nothing + , prelude = Prelude Nothing , logFile = Nothing , timeOut = TimeOut (Limit 40) + , resetInterval = ResetInterval 100 } initSolver :: Config -> SMT () -initSolver Config { timeOut, preludeFile } = do +initSolver Config { timeOut, prelude } = do setTimeOut timeOut Foldable.traverse_ loadFile preludeFile join $ SMT (Reader.asks userInit) + where + preludeFile = getPrelude prelude {- | Initialize a new solverHandle with the given 'Config'. @@ -538,3 +557,9 @@ setTimeOut TimeOut { getTimeOut } = setOption ":timeout" (SimpleSMT.int timeOut) Unlimited -> return () + +-- | Extract the reset interval value from the configuration. +extractResetInterval :: SMT ResetInterval +extractResetInterval = + SMT (Reader.asks config) + >>= return . resetInterval