Revert "Revert "Enable preserving-definedness ... (#440)" (#441)

~Blocked on #453 This reverts commit c6edfad. This PR brings back the preserves-definiteness attribute addition. ~It sometimes causes rules with question mark variables to apply in Booster, which causes a failure in `pyk`. We cannot re-apply this change until we have a fix for `test-question-mark` variable integration test. We also need to change `test-existential`.~
runtimeverification · Jan 15, 2024 · 4948a2f · 4948a2f
1 parent bdc5d37
commit 4948a2f
Show file tree

Hide file tree

Showing 6 changed files with 188 additions and 2 deletions.
diff --git 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
@@ -42,7 +42,7 @@ for dir in $(ls -d test-*); do
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             SERVER=$KORE_RPC_DEV ./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
@@ -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
@@ -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
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
@@ -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"
+                                }
+                            ]
+                        }
+                    ]
+                }
+            }
+        }
+    }
+}
diff --git a/test/rpc-integration/test-compute-ceil/state-evaluate-g.execute 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"
+          }
+        ]
+      }
+    ]
+  }
+}