Skip to content

Commit e7d0b96

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 34fd0e1 + 6fdb95b commit e7d0b96

File tree

8 files changed

+223
-136
lines changed

8 files changed

+223
-136
lines changed

‎booster/library/Booster/CLOptions.hs‎

Lines changed: 68 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@ module Booster.CLOptions (
77
CLOptions (..),
88
EquationOptions (..),
99
LogFormat (..),
10+
LogOptions (..),
11+
RewriteOptions (..),
1012
TimestampFormat (..),
1113
clOptionsParser,
1214
adjustLogLevels,
@@ -25,6 +27,7 @@ import Data.Maybe (fromMaybe)
2527
import Data.Text (Text, pack)
2628
import Data.Text.Encoding (decodeASCII)
2729
import Data.Version (Version (..), showVersion)
30+
import Numeric.Natural (Natural)
2831
import Options.Applicative
2932

3033
import Booster.GlobalState (EquationOptions (..))
@@ -41,18 +44,23 @@ data CLOptions = CLOptions
4144
, mainModuleName :: Text
4245
, llvmLibraryFile :: Maybe FilePath
4346
, port :: Int
44-
, logLevels :: [LogLevel]
47+
, logOptions :: LogOptions
48+
, smtOptions :: Maybe SMTOptions
49+
, equationOptions :: EquationOptions
50+
, rewriteOptions :: RewriteOptions
51+
}
52+
deriving stock (Show)
53+
54+
data LogOptions = LogOptions
55+
{ logLevels :: [LogLevel]
4556
, logTimeStamps :: Bool
4657
, timeStampsFormat :: TimestampFormat
4758
, logFormat :: LogFormat
4859
, logContexts :: [ContextFilter]
4960
, logFile :: Maybe FilePath
50-
, smtOptions :: Maybe SMTOptions
51-
, equationOptions :: EquationOptions
52-
, indexCells :: [Text]
5361
, prettyPrintOptions :: [ModifierT]
5462
}
55-
deriving (Show)
63+
deriving stock (Show)
5664

5765
data LogFormat
5866
= Standard
@@ -76,6 +84,12 @@ instance Show TimestampFormat where
7684
Pretty -> "pretty"
7785
Nanoseconds -> "nanoseconds"
7886

87+
data RewriteOptions = RewriteOptions
88+
{ indexCells :: [Text]
89+
, interimSimplification :: Maybe Natural
90+
}
91+
deriving stock (Show, Eq)
92+
7993
clOptionsParser :: Parser CLOptions
8094
clOptionsParser =
8195
CLOptions
@@ -103,7 +117,15 @@ clOptionsParser =
103117
<> help "Port for the RPC server to bind to"
104118
<> showDefault
105119
)
106-
<*> many
120+
<*> parseLogOptions
121+
<*> parseSMTOptions
122+
<*> parseEquationOptions
123+
<*> parseRewriteOptions
124+
125+
parseLogOptions :: Parser LogOptions
126+
parseLogOptions =
127+
LogOptions
128+
<$> many
107129
( option
108130
(eitherReader readLogLevel)
109131
( metavar "LEVEL"
@@ -154,15 +176,6 @@ clOptionsParser =
154176
"Log file to output the logs into"
155177
)
156178
)
157-
<*> parseSMTOptions
158-
<*> parseEquationOptions
159-
<*> option
160-
(eitherReader $ mapM (readCellName . trim) . splitOn ",")
161-
( metavar "CELL-NAME[,CELL-NAME]"
162-
<> long "index-cells"
163-
<> help "Names of configuration cells to index rewrite rules with (default: 'k')"
164-
<> value []
165-
)
166179
<*> option
167180
(eitherReader $ mapM (readModifierT . trim) . splitOn ",")
168181
( metavar "PRETTY_PRINT"
@@ -202,18 +215,6 @@ clOptionsParser =
202215
"nanoseconds" -> Right Nanoseconds
203216
other -> Left $ other <> ": Unsupported timestamp format"
204217

205-
readCellName :: String -> Either String Text
206-
readCellName input
207-
| null input =
208-
Left "Empty cell name"
209-
| all isAscii input
210-
, all isPrint input =
211-
Right $ "Lbl'-LT-'" <> enquote input <> "'-GT-'"
212-
| otherwise =
213-
Left $ "Illegal non-ascii characters in `" <> input <> "'"
214-
215-
enquote = decodeASCII . encodeLabel . BS.pack
216-
217218
-- custom log levels that can be selected
218219
allowedLogLevels :: [(String, String)]
219220
allowedLogLevels =
@@ -364,13 +365,6 @@ parseSMTOptions =
364365
where
365366
smtDefaults = defaultSMTOptions
366367

367-
nonnegativeInt :: ReadM Int
368-
nonnegativeInt =
369-
auto >>= \case
370-
i
371-
| i < 0 -> readerError "must be a non-negative integer."
372-
| otherwise -> pure i
373-
374368
readTactic =
375369
either (readerError . ("Invalid s-expression. " <>)) pure . SMT.parseSExpr . BS.pack =<< str
376370

@@ -397,12 +391,46 @@ parseEquationOptions =
397391
defaultMaxIterations = 100
398392
defaultMaxRecursion = 5
399393

400-
nonnegativeInt :: ReadM Int
401-
nonnegativeInt =
402-
auto >>= \case
403-
i
404-
| i < 0 -> readerError "must be a non-negative integer."
405-
| otherwise -> pure i
394+
parseRewriteOptions :: Parser RewriteOptions
395+
parseRewriteOptions =
396+
RewriteOptions
397+
<$> option
398+
(eitherReader $ mapM (readCellName . trim) . splitOn ",")
399+
( metavar "CELL-NAME[,CELL-NAME]"
400+
<> long "index-cells"
401+
<> help "Names of configuration cells to index rewrite rules with (default: 'k')"
402+
<> value []
403+
)
404+
<*> optional
405+
( option
406+
(intWith (> 0))
407+
( metavar "DEPTH"
408+
<> long "simplify-each"
409+
<> help "If given: Simplify the term each time the given rewrite depth is reached"
410+
)
411+
)
412+
where
413+
readCellName :: String -> Either String Text
414+
readCellName input
415+
| null input =
416+
Left "Empty cell name"
417+
| all isAscii input
418+
, all isPrint input =
419+
Right $ "Lbl'-LT-'" <> enquote input <> "'-GT-'"
420+
| otherwise =
421+
Left $ "Illegal non-ascii characters in `" <> input <> "'"
422+
423+
enquote = decodeASCII . encodeLabel . BS.pack
424+
425+
intWith :: Integral i => (Integer -> Bool) -> ReadM i
426+
intWith p =
427+
auto >>= \case
428+
i
429+
| not (p i) -> readerError $ show i <> ": Invalid integer value."
430+
| otherwise -> pure (fromIntegral i)
431+
432+
nonnegativeInt :: Integral i => ReadM i
433+
nonnegativeInt = intWith (>= 0)
406434

407435
versionInfoParser :: Parser (a -> a)
408436
versionInfoParser =

‎booster/library/Booster/JsonRpc.hs‎

Lines changed: 31 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ import Numeric.Natural
4141
import Prettyprinter (comma, hsep, punctuate, (<+>))
4242
import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)
4343

44+
import Booster.CLOptions (RewriteOptions (..))
4445
import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
4546
import Booster.Definition.Base (KoreDefinition (..))
4647
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
@@ -53,6 +54,7 @@ import Booster.Pattern.Bool (pattern TrueBool)
5354
import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
5455
import Booster.Pattern.Pretty
5556
import Booster.Pattern.Rewrite (
57+
RewriteConfig (..),
5658
RewriteFailed (..),
5759
RewriteResult (..),
5860
RewriteTrace (..),
@@ -108,7 +110,7 @@ respond stateVar request =
108110
| isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String)
109111
| isJust req.movingAverageStepTimeout ->
110112
pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
111-
RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ do
113+
RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, rewriteOpts) -> Booster.Log.withContext CtxExecute $ do
112114
start <- liftIO $ getTime Monotonic
113115
-- internalise given constrained term
114116
let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -152,8 +154,25 @@ respond stateVar request =
152154
]
153155

154156
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
157+
158+
logger <- getLogger
159+
prettyModifiers <- getPrettyModifiers
160+
let rewriteConfig =
161+
RewriteConfig
162+
{ definition = def
163+
, llvmApi = mLlvmLibrary
164+
, smtSolver = solver
165+
, varsToAvoid = substVars
166+
, doTracing
167+
, logger
168+
, prettyModifiers
169+
, mbMaxDepth = mbDepth
170+
, mbSimplify = rewriteOpts.interimSimplification
171+
, cutLabels = cutPoints
172+
, terminalLabels = terminals
173+
}
155174
result <-
156-
performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals substPat
175+
performRewrite rewriteConfig substPat
157176
SMT.finaliseSolver solver
158177
stop <- liftIO $ getTime Monotonic
159178
let duration =
@@ -224,7 +243,7 @@ respond stateVar request =
224243
Booster.Log.logMessage $
225244
"Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
226245
pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
227-
RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do
246+
RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxSimplify $ do
228247
start <- liftIO $ getTime Monotonic
229248
let internalised =
230249
runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -315,11 +334,11 @@ respond stateVar request =
315334
RpcTypes.SimplifyResult{state, logs = mkTraces duration}
316335
pure $ second mkSimplifyResponse result
317336
RpcTypes.GetModel req -> withModule req._module $ \case
318-
(_, _, Nothing) -> do
337+
(_, _, Nothing, _) -> do
319338
withContext CtxGetModel $
320339
logMessage' ("get-model request, not supported without SMT solver" :: Text)
321340
pure $ Left RpcError.notImplemented
322-
(def, _, Just smtOptions) -> do
341+
(def, _, Just smtOptions, _) -> do
323342
let internalised =
324343
runExcept $
325344
internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -419,7 +438,7 @@ respond stateVar request =
419438
{ satisfiable = RpcTypes.Sat
420439
, substitution
421440
}
422-
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do
441+
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxImplies $ do
423442
-- internalise given constrained term
424443
let internalised =
425444
runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials
@@ -504,7 +523,7 @@ respond stateVar request =
504523
where
505524
withModule ::
506525
Maybe Text ->
507-
( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions) ->
526+
( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions, RewriteOptions) ->
508527
m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
509528
) ->
510529
m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
@@ -513,7 +532,7 @@ respond stateVar request =
513532
let mainName = fromMaybe state.defaultMain mbMainModule
514533
case Map.lookup mainName state.definitions of
515534
Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
516-
Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions)
535+
Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions)
517536

518537
doesNotImply s l r =
519538
pure $
@@ -571,9 +590,11 @@ data ServerState = ServerState
571590
, defaultMain :: Text
572591
-- ^ default main module (initially from command line, could be changed later)
573592
, mLlvmLibrary :: Maybe LLVM.API
574-
-- ^ optional LLVM simplification library
593+
-- ^ Read-only: optional LLVM simplification library
575594
, mSMTOptions :: Maybe SMT.SMTOptions
576-
-- ^ (optional) SMT solver options
595+
-- ^ Read-only: (optional) SMT solver options
596+
, rewriteOptions :: RewriteOptions
597+
-- ^ Read-only: configuration related to booster rewriting
577598
, addedModules :: Map Text Text
578599
-- ^ map of raw modules added via add-module
579600
}

0 commit comments

Comments
 (0)