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.

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

Track metrics for core and std crates, add loop metrics #258

Merged
merged 16 commits into from
Mar 21, 2025

Conversation

tautschnig
Copy link
Member

@tautschnig tautschnig commented Feb 24, 2025

The crate that we compute metrics for is now configurable when invoking kani_std_analysis.py. Should we find a need for further crates beyond core or std we just need to invoke it more times.

We are now also reporting loop/no-loop information across all the kinds of functions we are tracking as metrics.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

The crate that we compute metrics for is now configurable when invoking
`kani_std_analysis.py`. Should we find a need for further crates beyond
`core` or `std` we just need to invoke it more times.
@tautschnig tautschnig requested a review from a team as a code owner February 24, 2025 15:46
Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

Thanks for doing this!

@tautschnig tautschnig changed the title Track metrics for core and std crates Track metrics for core and std cratess, add loop metrics Feb 25, 2025
Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

Thanks!

@tautschnig
Copy link
Member Author

We might want #261 to be merged first and we need model-checking/kani#3915 to be merged.

@carolynzech carolynzech changed the title Track metrics for core and std cratess, add loop metrics Track metrics for core and std crates, add loop metrics Mar 3, 2025
@tautschnig tautschnig self-assigned this Mar 13, 2025
@tautschnig
Copy link
Member Author

This is now working as expected, see tautschnig#11.

@tautschnig tautschnig removed their assignment Mar 20, 2025
@thanhnguyen-aws thanhnguyen-aws self-assigned this Mar 20, 2025
@tautschnig tautschnig added this pull request to the merge queue Mar 20, 2025
@carolynzech carolynzech removed this pull request from the merge queue due to a manual request Mar 20, 2025
Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

Can you revert the changes to the submodules before we merge this?
Also, have you tested the plotting functionality to make sure that it renders okay even though the earlier dates don't have these datapoints?

@tautschnig
Copy link
Member Author

Can you revert the changes to the submodules before we merge this?

Thank you for catching this! (This is now fixed.)

Also, have you tested the plotting functionality to make sure that it renders okay even though the earlier dates don't have these datapoints?

With the data from tautschnig#11 we get the following for the core crate (where we had data, but only a subset of the datapoints):

core_safe_abstractions_metrics
core_safe_metrics
core_unsafe_metrics

And for the std crate (where we had no data at all):

std_safe_abstractions_metrics
std_safe_metrics
std_unsafe_metrics

I believe these match expectations.

@carolynzech
Copy link

carolynzech commented Mar 20, 2025

I believe these match expectations.

The purple entry in the legend on the first graph looks off? But otherwise LGTM

@tautschnig
Copy link
Member Author

Fixed by adding a missing comma. Now it looks better:

core_safe_abstractions_metrics

@carolynzech carolynzech enabled auto-merge March 20, 2025 21:24
@carolynzech carolynzech added this pull request to the merge queue Mar 20, 2025
Merged via the queue into model-checking:main with commit 9aa99c3 Mar 21, 2025
15 of 17 checks passed
@tautschnig tautschnig deleted the metrics-std branch March 21, 2025 07:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants