Skip to content

Commit

Permalink
Turn Pattern into #Bottom if any constraint is literal false (#4069)
Browse files Browse the repository at this point in the history 
- before returning a `"simplify"` response, check if any constrains are
`false` and return `#Bottom` in that case
- when simplifying rewriting results, prune branches if there's a
literal `false`
- this triggers the change in the `test-vacuous` integration test, where
the original state is now returned.
[simplifyP](https://github.com/runtimeverification/haskell-backend/blob/booster-bottom-on-false-constaint/booster/library/Booster/Pattern/Rewrite.hs#L1029)
now returns `Nothing` for the result and thus we get to return
`RewriteTrivial` from `performRewrite`
- note that the outdated responses for this integration tests actually
had a literal `false` as one of the constraints.
  • Loading branch information
@geo2a
geo2a authored Oct 30, 2024
1 parent 328cd2c commit f1e3717
Show file tree
Hide file tree
Showing 5 changed files with 68 additions and 25 deletions.
27 changes: 18 additions & 9 deletions booster/library/Booster/JsonRpc.hs
View file
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
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
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
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
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

0 comments on commit f1e3717

Please sign in to comment.