Merge branch 'master' into map-input-names

.github/workflows/Dockerfile

@@ -65,6 +65,7 @@ RUN    apt-get update              \
         python3-dev                \
         python3-distutils          \
         python3-pip                \
+        xxd                        \
         zlib1g-dev
 
 COPY --from=Z3 /usr/bin/z3 /usr/bin/z3

README.md

@@ -104,6 +104,7 @@ The following dependencies are needed either at build time or runtime:
 *   [pkg-config](https://www.freedesktop.org/wiki/Software/pkg-config/)
 *   [python](https://www.python.org)
 *   [stack](https://docs.haskellstack.org/en/stable/README/)
+*   [xxd](https://github.com/vim/vim/blob/master/runtime/doc/xxd.man)
 *   [zlib](https://www.zlib.net/)
 *   [z3](https://github.com/Z3Prover/z3) (on some distributions libz3 is also
     needed and packaged separately) Note that you need version 4.12.1 of Z3,

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.58
+v0.1.76

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.69
+0.1.81

deps/z3

@@ -1 +1 @@
-4.12.1
+4.13.0

flake.nix

@@ -1,9 +1,9 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.81";
     haskell-backend = {
-      url = "github:runtimeverification/haskell-backend/v0.1.58";
+      url = "github:runtimeverification/haskell-backend/v0.1.76";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";
       inputs.nixpkgs.follows = "llvm-backend/nixpkgs";
     };

install-build-deps

@@ -34,6 +34,7 @@ inst_Debian() {
         pkg-config              \
         python3                 \
         python3-dev             \
+        xxd                     \
         z3                      \
         zlib1g-dev
 

install-k

@@ -1,6 +1,6 @@
 #!/bin/sh -e
 
-K_VERSION=7.1.0
+K_VERSION=7.1.117
 
 if [ `id -u` -ne 0 ]; then
   echo "$0: error: This script must be run as root."

k-distribution/include/kframework/builtin/domains.md

@@ -3015,6 +3015,7 @@ than the input.
 
 ```k
   syntax {Width1, Width2} MInt{Width1} ::= roundMInt(MInt{Width2}) [function, total, hook(MINT.round)]
+  syntax {Width1, Width2} MInt{Width1} ::= signExtendMInt(MInt{Width2}) [function, total, hook(MINT.sext)]
 ```
 
 ```k

k-distribution/tests/regression-new/mint-llvm-3/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/mint-llvm-3/test.k

@@ -0,0 +1,19 @@
+module TEST
+  imports BOOL
+  imports MINT
+
+  syntax MInt{64}
+  syntax MInt{32}
+
+  syntax KItem ::= foo(MInt{64})
+
+  syntax MInt{64} ::= m64() [function]
+  rule m64() => 0p64
+  syntax MInt{32} ::= m32() [function]
+  rule m32() => 0p32
+
+  rule foo(X) => .K
+    requires (X +MInt m64()) <=uMInt (roundMInt(m32()) <<MInt 0p64)
+
+  rule true => foo(0p64)
+endmodule

k-frontend/src/main/java/org/kframework/compile/AddSortInjections.java

@@ -501,7 +501,9 @@ private static Sort lub(
         s ->
             mod.subsorts().lessThanEq(s, Sorts.KBott())
                 || mod.subsorts().greaterThan(s, Sorts.K()));
-    if (expectedSort != null && !expectedSort.name().equals(SORTPARAM_NAME)) {
+    if (expectedSort != null
+        && expectedSort.head().params() == 0
+        && !expectedSort.name().equals(SORTPARAM_NAME)) {
       bounds.removeIf(s -> !mod.subsorts().lessThanEq(s, expectedSort));
     }
 

k-frontend/src/main/java/org/kframework/compile/ResolveFun.java

@@ -214,7 +214,7 @@ private List<KVariable> closure(K k) {
     List<KVariable> result = new ArrayList<>();
     new GatherVarsVisitor(true, errors, vars, false).apply(k);
     new ComputeUnboundVariables(true, true, errors, vars, result::add).apply(k);
-    return result;
+    return result.stream().distinct().collect(Collectors.toList());
   }
 
   private Production funProd(KLabel fun, K k, Sort arg, boolean total) {

k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java

@@ -60,6 +60,7 @@ private void checkRule(Rule rule) {
     checkNonExecutable(rule);
     checkSimplification(rule);
     checkSymbolic(rule);
+    checkSyntactic(rule);
   }
 
   private void checkProduction(Production prod) {
@@ -151,6 +152,14 @@ private void checkSymbolic(Rule rule) {
     }
   }
 
+  private void checkSyntactic(Rule rule) {
+    if (rule.att().contains(Att.SYNTACTIC()) && !rule.att().contains(Att.SIMPLIFICATION())) {
+      errors.add(
+          KEMException.compilerError(
+              "syntactic attribute is only supported on simplification rules."));
+    }
+  }
+
   private void checkHookedSortConstructors(Production prod) {
     if (prod.sort().equals(Sorts.KItem())) {
       return;

k-frontend/src/main/java/org/kframework/kil/UserList.java

@@ -18,13 +18,13 @@ public class UserList extends ProductionItem {
 
   public UserList(Sort sort, String separator) {
     this.sort = sort;
-    this.separator = separator.trim();
+    this.separator = separator;
     this.listType = ZERO_OR_MORE;
   }
 
   public UserList(Sort sort, String separator, String listType) {
     this.sort = sort;
-    this.separator = separator.trim();
+    this.separator = separator;
     this.listType = listType;
   }
 
@@ -58,7 +58,7 @@ public String getSeparator() {
   }
 
   public void setSeparator(String separator) {
-    this.separator = separator.trim();
+    this.separator = separator;
   }
 
   @Override

k-frontend/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -429,15 +429,6 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
         stream(mod.allSorts())
             .filter(s -> (!isParserSort(s) || s.equals(Sorts.KItem()) || s.equals(Sorts.K())))
             .toList();
-    for (SortHead sh : mutable(mod.definedInstantiations()).keySet()) {
-      for (Sort s : mutable(mod.definedInstantiations().apply(sh))) {
-        // syntax MInt{K} ::= MInt{6}
-        Production p1 =
-            Production(
-                Option.empty(), Seq(), Sort(s.name(), Sorts.K()), Seq(NonTerminal(s)), Att.empty());
-        prods.add(p1);
-      }
-    }
     for (Production p : iterable(mod.productions())) {
       if (p.params().nonEmpty()) {
         if (p.params().contains(p.sort())) { // case 1
@@ -634,6 +625,17 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
     }
 
     disambProds = new HashSet<>(parseProds);
+
+    for (SortHead sh : mutable(mod.definedInstantiations()).keySet()) {
+      for (Sort s : mutable(mod.definedInstantiations().apply(sh))) {
+        // syntax MInt{K} ::= MInt{6}
+        Production p1 =
+            Production(
+                Option.empty(), Seq(), Sort(s.name(), Sorts.K()), Seq(NonTerminal(s)), Att.empty());
+        parseProds.add(p1);
+      }
+    }
+
     if (mod.importedModuleNames().contains(PROGRAM_LISTS)) {
       Set<Sentence> prods3 = new HashSet<>();
       // if no start symbol has been defined in the configuration, then use K

k-frontend/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java

@@ -230,7 +230,7 @@ public Either<Set<KEMException>, Term> apply(Term term) {
           return typeError(pr, expectedSort, inferred);
         }
         // well typed, so add a cast and return
-        return wrapTermWithCast((Constant) pr, inferred);
+        return wrapTermWithCast(pr, inferred);
       }
       // compute the instantiated production with its sort parameters
       Production substituted = pr.production().substitute(inferencer.getArgs(pr));
@@ -275,12 +275,26 @@ public Either<Set<KEMException>, Term> apply(Term term) {
             j++;
           }
         }
+        if (pr.production().params().nonEmpty() && hasParametricSort(pr.production())) {
+          return wrapTermWithCast(tc, substituted.sort());
+        }
         return Right.apply(tc);
       }
       return Right.apply(pr);
     }
 
-    private Either<Set<KEMException>, Term> wrapTermWithCast(Constant c, Sort declared) {
+    private boolean hasParametricSort(Production prod) {
+      if (prod.sort().head().params() != 0) {
+        return true;
+      }
+      if (stream(prod.nonterminals()).anyMatch(nt -> nt.sort().head().params() != 0)) {
+        return true;
+      }
+      return false;
+    }
+
+    private Either<Set<KEMException>, Term> wrapTermWithCast(
+        ProductionReference pr, Sort declared) {
       if (castContext != CastContext.SEMANTIC) {
         // There isn't an existing :Sort, so add one
         Production cast =
@@ -289,9 +303,10 @@ private Either<Set<KEMException>, Term> wrapTermWithCast(Constant c, Sort declar
                 .productionsFor()
                 .apply(KLabel("#SemanticCastTo" + declared.toString()))
                 .head();
-        return Right.apply(TermCons.apply(ConsPStack.singleton(c), cast, c.location(), c.source()));
+        return Right.apply(
+            TermCons.apply(ConsPStack.singleton(pr), cast, pr.location(), pr.source()));
       }
-      return Right.apply(c);
+      return Right.apply(pr);
     }
   }
 }

k-frontend/src/main/scala/org/kframework/attributes/Att.scala

@@ -416,6 +416,8 @@ object Att {
       onlyon3[Module, Production, Rule],
       KeyRange.WholePipeline
     )
+  final val SYNTACTIC =
+    Key.builtin("syntactic", KeyParameter.Required, onlyon[Rule], KeyRange.WholePipeline)
   final val TOKEN = Key.builtin(
     "token",
     KeyParameter.Forbidden,

package/debian/kframework/changelog

@@ -1,4 +1,4 @@
-kframework (7.1.0) unstable; urgency=medium
+kframework (7.1.117) unstable; urgency=medium
 
   * Initial Release.
 

package/debian/kframework/control.jammy

@@ -2,7 +2,7 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <dwight.guth@runtimeverification.com>
-Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
+Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , xxd , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 

package/version

@@ -1 +1 @@
-7.1.0
+7.1.117

pyk/.gitignore

@@ -10,3 +10,6 @@ __pycache__/
 
 .kprove*
 *.debug-log
+
+.idea/
+.DS_Store

pyk/docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '7.1.0'
-release = '7.1.0'
+version = '7.1.117'
+release = '7.1.117'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kframework"
-version = "7.1.0"
+version = "7.1.117"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-__version__: Final = '7.1.0'
+__version__: Final = '7.1.117'

pyk/src/pyk/cli/pyk.py

@@ -320,6 +320,7 @@ class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions):
     kore_rpc_command: str | Iterable[str] | None
     max_depth: int | None
     max_iterations: int | None
+    assume_defined: bool
     show_kcfg: bool
 
     @staticmethod
@@ -331,6 +332,7 @@ def default() -> dict[str, Any]:
             'kore_rpc_command': None,
             'max_depth': None,
             'max_iterations': None,
+            'assume_defined': False,
             'show_kcfg': False,
         }