Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend

.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/llvm-backend_release

@@ -1 +1 @@
-0.1.69
+0.1.75

flake.nix

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

install-build-deps

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

package/debian/kframework/control.jammy

@@ -2,7 +2,7 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <[email protected]>
-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
 

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,
         }
 

pyk/src/pyk/cterm/symbolic.py

@@ -25,7 +25,7 @@
     kore_server,
 )
 from ..prelude.k import GENERATED_TOP_CELL, K_ITEM
-from ..prelude.ml import is_top, mlAnd, mlEquals
+from ..prelude.ml import is_top, mlEquals
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Iterator
@@ -92,28 +92,6 @@ def kast_to_kore(self, kinner: KInner) -> Pattern:
     def kore_to_kast(self, pattern: Pattern) -> KInner:
         return kore_to_kast(self._definition, pattern)
 
-    def minimize_constraints(self, constraints: tuple[KInner, ...], path_condition: KInner) -> tuple[KInner, ...]:
-        """Minimize given branching constraints with respect to a given path condition."""
-        # By construction, this function is to be called with at least two sets of constraints
-        assert len(constraints) >= 2
-        # Determine intersection between all returned sets of branching constraints
-        flattened_default = [flatten_label('#And', c) for c in constraints]
-        intersection = set.intersection(*(set(cs) for cs in flattened_default))
-        # If intersection is empty, there is nothing to be done
-        if not intersection:
-            return constraints
-        # Check if non-empty intersection is entailed by the path condition
-        dummy_config = self._definition.empty_config(sort=GENERATED_TOP_CELL)
-        path_condition_cterm = CTerm(dummy_config, constraints=[path_condition])
-        intersection_cterm = CTerm(dummy_config, constraints=intersection)
-        implication_check = self.implies(path_condition_cterm, intersection_cterm, bind_universally=True)
-        # The intersection is not entailed, there is nothing to be done
-        if implication_check.csubst is None:
-            return constraints
-        # The intersection is entailed and can be filtered out of the branching constraints
-        else:
-            return tuple(mlAnd(c for c in cs if c not in intersection) for cs in flattened_default)
-
     def execute(
         self,
         cterm: CTerm,
@@ -148,11 +126,6 @@ def execute(
             self.kore_to_kast(not_none(s.rule_predicate)) if s.rule_predicate is not None else None
             for s in resp_next_states
         )
-        # Branch constraint minimization makes sense only if there is a proper branching
-        if len(branching_constraints) >= 2 and all(bc is not None for bc in branching_constraints):
-            branching_constraints = self.minimize_constraints(
-                tuple(not_none(bc) for bc in branching_constraints), path_condition=mlAnd(cterm.constraints)
-            )
         next_states = tuple(
             NextState(CTerm.from_kast(self.kore_to_kast(ns.kore)), c)
             for ns, c in zip(resp_next_states, branching_constraints, strict=True)
@@ -219,6 +192,7 @@ def implies(
         bind_universally: bool = False,
         failure_reason: bool = False,
         module_name: str | None = None,
+        assume_defined: bool = False,
     ) -> CTermImplies:
         _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}')
         _consequent = consequent.kast
@@ -235,7 +209,9 @@ def implies(
         antecedent_kore = self.kast_to_kore(antecedent.kast)
         consequent_kore = self.kast_to_kore(_consequent)
         try:
-            result = self._kore_client.implies(antecedent_kore, consequent_kore, module_name=module_name)
+            result = self._kore_client.implies(
+                antecedent_kore, consequent_kore, module_name=module_name, assume_defined=assume_defined
+            )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
 
@@ -253,6 +229,7 @@ def implies(
                     bind_universally=bind_universally,
                     failure_reason=False,
                     module_name=module_name,
+                    assume_defined=assume_defined,
                 )
                 config_match = _config_match.csubst
                 if config_match is None:

pyk/src/pyk/kcfg/explore.py

@@ -72,7 +72,9 @@ def _extract_rule_labels(self, _logs: tuple[LogEntry, ...]) -> list[str]:
                     _rule_lines.append(f'{node_log.result.rule_id}:UNKNOWN')
         return _rule_lines
 
-    def implication_failure_reason(self, antecedent: CTerm, consequent: CTerm) -> tuple[bool, str]:
+    def implication_failure_reason(
+        self, antecedent: CTerm, consequent: CTerm, assume_defined: bool = False
+    ) -> tuple[bool, str]:
         def _is_cell_subst(csubst: KInner) -> bool:
             if type(csubst) is KApply and csubst.label.name == '_==K_':
                 csubst_arg = csubst.args[0]
@@ -91,7 +93,9 @@ def _is_negative_cell_subst(constraint: KInner) -> bool:
                         return True
             return False
 
-        cterm_implies = self.cterm_symbolic.implies(antecedent, consequent, failure_reason=True)
+        cterm_implies = self.cterm_symbolic.implies(
+            antecedent, consequent, failure_reason=True, assume_defined=assume_defined
+        )
         if cterm_implies.csubst is not None:
             return (True, '')
 

pyk/src/pyk/kcfg/kcfg.py

@@ -73,23 +73,18 @@ def kcfg_node_path(self, node_id: int) -> Path:
         return self.kcfg_node_dir / f'{node_id}.json'
 
     def write_cfg_data(
-        self, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = ()
+        self, kcfg: KCFG, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = ()
     ) -> None:
-        node_dict = {node_dct['id']: node_dct for node_dct in dct['nodes']}
         vacuous_nodes = [
-            node_id for node_id in node_dict.keys() if KCFGNodeAttr.VACUOUS.value in node_dict[node_id]['attrs']
-        ]
-        stuck_nodes = [
-            node_id for node_id in node_dict.keys() if KCFGNodeAttr.STUCK.value in node_dict[node_id]['attrs']
+            node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.VACUOUS in kcfg._nodes[node_id].attrs
         ]
+        stuck_nodes = [node_id for node_id in kcfg._nodes.keys() if KCFGNodeAttr.STUCK in kcfg._nodes[node_id].attrs]
         dct['vacuous'] = vacuous_nodes
         dct['stuck'] = stuck_nodes
         for node_id in deleted_nodes:
             self.kcfg_node_path(node_id).unlink(missing_ok=True)
         for node_id in created_nodes:
-            del node_dict[node_id]['attrs']
-            self.kcfg_node_path(node_id).write_text(json.dumps(node_dict[node_id]))
-        dct['nodes'] = list(node_dict.keys())
+            self.kcfg_node_path(node_id).write_text(json.dumps(kcfg._nodes[node_id].to_dict()))
         self.kcfg_json_path.write_text(json.dumps(dct))
 
     def read_cfg_data(self) -> dict[str, Any]:
@@ -542,6 +537,26 @@ def extend(
             case _:
                 raise AssertionError()
 
+    def to_dict_no_nodes(self) -> dict[str, Any]:
+        nodes = list(self._nodes.keys())
+        edges = [edge.to_dict() for edge in self.edges()]
+        covers = [cover.to_dict() for cover in self.covers()]
+        splits = [split.to_dict() for split in self.splits()]
+        ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()]
+
+        aliases = dict(sorted(self._aliases.items()))
+
+        res = {
+            'next': self._node_id,
+            'nodes': nodes,
+            'edges': edges,
+            'covers': covers,
+            'splits': splits,
+            'ndbranches': ndbranches,
+            'aliases': aliases,
+        }
+        return {k: v for k, v in res.items() if v}
+
     def to_dict(self) -> dict[str, Any]:
         nodes = [node.to_dict() for node in self.nodes]
         edges = [edge.to_dict() for edge in self.edges()]
@@ -1261,7 +1276,7 @@ def reachable_nodes(self, source_id: NodeIdLike, *, reverse: bool = False) -> se
     def write_cfg_data(self) -> None:
         assert self._kcfg_store is not None
         self._kcfg_store.write_cfg_data(
-            self.to_dict(), deleted_nodes=self._deleted_nodes, created_nodes=self._created_nodes
+            self, self.to_dict_no_nodes(), deleted_nodes=self._deleted_nodes, created_nodes=self._created_nodes
         )
         self._deleted_nodes.clear()
         self._created_nodes.clear()

pyk/src/pyk/kllvm/convert.py

@@ -108,7 +108,7 @@ def sentence_to_llvm(sentence: Sentence) -> kllvm.Declaration:
 def pattern_to_llvm(pattern: Pattern) -> kllvm.Pattern:
     match pattern:
         case String(value):
-            return kllvm.StringPattern(value)
+            return kllvm.StringPattern(value.encode('latin-1'))
         case VarPattern(name, sort):
             return kllvm.VariablePattern(name, sort_to_llvm(sort))
         case App(symbol, sorts, args):
@@ -201,7 +201,7 @@ def llvm_to_sentence(decl: kllvm.Declaration) -> Sentence:
 def llvm_to_pattern(pattern: kllvm.Pattern) -> Pattern:
     match pattern:
         case kllvm.StringPattern():  # type: ignore
-            return String(pattern.contents)
+            return String(pattern.contents.decode('latin-1'))
         case kllvm.VariablePattern():  # type: ignore
             if pattern.name and pattern.name[0] == '@':
                 return SVar(pattern.name, llvm_to_sort(pattern.sort))

pyk/src/pyk/kore/rpc.py

@@ -1027,12 +1027,14 @@ def implies(
         consequent: Pattern,
         *,
         module_name: str | None = None,
+        assume_defined: bool = False,
     ) -> ImpliesResult:
         params = filter_none(
             {
                 'antecedent': self._state(antecedent),
                 'consequent': self._state(consequent),
                 'module': module_name,
+                'assume-defined': assume_defined,
             }
         )
 

pyk/src/pyk/ktool/prove_rpc.py

@@ -48,6 +48,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]:
         return [
             self._prove_claim_rpc(
                 claim,
+                assume_defined=options.assume_defined,
                 max_depth=options.max_depth,
                 save_directory=options.save_directory,
                 max_iterations=options.max_iterations,
@@ -58,6 +59,7 @@ def prove_rpc(self, options: ProveOptions) -> list[Proof]:
     def _prove_claim_rpc(
         self,
         claim: KClaim,
+        assume_defined: bool,
         max_depth: int | None = None,
         save_directory: Path | None = None,
         max_iterations: int | None = None,
@@ -85,10 +87,10 @@ def _prove_claim_rpc(
             with self._explore_context() as kcfg_explore:
                 if is_functional_claim:
                     assert type(proof) is EqualityProof
-                    prover = ImpliesProver(proof, kcfg_explore)
+                    prover = ImpliesProver(proof, kcfg_explore, assume_defined=assume_defined)
                 else:
                     assert type(proof) is APRProof
-                    prover = APRProver(kcfg_explore, execute_depth=max_depth)
+                    prover = APRProver(kcfg_explore, execute_depth=max_depth, assume_defined=assume_defined)
                 prover.advance_proof(proof, max_iterations=max_iterations)
 
         if proof.passed:

pyk/src/pyk/proof/implies.py

@@ -410,13 +410,15 @@ def lines(self) -> list[str]:
 class ImpliesProver(Prover[ImpliesProof, ImpliesProofStep, ImpliesProofResult]):
     proof: ImpliesProof
     kcfg_explore: KCFGExplore
+    assume_defined: bool
 
     def close(self) -> None:
         self.kcfg_explore.cterm_symbolic._kore_client.close()
 
-    def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore):
+    def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore, assume_defined: bool = False):
         self.kcfg_explore = kcfg_explore
         self.proof = proof
+        self.assume_defined = assume_defined
 
     def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
         proof_type = type(step.proof).__name__
@@ -450,6 +452,7 @@ def step_proof(self, step: ImpliesProofStep) -> list[ImpliesProofResult]:
                 antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]),
                 consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]),
                 bind_universally=step.proof.bind_universally,
+                assume_defined=self.assume_defined,
             )
             result = _result.csubst
             if result is not None:

pyk/src/pyk/proof/reachability.py

@@ -671,6 +671,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]):
     always_check_subsumption: bool
     fast_check_subsumption: bool
     direct_subproof_rules: bool
+    assume_defined: bool
     kcfg_explore: KCFGExplore
 
     def __init__(
@@ -683,6 +684,7 @@ def __init__(
         always_check_subsumption: bool = True,
         fast_check_subsumption: bool = False,
         direct_subproof_rules: bool = False,
+        assume_defined: bool = False,
     ) -> None:
 
         self.kcfg_explore = kcfg_explore
@@ -694,6 +696,7 @@ def __init__(
         self.always_check_subsumption = always_check_subsumption
         self.fast_check_subsumption = fast_check_subsumption
         self.direct_subproof_rules = direct_subproof_rules
+        self.assume_defined = assume_defined
 
     def close(self) -> None:
         self.kcfg_explore.cterm_symbolic._kore_client.close()
@@ -737,7 +740,7 @@ def _check_subsume(self, node: KCFG.Node, target_node: KCFG.Node, proof_id: str)
         if self.fast_check_subsumption and not self._may_subsume(node, target_node):
             _LOGGER.info(f'Skipping full subsumption check because of fast may subsume check {proof_id}: {node.id}')
             return None
-        _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm)
+        _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm, assume_defined=self.assume_defined)
         csubst = _csubst.csubst
         if csubst is not None:
             _LOGGER.info(f'Subsumed into target node {proof_id}: {shorten_hashes((node.id, target_node.id))}')
@@ -804,7 +807,9 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]:
         ]
 
     def failure_info(self, proof: APRProof) -> FailureInfo:
-        return APRFailureInfo.from_proof(proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
+        return APRFailureInfo.from_proof(
+            proof, self.kcfg_explore, counterexample_info=self.counterexample_info, assume_defined=self.assume_defined
+        )
 
 
 @dataclass(frozen=True)
@@ -871,7 +876,9 @@ def __init__(
         )
 
     @staticmethod
-    def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo:
+    def from_proof(
+        proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False, assume_defined: bool = False
+    ) -> APRFailureInfo:
         target = proof.kcfg.node(proof.target)
         pending_nodes = {node.id for node in proof.pending}
         failing_nodes = {node.id for node in proof.failing}
@@ -881,7 +888,7 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info:
         for node in proof.failing:
             node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm)
             target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm)
-            _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
+            _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm, assume_defined=assume_defined)
             path_condition = kcfg_explore.pretty_print(proof.path_constraints(node.id))
             failure_reasons[node.id] = reason
             path_conditions[node.id] = path_condition