Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

(Dev.) Options to control fall-back reasons and post-exec simplification #436

Merged
merged 4 commits into from
Dec 19, 2023
Merged

(Dev.) Options to control fall-back reasons and post-exec simplification #436

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
28bac67
(Dev.) Options to control fall-back reasons and post-exec simplification
jberthold Dec 19, 2023
baf741a
Format with fourmolu
invalid-email-address Dec 19, 2023
c91c446
Harmonize default value display
geo2a Dec 19, 2023
4e6ea00
Merge branch 'main' into 434-options-for-fallback-reasons-and-post-ex…
jberthold Dec 19, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 21 additions & 23 deletions tools/booster/Proxy.hs
View file
Open in desktop
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
Open in desktop
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