!!! regression-new: update all expected output

runtimeverification · Mar 28, 2024 · e4e58e7 · e4e58e7
1 parent a71f988
commit e4e58e7
Show file tree

Hide file tree

Showing 281 changed files with 9,783 additions and 3,408 deletions.
diff --git a/regression-new/bad-flags/no-flags.out b/regression-new/bad-flags/no-flags.out
@@ -1,11 +1,15 @@
-usage: pyk kompile [-h] [--verbose] [--debug] [--warnings WARNINGS] [-w2e] [-I INCLUDES]
-                   [--main-module MAIN_MODULE] [--syntax-module SYNTAX_MODULE]
-                   [--md-selector MD_SELECTOR] [--output-definition DEFINITION_DIR] [--backend BACKEND]
-                   [--type-inference-mode TYPE_INFERENCE_MODE] [--emit-json] [-ccopt CCOPTS]
-                   [--no-llvm-kompile] [--with-llvm-library] [--enable-llvm-debug]
-                   [--llvm-kompile-type LLVM_KOMPILE_TYPE] [--llvm-kompile-output LLVM_KOMPILE_OUTPUT]
-                   [--read-only-kompiled-directory] [-O0] [-O1] [-O2] [-O3] [--enable-search]
-                   [--coverage] [--gen-bison-parser] [--gen-glr-bison-parser] [--bison-lists]
+usage: pyk kompile [-h] [--verbose] [--debug] [--warnings WARNINGS] [-w2e]
+                   [-I INCLUDES] [--main-module MAIN_MODULE]
+                   [--syntax-module SYNTAX_MODULE] [--md-selector MD_SELECTOR]
+                   [--output-definition DEFINITION_DIR] [--backend BACKEND]
+                   [--type-inference-mode TYPE_INFERENCE_MODE] [--emit-json]
+                   [-ccopt CCOPTS] [--no-llvm-kompile] [--with-llvm-library]
+                   [--enable-llvm-debug]
+                   [--llvm-kompile-type LLVM_KOMPILE_TYPE]
+                   [--llvm-kompile-output LLVM_KOMPILE_OUTPUT]
+                   [--read-only-kompiled-directory] [-O0] [-O1] [-O2] [-O3]
+                   [--enable-search] [--coverage] [--gen-bison-parser]
+                   [--gen-glr-bison-parser] [--bison-lists]
                    [--llvm-proof-hint-instrumentation] [--no-exc-wrap]
                    main_file
 pyk kompile: error: the following arguments are required: main_file
diff --git a/regression-new/cell-sort-haskell/1.test.out b/regression-new/cell-sort-haskell/1.test.out
@@ -1,35 +1,38 @@
-<T>
-  <k>
-    "done" ~> .K
-  </k>
-  <nextFunction>
-    3
-  </nextFunction>
-  <functions>
-    <function>
-      <fId>
-        0
-      </fId>
-    </function> <function>
-      <fId>
-        1
-      </fId>
-    </function> <function>
-      <fId>
-        2
-      </fId>
-    </function>
-  </functions>
-  <contracts>
-    <contract>
-      <cName>
-        foo ~> .K
-      </cName>
-      <cFunctions>
-        f1 |-> 0
-        f2 |-> 1
-        f3 |-> 2
-      </cFunctions>
-    </contract>
-  </contracts>
-</T>
+<generatedTop>
+  <T>
+    <k>
+      "done" ~> .K
+    </k>
+    <nextFunction>
+      3
+    </nextFunction>
+    <functions>
+      <function>
+        <fId>
+          0
+        </fId>
+      </function> <function>
+        <fId>
+          2
+        </fId>
+      </function> <function>
+        <fId>
+          1
+        </fId>
+      </function>
+    </functions>
+    <contracts>
+      <contract>
+        <cName>
+          foo ~> .K
+        </cName>
+        <cFunctions>
+          f1 |-> 0 f3 |-> 2 f2 |-> 1
+        </cFunctions>
+      </contract>
+    </contracts>
+  </T>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/regression-new/checkClaimError/rule-spec.k.out b/regression-new/checkClaimError/rule-spec.k.out
@@ -1,6 +1,33 @@
-[Error] Compiler: Only claims and simplification rules are allowed in proof modules.
+[Error] Compiler: Only claims and simplification rules are allowed in proof
+modules.
 	Source(rule-spec.k)
 	Location(6,10,6,43)
 	6 |	    rule <k> doIt(foo) => doIt(0) ... </k>
 	  .	         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 [Error] Compiler: Had 1 structural errors.
+Traceback (most recent call last):
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 105, in _kprove
+    return run_process(run_args, logger=_LOGGER, env=env, check=check)
+  File "/home/dev/src/pyk/src/pyk/utils.py", line 451, in run_process
+    res.check_returncode()
+  File "/usr/lib/python3.10/subprocess.py", line 457, in check_returncode
+    raise CalledProcessError(self.returncode, self.args, self.stdout,
+subprocess.CalledProcessError: Command '('kprove', 'rule-spec.k', '--definition', 'errorClaim-kompiled', '--output', 'json', '--type-inference-mode', 'checked', '--dry-run', '--emit-json-spec', '/tmp/tmppacrxgx1')' returned non-zero exit status 113.
+
+The above exception was the direct cause of the following exception:
+
+Traceback (most recent call last):
+  File "<string>", line 1, in <module>
+  File "/home/dev/src/pyk/src/pyk/__main__.py", line 90, in main
+    execute(options)
+  File "/home/dev/src/pyk/src/pyk/__main__.py", line 252, in exec_prove
+    proofs = kprove.prove_rpc(options=options)
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 380, in prove_rpc
+    all_claims = self.get_claims(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 425, in get_claims
+    flat_module_list = self.get_claim_modules(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 400, in get_claim_modules
+    _kprove(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 107, in _kprove
+    raise RuntimeError(
+RuntimeError: ('Command kprove exited with code 113 for: rule-spec.k', '', None)
diff --git a/regression-new/checkClaimError/syntax-spec.k.out b/regression-new/checkClaimError/syntax-spec.k.out
@@ -1,11 +1,39 @@
-[Error] Compiler: Found syntax declaration in proof module. Only tokens for existing sorts are allowed.
+[Error] Compiler: Found syntax declaration in proof module. Only tokens for
+existing sorts are allowed.
 	Source(syntax-spec.k)
 	Location(6,18,6,29)
 	6 |	    syntax X ::= "errorHere"
 	  .	                 ^~~~~~~~~~~
-[Error] Compiler: Found syntax declaration in proof module. Only tokens for existing sorts are allowed.
+[Error] Compiler: Found syntax declaration in proof module. Only tokens for
+existing sorts are allowed.
 	Source(syntax-spec.k)
 	Location(7,5,7,13)
 	7 |	    syntax Y
 	  .	    ^~~~~~~~
 [Error] Compiler: Had 2 structural errors.
+Traceback (most recent call last):
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 105, in _kprove
+    return run_process(run_args, logger=_LOGGER, env=env, check=check)
+  File "/home/dev/src/pyk/src/pyk/utils.py", line 451, in run_process
+    res.check_returncode()
+  File "/usr/lib/python3.10/subprocess.py", line 457, in check_returncode
+    raise CalledProcessError(self.returncode, self.args, self.stdout,
+subprocess.CalledProcessError: Command '('kprove', 'syntax-spec.k', '--definition', 'errorClaim-kompiled', '--output', 'json', '--type-inference-mode', 'checked', '--dry-run', '--emit-json-spec', '/tmp/tmp2z_mabgd')' returned non-zero exit status 113.
+
+The above exception was the direct cause of the following exception:
+
+Traceback (most recent call last):
+  File "<string>", line 1, in <module>
+  File "/home/dev/src/pyk/src/pyk/__main__.py", line 90, in main
+    execute(options)
+  File "/home/dev/src/pyk/src/pyk/__main__.py", line 252, in exec_prove
+    proofs = kprove.prove_rpc(options=options)
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 380, in prove_rpc
+    all_claims = self.get_claims(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 425, in get_claims
+    flat_module_list = self.get_claim_modules(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 400, in get_claim_modules
+    _kprove(
+  File "/home/dev/src/pyk/src/pyk/ktool/kprove.py", line 107, in _kprove
+    raise RuntimeError(
+RuntimeError: ('Command kprove exited with code 113 for: syntax-spec.k', '', None)
diff --git a/regression-new/checks/checkCircularList.k.out b/regression-new/checks/checkCircularList.k.out
@@ -1,4 +1,4 @@
 [Error] Compiler: Had 1 parsing errors.
-[Error] Compiler: Illegal circular relation: Exp < ExpList < Exp
+[Error] Compiler: Illegal circular relation: ExpList < Exp < ExpList
 [ERROR] Running process failed with returncode 113:
     kompile checkCircularList.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition checkCircularList-kompiled --type-inference-mode checked
diff --git a/regression-new/checks/existentialCheck.k.out b/regression-new/checks/existentialCheck.k.out
@@ -1,8 +1,8 @@
 [Error] Compiler: Claims are not allowed in the definition.
 	Source(existentialCheck.k)
-	Location(15,9,15,29)
+	Location(15,9,15,30)
 	15 |	  claim <k> ?X:Int => .K </k>
-	   .	        ^~~~~~~~~~~~~~~~~~~~
+	   .	        ^~~~~~~~~~~~~~~~~~~~~
 [Error] Compiler: Existential variable ?X found in LHS. Existential variables are only allowed in the RHS.
 	Source(existentialCheck.k)
 	Location(15,13,15,15)

diff --git a/regression-new/checks/macroWithFunction.k.out b/regression-new/checks/macroWithFunction.k.out
@@ -6,6 +6,6 @@
 [Error] Compiler: Had 1 structural errors after macro expansion.
   while executing phase "expand macros" on sentence at
 	Source(macroWithFunction.k)
-	Location(23,10,23,37)
+	Location(23,10,23,38)
 [ERROR] Running process failed with returncode 113:
     kompile macroWithFunction.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition macroWithFunction-kompiled --type-inference-mode checked
diff --git a/regression-new/checks/priorityError.k.out b/regression-new/checks/priorityError.k.out
@@ -1,22 +1,22 @@
 [Error] Inner Parser: Priority filter exception. Cannot use lguard as an immediate child of plus. Consider using parentheses around lguard
 	Source(priorityError.k)
-	Location(21,19,21,22)
+	Location(21,20,21,23)
 	21 |	    rule .K => 1 + l 2 // unable to disambiguate - error
-	   .	                  ^~~
+	   .	                   ^~~
 [Error] Inner Parser: Priority filter exception. Cannot use rguard as an immediate child of plus. Consider using parentheses around rguard
 	Source(priorityError.k)
-	Location(22,15,22,18)
+	Location(22,16,22,19)
 	22 |	    rule .K => 1 r + 2 // unable to disambiguate - error
-	   .	              ^~~
+	   .	               ^~~
 [Error] Inner Parser: Parsing ambiguity.
 1: syntax Exp ::= "l" Exp [klabel(lguard), symbol]
     lguard(rguard(#token("1","Int")))
 2: syntax Exp ::= Exp "r" [klabel(rguard), symbol]
     rguard(lguard(#token("1","Int")))
 	Source(priorityError.k)
-	Location(23,15,23,20)
+	Location(23,16,23,21)
 	23 |	    rule .K => l 1 r   // ambiguous - error
-	   .	              ^~~~~
+	   .	               ^~~~~
 [Error] Compiler: Had 3 parsing errors.
 [ERROR] Running process failed with returncode 113:
     kompile priorityError.k --md-selector k --emit-json --warnings none --no-exc-wrap --backend llvm --output-definition priorityError-kompiled --type-inference-mode checked
diff --git a/regression-new/concrete-function-cache/a2-spec.k.out b/regression-new/concrete-function-cache/a2-spec.k.out
@@ -1,24 +1,27 @@
-kore-exec: [] Warning (WarnStuckClaimState):
-    The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: a2-spec.k:7:1-8:18
-Context:
-    (InfoReachability) while checking the implication
-  #Ceil ( bar ( X ) )
-#And
-  #Not ( #Ceil ( baz ( X ) )
-  #And
-    {
-      bar ( X )
-    #Equals
-      baz ( X )
-    } )
-#And
-  <k>
-    end ( bar ( X ) ) ~> .K
-  </k>
-#And
-  {
-    true
-  #Equals
-    X <Int 0
-  }
-[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
+APRProof: A2-SPEC.s2
+    status: ProofStatus.FAILED
+    admitted: False
+    nodes: 5
+    pending: 0
+    failing: 1
+    vacuous: 0
+    stuck: 1
+    terminal: 0
+    refuted: 0
+    bounded: 0
+    execution time: 0s
+Subproofs: 0
+1 Failure nodes. (0 pending and 1 failing)
+
+Failing nodes:
+
+  Node id: 5
+  Failure reason:
+    Matching failed.
+    The following cells failed matching individually (antecedent #Implies consequent):
+    K_CELL: end ( bar ( X:Int ) ) #Implies end ( baz ( X:Int ) )
+  Path condition:
+    #Ceil ( bar ( X:Int ) )
+  Failed to generate a model.
+
+Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN
diff --git a/regression-new/concrete-function/a1-spec.k.out b/regression-new/concrete-function/a1-spec.k.out
@@ -1,24 +1,27 @@
-kore-exec: [] Warning (WarnStuckClaimState):
-    The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: a1-spec.k:7:1-8:18
-Context:
-    (InfoReachability) while checking the implication
-  #Ceil ( barConcrete ( X ) )
-#And
-  #Not ( #Ceil ( baz ( X ) )
-  #And
-    {
-      barConcrete ( X )
-    #Equals
-      baz ( X )
-    } )
-#And
-  <k>
-    end ( barConcrete ( X ) ) ~> .K
-  </k>
-#And
-  {
-    true
-  #Equals
-    X >Int 0
-  }
-[Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
+APRProof: A1-SPEC.s1
+    status: ProofStatus.FAILED
+    admitted: False
+    nodes: 5
+    pending: 0
+    failing: 1
+    vacuous: 0
+    stuck: 1
+    terminal: 0
+    refuted: 0
+    bounded: 0
+    execution time: 0s
+Subproofs: 0
+1 Failure nodes. (0 pending and 1 failing)
+
+Failing nodes:
+
+  Node id: 5
+  Failure reason:
+    Matching failed.
+    The following cells failed matching individually (antecedent #Implies consequent):
+    K_CELL: end ( barConcrete ( X:Int ) ) #Implies end ( baz ( X:Int ) )
+  Path condition:
+    #Ceil ( barConcrete ( X:Int ) )
+  Failed to generate a model.
+
+Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN
diff --git a/regression-new/concrete-haskell/a1-spec.k.out b/regression-new/concrete-haskell/a1-spec.k.out
@@ -1 +1,27 @@
-#Top
+APRProof: A1-SPEC.s1
+    status: ProofStatus.FAILED
+    admitted: False
+    nodes: 3
+    pending: 0
+    failing: 1
+    vacuous: 0
+    stuck: 1
+    terminal: 0
+    refuted: 0
+    bounded: 0
+    execution time: 0s
+Subproofs: 0
+1 Failure nodes. (0 pending and 1 failing)
+
+Failing nodes:
+
+  Node id: 3
+  Failure reason:
+    Matching failed.
+    The following cells failed matching individually (antecedent #Implies consequent):
+    COUNTER_CELL: final ( n +Int 5 ) #Implies 0
+  Path condition:
+    #Top
+  Failed to generate a model.
+
+Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN