Skip to content

Commit 47d84d0

Browse files
rv-jenkinsrv-auditorehildenb
authored
Update dependency: deps/k_release (#2764)
* deps/k_release: Set Version 7.1.254 * kevm-pyk/: sync poetry files pyk version 7.1.254 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.255 * kevm-pyk/: sync poetry files pyk version 7.1.255 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.256 * kevm-pyk/: sync poetry files pyk version 7.1.256 * flake.{nix,lock}: update Nix derivations * deps/k_release: Set Version 7.1.257 * kevm-pyk/: sync poetry files pyk version 7.1.257 * flake.{nix,lock}: update Nix derivations * kevm-pyk/{kevm,summarizer,__main__}: migrate to CTermShow * kevm-pyk/: sync poetry files pyk version 7.1.257 * deps/k_release: Set Version 7.1.258 * kevm-pyk/: sync poetry files pyk version 7.1.258 * flake.{nix,lock}: update Nix derivations * kevm-pyk/poetry.lock: update file * kevm-pyk/kompile: switch C++17 => C++20 * kevm-pyk/: sync poetry files pyk version 7.1.258 * deps/k_release: Set Version 7.1.259 * kevm-pyk/: sync poetry files pyk version 7.1.259 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
1 parent 3c7651b commit 47d84d0

10 files changed

Lines changed: 97 additions & 96 deletions

File tree

‎deps/k_release‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
7.1.253
1+
7.1.259

‎flake.lock‎

Lines changed: 8 additions & 8 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
description = "A flake for the KEVM Semantics";
33

44
inputs = {
5-
k-framework.url = "github:runtimeverification/k/v7.1.253";
5+
k-framework.url = "github:runtimeverification/k/v7.1.259";
66
nixpkgs.follows = "k-framework/nixpkgs";
77
flake-utils.follows = "k-framework/flake-utils";
88
rv-utils.follows = "k-framework/rv-utils";

‎kevm-pyk/poetry.lock‎

Lines changed: 71 additions & 71 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎kevm-pyk/pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ authors = [
1313
[tool.poetry.dependencies]
1414
python = "^3.10"
1515
pathos = "*"
16-
kframework = "7.1.253"
16+
kframework = "7.1.259"
1717
tomlkit = "^0.11.6"
1818
frozendict = "^2.4.6"
1919

‎kevm-pyk/src/kevm_pyk/__main__.py‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -538,15 +538,14 @@ def exec_show_kcfg(options: ShowKCFGOptions) -> None:
538538
nodes = list(nodes) + [node.id for node in proof.failing]
539539

540540
node_printer = kevm_node_printer(kevm, proof)
541-
proof_show = APRProofShow(kevm, node_printer=node_printer)
541+
proof_show = APRProofShow(kevm.definition, node_printer=node_printer)
542542

543543
res_lines = proof_show.show(
544544
proof,
545545
nodes=nodes,
546546
node_deltas=options.node_deltas,
547547
to_module=options.to_module,
548548
minimize=options.minimize,
549-
sort_collections=options.sort_collections,
550549
)
551550

552551
if options.failure_info:

‎kevm-pyk/src/kevm_pyk/kevm.py‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
from typing import TYPE_CHECKING, NamedTuple
66

77
from pyk.cterm import CTerm, CTermSymbolic
8+
from pyk.cterm.show import CTermShow
89
from pyk.kast import KInner
910
from pyk.kast.inner import (
1011
KApply,
@@ -25,7 +26,7 @@
2526
from pyk.kast.prelude.ml import mlEqualsFalse, mlEqualsTrue
2627
from pyk.kast.prelude.string import stringToken
2728
from pyk.kast.prelude.utils import token
28-
from pyk.kast.pretty import paren
29+
from pyk.kast.pretty import PrettyPrinter, paren
2930
from pyk.kcfg.kcfg import KCFGExtendResult, Step
3031
from pyk.kcfg.semantics import DefaultSemantics
3132
from pyk.kcfg.show import NodePrinter
@@ -697,8 +698,8 @@ def end_basic_block() -> KInner:
697698
class KEVMNodePrinter(NodePrinter):
698699
kevm: KEVM
699700

700-
def __init__(self, kevm: KEVM):
701-
NodePrinter.__init__(self, kevm)
701+
def __init__(self, kevm: KEVM, cterm_show: CTermShow, full_printer: bool = True):
702+
NodePrinter.__init__(self, cterm_show, full_printer=full_printer)
702703
self.kevm = kevm
703704

704705
def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
@@ -708,14 +709,15 @@ def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
708709

709710

710711
class KEVMAPRNodePrinter(KEVMNodePrinter, APRProofNodePrinter):
711-
def __init__(self, kevm: KEVM, proof: APRProof):
712-
KEVMNodePrinter.__init__(self, kevm)
713-
APRProofNodePrinter.__init__(self, proof, kevm)
712+
def __init__(self, kevm: KEVM, cterm_show: CTermShow, proof: APRProof, full_printer: bool = True):
713+
KEVMNodePrinter.__init__(self, kevm, cterm_show, full_printer=full_printer)
714+
APRProofNodePrinter.__init__(self, proof, cterm_show, full_printer=full_printer)
714715

715716

716-
def kevm_node_printer(kevm: KEVM, proof: APRProof) -> NodePrinter:
717+
def kevm_node_printer(kevm: KEVM, proof: APRProof, full_printer: bool = True) -> NodePrinter:
718+
cterm_show = CTermShow(PrettyPrinter(kevm.definition, patch_symbol_table=KEVM._kevm_patch_symbol_table).print)
717719
if type(proof) is APRProof:
718-
return KEVMAPRNodePrinter(kevm, proof)
720+
return KEVMAPRNodePrinter(kevm, cterm_show, proof, full_printer=full_printer)
719721
raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}')
720722

721723

‎kevm-pyk/src/kevm_pyk/kompile.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,7 @@ def _kompile_haskell() -> None:
224224

225225

226226
def lib_ccopts(plugin_dir: Path, debug_build: bool = False) -> list[str]:
227-
ccopts = ['-std=c++17']
227+
ccopts = ['-std=c++20']
228228

229229
if debug_build:
230230
ccopts += ['-g']

‎kevm-pyk/src/kevm_pyk/summarizer.py‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -613,7 +613,7 @@ def show_proof(
613613
omit_cells: Iterable[str] = (),
614614
) -> list[str]:
615615
node_printer = kevm_node_printer(self.kevm, proof)
616-
proof_show = APRProofShow(self.kevm, node_printer=node_printer)
616+
proof_show = APRProofShow(self.kevm.definition, node_printer=node_printer)
617617
return proof_show.show(
618618
proof,
619619
nodes=nodes,
@@ -841,7 +841,7 @@ def create_kcfg_explore() -> KCFGExplore:
841841

842842
def _to_rules(self, proof: APRProof) -> list[KRule]:
843843
krules = []
844-
module = APRProofShow(self.kevm, kevm_node_printer(self.kevm, proof)).kcfg_show.to_module(proof.kcfg)
844+
module = APRProofShow(self.kevm.definition, kevm_node_printer(self.kevm, proof)).kcfg_show.to_module(proof.kcfg)
845845
for krule in module.sentences:
846846
assert isinstance(krule, KRule), f'Unexpected sentence type: {type(krule)}\n{self.kevm.pretty_print(krule)}'
847847
body, requires, ensures, atts = krule.body, krule.requires, krule.ensures, krule.att

‎kevm-pyk/src/tests/integration/test_prove.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -425,7 +425,7 @@ def _validate_proofs(kevm: KEVM, kore_rpc_command: tuple[str, ...], proofs: list
425425
initialize_apr_proof(kcfg_explore.cterm_symbolic, proof)
426426
prover.advance_proof(proof, max_iterations=20)
427427
node_printer = kevm_node_printer(kevm, proof)
428-
proof_show = APRProofShow(kevm, node_printer=node_printer)
428+
proof_show = APRProofShow(kevm.definition, node_printer=node_printer)
429429
proof_display = '\n'.join(' ' + line for line in proof_show.show(proof))
430430
_LOGGER.info(f'Proof {proof.id}:\n{proof_display}')
431431
assert proof.passed

0 commit comments

Comments
 (0)