diff --git a/Cargo.lock b/Cargo.lock index 67ad0c2f0e9c..141bc37e32bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -219,6 +219,7 @@ dependencies = [ "libc", "measureme", "num", + "num-traits", "serde", "serde_test", "snap", diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index e706605136c1..b60eede1ec61 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -17,6 +17,7 @@ cstr = "0.2" libc = "0.2" measureme = "9.1.0" num = "0.4.0" +num-traits = "0.2" serde = {version = "1", features = ["derive"]} snap = "1" string-interner = "0.14.0" diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index cef724626253..82a788d2f020 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -517,7 +517,7 @@ impl Expr { { assert!(typ.is_integer()); let i = i.into(); - //TODO: This check fails on some regressions + // TODO: https://github.com/model-checking/kani/issues/996 // if i != 0 && i != 1 { // assert!( // typ.min_int() <= i && i <= typ.max_int(), diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs index f9071cf5f805..73ba1b3f30f7 100644 --- a/cprover_bindings/src/irep/irep.rs +++ b/cprover_bindings/src/irep/irep.rs @@ -26,13 +26,6 @@ impl Irep { self.named_sub.get(&key) } - pub fn lookup_as_int(&self, id: IrepId) -> Option<&BigInt> { - self.lookup(id).and_then(|x| match &x.id { - IrepId::FreeformInteger(i) | IrepId::FreeformHexInteger(i) => Some(i), - _ => None, - }) - } - pub fn lookup_as_string(&self, id: IrepId) -> Option { self.lookup(id).and_then(|x| { let s = x.id.to_string(); @@ -101,11 +94,11 @@ impl Irep { Irep::just_id(IrepId::Empty) } - pub fn just_hex_id(i: T) -> Irep + pub fn just_bitpattern_id(i: T, width: u64, signed: bool) -> Irep where T: Into, { - Irep::just_id(IrepId::hex_from_int(i)) + Irep::just_id(IrepId::bitpattern_from_int(i, width, signed)) } pub fn just_id(id: IrepId) -> Irep { diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index f8cf3cf74f85..9968e47f5966 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -5,17 +5,18 @@ //! This file contains [IrepId] which is the id's used in CBMC. //! c.f. CBMC source code [src/util/irep_ids.def] use crate::cbmc_string::InternedString; -use num::bigint::BigInt; +use crate::utils::NumUtils; +use num::bigint::{BigInt, BigUint, Sign}; #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)] pub enum IrepId { /// In addition to the standard enums defined below, CBMC also allows ids to be strings. /// For e.g, to store the id of a variable. This enum variant captures those strings. FreeformString(InternedString), - /// An integer, encoded as a decimal string + /// An integer, to be encoded as a decimal string FreeformInteger(BigInt), - /// An integer, encoded as a hex string - FreeformHexInteger(BigInt), + /// A constant, stored as a bit pattern (negative numbers in 2's complement). + FreeformBitPattern(BigUint), EmptyString, Let, LetBinding, @@ -829,11 +830,29 @@ impl IrepId { IrepId::FreeformInteger(i.into()) } - pub fn hex_from_int(i: T) -> IrepId + /// CBMC expects two's complement for negative numbers. + /// https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424 + /// The bignum crate instead does sign/magnitude when making hex. + /// So for negatives, do the two's complement ourselves. + pub fn bitpattern_from_int(i: T, width: u64, _signed: bool) -> IrepId where T: Into, { - IrepId::FreeformHexInteger(i.into()) + let value: BigInt = i.into(); + // TODO https://github.com/model-checking/kani/issues/996 + // assert!( + // value.fits_in_bits(width, signed), + // "Cannot fit value into bits. value {} width: {} signed: {}", + // value, + // width, + // signed + // ); + let bitpattern = if value.sign() == Sign::Minus { + value.two_complement(width).to_biguint().unwrap() + } else { + value.to_biguint().unwrap() + }; + IrepId::FreeformBitPattern(bitpattern) } //TODO assert that s is not the string produced by any other IrepId @@ -847,14 +866,16 @@ impl ToString for IrepId { match self { IrepId::FreeformString(s) => return s.to_string(), IrepId::FreeformInteger(i) => return i.to_string(), - IrepId::FreeformHexInteger(i) => return format!("{:X}", i), + IrepId::FreeformBitPattern(i) => { + return format!("{:X}", i); + } _ => (), } let s = match self { IrepId::FreeformString(_) | IrepId::FreeformInteger(_) - | IrepId::FreeformHexInteger(_) => unreachable!(), + | IrepId::FreeformBitPattern { .. } => unreachable!(), IrepId::EmptyString => "", IrepId::Let => "let", IrepId::LetBinding => "let_binding", @@ -1668,3 +1689,89 @@ impl ToString for IrepId { s.to_string() } } + +#[cfg(test)] +mod tests { + use crate::irep::IrepId; + use num::BigInt; + // #[test] + // #[should_panic] + // fn test_hex_id_panic1() { + // IrepId::hex_from_int(-127, 7, true); + // } + + // #[test] + // #[should_panic] + // fn test_hex_id_panic2() { + // IrepId::hex_from_int(12, 4, true); + // } + + // #[test] + // #[should_panic] + // fn test_hex_id_panic3() { + // IrepId::hex_from_int(-12, 4, true); + // } + + // #[test] + // #[should_panic] + // fn test_hex_id_panic_string1() { + // IrepId::FreeformHexInteger { value: BigInt::from(-127), width: 7, signed: true } + // .to_string(); + // } + + // #[test] + // #[should_panic] + // fn test_hex_id_panic_string2() { + // IrepId::FreeformHexInteger { value: BigInt::from(12), width: 4, signed: true }.to_string(); + // } + + // #[test] + // #[should_panic] + // fn test_hex_id_panic_string3() { + // IrepId::FreeformHexInteger { value: BigInt::from(-12), width: 4, signed: true }.to_string(); + // } + + #[test] + fn test_hex_id() { + // For positive numbers, should just give the smallest representation. + // No need to zero pad. + // https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424 + assert_eq!(IrepId::bitpattern_from_int(0, 4, true).to_string(), "0"); + assert_eq!(IrepId::bitpattern_from_int(12, 5, true).to_string(), "C"); + assert_eq!(IrepId::bitpattern_from_int(12, 32, true).to_string(), "C"); + assert_eq!(IrepId::bitpattern_from_int(234, 16, true).to_string(), "EA"); + assert_eq!(IrepId::bitpattern_from_int(234, 32, true).to_string(), "EA"); + + // For positive numbers, signed and unsigned should produce the same value + assert_eq!(IrepId::bitpattern_from_int(0, 4, false).to_string(), "0"); + assert_eq!(IrepId::bitpattern_from_int(12, 4, false).to_string(), "C"); + assert_eq!(IrepId::bitpattern_from_int(12, 32, false).to_string(), "C"); + assert_eq!(IrepId::bitpattern_from_int(234, 16, false).to_string(), "EA"); + assert_eq!(IrepId::bitpattern_from_int(234, 32, false).to_string(), "EA"); + + // // For negative numbers, should convert to 2s complement of `width` bits, then print hex. + assert_eq!(IrepId::bitpattern_from_int(-1, 2, true).to_string(), "3"); + assert_eq!(IrepId::bitpattern_from_int(-1, 3, true).to_string(), "7"); + assert_eq!(IrepId::bitpattern_from_int(-1, 4, true).to_string(), "F"); + assert_eq!(IrepId::bitpattern_from_int(-1, 8, true).to_string(), "FF"); + assert_eq!(IrepId::bitpattern_from_int(-1, 9, true).to_string(), "1FF"); + assert_eq!(IrepId::bitpattern_from_int(-1, 16, true).to_string(), "FFFF"); + assert_eq!(IrepId::bitpattern_from_int(-1, 32, true).to_string(), "FFFFFFFF"); + + assert_eq!(IrepId::bitpattern_from_int(-12, 5, true).to_string(), "14"); + assert_eq!(IrepId::bitpattern_from_int(-12, 6, true).to_string(), "34"); + assert_eq!(IrepId::bitpattern_from_int(-12, 7, true).to_string(), "74"); + assert_eq!(IrepId::bitpattern_from_int(-12, 8, true).to_string(), "F4"); + assert_eq!(IrepId::bitpattern_from_int(-12, 32, true).to_string(), "FFFFFFF4"); + + assert_eq!(IrepId::bitpattern_from_int(-127, 8, true).to_string(), "81"); + assert_eq!(IrepId::bitpattern_from_int(-127, 9, true).to_string(), "181"); + assert_eq!(IrepId::bitpattern_from_int(-127, 10, true).to_string(), "381"); + assert_eq!(IrepId::bitpattern_from_int(-127, 11, true).to_string(), "781"); + assert_eq!(IrepId::bitpattern_from_int(-127, 12, true).to_string(), "F81"); + assert_eq!(IrepId::bitpattern_from_int(-127, 36, true).to_string(), "FFFFFFF81"); + + assert_eq!(IrepId::bitpattern_from_int(-255, 9, true).to_string(), "101"); + assert_eq!(IrepId::bitpattern_from_int(-255, 32, true).to_string(), "FFFFFF01"); + } +} diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 627ec5953aa4..cfcfb00c28ad 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -135,7 +135,21 @@ impl ToIrep for DatatypeComponent { impl ToIrep for Expr { fn to_irep(&self, mm: &MachineModel) -> Irep { - self.value().to_irep(mm).with_location(self.location(), mm).with_type(self.typ(), mm) + if let ExprValue::IntConstant(i) = self.value() { + let width = self.typ().native_width(mm).unwrap(); + Irep { + id: IrepId::Constant, + sub: vec![], + named_sub: vector_map![( + IrepId::Value, + Irep::just_bitpattern_id(i.clone(), width, self.typ().is_signed(mm)) + )], + } + .with_location(self.location(), mm) + .with_type(self.typ(), mm) + } else { + self.value().to_irep(mm).with_location(self.location(), mm).with_type(self.typ(), mm) + } } } @@ -181,7 +195,10 @@ impl ToIrep for ExprValue { ExprValue::CBoolConstant(i) => Irep { id: IrepId::Constant, sub: vec![], - named_sub: vector_map![(IrepId::Value, Irep::just_hex_id(if *i { 1 } else { 0 }),)], + named_sub: vector_map![( + IrepId::Value, + Irep::just_bitpattern_id(if *i { 1u8 } else { 0 }, mm.bool_width(), false) + )], }, ExprValue::Dereference(e) => { Irep { id: IrepId::Dereference, sub: vec![e.to_irep(mm)], named_sub: vector_map![] } @@ -192,7 +209,10 @@ impl ToIrep for ExprValue { Irep { id: IrepId::Constant, sub: vec![], - named_sub: vector_map![(IrepId::Value, Irep::just_hex_id(c))], + named_sub: vector_map![( + IrepId::Value, + Irep::just_bitpattern_id(c, mm.double_width(), false) + )], } } ExprValue::FloatConstant(i) => { @@ -200,7 +220,10 @@ impl ToIrep for ExprValue { Irep { id: IrepId::Constant, sub: vec![], - named_sub: vector_map![(IrepId::Value, Irep::just_hex_id(c))], + named_sub: vector_map![( + IrepId::Value, + Irep::just_bitpattern_id(c, mm.float_width(), false) + )], } } ExprValue::FunctionCall { function, arguments } => side_effect_irep( @@ -217,11 +240,9 @@ impl ToIrep for ExprValue { sub: vec![array.to_irep(mm), index.to_irep(mm)], named_sub: vector_map![], }, - ExprValue::IntConstant(i) => Irep { - id: IrepId::Constant, - sub: vec![], - named_sub: vector_map![(IrepId::Value, Irep::just_hex_id(i.clone()))], - }, + ExprValue::IntConstant(_) => { + unreachable!("Should have been processed in previous step") + } ExprValue::Member { lhs, field } => Irep { id: IrepId::Member, sub: vec![lhs.to_irep(mm)], @@ -239,7 +260,10 @@ impl ToIrep for ExprValue { ExprValue::PointerConstant(i) => Irep { id: IrepId::Constant, sub: vec![], - named_sub: vector_map![(IrepId::Value, Irep::just_hex_id(*i))], + named_sub: vector_map![( + IrepId::Value, + Irep::just_bitpattern_id(*i, mm.pointer_width(), false) + )], }, ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]), ExprValue::StatementExpression { statements: ops } => side_effect_irep( @@ -278,7 +302,7 @@ impl ToIrep for ExprValue { ExprValue::UnOp { op: UnaryOperand::Bswap, e } => Irep { id: IrepId::Bswap, sub: vec![e.to_irep(mm)], - named_sub: vector_map![(IrepId::BitsPerByte, Irep::just_int_id(8))], + named_sub: vector_map![(IrepId::BitsPerByte, Irep::just_int_id(8u8))], }, ExprValue::UnOp { op: UnaryOperand::BitReverse, e } => { Irep { id: IrepId::BitReverse, sub: vec![e.to_irep(mm)], named_sub: vector_map![] } diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs index d765d3b19799..d5f312cb67c6 100644 --- a/cprover_bindings/src/utils.rs +++ b/cprover_bindings/src/utils.rs @@ -3,7 +3,9 @@ //! Useful utilities for CBMC use crate::InternedString; -use num::bigint::BigInt; +use num::bigint::{BigInt, Sign}; +use num::Signed; +use num_traits::Zero; /// Kani bug report URL, for asserts/errors pub const BUG_REPORT_URL: &str = @@ -15,6 +17,24 @@ pub fn aggr_tag>(n: T) -> InternedString { format!("tag-{}", n.to_string()).into() } +pub trait NumUtils { + fn fits_in_bits(&self, width: u64, signed: bool) -> bool; + fn two_complement(&self, width: u64) -> Self; +} + +impl NumUtils for BigInt { + fn fits_in_bits(&self, width: u64, signed: bool) -> bool { + self <= &max_int(width, signed) && self >= &min_int(width, signed) + } + + fn two_complement(&self, width: u64) -> Self { + assert_eq!(self.sign(), Sign::Minus); + let max = max_int(width, false); + assert!(self.abs() < max); + max - (self.abs() - 1) + } +} + /// Provides a useful shortcut for making BTreeMaps. #[macro_export] macro_rules! btree_map { @@ -79,14 +99,39 @@ pub fn min_int(width: u64, signed: bool) -> BigInt { let min = -max - 1; min } else { - BigInt::from(0) + BigInt::zero() } } #[cfg(test)] mod tests { + + use crate::utils::NumUtils; use crate::utils::{max_int, min_int}; use num::BigInt; + + #[test] + fn test_fits_in_bits() { + assert_eq!(BigInt::from(10).fits_in_bits(3, false), false); + assert_eq!(BigInt::from(10).fits_in_bits(4, false), true); + assert_eq!(BigInt::from(10).fits_in_bits(5, false), true); + assert_eq!(BigInt::from(10).fits_in_bits(3, true), false); + assert_eq!(BigInt::from(10).fits_in_bits(4, true), false); + assert_eq!(BigInt::from(10).fits_in_bits(5, true), true); + + assert_eq!(BigInt::from(-10).fits_in_bits(3, false), false); + assert_eq!(BigInt::from(-10).fits_in_bits(4, false), false); + assert_eq!(BigInt::from(-10).fits_in_bits(5, false), false); + assert_eq!(BigInt::from(-10).fits_in_bits(3, true), false); + assert_eq!(BigInt::from(-10).fits_in_bits(4, true), false); + assert_eq!(BigInt::from(-10).fits_in_bits(5, true), true); + } + + #[test] + fn test_twos_complement() { + assert_eq!(BigInt::from(-10).two_complement(8), BigInt::from(246)); + } + #[test] fn test_max_int() { // Unsigned diff --git a/tests/kani/Intrinsics/exact_div.rs b/tests/kani/Intrinsics/exact_div.rs new file mode 100644 index 000000000000..c7e0f66ced0a --- /dev/null +++ b/tests/kani/Intrinsics/exact_div.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-verify-fail + +#![feature(core_intrinsics)] + +#[kani::proof] +fn main() { + let a: i8 = -128; + let b: i8 = -1; + let i = unsafe { std::intrinsics::exact_div(a, b) }; +}