Print negative hex instead of -positive

Cargo.lock

@@ -219,6 +219,7 @@ dependencies = [
  "libc",
  "measureme",
  "num",
+ "num-traits",
  "serde",
  "serde_test",
  "snap",

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"

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(),

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<String> {
         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<T>(i: T) -> Irep
+    pub fn just_bitpattern_id<T>(i: T, width: u64, signed: bool) -> Irep
     where
         T: Into<BigInt>,
     {
-        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 {

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<T>(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<T>(i: T, width: u64, _signed: bool) -> IrepId
     where
         T: Into<BigInt>,
     {
-        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");
+    }
+}

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,15 +209,21 @@ 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) => {
                 let c: u32 = unsafe { std::mem::transmute(*i) };
                 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![] }

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<T: Into<InternedString>>(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