Skip to content

Commit 742087a

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents bc4baaf + f1e3717 commit 742087a

File tree

5 files changed

+68
-25
lines changed

5 files changed

+68
-25
lines changed

‎booster/library/Booster/JsonRpc.hs‎

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,8 @@ import Booster.Log
4646
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
4747
import Booster.Pattern.Base (Pattern (..), Sort (SortApp))
4848
import Booster.Pattern.Base qualified as Pattern
49+
import Booster.Pattern.Bool (isFalse)
50+
import Booster.Pattern.Bool qualified as Pattern
4951
import Booster.Pattern.Implies (runImplies)
5052
import Booster.Pattern.Pretty
5153
import Booster.Pattern.Rewrite (
@@ -255,13 +257,18 @@ respond stateVar request =
255257
withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
256258
logMessage ("ignoring unsupported predicate parts" :: Text)
257259
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
258-
(Right newPattern, _) -> do
259-
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
260-
tSort = externaliseSort (sortOfPattern newPattern)
261-
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
262-
[] -> term
263-
ps -> KoreJson.KJAnd tSort $ term : ps
264-
pure $ Right (addHeader result)
260+
(Right newPattern, _) ->
261+
if Pattern.isBottom newPattern
262+
then
263+
let tSort = externaliseSort $ sortOfPattern pat
264+
in pure $ Right (addHeader $ KoreJson.KJBottom tSort)
265+
else do
266+
let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
267+
tSort = externaliseSort (sortOfPattern newPattern)
268+
result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
269+
[] -> term
270+
ps -> KoreJson.KJAnd tSort $ term : ps
271+
pure $ Right (addHeader result)
265272
(Left ApplyEquations.SideConditionFalse{}, _) -> do
266273
let tSort = externaliseSort $ sortOfPattern pat
267274
pure $ Right (addHeader $ KoreJson.KJBottom tSort)
@@ -299,8 +306,10 @@ respond stateVar request =
299306
<> map (externaliseCeil predicateSort) ps.ceilPredicates
300307
<> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
301308
<> ps.unsupported
302-
303-
pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
309+
pure . Right $
310+
if any isFalse simplified
311+
then addHeader $ KoreJson.KJBottom predicateSort
312+
else addHeader $ Syntax.KJAnd predicateSort result
304313
(Left something, _) ->
305314
pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something
306315
SMT.finaliseSolver solver

‎booster/library/Booster/Pattern/Rewrite.hs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1034,7 +1034,9 @@ performRewrite rewriteConfig pat = do
10341034
case res of
10351035
Right newPattern -> do
10361036
emitRewriteTrace $ RewriteSimplified Nothing
1037-
pure $ Just newPattern
1037+
if isBottom newPattern
1038+
then pure Nothing
1039+
else pure $ Just newPattern
10381040
Left r@SideConditionFalse{} -> do
10391041
emitRewriteTrace $ RewriteSimplified (Just r)
10401042
pure Nothing

‎booster/test/rpc-integration/test-vacuous/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Tests for `kore-rpc-booster` returning vacuous results after simplification
22

3-
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.
3+
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.
44

55
The `diamond/test.k` semantics is used, which consists of simple state
66
transition rules featuring additional constraints on a variable

‎booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json‎

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -155,13 +155,29 @@
155155
"value": "true"
156156
},
157157
"second": {
158-
"tag": "DV",
159-
"sort": {
160-
"tag": "SortApp",
161-
"name": "SortBool",
162-
"args": []
163-
},
164-
"value": "false"
158+
"tag": "App",
159+
"name": "Lbl'UndsEqlsSlshEqls'Int'Unds'",
160+
"sorts": [],
161+
"args": [
162+
{
163+
"tag": "DV",
164+
"sort": {
165+
"tag": "SortApp",
166+
"name": "SortInt",
167+
"args": []
168+
},
169+
"value": "0"
170+
},
171+
{
172+
"tag": "DV",
173+
"sort": {
174+
"tag": "SortApp",
175+
"name": "SortInt",
176+
"args": []
177+
},
178+
"value": "0"
179+
}
180+
]
165181
}
166182
}
167183
}

‎booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json‎

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -155,13 +155,29 @@
155155
"value": "true"
156156
},
157157
"second": {
158-
"tag": "DV",
159-
"sort": {
160-
"tag": "SortApp",
161-
"name": "SortBool",
162-
"args": []
163-
},
164-
"value": "false"
158+
"tag": "App",
159+
"name": "Lbl'UndsEqlsSlshEqls'Int'Unds'",
160+
"sorts": [],
161+
"args": [
162+
{
163+
"tag": "DV",
164+
"sort": {
165+
"tag": "SortApp",
166+
"name": "SortInt",
167+
"args": []
168+
},
169+
"value": "0"
170+
},
171+
{
172+
"tag": "DV",
173+
"sort": {
174+
"tag": "SortApp",
175+
"name": "SortInt",
176+
"args": []
177+
},
178+
"value": "0"
179+
}
180+
]
165181
}
166182
}
167183
}

0 commit comments

Comments
 (0)