Merge branch 'develop' into version-file2

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/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);
 

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

@@ -31,6 +31,9 @@
 @RequestScoped
 public final class KastOptions {
 
+    @Inject
+    public KastOptions() {}
+
     @Parameter(description="<file>")
     private List<String> parameters;
 
@@ -155,4 +158,7 @@ public Class<InputModes> enumClass() {
             return InputModes.class;
         }
     }
+
+    @Parameter(names="--debug-tokens", description="Print a Markdown table of tokens matched by the scanner. Useful for debugging parsing errors.")
+    public boolean debugTokens = false;
 }

kernel/src/main/java/org/kframework/kdep/KDepModule.java

@@ -22,7 +22,7 @@
 public class KDepModule extends AbstractModule {
     @Override
     protected void configure() {
-
+        binder().requireAtInjectOnConstructors();
         bind(FrontEnd.class).to(KDepFrontEnd.class);
         bind(Tool.class).toInstance(Tool.KDEP);
 

kernel/src/main/java/org/kframework/kdep/KDepOptions.java

@@ -3,6 +3,7 @@
 
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
+import com.google.inject.Inject;
 import org.kframework.main.GlobalOptions;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.OuterParsingOptions;
@@ -16,6 +17,9 @@
 @RequestScoped
 public class KDepOptions {
 
+    @Inject
+    public KDepOptions() {}
+
     @ParametersDelegate
     public transient GlobalOptions global = new GlobalOptions();
 

kernel/src/main/java/org/kframework/kil/loader/Context.java

@@ -19,6 +19,9 @@
 @RequestScoped
 public class Context implements Serializable {
 
+    @Inject
+    public Context() {}
+
     /**
      * Represents a map from all Klabels or attributes in string representation
      * to sets of corresponding productions.

kernel/src/main/java/org/kframework/kompile/BackendModule.java

@@ -14,6 +14,7 @@
 public class BackendModule extends AbstractModule {
     @Override
     protected void configure() {
+        binder().requireAtInjectOnConstructors();
         MapBinder<String, Backend> backendBinder = MapBinder.newMapBinder(
                 binder(), String.class, org.kframework.compile.Backend.class);
         backendBinder.addBinding("kore").to(KoreBackend.class);

kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java

@@ -207,6 +207,12 @@ public K parseSingleTerm(Module module, Sort programStartSymbol, String startSym
         }
     }
 
+    public String showTokens(Module module, FileUtil files, String s, Source source) {
+        try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(module, true, files)) {
+            return parseInModule.tokenizeString(s, source);
+        }
+    }
+
     public Module getExtensionModule(Module module, FileUtil files) {
         return RuleGrammarGenerator.getCombinedGrammar(module, true, files).getExtensionModule();
     }