From 5e541e2eb50e40b7fcc221bc856449f731f219de Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Tue, 1 Feb 2022 17:51:23 -0500 Subject: [PATCH 1/3] Don't use the broken overflow builtins for pointers --- .../cbmc/src/goto_program/expr.rs | 29 ++++++++++++------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index b9a291a4d79f..95e485def95d 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -9,6 +9,7 @@ use crate::InternedString; use num::bigint::BigInt; use std::collections::BTreeMap; use std::fmt::Debug; +use tracing::warn; /////////////////////////////////////////////////////////////////////////////////////////////// /// Datatypes @@ -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 => { @@ -851,13 +852,10 @@ 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())) - || (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. + OverflowMinus | OverflowMult | OverflowPlus => { + lhs.typ.is_integer() && rhs.typ.is_integer() } } } @@ -1205,7 +1203,18 @@ 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. + // Instead, we rely on `--pointer-overflow-check` in CBMC. + let overflowed = if self.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 } } From e3802325a56b2f0c62484dfbca5ba13ca9f3b861 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Wed, 2 Feb 2022 12:13:56 -0500 Subject: [PATCH 2/3] PR Comments --- src/kani-compiler/cbmc/src/goto_program/expr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index 95e485def95d..0df742918c15 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -855,7 +855,7 @@ impl Expr { // While one can technically use these on pointers, the result is treated as an integer. // This is almost never what you actually want. OverflowMinus | OverflowMult | OverflowPlus => { - lhs.typ.is_integer() && rhs.typ.is_integer() + lhs.typ == rhs.typ && lhs.typ.is_integer() } } } @@ -1206,7 +1206,7 @@ impl Expr { // FIXME: https://github.com/model-checking/kani/issues/786 // Overflow checking on pointers is hard to do at the IREP level. // Instead, we rely on `--pointer-overflow-check` in CBMC. - let overflowed = if self.typ.is_pointer() { + let overflowed = if self.typ.is_pointer() || e.typ.is_pointer() { warn!( "Overflow operations are not properly supported on pointer types {:?} {:?}", self, e From 09a8a59b2dd37d02837af7e0ed79f619cef3e0db Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Thu, 3 Feb 2022 14:09:26 -0500 Subject: [PATCH 3/3] better comments --- src/kani-compiler/cbmc/src/goto_program/expr.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index 0df742918c15..d13dc749d97a 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -854,6 +854,12 @@ impl Expr { // Overflow flags // 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() } @@ -1205,7 +1211,9 @@ impl Expr { let result = self.clone().plus(e.clone()); // FIXME: https://github.com/model-checking/kani/issues/786 // Overflow checking on pointers is hard to do at the IREP level. - // Instead, we rely on `--pointer-overflow-check` in CBMC. + // 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 {:?} {:?}",