From ad469900f0551af07c7a5dc64ac5c9297012fb2c Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Mon, 18 Dec 2023 14:04:30 +0100 Subject: [PATCH] Enable preserving-definedness atrribute for rules discovered during ceil analysis (#426) Closes #424. This is a fix for the ceil analysis introduced in #402. We successfully infer definedness, but don't currently mark the rules as preserving definedness correctly. The added integration tests makes sure that a rule that contains a partial function on the RHS (discovered to be preserving definedness during the ceil analysis) will apply during execution. --------- Co-authored-by: Jost Berthold Co-authored-by: rv-jenkins --- library/Booster/Definition/Ceil.hs | 7 +- scripts/integration-tests.sh | 2 +- test/rpc-integration/resources/compute-ceil.k | 9 ++ .../resources/compute-ceil.kompile | 7 ++ .../response-evaluate-g.booster-dev | 84 +++++++++++++++++++ .../state-evaluate-g.execute | 81 ++++++++++++++++++ 6 files changed, 188 insertions(+), 2 deletions(-) create mode 100644 test/rpc-integration/resources/compute-ceil.k create mode 100755 test/rpc-integration/resources/compute-ceil.kompile create mode 100644 test/rpc-integration/test-compute-ceil/response-evaluate-g.booster-dev create mode 100644 test/rpc-integration/test-compute-ceil/state-evaluate-g.execute diff --git a/library/Booster/Definition/Ceil.hs b/library/Booster/Definition/Ceil.hs index e6f4557c7..58efc24da 100644 --- a/library/Booster/Definition/Ceil.hs +++ b/library/Booster/Definition/Ceil.hs @@ -108,7 +108,12 @@ computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attribut , ceils = requiresCeils <> rhsCeils , newRule = if null requiresCeils && null rhsCeils - then Just r{RewriteRule.attributes = attributes{preserving = Flag True}} + then + Just + r + { RewriteRule.attributes = attributes{preserving = Flag True} + , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []} + } else -- we could add a case when ceils are fully resolved into predicates, which we would then -- add to the requires clause of a rule Nothing diff --git a/scripts/integration-tests.sh b/scripts/integration-tests.sh index d2ca4c2b1..9319c3ceb 100755 --- a/scripts/integration-tests.sh +++ b/scripts/integration-tests.sh @@ -38,7 +38,7 @@ for dir in $(ls -d test-*); do SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;; - "no-evaluator") + "compute-ceil" | "no-evaluator") SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@ ;; "foundry-bug-report") diff --git a/test/rpc-integration/resources/compute-ceil.k b/test/rpc-integration/resources/compute-ceil.k new file mode 100644 index 000000000..6fcbeee0c --- /dev/null +++ b/test/rpc-integration/resources/compute-ceil.k @@ -0,0 +1,9 @@ +module COMPUTE-CEIL + imports INT + imports ID-SYNTAX + + syntax Foo ::= g ( Int ) + + rule g ( N:Int ) => N %Int 5 + +endmodule diff --git a/test/rpc-integration/resources/compute-ceil.kompile b/test/rpc-integration/resources/compute-ceil.kompile new file mode 100755 index 000000000..d928aa2fc --- /dev/null +++ b/test/rpc-integration/resources/compute-ceil.kompile @@ -0,0 +1,7 @@ +echo "kompiling compute-ceil.k" +kompile --backend haskell compute-ceil.k +cp compute-ceil-kompiled/definition.kore compute-ceil.kore +rm -r compute-ceil-kompiled +kompile --llvm-kompile-type c -o compute-ceil-library compute-ceil.k +cp compute-ceil-library/interpreter.* ./compute-ceil.dylib +rm -r compute-ceil-library \ No newline at end of file diff --git a/test/rpc-integration/test-compute-ceil/response-evaluate-g.booster-dev b/test/rpc-integration/test-compute-ceil/response-evaluate-g.booster-dev new file mode 100644 index 000000000..3f1e54c06 --- /dev/null +++ b/test/rpc-integration/test-compute-ceil/response-evaluate-g.booster-dev @@ -0,0 +1,84 @@ +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "reason": "aborted", + "depth": 1, + "state": { + "term": { + "format": "KORE", + "version": 1, + "term": { + "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": "SortInt", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "2" + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } + } + } + } +} \ No newline at end of file diff --git a/test/rpc-integration/test-compute-ceil/state-evaluate-g.execute b/test/rpc-integration/test-compute-ceil/state-evaluate-g.execute new file mode 100644 index 000000000..3bcc34466 --- /dev/null +++ b/test/rpc-integration/test-compute-ceil/state-evaluate-g.execute @@ -0,0 +1,81 @@ +{ + "format": "KORE", + "version": 1, + "term": { + "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": "SortFoo", + "args": [] + }, + { + "tag": "SortApp", + "name": "SortKItem", + "args": [] + } + ], + "args": [ + { + "tag": "App", + "name": "Lblg'LParUndsRParUnds'COMPUTE-CEIL'Unds'Foo'Unds'Int", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "12" + } + ] + } + ] + }, + { + "tag": "App", + "name": "dotk", + "sorts": [], + "args": [] + } + ] + } + ] + }, + { + "tag": "App", + "name": "Lbl'-LT-'generatedCounter'-GT-'", + "sorts": [], + "args": [ + { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + ] + } + ] + } +}