diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 106f8de707e..9dfe5840555 100644 --- a/.github/actions/with-docker/action.yml +++ b/.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} \ diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 1e60083f4ef..d250f1c033d 100644 --- a/.github/workflows/Dockerfile +++ b/.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 diff --git a/.github/workflows/Dockerfile.z3 b/.github/workflows/Dockerfile.z3 deleted file mode 100644 index c2ec54df25c..00000000000 --- a/.github/workflows/Dockerfile.z3 +++ /dev/null @@ -1,24 +0,0 @@ -ARG BASE_DISTRO -ARG BASE_OS -FROM ${BASE_OS}:${BASE_DISTRO} - -ENV TZ=America/Chicago -RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone - -RUN apt-get update \ - && apt-get upgrade --yes \ - && apt-get install --yes \ - clang \ - cmake \ - git \ - python3 - -ARG Z3_VERSION=4.8.15 -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \ - && cd z3 \ - && python3 scripts/mk_make.py \ - && cd build \ - && make -j8 \ - && make install \ - && cd ../.. \ - && rm -rf z3 diff --git a/deps/z3 b/deps/z3 new file mode 100644 index 00000000000..53cf85e173b --- /dev/null +++ b/deps/z3 @@ -0,0 +1 @@ +4.12.1 diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java index b2fd5daa67a..d86230dbafa 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java @@ -26,6 +26,7 @@ public List getKompileModules() { mods.add(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bindOptions(HaskellBackendKModule.this::kompileOptions, binder()); installHaskellBackend(binder()); } @@ -54,6 +55,7 @@ public List getKRunModules() { return Collections.singletonList(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); installHaskellRewriter(binder()); } }); @@ -74,6 +76,7 @@ public List getKProveModules() { return Collections.singletonList(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); installHaskellBackend(binder()); installHaskellRewriter(binder()); } diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java index 5c20d442625..3a6649ef34c 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java +++ b/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) diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java index 69a9c8b4b2c..081be372136 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java +++ b/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"; diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun index 7f684964a01..e5e88599fe4 100755 --- a/k-distribution/src/main/scripts/bin/krun +++ b/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 ;; diff --git a/k-distribution/src/main/scripts/lib/k b/k-distribution/src/main/scripts/lib/k index 34f4bf3b639..1d510a2ff60 100755 --- a/k-distribution/src/main/scripts/lib/k +++ b/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}" diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile b/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile new file mode 100644 index 00000000000..5ab56c86a70 --- /dev/null +++ b/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 diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast new file mode 100644 index 00000000000..0d8c763edc3 --- /dev/null +++ b/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" diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out new file mode 100644 index 00000000000..903a7ba1fd5 --- /dev/null +++ b/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) | "" | + diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast new file mode 100644 index 00000000000..f845bb7df41 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast @@ -0,0 +1 @@ +1 + 2 + aaa diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out new file mode 100644 index 00000000000..1525daf1bc8 --- /dev/null +++ b/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) | "" | + diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k b/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k new file mode 100644 index 00000000000..90b98cf29a9 --- /dev/null +++ b/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 $PGM:Exp + +endmodule diff --git a/kernel/pom.xml b/kernel/pom.xml index c932c02dcc6..aa1541af51d 100644 --- a/kernel/pom.xml +++ b/kernel/pom.xml @@ -32,13 +32,13 @@ com.google.inject guice - 4.0-beta5 + 4.0 no_aop com.google.inject.extensions guice-multibindings - 4.0-beta5 + 4.0 com.google.inject @@ -49,7 +49,7 @@ com.google.inject.extensions guice-grapher - 4.0-beta5 + 4.0 com.google.inject @@ -60,7 +60,7 @@ com.google.inject.extensions guice-throwingproviders - 4.0-beta5 + 4.0 com.google.inject diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java index 9156ed7c766..c222faa9924 100644 --- a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java +++ b/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, K>, Set> 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, K>, Set> 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"); diff --git a/kernel/src/main/java/org/kframework/kast/KastModule.java b/kernel/src/main/java/org/kframework/kast/KastModule.java index aeb3976a48d..a28605ce26d 100644 --- a/kernel/src/main/java/org/kframework/kast/KastModule.java +++ b/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); diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java index 2aaa084b516..7ef74e430c6 100644 --- a/kernel/src/main/java/org/kframework/kast/KastOptions.java +++ b/kernel/src/main/java/org/kframework/kast/KastOptions.java @@ -31,6 +31,9 @@ @RequestScoped public final class KastOptions { + @Inject + public KastOptions() {} + @Parameter(description="") private List parameters; @@ -155,4 +158,7 @@ public Class 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; } diff --git a/kernel/src/main/java/org/kframework/kdep/KDepModule.java b/kernel/src/main/java/org/kframework/kdep/KDepModule.java index c068f105368..ed6af4762b9 100644 --- a/kernel/src/main/java/org/kframework/kdep/KDepModule.java +++ b/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); diff --git a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java index d830c3b8bf3..c65cc98273e 100644 --- a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java +++ b/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(); diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java index 2bc8a8252db..a136a3922e6 100644 --- a/kernel/src/main/java/org/kframework/kil/loader/Context.java +++ b/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. diff --git a/kernel/src/main/java/org/kframework/kompile/BackendModule.java b/kernel/src/main/java/org/kframework/kompile/BackendModule.java index 35b91d2654f..5425cabee5c 100644 --- a/kernel/src/main/java/org/kframework/kompile/BackendModule.java +++ b/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 backendBinder = MapBinder.newMapBinder( binder(), String.class, org.kframework.compile.Backend.class); backendBinder.addBinding("kore").to(KoreBackend.class); diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java index a2342afd40d..289619a9fa7 100644 --- a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java +++ b/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(); } diff --git a/kernel/src/main/java/org/kframework/kompile/KompileModule.java b/kernel/src/main/java/org/kframework/kompile/KompileModule.java index 10ed758e44e..3757d7c6432 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileModule.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileModule.java @@ -25,6 +25,7 @@ public KompileModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KompileFrontEnd.class); bind(Tool.class).toInstance(Tool.KOMPILE); diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 8d494435b6d..ba96c409fdd 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.apache.commons.io.FilenameUtils; import org.kframework.backend.Backends; import org.kframework.main.GlobalOptions; @@ -23,7 +24,8 @@ @RequestScoped public class KompileOptions implements Serializable { - + @Inject + public KompileOptions() {} /** * WARNING: this field will be non-null in kompile tool, but null when KompileOption is deserialized, diff --git a/kernel/src/main/java/org/kframework/kprove/KProveModule.java b/kernel/src/main/java/org/kframework/kprove/KProveModule.java index 84b17c42eb3..ca375b76ad7 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveModule.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveModule.java @@ -20,6 +20,7 @@ public class KProveModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KProveFrontEnd.class); bind(Tool.class).toInstance(Tool.KPROVE); diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java index b5b59d83917..d25a5b6b6c3 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java @@ -4,6 +4,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.kframework.unparser.PrintOptions; import org.kframework.main.GlobalOptions; import org.kframework.utils.file.FileUtil; @@ -20,6 +21,8 @@ @RequestScoped public class KProveOptions { + @Inject + public KProveOptions() {} @ParametersDelegate private final transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java index 5670711aa9b..90ea42f76b8 100644 --- a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java +++ b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java @@ -17,6 +17,7 @@ public class RewriterModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FileUtil.class); } diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java index 2ae3035c72b..93328edf004 100644 --- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java +++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java @@ -22,6 +22,7 @@ public class KSearchPatternModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KSearchPatternFrontEnd.class); bind(Tool.class).toInstance(Tool.KSEARCHPATTERN); diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java index 1c2d9a32a08..9fcc1baec84 100644 --- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java +++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.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.DefinitionLoadingOptions; @@ -16,6 +17,9 @@ @RequestScoped public class KSearchPatternOptions { + @Inject + public KSearchPatternOptions() {} + @ParametersDelegate public transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/kserver/KServerModule.java b/kernel/src/main/java/org/kframework/kserver/KServerModule.java index f8e9f4d57bb..865cdfc76f4 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerModule.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerModule.java @@ -20,6 +20,7 @@ public class KServerModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(Tool.class).toInstance(Tool.KSERVER); bind(FrontEnd.class).to(KServerFrontEnd.class); diff --git a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java index 322b689b874..b09695b0ac3 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java @@ -1,6 +1,7 @@ // Copyright (c) K Team. All Rights Reserved. package org.kframework.kserver; +import com.google.inject.Inject; import org.kframework.main.GlobalOptions; import org.kframework.utils.inject.RequestScoped; @@ -10,6 +11,9 @@ @RequestScoped public class KServerOptions { + @Inject + public KServerOptions() {} + @ParametersDelegate public transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/kernel/src/main/java/org/kframework/main/AbstractKModule.java index 9fc12a9cb48..2a8dd35361b 100644 --- a/kernel/src/main/java/org/kframework/main/AbstractKModule.java +++ b/kernel/src/main/java/org/kframework/main/AbstractKModule.java @@ -37,6 +37,7 @@ public List, Boolean>> kproveOptions() { } protected void bindOptions(Supplier, Boolean>>> action, Binder binder) { + binder.requireAtInjectOnConstructors(); Multibinder optionsBinder = Multibinder.newSetBinder(binder, Object.class, Options.class); for (Pair, Boolean> option : action.get()) { optionsBinder.addBinding().to(option.getKey()); @@ -81,6 +82,7 @@ public List getDefinitionSpecificKEqModules() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); //bind backend implementations of tools to their interfaces } }); diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/kernel/src/main/java/org/kframework/main/FrontEnd.java index 7417d75ee92..08e015488e0 100644 --- a/kernel/src/main/java/org/kframework/main/FrontEnd.java +++ b/kernel/src/main/java/org/kframework/main/FrontEnd.java @@ -2,6 +2,7 @@ package org.kframework.main; import com.beust.jcommander.ParameterException; +import com.google.inject.Inject; import com.google.inject.Provider; import org.kframework.utils.ExitOnTimeoutThread; import org.kframework.utils.InterrupterRunnable; @@ -22,6 +23,7 @@ public abstract class FrontEnd { private final JarInfo jarInfo; private final Provider files; + @Inject public FrontEnd( KExceptionManager kem, GlobalOptions globalOptions, diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/kernel/src/main/java/org/kframework/main/GlobalOptions.java index f0ae7d82c66..d78fad84535 100644 --- a/kernel/src/main/java/org/kframework/main/GlobalOptions.java +++ b/kernel/src/main/java/org/kframework/main/GlobalOptions.java @@ -19,13 +19,6 @@ public final class GlobalOptions { public GlobalOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - /** - * Prevents instantiation by Guice when not explicitly configured in a Module. - */ - @Inject - public GlobalOptions(Void v) {} - public GlobalOptions(boolean debug, Warnings warnings, boolean verbose) { this.debug = debug; this.warnings = warnings; diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index c5b50cf4afb..6ed83e89188 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -51,6 +51,10 @@ public KRead( this.globalOptions = globalOptions; } + public String showTokens(Module mod, CompiledDefinition def, String stringToParse, Source source) { + return def.showTokens(mod, files, stringToParse, source); + } + public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledDefinition def, Source source, String stringToParse) { return prettyRead(mod, sort, startSymbolLocation, def, source, stringToParse, this.input); } diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index 3aa8b4bf713..4e3cbdb4066 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -7,6 +7,8 @@ import org.kframework.attributes.Source; import org.kframework.builtin.Sorts; import org.kframework.definition.Module; +import org.kframework.definition.Terminal; +import org.kframework.definition.TerminalLike; import org.kframework.kore.K; import org.kframework.kore.Sort; import org.kframework.main.GlobalOptions; @@ -16,6 +18,7 @@ import org.kframework.parser.inner.kernel.EarleyParser; import org.kframework.parser.inner.kernel.Scanner; import org.kframework.parser.outer.Outer; +import org.kframework.utils.StringUtil; import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.file.FileUtil; import scala.Tuple2; @@ -28,10 +31,9 @@ import java.io.IOException; import java.io.Serializable; import java.nio.charset.StandardCharsets; -import java.util.Collections; -import java.util.Queue; -import java.util.Set; +import java.util.*; import java.util.concurrent.ConcurrentLinkedQueue; +import java.util.stream.Collectors; /** * A wrapper that takes a module and one can call the parser @@ -159,6 +161,52 @@ public void initialize() { } } + /** + * Print the list of tokens matched by the scanner, the location and the Regex Terminal + * The output is a valid Markdown table. + */ + public String tokenizeString(String input, Source source) { + StringBuilder sb = new StringBuilder(); + try (Scanner scanner = getScanner()) { + EarleyParser.ParserMetadata mdata = new EarleyParser.ParserMetadata(input, scanner, source, 1, 1); + Map kind2Token = + scanner.getTokens().entrySet().stream().map(a -> new Tuple2<>(a.getValue()._1, a.getKey())) + .collect(Collectors.toMap(Tuple2::_1, Tuple2::_2)); + List lines = mdata.getLines(); + List columns = mdata.getColumns(); + int maxTokenLen = 7, maxLocLen = 10, maxTerminalLen = 10; + List locs = new ArrayList<>(); + List tokens = new ArrayList<>(); + List terminals = new ArrayList<>(); + List words = mdata.getWords(); + for (Scanner.Token word : mdata.getWords()) { + String loc = String.format("(%d,%d,%d,%d)", + lines.get(word.startLoc), columns.get(word.startLoc), + lines.get(word.endLoc), columns.get(word.endLoc)); + locs.add(loc); + maxLocLen = Math.max(maxLocLen, loc.length()); + String tok = StringUtil.enquoteKString(word.value); + tokens.add(tok); + maxTokenLen = Math.max(maxTokenLen, tok.length()); + String terminal = kind2Token.getOrDefault(word.kind, Terminal.apply("")).toString(); + terminals.add(terminal); + maxTerminalLen = Math.max(maxTerminalLen, terminal.length()); + } + // if the token is absurdly large limit the column to 80 chars to maintain alignment + maxTokenLen = Math.min(maxTokenLen, 80); + maxTerminalLen = Math.min(maxTerminalLen, 20); + sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n", + "\"Match\"", "(location)", "Terminal")); + sb.append(String.format("|-%s|--%s|-%s|\n", "-".repeat(maxTokenLen), "-".repeat(maxLocLen), "-".repeat(maxTerminalLen))); + for (int i = 0; i < words.size(); i++) { + Scanner.Token word = words.get(i); + sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n", + tokens.get(i), locs.get(i), terminals.get(i))); + } + } + return sb.toString(); + } + public Tuple2, K>, Set> parseString(String input, Sort startSymbol, String startSymbolLocation, Source source) { try (Scanner scanner = getScanner()) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java index 7f48bda662e..8f3f541295e 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java @@ -1,6 +1,7 @@ // Copyright (c) K Team. All Rights Reserved. package org.kframework.parser.inner.kernel; +import com.google.common.primitives.Ints; import org.apache.commons.codec.binary.StringUtils; import org.jetbrains.annotations.NotNull; import org.kframework.attributes.Att; @@ -23,18 +24,7 @@ import org.pcollections.ConsPStack; import org.pcollections.PStack; -import java.nio.charset.StandardCharsets; -import java.util.Arrays; -import java.util.ArrayList; -import java.util.BitSet; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.List; -import java.util.Map; -import java.util.Objects; -import java.util.Optional; -import java.util.Set; +import java.util.*; import java.util.stream.Collectors; import static org.kframework.Collections.*; @@ -525,7 +515,7 @@ public void finish() { * Metadata about the state of the sentence being parsed. We collect this all in a single place in order to simplify * the type signatures of many methods. */ - private static class ParserMetadata { + public static class ParserMetadata { /** * @param input The sentence being parsed * @param scanner The scanner to use to tokenize the sentence @@ -583,15 +573,27 @@ public ParserMetadata(String input, Scanner scanner, Source source, int startLin } // the list of tokens in the sentence - Scanner.Token[] words; + final Scanner.Token[] words; // an array containing the line of each character in the input sentence - int[] lines; + final int[] lines; // an array containing the column of each character in the input sentence - int[] columns; + final int[] columns; // a Source containing the file the sentence was parsed from Source source; // the original un-tokenized input sentence String input; + + public List getWords() { + return List.of(words); + } + + public List getLines() { + return Collections.unmodifiableList(Ints.asList(lines)); + } + + public List getColumns() { + return Collections.unmodifiableList(Ints.asList(columns)); + } } /** diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java index d59300a5b39..b71d0c44c16 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java @@ -30,14 +30,7 @@ import java.nio.ByteOrder; import java.nio.file.StandardCopyOption; import java.nio.file.Files; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.TreeMap; +import java.util.*; import java.util.concurrent.Semaphore; import java.util.function.BiConsumer; import java.util.stream.Collectors; @@ -57,6 +50,10 @@ public class Scanner implements AutoCloseable { public static final String COMPILER = OS.current().equals(OS.OSX) ? "clang" : "gcc"; + public Map> getTokens() { + return Collections.unmodifiableMap(tokens); + } + public static Map> getTokens(Module module) { Map tokens = new TreeMap<>(); Set terminals = new HashSet<>(); @@ -349,10 +346,10 @@ public int resolve(TerminalLike terminal) { } public static class Token { - final int kind; - final String value; - final int startLoc; - final int endLoc; + public final int kind; + public final String value; + public final int startLoc; + public final int endLoc; public Token(int kind, String value, long startLoc, long endLoc) { this.kind = kind; diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java index c74146e45ea..74c860c80da 100644 --- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java +++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java @@ -23,14 +23,6 @@ public PrintOptions(OutputModes output) { this.output = output; } - //TODO(dwightguth): remove in Guice 4.0 - /** - * Prevents instantiation by Guice when not explicitly configured in a Module. - */ - @Inject - public PrintOptions(Void v) { - } - @Parameter(names = "--color", description = "Use colors in output. Default is on.", descriptionKey = "mode", converter=ColorModeConverter.class) private ColorSetting color; diff --git a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java index 1eedd8619c1..bb1a47f6d2c 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java @@ -22,6 +22,7 @@ public class CommonModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); SimpleScope requestScope = new SimpleScope(); bindScope(RequestScoped.class, requestScope); DefinitionScope definitionScope = new DefinitionScope(); diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java index d093fdf0228..9f3f60084de 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java @@ -27,6 +27,7 @@ public class DefinitionLoadingModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); } @Provides @DefinitionScoped diff --git a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java index 5c5f2c87414..495db016164 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java @@ -31,6 +31,7 @@ public class JCommanderModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(String[].class).annotatedWith(Options.class) .toProvider(SimpleScope.seededKeyProvider()).in(RequestScoped.class);; } diff --git a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java index f6f0a7eec3c..cdb86466444 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java @@ -27,7 +27,7 @@ public class OuterParsingModule extends AbstractModule { @Override protected void configure() { - + binder().requireAtInjectOnConstructors(); } @Provides diff --git a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java index 2046937054e..14c57e748d1 100644 --- a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java @@ -10,10 +10,6 @@ public class BackendOptions implements Serializable { public BackendOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public BackendOptions(Void v) {} - @Parameter(names="--dry-run", description="Compile program into KORE format but do not run. Only used in Haskell and LLVM backend.") public boolean dryRun = false; } diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java index 8f9ed1b7b41..a4d1c9c4f8b 100644 --- a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java @@ -8,10 +8,6 @@ public class DefinitionLoadingOptions { public DefinitionLoadingOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public DefinitionLoadingOptions(Void v) {} - @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the kompiled " + "K definition resides. The default is the unique, only directory with the suffix '-kompiled' " + "in the current directory.", descriptionKey = "path", hidden = true) diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java index b1acb132943..9fd7cc13a32 100644 --- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java @@ -10,12 +10,7 @@ public class SMTOptions implements Serializable { public SMTOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public SMTOptions(Void v) {} - - @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class, - description="SMT solver to use for checking constraints. is one of [z3|none].", hidden = true) + @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. is one of [z3|none].", descriptionKey = "executable", hidden = true) public SMTSolver smt = SMTSolver.Z3; public static class SMTSolverConverter extends BaseEnumConverter { diff --git a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java index 17212387f6a..4ccafc4829a 100644 --- a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java +++ b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java @@ -71,6 +71,7 @@ public class DefinitionSpecificTestModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(KompileOptions.class).toInstance(context.kompileOptions); bind(Definition.class).toInstance(definition); bind(File.class).annotatedWith(KompiledDir.class).toInstance(kompiledDir); @@ -88,6 +89,7 @@ public class TestModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(RunProcess.class).toInstance(rp); bind(KastOptions.class).toInstance(new KastOptions()); } diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java index e81ce93f110..bb757de59a8 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.IStringConverter; +import com.google.inject.Inject; import org.kframework.utils.inject.RequestScoped; import java.util.Arrays; @@ -12,6 +13,9 @@ @RequestScoped public class LLVMKompileOptions { + @Inject + public LLVMKompileOptions() {} + @Parameter(names="--enable-llvm-debug", description="Enable debugging support for the LLVM backend.") public boolean debug = false; diff --git a/nix/mavenix.lock b/nix/mavenix.lock index 7be2b7a378a..541407e5860 100644 --- a/nix/mavenix.lock +++ b/nix/mavenix.lock @@ -282,52 +282,52 @@ "sha1": "1b77ba79f9b2b7dfd4e15ea7bb0d568d5eb9cb8d" }, { - "path": "com/google/inject/extensions/extensions-parent/4.0-beta5/extensions-parent-4.0-beta5.pom", - "sha1": "516d8e5e771cd573364dc6ff53c2c6c13908a713" + "path": "com/google/inject/extensions/extensions-parent/4.0/extensions-parent-4.0.pom", + "sha1": "db8e45ab989a2347421ff0d32be5446528d6f63f" }, { - "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.jar", - "sha1": "820f10e0650cd9ed2591f398937df50f330b147d" + "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.jar", + "sha1": "8fa6431da1a2187817e3e52e967535899e2e46ca" }, { - "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.pom", - "sha1": "4b9b352e0537b0ca49cb97533387864b185df09b" + "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.pom", + "sha1": "00c7fc29684b20dd475f517d5dafc850c613efde" }, { - "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.jar", - "sha1": "dd9a00d72fecfa05a77bf28c7922eacddda23b18" + "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.jar", + "sha1": "4e611ae9b12bfc4ddd430a58c65ba1c4328eeaf9" }, { - "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.pom", - "sha1": "1cd692901e55d382cdb9e647d74617bb68d63126" + "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.pom", + "sha1": "86b9c4937ebba7d14054d0f025f0df51d071218d" }, { - "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.jar", - "sha1": "f432356db0a167127ffe4a7921238d7205b12682" + "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.jar", + "sha1": "f4509545b4470bbcc865aa500ad6fef2e97d28bf" }, { - "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.pom", - "sha1": "3cff7b7b5f418f5edca0fa1b0d4bcd3f3215d9c7" + "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.pom", + "sha1": "2387a1e5163308cd826b348db825973df0800ad3" }, { - "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.jar", - "sha1": "8840bd8267a5b09ee84a314a54dbdc6c1b0a7efb" + "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.jar", + "sha1": "90876169e80b4db9b61d654367c4c55079ae4e91" }, { - "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.pom", - "sha1": "cb52affb5a89e66a5f1d9ab3a7fde7dda1cc5baa" + "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.pom", + "sha1": "5118433baea2efed034af00a96e324b5717e8059" }, { - "path": "com/google/inject/guice-parent/4.0-beta5/guice-parent-4.0-beta5.pom", - "sha1": "13d7df2b77236548d1e7cb9ba688686ddd4f19a5" + "path": "com/google/inject/guice-parent/4.0/guice-parent-4.0.pom", + "sha1": "a59ca1d3d70552158088d7f71e6c7e8779b9a8a1" }, { - "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5-no_aop.jar", - "sha1": "7706f581d709b1afd89b4e0dbf1bebf250abbd9b" + "path": "com/google/inject/guice/4.0/guice-4.0-no_aop.jar", + "sha1": "199b7acaa05b570bbccf31be998f013963e5e752" }, { - "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5.pom", - "sha1": "1e968b8c1da8cb48b7c0b77ffc565f92f313c392" + "path": "com/google/inject/guice/4.0/guice-4.0.pom", + "sha1": "688cb7b0d86456e3706573fe583173ee5e728f4e" }, { "path": "com/google/j2objc/j2objc-annotations/1.3/j2objc-annotations-1.3.jar", diff --git a/package/test-package b/package/test-package index 704750337ac..6c4ae1f0bcb 100755 --- a/package/test-package +++ b/package/test-package @@ -23,5 +23,27 @@ sort_int = kllvm.ast.CompositeSort("SortInt") assert str(sort_int) == "SortInt{}" HERE +# Make sure that the help messages work and that the version of the various components is correct +PACKAGE_VERSION=$(cat /usr/lib/kframework/version) + +kast --help | grep -q -- "--version" +kdep --help | grep -q -- "--version" +kompile --help | grep -q -- "--version" +kprove --help | grep -q -- "--version" +krun --help | grep -q -- "--version" +kserver --help | grep -q -- "--version" +kparse --help | grep -q -- "--version" +kparse-gen --help | grep -q -- "--version" +kore-print --help | grep -q -- "--version" +kast --version | grep -q ${PACKAGE_VERSION} +kdep --version | grep -q ${PACKAGE_VERSION} +kompile --version | grep -q ${PACKAGE_VERSION} +kprove --version | grep -q ${PACKAGE_VERSION} +krun --version | grep -q ${PACKAGE_VERSION} +kserver --version | grep -q ${PACKAGE_VERSION} +kparse --version | grep -q ${PACKAGE_VERSION} +kparse-gen --version | grep -q ${PACKAGE_VERSION} +kore-print --version | grep -q ${PACKAGE_VERSION} + # Make sure that the Haskell Backend Booster has been installed properly. kore-rpc-booster --help