Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Output counterexamples for failed Foundry proofs #1946

Merged
merged 15 commits into from
Jul 12, 2023
Merged

Output counterexamples for failed Foundry proofs #1946

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
c9e37f3
Showing counterexamples for failed Foundry tests
palinatolmach Jun 30, 2023
b51288c
Add `smt-hook` to `chop` for SMT solving
palinatolmach Jun 30, 2023
89c0085
Prettier counterexample printing
palinatolmach Jun 30, 2023
28bedb6
Revert `smtlib` -> `smt-hook` change to `chop`
palinatolmach Jul 5, 2023
f95834e
Fixed Discord link, counterexample error message
palinatolmach Jul 6, 2023
7bfa8df
Refactor `print_failure_info`, add counterexamples
palinatolmach Jul 7, 2023
988e9e9
Add `foundry-get-model` command
palinatolmach Jul 7, 2023
c7b11d8
Fix merge conflicts
palinatolmach Jul 7, 2023
cd569a7
Show Discord invite once in `print_failure_info`
palinatolmach Jul 7, 2023
b9130b9
Minor code quality fix
palinatolmach Jul 7, 2023
c283305
Set Version: 1.0.232
Jul 10, 2023
c9d786f
Minor code refactor; update tests w/new output
palinatolmach Jul 11, 2023
6d0257a
Remove pending nodes model generation by default
palinatolmach Jul 11, 2023
53142aa
Add `--counterexample-information` to prove, show
palinatolmach Jul 11, 2023
dfb0c1b
Use `counterexample_info=True` in Foundry tests
palinatolmach Jul 11, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion kevm-pyk/pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kevm-pyk"
version = "1.0.231"
version = "1.0.232"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
49 changes: 49 additions & 0 deletions kevm-pyk/src/kevm_pyk/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
from .cli import KEVMCLIArgs, node_id_like
from .foundry import (
Foundry,
foundry_get_model,
foundry_kompile,
foundry_list,
foundry_node_printer,
Expand Down Expand Up @@ -526,6 +527,7 @@ def exec_foundry_prove(
smt_timeout: int | None = None,
smt_retry_limit: int | None = None,
failure_info: bool = True,
counterexample_info: bool = False,
trace_rewrites: bool = False,
auto_abstract_gas: bool = False,
**kwargs: Any,
Expand Down Expand Up @@ -555,6 +557,7 @@ def exec_foundry_prove(
bug_report=bug_report,
kore_rpc_command=kore_rpc_command,
use_booster=use_booster,
counterexample_info=counterexample_info,
smt_timeout=smt_timeout,
smt_retry_limit=smt_retry_limit,
trace_rewrites=trace_rewrites,
Expand Down Expand Up @@ -588,6 +591,7 @@ def exec_foundry_show(
pending: bool = False,
failing: bool = False,
failure_info: bool = False,
counterexample_info: bool = False,
**kwargs: Any,
) -> None:
output = foundry_show(
Expand All @@ -602,6 +606,7 @@ def exec_foundry_show(
pending=pending,
failing=failing,
failure_info=failure_info,
counterexample_info=counterexample_info,
)
print(output)

Expand Down Expand Up @@ -750,6 +755,24 @@ def exec_foundry_section_edge(
)


def exec_foundry_get_model(
foundry_root: Path,
test: str,
nodes: Iterable[NodeIdLike] = (),
pending: bool = False,
failing: bool = False,
**kwargs: Any,
) -> None:
output = foundry_get_model(
foundry_root=foundry_root,
test=test,
nodes=nodes,
pending=pending,
failing=failing,
)
print(output)


# Helpers


Expand Down Expand Up @@ -1058,6 +1081,32 @@ def parse(s: str) -> list[T]:
'--sections', type=int, default=2, help='Number of sections to make from edge (>= 2).'
)

foundry_get_model = command_parser.add_parser(
'foundry-get-model',
help='Display a model for a given node.',
parents=[
kevm_cli_args.logging_args,
kevm_cli_args.rpc_args,
kevm_cli_args.smt_args,
kevm_cli_args.foundry_args,
],
)
foundry_get_model.add_argument('test', type=str, help='Display the models of nodes in this test.')
foundry_get_model.add_argument(
'--node',
type=node_id_like,
dest='nodes',
default=[],
action='append',
help='List of nodes to display the models of.',
)
foundry_get_model.add_argument(
'--pending', dest='pending', default=False, action='store_true', help='Also display models of pending nodes'
)
foundry_get_model.add_argument(
'--failing', dest='failing', default=False, action='store_true', help='Also display models of failing nodes'
)

return parser


Expand Down
14 changes: 14 additions & 0 deletions kevm-pyk/src/kevm_pyk/cli.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -283,6 +283,13 @@ def explore_args(self) -> ArgumentParser:
action='store_true',
help='Automatically extract gas cell when infinite gas is enabled',
)
args.add_argument(
'--counterexample-information',
dest='counterexample_info',
default=False,
action='store_true',
help='Show models for failing nodes.',
)
return args

@cached_property
Expand Down Expand Up @@ -345,4 +352,11 @@ def kcfg_show_args(self) -> ArgumentParser:
args.add_argument(
'--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes'
)
args.add_argument(
'--counterexample-information',
dest='counterexample_info',
default=False,
action='store_true',
help="Show models for failing nodes. Should be called with the '--failure-information' flag",
)
return args
48 changes: 44 additions & 4 deletions kevm-pyk/src/kevm_pyk/foundry.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,13 +37,14 @@
constraints_for,
kevm_prove,
print_failure_info,
print_model,
)

if TYPE_CHECKING:
from collections.abc import Iterable
from typing import Any, Final

from pyk.kast import KInner
from pyk.kast.inner import KInner
from pyk.kcfg.kcfg import NodeIdLike
from pyk.kcfg.tui import KCFGElem
from pyk.proof.show import NodePrinter
Expand Down Expand Up @@ -427,6 +428,7 @@ def foundry_prove(
smt_timeout: int | None = None,
smt_retry_limit: int | None = None,
failure_info: bool = True,
counterexample_info: bool = False,
trace_rewrites: bool = False,
auto_abstract_gas: bool = False,
) -> dict[str, tuple[bool, list[str] | None]]:
Expand Down Expand Up @@ -561,8 +563,7 @@ def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str]
)
failure_log = None
if not passed:
failure_log = print_failure_info(proof, kcfg_explore)

failure_log = print_failure_info(proof, kcfg_explore, counterexample_info)
return passed, failure_log

def run_cfg_group(tests: list[str]) -> dict[str, tuple[bool, list[str] | None]]:
Expand Down Expand Up @@ -597,6 +598,7 @@ def foundry_show(
pending: bool = False,
failing: bool = False,
failure_info: bool = False,
counterexample_info: bool = False,
) -> str:
contract_name = test.split('.')[0]
foundry = Foundry(foundry_root)
Expand Down Expand Up @@ -639,7 +641,7 @@ def _short_info(cterm: CTerm) -> Iterable[str]:

if failure_info:
with KCFGExplore(foundry.kevm, id=proof.id) as kcfg_explore:
res_lines += print_failure_info(proof, kcfg_explore)
res_lines += print_failure_info(proof, kcfg_explore, counterexample_info)
res_lines += Foundry.help_info()

return '\n'.join(res_lines)
Expand Down Expand Up @@ -795,6 +797,44 @@ def foundry_section_edge(
apr_proof.write_proof()


def foundry_get_model(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function should produce a data structure (maybe FoundryModel | None). Function print_model can be a method on this class (without the "Failed to ..." branch). Function print_failure_info then can be redefined as

def print_failure_info(kprint: KPrint, proof: Proof, *, model: FoundryModel | None = None) -> list[str]:
    ...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, I agree! Will add the FoundryModel class and modify the printing functions accordingly (there's some more refactoring to be done, as suggested by @nwatson22), but I need a bit more time to work on it. Would you recommend to merge the current PR and refactor it later, or should I include this change in this PR? Thank you!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's fine either way. If you decide to merge now, please open an issue to document the requested changes.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Issue created: #1955

foundry_root: Path,
test: str,
nodes: Iterable[NodeIdLike] = (),
pending: bool = False,
failing: bool = False,
) -> str:
contract_name = test.split('.')[0]
foundry = Foundry(foundry_root)
proofs_dir = foundry.out / 'apr_proofs'

contract_name, test_name = test.split('.')
proof_digest = foundry.proof_digest(contract_name, test_name)
proof = Proof.read_proof(proof_digest, proofs_dir)
assert isinstance(proof, APRProof)

if not nodes:
_LOGGER.warning('Node ID is not provided. Displaying models of failing and pending nodes:')
failing = pending = True

if pending:
nodes = list(nodes) + [node.id for node in proof.pending]
if failing:
nodes = list(nodes) + [node.id for node in proof.failing]
nodes = unique(nodes)

res_lines = []

with KCFGExplore(foundry.kevm, id=proof.id) as kcfg_explore:
for node_id in nodes:
res_lines.append('')
res_lines.append(f'Node id: {node_id}')
node = proof.kcfg.node(node_id)
res_lines.extend(print_model(node, kcfg_explore))

return '\n'.join(res_lines)


def _write_cfg(cfg: KCFG, path: Path) -> None:
path.write_text(cfg.to_json())
_LOGGER.info(f'Updated CFG file: {path}')
Expand Down
31 changes: 23 additions & 8 deletions kevm-pyk/src/kevm_pyk/utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
from typing import TYPE_CHECKING

from pyk.cterm import CTerm
from pyk.kast.inner import KApply, KRewrite, KVariable, Subst
from pyk.kast.inner import KApply, KInner, KRewrite, KVariable, Subst
from pyk.kast.manip import (
abstract_term_safely,
bottom_up,
Expand All @@ -25,9 +25,8 @@
from collections.abc import Callable, Collection, Iterable
from typing import Final, TypeVar

from pyk.kast import KInner
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg import KCFG, KCFGExplore
from pyk.ktool.kprove import KProve
from pyk.proof.proof import Proof
from pyk.utils import BugReport
Expand Down Expand Up @@ -177,7 +176,7 @@ def kevm_prove(
return False


def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]:
def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> list[str]:
if type(proof) is APRProof or type(proof) is APRBMCProof:
target = proof.kcfg.node(proof.target)

Expand Down Expand Up @@ -213,11 +212,13 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]:

res_lines.append(' Path condition:')
res_lines += [f' {kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))}']
if counterexample_info:
res_lines.extend(print_model(node, kcfg_explore))

res_lines.append('')
res_lines.append(
'Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD'
)
res_lines.append('')
res_lines.append(
'Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN'
)

return res_lines
elif type(proof) is EqualityProof:
Expand All @@ -226,6 +227,20 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]:
raise ValueError('Unknown proof type.')


def print_model(node: KCFG.Node, kcfg_explore: KCFGExplore) -> list[str]:
res_lines: list[str] = []
result_subst = kcfg_explore.cterm_get_model(node.cterm)
if type(result_subst) is Subst:
res_lines.append(' Model:')
for var, term in result_subst.to_dict().items():
term_kast = KInner.from_dict(term)
res_lines.append(f' {var} = {kcfg_explore.kprint.pretty_print(term_kast)}')
else:
res_lines.append(' Failed to generate a model.')

return res_lines
Comment on lines +230 to +241
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We rewrote the print_failure_info function in pyk to separate the printing from the RPC calls here: runtimeverification/pyk@6c28b66
Possibly we would want to do something similar here, since it makes testing cleaner. I realized we haven't updated kevm to use that function yet and we still just use the kevm version, so actually we can probably just refactor this when we make those changes later.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks Noah! I can probably try integrating the new failure_info function into kevm to include it in this PR, if this works--will update you on that tomorrow.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, didn't have a chance to do this, and I'll unfortunately be travelling starting tomorrow. Could you please advise if we should merge it in as it is and refactor print_failure_info later? I'll create a separate issue for it, in this case.



def arg_pair_of(
fst_type: Callable[[str], T1], snd_type: Callable[[str], T2], delim: str = ','
) -> Callable[[str], tuple[T1, T2]]:
Expand Down
2 changes: 2 additions & 0 deletions kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -677,4 +677,6 @@ module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:D9767505A49B578A77DD3E9B8A9FE01E
endmodule
0 Failure nodes. (0 pending and 0 failing)

Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
6 changes: 5 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -894,7 +894,11 @@ Failing nodes:
#And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
#Top
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
6 changes: 5 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1350,7 +1350,11 @@ Failing nodes:
#And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
#Top
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
6 changes: 5 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -894,7 +894,11 @@ Failing nodes:
#And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
#Top
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
2 changes: 2 additions & 0 deletions kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -677,4 +677,6 @@ module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:E200EADD2408C03C6CCDB315095224AC1D58D
endmodule
0 Failure nodes. (0 pending and 0 failing)

Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
7 changes: 6 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1793,7 +1793,12 @@ Failing nodes:
#And { true #Equals VV0_x_114b9705:Int <Int pow256 } ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
{ true #Equals ( notBool 100 <=Int VV0_x_114b9705:Int ) }
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0
VV0_x_114b9705 = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
8 changes: 7 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1811,7 +1811,13 @@ Failing nodes:
#And { true #Equals VV1_y_114b9705:Int <Int pow256 } ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
{ true #Equals VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int }
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0
VV0_x_114b9705 = 0
VV1_y_114b9705 = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
8 changes: 7 additions & 1 deletion kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1355,7 +1355,13 @@ Failing nodes:
#And { true #Equals VV1_b_114b9705:Int <Int pow256 } ) ) ) ) ) ) ) ) #Implies { false #Equals foundry_success ( ... statusCode: EVMC_SUCCESS , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
Path condition:
#Top
Model:
CALLER_ID = 0
NUMBER_CELL = 0
ORIGIN_ID = 0
VV0_a_114b9705 = 0
VV1_b_114b9705 = 0

Join the Runtime Verification Discord server for support: https://discord.gg/GHvFbRDD
Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN

Access documentation for KEVM foundry integration at https://docs.runtimeverification.com/kevm-integration-for-foundry/
Loading