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

Replacing supported features scripts with assess #1922

Closed
6 tasks
tedinski opened this issue Nov 21, 2022 · 0 comments · Fixed by #2029
Closed
6 tasks

Replacing supported features scripts with assess #1922

tedinski opened this issue Nov 21, 2022 · 0 comments · Fixed by #2029
Assignees
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.

Comments

@tedinski
Copy link
Contributor

There are a few tasks that need doing to replace the scripts (located here) for measuring unsupported features with Assess.

  • Develop a JSON output format for Assess.
  • New unsupported features table for assess #1819 is required to reproduce the same metrics we currently produce. (This is a consequence of the switch to MIR linker.)
  • We should have a new mode for measuring unsupported features only. (As opposed to the current goal for assess, of running tests under Kani. To reproduce the current behavior we only need build information, not test running results. We'll want those later.)
  • The reachability mode needs changing as well. We should treat public functions as roots and NOT build in test mode for this.
  • We should produce a real aggregator that runs assess on all targets, reads the json outputs, and outputs aggregate results.
  • Finally, we should run this nightly.

Over time I suspect we'll want to experiment with the mode changing behaviors, to move towards more useful metrics than the current ones we're tracking. But to start we need to reproduce our current metrics, then starting changing things. So I suspect we'll want all of (codegen only, tests mode, pubfns/test fns) to be flags we can turn on/off.

@tedinski tedinski added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label Nov 21, 2022
@tedinski tedinski self-assigned this Nov 28, 2022
@tedinski tedinski added this to the Create Kani Assess tool milestone Nov 28, 2022
@tedinski tedinski moved this to In Progress in Kani 2023-01-23 Jan 3, 2023
@github-project-automation github-project-automation bot moved this to Done in Kani 0.17 Jan 4, 2023
@github-project-automation github-project-automation bot moved this to Done in Kani 0.18 Jan 4, 2023
@github-project-automation github-project-automation bot moved this from In Progress to Done in Kani 2023-01-23 Jan 4, 2023
@tedinski tedinski changed the title Tracking issue: Replacing supported features scripts with assess Replacing supported features scripts with assess Jan 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected.
Projects
No open projects
Status: Done
Status: Done
Status: Done
Development

Successfully merging a pull request may close this issue.

1 participant