Update integration tests

runtimeverification · Aug 7, 2024 · 84b3b61 · 84b3b61
1 parent 2025987
commit 84b3b61
Show file tree

Hide file tree

Showing 12 changed files with 93 additions and 453 deletions.
diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
@@ -1,6 +1,7 @@
 {"context":["proxy"],"message":"Loading definition from resources/log-simplify-json.kore, main module \"IMP-VERIFICATION\""}
 {"context":["proxy"],"message":"Starting RPC server"}
 {"context":["proxy"],"message":"Processing request 4"}
+{"context":[{"request":"4"},"booster","execute",{"term":"bd7c50d"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"match","failure","continue"],"message":"Sorts differ: Eq#VarKResult:SortKResult{} =/= !__EXPRESSIONS-SYNTAX_Expr_Expr(_<=__EXPRESSIONS-SYNTAX_Expr_Expr_Expr(\"$n\", \"0\"))"}
 {"context":[{"request":"4"},"booster","execute",{"term":"4b03f8b"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"a2a070a"},{"function":"afefecb36598372bc1ba6e5d0b24a00b91796244dc3bd7435e40ca6e9ab33d4b"},"detail"],"message":"UNKNOWN"}
@@ -51,7 +52,6 @@
 {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"}
-{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"d3dc513"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}}
 {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}}

diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md
@@ -31,17 +31,16 @@ NB: Booster applies the given substitution before performing any action.
   - with an additional constraint `Y = 1 +Int X` (internalised as a substitution)
   - leading to a contradictory constraint `X = 1 +Int X` after
     rewriting and adding `Y =Int X` from the `ensures`-clause
-    - `kore-rpc-booster` returns `vacuous` after 1 step
-    - `kore-rpc-dev` returns `vacuous` after 0 steps (detects the contradiction earlier)
-    - `kore-rpc-dev` reproduces the exact input as `state` while
-      `kore-rpc-booster` splits off `substitution` (from input) and `predicate` (from the rule)
+    - `kore-rpc-booster` and `booster-dev` return `vacuous` after 0 step, substitution `Y` for `X +Int 1` in the state. However, `kore-rpc-booster` and `booster-dev` disagree a little on the value in the substitution, hence the two responses.
+    - `kore-rpc-dev` returns `vacuous` after 0 steps and reproduces the exact input as `state`
+
 * `state-circular-equations.execute`
   - starts from `concrete-subst`
   - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1`
   - leading to end state with `X == 42` from the `ensures`-clause
 * `state-symbolic-bottom-predicate.execute`
   - starts from `symbolic-subst`
   - with an equation that is instantly false: `X = 1 +Int X`
-  - leading to a vacuous state in `kore-rpc-booster` after rewriting once,
+  - leading to a vacuous state in `booster-dev` and `kore-rpc-booster`,
   - while `kore-rpc-dev` returns `stuck` instantly after 0 steps,
     returning the exact input as `state`.
diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
@@ -225,61 +225,13 @@
                                         }
                                     },
                                     {
-                                        "tag": "App",
-                                        "name": "Lbl'UndsPlus'Int'Unds'",
-                                        "sorts": [],
-                                        "args": [
-                                            {
-                                                "tag": "App",
-                                                "name": "Lbl'UndsPlus'Int'Unds'",
-                                                "sorts": [],
-                                                "args": [
-                                                    {
-                                                        "tag": "EVar",
-                                                        "name": "X",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        }
-                                                    },
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "1"
-                                                    }
-                                                ]
-                                            },
-                                            {
-                                                "tag": "App",
-                                                "name": "Lbl'Unds'-Int'Unds'",
-                                                "sorts": [],
-                                                "args": [
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "0"
-                                                    },
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortInt",
-                                                            "args": []
-                                                        },
-                                                        "value": "1"
-                                                    }
-                                                ]
-                                            }
-                                        ]
+                                        "tag": "EVar",
+                                        "name": "X",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortInt",
+                                            "args": []
+                                        }
                                     }
                                 ]
                             }

diff --git a/...er/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/...er/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev