Import the regression-new testsuite from K (runtimeverification/pyk#980)

This PR imports the entire `regression-new` test-suite from K.

- The directory `k-distribution/tests/regression-new` from the K
repository is copied to `regression-new`:
runtimeverification/pyk@e33cc1f
- The tests that use regular `ktest.mak` are adjusted to point at
`regression-new/include/ktest.mak` instead of the old path.
- The default backend to run these tests with is corrected to `llvm` in
`regression-new/include/ktest.mak`.
- All of the newly added tests are added to a skipped list
`regression-new/skipped`, so that they are not run on CI. The existing
tests `regression-new/kprove-haskell` from
runtimeverification/pyk#958 and
`regression-new/withConfig` from
runtimeverification/pyk#973 are left enabled.

---------

Co-authored-by: devops <devops@runtimeverification.com>

pyk/docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.705'
-release = '0.1.705'
+version = '0.1.706'
+release = '0.1.706'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyk/package/version

@@ -1 +1 @@
-0.1.705
+0.1.706

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.705"
+version = "0.1.706"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/regression-new/Makefile

@@ -1,2 +1,3 @@
-SUBDIRS=$(filter-out Makefile include, $(wildcard *))
+SKIPPED=$(shell cat skipped)
+SUBDIRS=$(filter-out Makefile include $(SKIPPED), $(wildcard *))
 include ./include/ktest-group.mak

pyk/regression-new/amb-rew/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=-w2e
+
+include ../include/ktest.mak

pyk/regression-new/amb-rew/test.k

@@ -0,0 +1,17 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST-SYNTAX
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  imports INT
+  imports MAP
+  imports ID
+
+syntax Type ::= "type"
+syntax Foo ::= foo(Map)
+
+rule foo(1 |-> 0 => 1 |-> #fun(T::Type => T |-> T)(type))
+
+
+endmodule

pyk/regression-new/append/1.test.kparse

@@ -0,0 +1 @@
+1

pyk/regression-new/append/1.test.kparse.out

@@ -0,0 +1 @@
+\dv{SortInt{}}("1")\dv{SortInt{}}("1")

pyk/regression-new/append/Makefile

@@ -0,0 +1,9 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../include/ktest.mak
+
+KPARSE=./kparse-twice

pyk/regression-new/append/kparse-twice

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+"$(dirname "$0")/../../../bin/kparse" "$@"
+"$(dirname "$0")/../../../bin/kparse" "$@"

pyk/regression-new/append/test.k

@@ -0,0 +1,15 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEAL-SYNTAX
+  imports INT-SYNTAX
+endmodule
+
+module TEST-SYNTAX
+  imports TEAL-SYNTAX
+endmodule
+
+module TEST
+  imports TEAL-SYNTAX
+
+  configuration
+      <k> $PGM:Int </k>
+endmodule

pyk/regression-new/array-haskell/1.test

@@ -0,0 +1 @@
+makeArray(0, 0) [ 0 ]

pyk/regression-new/array-haskell/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  0 ~> .K
+</k>

pyk/regression-new/array-haskell/2.test

@@ -0,0 +1 @@
+makeArray(0, 0) [ 1 ]

pyk/regression-new/array-haskell/2.test.out

@@ -0,0 +1,3 @@
+<k>
+  0 ~> .K
+</k>

pyk/regression-new/array-haskell/3.test

@@ -0,0 +1 @@
+makeArray(1, 0) [ 0 <- 1 ] [ 0 ]

pyk/regression-new/array-haskell/3.test.out

@@ -0,0 +1,3 @@
+<k>
+  1 ~> .K
+</k>

pyk/regression-new/array-haskell/4.test

@@ -0,0 +1 @@
+makeArray(1, 0) [ 0 <- 1] [ 1 ]

pyk/regression-new/array-haskell/4.test.out

@@ -0,0 +1,3 @@
+<k>
+  0 ~> .K
+</k>

pyk/regression-new/array-haskell/5.test

@@ -0,0 +1 @@
+makeArray(1, 0) [0 <- 1] [ -1 ]

pyk/regression-new/array-haskell/5.test.out

@@ -0,0 +1,3 @@
+<k>
+  0 ~> .K
+</k>

pyk/regression-new/array-haskell/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND?=haskell
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../include/ktest.mak

pyk/regression-new/array-haskell/test.k

@@ -0,0 +1,8 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST
+  imports DOMAINS
+  imports ARRAY
+
+configuration <k> $PGM:K </k>
+
+endmodule

pyk/regression-new/bad-bytes-literal/Makefile

@@ -0,0 +1,3 @@
+KOMPILE_FLAGS=-w none
+
+include ../../../include/kframework/ktest-fail.mak

pyk/regression-new/bad-bytes-literal/quote.k

@@ -0,0 +1,7 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module QUOTE
+    imports BYTES
+    configuration <k> $PGM:Bool </k>
+
+    rule <k> b""" => b"" </k>
+endmodule

pyk/regression-new/bad-bytes-literal/quote.k.out

@@ -0,0 +1,6 @@
+[Error] Inner Parser: Scanner error: unexpected character sequence '"'.
+	Source(quote.k)
+	Location(6,24,6,25)
+	6 |	    rule <k> b""" => b"" </k>
+	  .	                       ^
+[Error] Compiler: Had 1 parsing errors.

pyk/regression-new/bad-bytes-literal/slash.k

@@ -0,0 +1,7 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module SLASH
+    imports BYTES
+    configuration <k> $PGM:Bool </k>
+
+    rule <k> b"\" => b"" </k>
+endmodule

pyk/regression-new/bad-bytes-literal/slash.k.out

@@ -0,0 +1,6 @@
+[Error] Inner Parser: Scanner error: unexpected character sequence '"'.
+	Source(slash.k)
+	Location(6,24,6,25)
+	6 |	    rule <k> b"\" => b"" </k>
+	  .	                       ^
+[Error] Compiler: Had 1 parsing errors.

pyk/regression-new/bad-bytes-literal/unicode-escape.k

@@ -0,0 +1,7 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module UNICODE-ESCAPE
+    imports BYTES
+    configuration <k> $PGM:Bool </k>
+
+    rule <k> b"\u0012" => b"" </k>
+endmodule

pyk/regression-new/bad-bytes-literal/unicode-escape.k.out

@@ -0,0 +1,6 @@
+[Error] Inner Parser: Parse error: unexpected token '"\u0012"' following token 'b'.
+	Source(unicode-escape.k)
+	Location(6,15,6,23)
+	6 |	    rule <k> b"\u0012" => b"" </k>
+	  .	              ^~~~~~~~
+[Error] Compiler: Had 1 parsing errors.

pyk/regression-new/bad-bytes-literal/unicode.k

@@ -0,0 +1,7 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module UNICODE
+    imports BYTES
+    configuration <k> $PGM:Bool </k>
+
+    rule <k> b"\x😃" => b"" </k>
+endmodule

pyk/regression-new/bad-bytes-literal/unicode.k.out

@@ -0,0 +1,6 @@
+[Error] Inner Parser: Scanner error: unexpected character sequence '"'.
+	Source(unicode.k)
+	Location(6,15,6,16)
+	6 |	    rule <k> b"\x😃" => b"" </k>
+	  .	              ^
+[Error] Compiler: Had 1 parsing errors.

pyk/regression-new/bad-flags/Makefile

@@ -0,0 +1,16 @@
+DEF=test
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+CHECK=2>&1 | diff -
+ALLOW_FAIL=
+
+.PHONY: all clean update-results
+all:
+	$(KOMPILE) $(CHECK) no-flags.out $(ALLOW_FAIL)
+	$(KOMPILE) $(KOMPILE_FLAGS) --badflag --extra --backend $(KOMPILE_BACKEND) $(DEBUG) $(DEF).$(SOURCE_EXT) ---output-definition $(DEF)-kompiled $(CHECK) extra-flags.out $(ALLOW_FAIL)
+
+include ../include/ktest.mak
+
+update-results: CHECK=2>
+update-results: ALLOW_FAIL=; true

pyk/regression-new/bad-flags/extra-flags.out

@@ -0,0 +1 @@
+[Error] Critical: Only one main parameter allowed but found several: "--badflag" and "--extra"

pyk/regression-new/bad-flags/no-flags.out

@@ -0,0 +1,2 @@
+[Error] Critical: You have to provide exactly one main file in order to do
+outer parsing.

pyk/regression-new/bad-flags/test.k

@@ -0,0 +1,3 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST
+endmodule

pyk/regression-new/bison-glr-bug/Makefile

@@ -0,0 +1,17 @@
+DEF=iele
+EXT=
+TESTDIR=.
+KOMPILE_FLAGS+=--gen-glr-bison-parser
+
+test: test.kore
+	cat test.kore | diff - test.ref
+
+test.kore: forwarder.iele kompile
+	./iele-kompiled/parser_PGM forwarder.iele > test.kore
+include ../include/ktest.mak
+
+clean:
+	rm -rf test.kore $(KOMPILED_DIR) .depend-tmp .depend .kompile-* .krun-* .kprove-* kore-exec.tar.gz
+
+
+KRUN_OR_KX=./parse

pyk/regression-new/bison-glr-bug/forwarder.iele

@@ -0,0 +1,34 @@
+// Copyright (c) 2017 Runtime Verification, Inc. All Rights Reserved.
+//
+// This contract implements a forwarder that forwards any funds sent to
+// the account it is deployed with to the account that created it.
+contract Forwarder {
+
+  // initializes a forwarder by storing in the account storage the account
+  // number of the creator, this is the account to which received funds should
+  // be forwarded
+  define @init() {
+    %parent = call @iele.caller()
+    %zero = 0
+    sstore %parent, %zero
+  }
+
+  // deposit forwards the recieved funds to the creator of this account
+  define public @deposit() {
+    // get the received funds
+    %value = call @iele.callvalue()
+
+    // get the creator account, where we should forward funds, from the storage
+    %zero = 0
+    %sender = sload %zero
+
+    // forward funds by calling deposit at the creator account
+    %gas = call @iele.gas()
+    %status = call @deposit at %sender () send %value , gaslimit %gas
+    br %status, throw // contract call failed
+    ret void
+
+  throw:
+    call @iele.invalid()
+  }
+}