Merge branch 'develop' into hotfix/maven-release-push

docs/ktools.md

@@ -366,3 +366,21 @@ This is the line of `definition.kore` that the axiom appears on as
 well as the original location of the rule in the K semantics. You can
 use this information to figure out which rules and functions are
 causing the most time and optimize them to be more efficient.
+
+Running tests - kserver
+--------------------------
+
+The `kserver` is a front-end tool based on [Nailgun](https://github.com/facebookarchive/nailgun)
+which helps to reduce the startup time of the JVM. Calling `kserver` in a terminal
+window will wait for all kompile/kprove calls and force them to run in the same process
+and share the same threads. This also reduces the thread contention significantly. `kompile`
+uses all the threads available to do rule parsing. Another benefit is that it saves caches,
+and each time you call kprove/kast, you can access those directly w/o extra disk usage.
+Running the `regression-new` integration tests on a powerful machine (32 threads) takes 8m,
+with the kserver active it takes 2m. You can start the kserver in two ways.
+- blocking: call `kserver` in the command line. Close it after you are done testing. Useful for quick testing.
+- non-blocking: call `spawn-kserver <log.flie>` and close it with `stop-kserver` - this is used for automation on CI
+
+Because we reuse caches, you should stop and restart the server between runs.
+The Nailgun implementation hasn't been updated in the last 3-5 years, and it's not compatible with Java 18 onwards.
+

docs/user_manual.md

@@ -1663,24 +1663,27 @@ For example:
 
 ```k
 syntax AExp ::= Int
-              | AExp "+" AExp [strict]
+              | AExp "+" AExp [strict, klabel(addExp)]
 ```
 
 This generates two heating rules (where the hole syntaxes `"[]" "+" AExp` and
 `AExp "+" "[]"` is automatically added to create an evaluation context):
 
 ```k
-rule <k> HOLE:AExp +  AE2:AExp => HOLE ~>  [] + AE2 ... </k> [heat]
-rule <k>  AE1:AExp + HOLE:AExp => HOLE ~> AE1 +  [] ... </k> [heat]
+rule [addExp1-heat]: <k> HOLE:AExp +  AE2:AExp => HOLE ~>  [] + AE2 ... </k> [heat]
+rule [addExp2-heat]: <k>  AE1:AExp + HOLE:AExp => HOLE ~> AE1 +  [] ... </k> [heat]
 ```
 
 And two corresponding cooling rules:
 
 ```k
-rule <k> HOLE:AExp ~>  [] + AE2 => HOLE +  AE2 ... </k> [cool]
-rule <k> HOLE:AExp ~> AE1 +  [] =>  AE1 + HOLE ... </k> [cool]
+rule [addExp1-cool]: <k> HOLE:AExp ~>  [] + AE2 => HOLE +  AE2 ... </k> [cool]
+rule [addExp2-cool]: <k> HOLE:AExp ~> AE1 +  [] =>  AE1 + HOLE ... </k> [cool]
 ```
 
+Note that the rules are given labels based on the klabel of the production, which
+nonterminal is the hole, and whether it's the heating or the cooling rule.
+
 You will note that these rules can apply one after another infinitely. In
 practice, the `KResult` sort is used to break this cycle by ensuring that only
 terms that are not part of the `KResult` sort will be heated. The `heat` and
@@ -1766,10 +1769,10 @@ unnecessarily verbose to write heating and cooling rules directly.
 
 For example, if the user wants to heat a term if it exists under a `foo`
 constructor if the term to be heated is of sort `bar`, one might write the
-following context:
+following context (with the optional label):
 
 ```k
-context foo(HOLE:Bar)
+context [foo]: foo(HOLE:Bar)
 ```
 
 Once again, note that `HOLE` is just a variable, but one that has special
@@ -1779,8 +1782,8 @@ be heated or cooled.
 This will automatically generate the following sentences:
 
 ```k
-rule <k> foo(HOLE:Bar) => HOLE ~> foo([]) ... </k> [heat]
-rule <k> HOLE:Bar ~> foo([]) => foo(HOLE) ... </k> [cool]
+rule [foo-heat]: <k> foo(HOLE:Bar) => HOLE ~> foo([]) ... </k> [heat]
+rule [foo-cool]: <k> HOLE:Bar ~> foo([]) => foo(HOLE) ... </k> [cool]
 ```
 
 The user may also write the K cell explicitly in the context declaration

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

@@ -348,7 +348,7 @@ private RewriterResult executeKoreCommands(Module rules, String[] koreCommand,
 
             @Override
             public RewriterResult prove(Module rules, Boolean reuseDef) {
-                Module kompiledModule = KoreBackend.getKompiledModule(module, true, kompileOptions);
+                Module kompiledModule = KoreBackend.getKompiledModule(module, true);
                 ModuleToKORE converter = new ModuleToKORE(kompiledModule, def.topCellInitializer, kompileOptions, kem);
                 String defPath = reuseDef ? files.resolveKompiled("definition.kore").getAbsolutePath() : saveKoreDefinitionToTemp(converter);
                 String specPath = saveKoreSpecToTemp(converter, rules);

k-distribution/tests/regression-new/checks/duplicateContextLabels.k

@@ -0,0 +1,14 @@
+// Copyright (c) K Team. All Rights Reserved.
+module DUPLICATECONTEXTLABELS
+  imports INT
+
+  syntax KResult ::= Int
+  syntax A ::= "a"
+             | foo( A, A )
+
+  context [foo-left]:  foo( HOLE,    _ )
+  context [foo-right]: foo(    _, HOLE )
+
+  rule [foo-left-cool]: a => 1
+
+endmodule

k-distribution/tests/regression-new/checks/duplicateContextLabels.k.out

@@ -0,0 +1,5 @@
+[Error] Compiler: The generated label for a context rule conflicts with a user-defined label at Source(duplicateContextLabels.k) and Location(12,25,12,31). Please consider renaming.
+	Source(duplicateContextLabels.k)
+	Location(9,24,9,41)
+	9 |	  context [foo-left]:  foo( HOLE,    _ )
+	  .	                       ^~~~~~~~~~~~~~~~~

k-distribution/tests/regression-new/checks/freshConfig.k

@@ -0,0 +1,19 @@
+// Copyright (c) K Team. All Rights Reserved.
+module FRESHCONFIG-SYNTAX
+endmodule
+
+module FRESHCONFIG
+  imports INT
+
+  syntax Foo ::= foo(Int)
+
+  syntax Foo ::= freshFoo(Int)    [freshGenerator, function, total]
+  rule freshFoo(I:Int) => foo(I)
+
+configuration
+  <k> $PGM:Int </k>
+  <freshFoo> !_:Foo </freshFoo>
+
+  rule 0 => !_:Foo
+
+endmodule

k-distribution/tests/regression-new/checks/freshConfig.k.out

@@ -0,0 +1,6 @@
+[Error] Compiler: Can't resolve fresh configuration variable not of sort Int
+  while executing phase "Resolve fresh variables in cell initializers"
+	Source(freshConfig.k)
+	Location(15,14,15,16)
+	15 |	  <freshFoo> !_:Foo </freshFoo>
+	   .	             ^~

k-distribution/tests/regression-new/context-labels/Makefile

@@ -0,0 +1,27 @@
+DEF=context
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+KPROVE_FLAGS+=--debugger --debug-script context-spec.k.in
+KORE_REPL_OPTS=--log-entries DebugAppliedLabeledRewriteRule
+export KORE_REPL_OPTS
+CONSIDER_PROVER_ERRORS=2>&1 | sed 's!\[[0-9]\+]!!g' # Hacking in a sed command here to remove strings of the form '[23452]'
+
+include ../../../include/kframework/ktest.mak
+
+K_RULE_FIND=${K_BIN}/k-rule-find
+
+FIND_RULES_TESTS?=$(wildcard $(TESTDIR)/*.find-rule)
+
+.PHONY: find-rules
+
+all: find-rules
+
+find-rules: $(FIND_RULES_TESTS)
+
+%.find-rule: kompile
+ifeq ($(TESTDIR),$(RESULTDIR))
+	$(K_RULE_FIND) $(KOMPILED_DIR) $(shell cat $@) $(CHECK) $@.out
+else
+	$(K_RULE_FIND) $(KOMPILED_DIR) $(shell cat $@) $(CHECK) $(RESULTDIR)/$(notdir $@).out
+endif
+

k-distribution/tests/regression-new/context-labels/barlabel.find-rule

@@ -0,0 +1 @@
+context.k:12

k-distribution/tests/regression-new/context-labels/barlabel.find-rule.out

@@ -0,0 +1 @@
+CONTEXT.bar1-heat

k-distribution/tests/regression-new/context-labels/bazlabel.find-rule

@@ -0,0 +1 @@
+context.k:10

k-distribution/tests/regression-new/context-labels/bazlabel.find-rule.out

@@ -0,0 +1 @@
+CONTEXT.baz2-heat

k-distribution/tests/regression-new/context-labels/context-spec.k

@@ -0,0 +1,13 @@
+// Copyright (c) K Team. All Rights Reserved.
+requires "context.k"
+
+module CONTEXT-SPEC
+  imports CONTEXT
+
+  claim <k> foo( a, a ) => foo( 0, 0 ) ... </k>
+
+  claim <k> bar( a, a ) => bar( 0, 0 ) ... </k>
+
+  claim <k> baz( a, a ) => baz( a, 0 ) ... </k>
+
+endmodule

k-distribution/tests/regression-new/context-labels/context-spec.k.in

@@ -0,0 +1,22 @@
+prove 0
+ktryf CONTEXT.foo1-heat
+step
+ktryf CONTEXT.foo1-cool
+ktryf CONTEXT.foo2-heat
+step
+ktryf CONTEXT.foo2-cool
+step
+prove 1
+ktryf CONTEXT.bar1-heat
+step
+ktryf CONTEXT.bar1-cool
+ktryf CONTEXT.bar2-heat
+step
+ktryf CONTEXT.bar2-cool
+step
+prove 2
+ktryf CONTEXT.baz2-heat
+step
+ktryf CONTEXT.baz2-cool
+step
+exit