Skip to content

Commit 692a31c

Browse files
ehildenbrv-auditor
ehildenb
and
rv-auditor
authored
Adjustments to bug reports, enable collecting bug reports for all proofs (#2047)
* kevm-pyk/{cli,__main__,foundry}: use upstreamed KCLIArgs.bug_report_args * kevm-pyk/{test_prove,test_foundry_prove}: allow generating bug reports * Set Version: 1.0.280 * Set Version: 1.0.286 * Set Version: 1.0.287 * {kevm-pyk,kontrol}/__main__: add rpc_args * test_foundry_prove: remove use_booster arguments where not used * package/debian/changelog: fx merge conflict * kontrol/__main__: remove unused bug_report_args * Set Version: 1.0.289 --------- Co-authored-by: devops <[email protected]>
1 parent 7f1daf9 commit 692a31c

File tree

9 files changed

+79
-50
lines changed

9 files changed

+79
-50
lines changed

‎kevm-pyk/pyproject.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kevm-pyk"
7-
version = "1.0.288"
7+
version = "1.0.289"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

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

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@
2020
from pyk.proof.equality import EqualityProof
2121
from pyk.proof.show import APRProofShow
2222
from pyk.proof.tui import APRProofViewer
23-
from pyk.utils import BugReport, single
23+
from pyk.utils import single
2424

2525
from .cli import KEVMCLIArgs, node_id_like
2626
from .config import INCLUDE_DIR, KEVM_LIB
@@ -37,6 +37,7 @@
3737
from pyk.kast.outer import KClaim
3838
from pyk.kcfg.kcfg import NodeIdLike
3939
from pyk.proof.proof import Proof
40+
from pyk.utils import BugReport
4041

4142
T = TypeVar('T')
4243

@@ -127,7 +128,7 @@ def exec_prove_legacy(
127128
spec_file: Path,
128129
definition_dir: Path | None = None,
129130
includes: Iterable[str] = (),
130-
bug_report: bool = False,
131+
bug_report_legacy: bool = False,
131132
save_directory: Path | None = None,
132133
spec_module: str | None = None,
133134
claim_labels: Iterable[str] | None = None,
@@ -153,7 +154,7 @@ def exec_prove_legacy(
153154
final_state = kevm.prove_legacy(
154155
spec_file=spec_file,
155156
includes=include_dirs,
156-
bug_report=bug_report,
157+
bug_report=bug_report_legacy,
157158
spec_module=spec_module,
158159
claim_labels=claim_labels,
159160
exclude_claim_labels=exclude_claim_labels,
@@ -174,7 +175,7 @@ def exec_prove(
174175
spec_file: Path,
175176
includes: Iterable[str],
176177
definition_dir: Path | None = None,
177-
bug_report: bool = False,
178+
bug_report: BugReport | None = None,
178179
save_directory: Path | None = None,
179180
spec_module: str | None = None,
180181
claim_labels: Iterable[str] | None = None,
@@ -207,8 +208,7 @@ def exec_prove(
207208
if smt_retry_limit is None:
208209
smt_retry_limit = 10
209210

210-
br = BugReport(spec_file.with_suffix('.bug_report')) if bug_report else None
211-
kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=br)
211+
kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report)
212212

213213
include_dirs = [Path(include) for include in includes]
214214
include_dirs += [INCLUDE_DIR]
@@ -242,7 +242,7 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
242242
kevm,
243243
kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas),
244244
id=claim.label,
245-
bug_report=br,
245+
bug_report=bug_report,
246246
kore_rpc_command=kore_rpc_command,
247247
smt_timeout=smt_timeout,
248248
smt_retry_limit=smt_retry_limit,
@@ -571,6 +571,7 @@ def parse(s: str) -> list[T]:
571571
kevm_cli_args.k_args,
572572
kevm_cli_args.kprove_args,
573573
kevm_cli_args.rpc_args,
574+
kevm_cli_args.bug_report_args,
574575
kevm_cli_args.smt_args,
575576
kevm_cli_args.explore_args,
576577
kevm_cli_args.spec_args,
@@ -602,7 +603,7 @@ def parse(s: str) -> list[T]:
602603
)
603604
prune_proof_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.')
604605

605-
command_parser.add_parser(
606+
prove_legacy_args = command_parser.add_parser(
606607
'prove-legacy',
607608
help='Run KEVM proof using the legacy kprove binary.',
608609
parents=[
@@ -612,6 +613,9 @@ def parse(s: str) -> list[T]:
612613
kevm_cli_args.kprove_legacy_args,
613614
],
614615
)
616+
prove_legacy_args.add_argument(
617+
'--bug-report-legacy', default=False, action='store_true', help='Generate a legacy bug report.'
618+
)
615619

616620
command_parser.add_parser(
617621
'view-kcfg',

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

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -172,12 +172,6 @@ def foundry_test_args(self) -> ArgumentParser:
172172
@cached_property
173173
def rpc_args(self) -> ArgumentParser:
174174
args = ArgumentParser(add_help=False)
175-
args.add_argument(
176-
'--bug-report',
177-
default=False,
178-
action='store_true',
179-
help='Generate a haskell-backend bug report for the execution.',
180-
)
181175
args.add_argument(
182176
'--trace-rewrites',
183177
default=False,

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

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@
4242
from pyk.cterm import CTerm
4343
from pyk.kcfg.kcfg import NodeIdLike
4444
from pyk.kcfg.tui import KCFGElem
45+
from pyk.utils import BugReport
4546

4647
T = TypeVar('T')
4748

@@ -155,7 +156,7 @@ def exec_foundry_prove(
155156
break_on_jumpi: bool = False,
156157
break_on_calls: bool = True,
157158
bmc_depth: int | None = None,
158-
bug_report: bool = False,
159+
bug_report: BugReport | None = None,
159160
kore_rpc_command: str | Iterable[str] | None = None,
160161
use_booster: bool = False,
161162
smt_timeout: int | None = None,
@@ -289,7 +290,7 @@ def exec_foundry_simplify_node(
289290
replace: bool = False,
290291
minimize: bool = True,
291292
sort_collections: bool = False,
292-
bug_report: bool = False,
293+
bug_report: BugReport | None = None,
293294
smt_timeout: int | None = None,
294295
smt_retry_limit: int | None = None,
295296
trace_rewrites: bool = False,
@@ -323,7 +324,7 @@ def exec_foundry_step_node(
323324
node: NodeIdLike,
324325
repeat: int = 1,
325326
depth: int = 1,
326-
bug_report: bool = False,
327+
bug_report: BugReport | None = None,
327328
smt_timeout: int | None = None,
328329
smt_retry_limit: int | None = None,
329330
trace_rewrites: bool = False,
@@ -353,7 +354,6 @@ def exec_foundry_merge_nodes(
353354
test: str,
354355
id: str | None,
355356
nodes: Iterable[NodeIdLike],
356-
bug_report: bool = False,
357357
**kwargs: Any,
358358
) -> None:
359359
foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, id=id)
@@ -366,7 +366,7 @@ def exec_foundry_section_edge(
366366
edge: tuple[str, str],
367367
sections: int = 2,
368368
replace: bool = False,
369-
bug_report: bool = False,
369+
bug_report: BugReport | None = None,
370370
smt_timeout: int | None = None,
371371
smt_retry_limit: int | None = None,
372372
trace_rewrites: bool = False,
@@ -485,6 +485,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
485485
kevm_cli_args.kprove_args,
486486
kevm_cli_args.smt_args,
487487
kevm_cli_args.rpc_args,
488+
kevm_cli_args.bug_report_args,
488489
kevm_cli_args.explore_args,
489490
kevm_cli_args.foundry_args,
490491
],
@@ -579,6 +580,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
579580
kevm_cli_args.logging_args,
580581
kevm_cli_args.smt_args,
581582
kevm_cli_args.rpc_args,
583+
kevm_cli_args.bug_report_args,
582584
kevm_cli_args.display_args,
583585
kevm_cli_args.foundry_args,
584586
],
@@ -595,6 +597,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
595597
kevm_cli_args.foundry_test_args,
596598
kevm_cli_args.logging_args,
597599
kevm_cli_args.rpc_args,
600+
kevm_cli_args.bug_report_args,
598601
kevm_cli_args.smt_args,
599602
kevm_cli_args.foundry_args,
600603
],
@@ -631,6 +634,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]:
631634
kevm_cli_args.foundry_test_args,
632635
kevm_cli_args.logging_args,
633636
kevm_cli_args.rpc_args,
637+
kevm_cli_args.bug_report_args,
634638
kevm_cli_args.smt_args,
635639
kevm_cli_args.foundry_args,
636640
],

‎kevm-pyk/src/kontrol/foundry.py

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@
2727
from pyk.proof.proof import Proof
2828
from pyk.proof.reachability import APRBMCProof, APRProof
2929
from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter, APRProofShow
30-
from pyk.utils import BugReport, ensure_dir_path, hash_str, run_process, single, unique
30+
from pyk.utils import ensure_dir_path, hash_str, run_process, single, unique
3131

3232
from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics
3333
from kevm_pyk.utils import (
@@ -52,6 +52,7 @@
5252
from pyk.kcfg.kcfg import NodeIdLike
5353
from pyk.kcfg.tui import KCFGElem
5454
from pyk.proof.show import NodePrinter
55+
from pyk.utils import BugReport
5556

5657
_LOGGER: Final = logging.getLogger(__name__)
5758

@@ -620,7 +621,7 @@ def foundry_prove(
620621
break_on_jumpi: bool = False,
621622
break_on_calls: bool = True,
622623
bmc_depth: int | None = None,
623-
bug_report: bool = False,
624+
bug_report: BugReport | None = None,
624625
kore_rpc_command: str | Iterable[str] | None = None,
625626
use_booster: bool = False,
626627
smt_timeout: int | None = None,
@@ -636,8 +637,7 @@ def foundry_prove(
636637
if max_iterations is not None and max_iterations < 0:
637638
raise ValueError(f'Must have a non-negative number of iterations, found: --max-iterations {max_iterations}')
638639

639-
br = BugReport(foundry_root / 'bug_report') if bug_report else None
640-
foundry = Foundry(foundry_root, bug_report=br)
640+
foundry = Foundry(foundry_root, bug_report=bug_report)
641641

642642
foundry.mk_proofs_dir()
643643

@@ -728,7 +728,7 @@ def _init_and_run_proof(_init_problem: tuple[str, str, str | None]) -> tuple[boo
728728
foundry.kevm,
729729
kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas),
730730
id=test_id,
731-
bug_report=br,
731+
bug_report=bug_report,
732732
kore_rpc_command=kore_rpc_command,
733733
llvm_definition_dir=llvm_definition_dir,
734734
smt_timeout=smt_timeout,
@@ -917,14 +917,13 @@ def foundry_simplify_node(
917917
replace: bool = False,
918918
minimize: bool = True,
919919
sort_collections: bool = False,
920-
bug_report: bool = False,
920+
bug_report: BugReport | None = None,
921921
smt_timeout: int | None = None,
922922
smt_retry_limit: int | None = None,
923923
trace_rewrites: bool = False,
924924
port: int | None = None,
925925
) -> str:
926-
br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
927-
foundry = Foundry(foundry_root, bug_report=br)
926+
foundry = Foundry(foundry_root, bug_report=bug_report)
928927
test_id = foundry.get_test_id(test, id)
929928
apr_proof = foundry.get_apr_proof(test_id)
930929
cterm = apr_proof.kcfg.node(node).cterm
@@ -934,7 +933,7 @@ def foundry_simplify_node(
934933
foundry.kevm,
935934
kcfg_semantics=KEVMSemantics(),
936935
id=apr_proof.id,
937-
bug_report=br,
936+
bug_report=bug_report,
938937
smt_timeout=smt_timeout,
939938
smt_retry_limit=smt_retry_limit,
940939
trace_rewrites=trace_rewrites,
@@ -954,7 +953,7 @@ def foundry_merge_nodes(
954953
test: str,
955954
node_ids: Iterable[NodeIdLike],
956955
id: str | None = None,
957-
bug_report: bool = False,
956+
bug_report: BugReport | None = None,
958957
include_disjunct: bool = False,
959958
) -> None:
960959
def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
@@ -969,8 +968,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
969968
return False
970969
return True
971970

972-
br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
973-
foundry = Foundry(foundry_root, bug_report=br)
971+
foundry = Foundry(foundry_root, bug_report=bug_report)
974972
test_id = foundry.get_test_id(test, id)
975973
apr_proof = foundry.get_apr_proof(test_id)
976974

@@ -1003,7 +1001,7 @@ def foundry_step_node(
10031001
id: str | None = None,
10041002
repeat: int = 1,
10051003
depth: int = 1,
1006-
bug_report: bool = False,
1004+
bug_report: BugReport | None = None,
10071005
smt_timeout: int | None = None,
10081006
smt_retry_limit: int | None = None,
10091007
trace_rewrites: bool = False,
@@ -1014,8 +1012,7 @@ def foundry_step_node(
10141012
if depth < 1:
10151013
raise ValueError(f'Expected positive value for --depth, got: {depth}')
10161014

1017-
br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
1018-
foundry = Foundry(foundry_root, bug_report=br)
1015+
foundry = Foundry(foundry_root, bug_report=bug_report)
10191016
test_id = foundry.get_test_id(test, id)
10201017
apr_proof = foundry.get_apr_proof(test_id)
10211018
start_server = port is None
@@ -1024,7 +1021,7 @@ def foundry_step_node(
10241021
foundry.kevm,
10251022
kcfg_semantics=KEVMSemantics(),
10261023
id=apr_proof.id,
1027-
bug_report=br,
1024+
bug_report=bug_report,
10281025
smt_timeout=smt_timeout,
10291026
smt_retry_limit=smt_retry_limit,
10301027
trace_rewrites=trace_rewrites,
@@ -1043,14 +1040,13 @@ def foundry_section_edge(
10431040
id: str | None = None,
10441041
sections: int = 2,
10451042
replace: bool = False,
1046-
bug_report: bool = False,
1043+
bug_report: BugReport | None = None,
10471044
smt_timeout: int | None = None,
10481045
smt_retry_limit: int | None = None,
10491046
trace_rewrites: bool = False,
10501047
port: int | None = None,
10511048
) -> None:
1052-
br = BugReport(Path(f'{test}.bug_report')) if bug_report else None
1053-
foundry = Foundry(foundry_root, bug_report=br)
1049+
foundry = Foundry(foundry_root, bug_report=bug_report)
10541050
test_id = foundry.get_test_id(test, id)
10551051
apr_proof = foundry.get_apr_proof(test_id)
10561052
source_id, target_id = edge
@@ -1060,7 +1056,7 @@ def foundry_section_edge(
10601056
foundry.kevm,
10611057
kcfg_semantics=KEVMSemantics(),
10621058
id=apr_proof.id,
1063-
bug_report=br,
1059+
bug_report=bug_report,
10641060
smt_timeout=smt_timeout,
10651061
smt_retry_limit=smt_retry_limit,
10661062
trace_rewrites=trace_rewrites,

0 commit comments

Comments
 (0)