From a87f74ec0f16f594d41a2a4e4ad6f1928eb75be5 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 5 May 2023 12:03:17 -0500 Subject: [PATCH 01/14] remove --gen-bison-parser and --gen-glr-bison-parser calls --- k-distribution/k-tutorial/1_basic/commands.sh | 2 +- k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile | 1 - k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile | 1 - k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile | 1 - .../lesson_1/exercises/from-call-CC-to-callcc/Makefile | 2 +- .../lesson_1/exercises/from-callcc-to-call-CC/Makefile | 2 +- k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile | 2 +- .../pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete | 2 +- k-distribution/tests/regression-new/bison-glr-bug/Makefile | 1 - .../tests/regression-new/bison-parser-library/Makefile | 2 +- k-distribution/tests/regression-new/glr/Makefile | 1 - k-distribution/tests/regression-new/glr2/Makefile | 1 - k-distribution/tests/regression-new/glr3/Makefile | 1 - k-distribution/tests/regression-new/glr4/Makefile | 1 - k-distribution/tests/regression-new/imp++-llvm/Makefile | 2 +- k-distribution/tests/regression-new/issue-1572/Makefile | 2 +- k-distribution/tests/regression-new/issue-1602/Makefile | 2 +- k-distribution/tests/regression-new/llvm-krun/Makefile | 1 - k-distribution/tests/regression-new/locations/Makefile | 1 - k-distribution/tests/regression-new/locations2/Makefile | 1 - k-distribution/tests/regression-new/locations3/Makefile | 2 +- k-distribution/tests/regression-new/parse-c/Makefile | 2 +- k-distribution/tests/regression-new/parseNonPgm/Makefile | 1 - 23 files changed, 11 insertions(+), 23 deletions(-) diff --git a/k-distribution/k-tutorial/1_basic/commands.sh b/k-distribution/k-tutorial/1_basic/commands.sh index 66ca5cf6aae..0d2b5e14f36 100644 --- a/k-distribution/k-tutorial/1_basic/commands.sh +++ b/k-distribution/k-tutorial/1_basic/commands.sh @@ -5,7 +5,7 @@ kompile 02_basics/README.md --md-selector "k & ! exclude" --main-module LESSON-0 kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-A --syntax-module LESSON-03-A --output-definition build/03a kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-B --syntax-module LESSON-03-B --output-definition build/03b kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-C --syntax-module LESSON-03-C --output-definition build/03c -kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-D --syntax-module LESSON-03-D --output-definition build/03d --gen-bison-parser +kompile 03_parsing/README.md --md-selector "k & ! exclude" --main-module LESSON-03-D --syntax-module LESSON-03-D --output-definition build/03d kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-A --syntax-module LESSON-04-A --output-definition build/04a kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-B --syntax-module LESSON-04-B --output-definition build/04b kompile 04_disambiguation/README.md --md-selector "k & ! exclude" --main-module LESSON-04-C --syntax-module LESSON-04-C --output-definition build/04c diff --git a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile index 4211afaf951..7f9a78b77df 100644 --- a/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile +++ b/k-distribution/pl-tutorial/1_k/1_lambda/lesson_1/Makefile @@ -1,7 +1,6 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) DEF=lambda EXT=lambda -KOMPILE_FLAGS=--gen-bison-parser %/arithmetic-div-zero.lambda: true diff --git a/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile index 0bfaa2a7602..94dbb07c8f4 100644 --- a/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile +++ b/k-distribution/pl-tutorial/1_k/2_imp/lesson_1/Makefile @@ -1,7 +1,6 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) DEF=imp EXT=imp -KOMPILE_FLAGS=--gen-glr-bison-parser include $(MAKEFILE_PATH)/../../../find-k.mak include ${K_HOME}/include/kframework/ktest.mak diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile index 9fe6d749b0a..d2ba3655045 100644 --- a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile +++ b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/Makefile @@ -1,3 +1,2 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) include $(MAKEFILE_PATH)/../../1_lambda/lesson_1/Makefile -KOMPILE_FLAGS=--gen-glr-bison-parser diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile index 81ad3b4b2f6..288b0a98b46 100644 --- a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile +++ b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-call-CC-to-callcc/Makefile @@ -1,3 +1,3 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) include $(MAKEFILE_PATH)/../../Makefile -KOMPILE_FLAGS=--main-module CALLCC --gen-glr-bison-parser +KOMPILE_FLAGS=--main-module CALLCC diff --git a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile index a03350d91da..153fe239298 100644 --- a/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile +++ b/k-distribution/pl-tutorial/1_k/3_lambda++/lesson_1/exercises/from-callcc-to-call-CC/Makefile @@ -1,3 +1,3 @@ MAKEFILE_PATH := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) include $(MAKEFILE_PATH)/../callCC/Makefile -KOMPILE_FLAGS=--main-module CALLCC --syntax-module CALLCC-SYNTAX --gen-glr-bison-parser +KOMPILE_FLAGS=--main-module CALLCC --syntax-module CALLCC-SYNTAX diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile index 4f4b17d9efe..7af98e961c7 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_6/Makefile @@ -1,7 +1,7 @@ DEF=imp EXT=imp KRUN_FLAGS=--output none -KOMPILE_FLAGS=--gen-glr-bison-parser --enable-search +KOMPILE_FLAGS=--enable-search include ../../../find-k.mak include ${K_HOME}/include/kframework/ktest.mak diff --git a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete index bbf3736c545..e79cc27273f 100644 --- a/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete +++ b/k-distribution/pl-tutorial/1_k/4_imp++/lesson_7/Makefile.concrete @@ -3,7 +3,7 @@ DEF=imp DEFDIR=concrete KOMPILED=$(DEFDIR)/$(DEF)-kompiled EXT=imp -KOMPILE_FLAGS+=--gen-glr-bison-parser --enable-search +KOMPILE_FLAGS+=--enable-search KRUN_FLAGS=--output none include $(MAKEFILE_PATH)/../../../find-k.mak diff --git a/k-distribution/tests/regression-new/bison-glr-bug/Makefile b/k-distribution/tests/regression-new/bison-glr-bug/Makefile index 4d2832b4df9..f0da7ed86ca 100644 --- a/k-distribution/tests/regression-new/bison-glr-bug/Makefile +++ b/k-distribution/tests/regression-new/bison-glr-bug/Makefile @@ -1,7 +1,6 @@ DEF=iele EXT= TESTDIR=. -KOMPILE_FLAGS+=--gen-glr-bison-parser test: test.kore cat test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/bison-parser-library/Makefile b/k-distribution/tests/regression-new/bison-parser-library/Makefile index 0155c2b2269..a1bedb70688 100644 --- a/k-distribution/tests/regression-new/bison-parser-library/Makefile +++ b/k-distribution/tests/regression-new/bison-parser-library/Makefile @@ -1,7 +1,7 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=--syntax-module TEST --gen-glr-bison-parser --bison-parser-library --llvm-kompile-type c --llvm-kompile-output libfoo +KOMPILE_FLAGS=--syntax-module TEST --bison-parser-library --llvm-kompile-type c --llvm-kompile-output libfoo UNAME := $(shell uname) ifeq ($(UNAME),Darwin) diff --git a/k-distribution/tests/regression-new/glr/Makefile b/k-distribution/tests/regression-new/glr/Makefile index 7575505f6d1..9b398d719de 100644 --- a/k-distribution/tests/regression-new/glr/Makefile +++ b/k-distribution/tests/regression-new/glr/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=foo TESTDIR=. -KOMPILE_FLAGS+=--gen-glr-bison-parser test: test.kore $(KPRINT) test-kompiled test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/glr2/Makefile b/k-distribution/tests/regression-new/glr2/Makefile index 7575505f6d1..9b398d719de 100644 --- a/k-distribution/tests/regression-new/glr2/Makefile +++ b/k-distribution/tests/regression-new/glr2/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=foo TESTDIR=. -KOMPILE_FLAGS+=--gen-glr-bison-parser test: test.kore $(KPRINT) test-kompiled test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/glr3/Makefile b/k-distribution/tests/regression-new/glr3/Makefile index 7575505f6d1..9b398d719de 100644 --- a/k-distribution/tests/regression-new/glr3/Makefile +++ b/k-distribution/tests/regression-new/glr3/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=foo TESTDIR=. -KOMPILE_FLAGS+=--gen-glr-bison-parser test: test.kore $(KPRINT) test-kompiled test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/glr4/Makefile b/k-distribution/tests/regression-new/glr4/Makefile index 7575505f6d1..9b398d719de 100644 --- a/k-distribution/tests/regression-new/glr4/Makefile +++ b/k-distribution/tests/regression-new/glr4/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=foo TESTDIR=. -KOMPILE_FLAGS+=--gen-glr-bison-parser test: test.kore $(KPRINT) test-kompiled test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/imp++-llvm/Makefile b/k-distribution/tests/regression-new/imp++-llvm/Makefile index 53d4a1f6cd6..ba9be2373c2 100644 --- a/k-distribution/tests/regression-new/imp++-llvm/Makefile +++ b/k-distribution/tests/regression-new/imp++-llvm/Makefile @@ -2,7 +2,7 @@ DEF=imp EXT=imp TESTDIR=. KOMPILE_BACKEND=llvm -KOMPILE_FLAGS=--gen-glr-bison-parser --enable-search +KOMPILE_FLAGS=--enable-search KRUN_FLAGS=--search include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/issue-1572/Makefile b/k-distribution/tests/regression-new/issue-1572/Makefile index f1e1170ba95..3b59c03a3cc 100644 --- a/k-distribution/tests/regression-new/issue-1572/Makefile +++ b/k-distribution/tests/regression-new/issue-1572/Makefile @@ -1,3 +1,3 @@ -KOMPILE_FLAGS=-w2e -w all --gen-bison-parser +KOMPILE_FLAGS=-w2e -w all include ../../../include/kframework/ktest-fail.mak diff --git a/k-distribution/tests/regression-new/issue-1602/Makefile b/k-distribution/tests/regression-new/issue-1602/Makefile index 9915465f807..aea2c8504bf 100644 --- a/k-distribution/tests/regression-new/issue-1602/Makefile +++ b/k-distribution/tests/regression-new/issue-1602/Makefile @@ -1,7 +1,7 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS+=--gen-bison-parser --bison-stack-max-depth 12000 +KOMPILE_FLAGS+=--bison-stack-max-depth 12000 KRUN_FLAGS=--dry-run --no-expand-macros 1>/dev/null 2>/dev/null include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/llvm-krun/Makefile b/k-distribution/tests/regression-new/llvm-krun/Makefile index 5552e06f454..f011686d72a 100644 --- a/k-distribution/tests/regression-new/llvm-krun/Makefile +++ b/k-distribution/tests/regression-new/llvm-krun/Makefile @@ -1,6 +1,5 @@ DEF=test KOMPILE_BACKEND=llvm -KOMPILE_FLAGS+=--gen-glr-bison-parser CHECK=| diff - test.out LLVM_KRUN_FLAGS=-p -d ./test-kompiled diff --git a/k-distribution/tests/regression-new/locations/Makefile b/k-distribution/tests/regression-new/locations/Makefile index 7c00a581484..cb58e089af8 100644 --- a/k-distribution/tests/regression-new/locations/Makefile +++ b/k-distribution/tests/regression-new/locations/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=--gen-bison-parser KRUN_FLAGS=-o kore include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/locations2/Makefile b/k-distribution/tests/regression-new/locations2/Makefile index 7c00a581484..cb58e089af8 100644 --- a/k-distribution/tests/regression-new/locations2/Makefile +++ b/k-distribution/tests/regression-new/locations2/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=--gen-bison-parser KRUN_FLAGS=-o kore include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/locations3/Makefile b/k-distribution/tests/regression-new/locations3/Makefile index 37fdc9bbeaf..8216ed4a7bc 100644 --- a/k-distribution/tests/regression-new/locations3/Makefile +++ b/k-distribution/tests/regression-new/locations3/Makefile @@ -1,7 +1,7 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=--gen-bison-parser --bison-lists +KOMPILE_FLAGS=--bison-lists KRUN_FLAGS=-o kore include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/parse-c/Makefile b/k-distribution/tests/regression-new/parse-c/Makefile index 03d83c14195..6cb9aef5b86 100644 --- a/k-distribution/tests/regression-new/parse-c/Makefile +++ b/k-distribution/tests/regression-new/parse-c/Makefile @@ -1,7 +1,7 @@ DEF=c18-translation EXT=kc TESTDIR=. -KOMPILE_FLAGS+=--bison-lists --gen-glr-bison-parser +KOMPILE_FLAGS+=--bison-lists test: test.kore $(KPRINT) c18-translation-kompiled test.kore | diff - test.ref diff --git a/k-distribution/tests/regression-new/parseNonPgm/Makefile b/k-distribution/tests/regression-new/parseNonPgm/Makefile index 3b5e87a08da..b06e749b149 100644 --- a/k-distribution/tests/regression-new/parseNonPgm/Makefile +++ b/k-distribution/tests/regression-new/parseNonPgm/Makefile @@ -1,7 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS+=--gen-bison-parser KRUN_FLAGS+=print include ../../../include/kframework/ktest.mak From 1f5bb01c7c05080154aaf8a7311384b02b0a2884 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Jul 2021 10:34:49 -0500 Subject: [PATCH 02/14] add warning if user tries to create bison parser with no syntax, and fix crash --- .../tests/regression-new/nonexhaustive/Makefile | 2 +- .../main/java/org/kframework/parser/KRead.java | 17 ++++++++++++++++- .../utils/errorsystem/KException.java | 1 + 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/k-distribution/tests/regression-new/nonexhaustive/Makefile b/k-distribution/tests/regression-new/nonexhaustive/Makefile index a5e31ecb0ea..069e4376916 100644 --- a/k-distribution/tests/regression-new/nonexhaustive/Makefile +++ b/k-distribution/tests/regression-new/nonexhaustive/Makefile @@ -1,4 +1,4 @@ -KOMPILE_FLAGS=-w2e -w all -Wno useless-rule +KOMPILE_FLAGS=-w2e -w all -Wno useless-rule -Wno empty-parser KOMPILE_BACKEND=llvm include ../../../include/kframework/ktest-fail.mak diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index 6ed83e89188..63b3a396178 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -17,6 +17,7 @@ import org.kframework.utils.OS; import org.kframework.utils.Stopwatch; import org.kframework.utils.errorsystem.KEMException; +import org.kframework.utils.errorsystem.KException.ExceptionType; import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; @@ -76,9 +77,15 @@ public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledD } } + private static final String ERROR_FILE = "bison-error.txt"; + public void createBisonParser(Module mod, Sort sort, File outputFile, boolean glr, String bisonFile, long stackDepth, boolean library) { Stopwatch sw = new Stopwatch(globalOptions); try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, true, false, true, false, files)) { + if (!parseInModule.getParsingModule().productionsForSort().contains(sort.head())) { + kem.registerInnerParserWarning(ExceptionType.EMPTY_PARSER, "Trying to generate parser for sort " + sort + " in module " + mod.name() + " which has no terms; skipping."); + return; + } try (Scanner scanner = parseInModule.getScanner(kem.options)) { File scannerFile = files.resolveTemp("scanner.l"); File scanHdr = files.resolveTemp("scanner.h"); @@ -98,10 +105,18 @@ public void createBisonParser(Module mod, Sort sort, File outputFile, boolean gl .directory(files.resolveTemp(".")) .command("bison", "-d", "-Wno-other", "-Wno-conflicts-sr", "-Wno-conflicts-rr", parserFile.getAbsolutePath()) .inheritIO() + .redirectError(files.resolveTemp(ERROR_FILE)) .start() .waitFor(); if (exit != 0) { - throw KEMException.internalError("bison returned nonzero exit code: " + exit + "\n"); + String error = files.loadFromTemp(ERROR_FILE); + if (error.contains("start symbol top does not derive any sentence")) { + kem.registerInnerParserWarning(ExceptionType.EMPTY_PARSER, "Trying to generate parser for sort " + sort + " in module " + mod.name() + " which has no terms; skipping."); + return; + } else { + System.err.println(error); + throw KEMException.internalError("bison returned nonzero exit code: " + exit + "\n"); + } } List command = new ArrayList<>(); command.addAll(Arrays.asList( diff --git a/kore/src/main/java/org/kframework/utils/errorsystem/KException.java b/kore/src/main/java/org/kframework/utils/errorsystem/KException.java index 92d6aedc235..c1859b9a24d 100755 --- a/kore/src/main/java/org/kframework/utils/errorsystem/KException.java +++ b/kore/src/main/java/org/kframework/utils/errorsystem/KException.java @@ -124,6 +124,7 @@ public enum ExceptionType { REMOVED_ANYWHERE, DEPRECATED_DIRECTORY_FLAG, MISSING_HOOK, + EMPTY_PARSER, FIRST_HIDDEN, // warnings below here are hidden by default USELESS_RULE, UNRESOLVED_FUNCTION_SYMBOL, From 5c9ae42a24c7df8fb7ac661f70f3a300b0f2a487 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Jul 2021 10:35:26 -0500 Subject: [PATCH 03/14] bison parser as default --- kernel/src/main/java/org/kframework/kompile/Kompile.java | 6 +++--- .../main/java/org/kframework/kompile/KompileOptions.java | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 6c0f56f698b..a974f51eda7 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -191,12 +191,12 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String } CompiledDefinition def = new CompiledDefinition(kompileOptions, kompileOptions.outerParsing, kompileOptions.innerParsing, globalOptions, parsedDef, kompiledDefinition, files, kem, configInfo.getDefaultCell(rootCell).klabel()); - if (kompileOptions.genBisonParser || kompileOptions.genGlrBisonParser) { + if (!kompileOptions.jitParser || kompileOptions.lr1Parser) { if (def.configurationVariableDefaultSorts.containsKey("$PGM")) { String filename = getBisonParserFilename(def.programStartSymbol.name(), def.mainSyntaxModuleName()); File outputFile = files.resolveKompiled(filename); File linkFile = files.resolveKompiled("parser_PGM"); - new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(def.programParsingModuleFor(def.mainSyntaxModuleName(), kem).get(), def.programStartSymbol, outputFile, kompileOptions.genGlrBisonParser, kompileOptions.bisonFile, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary); + new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(def.programParsingModuleFor(def.mainSyntaxModuleName(), kem).get(), def.programStartSymbol, outputFile, !kompileOptions.lr1Parser, kompileOptions.bisonFile, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary); try { linkFile.delete(); Files.createSymbolicLink(linkFile.toPath(), files.resolveKompiled(".").toPath().relativize(outputFile.toPath())); @@ -222,7 +222,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String String filename = getBisonParserFilename(sort.name(), module); File outputFile = files.resolveKompiled(filename); File linkFile = files.resolveKompiled("parser_" + name); - new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(mod.get(), sort, outputFile, kompileOptions.genGlrBisonParser, null, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary); + new KRead(kem, files, InputModes.PROGRAM, globalOptions).createBisonParser(mod.get(), sort, outputFile, !kompileOptions.lr1Parser, null, kompileOptions.bisonStackMaxDepth, kompileOptions.genBisonParserLibrary); try { linkFile.delete(); Files.createSymbolicLink(linkFile.toPath(), files.resolveKompiled(".").toPath().relativize(outputFile.toPath())); diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index ba96c409fdd..9d6cd449e3f 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -113,11 +113,11 @@ public String syntaxModule(FileUtil files) { @Parameter(names="--emit-json", description="Emit JSON serialized version of parsed and kompiled definitions.") public boolean emitJson = false; - @Parameter(names="--gen-bison-parser", description="Emit bison parser for the PGM configuration variable within the syntax module of your definition into the kompiled definition.") - public boolean genBisonParser; + @Parameter(names="--lr1-parser", description="Emit LR(1) bison parser for the PGM configuration variable within the syntax module of your definition into the kompiled definition.") + public boolean lr1Parser; - @Parameter(names="--gen-glr-bison-parser", description="Emit GLR bison parser for the PGM configuration variable within the syntax module of your definition into the kompiled definition.") - public boolean genGlrBisonParser; + @Parameter(names="--jit-parser", description="Do not emit a GLR bison parser for the PGM configuration variable. Instead, use K's just-in-time parsing capabilities.") + public boolean jitParser; @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", descriptionKey = "file", hidden = true) public String bisonFile; From 85e40e8eede60cb184c1fd2939936494a7f67f71 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 5 May 2023 12:20:27 -0500 Subject: [PATCH 04/14] remove dead java backend code --- .../org/kframework/compile/checks/CheckAtt.java | 8 +++----- .../compile/checks/CheckConfigurationCells.java | 13 ++++--------- .../java/org/kframework/kompile/Kompile.java | 17 ++++------------- 3 files changed, 11 insertions(+), 27 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index b47da2a6b2c..c9d6ea8f383 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -32,13 +32,11 @@ public class CheckAtt { private final Set errors; private final KExceptionManager kem; private final Module m; - private final boolean isSymbolicKast; - public CheckAtt(Set errors, KExceptionManager kem, Module m, boolean isSymbolicKast) { + public CheckAtt(Set errors, KExceptionManager kem, Module m) { this.errors = errors; this.kem = kem; this.m = m; - this.isSymbolicKast = isSymbolicKast; this.macros = m.macroKLabels(); } @@ -95,7 +93,7 @@ private void checkRestrictedAtts(Sentence sentence) { private void check(Production prod) { if (!prod.sort().equals(Sorts.KItem())) { Att sortAtt = m.sortAttributesFor().getOrElse(prod.sort().head(), () -> Att.empty()); - if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array") && !(sortAtt.get(Att.HOOK()).equals("KVAR.KVar") && isSymbolicKast)) { + if (sortAtt.contains(Att.HOOK()) && !sortAtt.get(Att.HOOK()).equals("ARRAY.Array")) { if (!prod.att().contains(Att.FUNCTION()) && !prod.att().contains(Att.BRACKET()) && !prod.att().contains(Att.TOKEN()) && !prod.att().contains(Att.MACRO()) && !(prod.klabel().isDefined() && macros.contains(prod.klabel().get()))) { if (!(prod.sort().equals(Sorts.K()) && ((prod.klabel().isDefined() && (prod.klabel().get().name().equals("#EmptyK") || prod.klabel().get().name().equals("#KSequence"))) || prod.isSubsort()))) { @@ -106,7 +104,7 @@ private void check(Production prod) { } } } - if (prod.att().contains(Att.BINDER()) && !isSymbolicKast) { + if (prod.att().contains(Att.BINDER())) { if (!prod.att().get(Att.BINDER()).equals("")) { errors.add(KEMException.compilerError("Attribute value for 'binder' attribute is not supported.", prod)); } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java b/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java index 1b53ff61127..f5ae51c2d5e 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckConfigurationCells.java @@ -24,12 +24,9 @@ public class CheckConfigurationCells { private final Module module; - private final boolean isSymbolicKast; - - public CheckConfigurationCells(Set errors, Module module, boolean isSymbolicKast) { + public CheckConfigurationCells(Set errors, Module module) { this.errors = errors; this.module = module; - this.isSymbolicKast = isSymbolicKast; } public void check(Sentence s) { @@ -55,11 +52,9 @@ private void check(Production p) { } } if (p.att().getOptional(Att.MULTIPLICITY()).orElse("").equals("*") && p.att().getOptional(Att.TYPE()).orElse("Bag").equals("Bag")) { - if (!isSymbolicKast) { - errors.add(KEMException.compilerError("Cell bags are only supported on the Java backend. If you want " - + "this feature, comment on https://github.com/runtimeverification/k/issues/1419 . As a workaround, you can add the attribute " - + "type=\"Set\" and add a unique identifier to each element in the set.", p)); - } + errors.add(KEMException.compilerError("Cell bags are only supported on the Java backend. If you want " + + "this feature, comment on https://github.com/runtimeverification/k/issues/1419 . As a workaround, you can add the attribute " + + "type=\"Set\" and add a unique identifier to each element in the set.", p)); } } } diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index a974f51eda7..5a873ede64c 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -182,13 +182,7 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(kompiledDefinition.mainModule()); - boolean isKast = excludedModuleTags.contains(Att.KORE()); - Sort rootCell; - if (isKast) { - rootCell = configInfo.getRootCell(); - } else { - rootCell = Sorts.GeneratedTopCell(); - } + Sort rootCell = Sorts.GeneratedTopCell(); CompiledDefinition def = new CompiledDefinition(kompileOptions, kompileOptions.outerParsing, kompileOptions.innerParsing, globalOptions, parsedDef, kompiledDefinition, files, kem, configInfo.getDefaultCell(rootCell).klabel()); if (!kompileOptions.jitParser || kompileOptions.lr1Parser) { @@ -441,17 +435,16 @@ public void proverChecksX(Module specModule, Module mainDefModule) { public void structuralChecks(scala.collection.Set modules, Module mainModule, Option kModule, Set excludedModuleTags) { checkAnywhereRules(modules); boolean isSymbolic = excludedModuleTags.contains(Att.CONCRETE()); - boolean isKast = excludedModuleTags.contains(Att.KORE()); CheckRHSVariables checkRHSVariables = new CheckRHSVariables(errors, !isSymbolic, kompileOptions.backend); stream(modules).forEach(m -> stream(m.localSentences()).forEach(checkRHSVariables::check)); stream(modules).forEach(m -> { - CheckAtt checkAtt = new CheckAtt(errors, kem, m, isSymbolic && isKast); + CheckAtt checkAtt = new CheckAtt(errors, kem, m); checkAtt.checkUnrecognizedModuleAtts(); stream(m.localSentences()).forEach(checkAtt::check); }); - stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckConfigurationCells(errors, m, isSymbolic && isKast)::check)); + stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckConfigurationCells(errors, m)::check)); stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckSortTopUniqueness(errors, m)::check)); @@ -461,9 +454,7 @@ public void structuralChecks(scala.collection.Set modules, Module mainMo stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckHOLE(errors, m)::check)); - if (!(isSymbolic && isKast)) { // if it's not the java backend - stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check)); - } + stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckTokens(errors, m)::check)); stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckK(errors)::check)); From 4f54773fa43c77291c56cac7156d0fd4b0810255 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Jul 2021 10:49:59 -0500 Subject: [PATCH 05/14] fix bug in bison parser with ksequences in output --- .../parser/inner/kernel/KSyntax2Bison.java | 118 ++++++++++-------- 1 file changed, 69 insertions(+), 49 deletions(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java index a1690ef0b85..8a8f704f589 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java @@ -6,6 +6,7 @@ import org.kframework.Collections; import org.kframework.TopologicalSort; import org.kframework.attributes.Att; +import org.kframework.builtin.Sorts; import org.kframework.backend.kore.ModuleToKORE; import org.kframework.definition.Module; import org.kframework.definition.NonTerminal; @@ -396,60 +397,79 @@ private static void processProduction(Production prod, Module module, Module dis " node *n = malloc(sizeof(node) + sizeof(node *));\n" + " n->str = false;\n" + " n->location = @$;\n" + - " n->hasLocation = " + (hasLocation ? "1" : "0") + ";\n" + - " n->nchildren = 1;\n" + - " n->sort = \""); - encodeKore(prod.sort(), bison); - bison.append("\";\n" + - " if (!$1.nterm->str && strncmp($1.nterm->symbol, \"inj{\", 4) == 0) {\n" + - " char *childSort = $1.nterm->children[0]->sort;\n" + - " n->symbol = injSymbol(childSort, n->sort);\n" + - " n->children[0] = $1.nterm->children[0];\n" + - " } else {\n" + - " n->symbol = \"inj{"); - encodeKore(prod.getSubsortSort(), bison); - bison.append(", "); - encodeKore(prod.sort(), bison); - bison.append("}\";\n" + - " n->children[0] = $1.nterm;\n" + - " }\n"); - if (prod.att().contains(Att.USER_LIST_TERMINATOR())) { - KLabel nil = KLabel(prod.att().get(Att.USER_LIST_TERMINATOR())); - KLabel cons = KLabel(prod.att().get(Att.USER_LIST())); - bison.append( - " node *n2 = malloc(sizeof(node));\n" + - " n2->symbol = \""); - encodeKore(nil, bison); - bison.append("\";\n" + - " n2->str = false;\n" + - " n2->location = @$;\n" + - " n2->hasLocation = 0;\n" + - " n2->nchildren = 0;\n" + - " n2->sort = \""); + " n->hasLocation = " + (hasLocation ? "1" : "0") + ";\n"); + if (prod.sort().equals(Sorts.K()) && prod.getSubsortSort().equals(Sorts.KItem())) { + bison.append(" n->nchildren = 2;\n" + + " n->sort = \""); encodeKore(prod.sort(), bison); bison.append("\";\n" + - " node *n3 = malloc(sizeof(node) + 2*sizeof(node *));\n" + - " n3->symbol = \""); - encodeKore(cons, bison); - bison.append("\";\n" + - " n3->str = false;\n" + - " n3->location = @$;\n" + - " n3->hasLocation = " + (hasLocation ? "1" : "0") + ";\n" + - " n3->nchildren = 2;\n" + - " n3->children[0] = n2;\n" + - " n3->children[1] = $1.nterm;\n" + - " n3->sort = \""); + " n->symbol = \"kseq{}\";\n" + + " n->children[0] = $1.nterm;\n" + + " node *n2 = malloc(sizeof(node));\n" + + " n2->symbol = \"dotk{}\";\n" + + " n2->str = false;\n" + + " n2->location = @$;\n" + + " n2->hasLocation = false;\n" + + " n2->nchildren = 0;\n" + + " n2->sort = \"SortK{}\";\n" + + " n->children[1] = n2;\n" + + " value_type result = {.nterm = n};\n" + + " $$ = result;\n" + + "}\n"); + } else { + bison.append(" n->nchildren = 1;\n" + + " n->sort = \""); encodeKore(prod.sort(), bison); bison.append("\";\n" + - " value_type result = {.nterm = n3};\n" + - " $$ = result;\n" + - "}\n"); - } else { - bison.append(" value_type result = {.nterm = n};\n" + - " $$ = result;\n" + - "}\n"); + " if (!$1.nterm->str && strncmp($1.nterm->symbol, \"inj{\", 4) == 0) {\n" + + " char *childSort = $1.nterm->children[0]->sort;\n" + + " n->symbol = injSymbol(childSort, n->sort);\n" + + " n->children[0] = $1.nterm->children[0];\n" + + " } else {\n" + + " n->symbol = \"inj{"); + encodeKore(prod.getSubsortSort(), bison); + bison.append(", "); + encodeKore(prod.sort(), bison); + bison.append("}\";\n" + + " n->children[0] = $1.nterm;\n" + + " }\n"); + if (prod.att().contains(Att.USER_LIST_TERMINATOR())) { + KLabel nil = KLabel(prod.att().get(Att.USER_LIST_TERMINATOR())); + KLabel cons = KLabel(prod.att().get(Att.USER_LIST())); + bison.append( + " node *n2 = malloc(sizeof(node));\n" + + " n2->symbol = \""); + encodeKore(nil, bison); + bison.append("\";\n" + + " n2->str = false;\n" + + " n2->location = @$;\n" + + " n2->hasLocation = 0;\n" + + " n2->nchildren = 0;\n" + + " n2->sort = \""); + encodeKore(prod.sort(), bison); + bison.append("\";\n" + + " node *n3 = malloc(sizeof(node) + 2*sizeof(node *));\n" + + " n3->symbol = \""); + encodeKore(cons, bison); + bison.append("\";\n" + + " n3->str = false;\n" + + " n3->location = @$;\n" + + " n3->hasLocation = " + (hasLocation ? "1" : "0") + ";\n" + + " n3->nchildren = 2;\n" + + " n3->children[0] = n2;\n" + + " n3->children[1] = $1.nterm;\n" + + " n3->sort = \""); + encodeKore(prod.getSort(), bison); + bison.append("\";\n" + + " value_type result = {.nterm = n3};\n" + + " $$ = result;\n" + + "}\n"); + } else { + bison.append(" value_type result = {.nterm = n};\n" + + " $$ = result;\n" + + "}\n"); + } } - } else if (prod.att().contains(Att.TOKEN()) && prod.isSubsort()) { bison.append("{\n" + " node *n = malloc(sizeof(node) + sizeof(node *));\n" + From 5a0dbd85fb4e9e29baa32d0694895891349c7c0b Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 7 Jul 2021 10:50:12 -0500 Subject: [PATCH 06/14] disable warnings that should be ignored --- k-distribution/tests/regression-new/amb-rew/Makefile | 2 +- k-distribution/tests/regression-new/equals-pattern/Makefile | 2 +- k-distribution/tests/regression-new/issue-1384/Makefile | 2 +- k-distribution/tests/regression-new/prelude-warnings/Makefile | 2 +- k-distribution/tests/regression-new/werrorCategory/Makefile | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/k-distribution/tests/regression-new/amb-rew/Makefile b/k-distribution/tests/regression-new/amb-rew/Makefile index 5993a6b4b08..0a0458ba35e 100644 --- a/k-distribution/tests/regression-new/amb-rew/Makefile +++ b/k-distribution/tests/regression-new/amb-rew/Makefile @@ -1,6 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=-w2e +KOMPILE_FLAGS=-w2e -Wno empty-parser include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/equals-pattern/Makefile b/k-distribution/tests/regression-new/equals-pattern/Makefile index 90915e9a9dc..593b9c0e6c0 100644 --- a/k-distribution/tests/regression-new/equals-pattern/Makefile +++ b/k-distribution/tests/regression-new/equals-pattern/Makefile @@ -2,6 +2,6 @@ DEF=test EXT=test TESTDIR=. KOMPILE_BACKEND?=llvm -KOMPILE_FLAGS=-w2e +KOMPILE_FLAGS=-w2e -Wno non-lr-grammar include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/issue-1384/Makefile b/k-distribution/tests/regression-new/issue-1384/Makefile index 9970931a789..2f7665ed817 100644 --- a/k-distribution/tests/regression-new/issue-1384/Makefile +++ b/k-distribution/tests/regression-new/issue-1384/Makefile @@ -2,6 +2,6 @@ DEF=test EXT=test TESTDIR=. KOMPILE_BACKEND=llvm -KOMPILE_FLAGS=-w2e +KOMPILE_FLAGS=-w2e -Wno empty-parser include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/prelude-warnings/Makefile b/k-distribution/tests/regression-new/prelude-warnings/Makefile index 22d6c494f8b..bcbf329fbe9 100644 --- a/k-distribution/tests/regression-new/prelude-warnings/Makefile +++ b/k-distribution/tests/regression-new/prelude-warnings/Makefile @@ -1,6 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=-w all -w2e +KOMPILE_FLAGS=-w all -w2e -Wno empty-parser include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/werrorCategory/Makefile b/k-distribution/tests/regression-new/werrorCategory/Makefile index fe26dc51e36..fee7f45d474 100644 --- a/k-distribution/tests/regression-new/werrorCategory/Makefile +++ b/k-distribution/tests/regression-new/werrorCategory/Makefile @@ -1,6 +1,6 @@ DEF=test EXT=test TESTDIR=. -KOMPILE_FLAGS=-w2e -Wno missing-syntax-module +KOMPILE_FLAGS=-w2e -Wno missing-syntax-module -Wno non-lr-grammar include ../../../include/kframework/ktest.mak From 0c876bfcaed81e6df91ff77e39c8dd272dd93993 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 17 Oct 2023 13:18:14 -0500 Subject: [PATCH 07/14] fix compile error --- .../java/org/kframework/parser/inner/kernel/KSyntax2Bison.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java index 8a8f704f589..fc31d527294 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java @@ -459,7 +459,7 @@ private static void processProduction(Production prod, Module module, Module dis " n3->children[0] = n2;\n" + " n3->children[1] = $1.nterm;\n" + " n3->sort = \""); - encodeKore(prod.getSort(), bison); + encodeKore(prod.sort(), bison); bison.append("\";\n" + " value_type result = {.nterm = n3};\n" + " $$ = result;\n" + From 52817dc4dcc4458916013653d7af1f52736928cd Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 20 Oct 2023 10:44:39 -0500 Subject: [PATCH 08/14] fix output file --- k-distribution/tests/regression-new/append/1.test.kparse.out | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/k-distribution/tests/regression-new/append/1.test.kparse.out b/k-distribution/tests/regression-new/append/1.test.kparse.out index 8ade6ae5038..8582901a335 100644 --- a/k-distribution/tests/regression-new/append/1.test.kparse.out +++ b/k-distribution/tests/regression-new/append/1.test.kparse.out @@ -1 +1,2 @@ -\dv{SortInt{}}("1")\dv{SortInt{}}("1") \ No newline at end of file +\dv{SortInt{}}("1") +\dv{SortInt{}}("1") From 11356770adafceceebc408325bcb69548f2aadc7 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 20 Oct 2023 12:03:35 -0500 Subject: [PATCH 09/14] fix warning --- k-distribution/tests/regression-new/checkWarns/missingKlabel.k | 2 ++ 1 file changed, 2 insertions(+) diff --git a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k index ca6228824c2..4e5552ee079 100644 --- a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k +++ b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k @@ -14,4 +14,6 @@ module MISSINGKLABEL , unit(.MyMap), element(_M|->_), index(0), format(%1%n%2), unused ] + syntax KItem ::= "foo" [unused] + endmodule From 7f3fcd5a2e58a7de0bc2403fbb3813c110bb300d Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 20 Oct 2023 12:32:59 -0500 Subject: [PATCH 10/14] fix bug in fix for parser warning --- k-distribution/tests/regression-new/checkWarns/missingKlabel.k | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k index 4e5552ee079..ef759b90568 100644 --- a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k +++ b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k @@ -1,5 +1,6 @@ // Copyright (c) K Team. All Rights Reserved. module MISSINGKLABEL-SYNTAX + syntax KItem ::= "foo" [unused] endmodule module MISSINGKLABEL @@ -14,6 +15,4 @@ module MISSINGKLABEL , unit(.MyMap), element(_M|->_), index(0), format(%1%n%2), unused ] - syntax KItem ::= "foo" [unused] - endmodule From 85d97ad1ebf05ce89b942424edbf9ba850d4e8be Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Fri, 20 Oct 2023 13:57:22 -0500 Subject: [PATCH 11/14] fix test output --- k-distribution/tests/regression-new/issue-1572/test.k | 2 ++ 1 file changed, 2 insertions(+) diff --git a/k-distribution/tests/regression-new/issue-1572/test.k b/k-distribution/tests/regression-new/issue-1572/test.k index 10b0464c81e..df496ac6dc7 100644 --- a/k-distribution/tests/regression-new/issue-1572/test.k +++ b/k-distribution/tests/regression-new/issue-1572/test.k @@ -2,6 +2,8 @@ module TEST-SYNTAX imports ML-SYNTAX + syntax KItem ::= "foo" [unused] + endmodule module TEST From 4b45a2f0ed2caa22d0a982ecc7293f27be3e3b9f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 24 Oct 2023 16:10:54 -0500 Subject: [PATCH 12/14] don't use bison to build elrond parser --- k-distribution/tests/profiling/elrond-semantics/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/profiling/elrond-semantics/Makefile b/k-distribution/tests/profiling/elrond-semantics/Makefile index fce6db53b7d..d9712f17f48 100644 --- a/k-distribution/tests/profiling/elrond-semantics/Makefile +++ b/k-distribution/tests/profiling/elrond-semantics/Makefile @@ -4,6 +4,6 @@ ITER=1 TESTDIR=. KOMPILE_BACKEND=llvm BENCHMARK_NAME=ELROND-SEMANTICS -KOMPILE_FLAGS=--main-module MANDOS --syntax-module MANDOS-SYNTAX +KOMPILE_FLAGS=--main-module MANDOS --syntax-module MANDOS-SYNTAX --jit-parser include ../kprofiling.mak From ff239bd589c5a3305d3d85957c4a0dea90a6c22e Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 25 Oct 2023 10:32:55 -0500 Subject: [PATCH 13/14] Update Makefile --- k-distribution/tests/profiling/evm-semantics/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/profiling/evm-semantics/Makefile b/k-distribution/tests/profiling/evm-semantics/Makefile index 5a3f8e21825..21a063ece09 100644 --- a/k-distribution/tests/profiling/evm-semantics/Makefile +++ b/k-distribution/tests/profiling/evm-semantics/Makefile @@ -4,6 +4,6 @@ ITER=1 TESTDIR=. KOMPILE_BACKEND=llvm BENCHMARK_NAME=EVM-SEMANTICS -KOMPILE_FLAGS=--main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION +KOMPILE_FLAGS=--main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION --jit-parser include ../kprofiling.mak From d128f0c83f8f8e8521eda81717e1be64719e27fa Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 25 Oct 2023 14:19:43 -0500 Subject: [PATCH 14/14] disable bison on wasm --- k-distribution/tests/profiling/wasm-semantics/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/profiling/wasm-semantics/Makefile b/k-distribution/tests/profiling/wasm-semantics/Makefile index 5f003664b65..b64d3ba866c 100644 --- a/k-distribution/tests/profiling/wasm-semantics/Makefile +++ b/k-distribution/tests/profiling/wasm-semantics/Makefile @@ -4,6 +4,6 @@ ITER=1 TESTDIR=. KOMPILE_BACKEND=llvm BENCHMARK_NAME=WASM-SEMANTICS -KOMPILE_FLAGS=--main-module WASM-TEST --syntax-module WASM-TEST-SYNTAX +KOMPILE_FLAGS=--main-module WASM-TEST --syntax-module WASM-TEST-SYNTAX --jit-parser include ../kprofiling.mak