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

Simplifier: c_bool (and others) are also bitvector types #8247

Merged
merged 1 commit into from
Jun 12, 2024

Conversation

tautschnig
Copy link
Collaborator

Remove simplifier's own is_bitvector_type in favour of using can_cast_type<bitvector_typet>, which will make sure that expressions like bitxor(false, false) over c_bool types gets simplified. Such expressions were seen in Kani (the C front-end would promote bitxor operands to int, and, therefore, not end up in this code path).

  • 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 added aws-high Kani Bugs or features of importance to Kani Rust Verifier labels Mar 20, 2024
Copy link

codecov bot commented Mar 20, 2024

Codecov Report

Attention: Patch coverage is 75.00000% with 6 lines in your changes are missing coverage. Please review.

Project coverage is 78.32%. Comparing base (905033e) to head (a697de0).
Report is 2 commits behind head on develop.

Files Patch % Lines
src/util/simplify_expr_int.cpp 66.66% 5 Missing ⚠️
unit/util/simplify_expr.cpp 88.88% 1 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8247      +/-   ##
===========================================
- Coverage    78.32%   78.32%   -0.01%     
===========================================
  Files         1721     1721              
  Lines       188210   188243      +33     
  Branches     18462    18517      +55     
===========================================
+ Hits        147416   147435      +19     
- Misses       40794    40808      +14     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@kroening
Copy link
Member

kroening commented May 1, 2024

Can we test this somehow? The simplifier may be a good use-case for unit tests.

@tautschnig tautschnig force-pushed the features/simp-c_bool branch from 1be9830 to c9bcfce Compare May 2, 2024 10:03
@tautschnig
Copy link
Collaborator Author

Can we test this somehow? The simplifier may be a good use-case for unit tests.

Done!

Remove simplifier's own is_bitvector_type in favour of using
can_cast_type<bitvector_typet>, which will make sure that expressions
like bitxor(false, false) over c_bool types gets simplified. Such
expressions were seen in Kani (the C front-end would promote bitxor
operands to int, and, therefore, not end up in this code path).
@kroening kroening merged commit e1ff0e0 into diffblue:develop Jun 12, 2024
38 of 40 checks passed
@tautschnig tautschnig deleted the features/simp-c_bool branch June 12, 2024 17:49
tautschnig added a commit to tautschnig/kani that referenced this pull request Aug 1, 2024
CBMC v6 includes diffblue/cbmc#8247, which fixes
the need for unwind attributes that were newly found to be necessary
when upgrading to nightly-2024-03-15 (model-checking#3084).

Resolves: model-checking#3088
tautschnig added a commit to model-checking/kani that referenced this pull request Aug 1, 2024
CBMC v6 includes diffblue/cbmc#8247, which fixes
the need for unwind attributes that were newly found to be necessary
when upgrading to nightly-2024-03-15 (#3084).

Resolves: #3088
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws-high Kani Bugs or features of importance to Kani Rust Verifier
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants