Simplify byte extract: fix unconditional read from optional values #7376
Conversation
We did not take into account that pointer_offset_bits may have failed to produce an integer value. Observed on some SV-COMP benchmarks (busybox/od).
Codecov ReportBase: 78.35% // Head: 78.35% // Decreases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7376 +/- ##
===========================================
- Coverage 78.35% 78.35% -0.01%
===========================================
Files 1645 1645
Lines 190190 190182 -8
===========================================
- Hits 149031 149015 -16
- Misses 41159 41167 +8
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. |
| @@ -1680,15 +1680,19 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) | |||
| { | |||
| return op_byte_update.value(); | |||
| } | |||
| else if( | |||
| el_size.has_value() && | |||
| *el_size <= pointer_offset_bits(op_byte_update.value().type(), ns)) | |||
There was a problem hiding this comment.
Huh.. wasn't there even a compiler warning on that?
There was a problem hiding this comment.
This was invoking this piece of code:
https://github.com/diffblue/cbmc/blob/8848ad878da46bbcd0cedad634e235e6faf8cb17/src/nonstd/optional.hpp#L997..L1000
which will return false when the optionalt doesn't have a value.
We did not take into account that pointer_offset_bits may have failed to produce an integer value. Observed on some SV-COMP benchmarks (busybox/od).