Skip to content

Commit

Permalink
Merge branch 'main' into sam/ceil-fetch-in_key-hooks
Browse files Browse the repository at this point in the history
  • Loading branch information
@geo2a
geo2a authored Dec 19, 2023
2 parents 1922e9e + 152d94d commit d6ccaf2
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 31 deletions.
1 change: 0 additions & 1 deletion library/Booster/Pattern/ApplyEquations.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -721,7 +721,6 @@ simplifyConstraint' recurseIntoEvalBool = \case
then TrueBool
else FalseBool
Nothing -> if recurseIntoEvalBool then evalBool t else pure t
t@(NotBool _) -> evalBool t -- always evaluate under notBool
EqualsK (KSeq _ l) (KSeq _ r) -> evalEqualsK l r
NEqualsK (KSeq _ l) (KSeq _ r) -> negateBool <$> evalEqualsK l r
t -> if recurseIntoEvalBool then evalBool t else pure t
Expand Down
10 changes: 7 additions & 3 deletions library/Booster/Pattern/Rewrite.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -665,10 +665,14 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
rewriteTrace $ RewriteSimplified traces (Just r)
pure $ Just p
Left r@(EquationLoop (t : ts)) -> do
let termDiffs = zipWith (curry mkDiffTerms) (t : ts) ts
logError "Equation evaluation loop"
logSimplify $
"produced the evaluation loop: " <> Text.unlines (map (prettyText . fst) termDiffs)
logOtherNS "booster" (LevelOther "ErrorDetails") $
let termDiffs = zipWith (curry mkDiffTerms) (t : ts) ts
l = length ts
in "Evaluation loop of length "
<> prettyText l
<> ": \n"
<> Text.unlines (map (prettyText . fst) termDiffs)
rewriteTrace $ RewriteSimplified traces (Just r)
pure $ Just p
Left other -> do
Expand Down
44 changes: 21 additions & 23 deletions tools/booster/Proxy.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,8 @@ data ProxyConfig = ProxyConfig
{ statsVar :: Maybe StatsVar
, forceFallback :: Maybe Depth
, boosterState :: MVar.MVar Booster.ServerState
, fallbackReasons :: [HaltReason]
, simplifyAtEnd :: Bool
}

serverError :: String -> Value -> ErrorObj
Expand All @@ -79,7 +81,7 @@ respondEither ::
Respond (API 'Req) m (API 'Res) ->
Respond (API 'Req) m (API 'Res) ->
Respond (API 'Req) m (API 'Res)
respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore req = case req of
respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case req of
Execute execReq
| isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout ->
loggedKore ExecuteM req
Expand Down Expand Up @@ -202,22 +204,21 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re

handleExecute :: LogSettings -> KoreDefinition -> ExecuteRequest -> m (Either ErrorObj (API 'Res))
handleExecute logSettings def =
executionLoop logSettings forceFallback def (0, 0.0, 0.0, Nothing)
executionLoop logSettings def (0, 0.0, 0.0, Nothing)

executionLoop ::
LogSettings ->
Maybe Depth ->
KoreDefinition ->
(Depth, Double, Double, Maybe [RPCLog.LogEntry]) ->
ExecuteRequest ->
m (Either ErrorObj (API 'Res))
executionLoop logSettings mforceSimplification def (currentDepth@(Depth cDepth), !time, !koreTime, !rpcLogs) r = do
executionLoop logSettings def (currentDepth@(Depth cDepth), !time, !koreTime, !rpcLogs) r = do
Log.logInfoNS "proxy" . Text.pack $
if currentDepth == 0
then "Starting execute request"
else "Iterating execute request at " <> show currentDepth
-- calculate depth limit, considering possible forced Kore simplification
let mbDepthLimit = case (mforceSimplification, r.maxDepth) of
let mbDepthLimit = case (cfg.forceFallback, r.maxDepth) of
(Just (Depth forceDepth), Just (Depth maxDepth)) ->
if cDepth + forceDepth < maxDepth
then Just $ Depth forceDepth
Expand All @@ -229,7 +230,7 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re
case bResult of
Right (Execute boosterResult)
-- the execution reached the depth bound due to a forced Kore simplification
| boosterResult.reason == DepthBound && isJust mforceSimplification -> do
| boosterResult.reason == DepthBound && isJust cfg.forceFallback -> do
Log.logInfoNS "proxy" . Text.pack $
"Forced simplification at " <> show (currentDepth + boosterResult.depth)
simplifyResult <- simplifyExecuteState logSettings r._module def boosterResult.state
Expand All @@ -247,20 +248,16 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re
]
executionLoop
logSettings
mforceSimplification
def
( currentDepth + boosterResult.depth
, time + bTime
, koreTime
, accumulatedLogs
)
r{ExecuteRequest.state = execStateToKoreJson simplifiedBoosterState}
-- if the new backend aborts, branches or gets stuck, revert to the old one
--
-- if we are stuck in the new backend we try to re-run
-- in the old one to work around any potential
-- unification bugs.
| boosterResult.reason `elem` [Aborted, Stuck, Branching] -> do
-- if we stop for a reason in fallbackReasons (default [Aborted, Stuck, Branching],
-- revert to the old backend to re-confirm and possibly proceed
| boosterResult.reason `elem` cfg.fallbackReasons -> do
Log.logInfoNS "proxy" . Text.pack $
"Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
-- simplify Booster's state with Kore's simplifier
Expand Down Expand Up @@ -325,7 +322,6 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re
]
executionLoop
logSettings
mforceSimplification
def
( currentDepth + boosterResult.depth + koreResult.depth
, time + bTime + kTime
Expand Down Expand Up @@ -431,15 +427,17 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re

postExecSimplify ::
LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res)
postExecSimplify logSettings start mbModule def = \case
Execute res ->
Execute
<$> ( simplifyResult res
`catch` ( \(err :: DecidePredicateUnknown) ->
pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err}
)
)
other -> pure other
postExecSimplify logSettings start mbModule def
| not cfg.simplifyAtEnd = pure
| otherwise = \case
Execute res ->
Execute
<$> ( simplifyResult res
`catch` ( \(err :: DecidePredicateUnknown) ->
pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err}
)
)
other -> pure other
where
-- timeLog :: TimeDiff -> Maybe [LogEntry]
timeLog stop
Expand Down
49 changes: 45 additions & 4 deletions tools/booster/Server.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,8 @@ import Control.Monad.Logger qualified as Logger
import Data.Conduit.Network (serverSettings)
import Data.IORef (writeIORef)
import Data.InternedText (globalInternedTextCache)
import Data.List (intercalate)
import Data.List.Extra (splitOn)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe, isJust, mapMaybe)
import Data.Set qualified as Set
Expand Down Expand Up @@ -56,9 +58,9 @@ import Kore.IndexedModule.MetadataTools (SmtMetadataTools)
import Kore.Internal.TermLike (TermLike, VariableName)
import Kore.JsonRpc (ServerState (..))
import Kore.JsonRpc qualified as Kore
import Kore.JsonRpc.Error
import Kore.JsonRpc.Error hiding (Aborted)
import Kore.JsonRpc.Server
import Kore.JsonRpc.Types (API, ReqOrRes (Req, Res))
import Kore.JsonRpc.Types (API, HaltReason (..), ReqOrRes (Req, Res))
import Kore.JsonRpc.Types.Depth (Depth (..))
import Kore.Log (
ExeName (..),
Expand Down Expand Up @@ -95,7 +97,14 @@ main = do
, smtOptions
, eventlogEnabledUserEvents
}
, proxyOptions = ProxyOptions{printStats, forceFallback, boosterSMT}
, proxyOptions =
ProxyOptions
{ printStats
, forceFallback
, boosterSMT
, fallbackReasons
, simplifyAtEnd
}
} = options
(logLevel, customLevels) = adjustLogLevels logLevels
levelFilter :: Logger.LogSource -> LogLevel -> Bool
Expand Down Expand Up @@ -167,7 +176,14 @@ main = do
koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT
boosterRespond = Booster.respond boosterState

proxyConfig = ProxyConfig{statsVar, forceFallback, boosterState}
proxyConfig =
ProxyConfig
{ statsVar
, forceFallback
, boosterState
, fallbackReasons
, simplifyAtEnd
}
server =
jsonRpcServer
srvSettings
Expand Down Expand Up @@ -221,6 +237,10 @@ data ProxyOptions = ProxyOptions
-- ^ force fallback every n-steps
, boosterSMT :: Bool
-- ^ whether to use an SMT solver in booster code (but keeping kore-rpc's SMT solver)
, fallbackReasons :: [HaltReason]
-- ^ halt reasons to re-execute (fallback) to double-check the result
, simplifyAtEnd :: Bool
-- ^ whether to run a post-exec simplification
}

parserInfoModifiers :: InfoMod options
Expand Down Expand Up @@ -255,6 +275,27 @@ clProxyOptionsParser =
( long "no-booster-smt"
<> help "Disable SMT solver for booster code (but keep enabled for legacy code)"
)
<*> option
(eitherReader $ mapM reasonReader . splitOn ",")
( long "fallback-on"
<> metavar "REASON1,REASON2..."
<> value [Branching, Stuck, Aborted]
<> help "Halt reasons for which requests should be re-executed with kore-rpc"
<> showDefaultWith (intercalate "," . map show)
)
<*> flag
True
False
( long "no-post-exec-simplify"
<> help "disable post-exec simplification"
)

reasonReader :: String -> Either String HaltReason
reasonReader = \case
"Branching" -> Right Branching
"Stuck" -> Right Stuck
"Aborted" -> Right Aborted
other -> Left $ "Reason `" <> other <> "' not supported"

translateSMTOpts :: Maybe SMTOptions -> KoreSMT.KoreSolverOptions
translateSMTOpts = \case
Expand Down

0 comments on commit d6ccaf2

Please sign in to comment.