Merge branch 'develop' into georgy/pyk-prove-add-missing-options

.github/workflows/update-deps.yml

@@ -4,7 +4,6 @@ on:
     branches:
       - '_update-deps/runtimeverification/llvm-backend'
       - '_update-deps/runtimeverification/haskell-backend'
-      - 'booster-532-depend-on-single-hs-backend-repo' # FIXME remove this line
   workflow_dispatch:
 # Stop in progress workflows on the same branch and same workflow to use latest committed code
 concurrency:
@@ -56,9 +55,17 @@ jobs:
             changed=true
           fi
 
+          llvm_backend_version="v$(cat deps/llvm-backend_release)"
+          cd llvm-backend/src/main/native/llvm-backend
+          git checkout ${llvm_backend_version}
+          cd -
+          sed -i 's!      url = "github:runtimeverification/llvm-backend/.*";!      url = "github:runtimeverification/llvm-backend/'"${llvm_backend_version}"'";!' flake.nix
+          if git add flake.nix llvm-backend/src/main/native/llvm-backend && git commit -m "flake.nix, llvm-backend/src/main/native/llvm-backend: update to version ${llvm_backend_version}"; then
+            changed=true
+          fi
+
           nix flake update
-          GC_DONT_GC=1 nix run .#update-from-submodules
-          if git add flake.nix flake.lock && git commit -m 'flake.nix, flake.lock: update'; then
+          if git add flake.lock && git commit -m 'flake.lock: update'; then
             changed=true
           fi
 

deps/llvm-backend_release

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

flake.nix

@@ -5,7 +5,7 @@
     nixpkgs.follows = "llvm-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
     llvm-backend = {
-      url = "github:runtimeverification/llvm-backend";
+      url = "github:runtimeverification/llvm-backend/v0.1.3";
       inputs.utils.follows = "flake-utils";
     };
     rv-utils.url = "github:runtimeverification/rv-nix-tools";
@@ -135,12 +135,6 @@
             inherit llvm-backend haskell-backend;
           };
 
-          update-from-submodules =
-            rv-utils.lib.update-from-submodules pkgs ./flake.lock {
-              llvm-backend.submodule =
-                "llvm-backend/src/main/native/llvm-backend";
-            };
-
           smoke-test = with pkgs;
             stdenv.mkDerivation {
               name = "k-${k-version}-${self.rev or "dirty"}-smoke-test";

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java

@@ -14,6 +14,7 @@
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.Tool;
+import org.kframework.utils.OS;
 import org.kframework.utils.Stopwatch;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.errorsystem.KExceptionManager;
@@ -50,7 +51,7 @@ public void accept(Backend.Holder h) {
     sw.printIntermediate("  Print definition.kore");
     ProcessBuilder pb = files.getProcessBuilder();
     List<String> args = new ArrayList<>();
-    if (haskellKompileOptions.noHaskellBinary) {
+    if (haskellKompileOptions.noHaskellBinary || OS.current().equals(OS.OSX)) {
       args.add("kore-parser");
       args.add("--no-print-definition");
       args.add("definition.kore");

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java

@@ -22,7 +22,7 @@ public HaskellKompileOptions() {}
       names = "--no-haskell-binary",
       description =
           "Use the textual KORE format in the haskell backend instead of the binary KORE format."
-              + " This is a development option, but may be necessary on MacOS due to known issues"
-              + " with the binary format.")
+              + " This flag is disabled by default, except when running on macOS, where it is enabled and cannot be disabled because of a bug in the underlying Haskell libraries.",
+      hidden = true)
   public boolean noHaskellBinary = false;
 }

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

@@ -2240,7 +2240,7 @@ Provided are the following pieces of functionality:
 ```k
 module ID-SYNTAX-PROGRAM-PARSING
   imports BUILTIN-ID-TOKENS
-  syntax Id ::= r"(?<![A-Za-z0-9\\_])[A-Za-z\\_][A-Za-z0-9\\_]*"     [prec(1), token]
+  syntax Id ::= r"[A-Za-z\\_][A-Za-z0-9\\_]*"     [prec(1), token]
               | #LowerId                                             [token]
               | #UpperId                                             [token]
 endmodule

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

@@ -83,8 +83,7 @@ module KAST
 
   syntax KLabel ::= r"`(\\\\`|\\\\\\\\|[^`\\\\\\n\\r])+`" [token]
                   | #LowerId                                   [token]
-                  | r"(?<![a-zA-Z0-9])[#a-z][a-zA-Z0-9]*"               [token, prec(1)]
-                       // something that doesn't collide with meta-variables
+                  | r"[#a-z][a-zA-Z0-9]*"               [token, prec(1)]
 
   syntax KList ::= K
                  | ".KList"          [klabel(#EmptyKList), symbol]
@@ -204,9 +203,9 @@ module KSEQ-SYMBOLIC
   imports ML-SYNTAX
   imports KVARIABLE-SYNTAX
 
-  syntax #KVariable ::= r"(?<![A-Za-z0-9_\\$!\\?@])(\\!|\\?|@)?([A-Z][A-Za-z0-9'_]*|_|_[A-Z][A-Za-z0-9'_]*)"   [token, prec(1)]
+  syntax #KVariable ::= r"(\\!|\\?|@)?([A-Z][A-Za-z0-9'_]*|_|_[A-Z][A-Za-z0-9'_]*)"   [token, prec(1)]
                       | #UpperId                                                          [token]
-  syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?@])(\\$)([A-Z][A-Za-z0-9'_]*)"            [token]
+  syntax KConfigVar ::= r"(\\$)([A-Z][A-Za-z0-9'_]*)"            [token]
   syntax KBott      ::= #KVariable
   syntax KBott      ::= KConfigVar
 endmodule

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

@@ -35,7 +35,7 @@ and can be followed by zero or more letters, numbers, or underscores.
 module KVAR-SYNTAX-PROGRAM-PARSING
   imports BUILTIN-ID-TOKENS
 
-  syntax KVar ::= r"(?<![A-Za-z0-9\\_])[A-Za-z\\_][A-Za-z0-9\\_]*"     [prec(1), token]
+  syntax KVar ::= r"[A-Za-z\\_][A-Za-z0-9\\_]*"     [prec(1), token]
                 | #LowerId                                             [token]
                 | #UpperId                                             [token]
 endmodule

k-distribution/tests/regression-new/bison-glr-bug/iele.k

@@ -2,7 +2,7 @@
 module IELE-SYNTAX
   imports IELE-COMMON
   syntax IeleNameToken  ::=
-    r"(?<![A-Za-z0-9\\_\\.\\-\\$])[a-zA-Z\\.\\_\\$][0-9a-zA-Z\\.\\_\\-\\$]*" [prec(3), token]
+    r"[a-zA-Z\\.\\_\\$][0-9a-zA-Z\\.\\_\\-\\$]*" [prec(3), token]
   syntax Keyword  ::=
     "load" [token]
   | "store" [token]

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

@@ -1,12 +1,12 @@
 |"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}))*[\\\"]"|
 |"+"                                                                              | (14,1,14,2)   | "+"                 |

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-frontend/src/main/java/org/kframework/kore/convertors/KILtoKORE.java

@@ -261,9 +261,7 @@ public Set<org.kframework.definition.Sentence> apply(Syntax s) {
               throw new AssertionError("Lists should have applied before.");
             } else if (it instanceof Lexical) {
               String regex = ((Lexical) it).getLexicalRule();
-              RegexTerminal regexTerminal = getRegexTerminal(regex);
-
-              items.add(regexTerminal);
+              items.add(RegexTerminal(regex));
             } else if (it instanceof Terminal) {
               items.add(Terminal(((Terminal) it).getTerminal()));
             } else {
@@ -305,35 +303,6 @@ else if (p.containsAttribute(Att.NON_ASSOC()))
     return res;
   }
 
-  public static RegexTerminal getRegexTerminal(String regex) {
-    String precede = "#";
-    if (regex.startsWith("(?<!")) { // find the precede pattern in the beginning: (?<!X)
-      int depth = 1;
-      for (int i = 1; i < regex.length(); i++) {
-        if (regex.charAt(i) == '\\') {
-          i++;
-          continue;
-        }
-        if (regex.charAt(i) == '(') depth++;
-        if (regex.charAt(i) == ')') depth--;
-        if (depth == 0) {
-          precede = regex.substring("(?<!".length(), i);
-          regex = regex.substring(i + 1);
-          break;
-        }
-      }
-    }
-    String follow = "#";
-    int followIndex = regex.lastIndexOf("(?!");
-    if (followIndex != -1 && regex.endsWith(")")) { // find the follow pattern at the end: (?!X)
-      if (!(followIndex > 0 && regex.charAt(followIndex - 1) == '\\')) {
-        follow = regex.substring(followIndex + "(?!".length(), regex.length() - 1);
-        regex = regex.substring(0, followIndex);
-      }
-    }
-    return RegexTerminal(precede, regex, follow);
-  }
-
   public void applyUserList(
       Set<org.kframework.definition.Sentence> res,
       org.kframework.kore.Sort sort,

k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java

@@ -298,10 +298,8 @@ private static ProductionItem toProductionItem(JsonObject data) {
         return new NonTerminal(sort, name);
       }
       case KREGEXTERMINAL -> {
-        String precedeRegex = data.getString("precedeRegex");
         String regex = data.getString("regex");
-        String followRegex = data.getString("followRegex");
-        return new RegexTerminal(precedeRegex, regex, followRegex);
+        return new RegexTerminal(regex);
       }
       case KTERMINAL -> {
         String value = data.getString("value");

k-frontend/src/main/java/org/kframework/unparser/ToJson.java

@@ -369,9 +369,7 @@ public static JsonObject toJson(ProductionItem prod) {
       if (!name.isEmpty()) jsonProduction.add("name", name.get());
     } else if (prod instanceof RegexTerminal t) {
       jsonProduction.add("node", JsonParser.KREGEXTERMINAL);
-      jsonProduction.add("precedeRegex", t.precedeRegex());
       jsonProduction.add("regex", t.regex());
-      jsonProduction.add("followRegex", t.followRegex());
     } else if (prod instanceof Terminal t) {
       jsonProduction.add("node", JsonParser.KTERMINAL);
       jsonProduction.add("value", t.value());

k-frontend/src/main/scala/org/kframework/definition/Constructors.scala

@@ -75,9 +75,7 @@ object Constructors {
   def Terminal(s: String)                           = definition.Terminal(s)
   def NonTerminal(sort: Sort)                       = definition.NonTerminal(sort, None)
   def NonTerminal(sort: Sort, name: Option[String]) = definition.NonTerminal(sort, name)
-  def RegexTerminal(regexString: String) = definition.RegexTerminal("#", regexString, "#")
-  def RegexTerminal(precedeRegexString: String, regexString: String, followRegexString: String) =
-    definition.RegexTerminal(precedeRegexString, regexString, followRegexString)
+  def RegexTerminal(regexString: String)            = definition.RegexTerminal(regexString)
 
   def Tag(s: String) = definition.Tag(s)
 

k-frontend/src/main/scala/org/kframework/definition/outer-to-string.scala

@@ -75,11 +75,7 @@ trait NonTerminalToString {
 trait RegexTerminalToString {
   self: RegexTerminal =>
   override def toString =
-    "r" + StringUtil.enquoteKString(
-      (if ("#" == precedeRegex) "" else "(?<!" + precedeRegex + ")") +
-        regex +
-        (if ("#" == followRegex) "" else "(?!" + followRegex + ")")
-    )
+    "r" + StringUtil.enquoteKString(regex)
 }
 
 trait SyntaxAssociativityToString {

k-frontend/src/main/scala/org/kframework/definition/outer.scala

@@ -244,7 +244,7 @@ case class Module(
     productionsForSort
       .getOrElse(Sorts.Layout.head, immutable.Set[Production]())
       .collect {
-        case Production(_, _, _, immutable.Seq(RegexTerminal(_, terminalRegex, _)), _) =>
+        case Production(_, _, _, immutable.Seq(RegexTerminal(terminalRegex)), _) =>
           terminalRegex
         case p =>
           throw KEMException.compilerError(
@@ -967,7 +967,7 @@ case class Production(
           case (Terminal("("), i)              => s"%${i + 1}..."
           case (Terminal(_), i)                => s"%${i + 1}"
           case (NonTerminal(_, Some(name)), i) => s"$name: %${i + 1}"
-          case (RegexTerminal(_, _, _), _) =>
+          case (RegexTerminal(_), _) =>
             throw new IllegalArgumentException(
               "Default format not supported for productions with regex terminals"
             )
@@ -1022,9 +1022,7 @@ case class NonTerminal(sort: Sort, name: Option[String])
     extends ProductionItem
     with NonTerminalToString
 
-case class RegexTerminal(precedeRegex: String, regex: String, followRegex: String)
-    extends TerminalLike
-    with RegexTerminalToString {
+case class RegexTerminal(regex: String) extends TerminalLike with RegexTerminalToString {
   lazy val pattern = new RunAutomaton(new RegExp(regex).toAutomaton, false)
 
   def compareTo(t: TerminalLike): Int = {

k-frontend/src/test/java/org/kframework/parser/inner/RuleGrammarTest.java

@@ -15,13 +15,11 @@
 import org.kframework.attributes.Source;
 import org.kframework.definition.Definition;
 import org.kframework.definition.Module;
-import org.kframework.definition.RegexTerminal;
 import org.kframework.kompile.DefinitionParsing;
 import org.kframework.kompile.Kompile;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.kore.K;
 import org.kframework.kore.Sort;
-import org.kframework.kore.convertors.KILtoKORE;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.GlobalOptions.Warnings;
 import org.kframework.parser.ParserUtils;
@@ -347,26 +345,6 @@ public void test15() {
     parseRule("Divide(K1:K, K2:K) => K1:K / K2:K", def, 0, false);
   }
 
-  // test lexical to RegexTerminal extractor
-  @Test
-  public void test16() {
-    assertPatterns("", "#", "", "#");
-    assertPatterns("abc", "#", "abc", "#");
-    assertPatterns("(?<!abc)", "abc", "", "#");
-    assertPatterns("(?<!abc)def", "abc", "def", "#");
-    assertPatterns("(?<!abcdef", "#", "(?<!abcdef", "#");
-    assertPatterns("(?!abc)", "#", "", "abc");
-    assertPatterns("\\(?!abc)", "#", "\\(?!abc)", "#");
-  }
-
-  private static void assertPatterns(
-      String original, String precede, String pattern, String follow) {
-    RegexTerminal re1 = KILtoKORE.getRegexTerminal(original);
-    Assert.assertEquals(precede, re1.precedeRegex());
-    Assert.assertEquals(pattern, re1.regex());
-    Assert.assertEquals(follow, re1.followRegex());
-  }
-
   // test the new regex engine
   @Test
   public void test17() {

k-frontend/src/test/java/org/kframework/unparser/AddBracketsTest.java

@@ -73,7 +73,7 @@ public void testLambda() {
             + "  syntax Exp ::= Val\n"
             + "               | Exp Exp      [left]\n"
             + "               | \"(\" Exp \")\"  [bracket]\n"
-            + "  syntax Id ::= r\"(?<![A-Za-z0-9\\\\_])[A-Za-z\\\\_][A-Za-z0-9\\\\_]*\"     [token,"
+            + "  syntax Id ::= r\"[A-Za-z\\\\_][A-Za-z0-9\\\\_]*\"     [token,"
             + " autoreject]\n"
             + "endmodule\n";
     unparserTest(def, "( lambda z . ( z z ) ) lambda x . lambda y . ( x y )");

k-frontend/src/test/resources/convertor-tests/kore.k

@@ -82,7 +82,7 @@ endmodule
 // To be used to parse semantic rules
 module K
   imports KSEQ
-  syntax KVariable ::= r"(?<![A-Za-z0-9\\_])(\\$|\\!|\\?)?([A-Z][A-Za-z0-9']*|_)" [ hook, token ] // same like KSort?
+  syntax KVariable ::= r"(\\$|\\!|\\?)?([A-Z][A-Za-z0-9']*|_)" [ hook, token ] // same like KSort?
   syntax KItem     ::= KVariable        //[ ... ]
   syntax KLabel    ::= KVariable        //[ ... ]
   syntax K         ::= K "=>" K         [ klabel(#KRewrite), hook(Rewrite) ]

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

@@ -2,7 +2,7 @@
 module IELE-SYNTAX
   imports IELE-COMMON
   syntax IeleNameToken  ::=
-    r"(?<![A-Za-z0-9\\_\\.\\-\\$])[a-zA-Z\\.\\_\\$][0-9a-zA-Z\\.\\_\\-\\$]*" [prec(3), token]
+    r"[a-zA-Z\\.\\_\\$][0-9a-zA-Z\\.\\_\\-\\$]*" [prec(3), token]
   syntax Keyword  ::=
     "load" [token]
   | "store" [token]