Merge branch 'main' into attr-invariant

.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

.github/workflows/verify-std-check.yml

@@ -0,0 +1,86 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to build and run the `verify-rust-std` repository.
+#
+# This check should be optional, but it has been added to help provide
+# visibility to when a PR may break the `verify-rust-std` repository.
+#
+# We expect toolchain updates to potentially break this workflow in cases where
+# the version tracked in the `verify-rust-std` is not compatible with newer
+# versions of the Rust toolchain.
+#
+# Changes unrelated to the toolchain should match the current status of main.
+
+name: Check Std Verification
+on:
+  pull_request:
+  workflow_call:
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  verify-std:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Kani does not support windows.
+        os: [ ubuntu-22.04, macos-14 ]
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          repository: model-checking/verify-rust-std
+          path: verify-rust-std
+          submodules: true
+
+      - name: Checkout `Kani`
+        uses: actions/checkout@v4
+        with:
+          path: kani
+
+      - name: Setup Kani Dependencies
+        uses: ./kani/.github/actions/setup
+        with:
+          os: ${{ matrix.os }}
+          kani_dir: kani
+
+      - name: Build Kani
+        working-directory: kani
+        run: |
+          cargo build-dev
+          echo "$(pwd)/scripts" >> $GITHUB_PATH
+
+      - name: Run verification with HEAD
+        id: check-head
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      # If the head failed, check if it's a new failure.
+      - name: Checkout base
+        working-directory: kani
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        run: |
+          BASE_REF=${{ github.event.pull_request.base.sha }}
+          git checkout ${BASE_REF}
+          cargo build-dev
+
+      - name: Run verification with BASE
+        id: check-base
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      - name: Compare PR results
+        if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output
+        run: |
+          echo "New failure introduced by this change"
+          exit 1
+

.github/workflows/verify-std-update.yml

@@ -0,0 +1,35 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to update the verify std branch.
+
+name: Update "features/verify-rust-std"
+on:
+  schedule:
+    - cron: "30 3 * * *" # Run this every day at 03:30 UTC
+  workflow_dispatch:     # Allow manual dispatching.
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  # First ensure the HEAD is compatible with the `verify-rust-std` repository.
+  verify-std:
+    name: Verify Std
+    permissions: { }
+    uses: ./.github/workflows/verify-std-check.yml
+
+  # Push changes to the features branch.
+  update-branch:
+    needs: verify-std
+    permissions:
+      contents: write
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v4
+
+      - name: Update feature branch
+        run: |
+          git push origin HEAD:features/verify-rust-std
+

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;

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
     }

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 {

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