Skip to content

Field sensitivity for unions #7230

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
Merged
merged 1 commit into from
Nov 22, 2022
Merged

Field sensitivity for unions #7230

merged 1 commit into from
Nov 22, 2022

Conversation

tautschnig
Copy link
Collaborator

Field-sensitive tracking of unions permits propagating constants even when those do not affect the full width of the union (implying that some bits remain non-constant).

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this Oct 10, 2022
This was referenced Oct 10, 2022
Closed
Closed
@tautschnig tautschnig added Performance Optimisations Kani Bugs or features of importance to Kani Rust Verifier labels Oct 12, 2022
@feliperodri feliperodri added aws Bugs or features of importance to AWS CBMC users aws-high labels Oct 12, 2022
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch 2 times, most recently from c6c2eb5 to 5ff4248 Compare October 18, 2022 11:09
@codecov
Copy link

codecov bot commented Oct 18, 2022 •
edited
Loading

Codecov Report

Base: 78.25% // Head: 78.27% // Increases project coverage by +0.02% 🎉

Coverage data is based on head (50dbf7e) compared to base (2693a07).
Patch coverage: 97.42% of modified lines in pull request are covered.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7230      +/-   ##
===========================================
+ Coverage    78.25%   78.27%   +0.02%     
===========================================
  Files         1642     1642              
  Lines       189763   189922     +159     
===========================================
+ Hits        148490   148655     +165     
+ Misses       41273    41267       -6
Impacted Files Coverage Δ
src/util/simplify_expr_class.h 90.47% <ø> (ø)
src/goto-programs/goto_trace.cpp 81.51% <83.33%> (+0.09%) ⬆️
src/goto-symex/field_sensitivity.cpp 93.03% <95.95%> (+1.41%) ⬆️
src/goto-programs/goto_trace.h 100.00% <100.00%> (ø)
src/goto-programs/rewrite_union.cpp 100.00% <100.00%> (ø)
src/goto-symex/build_goto_trace.cpp 87.86% <100.00%> (+0.24%) ⬆️
src/goto-symex/field_sensitivity.h 100.00% <100.00%> (ø)
src/goto-symex/goto_symex_state.cpp 91.82% <100.00%> (+0.11%) ⬆️
src/goto-symex/symex_assign.cpp 81.56% <100.00%> (+0.13%) ⬆️
src/goto-symex/symex_dead.cpp 100.00% <100.00%> (ø)
... and 13 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch 3 times, most recently from dfd74be to 11f54ad Compare October 19, 2022 15:16
@tautschnig tautschnig mentioned this pull request Oct 19, 2022
Closed
3 tasks
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch 2 times, most recently from 3cf746e to 40f59a6 Compare October 21, 2022 10:16
@tautschnig tautschnig changed the title WIP: Field sensitivity for unions Field sensitivity for unions Oct 21, 2022
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch 2 times, most recently from 7d2d07b to 96b0484 Compare October 27, 2022 15:07
@tautschnig tautschnig mentioned this pull request Oct 27, 2022
Merged
2 tasks
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch from 96b0484 to 08dd144 Compare November 3, 2022 18:52
@tautschnig tautschnig marked this pull request as ready for review November 3, 2022 18:52
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch from 08dd144 to 1d49284 Compare November 3, 2022 19:31
@tautschnig tautschnig removed their assignment Nov 3, 2022
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch from 1d49284 to 5d1964d Compare November 6, 2022 22:12
@tautschnig
Field sensitivity for unions
50dbf7e 
Field-sensitive tracking of unions permits propagating constants even
when those do not affect the full width of the union (implying that some
bits remain non-constant).
@tautschnig tautschnig force-pushed the feature/union-field-sensitivity branch from 5d1964d to 50dbf7e Compare November 7, 2022 14:12
This was referenced Nov 9, 2022
Closed
Closed
@peterschrammel peterschrammel removed their assignment Nov 22, 2022
@tautschnig tautschnig merged commit f1aaf5b into diffblue:develop Nov 22, 2022
@tautschnig tautschnig deleted the feature/union-field-sensitivity branch November 22, 2022 10:38
This was referenced Feb 4, 2023
Merged
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

Assignees

@kroening kroening

Labels
aws Bugs or features of importance to AWS CBMC users aws-high Kani Bugs or features of importance to Kani Rust Verifier Performance Optimisations
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@tautschnig @peterschrammel @kroening @feliperodri