Merge remote-tracking branch 'origin/main' into issue-3206-contract-m…

…ethod Conflicts: library/kani/src/lib.rs library/kani_core/src/lib.rs
model-checking · Jul 25, 2024 · 6a26653 · 6a26653
2 parents 5ad1b05 + b18698f
commit 6a26653
Show file tree

Hide file tree

Showing 77 changed files with 1,544 additions and 387 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -104,10 +104,14 @@ jobs:
           apt-get install -y software-properties-common apt-utils
           add-apt-repository ppa:git-core/ppa
           add-apt-repository ppa:deadsnakes/ppa
+          add-apt-repository ppa:ubuntu-toolchain-r/test
           apt-get update
           apt-get install -y \
-            build-essential bash-completion curl lsb-release sudo g++ gcc flex \
+            build-essential bash-completion curl lsb-release sudo g++-9 gcc-9 flex \
             bison make patch git python3.7 python3.7-dev python3.7-distutils
+          update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 110 \
+            --slave /usr/bin/g++ g++ /usr/bin/g++-9
+          ln -sf cpp-9 /usr/bin/cpp
           update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
           curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall

diff --git a/Cargo.lock b/Cargo.lock
@@ -169,7 +169,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -482,7 +482,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -801,9 +801,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.2"
+version = "0.5.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd"
+checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4"
 dependencies = [
  "bitflags",
 ]
@@ -924,7 +924,7 @@ checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1030,7 +1030,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1045,9 +1045,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.71"
+version = "2.0.72"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b146dcf730474b4bcd16c311627b31ede9ab149045db4d6088b3becaea046462"
+checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1068,22 +1068,22 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.62"
+version = "1.0.63"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f2675633b1499176c2dff06b0856a27976a8f9d436737b4cf4f312d4d91d8bbb"
+checksum = "c0342370b38b6a11b6cc11d6a805569958d54cfa061a29969c3b5ce2ea405724"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.62"
+version = "1.0.63"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d20468752b09f49e909e55a5d338caa8bedf615594e9d80bc4c565d30faf798c"
+checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1098,9 +1098,9 @@ dependencies = [
 
 [[package]]
 name = "toml"
-version = "0.8.14"
+version = "0.8.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f49eb2ab21d2f26bd6db7bf383edc527a7ebaee412d17af4d40fdccd442f335"
+checksum = "ac2caab0bf757388c6c0ae23b3293fdb463fee59434529014f85e3263b995c28"
 dependencies = [
  "serde",
  "serde_spanned",
@@ -1119,9 +1119,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.22.15"
+version = "0.22.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d59a3a72298453f564e2b111fa896f8d07fabb36f51f06d7e875fc5e0b5a3ef1"
+checksum = "278f3d518e152219c994ce877758516bca5e118eaed6996192a774fb9fbf0788"
 dependencies = [
  "indexmap",
  "serde",
@@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
 
 [[package]]
@@ -1384,9 +1384,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
 
 [[package]]
 name = "winnow"
-version = "0.6.13"
+version = "0.6.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "59b5e5f6c299a3c7890b876a2a587f3115162487e704907d9b6cd29473052ba1"
+checksum = "374ec40a2d767a3c1b4972d9475ecd557356637be906f2cb3f7fe17a6eb5e22f"
 dependencies = [
  "memchr",
 ]
@@ -1414,5 +1414,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.71",
+ "syn 2.0.72",
 ]
diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs
@@ -8,6 +8,8 @@ use std::fmt::Display;
 
 /// Based off the CBMC symbol implementation here:
 /// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h>
+///
+/// TODO: We should consider using BitFlags for all the boolean flags.
 #[derive(Clone, Debug)]
 pub struct Symbol {
     /// Unique identifier. Mangled name from compiler `foo12_bar17_x@1`
@@ -46,6 +48,14 @@ pub struct Symbol {
     pub is_thread_local: bool,
     pub is_volatile: bool,
     pub is_weak: bool,
+
+    /// This flag marks a variable as constant (IrepId: `ID_C_constant`).
+    ///
+    /// In CBMC, this is a property of the type or expression. However, we keep it here to avoid
+    /// having to propagate the attribute to all variants of `Type` and `Expr`.
+    ///
+    /// During contract verification, CBMC will not havoc static variables marked as constant.
+    pub is_static_const: bool,
 }
 
 /// The equivalent of a "mathematical function" in CBMC. Semantically this is an
@@ -157,6 +167,7 @@ impl Symbol {
             is_lvalue: false,
             is_parameter: false,
             is_static_lifetime: false,
+            is_static_const: false,
             is_thread_local: false,
             is_volatile: false,
             is_weak: false,
@@ -363,6 +374,11 @@ impl Symbol {
         self
     }
 
+    pub fn set_is_static_const(&mut self, v: bool) -> &mut Symbol {
+        self.is_static_const = v;
+        self
+    }
+
     pub fn with_is_state_var(mut self, v: bool) -> Symbol {
         self.is_state_var = v;
         self
@@ -383,11 +399,21 @@ impl Symbol {
         self
     }
 
+    pub fn set_pretty_name<T: Into<InternedString>>(&mut self, pretty_name: T) -> &mut Symbol {
+        self.pretty_name = Some(pretty_name.into());
+        self
+    }
+
     pub fn with_is_hidden(mut self, hidden: bool) -> Symbol {
         self.is_auxiliary = hidden;
         self
     }
 
+    pub fn set_is_hidden(&mut self, hidden: bool) -> &mut Symbol {
+        self.is_auxiliary = hidden;
+        self
+    }
+
     /// Set `is_property`.
     pub fn with_is_property(mut self, v: bool) -> Self {
         self.is_property = v;

diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs
@@ -107,6 +107,11 @@ impl SymbolTable {
         self.symbol_table.get(&name)
     }
 
+    pub fn lookup_mut<T: Into<InternedString>>(&mut self, name: T) -> Option<&mut Symbol> {
+        let name = name.into();
+        self.symbol_table.get_mut(&name)
+    }
+
     pub fn machine_model(&self) -> &MachineModel {
         &self.machine_model
     }

diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
@@ -598,6 +598,10 @@ impl goto_program::Symbol {
                 Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()),
             );
         }
+        if self.is_static_const {
+            // Add a `const` to the type.
+            typ = typ.with_named_sub(IrepId::CConstant, Irep::just_id(IrepId::from_int(1)))
+        }
         super::Symbol {
             typ,
             value: match &self.value {

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -3,13 +3,13 @@
 use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
-use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type};
+use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
 use rustc_middle::ty::Const as ConstInternal;
 use rustc_smir::rustc_internal;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
-use stable_mir::mir::Operand;
+use stable_mir::mir::{Mutability, Operand};
 use stable_mir::ty::{
     Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
     TyConst, TyConstKind, TyKind, UintTy,
@@ -470,11 +470,17 @@ impl<'tcx> GotocCtx<'tcx> {
         name: Option<String>,
         loc: Location,
     ) -> Expr {
-        debug!(?name, "codegen_const_allocation");
+        debug!(?name, ?alloc, "codegen_const_allocation");
         let alloc_name = match self.alloc_map.get(alloc) {
             None => {
                 let alloc_name = if let Some(name) = name { name } else { self.next_global_name() };
-                self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone(), loc);
+                let has_interior_mutabity = false; // Constants cannot be mutated.
+                self.codegen_alloc_in_memory(
+                    alloc.clone(),
+                    alloc_name.clone(),
+                    loc,
+                    has_interior_mutabity,
+                );
                 alloc_name
             }
             Some(name) => name.clone(),
@@ -484,13 +490,18 @@ impl<'tcx> GotocCtx<'tcx> {
         mem_place.address_of()
     }
 
-    /// Insert an allocation into the goto symbol table, and generate a goto function that will
-    /// initialize it.
+    /// Insert an allocation into the goto symbol table, and generate an init value.
     ///
-    /// This function is ultimately responsible for creating new statically initialized global variables
-    /// in our goto binaries.
-    pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String, loc: Location) {
-        debug!(?alloc, ?name, "codegen_alloc_in_memory");
+    /// This function is ultimately responsible for creating new statically initialized global
+    /// variables.
+    pub fn codegen_alloc_in_memory(
+        &mut self,
+        alloc: Allocation,
+        name: String,
+        loc: Location,
+        has_interior_mutabity: bool,
+    ) {
+        debug!(?name, ?alloc, "codegen_alloc_in_memory");
         let struct_name = &format!("{name}::struct");
 
         // The declaration of a static variable may have one type and the constant initializer for
@@ -513,50 +524,40 @@ impl<'tcx> GotocCtx<'tcx> {
                 .collect()
         });
 
+        // Create the allocation from a byte array.
+        let init_fn = |gcx: &mut GotocCtx, var: Symbol| {
+            let val = Expr::struct_expr_from_values(
+                alloc_typ_ref.clone(),
+                alloc_data
+                    .iter()
+                    .map(|d| match d {
+                        AllocData::Bytes(bytes) => Expr::array_expr(
+                            Type::unsigned_int(8).array_of(bytes.len()),
+                            bytes
+                                .iter()
+                                // We should consider adding a poison / undet where we have none
+                                // This mimics the behaviour before StableMIR though.
+                                .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8)))
+                                .collect(),
+                        ),
+                        AllocData::Expr(e) => e.clone(),
+                    })
+                    .collect(),
+                &gcx.symbol_table,
+            );
+            if val.typ() == &var.typ { val } else { val.transmute_to(var.typ, &gcx.symbol_table) }
+        };
+
         // The global static variable may not be in the symbol table if we are dealing
-        // with a literal that can be statically allocated.
-        // We need to make a constructor whether it was in the table or not, so we can't use the
-        // closure argument to ensure_global_var to do that here.
-        let var = self.ensure_global_var(
+        // with a promoted constant.
+        let _var = self.ensure_global_var_init(
             &name,
             false, //TODO is this correct?
+            alloc.mutability == Mutability::Not && !has_interior_mutabity,
             alloc_typ_ref.clone(),
             loc,
-            |_, _| None,
-        );
-        let var_typ = var.typ().clone();
-
-        // Assign the initial value `val` to `var` via an intermediate `temp_var` to allow for
-        // transmuting the allocation type to the global static variable type.
-        let val = Expr::struct_expr_from_values(
-            alloc_typ_ref.clone(),
-            alloc_data
-                .iter()
-                .map(|d| match d {
-                    AllocData::Bytes(bytes) => Expr::array_expr(
-                        Type::unsigned_int(8).array_of(bytes.len()),
-                        bytes
-                            .iter()
-                            // We should consider adding a poison / undet where we have none
-                            // This mimics the behaviour before StableMIR though.
-                            .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8)))
-                            .collect(),
-                    ),
-                    AllocData::Expr(e) => e.clone(),
-                })
-                .collect(),
-            &self.symbol_table,
-        );
-        let fn_name = Self::initializer_fn_name(&name);
-        let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref, loc).to_expr();
-        let body = Stmt::block(
-            vec![
-                Stmt::decl(temp_var.clone(), Some(val), loc),
-                var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), loc),
-            ],
-            loc,
+            init_fn,
         );
-        self.register_initializer(&name, body);
 
         self.alloc_map.insert(alloc, name);
     }
@@ -663,12 +664,6 @@ impl<'tcx> GotocCtx<'tcx> {
         let fn_item_struct_ty = self.codegen_fndef_type_stable(instance);
         // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object.
         let fn_singleton_name = format!("{mangled_name}::FnDefSingleton");
-        self.ensure_global_var(
-            &fn_singleton_name,
-            false,
-            fn_item_struct_ty,
-            loc,
-            |_, _| None, // zero-sized, so no initialization necessary
-        )
+        self.ensure_global_var(&fn_singleton_name, false, fn_item_struct_ty, loc).to_expr()
     }
 }