Skip to content

Commit

Permalink
Merge branch 'master' into _update-deps/runtimeverification/evm-seman…
Browse files Browse the repository at this point in the history
…tics
  • Loading branch information
PetarMax authored Oct 9, 2024
2 parents e54a901 + c402a16 commit e17b6b1
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 18 deletions.
11 changes: 0 additions & 11 deletions src/kontrol/foundry.py
Original file line number Diff line number Diff line change
Expand Up @@ -959,16 +959,6 @@ def foundry_list(foundry: Foundry) -> list[str]:
return lines


def setup_exec_time(foundry: Foundry, contract: Contract) -> float:
setup_exec_time = 0.0
if 'setUp' in contract.method_by_name:
latest_version = foundry.latest_proof_version(f'{contract.name_with_path}.setUp()')
setup_digest = f'{contract.name_with_path}.setUp():{latest_version}'
apr_proof = APRProof.read_proof_data(foundry.proofs_dir, setup_digest)
setup_exec_time = apr_proof.exec_time
return setup_exec_time


def foundry_to_xml(foundry: Foundry, proofs: list[APRProof]) -> None:
testsuites = Et.Element(
'testsuites', tests='0', failures='0', errors='0', time='0', timestamp=str(datetime.datetime.now())
Expand All @@ -985,7 +975,6 @@ def foundry_to_xml(foundry: Foundry, proofs: list[APRProof]) -> None:
proof_exec_time = proof.exec_time
testsuite = testsuites.find(f'testsuite[@name={contract_name!r}]')
if testsuite is None:
proof_exec_time += setup_exec_time(foundry, foundry_contract)
testsuite = Et.SubElement(
testsuites,
'testsuite',
Expand Down
15 changes: 8 additions & 7 deletions src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,7 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
recorded_state_entries=recorded_state_entries,
)

constructor_results: list[APRProof] = []
if options.run_constructor:
constructor_tests = collect_constructors(foundry, contracts, reinit=options.reinit)
constructor_names = [test.name for test in constructor_tests]
Expand All @@ -156,8 +157,8 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
else:
console.print(f'[bold]Running initialization code for contracts in parallel:[/bold] {constructor_names}')

results = _run_prover(constructor_tests, include_summaries=False)
failed = [proof for proof in results if not proof.passed]
constructor_results = _run_prover(constructor_tests, include_summaries=False)
failed = [proof for proof in constructor_results if not proof.passed]
if failed:
raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}')

Expand All @@ -166,9 +167,9 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
else:
separator = '\n\t\t\t\t ' # ad-hoc separator for the string "Running setup functions in parallel: " below
console.print(f'[bold]Running setup functions in parallel:[/bold] {separator.join(setup_method_names)}')
results = _run_prover(setup_method_tests, include_summaries=False)
setup_results = _run_prover(setup_method_tests, include_summaries=False)

failed = [proof for proof in results if not proof.passed]
failed = [proof for proof in setup_results if not proof.passed]
if failed:
raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}')

Expand All @@ -177,12 +178,12 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
else:
separator = '\n\t\t\t\t ' # ad-hoc separator for the string "Running test functions in parallel: " below
console.print(f'[bold]Running test functions in parallel:[/bold] {separator.join(test_names)}')
results = _run_prover(test_suite, include_summaries=True)
test_results = _run_prover(test_suite, include_summaries=True)

if options.xml_test_report:
foundry_to_xml(foundry, results)
foundry_to_xml(foundry, constructor_results + setup_results + test_results)

return results
return test_results


class FoundryTest(NamedTuple):
Expand Down

0 comments on commit e17b6b1

Please sign in to comment.