CONTRACTS: handle locals with composite types when checking assigns clauses #6818
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
remi-delmas-3000
requested review from
tautschnig,
feliperodri and
SaswatPadhi
as code owners
remi-delmas-3000
force-pushed
the
assigns-clause-local-arrays
branch
from
9766e9f to
78f92c9
Compare
tautschnig
approved these changes
Apr 20, 2022
| @@ -190,6 +190,34 @@ class cfg_infot | |||
| return locals.is_local(ident) || symbol.is_parameter; | |||
| } | |||
|
|
|||
| /// Returns true iff `expr` is a composite type access on a locally declared | |||
| /// or parameter symbol, without any dereference operations. | |||
| bool is_access_to_local_composite(const exprt &expr) const | |||
There was a problem hiding this comment.
I believe typecasts and byte extract expressions are also possible left-hand sides in goto programs.
remi-delmas-3000
force-pushed
the
assigns-clause-local-arrays
branch
from
78f92c9 to
4bc8724
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6818 +/- ##
========================================
Coverage 77.00% 77.01%
========================================
Files 1594 1594
Lines 184345 184417 +72
========================================
+ Hits 141957 142021 +64
- Misses 42388 42396 +8
Continue to review full report at Codecov.
|
remi-delmas-3000
force-pushed
the
assigns-clause-local-arrays
branch
2 times, most recently
from
4838f54 to
632828a
Compare
feliperodri
approved these changes
Apr 22, 2022
| @@ -11,6 +11,7 @@ Date: September 2021 | |||
| #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H | |||
| #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H | |||
|
|
|||
| // clang-format off | |||
There was a problem hiding this comment.
Why do we need to add this only in this file? Our https://github.com/diffblue/cbmc/blob/develop/.clang-format doesn't handle includes properly already?
Comment on lines
+218
to
+248
| else | ||
| { | ||
| throw unsupported_operation_exceptiont( | ||
| "is_local_composite_access: unexpected assignment to member of '" + | ||
| type.id_string() + "'"); | ||
| } | ||
| } | ||
| else if(expr.id() == ID_if) | ||
| { | ||
| return is_local_composite_access(to_if_expr(expr).true_case()) && | ||
| is_local_composite_access(to_if_expr(expr).false_case()); | ||
| } | ||
| else if(expr.id() == ID_typecast) | ||
| { | ||
| return is_local_composite_access(to_typecast_expr(expr).op()); | ||
| } | ||
| else if( | ||
| expr.id() == ID_byte_extract_little_endian || | ||
| expr.id() == ID_byte_extract_big_endian) | ||
| { | ||
| return is_local_composite_access(to_byte_extract_expr(expr).op()); | ||
| } | ||
| else if(expr.id() == ID_complex_real) | ||
| { | ||
| return is_local_composite_access(to_complex_real_expr(expr).op()); | ||
| } | ||
| else if(expr.id() == ID_complex_imag) | ||
| { | ||
| return is_local_composite_access(to_complex_imag_expr(expr).op()); | ||
| } | ||
| else |
There was a problem hiding this comment.
Can we not express this cases using regression tests?
Detect and skip checking assignments to members of local symbols that have composite types. Added debug output prints about tracked locations, detected local statics, checked or skipped assignments.
remi-delmas-3000
force-pushed
the
assigns-clause-local-arrays
branch
from
632828a to
d0b5fb4
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We now detect and skip checking assignments to members of local symbols that have composite types (i.e. local objects are not explicitly tracked and assignments to them are implicitly allowed).
As a results OOB accesses to locals must be checked using
--pointer-checks.Before, these assignments would cause assigns clause checking to systematically fail, because the targets are not tracked in the write set.
Added debug output prints (when
--verbosity 10) to give users insight into which targets are tracked, which local statics are automatically included in the write set, which assignments are checked or skipped.