diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index a6654c141c..0b1a2102f4 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -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 ( @@ -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) @@ -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 diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 68ab3a0b5d..0c60754a7e 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -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 diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md index 80b71a94c7..f5cc75a0c8 100644 --- a/booster/test/rpc-integration/test-vacuous/README.md +++ b/booster/test/rpc-integration/test-vacuous/README.md @@ -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 diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json index c604e9284f..f5792161a3 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json @@ -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" + } + ] } } } diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json index 9bb9e7c837..ce2d1d7174 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json @@ -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" + } + ] } } }