Break min/max_int into their own util functions, and have them return BigInt to avoid any arbitrary width constraints (rust-lang#605)

Author: danielsn

compiler/cbmc/src/goto_program/typ.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use self::DatatypeComponent::*;
 use self::Type::*;
-use super::super::utils::aggr_name;
+use super::super::utils::{aggr_name, max_int, min_int};
 use super::super::MachineModel;
 use super::{Expr, SymbolTable};
 use std::collections::BTreeMap;
@@ -790,33 +790,18 @@ impl Type {
 
 /// Constants from Types, for use in Expr contexts
 impl Type {
-    //TODO second mathematical check
-    pub fn max_int(&self, mm: &MachineModel) -> i128 {
-        assert!(self.is_integer());
-        let w = self.native_width(mm).unwrap();
-        assert!(w < 128);
-        let shift = if self.is_signed(mm) { 129 - w } else { 128 - w };
-        let max: u128 = u128::MAX >> shift;
-        max.try_into().unwrap()
-    }
-
     pub fn max_int_expr(&self, mm: &MachineModel) -> Expr {
-        Expr::int_constant(self.max_int(mm), self.clone())
-    }
-
-    pub fn min_int(&self, mm: &MachineModel) -> i128 {
         assert!(self.is_integer());
-        if self.is_unsigned(mm) {
-            0
-        } else {
-            let max = self.max_int(mm);
-            let min = -max - 1;
-            min
-        }
+        let width = self.native_width(mm).unwrap();
+        let signed = self.is_signed(mm);
+        Expr::int_constant(max_int(width, signed), self.clone())
     }
 
     pub fn min_int_expr(&self, mm: &MachineModel) -> Expr {
-        Expr::int_constant(self.min_int(mm), self.clone())
+        assert!(self.is_integer());
+        let width = self.native_width(mm).unwrap();
+        let signed = self.is_signed(mm);
+        Expr::int_constant(min_int(width, signed), self.clone())
     }
 
     /// an expression of nondeterministic value of type self

compiler/cbmc/src/utils.rs

@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Useful utilities for CBMC
 
+use num::bigint::BigInt;
+
 /// RMC bug report URL, for asserts/errors
 pub const BUG_REPORT_URL: &str =
     "https://github.com/model-checking/rmc/issues/new?template=bug_report.md";
@@ -42,3 +44,62 @@ macro_rules! btree_string_map {
         (BTreeMap::from_iter(vec![$($x),*].into_iter().map(|(k,v)|(k.to_string(),v))))
     }}
 }
+
+pub fn max_int(width: u64, signed: bool) -> BigInt {
+    let mut bi = BigInt::from(0);
+    if signed {
+        bi.set_bit(width - 1, true);
+    } else {
+        bi.set_bit(width, true);
+    }
+    bi - 1
+}
+
+pub fn min_int(width: u64, signed: bool) -> BigInt {
+    if signed {
+        let max = max_int(width, true);
+        let min = -max - 1;
+        min
+    } else {
+        BigInt::from(0)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::utils::{max_int, min_int};
+    use num::BigInt;
+    #[test]
+    fn test_max_int() {
+        // Unsigned
+        assert_eq!(max_int(8, false), BigInt::from(u8::MAX));
+        assert_eq!(max_int(16, false), BigInt::from(u16::MAX));
+        assert_eq!(max_int(32, false), BigInt::from(u32::MAX));
+        assert_eq!(max_int(64, false), BigInt::from(u64::MAX));
+        assert_eq!(max_int(128, false), BigInt::from(u128::MAX));
+
+        //Signed
+        assert_eq!(max_int(8, true), BigInt::from(i8::MAX));
+        assert_eq!(max_int(16, true), BigInt::from(i16::MAX));
+        assert_eq!(max_int(32, true), BigInt::from(i32::MAX));
+        assert_eq!(max_int(64, true), BigInt::from(i64::MAX));
+        assert_eq!(max_int(128, true), BigInt::from(i128::MAX));
+    }
+
+    #[test]
+    fn test_min_int() {
+        // Unsigned
+        assert_eq!(min_int(8, false), BigInt::from(u8::MIN));
+        assert_eq!(min_int(16, false), BigInt::from(u16::MIN));
+        assert_eq!(min_int(32, false), BigInt::from(u32::MIN));
+        assert_eq!(min_int(64, false), BigInt::from(u64::MIN));
+        assert_eq!(min_int(128, false), BigInt::from(u128::MIN));
+
+        //Signed
+        assert_eq!(min_int(8, true), BigInt::from(i8::MIN));
+        assert_eq!(min_int(16, true), BigInt::from(i16::MIN));
+        assert_eq!(min_int(32, true), BigInt::from(i32::MIN));
+        assert_eq!(min_int(64, true), BigInt::from(i64::MIN));
+        assert_eq!(min_int(128, true), BigInt::from(i128::MIN));
+    }
+}