Merge remote-tracking branch 'origin/develop'

k-distribution/include/kframework/builtin/domains.md

@@ -1201,7 +1201,7 @@ endmodule
 
 module INT-SYNTAX
   imports UNSIGNED-INT-SYNTAX
-  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)]
+  syntax Int ::= r"[\\+\\-]?[0-9]+" [prefer, token, prec(2)]
 endmodule
 
 module INT-COMMON
@@ -1477,8 +1477,8 @@ is equal to the IEEE `binary32` format, and `p53x11` is equal to the IEEE
 ```k
 module FLOAT-SYNTAX
   syntax Float [hook(FLOAT.Float)]
-  syntax Float ::= r"([\\+-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+-]?[0-9]+)?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(1)]
-  syntax Float ::= r"[\\+-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(3)]
+  syntax Float ::= r"([\\+\\-]?[0-9]+(\\.[0-9]*)?|\\.[0-9]+)([eE][\\+\\-]?[0-9]+)?([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(1)]
+  syntax Float ::= r"[\\+\\-]?Infinity([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(3)]
   syntax Float ::= r"NaN([fFdD]|([pP][0-9]+[xX][0-9]+))?" [token, prec(3)]
 endmodule
 
@@ -1984,7 +1984,7 @@ module BYTES-SYNTAX
   imports private STRING-SYNTAX
 
   syntax Bytes [hook(BYTES.Bytes)]
-  syntax Bytes ::= r"b[\\\"](([\\x20\\x21\\x23-\\x5B\\x5D-\\x7E])|([\\\\][tnfr\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2}))*[\\\"]"      [token]
+  syntax Bytes ::= r"b[\\\"](([ !#-\\[\\]-~])|([\\\\][tnfr\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2}))*[\\\"]"      [token]
 endmodule
 ```
 
@@ -2849,7 +2849,7 @@ module MINT-SYNTAX
   syntax {Width} MInt{Width} [hook(MINT.MInt)]
 
   /*@ Machine integer of bit width and value. */
-  syntax {Width} MInt{Width} ::= r"[\\+-]?[0-9]+[pP][0-9]+" [token, prec(2), hook(MINT.literal)]
+  syntax {Width} MInt{Width} ::= r"[\\+\\-]?[0-9]+[pP][0-9]+" [token, prec(2), hook(MINT.literal)]
 endmodule
 
 module MINT

k-distribution/include/kframework/ktest-common.mak

@@ -0,0 +1,31 @@
+SHELL=/bin/bash
+# path to the current makefile
+MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
+# path to builtin include directory
+BUILTIN_DIR=$(abspath $(MAKEFILE_PATH)/../../target/release/k/include/kframework/builtin)
+# path to binary directory of this distribution
+K_BIN=$(abspath $(MAKEFILE_PATH)/../../bin)
+# path to the kompile binary of this distribuition
+KOMPILE=${K_BIN}/kompile
+# and krun
+KRUN=${K_BIN}/krun
+# and kdep
+KDEP=${K_BIN}/kdep
+# and kprove
+KPROVE=${K_BIN}/kprove
+# and kast
+KAST=${K_BIN}/kast
+# and kparse
+KPARSE=${K_BIN}/kparse
+# and kserver
+KSERVER=${K_BIN}/kserver
+# and ksearch
+KSEARCH:=$(KRUN) --search-all
+# and kprint
+KPRINT=${K_BIN}/kprint
+# and llvm-krun
+LLVM_KRUN=${K_BIN}/llvm-krun
+# and kdep
+KDEP=${K_BIN}/kdep
+# command to strip paths from test outputs
+REMOVE_PATHS=| sed 's!\('`pwd`'\|'${BUILTIN_DIR}'\|/nix/store/.\+/include/kframework/builtin\)/\(\./\)\{0,2\}!!g'

k-distribution/include/kframework/ktest-fail.mak

@@ -1,11 +1,6 @@
-# path to the current makefile
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
-# path to the kompile binary of this distribuition
-K_BIN=$(abspath $(MAKEFILE_PATH)/../../bin)
-KOMPILE=${K_BIN}/kompile
-KAST=${K_BIN}/kast
-# and kdep
-KDEP=${K_BIN}/kdep
+include $(MAKEFILE_PATH)/ktest-common.mak
+
 # path to put -kompiled directory in
 DEFDIR?=.
 # all tests in test directory with matching file extension
@@ -33,10 +28,10 @@ kast: $(KAST_TESTS)
 dummy:
 
 %.k %.md: dummy
-	$(KOMPILE) $(KOMPILE_FLAGS) --backend $(KOMPILE_BACKEND) $(DEBUG_FAIL) $@ --output-definition $(DEFDIR)/$(basename $@)-kompiled 2>&1 | sed 's!'`pwd`'/\(\./\)\{0,2\}!!g' $(CHECK) $@.out $(CHECK2)
+	$(KOMPILE) $(KOMPILE_FLAGS) --backend $(KOMPILE_BACKEND) $(DEBUG_FAIL) $@ --output-definition $(DEFDIR)/$(basename $@)-kompiled 2>&1 $(REMOVE_PATHS) $(CHECK) $@.out $(CHECK2)
 
 %.kast: kompile
-	$(KAST) $@ $(KAST_FLAGS) $(DEBUG) 2>&1 | sed 's!'`pwd`'/\(\./\)\{0,2\}!!g' $(CHECK) $@.out
+	$(KAST) $@ $(KAST_FLAGS) $(DEBUG) 2>&1 $(REMOVE_PATHS) $(CHECK) $@.out
 
 # run all tests and regenerate output files
 update-results: kompile kast

k-distribution/include/kframework/ktest-kdep.mak

@@ -1,10 +1,6 @@
-SHELL=/bin/bash
-
-# path to the current makefile
 MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
-# path to the kdep binary of this distribuition
-K_BIN=$(abspath $(MAKEFILE_PATH)/../../bin)
-KDEP=${K_BIN}/kdep
+include $(MAKEFILE_PATH)/ktest-common.mak
+
 # all tests in test directory with matching file extension
 TESTS?=$(wildcard ./*.md) $(wildcard ./*.k)
 
@@ -18,7 +14,7 @@ all: $(TESTS)
 dummy:
 
 %.k %.md: dummy
-	$(PIPEFAIL) $(KDEP) $(KDEP_FLAGS) $@ | sed 's!'`pwd`'/\(\./\)\{0,2\}!!g' $(CHECK) $@.out
+	$(PIPEFAIL) $(KDEP) $(KDEP_FLAGS) $@ $(REMOVE_PATHS) $(CHECK) $@.out
 
 # run all tests and regenerate output files
 update-results: all

k-distribution/include/kframework/ktest.mak

@@ -1,31 +1,8 @@
-SHELL=/bin/bash
+MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
+include $(MAKEFILE_PATH)/ktest-common.mak
 
 UNAME := $(shell uname)
 
-# path to the current makefile
-MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
-# path to binary directory of this distribution
-K_BIN=$(abspath $(MAKEFILE_PATH)/../../bin)
-# path to the kompile binary of this distribuition
-KOMPILE=${K_BIN}/kompile
-# ditto for krun
-KRUN=${K_BIN}/krun
-# and kdep
-KDEP=${K_BIN}/kdep
-# and kprove
-KPROVE=${K_BIN}/kprove
-# and kast
-KAST=${K_BIN}/kast
-# and kparse
-KPARSE=${K_BIN}/kparse
-# and kserver
-KSERVER=${K_BIN}/kserver
-# and ksearch
-KSEARCH:=$(KRUN) --search-all
-# and kprint
-KPRINT=${K_BIN}/kprint
-# and llvm-krun
-LLVM_KRUN=${K_BIN}/llvm-krun
 # path relative to current definition of test programs
 TESTDIR?=tests
 # path to put -kompiled directory in
@@ -58,7 +35,6 @@ KRUN_FLAGS+=--no-exc-wrap
 KRUN_OR_LEGACY=$(KRUN)
 
 CHECK?=| diff -
-REMOVE_PATHS=| sed 's!'`pwd`'/\(\./\)\{0,2\}!!g'
 CONSIDER_ERRORS=2>&1
 
 PIPEFAIL?=set -o pipefail;

k-distribution/k-tutorial/1_basic/03_parsing/README.md

@@ -284,7 +284,7 @@ For example, the builtin integers in K are defined using the following
 production:
 
 ```{.k .exclude}
-syntax Int ::= r"[\\+-]?[0-9]+" [token]
+syntax Int ::= r"[\\+\\-]?[0-9]+" [token]
 ```
 
 Here we can see that we have defined that an integer is an optional sign

k-distribution/tests/profiling/avm-semantics/test.k

@@ -793,7 +793,7 @@ module TEAL-PARSER-SYNTAX
   syntax lexical Alpha = r"[a-zA-Z]"
   syntax lexical Alnum = r"{Alpha}|{Digit}"
   syntax lexical AlnumUbar = r"{Alnum}|_"
-  syntax lexical Special = r"[-!?+<>=/*]"
+  syntax lexical Special = r"[\\-!?+<>=/*]"
   syntax HexToken  ::=
     r"0x{HexDigit}+" [prec(2), token]
   syntax TAddressLiteral  ::=

k-distribution/tests/profiling/elrond-semantics/test.k

@@ -1470,10 +1470,10 @@ module WASM-TOKEN-SYNTAX
   syntax WasmStringToken  ::=
     r"\\\"(([^\\\"\\\\])|(\\\\[0-9a-fA-F]{2})|(\\\\t)|(\\\\n)|(\\\\r)|(\\\\\\\")|(\\\\')|(\\\\\\\\)|(\\\\u\\{[0-9a-fA-F]{1,6}\\}))*\\\"" [token]
   syntax IdentifierToken  ::=
-    r"\\$[0-9a-zA-Z!$%&'*+/<>?_`|~=:\\@^.-]+" [token]
+    r"\\$[0-9a-zA-Z!$%&'*+/<>?_`|~=:\\@\\^.\\-]+" [token]
   syntax WasmIntToken  ::=
-    r"[\\+-]?[0-9]+(_[0-9]+)*" [token]
-  | r"[\\+-]?0x[0-9a-fA-F]+(_[0-9a-fA-F]+)*" [token]
+    r"[\\+\\-]?[0-9]+(_[0-9]+)*" [token]
+  | r"[\\+\\-]?0x[0-9a-fA-F]+(_[0-9a-fA-F]+)*" [token]
   syntax #Layout  ::=
     r"\\(;([^;]|(;+([^;\\)])))*;\\)" [token]
   | r";;[^\\n\\r]*" [token]

k-distribution/tests/profiling/wasm-semantics/test.k

@@ -1470,10 +1470,10 @@ module WASM-TOKEN-SYNTAX
   syntax WasmStringToken  ::=
     r"\\\"(([^\\\"\\\\])|(\\\\[0-9a-fA-F]{2})|(\\\\t)|(\\\\n)|(\\\\r)|(\\\\\\\")|(\\\\')|(\\\\\\\\)|(\\\\u\\{[0-9a-fA-F]{1,6}\\}))*\\\"" [token]
   syntax IdentifierToken  ::=
-    r"\\$[0-9a-zA-Z!$%&'*+/<>?_`|~=:\\@^.-]+" [token]
+    r"\\$[0-9a-zA-Z!$%&'*+/<>?_`|~=:\\@\\^.\\-]+" [token]
   syntax WasmIntToken  ::=
-    r"[\\+-]?[0-9]+(_[0-9]+)*" [token]
-  | r"[\\+-]?0x[0-9a-fA-F]+(_[0-9a-fA-F]+)*" [token]
+    r"[\\+\\-]?[0-9]+(_[0-9]+)*" [token]
+  | r"[\\+\\-]?0x[0-9a-fA-F]+(_[0-9a-fA-F]+)*" [token]
   syntax #Layout  ::=
     r"\\(;([^;]|(;+([^;\\)])))*;\\)" [token]
   | r";;[^\\n\\r]*" [token]

k-distribution/tests/regression-new/checks/checkGroup.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module CHECKGROUP
-  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2)]
+  syntax Int ::= r"[\\+\\-]?[0-9]+" [prefer, token, prec(2)]
                | Int "+" Int [group(fun,)]
 endmodule

k-distribution/tests/regression-new/checks/checkMIntLiteral.k.out

@@ -1,4 +1,4 @@
-[Error] Inner Parser: Unexpected sort MInt{32} for term parsed as production syntax MInt{32} ::= r"[\\+-]?[0-9]+[pP][0-9]+" [hook(MINT.literal), prec(2), token]. Expected: MInt{6}
+[Error] Inner Parser: Unexpected sort MInt{32} for term parsed as production syntax MInt{32} ::= r"[+\\-]?[0-9]+[pP][0-9]+" [hook(MINT.literal), prec(2), token]. Expected: MInt{6}
 	Source(checkMIntLiteral.k)
 	Location(14,12,14,16)
 	14 |	  rule foo(0p32) => 0

k-distribution/tests/regression-new/checks/invalidPrec.k.out

@@ -1,5 +1,5 @@
 [Error] Compiler: Inconsistent token precedence detected.
-	Source(invalidPrec.k)
-	Location(4,17,4,34)
-	4 |	 syntax Foo ::= r"[0-9]+" [token]
-	  .	                ^~~~~~~~~~~~~~~~~
+	Source(domains.md)
+	Location(1199,18,1199,52)
+	1199 |	  syntax Int ::= r"[0-9]+" [prefer, token, prec(2)]
+	     .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

k-distribution/tests/regression-new/issue-1633/lexical.k

@@ -36,7 +36,7 @@ module LEXICAL-SYNTAX
   syntax lexical HexFloatConstant = r"{HexPrefix}({HexFractionalConstant}|{HexDigitSeq}){BinaryExponentPart}({FloatSuffix}?)"
   syntax lexical FractionalConstant = r"({DigitSeq}?)[.]{DigitSeq}|{DigitSeq}[.]"
   syntax lexical ExponentPart = r"[eE]({Sign}?){DigitSeq}"
-  syntax lexical Sign = r"[+-]"
+  syntax lexical Sign = r"[+\\-]"
   syntax lexical DigitSeq = r"{Digit}+"
   syntax lexical HexFractionalConstant = r"({HexDigitSeq}?)[.]{HexDigitSeq}|{HexDigitSeq}[.]"
   syntax lexical BinaryExponentPart = r"[pP]({Sign}?){DigitSeq}"

k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out

@@ -1,15 +1,15 @@
 |"Match"                                                                          | (location)    | Terminal            |
 |---------------------------------------------------------------------------------|---------------|---------------------|
-|"1"                                                                              | (1,1,1,2)     | r"[\\+-]?[0-9]+"    |
+|"1"                                                                              | (1,1,1,2)     | r"[0-9]+"           |
 |"+"                                                                              | (1,3,1,4)     | "+"                 |
-|"2"                                                                              | (1,5,1,6)     | r"[\\+-]?[0-9]+"    |
+|"2"                                                                              | (1,5,1,6)     | r"[0-9]+"           |
 |"+"                                                                              | (1,7,1,8)     | "+"                 |
 |"aaaaaaaaaaaa"                                                                   | (1,9,1,21)    | r"[a-z][a-zA-Z0-9]*"|
 |"+"                                                                              | (12,1,12,2)   | "+"                 |
-|"10000000"                                                                       | (12,3,12,11)  | r"[\\+-]?[0-9]+"    |
+|"10000000"                                                                       | (12,3,12,11)  | r"[0-9]+"           |
 |"+"                                                                              | (13,1,13,2)   | "+"                 |
-|"\"str\""                                                                        | (13,3,13,8)   | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"|
+|"\"str\""                                                                        | (13,3,13,8)   | r"[\"]([^\"\\n\\r\\\\]|([\\\\][nrtf\"\\\\]|([\\\\][x][0-9a-fA-F]{2}|([\\\\][u][0-9a-fA-F]{4}|[\\\\][U][0-9a-fA-F]{8}))))*[\"]"|
 |"+"                                                                              | (14,1,14,2)   | "+"                 |
-|"\"long str that breaks                                                                    alighnment\"" | (14,3,14,103) | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"|
+|"\"long str that breaks                                                                    alighnment\"" | (14,3,14,103) | r"[\"]([^\"\\n\\r\\\\]|([\\\\][nrtf\"\\\\]|([\\\\][x][0-9a-fA-F]{2}|([\\\\][u][0-9a-fA-F]{4}|[\\\\][U][0-9a-fA-F]{8}))))*[\"]"|
 |""                                                                               | (15,1,15,1)   | "<eof>"             |
 

k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out

@@ -1,8 +1,8 @@
 |"Match" | (location) | Terminal            |
 |--------|------------|---------------------|
-|"1"     | (1,1,1,2)  | r"[\\+-]?[0-9]+"    |
+|"1"     | (1,1,1,2)  | r"[0-9]+"           |
 |"+"     | (1,3,1,4)  | "+"                 |
-|"2"     | (1,5,1,6)  | r"[\\+-]?[0-9]+"    |
+|"2"     | (1,5,1,6)  | r"[0-9]+"           |
 |"+"     | (1,7,1,8)  | "+"                 |
 |"aaa"   | (1,9,1,12) | r"[a-z][a-zA-Z0-9]*"|
 |""      | (2,1,2,1)  | "<eof>"             |

k-distribution/tests/regression-new/pedanticAttributes/test.k

@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEST
-  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
+  syntax Int ::= r"[\\+\\-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
                | Int "+" Int [group(badAttButOkay),badAtt,function]
 endmodule

k-distribution/tests/regression-new/pedanticAttributes/test.k.out

@@ -1,8 +1,8 @@
 [Error] Compiler: Unrecognized attributes: [badAtt]
 	Source(test.k)
-	Location(3,18,3,71)
-	3 |	  syntax Int ::= r"[\\+-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
-	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+	Location(3,18,3,73)
+	3 |	  syntax Int ::= r"[\\+\\-]?[0-9]+" [prefer, token, prec(2), badAtt(10)]
+	  .	                 ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 [Error] Compiler: Unrecognized attributes: [badAtt]
 	Source(test.k)
 	Location(4,18,4,68)

k-frontend/src/main/java/org/kframework/definition/regex/Regex.java

@@ -0,0 +1,10 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+package org.kframework.definition.regex;
+
+import java.io.Serializable;
+
+public record Regex(boolean startLine, RegexBody reg, boolean endLine) implements Serializable {
+  public Regex(RegexBody reg) {
+    this(false, reg, false);
+  }
+}

k-frontend/src/main/java/org/kframework/definition/regex/RegexBody.java

@@ -0,0 +1,37 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+package org.kframework.definition.regex;
+
+import java.io.Serializable;
+import java.util.List;
+
+public sealed interface RegexBody extends Serializable {
+  record Char(int codePoint) implements RegexBody {}
+
+  record AnyChar() implements RegexBody {}
+
+  record Named(String name) implements RegexBody {}
+
+  record CharClassExp(boolean negated, List<CharClass> charClasses) implements RegexBody {}
+
+  sealed interface CharClass extends Serializable {
+    record Char(int codePoint) implements CharClass {}
+
+    record Range(CharClass.Char start, CharClass.Char end) implements CharClass {}
+  }
+
+  record Union(RegexBody left, RegexBody right) implements RegexBody {}
+
+  record Concat(List<RegexBody> members) implements RegexBody {}
+
+  record ZeroOrMoreTimes(RegexBody reg) implements RegexBody {}
+
+  record ZeroOrOneTimes(RegexBody reg) implements RegexBody {}
+
+  record OneOrMoreTimes(RegexBody reg) implements RegexBody {}
+
+  record ExactlyTimes(RegexBody reg, int exactly) implements RegexBody {}
+
+  record AtLeastTimes(RegexBody reg, int atLeast) implements RegexBody {}
+
+  record RangeOfTimes(RegexBody reg, int atLeast, int atMost) implements RegexBody {}
+}