diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d7bdae44813..a89d1cef418 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -84,9 +84,9 @@ jobs: packages: jq script: | export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH" - kup publish k-framework-binary .#k --keep-days 180 - kup publish k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180 - + kup publish --verbose k-framework-binary .#k --keep-days 180 + kup publish --verbose k-framework-binary .#k.openssl.procps.secp256k1 --keep-days 180 + ubuntu-noble: name: 'K Ubuntu Noble Package' runs-on: [self-hosted, linux, normal] diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 851e0865dca..675a7338f7a 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1241,9 +1241,13 @@ You can: > left: Int "*Int" Int [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)] /* FIXME: translate /Int and %Int into smtlib */ - /* /Int and %Int implement t-division, which rounds towards 0 */ - | Int "/Int" Int [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)] - | Int "%Int" Int [function, symbol(_%Int_), left, smt-hook(mod), hook(INT.tmod)] + /* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */ + | Int "/Int" Int [function, symbol(_/Int_), left, + smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))), + hook(INT.tdiv)] + | Int "%Int" Int [function, symbol(_%Int_), left, + smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))), + hook(INT.tmod)] /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */ | Int "divInt" Int [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)] | Int "modInt" Int [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)] diff --git a/pyk/regression-new/kprove-haskell/sum-spec.k.out b/pyk/regression-new/kprove-haskell/sum-spec.k.out index c1e50df076c..28179677cdc 100644 --- a/pyk/regression-new/kprove-haskell/sum-spec.k.out +++ b/pyk/regression-new/kprove-haskell/sum-spec.k.out @@ -31,7 +31,9 @@ Subproofs: 0 │ #And { true #Equals N:Int >=Int 0 } ┃ ┃ (branch) -┣━━┓ constraint: N:Int >Int 0 +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ N:Int >Int 0 ┃ │ ┃ ├─ 3 ┃ │ @@ -92,8 +94,11 @@ Subproofs: 0 ┃ │ #And { true #Equals N:Int >=Int 0 } ┃ │ #And { true #Equals N:Int +Int -1 >=Int 0 } ┃ │ -┃ ┊ constraint: OMITTED CONSTRAINT -┃ ┊ subst: OMITTED SUBST +┃ ┊ constraint: +┃ ┊ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2 +┃ ┊ subst: +┃ ┊ ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int +┃ ┊ ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int ┃ └─ 2 (leaf, target) ┃ ┃ @@ -112,7 +117,9 @@ Subproofs: 0 ┃ #And { true #Equals N:Int >=Int 0 } ┃ #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 } ┃ -┗━━┓ constraint: N:Int ==Int 0 +┗━━┓ subst: .Subst + ┃ constraint: + ┃ N:Int ==Int 0 │ ├─ 4 │ @@ -151,8 +158,11 @@ Subproofs: 0 │ │ #And { N:Int #Equals 0 } │ - ┊ constraint: OMITTED CONSTRAINT - ┊ subst: OMITTED SUBST + ┊ constraint: + ┊ S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2 + ┊ subst: + ┊ C <- COUNTER_CELL_af8c44a5:Int + ┊ GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int └─ 2 (leaf, target) diff --git a/pyk/regression-new/kprove-haskell/test-spec.k.out b/pyk/regression-new/kprove-haskell/test-spec.k.out index 57c171d4601..c63c190355f 100644 --- a/pyk/regression-new/kprove-haskell/test-spec.k.out +++ b/pyk/regression-new/kprove-haskell/test-spec.k.out @@ -48,7 +48,8 @@ Subproofs: 0 │ │ ┊ constraint: true -┊ subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int +┊ subst: +┊ GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int └─ 2 (leaf, target) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 9f1c2dc871f..81d09295acb 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -282,7 +282,7 @@ def explore_context() -> Iterator[KCFGExplore]: if options.show_kcfg and type(proof) is APRProof: node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) show = APRProofShow(kprove, node_printer=node_printer) - print('\n'.join(show.show(proof))) + print('\n'.join(show.show(proof, minimize=False))) sys.exit(len([p.id for p in proofs if not p.passed])) diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py index 10f9f1cb526..6a8189aa757 100644 --- a/pyk/src/pyk/cterm/cterm.py +++ b/pyk/src/pyk/cterm/cterm.py @@ -38,7 +38,7 @@ class CTerm: Contains the data: - `config`: the _configuration_ (structural component of the state, potentially containing free variabls) - - `constraints`: conditiions which limit/constraint the free variables from the `config` + - `constraints`: conditions which limit/constraint the free variables from the `config` """ config: KInner # TODO Optional? @@ -253,6 +253,25 @@ def remove_useless_constraints(self, keep_vars: Iterable[str] = ()) -> CTerm: return CTerm(self.config, new_constraints) +def cterm_match(cterm1: CTerm, cterm2: CTerm) -> CSubst | None: + """Find a substitution which can instantiate `cterm1` to `cterm2`. + + Args: + cterm1: `CTerm` to instantiate to `cterm2`. + cterm2: `CTerm` to instantiate `cterm1` to. + + Returns: + A `CSubst` which can instantiate `cterm1` to `cterm2`, or `None` if no such `CSubst` exists. + """ + # todo: delete this function and use cterm1.match_with_constraint(cterm2) directly after closing #4496 + subst = cterm1.config.match(cterm2.config) + if subst is None: + return None + source_constraints = [subst(c) for c in cterm1.constraints] + constraints = [c for c in cterm2.constraints if c not in source_constraints] + return CSubst(subst, constraints) + + def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]: """Return a generalized state over the two input states. @@ -333,8 +352,13 @@ def add_constraint(self, constraint: KInner) -> CSubst: def apply(self, cterm: CTerm) -> CTerm: """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints).""" - _kast = self.subst(cterm.kast) - return CTerm(_kast, [self.constraint]) + config = self.subst(cterm.config) + constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints) + return CTerm(config, constraints) + + def __call__(self, cterm: CTerm) -> CTerm: + """Overload for `CSubst.apply`.""" + return self.apply(cterm) def cterm_build_claim( diff --git a/pyk/src/pyk/kast/manip.py b/pyk/src/pyk/kast/manip.py index 932397bf80c..7a56ab62e60 100644 --- a/pyk/src/pyk/kast/manip.py +++ b/pyk/src/pyk/kast/manip.py @@ -215,48 +215,39 @@ def extract_rhs(term: KInner) -> KInner: def extract_subst(term: KInner) -> tuple[Subst, KInner]: - def _subst_for_terms(term1: KInner, term2: KInner) -> Subst | None: - if type(term1) is KVariable and type(term2) not in {KToken, KVariable}: - return Subst({term1.name: term2}) - if type(term2) is KVariable and type(term1) not in {KToken, KVariable}: - return Subst({term2.name: term1}) - return None - - def _extract_subst(conjunct: KInner) -> Subst | None: - if type(conjunct) is KApply: - if conjunct.label.name == '#Equals': - subst = _subst_for_terms(conjunct.args[0], conjunct.args[1]) - - if subst is not None: - return subst - - if ( - conjunct.args[0] == TRUE - and type(conjunct.args[1]) is KApply - and conjunct.args[1].label.name in {'_==K_', '_==Int_'} - ): - subst = _subst_for_terms(conjunct.args[1].args[0], conjunct.args[1].args[1]) - - if subst is not None: - return subst + subst = {} + rem_conjuncts: list[KInner] = [] + def _extract_subst(term: KInner, term2: KInner) -> tuple[str, KInner] | None: + if ( + (isinstance(term, KVariable) and term.name not in subst) + and not (isinstance(term2, KVariable) and term2.name in subst) + and term.name not in free_vars(term2) + ): + return (term.name, term2) + if ( + (isinstance(term2, KVariable) and term2.name not in subst) + and not (isinstance(term, KVariable) and term.name in subst) + and term2.name not in free_vars(term) + ): + return (term2.name, term) + if term == TRUE and isinstance(term2, KApply) and term2.label.name in {'_==K_', '_==Int_'}: + return _extract_subst(term2.args[0], term2.args[1]) + if term2 == TRUE and isinstance(term, KApply) and term.label.name in {'_==K_', '_==Int_'}: + return _extract_subst(term.args[0], term.args[1]) return None - conjuncts = flatten_label('#And', term) - subst = Subst() - rem_conjuncts: list[KInner] = [] - - for conjunct in conjuncts: - new_subst = _extract_subst(conjunct) - if new_subst is None: - rem_conjuncts.append(conjunct) + for conjunct in flatten_label('#And', term): + if isinstance(conjunct, KApply) and conjunct.label.name == '#Equals': + if _conjunct_subst := _extract_subst(conjunct.args[0], conjunct.args[1]): + name, value = _conjunct_subst + subst[name] = value + else: + rem_conjuncts.append(conjunct) else: - new_subst = subst.union(new_subst) - if new_subst is None: - raise ValueError('Conflicting substitutions') # TODO handle this case - subst = new_subst + rem_conjuncts.append(conjunct) - return subst, mlAnd(rem_conjuncts) + return Subst(subst), mlAnd(rem_conjuncts) def count_vars(term: KInner) -> Counter[str]: diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py index 2da3d3e9210..5937f02ceed 100644 --- a/pyk/src/pyk/kcfg/kcfg.py +++ b/pyk/src/pyk/kcfg/kcfg.py @@ -9,6 +9,8 @@ from threading import RLock from typing import TYPE_CHECKING, Final, List, Union, cast, final +from pyk.cterm.cterm import cterm_match + from ..cterm import CSubst, CTerm, cterm_build_claim, cterm_build_rule from ..kast import EMPTY_ATT from ..kast.inner import KApply @@ -1040,6 +1042,16 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike, self.add_successor(split) return split + def create_split_by_nodes(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> KCFG.Split | None: + """Create a split without crafting a CSubst.""" + source = self.node(source_id) + targets = [self.node(nid) for nid in target_ids] + try: + csubsts = [not_none(cterm_match(source.cterm, target.cterm)) for target in targets] + except ValueError: + return None + return self.create_split(source.id, zip(target_ids, csubsts, strict=True)) + def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: source_id = self._resolve(source_id) if source_id is not None else None target_id = self._resolve(target_id) if target_id is not None else None diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 6ace8d1abd8..b4e2db73338 100644 --- a/pyk/src/pyk/kcfg/show.py +++ b/pyk/src/pyk/kcfg/show.py @@ -27,6 +27,7 @@ from pathlib import Path from typing import Final + from ..cterm import CSubst from ..kast import KInner from ..kast.outer import KFlatModule, KSentence from ..ktool.kprint import KPrint @@ -126,6 +127,34 @@ def pretty_segments(self, kcfg: KCFG, minimize: bool = True) -> Iterable[tuple[s processed_nodes: list[KCFG.Node] = [] ret_lines: list[tuple[str, list[str]]] = [] + def _multi_line_print( + label: str, lines: list[str], default: str = 'None', indent: int = 4, max_width: int | None = None + ) -> list[str]: + ret_lines = [] + if len(lines) == 0: + ret_lines.append(f'{label}: {default}') + else: + ret_lines.append(f'{label}:') + ret_lines.extend([f'{indent * " "}{line}' for line in lines]) + if max_width is not None: + ret_lines = [ + ret_line if len(ret_line) <= max_width else ret_line[0:max_width] + '...' for ret_line in ret_lines + ] + return ret_lines + + def _print_csubst( + csubst: CSubst, subst_first: bool = False, indent: int = 4, max_width: int | None = None + ) -> list[str]: + _constraint_strs = [ + self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints + ] + constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width) + _subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in csubst.subst.minimize().items()] + subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width) + if subst_first: + return subst_strs + constraint_strs + return constraint_strs + subst_strs + def _print_node(node: KCFG.Node) -> list[str]: return self.node_short_info(kcfg, node) @@ -143,46 +172,12 @@ def _print_merged_edge(merged_edge: KCFG.MergedEdge) -> list[str]: return [res] if len(res) < 78 else ['(merged edge)'] def _print_cover(cover: KCFG.Cover) -> Iterable[str]: - subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in cover.csubst.subst.items()] - subst_str = '' - if len(subst_strs) == 0: - subst_str = '.Subst' - if len(subst_strs) == 1: - subst_str = subst_strs[0] - if len(subst_strs) > 1 and minimize: - subst_str = 'OMITTED SUBST' - if len(subst_strs) > 1 and not minimize: - subst_str = '{\n ' + '\n '.join(subst_strs) + '\n}' - constraint_str = self.kprint.pretty_print(ml_pred_to_bool(cover.csubst.constraint, unsafe=True)) - if len(constraint_str) > 78: - constraint_str = 'OMITTED CONSTRAINT' - return [ - f'constraint: {constraint_str}', - f'subst: {subst_str}', - ] + max_width = None if not minimize else 78 + return _print_csubst(cover.csubst, subst_first=False, indent=4, max_width=max_width) def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]: - csubst = split.splits[target_id] - ret_split_lines: list[str] = [] - substs = csubst.subst.minimize().items() - constraints = [ml_pred_to_bool(c, unsafe=True) for c in csubst.constraints] - if len(constraints) == 1: - first_line, *rest_lines = self.kprint.pretty_print(constraints[0]).split('\n') - ret_split_lines.append(f'constraint: {first_line}') - ret_split_lines.extend(f' {line}' for line in rest_lines) - elif len(constraints) > 1: - ret_split_lines.append('constraints:') - for constraint in constraints: - first_line, *rest_lines = self.kprint.pretty_print(constraint).split('\n') - ret_split_lines.append(f' {first_line}') - ret_split_lines.extend(f' {line}' for line in rest_lines) - if len(substs) == 1: - vname, term = list(substs)[0] - ret_split_lines.append(f'subst: {vname} <- {self.kprint.pretty_print(term)}') - elif len(substs) > 1: - ret_split_lines.append('substs:') - ret_split_lines.extend(f' {vname} <- {self.kprint.pretty_print(term)}' for vname, term in substs) - return ret_split_lines + max_width = None if not minimize else 78 + return _print_csubst(split.splits[target_id], subst_first=True, indent=4, max_width=max_width) def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG.Node]) -> None: processed = curr_node in processed_nodes diff --git a/pyk/src/pyk/prelude/ml.py b/pyk/src/pyk/prelude/ml.py index ab926469925..224c11fc7ea 100644 --- a/pyk/src/pyk/prelude/ml.py +++ b/pyk/src/pyk/prelude/ml.py @@ -5,7 +5,7 @@ from pyk.utils import single from ..kast.inner import KApply, KLabel, build_assoc, flatten_label -from .k import GENERATED_TOP_CELL, K_ITEM +from .k import GENERATED_TOP_CELL, K_ITEM, K from .kbool import BOOL, FALSE, TRUE if TYPE_CHECKING: @@ -55,7 +55,7 @@ def is_bottom(term: KInner, *, weak: bool = False) -> bool: def mlEquals( # noqa: N802 term1: KInner, term2: KInner, - arg_sort: str | KSort = GENERATED_TOP_CELL, + arg_sort: str | KSort = K, sort: str | KSort = GENERATED_TOP_CELL, ) -> KApply: return KLabel('#Equals', arg_sort, sort)(term1, term2) diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 8acbcd60cc7..da4a8082006 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -12,7 +12,7 @@ from pyk.kast.manip import minimize_term, sort_ac_collections from pyk.kcfg.semantics import KCFGSemantics from pyk.kcfg.show import KCFGShow -from pyk.prelude.kbool import FALSE, andBool, orBool +from pyk.prelude.kbool import BOOL, FALSE, andBool, orBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEquals, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.proof import APRProver, ProofStatus @@ -700,7 +700,7 @@ def custom_step(self, c: CTerm) -> KCFGExtendResult | None: 'failing-if', 0, 1, - (mlEquals(KVariable('_B', 'Bool'), FALSE),), + (mlEquals(KVariable('_B', 'Bool'), FALSE, arg_sort=BOOL),), False, ), ( diff --git a/pyk/src/tests/integration/test_division_hooks.py b/pyk/src/tests/integration/test_division_hooks.py new file mode 100644 index 00000000000..d64f4942987 --- /dev/null +++ b/pyk/src/tests/integration/test_division_hooks.py @@ -0,0 +1,162 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +from pyk.kore.prelude import ( + BOOL, + INT, + SORT_K_ITEM, + TRUE, + eq_int, + generated_counter, + generated_top, + inj, + int_dv, + k, + kseq, +) +from pyk.kore.rpc import SatResult, State, StuckResult +from pyk.kore.syntax import App, Equals, EVar +from pyk.ktool.krun import llvm_interpret +from pyk.testing import KompiledTest, KoreClientTest + +if TYPE_CHECKING: + from pathlib import Path + from typing import Final + + from pyk.kore.rpc import KoreClient + from pyk.kore.syntax import Pattern + + +T_DIVISION_TEST_DATA: Final = ( + # Op , a, b, a Op b + ('/Int', +8, +3, +2), + ('/Int', +8, -3, -2), + ('/Int', -8, +3, -2), + ('/Int', -8, -3, +2), + ('%Int', +8, +3, +2), + ('%Int', +8, -3, +2), + ('%Int', -8, +3, -2), + ('%Int', -8, -3, -2), + ##################### + ('/Int', +1, +2, 0), + ('/Int', +1, -2, 0), + ('/Int', -1, +2, 0), + ('/Int', -1, -2, 0), + ('%Int', +1, +2, +1), + ('%Int', +1, -2, +1), + ('%Int', -1, +2, -1), + ('%Int', -1, -2, -1), + ##################### + ('/Int', +4, +2, +2), + ('/Int', +4, -2, -2), + ('/Int', -4, +2, -2), + ('/Int', -4, -2, +2), + ('%Int', +4, +2, 0), + ('%Int', +4, -2, 0), + ('%Int', -4, +2, 0), + ('%Int', -4, -2, 0), +) +IDS: Final = tuple(f'{a} {op} {b} == {c}' for op, a, b, c in T_DIVISION_TEST_DATA) +DEFINITION = """ + module SMT + imports INT + endmodule +""" + + +def div_pattern(op: str, a: int, b: int) -> App: + kore_for = { + '/Int': "Lbl'UndsSlsh'Int'Unds'", + '%Int': "Lbl'UndsPerc'Int'Unds'", + } + return App(kore_for[op], (), (int_dv(a), int_dv(b))) + + +def config(pgm: Pattern) -> App: + return generated_top( + ( + k( + kseq( + (inj(INT, SORT_K_ITEM, pgm),), + ) + ), + generated_counter(int_dv(0)), + ), + ) + + +class TestDivisionHooksLlvm(KompiledTest): + KOMPILE_DEFINITION = DEFINITION + KOMPILE_MAIN_MODULE = 'SMT' + KOMPILE_ARGS = {'syntax_module': 'SMT'} + + @pytest.mark.parametrize('op, a, b, c', T_DIVISION_TEST_DATA, ids=IDS) + def test(self, definition_dir: Path, op: str, a: int, b: int, c: int) -> None: + # Given + pattern = config(div_pattern(op, a, b)) + expected = config(int_dv(c)) + + # When + actual = llvm_interpret(definition_dir, pattern) + + # Then + assert actual == expected + + +class TestDivisionHooksHs(KoreClientTest): + KOMPILE_DEFINITION = DEFINITION + KOMPILE_MAIN_MODULE = 'SMT' + KOMPILE_ARGS = {'syntax_module': 'SMT'} + LLVM_ARGS = {'syntax_module': 'SMT'} + + @pytest.mark.parametrize('op, a, b, c', T_DIVISION_TEST_DATA, ids=IDS) + def test_get_model(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None: + """Check whether the SMT solver returns ``X = c`` for ``X = a op b``.""" + + # Given + pattern = Equals( + BOOL, + INT, + TRUE, + eq_int(div_pattern(op, a, b), EVar('X', INT)), + ) + expected = SatResult(Equals(INT, INT, EVar('X', INT), int_dv(c))) + + # When + actual = kore_client.get_model(pattern) + + # Then + assert actual == expected + + @pytest.mark.parametrize('op, a, b, c', T_DIVISION_TEST_DATA, ids=IDS) + def test_simplify(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None: + """Check whether kore-rpc (HS hook) and booster (LLVM library) both return ``c`` for ``a op b``.""" + + # Given + pattern = div_pattern(op, a, b) + expected = (int_dv(c), ()) + + # When + actual = kore_client.simplify(pattern) + + # Then + assert actual == expected + + @pytest.mark.parametrize('op, a, b, c', T_DIVISION_TEST_DATA, ids=IDS) + def test_execute(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None: + # Given + pattern = config(div_pattern(op, a, b)) + expected = StuckResult( + state=State(config(int_dv(c))), + depth=0, + logs=(), + ) + + # When + actual = kore_client.execute(pattern) + + # Then + assert actual == expected diff --git a/pyk/src/tests/unit/kast/test_subst.py b/pyk/src/tests/unit/kast/test_subst.py index 3a06f698f5f..fa5fd1c628c 100644 --- a/pyk/src/tests/unit/kast/test_subst.py +++ b/pyk/src/tests/unit/kast/test_subst.py @@ -8,7 +8,7 @@ from pyk.kast.inner import KApply, KLabel, KVariable, Subst from pyk.kast.manip import extract_subst from pyk.prelude.kbool import TRUE -from pyk.prelude.kint import intToken +from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlAnd, mlEquals, mlEqualsTrue, mlOr, mlTop from ..utils import a, b, c, f, g, h, x, y, z @@ -131,11 +131,14 @@ def test_ml_pred(test_id: str, subst: Subst, pred: KInner) -> None: _EQ = KLabel('_==Int_') EXTRACT_SUBST_TEST_DATA: Final[tuple[tuple[KInner, dict[str, KInner], KInner], ...]] = ( (a, {}, a), - (mlEquals(a, b), {}, mlEquals(a, b)), - (mlEquals(x, a), {'x': a}, mlTop()), - (mlEquals(x, _0), {}, mlEquals(x, _0)), - (mlEquals(x, y), {}, mlEquals(x, y)), - (mlAnd([mlEquals(a, b), mlEquals(x, a)]), {'x': a}, mlEquals(a, b)), + (mlEquals(a, b, arg_sort=INT), {}, mlEquals(a, b, arg_sort=INT)), + (mlEquals(x, a, arg_sort=INT), {'x': a}, mlTop()), + (mlEquals(x, _0, arg_sort=INT), {'x': _0}, mlTop()), + (mlEquals(x, y, arg_sort=INT), {'x': y}, mlTop()), + (mlEquals(x, f(x), arg_sort=INT), {}, mlEquals(x, f(x), arg_sort=INT)), + (mlAnd([mlEquals(x, y, arg_sort=INT), mlEquals(x, b, arg_sort=INT)]), {'x': y}, mlEquals(x, b, arg_sort=INT)), + (mlAnd([mlEquals(x, b, arg_sort=INT), mlEquals(x, y, arg_sort=INT)]), {'x': b}, mlEquals(x, y, arg_sort=INT)), + (mlAnd([mlEquals(a, b, arg_sort=INT), mlEquals(x, a, arg_sort=INT)]), {'x': a}, mlEquals(a, b, arg_sort=INT)), (mlEqualsTrue(_EQ(a, b)), {}, mlEqualsTrue(_EQ(a, b))), (mlEqualsTrue(_EQ(x, a)), {'x': a}, mlTop()), ) @@ -158,7 +161,7 @@ def test_propagate_subst() -> None: bar_x = KApply('bar', [x]) config = KApply('', [bar_x]) - subst_conjunct = mlEquals(v1, bar_x) + subst_conjunct = mlEquals(v1, bar_x, arg_sort=INT) other_conjunct = mlEqualsTrue(KApply('_<=Int_', [v1, KApply('foo', [x, bar_x])])) term = mlAnd([config, subst_conjunct, other_conjunct]) @@ -181,8 +184,8 @@ def test_propagate_subst() -> None: 'positive', mlAnd( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), ] ), Subst({'X': intToken(1), 'Y': intToken(2)}), @@ -191,8 +194,8 @@ def test_propagate_subst() -> None: 'wrong-connective', mlOr( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), ] ), None, @@ -201,8 +204,8 @@ def test_propagate_subst() -> None: 'not-subst', mlAnd( [ - mlEquals(KVariable('X'), intToken(1)), - mlEquals(KVariable('Y'), intToken(2)), + mlEquals(KVariable('X'), intToken(1), arg_sort=INT), + mlEquals(KVariable('Y'), intToken(2), arg_sort=INT), mlEqualsTrue(KApply('_==K_', [KVariable('Y'), intToken(2)])), ] ), diff --git a/pyk/src/tests/unit/kcfg/test_minimize.py b/pyk/src/tests/unit/kcfg/test_minimize.py index 001f22998c4..4221f3eb650 100644 --- a/pyk/src/tests/unit/kcfg/test_minimize.py +++ b/pyk/src/tests/unit/kcfg/test_minimize.py @@ -340,56 +340,64 @@ def x_lt(n: int) -> KApply: '┌─ 1 (root, split)\n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 32 )\n' '┃ ┃ _>=Int_ ( X , 64 )\n' '┃ │\n' '┃ └─ 8 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 32 )\n' '┃ ┃ _=Int_ ( X , 0 )\n' '┃ ┃ _=Int_ ( X , 16 )\n' '┃ │\n' '┃ └─ 10 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _>=Int_ ( X , -16 )\n' '┃ │\n' '┃ └─ 12 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _=Int_ ( X , -64 )\n' '┃ │\n' '┃ └─ 14 (leaf)\n' '┃\n' - '┗━━┓ constraints:\n' + '┗━━┓ subst: .Subst\n' + ' ┃ constraint:\n' ' ┃ _ None: # Then assert cterm == expected + + +APPLY_TEST_DATA: Final = ( + (CTerm.top(), CSubst(), CTerm.top()), + (CTerm.bottom(), CSubst(), CTerm.bottom()), + ( + CTerm(k(KVariable('X'))), + CSubst(), + CTerm(k(KVariable('X'))), + ), + ( + CTerm(k(KVariable('X'))), + CSubst(Subst({'X': intToken(5)})), + CTerm(k(intToken(5))), + ), + ( + CTerm(k(KVariable('X'))), + CSubst(Subst({'X': KVariable('Y')})), + CTerm(k(KVariable('Y'))), + ), + ( + CTerm(k(KVariable('X')), [lt_ml('X', 5)]), + CSubst(Subst({'X': KVariable('Y')}), [ge_ml('Y', 0)]), + CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)]), + ), +) + + +@pytest.mark.parametrize( + 'term,subst,expected', + APPLY_TEST_DATA, +) +def test_csubst_apply(term: CTerm, subst: CSubst, expected: CTerm) -> None: + # When + actual = subst(term) + + # Then + assert actual == expected diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index 9ba68366a07..cfa5207d353 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -1,8 +1,9 @@ from __future__ import annotations -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, Final import pytest +from unit.utils import ge_ml, k, lt_ml from pyk.cterm import CSubst, CTerm from pyk.kast.inner import KApply, KRewrite, KToken, KVariable, Subst @@ -10,6 +11,7 @@ from pyk.kcfg import KCFG, KCFGShow from pyk.kcfg.kcfg import KCFGNodeAttr from pyk.kcfg.show import NodePrinter +from pyk.prelude.kint import INT from pyk.prelude.ml import mlEquals, mlTop from pyk.prelude.utils import token from pyk.utils import not_none, single @@ -41,7 +43,7 @@ def to_csubst_id(source_id: int, target_id: int, constraints: Iterable[KInner]) def x_equals(i: int) -> KInner: - return mlEquals(KVariable('X'), token(i)) + return mlEquals(KVariable('X'), token(i), arg_sort=INT) def x_config() -> KInner: @@ -590,8 +592,10 @@ def test_pretty_print() -> None: '├─ 14 (split, @bar, @foo)\n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraint: _==K_ ( X , 15 )\n' - '┃ ┃ subst: V14 <- V15\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V15\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' '┃ ├─ 15\n' '┃ │\n' @@ -602,27 +606,35 @@ def test_pretty_print() -> None: '┃ └─ 13\n' '┃ (looped back)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 16 )\n' - '┃ ┃ subst: V14 <- V16\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V16\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' '┃ └─ 16\n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 17 )\n' - '┃ ┃ subst: V14 <- V17\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V17\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 18 )\n' - '┃ ┃ subst: V14 <- V18\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V18\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' '┃ ├─ 18\n' '┃ │\n' '┃ │ (1 step)\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 20 )\n' - '┃ ┃ subst: V14 <- V20\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V20\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' '┃ ├─ 20\n' '┃ ┃\n' @@ -635,13 +647,17 @@ def test_pretty_print() -> None: '┃ │\n' '┃ └─ 25 (leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 23 )\n' - '┃ ┃ subst: V14 <- V23\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V23\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' '┃ └─ 23 (stuck, leaf)\n' '┃\n' - '┗━━┓ constraint: _==K_ ( X , 22 )\n' - ' ┃ subst: V14 <- V22\n' + '┗━━┓ subst:\n' + ' ┃ V14 <- V22\n' + ' ┃ constraint:\n' + ' ┃ _==K_ ( X , 22 )\n' ' │\n' ' ├─ 22\n' ' │\n' @@ -649,7 +665,8 @@ def test_pretty_print() -> None: ' ├─ 19\n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst: V22 <- V19\n' + ' ┊ subst:\n' + ' ┊ V22 <- V19\n' ' └─ 22\n' ' (looped back)\n' '\n' @@ -685,8 +702,10 @@ def test_pretty_print() -> None: '│ \n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraint: _==K_ ( X , 15 )\n' - '┃ ┃ subst: V14 <- V15\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V15\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' '┃ ├─ 15\n' '┃ │ \n' @@ -706,8 +725,10 @@ def test_pretty_print() -> None: '┃ \n' '┃ (looped back)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 16 )\n' - '┃ ┃ subst: V14 <- V16\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V16\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' '┃ └─ 16\n' '┃ \n' @@ -715,16 +736,20 @@ def test_pretty_print() -> None: '┃ \n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 17 )\n' - '┃ ┃ subst: V14 <- V17\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V17\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' '┃ └─ 17 (vacuous, leaf)\n' '┃ \n' '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 18 )\n' - '┃ ┃ subst: V14 <- V18\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V18\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' '┃ ├─ 18\n' '┃ │ \n' @@ -737,8 +762,10 @@ def test_pretty_print() -> None: '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 20 )\n' - '┃ ┃ subst: V14 <- V20\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V20\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' '┃ ├─ 20\n' '┃ │ \n' @@ -761,16 +788,20 @@ def test_pretty_print() -> None: '┃ \n' '┃ #And #Equals ( X , 25 )\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 23 )\n' - '┃ ┃ subst: V14 <- V23\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V23\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' '┃ └─ 23 (stuck, leaf)\n' '┃ \n' '┃ V23\n' '┃ \n' '┃\n' - '┗━━┓ constraint: _==K_ ( X , 22 )\n' - ' ┃ subst: V14 <- V22\n' + '┗━━┓ subst:\n' + ' ┃ V14 <- V22\n' + ' ┃ constraint:\n' + ' ┃ _==K_ ( X , 22 )\n' ' │\n' ' ├─ 22\n' ' │ \n' @@ -784,7 +815,8 @@ def test_pretty_print() -> None: ' │ \n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst: V22 <- V19\n' + ' ┊ subst:\n' + ' ┊ V22 <- V19\n' ' └─ 22\n' ' \n' ' V22\n' @@ -849,3 +881,96 @@ def test_no_cell_rewrite_to_dots() -> None: result = no_cell_rewrite_to_dots(term) assert result == term + + +CREATE_SPLIT_BY_NODES_TEST_DATA: Final = ( + (CTerm.bottom(), [CTerm.top(), CTerm.bottom()], None), + (CTerm.top(), [CTerm.top(), CTerm.bottom()], None), + ( + CTerm.top(), + [CTerm(k(KVariable('X'))), CTerm(k(KVariable('Y')))], + None, # todo: support split from top, because top means anything can be matched + ), + # not mutually exclusive + ( + CTerm.top(), + [CTerm.top(), CTerm.top()], + KCFG.Split( + KCFG.Node(1, CTerm.top()), [(KCFG.Node(2, CTerm.top()), CSubst()), (KCFG.Node(3, CTerm.top()), CSubst())] + ), + ), + # not mutually exclusive + ( + CTerm(k(KVariable('X'))), + [CTerm(k(KVariable('X'))), CTerm(k(KVariable('Y'))), CTerm(k(KVariable('Z')))], + KCFG.Split( + KCFG.Node(1, CTerm(k(KVariable('X')))), + [ + (KCFG.Node(2, CTerm(k(KVariable('X')))), CSubst(Subst({'X': KVariable('X')}))), + (KCFG.Node(3, CTerm(k(KVariable('Y')))), CSubst(Subst({'X': KVariable('Y')}))), + (KCFG.Node(4, CTerm(k(KVariable('Z')))), CSubst(Subst({'X': KVariable('Z')}))), + ], + ), + ), + (CTerm(k(KVariable('X'))), [CTerm(k(KVariable('Y'))), CTerm(KApply('', [KVariable('Z')]))], None), + # not mutually exclusive + # this target doesn't meet the implication relationship with source. + # So the CTerm of target and CSubst.apply(target) are not logically equal. + # But source -> CSubst.apply(target) can always be true. + ( + CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)]), + [CTerm(k(KVariable('Y')), [ge_ml('Y', 0)]), CTerm(k(KVariable('Z')), [ge_ml('Z', 5)])], + KCFG.Split( + KCFG.Node(1, CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)])), + [ + ( + KCFG.Node(2, CTerm(k(KVariable('Y')), [ge_ml('Y', 0)])), + CSubst(Subst({'X': KVariable('Y')}), []), + ), + ( + KCFG.Node(3, CTerm(k(KVariable('Z')), [ge_ml('Z', 5)])), + CSubst( + Subst({'X': KVariable('Z')}), + [ + ge_ml('Z', 5), + ], + ), + ), + ], + ), + ), + ( + CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)]), + [ + CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)]), + CTerm(k(KVariable('Z')), [ge_ml('Z', 5), lt_ml('Z', 10)]), + ], + KCFG.Split( + KCFG.Node(1, CTerm(k(KVariable('X')), [ge_ml('X', 0), lt_ml('X', 10)])), + [ + ( + KCFG.Node(2, CTerm(k(KVariable('Y')), [ge_ml('Y', 0), lt_ml('Y', 5)])), + CSubst(Subst({'X': KVariable('Y')}), [lt_ml('Y', 5)]), + ), + ( + KCFG.Node(3, CTerm(k(KVariable('Z')), [ge_ml('Z', 5), lt_ml('Z', 10)])), + CSubst(Subst({'X': KVariable('Z')}), [ge_ml('Z', 5)]), + ), + ], + ), + ), +) + + +@pytest.mark.parametrize('source,targets,expected', CREATE_SPLIT_BY_NODES_TEST_DATA) +def test_create_split_by_nodes(source: CTerm, targets: Iterable[CTerm], expected: KCFG.Split | None) -> None: + # Given + cfg = KCFG() + source_node = cfg.create_node(source) + target_nodes = [cfg.create_node(target) for target in targets] + + # When + actual = cfg.create_split_by_nodes(source_node.id, [n.id for n in target_nodes]) + + # Then + assert actual == expected diff --git a/pyk/src/tests/unit/utils.py b/pyk/src/tests/unit/utils.py index 73ed9ff8776..d31d2e0e9d3 100644 --- a/pyk/src/tests/unit/utils.py +++ b/pyk/src/tests/unit/utils.py @@ -4,6 +4,8 @@ from typing import TYPE_CHECKING from pyk.kast.inner import KApply, KLabel, KVariable +from pyk.prelude.kint import geInt, intToken, ltInt +from pyk.prelude.ml import mlEqualsTrue if TYPE_CHECKING: from typing import Final @@ -16,3 +18,11 @@ f, g, h = map(KLabel, ('f', 'g', 'h')) k = KLabel('') + + +def lt_ml(var: str, n: int) -> KApply: + return mlEqualsTrue(ltInt(KVariable(var), intToken(n))) + + +def ge_ml(var: str, n: int) -> KApply: + return mlEqualsTrue(geInt(KVariable(var), intToken(n)))