Skip to content

Turn Pattern into #Bottom if any constraint is literal false #4069

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

Merged
merged 2 commits into from
Oct 30, 2024
Merged

Turn Pattern into #Bottom if any constraint is literal false #4069

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
28e7526
Turn `Pattern` into `#Bottom` if any constraint is literal false
geo2a Oct 30, 2024
c72c34b
Update integration tests
geo2a Oct 30, 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
27 changes: 18 additions & 9 deletions booster/library/Booster/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@ import Booster.Log
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
import Booster.Pattern.Base (Pattern (..), Sort (SortApp))
import Booster.Pattern.Base qualified as Pattern
import Booster.Pattern.Bool (isFalse)
import Booster.Pattern.Bool qualified as Pattern
import Booster.Pattern.Implies (runImplies)
import Booster.Pattern.Pretty
import Booster.Pattern.Rewrite (
Expand Down Expand Up @@ -255,13 +257,18 @@ respond stateVar request =
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
logMessage ("ignoring unsupported predicate parts" :: Text)
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
(Right newPattern, _) -> do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
[] -> term
ps -> KoreJson.KJAnd tSort $ term : ps
pure $ Right (addHeader result)
(Right newPattern, _) ->
if Pattern.isBottom newPattern
then
let tSort = externaliseSort $ sortOfPattern pat
in pure $ Right (addHeader $ KoreJson.KJBottom tSort)
else do
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
tSort = externaliseSort (sortOfPattern newPattern)
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
[] -> term
ps -> KoreJson.KJAnd tSort $ term : ps
pure $ Right (addHeader result)
(Left ApplyEquations.SideConditionFalse{}, _) -> do
let tSort = externaliseSort $ sortOfPattern pat
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
Expand Down Expand Up @@ -299,8 +306,10 @@ respond stateVar request =
<> map (externaliseCeil predicateSort) ps.ceilPredicates
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
<> ps.unsupported

pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
pure . Right $
if any isFalse simplified
then addHeader $ KoreJson.KJBottom predicateSort
else addHeader $ Syntax.KJAnd predicateSort result
(Left something, _) ->
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something
SMT.finaliseSolver solver
Expand Down
4 changes: 3 additions & 1 deletion booster/library/Booster/Pattern/Rewrite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1034,7 +1034,9 @@ performRewrite rewriteConfig pat = do
case res of
Right newPattern -> do
emitRewriteTrace $ RewriteSimplified Nothing
pure $ Just newPattern
if isBottom newPattern
then pure Nothing
else pure $ Just newPattern
Left r@SideConditionFalse{} -> do
emitRewriteTrace $ RewriteSimplified (Just r)
pure Nothing
Expand Down
2 changes: 1 addition & 1 deletion booster/test/rpc-integration/test-vacuous/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Tests for `kore-rpc-booster` returning vacuous results after simplification

Since `kore-rpc-booster` does not consider combinations of constraints, it won't discover when a reached state (or the initial state) simplifies to `\bottom`. In such cases, the `execute` request should return the current state with `"reason": "vacuous"` in the result.
Since Booster does not check consistently of the initial pattern before starting rewriting, it won't always discover when a reached state (or the initial state) simplifies to `\bottom`. Ultimately, `kore-rpc-booster` relies on Kore's simplifier to detect such cases. When Kore prunes a `\bottom` branch, the `execute` endpoint of `kore-rpc-booster` should return the current state with `"reason": "vacuous"` in the result.

The `diamond/test.k` semantics is used, which consists of simple state
transition rules featuring additional constraints on a variable
Expand Down
30 changes: 23 additions & 7 deletions booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,13 +155,29 @@
"value": "true"
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "false"
"tag": "App",
"name": "Lbl'UndsEqlsSlshEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
}
}
Expand Down
30 changes: 23 additions & 7 deletions booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,13 +155,29 @@
"value": "true"
},
"second": {
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortBool",
"args": []
},
"value": "false"
"tag": "App",
"name": "Lbl'UndsEqlsSlshEqls'Int'Unds'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
},
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
}
}
Expand Down
Loading