Kore Server: fix substitution result sort (#3386)

* Kore Server: fix substitution result sort

* update expected sort in implication check endpoint tests

* Add instructions to update golden files to README

Co-authored-by: Jost Berthold <[email protected]>

Author: ana-pantilie

kore/src/Kore/JsonRpc.hs

@@ -347,7 +347,7 @@ respond runSMT serializedModule =
                     { term =
                         PatternJson.fromTermLike $ Pattern.term p
                     , substitution =
-                        PatternJson.fromSubstitution $ Pattern.substitution p
+                        PatternJson.fromSubstitution sort $ Pattern.substitution p
                     , predicate =
                         case Pattern.predicate p of
                             PredicateTrue -> Nothing
@@ -395,7 +395,7 @@ respond runSMT serializedModule =
                     predicate =
                         PatternJson.fromPredicate sort $ Condition.predicate pat
                     mbSubstitution =
-                        PatternJson.fromSubstitution $ Condition.substitution pat
+                        PatternJson.fromSubstitution sort $ Condition.substitution pat
                     noSubstitution = PatternJson.fromTermLike $ TermLike.mkTop sort
                  in Condition
                         { predicate

kore/src/Kore/Syntax/Json.hs

@@ -116,8 +116,8 @@ becomes
 
 The result sort is fixed to a made-up sort variable.
 -}
-fromSubstitution :: Substitution VariableName -> Maybe KoreJson
-fromSubstitution subst
+fromSubstitution :: Kore.Sort -> Substitution VariableName -> Maybe KoreJson
+fromSubstitution sort subst
     | Substitution.null subst = Nothing
     | otherwise =
         Just
@@ -127,16 +127,11 @@ fromSubstitution subst
             . Substitution.unwrap
             $ subst
   where
-    freshSort =
-        Kore.SortVariableSort
-            . Kore.SortVariable
-            $ Kore.noLocationId "JSONSortVariable"
-
     equals ::
         Kore.SomeVariable VariableName ->
         TermLike VariableName ->
         TermLike VariableName
-    v `equals` t = TermLike.mkEquals freshSort (TermLike.mkVar v) t
+    v `equals` t = TermLike.mkEquals sort (TermLike.mkVar v) t
 
     asPair :: Assignment v -> (Kore.SomeVariable v, TermLike v)
     asPair (Substitution.Assignment v t) = (v, t)

test/rpc-server/README.md

@@ -1,8 +1,34 @@
 # JSON RPC Roundtrip tests
 
-This README provides a guide for adding more tests to this test suite.
+## Requirements
 
-To add a test, you wil need to create a new folder in one of `execute/`, `simplify/`, etc. folders, corresponding to the API methods.
+The tests in this directory are run using the python-3 script `runTests.py`.
+It requires the library `jsonrpcclient` (simply use `pip install jsonrpcclient` to get it).
+
+## Running tests
+
+Tests are run using 
+
+```
+python3 ./runTests.py
+``` 
+
+The command will stop at the first failure, highlighting the difference to the expected output in colour.
+
+## Updating the tests when the expected output changes
+
+When the expected JSON output of any tests is expected to change, you can 
+run the tests with `RECREATE_BROKEN_GOLDEN=true` to overwrite the golden response files
+
+```
+RECREATE_BROKEN_GOLDEN=true python3 ./runTests.py
+```
+
+While running, the script will report the differences in the output, but overwrite the old files and continue running. The idea is to inspect changes in the output, or using `git diff` after the run.
+
+## Adding more tests to this test suite
+
+To add a test, you will need to create a new folder in one of `execute/`, `simplify/`, etc. folders, corresponding to the API methods.
 Note that the folders for the API methods may not contain anything else but subfolders with tests.
 
 The new folder must contain input components according to the different endpoints:
@@ -13,7 +39,8 @@ The new folder must contain input components according to the different endpoint
 * For `implies`:
   - `antecedent.json` - a JSON Kore pattern file containing the antecedent term
   - `consequent.json` - a JSON Kore pattern file containing the consequent term
-
+* For `simplify`:
+  - `state.json` - a JSON Kore pattern file containing the state to simplify
 
 For all endpoints:
 * `definition.kore` - the definition file with a module `TEST` (this module name is hard coded for all tests)
@@ -53,7 +80,8 @@ kore-parser definition.kore --module TEST --pattern state.kore --print-pattern-j
 Finally, run the tests with `CREATE_MISSING_GOLDEN=true` to generate a golden response
 
 ```
-CREATE_MISSING_GOLDEN=true ./runTests.py
+CREATE_MISSING_GOLDEN=true python3 ./runTests.py
 ```
 
 Clean up the folder and commit the new test
+

test/rpc-server/implies/implied-substitution/response.golden

@@ -1 +1 @@
-{"jsonrpc":"2.0","id":1,"result":{"satisfiable":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortVar","name":"JSONSortVariable"},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}
+{"jsonrpc":"2.0","id":1,"result":{"satisfiable":true,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}

test/rpc-server/implies/not-implied-stuck/response.golden

@@ -1 +1 @@
-{"jsonrpc":"2.0","id":1,"result":{"satisfiable":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"And","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortVar","name":"JSONSortVariable"},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}
+{"jsonrpc":"2.0","id":1,"result":{"satisfiable":false,"implication":{"format":"KORE","version":1,"term":{"tag":"Implies","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Exists","sort":{"tag":"SortApp","name":"SortK","args":[]},"var":"Z","varSort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"And","sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"Not","sort":{"tag":"SortApp","name":"SortK","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}}},"condition":{"substitution":{"format":"KORE","version":1,"term":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortK","args":[]},"sort":{"tag":"SortApp","name":"SortK","args":[]},"first":{"tag":"EVar","name":"X","sort":{"tag":"SortApp","name":"SortK","args":[]}},"second":{"tag":"EVar","name":"Z","sort":{"tag":"SortApp","name":"SortK","args":[]}}}},"predicate":{"format":"KORE","version":1,"term":{"tag":"Top","sort":{"tag":"SortApp","name":"SortK","args":[]}}}}}}