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.

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

Don't use the broken overflow builtins for pointers #791

Closed
wants to merge 3 commits into from
Closed

Don't use the broken overflow builtins for pointers #791

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5e541e2
Don't use the broken overflow builtins for pointers
danielsn Feb 1, 2022
e380232
PR Comments
danielsn Feb 2, 2022
09a8a59
better comments
danielsn Feb 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 27 additions & 10 deletions src/kani-compiler/cbmc/src/goto_program/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ use crate::InternedString;
use num::bigint::BigInt;
use std::collections::BTreeMap;
use std::fmt::Debug;
use tracing::warn;

///////////////////////////////////////////////////////////////////////////////////////////////
/// Datatypes
Expand Down Expand Up @@ -813,8 +814,8 @@ impl Expr {
match op {
// Arithmetic which can include pointers
Minus => {
(lhs.typ == rhs.typ)
&& (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector())
((lhs.typ == rhs.typ)
&& (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector()))
|| (lhs.typ.is_pointer() && rhs.typ.is_integer())
}
Plus => {
Expand Down Expand Up @@ -851,13 +852,16 @@ impl Expr {
// Floating Point Equalities
IeeeFloatEqual | IeeeFloatNotequal => lhs.typ == rhs.typ && lhs.typ.is_floating_point(),
// Overflow flags
OverflowMinus => {
(lhs.typ == rhs.typ && (lhs.typ.is_pointer() || lhs.typ.is_numeric()))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good to restrict this case to integers because I do not think we were handling floating point numbers anyway.

|| (lhs.typ.is_pointer() && rhs.typ.is_integer())
}
OverflowMult | OverflowPlus => {
(lhs.typ == rhs.typ && lhs.typ.is_integer())
|| (lhs.typ.is_pointer() && rhs.typ.is_integer())
// While one can technically use these on pointers, the result is treated as an integer.
// This is almost never what you actually want.
// In particular, this check can unsoundly report no overflow on pointer operations:
// ```
// uint32_t *p = (SIZE_MAX-4);
// uint32_t *q = p+1; //overflows
// OverflowPlus(p,1); //calculates SIZE_MAX-3, reports NO OVERFLOW
// ```
OverflowMinus | OverflowMult | OverflowPlus => {
lhs.typ == rhs.typ && lhs.typ.is_integer()
}
}
}
Expand Down Expand Up @@ -1205,7 +1209,20 @@ impl Expr {
/// `ArithmeticOverflowResult r; >>>r.overflowed = builtin_add_overflow(self, e, &r.result)<<<`
pub fn add_overflow(self, e: Expr) -> ArithmeticOverflowResult {
let result = self.clone().plus(e.clone());
let overflowed = self.add_overflow_p(e);
// FIXME: https://github.com/model-checking/kani/issues/786
// Overflow checking on pointers is hard to do at the IREP level.
// In particular, the `__overflow` primitives check INTEGER (not pointer) arithmatic.
// So the `__add_overflow_p` value really only makes sense for integer arithmatic.
// For pointers, we rely on `--pointer-overflow-check` in CBMC.
let overflowed = if self.typ.is_pointer() || e.typ.is_pointer() {
warn!(
"Overflow operations are not properly supported on pointer types {:?} {:?}",
self, e
);
Expr::bool_false()
} else {
self.add_overflow_p(e)
};
ArithmeticOverflowResult { result, overflowed }
}

Expand Down