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

3888 typed context and parser #3950

Merged
merged 18 commits into from
Jun 20, 2024
Merged

3888 typed context and parser #3950

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
2362d3e
Prior art: beginnings of parsing json context log
jberthold May 31, 2024
31e682b
adjust context type, reduce logline type just for testing
jberthold Jun 18, 2024
70c8168
WIP converting booster context logs to typed context
jberthold Jun 18, 2024
4c1ef28
Booster.Log type-checks, patterns for export
jberthold Jun 18, 2024
9deaf22
convert all logging call sites
jberthold Jun 19, 2024
2fc8bc9
formatting
jberthold Jun 19, 2024
c9677c4
Make UniqueId carry text instead of a number
jberthold Jun 19, 2024
5e80967
add hook-related lines to expected output for log-simplify-json test
jberthold Jun 19, 2024
a52f505
Refactoring to get rid of the patterns
jberthold Jun 19, 2024
bb29933
convert count-aborts app, make context a 'Seq' in LogLine
jberthold Jun 19, 2024
a880455
Use TH to derive the JSON instances (for performance)
jberthold Jun 20, 2024
40d47e6
Merge branch 'master' into 3888-typed-context-and-parser
jberthold Jun 20, 2024
a510b1a
fix kore-term tag (requires camelcase-ing)
jberthold Jun 20, 2024
bcef5c3
pimp show instance for SimpleContext to match json representation
jberthold Jun 20, 2024
3257cc5
Format with fourmolu
invalid-email-address Jun 20, 2024
0138c99
remove redundant import
jberthold Jun 20, 2024
8c33434
Anti-capitalism
jberthold Jun 20, 2024
2ab0fc0
Merge branch 'master' into 3888-typed-context-and-parser
jberthold Jun 20, 2024
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: 22 additions & 22 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,14 +103,14 @@ respond stateVar =
| isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String)
| isJust req.movingAverageStepTimeout ->
pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "execute" $ do
RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ do
start <- liftIO $ getTime Monotonic
-- internalise given constrained term
let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term

case internalised of
Left patternError -> do
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
Expand Down Expand Up @@ -152,7 +152,7 @@ respond stateVar =
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
else Nothing
pure $ execResponse duration req result substitution unsupported
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext "add-module" $ runExceptT $ do
RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
-- block other request executions while modifying the server state
state <- liftIO $ takeMVar stateVar
let nameAsId = fromMaybe False nameAsId'
Expand Down Expand Up @@ -213,7 +213,7 @@ respond stateVar =
Booster.Log.logMessage $
"Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "simplify" $ do
RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do
start <- liftIO $ getTime Monotonic
let internalised =
runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
Expand All @@ -228,7 +228,7 @@ respond stateVar =
result <- case internalised of
Left patternErrors -> do
forM_ patternErrors $ \patternError ->
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
Expand Down Expand Up @@ -273,7 +273,7 @@ respond stateVar =
logMessage ("ignoring unsupported predicate parts" :: Text)
-- apply the given substitution before doing anything else
let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
withContext "constraint" $
withContext CtxConstraint $
ApplyEquations.simplifyConstraints
def
mLlvmLibrary
Expand Down Expand Up @@ -305,7 +305,7 @@ respond stateVar =
pure $ second mkSimplifyResponse result
RpcTypes.GetModel req -> withModule req._module $ \case
(_, _, Nothing) -> do
withContext "get-model" $
withContext CtxGetModel $
logMessage' ("get-model request, not supported without SMT solver" :: Text)
pure $ Left RpcError.notImplemented
(def, _, Just smtOptions) -> do
Expand All @@ -315,7 +315,7 @@ respond stateVar =
case internalised of
Left patternErrors -> do
forM_ patternErrors $ \patternError ->
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
Expand All @@ -327,20 +327,20 @@ respond stateVar =
(boolPs, suppliedSubst) <-
case things of
TermAndPredicates pat substitution unsupported -> do
withContext "get-model" $
withContext CtxGetModel $
logMessage' ("ignoring supplied terms and only checking predicates" :: Text)

unless (null unsupported) $ do
withContext "get-model" $ do
withContext CtxGetModel $ do
logMessage' ("ignoring unsupported predicates" :: Text)
withContext "detail" $
withContext CtxDetail $
logMessage (Text.unwords $ map prettyPattern unsupported)
pure (Set.toList pat.constraints, substitution)
Predicates ps -> do
unless (null ps.ceilPredicates && null ps.unsupported) $ do
withContext "get-model" $ do
withContext CtxGetModel $ do
logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text)
withContext "detail" $
withContext CtxDetail $
logMessage
( Text.unlines $
map
Expand All @@ -354,8 +354,8 @@ respond stateVar =
if null boolPs && Map.null suppliedSubst
then do
-- as per spec, no predicate, no answer
withContext "get-model" $
withContext "smt" $
withContext CtxGetModel $
withContext CtxSMT $
logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
pure $ Left SMT.Unknown
else do
Expand All @@ -365,8 +365,8 @@ respond stateVar =
case result of
Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors
Right response -> pure response
withContext "get-model" $
withContext "smt" $
withContext CtxGetModel $
withContext CtxSMT $
logMessage $
"SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult)
pure . Right . RpcTypes.GetModel $ case smtResult of
Expand Down Expand Up @@ -413,22 +413,22 @@ respond stateVar =
{ satisfiable = RpcTypes.Sat
, substitution
}
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ do
RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do
-- internalise given constrained term
let internalised =
runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials

case (internalised req.antecedent.term, internalised req.consequent.term) of
(Left patternError, _) -> do
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
RpcError.CouldNotVerifyPattern
[ patternErrorToRpcError patternError
]
(_, Left patternError) -> do
void $ Booster.Log.withContext "internalise" $ logPatternError patternError
void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError
pure $
Left $
RpcError.backendError $
Expand All @@ -440,11 +440,11 @@ respond stateVar =
logMessage'
("aborting due to unsupported predicate parts" :: Text)
unless (null unsupportedL) $
withContext "detail" $
withContext CtxDetail $
logMessage
(Text.unwords $ map prettyPattern unsupportedL)
unless (null unsupportedR) $
withContext "detail" $
withContext CtxDetail $
logMessage
(Text.unwords $ map prettyPattern unsupportedR)
let
Expand Down
Loading
Loading