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

Jump to bottom

Remove --function option #2129

Closed
celinval opened this issue Jan 17, 2023 · 5 comments · Fixed by #3278
Closed

Remove --function option #2129

celinval opened this issue Jan 17, 2023 · 5 comments · Fixed by #3278
Assignees
@celinval
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code Z-Kani Compiler Issues that require some changes to the compiler
Milestone
Proof Caching

Comments

@celinval
Copy link
Contributor

Proposed change: We should include information about the public functions as part of the KaniMetadata when the reachability mode is pub_fns. We should stop merging all the metadata and goto binaries together.

Motivation: We have a special handling for --function today inside kani-driver because we cannot tell which artifacts are relevant to some function. So we just merge everything. If we treat functions as potential harnesses, we can get rid of the hack described above. We should also restrict the metadata to include functions that don't take any parameter.
@celinval celinval added [C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-Kani Compiler Issues that require some changes to the compiler labels Jan 17, 2023
@celinval celinval mentioned this issue Jan 17, 2023
Merged
4 tasks
@tedinski
Copy link
Contributor

We could also just search the symtab files directly, it might be simpler that way.

@celinval
Copy link
Contributor Author

Do we mean parse the symtab file or invoke some goto utility to print the functions available?

@tedinski
Copy link
Contributor

The former for now, and hopefully if we're able to directly generate goto binaries that will also come later with the ability to open and parse those

@celinval celinval self-assigned this Feb 23, 2023
@celinval celinval added this to the Proof Caching milestone Feb 23, 2023
@celinval celinval removed their assignment Feb 23, 2023
@celinval
Copy link
Contributor Author

I am leaning towards adding information to the Metadata because is more reliable and it will work well even with mangled names. Since this will only be done for the target crate, the cost shouldn't be too high.

@celinval celinval mentioned this issue May 12, 2023
Merged
4 tasks
celinval added a commit that referenced this issue May 16, 2023
@celinval
Perform reachability analysis on a per-harness basis (#2439)
2a09d79 
Kani compiler used to generate one `goto-program` for all harnesses in one crate. In some cases, this actually had a negative impact on the harness verification time. This was first reported in #1659

The main changes were done in the compiler's module `compiler_interface` and the module `project` from the driver. The compiler will now gather all the harnesses beforehand and it will perform reachability + codegen steps for each harness. All files related to a harness `goto-program` will follow the naming convention bellow:
```
<BASE_NAME>_<MANGLED_NAME>.<EXTENSION>
```
This applies to symtab / goto / type_map / restriction files.

The metadata file is still generated once per target crate, and its name is still the same (`<BASE_NAME>.kani-metadata.json`).

On the driver side, the way we process the artifacts have changed. The driver will now read the metadata for each crate, and collect all artifacts based on the symtab goto file that is recorded in the metadata of each harness.

These changes do not apply for `--function`. We still keep all artifacts based on the crate's `<BASE_NAME>` and we have a separate logic to handle that. Fixing this is captured by #2129.
@adpaco-aws adpaco-aws mentioned this issue Dec 20, 2023
Merged
@celinval celinval changed the title Improve how we handle --function Remove --function option Jun 19, 2024
@celinval
Copy link
Contributor Author

We no longer have a use for this flag. We used to keep it for the book runner, but we no longer use that. Users should use harnesses instead.

@celinval celinval self-assigned this Jun 19, 2024
@celinval celinval added the [I] Refactoring / Clean Up Refactoring or cleaning up of existing code label Jun 19, 2024
@celinval celinval mentioned this issue Jun 20, 2024
Merged
celinval added a commit that referenced this issue Jun 21, 2024
@celinval
Remove support for the unstable argument --function (#3278)
0d8675d 
This is a legacy argument that we have very limited support to. We kept
it around for bookrunner tests, which has been removed already.

Resolves #2129
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. [I] Refactoring / Clean Up Refactoring or cleaning up of existing code Z-Kani Compiler Issues that require some changes to the compiler
Projects
None yet
Milestone
Proof Caching
Development

Successfully merging a pull request may close this issue.

Remove support for the unstable argument --function celinval/kani-dev
2 participants
@tedinski @celinval