From 0c92b66dd65944b0f295b28162248197892017fd Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Wed, 21 Aug 2024 12:09:29 +0200 Subject: [PATCH] Don't check initial constraints when "assume-state-defined" --- booster/library/Booster/JsonRpc.hs | 7 +- .../params-unchecked-vacuous-rewrite.json | 1 + .../params-vacuous-but-rewritten.json | 1 + .../response-unchecked-vacuous-rewrite.json | 221 ++++++++++++++++++ .../response-vacuous-but-rewritten.json | 221 ++++++++++++++++++ .../state-unchecked-vacuous-rewrite.execute | 1 + .../state-vacuous-but-rewritten.execute | 1 + docs/2022-07-18-JSON-RPC-Server-API.md | 2 +- 8 files changed, 453 insertions(+), 2 deletions(-) create mode 100644 booster/test/rpc-integration/test-vacuous/params-unchecked-vacuous-rewrite.json create mode 100644 booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json create mode 100644 booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.json create mode 100644 booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json create mode 120000 booster/test/rpc-integration/test-vacuous/state-unchecked-vacuous-rewrite.execute create mode 120000 booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index b2a1593564..a5716fba05 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -131,6 +131,11 @@ respond stateVar request = [ req.logSuccessfulRewrites , req.logFailedRewrites ] + checkConstraintsConsistent = + case req.assumeStateDefined of + Nothing -> ApplyEquations.CheckConstraintsConsistent + Just False -> ApplyEquations.CheckConstraintsConsistent + Just True -> ApplyEquations.NoCheckConstraintsConsistent -- apply the given substitution before doing anything else let substPat = Pattern @@ -154,7 +159,7 @@ respond stateVar request = mLlvmLibrary solver mempty - ApplyEquations.CheckConstraintsConsistent + checkConstraintsConsistent substPat case evaluatedInitialPattern of diff --git a/booster/test/rpc-integration/test-vacuous/params-unchecked-vacuous-rewrite.json b/booster/test/rpc-integration/test-vacuous/params-unchecked-vacuous-rewrite.json new file mode 100644 index 0000000000..0ab8ffbc67 --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/params-unchecked-vacuous-rewrite.json @@ -0,0 +1 @@ +{ "assume-state-defined": true } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json new file mode 100644 index 0000000000..0ab8ffbc67 --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/params-vacuous-but-rewritten.json @@ -0,0 +1 @@ +{ "assume-state-defined": true } \ No newline at end of file diff --git a/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.json new file mode 100644 index 0000000000..becb8238f5 --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/response-unchecked-vacuous-rewrite.json @@ -0,0 +1,221 @@ +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "reason": "stuck", + "depth": 0, + "state": { + "term": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "patterns": [ + { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "value": "d" + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + }, + { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + ] + } + ] + } + } + } + } +} \ No newline at end of file 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 new file mode 100644 index 0000000000..76893afa95 --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json @@ -0,0 +1,221 @@ +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "reason": "stuck", + "depth": 1, + "state": { + "term": { + "format": "KORE", + "version": 1, + "term": { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "patterns": [ + { + "tag": "App", + "name": "Lbl'-LT-'generatedTop'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'-LT-'k'-GT-'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "kseq", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "inj", + "sorts": [ + { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "value": "d" + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'int'-GT-'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + }, + { + "tag": "And", + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "LblnotBool'Unds'", + "sorts": [], + "args": [ + { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + ] + } + ] + } + } + } + } +} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-vacuous/state-unchecked-vacuous-rewrite.execute b/booster/test/rpc-integration/test-vacuous/state-unchecked-vacuous-rewrite.execute new file mode 120000 index 0000000000..1b8dec8c83 --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/state-unchecked-vacuous-rewrite.execute @@ -0,0 +1 @@ +state-vacuous-without-rewrite.execute \ No newline at end of file diff --git a/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute b/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute new file mode 120000 index 0000000000..bc6397970f --- /dev/null +++ b/booster/test/rpc-integration/test-vacuous/state-vacuous-but-rewritten.execute @@ -0,0 +1 @@ +state-vacuous-not-rewritten.execute \ No newline at end of file diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md index a0fe111f3c..f2b5af1c4e 100644 --- a/docs/2022-07-18-JSON-RPC-Server-API.md +++ b/docs/2022-07-18-JSON-RPC-Server-API.md @@ -43,7 +43,7 @@ The server runs over sockets and can be interacted with by sending JSON RPC mess Optional parameters: `max-depth`, `cut-point-rules`, `terminal-rules`, `moving-average-step-timeout`, `step-timeout` (timeout is in milliseconds), `module` (main module name), `assume-state-defined` (description follows) and all the `log-*` options, which default to false if unspecified. -If `assume-state-defined` is set to `true`, the all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. +The `assume-state-defined` flag has different meaning in Booster and Kore. If set to `true`, Booster will not check the constraints of the initial pattern for satisfiability. It is the responsibility of the caller to ensure that the pattern is not vacuous. In Kore, if `assume-state-defined` is set to `true`, then all sub-terms of `state` will be assumed to be defined before attempting rewrite rules. _Note: `id` can be an int or a string and each message must have a new `id`. The response objects have the same id as the message._