Smir linker in python, cargo integration to get all SMIR JSON #608
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* Do not use `--release`, as it may introduce constants we cannot currently decode * cater for the case when a SMIR JSON file does not have types nor functions
jberthold
commented
Jun 9, 2025
Comment on lines
123
to
161
| MULTI_CRATE_DIR = (Path(__file__).parent / 'data' / 'multi-crate').resolve(strict=True) | ||
| MULTI_CRATE_TESTS = list(MULTI_CRATE_DIR.glob('*/main-crate')) | ||
|
|
||
|
|
||
| @pytest.mark.parametrize( | ||
| 'main_crate', | ||
| MULTI_CRATE_TESTS, | ||
| ids=[spec.parent.stem for spec in MULTI_CRATE_TESTS], | ||
| ) | ||
| def test_multi_crate_exec(main_crate: Path, kmir: KMIR, update_expected_output: bool) -> None: | ||
| cargo = CargoProject(main_crate) | ||
|
|
||
| smirs = cargo.smir_files_for_project(clean=True) | ||
|
|
||
| if len(smirs) == 0: | ||
| raise Exception('empty smirs') | ||
|
|
||
| linked = link([SMIRInfo.from_file(f) for f in smirs]) | ||
|
|
||
| # results for `run` have unstable IDs so run a termination proof for testing | ||
| _, linked_file_str = tempfile.mkstemp() | ||
| linked_file = Path(linked_file_str) | ||
| linked.dump(linked_file) | ||
| opts = ProveRSOpts(linked_file, smir=True) | ||
| proof = kmir.prove_rs(opts) | ||
|
|
||
| printer = PrettyPrinter(kmir.definition) | ||
| cterm_show = CTermShow(printer.print) | ||
| display_opts = ShowOpts(linked_file.parent, proof.id, full_printer=False, smir_info=None, omit_current_body=False) | ||
| shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, proof, display_opts)) | ||
| show_res = '\n'.join(shower.show(proof)) | ||
|
|
||
| os.unlink(linked_file) | ||
|
|
||
| assert_or_update_show_output( | ||
| show_res, | ||
| main_crate.parent / 'output.expected', | ||
| update=update_expected_output, | ||
| ) |
There was a problem hiding this comment.
This is the new test, other changes in this file are just moving existing code.
ehildenb
approved these changes
Jun 9, 2025
|
Tested in |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
kmir link SMIR_JSON1 [SMIR_JSON2 ...] --output OUTPUT_SMIR_JSONCargoProjectobjectAlso in this PR:
prove_rsandprove_pinocchiotests up intest-integrationfor better load distribution