Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into _update-deps/runtim…
Browse files Browse the repository at this point in the history 
…everification/k
  • Loading branch information
devops committed Oct 31, 2024
2 parents b03a079 + f1e3717 commit d8ff344
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 d8ff344

Please sign in to comment.