From de0f0b8013a4f74777a96b44beab7253e8e75297 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 29 Mar 2022 16:04:16 -0700 Subject: [PATCH 1/2] Use 2's complement when computing the relative discriminant to avoid signed to unsigned overflow failures --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 34 ++++++++++++++++--- tests/kani/Enum/neg_discriminant.rs | 29 ++++++++++++++++ tests/kani/LexicographicCmp/main.rs | 10 ++++++ 3 files changed, 69 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Enum/neg_discriminant.rs create mode 100644 tests/kani/LexicographicCmp/main.rs diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index b90e661046c1..381c446f36b5 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -447,6 +447,8 @@ impl<'tcx> GotocCtx<'tcx> { e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty)) } TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { + // This code follows the logic in the cranelift codegen backend: + // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116 let offset = match &layout.fields { FieldsShape::Arbitrary { offsets, .. } => offsets[0].bytes_usize(), _ => unreachable!("niche encoding must have arbitrary fields"), @@ -457,8 +459,32 @@ impl<'tcx> GotocCtx<'tcx> { let relative_discr = if *niche_start == 0 { niche_val } else { - // This should be a wrapping sub. - niche_val.sub(Expr::int_constant(*niche_start, discr_ty.clone())) + // Compute "niche_val - niche_start" where "-" is + // wrapping subtraction, i.e., the result should be + // interpreted as an unsigned value. + // While this can be done through a regular subtraction + // and then casting the result to an unsigned, doing so + // may result in CBMC flagging the operation with a + // signed to unsigned overflow failure (see + // https://github.com/model-checking/kani/issues/356). + // To avoid those overflow failures, the wrapping + // subtraction operation is computed as: + // if niche_val >= niche_start { + // // result is positive, so overflow may not occur + // niche_val - niche_start + // } else { + // // compute the 2's complement to avoid overflow + // niche_val - niche_start + 2^32 + // } + let s64 = Type::signed_int(64); + let niche_val = niche_val.cast_to(s64.clone()); + let twos_complement: i64 = + u32::MAX as i64 + 1 - i64::try_from(*niche_start).unwrap(); + let niche_start = Expr::int_constant(*niche_start, s64.clone()); + niche_val.clone().ge(niche_start.clone()).ternary( + niche_val.clone().sub(niche_start), + niche_val.plus(Expr::int_constant(twos_complement, s64)), + ) }; let relative_max = niche_variants.end().as_u32() - niche_variants.start().as_u32(); @@ -467,8 +493,8 @@ impl<'tcx> GotocCtx<'tcx> { } else { relative_discr .clone() - .cast_to(Type::unsigned_int(64)) - .le(Expr::int_constant(relative_max, Type::unsigned_int(64))) + .cast_to(Type::unsigned_int(128)) + .le(Expr::int_constant(relative_max, Type::unsigned_int(128))) }; let niche_discr = { let relative_discr = if relative_max == 0 { diff --git a/tests/kani/Enum/neg_discriminant.rs b/tests/kani/Enum/neg_discriminant.rs new file mode 100644 index 000000000000..94d4bdf07bd2 --- /dev/null +++ b/tests/kani/Enum/neg_discriminant.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that enums with negative discriminants are handled correctly + +enum Foo { + A = -500, + B = -200, + C = -100, + D = 0, + E = 1, + F = 256, +} + +#[kani::proof] +fn main() { + let a = Some(Foo::A); + let b = Some(Foo::B); + let c = Some(Foo::C); + let d = Some(Foo::D); + let e = Some(Foo::E); + let f = Some(Foo::F); + let _ = matches!(a, Some(Foo::A)); + let _ = matches!(b, Some(Foo::B)); + let _ = matches!(c, Some(Foo::C)); + let _ = matches!(d, Some(Foo::D)); + let _ = matches!(e, Some(Foo::E)); + let _ = matches!(f, Some(Foo::F)); +} diff --git a/tests/kani/LexicographicCmp/main.rs b/tests/kani/LexicographicCmp/main.rs new file mode 100644 index 000000000000..9f245cc3870a --- /dev/null +++ b/tests/kani/LexicographicCmp/main.rs @@ -0,0 +1,10 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that lexicographic comparison is handled correctly + +#[kani::proof] +fn main() { + assert!([1, 2, 3] < [1, 3, 4]); + assert!("World" >= "Hello"); +} From 9f60f533f032364a5a56a9b45dd7571797c58b23 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 30 Mar 2022 11:10:06 -0700 Subject: [PATCH 2/2] Address PR comments --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 57 ++++++++++--------- tests/kani/Enum/neg_discriminant.rs | 14 ++--- tests/kani/LexicographicCmp/main.rs | 2 +- 3 files changed, 37 insertions(+), 36 deletions(-) diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 381c446f36b5..21dd75e7f0d2 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -459,32 +459,7 @@ impl<'tcx> GotocCtx<'tcx> { let relative_discr = if *niche_start == 0 { niche_val } else { - // Compute "niche_val - niche_start" where "-" is - // wrapping subtraction, i.e., the result should be - // interpreted as an unsigned value. - // While this can be done through a regular subtraction - // and then casting the result to an unsigned, doing so - // may result in CBMC flagging the operation with a - // signed to unsigned overflow failure (see - // https://github.com/model-checking/kani/issues/356). - // To avoid those overflow failures, the wrapping - // subtraction operation is computed as: - // if niche_val >= niche_start { - // // result is positive, so overflow may not occur - // niche_val - niche_start - // } else { - // // compute the 2's complement to avoid overflow - // niche_val - niche_start + 2^32 - // } - let s64 = Type::signed_int(64); - let niche_val = niche_val.cast_to(s64.clone()); - let twos_complement: i64 = - u32::MAX as i64 + 1 - i64::try_from(*niche_start).unwrap(); - let niche_start = Expr::int_constant(*niche_start, s64.clone()); - niche_val.clone().ge(niche_start.clone()).ternary( - niche_val.clone().sub(niche_start), - niche_val.plus(Expr::int_constant(twos_complement, s64)), - ) + wrapping_sub(&niche_val, *niche_start) }; let relative_max = niche_variants.end().as_u32() - niche_variants.start().as_u32(); @@ -493,8 +468,7 @@ impl<'tcx> GotocCtx<'tcx> { } else { relative_discr .clone() - .cast_to(Type::unsigned_int(128)) - .le(Expr::int_constant(relative_max, Type::unsigned_int(128))) + .le(Expr::int_constant(relative_max, relative_discr.typ().clone())) }; let niche_discr = { let relative_discr = if relative_max == 0 { @@ -1249,3 +1223,30 @@ impl<'tcx> GotocCtx<'tcx> { } } } + +/// Perform a wrapping subtraction of an Expr with a constant "expr - constant" +/// where "-" is wrapping subtraction, i.e., the result should be interpreted as +/// an unsigned value (2's complement). +fn wrapping_sub(expr: &Expr, constant: u128) -> Expr { + // While the wrapping subtraction can be done through a regular subtraction + // and then casting the result to an unsigned, doing so may result in CBMC + // flagging the operation with a signed to unsigned overflow failure (see + // https://github.com/model-checking/kani/issues/356). + // To avoid those overflow failures, the wrapping subtraction operation is + // computed as: + // if expr >= constant { + // // result is positive, so overflow may not occur + // expr - constant + // } else { + // // compute the 2's complement to avoid overflow + // expr - constant + 2^32 + // } + let s64 = Type::signed_int(64); + let expr = expr.clone().cast_to(s64.clone()); + let twos_complement: i64 = u32::MAX as i64 + 1 - i64::try_from(constant).unwrap(); + let constant = Expr::int_constant(constant, s64.clone()); + expr.clone().ge(constant.clone()).ternary( + expr.clone().sub(constant), + expr.plus(Expr::int_constant(twos_complement, s64.clone())), + ) +} diff --git a/tests/kani/Enum/neg_discriminant.rs b/tests/kani/Enum/neg_discriminant.rs index 94d4bdf07bd2..598445f78319 100644 --- a/tests/kani/Enum/neg_discriminant.rs +++ b/tests/kani/Enum/neg_discriminant.rs @@ -13,17 +13,17 @@ enum Foo { } #[kani::proof] -fn main() { +fn check_negative_discriminant() { let a = Some(Foo::A); let b = Some(Foo::B); let c = Some(Foo::C); let d = Some(Foo::D); let e = Some(Foo::E); let f = Some(Foo::F); - let _ = matches!(a, Some(Foo::A)); - let _ = matches!(b, Some(Foo::B)); - let _ = matches!(c, Some(Foo::C)); - let _ = matches!(d, Some(Foo::D)); - let _ = matches!(e, Some(Foo::E)); - let _ = matches!(f, Some(Foo::F)); + let _ = assert!(matches!(a, Some(Foo::A))); + let _ = assert!(matches!(b, Some(Foo::B))); + let _ = assert!(matches!(c, Some(Foo::C))); + let _ = assert!(matches!(d, Some(Foo::D))); + let _ = assert!(matches!(e, Some(Foo::E))); + let _ = assert!(matches!(f, Some(Foo::F))); } diff --git a/tests/kani/LexicographicCmp/main.rs b/tests/kani/LexicographicCmp/main.rs index 9f245cc3870a..1e82389ea2e1 100644 --- a/tests/kani/LexicographicCmp/main.rs +++ b/tests/kani/LexicographicCmp/main.rs @@ -4,7 +4,7 @@ // This test checks that lexicographic comparison is handled correctly #[kani::proof] -fn main() { +fn check_lexicographic_cmp() { assert!([1, 2, 3] < [1, 3, 4]); assert!("World" >= "Hello"); }