Use num::BigInt instead of i128 in constants, as constants can be of …

…arbitrary size. (#141)

Cargo.lock

@@ -2262,21 +2262,78 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "num"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "43db66d1170d347f9a065114077f7dccb00c1b9478c89384490a3425279a4606"
+dependencies = [
+ "num-bigint",
+ "num-complex",
+ "num-integer",
+ "num-iter",
+ "num-rational",
+ "num-traits",
+]
+
+[[package]]
+name = "num-bigint"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e0d047c1062aa51e256408c560894e5251f08925980e53cf1aa5bd00eec6512"
+dependencies = [
+ "autocfg",
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-complex"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "26873667bbbb7c5182d4a37c1add32cdf09f841af72da53318fdb81543c15085"
+dependencies = [
+ "num-traits",
+]
+
 [[package]]
 name = "num-integer"
-version = "0.1.43"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2cc698a63b549a70bc047073d2949cce27cd1c7b0a4a862d08a8031bc2801db"
+dependencies = [
+ "autocfg",
+ "num-traits",
+]
+
+[[package]]
+name = "num-iter"
+version = "0.1.42"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8d59457e662d541ba17869cf51cf177c0b5f0cbf476c66bdc90bf1edac4f875b"
+checksum = "b2021c8337a54d21aca0d59a92577a029af9431cb59b909b03252b9c164fad59"
 dependencies = [
  "autocfg",
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-rational"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d41702bd167c2df5520b384281bc111a4b5efcf7fbc4c9c222c815b07e0a6a6a"
+dependencies = [
+ "autocfg",
+ "num-bigint",
+ "num-integer",
  "num-traits",
 ]
 
 [[package]]
 name = "num-traits"
-version = "0.2.12"
+version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ac267bcc07f48ee5f8935ab0d24f316fb722d7a1292e2913f0cc196b29ffd611"
+checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290"
 dependencies = [
  "autocfg",
 ]
@@ -3617,6 +3674,7 @@ dependencies = [
  "cstr",
  "libc",
  "measureme",
+ "num",
  "rustc-demangle",
  "rustc_ast",
  "rustc_attr",

compiler/rustc_codegen_llvm/Cargo.toml

@@ -12,6 +12,7 @@ bitflags = "1.0"
 cstr = "0.2"
 libc = "0.2"
 measureme = "9.1.0"
+num = "0.4.0"
 snap = "1"
 tracing = "0.1"
 rustc_middle = { path = "../rustc_middle" }

compiler/rustc_codegen_llvm/src/gotoc/cbmc/env.rs

@@ -10,27 +10,35 @@
 
 use super::goto_program::{Expr, Location, Symbol, Type};
 use super::MachineModel;
-use std::convert::TryInto;
-use std::fmt::Debug;
+use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
 where
-    T: TryInto<i128>,
-    T::Error: Debug,
+    T: Into<BigInt>,
 {
     Symbol::constant(name, name, name, Expr::int_constant(value, Type::c_int()), Location::none())
 }
 
+fn int_constant_from_bool(name: &str, value: bool) -> Symbol {
+    Symbol::constant(
+        name,
+        name,
+        name,
+        Expr::int_constant(if value { 1 } else { 0 }, Type::c_int()),
+        Location::none(),
+    )
+}
+
 fn string_constant(name: &str, value: &str) -> Symbol {
     Symbol::constant(name, name, name, Expr::string_constant(value), Location::none())
 }
 
 pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
     vec![
         string_constant("__CPROVER_architecture_arch", mm.architecture()),
-        int_constant("__CPROVER_architecture_NULL_is_zero", mm.null_is_zero()),
+        int_constant_from_bool("__CPROVER_architecture_NULL_is_zero", mm.null_is_zero()),
         int_constant("__CPROVER_architecture_alignment", mm.alignment()),
         int_constant("__CPROVER_architecture_bool_width", mm.bool_width()),
-        int_constant("__CPROVER_architecture_char_is_unsigned", mm.char_is_unsigned()),
+        int_constant_from_bool("__CPROVER_architecture_char_is_unsigned", mm.char_is_unsigned()),
         int_constant("__CPROVER_architecture_char_width", mm.char_width()),
         int_constant("__CPROVER_architecture_double_width", mm.double_width()),
         // c.f. https://github.com/diffblue/cbmc/blob/develop/src/util/config.h
@@ -44,7 +52,10 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
         int_constant("__CPROVER_architecture_pointer_width", mm.pointer_width()),
         int_constant("__CPROVER_architecture_short_int_width", mm.short_int_width()),
         int_constant("__CPROVER_architecture_single_width", mm.single_width()),
-        int_constant("__CPROVER_architecture_wchar_t_is_unsigned", mm.wchar_t_is_unsigned()),
+        int_constant_from_bool(
+            "__CPROVER_architecture_wchar_t_is_unsigned",
+            mm.wchar_t_is_unsigned(),
+        ),
         int_constant("__CPROVER_architecture_wchar_t_width", mm.wchar_t_width()),
         int_constant("__CPROVER_architecture_word_size", mm.word_size()),
         int_constant("__CPROVER_rounding_mode", mm.rounding_mode()),

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs

@@ -5,8 +5,8 @@ use self::ExprValue::*;
 use self::UnaryOperand::*;
 use super::super::MachineModel;
 use super::{DatatypeComponent, Location, Parameter, Stmt, SwitchCase, SymbolTable, Type};
+use num::bigint::BigInt;
 use std::collections::BTreeMap;
-use std::convert::TryInto;
 use std::fmt::Debug;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////
@@ -98,7 +98,7 @@ pub enum ExprValue {
         index: Expr,
     },
     /// `123`
-    IntConstant(i128),
+    IntConstant(BigInt),
     /// `lhs.field`
     Member {
         lhs: Expr,
@@ -247,9 +247,9 @@ impl Expr {
     }
 
     /// If the expression is an Int constant type, return its value
-    pub fn int_constant_value(&self) -> Option<i128> {
-        match *self.value {
-            ExprValue::IntConstant(i) => Some(i),
+    pub fn int_constant_value(&self) -> Option<BigInt> {
+        match &*self.value {
+            ExprValue::IntConstant(i) => Some(i.clone()),
             _ => None,
         }
     }
@@ -455,11 +455,10 @@ impl Expr {
     /// `123`
     pub fn int_constant<T>(i: T, typ: Type) -> Self
     where
-        T: TryInto<i128>,
-        T::Error: Debug,
+        T: Into<BigInt>,
     {
         assert!(typ.is_integer());
-        let i = i.try_into().unwrap();
+        let i = i.into();
         //TODO: This check fails on some regressions
         // if i != 0 && i != 1 {
         //     assert!(

compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/from_irep.rs

@@ -144,7 +144,8 @@ impl FromIrep for Type {
             IrepId::Bool => Type::Bool,
             IrepId::CBool => {
                 assert!(i.sub.is_empty());
-                assert!(i.lookup_as_int(IrepId::Width).unwrap() == 8);
+                let width: u64 = i.lookup_as_int(IrepId::Width).unwrap().try_into().unwrap();
+                assert!(width == 8);
                 Type::c_bool()
             }
             IrepId::Code => {
@@ -165,8 +166,8 @@ impl FromIrep for Type {
             }
             IrepId::Floatbv => {
                 assert!(i.sub.is_empty());
-                let f = i.lookup_as_int(IrepId::F).unwrap();
-                let width = i.lookup_as_int(IrepId::Width).unwrap();
+                let f: u64 = i.lookup_as_int(IrepId::F).unwrap().try_into().unwrap();
+                let width: u64 = i.lookup_as_int(IrepId::Width).unwrap().try_into().unwrap();
                 match i.lookup(IrepId::CCType).unwrap().id {
                     IrepId::Double => {
                         assert!(f == 52 && width == 64);

compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/irep.rs

@@ -5,11 +5,11 @@
 use super::super::goto_program::{Location, Type};
 use super::super::MachineModel;
 use super::{IrepId, ToIrep};
+use num::BigInt;
 use std::collections::BTreeMap;
-use std::convert::TryInto;
 use std::fmt::Debug;
 
-/// The CBMC serilization format for goto-programs.
+/// The CBMC serialization format for goto-programs.
 /// CBMC implementation code is at:
 /// https://github.com/diffblue/cbmc/blob/develop/src/util/irep.h
 #[derive(Clone, Debug)]
@@ -25,8 +25,8 @@ impl Irep {
         self.named_sub.get(&key)
     }
 
-    pub fn lookup_as_int(&self, id: IrepId) -> Option<i128> {
-        self.lookup(id).and_then(|x| match x.id {
+    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,
         })
@@ -102,8 +102,7 @@ impl Irep {
 
     pub fn just_hex_id<T>(i: T) -> Irep
     where
-        T: TryInto<i128>,
-        T::Error: Debug,
+        T: Into<BigInt>,
     {
         Irep::just_id(IrepId::hex_from_int(i))
     }
@@ -114,8 +113,7 @@ impl Irep {
 
     pub fn just_int_id<T>(i: T) -> Irep
     where
-        T: TryInto<i128>,
-        T::Error: Debug,
+        T: Into<BigInt>,
     {
         Irep::just_id(IrepId::from_int(i))
     }

compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/irep_id.rs

@@ -4,17 +4,16 @@
 //!
 //! This file contains [IrepId] which is the id's used in CBMC.
 //! c.f. CBMC source code [src/util/irep_ids.def]
-use std::convert::TryInto;
-use std::fmt::Debug;
+use num::bigint::BigInt;
 #[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(String),
     /// An integer, encoded as a decimal string
-    FreeformInteger(i128),
+    FreeformInteger(BigInt),
     /// An integer, encoded as a hex string
-    FreeformHexInteger(i128),
+    FreeformHexInteger(BigInt),
     EmptyString,
     Let,
     LetBinding,
@@ -822,18 +821,16 @@ pub enum IrepId {
 impl IrepId {
     pub fn from_int<T>(i: T) -> IrepId
     where
-        T: TryInto<i128>,
-        T::Error: Debug,
+        T: Into<BigInt>,
     {
-        IrepId::FreeformInteger(i.try_into().unwrap())
+        IrepId::FreeformInteger(i.into())
     }
 
     pub fn hex_from_int<T>(i: T) -> IrepId
     where
-        T: TryInto<i128>,
-        T::Error: Debug,
+        T: Into<BigInt>,
     {
-        IrepId::FreeformHexInteger(i.try_into().unwrap())
+        IrepId::FreeformHexInteger(i.into())
     }
 
     pub fn from_string(s: String) -> IrepId {

compiler/rustc_codegen_llvm/src/gotoc/cbmc/irep/to_irep.rs

@@ -218,7 +218,7 @@ impl ToIrep for ExprValue {
             ExprValue::IntConstant(i) => Irep {
                 id: IrepId::Constant,
                 sub: vec![],
-                named_sub: btree_map![(IrepId::Value, Irep::just_hex_id(*i))],
+                named_sub: btree_map![(IrepId::Value, Irep::just_hex_id(i.clone()))],
             },
             ExprValue::Member { lhs, field } => Irep {
                 id: IrepId::Member,

compiler/rustc_codegen_llvm/src/gotoc/cbmc/machine_model.rs

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 /// Represents the machine specific information necessary to generate an Irep.
+use num::bigint::BigInt;
 #[derive(Debug)]
 pub struct MachineModel {
     /// Is the architecture big endian?
@@ -39,6 +40,12 @@ pub enum RoundingMode {
     TowardsZero = 3,
 }
 
+impl From<RoundingMode> for BigInt {
+    fn from(rm: RoundingMode) -> Self {
+        (rm as i32).into()
+    }
+}
+
 /// Constructor
 impl MachineModel {
     pub fn new(

rust-tests/cbmc-reg/CodegenConstValue/u128.rs

@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Avoid RUST constant propagating this away
+fn assert_bigger(a: u128, b: u128) {
+    assert!(a > b);
+}
+
+fn main() {
+    assert_bigger(u128::MAX, 12);
+}