Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/llvm-backend

.github/actions/with-docker/action.yml

@@ -42,20 +42,13 @@ runs:
     run: |
       set -euxo pipefail
 
-      Z3_VERSION=4.8.15
+      Z3_VERSION=$(cat deps/z3)
       K_VERSION=$(cat ${SUBDIR}package/version)
       USER=$(id -un)
       USER_ID=$(id -u)
       GROUP=$(id -gn)
       GROUP_ID=$(id -g)
 
-      docker build ${SUBDIR}                                          \
-          --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
-          --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \
-          --build-arg BASE_OS=${BASE_OS}                              \
-          --build-arg BASE_DISTRO=${BASE_DISTRO}                      \
-          --tag z3:${BASE_DISTRO}-${Z3_VERSION}                       \
-          --file ${SUBDIR}${DOCKERFILE}.z3
       docker build ${SUBDIR}                                          \
           --build-arg USER=${USER} --build-arg USER_ID=${USER_ID}     \
           --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \

.github/workflows/Dockerfile

@@ -1,8 +1,9 @@
 ARG BASE_OS
 ARG BASE_DISTRO
 ARG K_VERSION
+
 ARG Z3_VERSION
-FROM z3:${BASE_DISTRO}-${Z3_VERSION} as Z3
+FROM runtimeverificationinc/${BASE_OS}-${BASE_DISTRO}-z3:${Z3_VERSION} as Z3
 
 ARG BASE_OS
 ARG BASE_DISTRO

deps/z3

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

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

@@ -26,6 +26,7 @@ public List<Module> getKompileModules() {
         mods.add(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
                 installHaskellBackend(binder());
             }
@@ -54,6 +55,7 @@ public List<Module> getKRunModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellRewriter(binder());
             }
         });
@@ -74,6 +76,7 @@ public List<Module> getKProveModules() {
         return Collections.singletonList(new AbstractModule() {
             @Override
             protected void configure() {
+                binder().requireAtInjectOnConstructors();
                 installHaskellBackend(binder());
                 installHaskellRewriter(binder());
             }

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

@@ -2,12 +2,15 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.backend.kore.ModuleToKORE;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.BaseEnumConverter;
 
 @RequestScoped
 public class HaskellKRunOptions {
+    @Inject
+    public HaskellKRunOptions() {}
 
     @Parameter(names="--haskell-backend-command", descriptionKey = "command",
             description="Command to run the Haskell backend execution engine.", hidden = true)

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

@@ -2,11 +2,14 @@
 package org.kframework.backend.haskell;
 
 import com.beust.jcommander.Parameter;
+import com.google.inject.Inject;
 import org.kframework.utils.inject.RequestScoped;
 
 @RequestScoped
 public class HaskellKompileOptions {
 
+    @Inject
+    public HaskellKompileOptions() {}
     @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 

k-distribution/src/main/scripts/bin/krun

@@ -37,12 +37,16 @@ filterSubst=
 if [[ "$OSTYPE" == "darwin"* ]]; then
   LLDB_FILE="$(dirname "$0")/../lib/kllvm/lldb/k_lldb_path"
   if [ -f "$LLDB_FILE" ]; then
-    DBG_CMD="$(cat "$LLDB_FILE") -- "
+    DBG_EXE="$(cat "$LLDB_FILE")"
   else
-    DBG_CMD="lldb --"
+    DBG_EXE="lldb"
   fi
+  DBG_CMD=" --"
+  DBG_FLAG=" -s "
 else
-  DBG_CMD="gdb --args "
+  DBG_EXE="gdb"
+  DBG_FLAG=" -x "
+  DBG_CMD=" --args "
 fi
 
 
@@ -112,6 +116,10 @@ $KRUN options:
                            parser. This can be overridden with -p.
       --debugger           Launch the backend in a debugging console.
                            Currently only supported on LLVM backend.
+      --debugger-batch     Launch the backend in a debugging console in batch
+                           mode. Currently only supported on LLVM backend.
+      --debugger-command FILE  Execute GDB commands from FILE to debug program.
+                               Currently only supported on LLVM backend.
   -d, --directory DIR      [DEPRECATED] Look for a kompiled directory ending in "-kompiled"
                            under the directory DIR.
       --dry-run            Do not execute backend, but instead print the
@@ -392,9 +400,24 @@ do
       ;;
 
       --debugger)
-      cmdprefix="$DBG_CMD"
+      cmdprefix="$DBG_EXE $DBG_CMD"
       ;;
 
+      --debugger-command)
+        debugCommandFile="$2"
+        cmdprefix="$DBG_EXE $DBG_FLAG $debugCommandFile $DBG_CMD"
+      shift
+      ;;
+
+      --debugger-batch)
+      if [[ $cmdprefix == *gdb* || $cmdprefix == *lldb* ]]; then
+        cmdprefix="$DBG_EXE --batch $DBG_FLAG $debugCommandFile $DBG_CMD"
+      else
+        DBG_CMD=" --batch $DBG_CMD"
+      fi
+      ;;
+
+
       --statistics)
       statistics=true
       ;;

k-distribution/src/main/scripts/lib/k

@@ -22,7 +22,7 @@ for flag in "$@"; do
         fi
 
         if [[ -z "${version}" ]]; then
-            version="v"$(cat "${K_BASE}"/version)
+            version="v"$(cat "${K_BASE}"/kframework/version)
         fi
 
         echo "K version:    ${version}"

k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KAST_FLAGS=--debug-tokens
+
+include ../../../include/kframework/ktest.mak

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

@@ -0,0 +1,14 @@
+1 + 2 + aaaaaaaaaaaa
+
+
+
+
+
+
+
+
+
+
++ 10000000
++ "str"
++ "long str that breaks                                                                    alighnment"

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

@@ -0,0 +1,15 @@
+|"Match"                                                                          | (location)    | Terminal            |
+|---------------------------------------------------------------------------------|---------------|---------------------|
+|"1"                                                                              | (1,1,1,2)     | r"[\\+-]?[0-9]+"    |
+|"+"                                                                              | (1,3,1,4)     | "+"                 |
+|"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]+"    |
+|"+"                                                                              | (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)   | "+"                 |
+|"\"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

@@ -0,0 +1 @@
+1 + 2 + aaa

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

@@ -0,0 +1,9 @@
+|"Match" | (location) | Terminal            |
+|--------|------------|---------------------|
+|"1"     | (1,1,1,2)  | r"[\\+-]?[0-9]+"    |
+|"+"     | (1,3,1,4)  | "+"                 |
+|"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/issue-3647-debugTokens/test.k

@@ -0,0 +1,14 @@
+// Copyright (c) K Team. All Rights Reserved.
+
+module TEST-SYNTAX
+    imports INT-SYNTAX
+    imports ID-SYNTAX
+    imports STRING-SYNTAX
+    syntax Exp ::= Exp "+" Exp [left] | Int | Id | String
+endmodule
+
+module TEST
+    imports TEST-SYNTAX
+    configuration <k> $PGM:Exp </k>
+
+endmodule

kernel/pom.xml

@@ -32,13 +32,13 @@
     <dependency>
       <groupId>com.google.inject</groupId>
       <artifactId>guice</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <classifier>no_aop</classifier>
     </dependency>
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-multibindings</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -49,7 +49,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-grapher</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>
@@ -60,7 +60,7 @@
     <dependency>
       <groupId>com.google.inject.extensions</groupId>
       <artifactId>guice-throwingproviders</artifactId>
-      <version>4.0-beta5</version>
+      <version>4.0</version>
       <exclusions>
         <exclusion>
           <groupId>com.google.inject</groupId>

kernel/src/main/java/org/kframework/kast/KastFrontEnd.java

@@ -135,35 +135,39 @@ public int run() {
                 Source source = options.source();
 
                 try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, true, null)) {
-                    Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source);
-                    kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet()));
-                    if (res._1().isLeft()) {
-                        throw res._1().left().get().iterator().next();
+                    if (options.debugTokens)
+                        System.out.println(parseInModule.tokenizeString(stringToParse, source));
+                    else {
+                        Tuple2<Either<Set<KEMException>, K>, Set<KEMException>> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source);
+                        kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet()));
+                        if (res._1().isLeft()) {
+                            throw res._1().left().get().iterator().next();
+                        }
+                        // important to get the extension module for unparsing because it contains generated syntax
+                        // like casts, projections and others
+                        Module unparsingMod = parseInModule.getExtensionModule();
+                        K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
+
+                        if (options.expandMacros) {
+                            parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
+                        }
+                        ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod);
+                        LabelInfo labelInfo = new LabelInfoFromModule(mod);
+                        SortInfo sortInfo = SortInfo.fromModule(mod);
+
+                        Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty());
+                        if (options.steps.contains(KompileSteps.anonVars))
+                            r = (Rule) new ResolveAnonVar().resolve(r);
+                        r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates
+                        r = (Rule) new ConstantFolding().fold(unparsingMod, r);
+                        r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r);
+                        if (options.steps.contains(KompileSteps.concretizeCells)) {
+                            r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r);
+                            r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r);
+                        }
+                        K result = r.body();
+                        kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort);
                     }
-                    // important to get the extension module for unparsing because it contains generated syntax
-                    // like casts, projections and others
-                    Module unparsingMod = parseInModule.getExtensionModule();
-                    K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get());
-
-                    if (options.expandMacros) {
-                        parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
-                    }
-                    ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod);
-                    LabelInfo labelInfo = new LabelInfoFromModule(mod);
-                    SortInfo sortInfo = SortInfo.fromModule(mod);
-
-                    Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty());
-                    if (options.steps.contains(KompileSteps.anonVars))
-                        r = (Rule) new ResolveAnonVar().resolve(r);
-                    r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates
-                    r = (Rule) new ConstantFolding().fold(unparsingMod, r);
-                    r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r);
-                    if (options.steps.contains(KompileSteps.concretizeCells)) {
-                        r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r);
-                        r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r);
-                    }
-                    K result = r.body();
-                    kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort);
                 }
 
                 sw.printTotal("Total");
@@ -210,17 +214,21 @@ public int run() {
             } else {
                 Reader stringToParse = options.stringToParse();
                 Source source = options.source();
-                K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse));
+                if (options.debugTokens)
+                    System.out.println(kread.showTokens(parsingMod, def, FileUtil.read(stringToParse), source));
+                else {
+                    K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse));
 
-                if (options.expandMacros) {
-                    parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
-                }
+                    if (options.expandMacros) {
+                        parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed);
+                    }
 
-                if (sort.equals(Sorts.K())) {
-                    sort = Sorts.KItem();
-                }
+                    if (sort.equals(Sorts.K())) {
+                        sort = Sorts.KItem();
+                    }
 
-                kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort);
+                    kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort);
+                }
             }
 
             sw.printTotal("Total");

kernel/src/main/java/org/kframework/kast/KastModule.java

@@ -21,6 +21,7 @@ public class KastModule extends AbstractModule {
 
     @Override
     public void configure() {
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KastFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KAST);