Merge branch 'develop' into _update-deps/runtimeverification/haskell-…

…backend

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.75
+0.1.77

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.75";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.77";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.63";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

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

pyk/src/pyk/cterm/symbolic.py

@@ -73,18 +73,21 @@ def __init__(self, message: str):
 class CTermSymbolic:
     _kore_client: KoreClient
     _definition: KDefinition
-    _trace_rewrites: bool
+    _log_succ_rewrites: bool
+    _log_fail_rewrites: bool
 
     def __init__(
         self,
         kore_client: KoreClient,
         definition: KDefinition,
         *,
-        trace_rewrites: bool = False,
+        log_succ_rewrites: bool = True,
+        log_fail_rewrites: bool = False,
     ):
         self._kore_client = kore_client
         self._definition = definition
-        self._trace_rewrites = trace_rewrites
+        self._log_succ_rewrites = log_succ_rewrites
+        self._log_fail_rewrites = log_fail_rewrites
 
     def kast_to_kore(self, kinner: KInner) -> Pattern:
         return kast_to_kore(self._definition, kinner, sort=GENERATED_TOP_CELL)
@@ -110,8 +113,8 @@ def execute(
                 cut_point_rules=cut_point_rules,
                 terminal_rules=terminal_rules,
                 module_name=module_name,
-                log_successful_rewrites=True,
-                log_failed_rewrites=self._trace_rewrites,
+                log_successful_rewrites=self._log_succ_rewrites,
+                log_failed_rewrites=self._log_succ_rewrites and self._log_fail_rewrites,
             )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
@@ -309,7 +312,8 @@ def cterm_symbolic(
     haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
     haskell_log_entries: Iterable[str] = (),
     log_axioms_file: Path | None = None,
-    trace_rewrites: bool = False,
+    log_succ_rewrites: bool = True,
+    log_fail_rewrites: bool = False,
     start_server: bool = True,
     maude_port: int | None = None,
     fallback_on: Iterable[FallbackReason] | None = None,
@@ -336,7 +340,9 @@ def cterm_symbolic(
             no_post_exec_simplify=no_post_exec_simplify,
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client:
-                yield CTermSymbolic(client, definition, trace_rewrites=trace_rewrites)
+                yield CTermSymbolic(
+                    client, definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+                )
     else:
         if port is None:
             raise ValueError('Missing port with start_server=False')
@@ -352,4 +358,6 @@ def cterm_symbolic(
                 ],
             }
         with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id, dispatch=dispatch) as client:
-            yield CTermSymbolic(client, definition, trace_rewrites=trace_rewrites)
+            yield CTermSymbolic(
+                client, definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+            )

pyk/src/pyk/kore/rpc.py

@@ -1227,10 +1227,14 @@ def _check_none_or_positive(n: int | None, param_name: str) -> None:
             if n is not None and n <= 0:
                 raise ValueError(f'Expected positive integer for: {param_name}, got: {n}')
 
+        def _check_none_or_nonnegative(n: int | None, param_name: str) -> None:
+            if n is not None and n < 0:
+                raise ValueError(f'Expected non-negative integer for: {param_name}, got: {n}')
+
         check_dir_path(self._kompiled_dir)
         check_file_path(self._definition_file)
         _check_none_or_positive(self._smt_timeout, 'smt_timeout')
-        _check_none_or_positive(self._smt_retry_limit, 'smt_retry_limit')
+        _check_none_or_nonnegative(self._smt_retry_limit, 'smt_retry_limit')
         _check_none_or_positive(self._smt_reset_interval, 'smt_reset_interval')
 
     def _cli_args(self) -> list[str]:
@@ -1244,16 +1248,16 @@ def _cli_args(self) -> list[str]:
     def _extra_args(self) -> list[str]:
         """Command line arguments that are intended to be included in the bug report."""
         smt_server_args = []
-        if self._smt_timeout:
+        if self._smt_timeout is not None:
             smt_server_args += ['--smt-timeout', str(self._smt_timeout)]
-        if self._smt_retry_limit:
+        if self._smt_retry_limit is not None:
             smt_server_args += ['--smt-retry-limit', str(self._smt_retry_limit)]
-        if self._smt_reset_interval:
+        if self._smt_reset_interval is not None:
             smt_server_args += ['--smt-reset-interval', str(self._smt_reset_interval)]
-        if self._smt_tactic:
+        if self._smt_tactic is not None:
             smt_server_args += ['--smt-tactic', self._smt_tactic]
 
-        if self._log_axioms_file:
+        if self._log_axioms_file is not None:
             haskell_log_args = [
                 '--log',
                 str(self._log_axioms_file),
@@ -1359,6 +1363,7 @@ def _validate(self) -> None:
 
         if self._interim_simplification and self._interim_simplification < 0:
             raise ValueError(f"'interim_simplification' must not be negative, got: {self._interim_simplification}")
+        super()._validate()
 
     def _extra_args(self) -> list[str]:
         res = super()._extra_args()