Upgrade to CBMC 5.69.1 (with fixes)

cprover_bindings/src/env.rs

@@ -12,6 +12,13 @@ use super::goto_program::{Expr, Location, Symbol, Type};
 use super::MachineModel;
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
+where
+    T: Into<BigInt>,
+{
+    Symbol::constant(name, name, name, Expr::int_constant(value, Type::integer()), Location::none())
+}
+
+fn int_constant_c_int<T>(name: &str, value: T) -> Symbol
 where
     T: Into<BigInt>,
 {
@@ -23,7 +30,7 @@ fn int_constant_from_bool(name: &str, value: bool) -> Symbol {
         name,
         name,
         name,
-        Expr::int_constant(if value { 1 } else { 0 }, Type::c_int()),
+        Expr::int_constant(if value { 1 } else { 0 }, Type::integer()),
         Location::none(),
     )
 }
@@ -58,7 +65,9 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
         ),
         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),
+        // `__CPROVER_rounding_mode` doesn't use `integer` type.
+        // More details in <https://github.com/diffblue/cbmc/issues/7282>
+        int_constant_c_int("__CPROVER_rounding_mode", mm.rounding_mode),
     ]
 }
 

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -55,6 +55,7 @@ pub trait Transformer: Sized {
             Type::IncompleteStruct { tag } => self.transform_type_incomplete_struct(*tag),
             Type::IncompleteUnion { tag } => self.transform_type_incomplete_union(*tag),
             Type::InfiniteArray { typ } => self.transform_type_infinite_array(typ),
+            Type::Integer => self.transform_type_integer(),
             Type::Pointer { typ } => self.transform_type_pointer(typ),
             Type::Signedbv { width } => self.transform_type_signedbv(width),
             Type::Struct { tag, components } => self.transform_type_struct(*tag, components),
@@ -154,6 +155,11 @@ pub trait Transformer: Sized {
         transformed_typ.infinite_array_of()
     }
 
+    /// Transforms a CPROVER integer type
+    fn transform_type_integer(&mut self) -> Type {
+        Type::integer()
+    }
+
     /// Transforms a pointer type (`typ*`)
     fn transform_type_pointer(&mut self, typ: &Type) -> Type {
         let transformed_typ = self.transform_type(typ);

cprover_bindings/src/goto_program/typ.rs

@@ -46,6 +46,8 @@ pub enum Type {
     IncompleteStruct { tag: InternedString },
     /// `union x {}`
     IncompleteUnion { tag: InternedString },
+    /// `integer`: A machine independent integer
+    Integer,
     /// CBMC specific. `typ x[__CPROVER_infinity()]`
     InfiniteArray { typ: Box<Type> },
     /// `typ*`
@@ -163,6 +165,7 @@ impl DatatypeComponent {
             | Double
             | FlexibleArray { .. }
             | Float
+            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -343,6 +346,7 @@ impl Type {
             IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
             IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
             InfiniteArray { .. } => unreachable!("InfiniteArray doesn't have a sizeof"),
+            Integer => unreachable!("Integer doesn't have a sizeof"),
             Pointer { .. } => st.machine_model().pointer_width,
             Signedbv { width } => *width,
             Struct { components, .. } => {
@@ -527,7 +531,7 @@ impl Type {
     pub fn is_integer(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            CInteger(_) | Signedbv { .. } | Unsignedbv { .. } => true,
+            CInteger(_) | Integer | Signedbv { .. } | Unsignedbv { .. } => true,
             _ => false,
         }
     }
@@ -540,6 +544,7 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -595,6 +600,7 @@ impl Type {
             | Double
             | Empty
             | Float
+            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Unsignedbv { .. } => true,
@@ -877,6 +883,7 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -1025,6 +1032,10 @@ impl Type {
         InfiniteArray { typ: Box::new(self) }
     }
 
+    pub fn integer() -> Self {
+        Integer
+    }
+
     /// self *
     pub fn to_pointer(self) -> Self {
         Pointer { typ: Box::new(self) }
@@ -1256,6 +1267,7 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Unsignedbv { .. } => self.zero(),
@@ -1364,6 +1376,7 @@ impl Type {
             Type::InfiniteArray { typ } => {
                 format!("infinite_array_of_{}", typ.to_identifier())
             }
+            Type::Integer => "integer".to_string(),
             Type::Pointer { typ } => format!("pointer_to_{}", typ.to_identifier()),
             Type::Signedbv { width } => format!("signed_bv_{width}"),
             Type::Struct { tag, .. } => format!("struct_{tag}"),

cprover_bindings/src/irep/to_irep.rs

@@ -140,14 +140,16 @@ impl ToIrep for DatatypeComponent {
 impl ToIrep for Expr {
     fn to_irep(&self, mm: &MachineModel) -> Irep {
         if let ExprValue::IntConstant(i) = self.value() {
-            let width = self.typ().native_width(mm).unwrap();
+            let typ_width = self.typ().native_width(mm);
+            let irep_value = if let Some(width) = typ_width {
+                Irep::just_bitpattern_id(i.clone(), width, self.typ().is_signed(mm))
+            } else {
+                Irep::just_int_id(i.clone())
+            };
             Irep {
                 id: IrepId::Constant,
                 sub: vec![],
-                named_sub: linear_map![(
-                    IrepId::Value,
-                    Irep::just_bitpattern_id(i.clone(), width, self.typ().is_signed(mm))
-                )],
+                named_sub: linear_map![(IrepId::Value, irep_value,)],
             }
             .with_location(self.location(), mm)
             .with_type(self.typ(), mm)
@@ -652,6 +654,7 @@ impl ToIrep for Type {
                     named_sub: linear_map![(IrepId::Size, infinity)],
                 }
             }
+            Type::Integer => Irep::just_id(IrepId::Integer),
             Type::Pointer { typ } => Irep {
                 id: IrepId::Pointer,
                 sub: vec![typ.to_irep(mm)],

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -174,6 +174,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 Type::IncompleteStruct { .. } => todo!(),
                 Type::IncompleteUnion { .. } => todo!(),
                 Type::InfiniteArray { .. } => todo!(),
+                Type::Integer => write!(out, "integer")?,
                 Type::Pointer { typ } => {
                     write!(out, "*")?;
                     debug_write_type(ctx, typ, out, indent)?;

kani-dependencies

@@ -1,3 +1,3 @@
-CBMC_VERSION="5.67.0"
+CBMC_VERSION="5.69.1"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.6"

kani-driver/src/call_cbmc.rs

@@ -124,12 +124,17 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize
-            && self.args.concrete_playback.is_none()
-            && !self.args.no_slice_formula
-        {
-            args.push("--slice-formula".into());
-        }
+        // Push `--slice-formula` argument.
+        // Previously, this would happen if the condition below was satisfied:
+        // ```rust
+        // if !self.args.visualize
+        //   && self.args.concrete_playback.is_none()
+        //   && !self.args.no_slice_formula
+        // ```
+        // But for some reason, not pushing it causes a CBMC invariant violation
+        // since version 5.68.0.
+        // <https://github.com/model-checking/kani/issues/1810>
+        args.push("--slice-formula".into());
 
         if self.args.concrete_playback.is_some() {
             args.push("--trace".into());

library/kani/kani_lib.c

@@ -11,6 +11,13 @@ void *calloc(size_t nmemb, size_t size);
 
 typedef __CPROVER_bool bool;
 
+/// Mapping unit to `void` works for functions with no return type but not for
+/// variables with type unit. We treat both uniformly by declaring an empty
+/// struct type: `struct Unit {}` and a global variable `struct Unit VoidUnit`
+/// returned by all void functions (both declared by the Kani compiler).
+struct Unit;
+extern struct Unit VoidUnit;
+
 // `assert` then `assume`
 #define __KANI_assert(cond, msg)            \
     do {                                    \
@@ -70,7 +77,7 @@ uint8_t *__rust_alloc_zeroed(size_t size, size_t align)
 // definition.
 // For safety, refer to the documentation of GlobalAlloc::dealloc:
 // https://doc.rust-lang.org/std/alloc/trait.GlobalAlloc.html#tymethod.dealloc
-void __rust_dealloc(uint8_t *ptr, size_t size, size_t align)
+struct Unit __rust_dealloc(uint8_t *ptr, size_t size, size_t align)
 {
     // TODO: Ensure we are doing the right thing with align
     // https://github.com/model-checking/kani/issues/1168
@@ -79,6 +86,7 @@ void __rust_dealloc(uint8_t *ptr, size_t size, size_t align)
     __KANI_assert(__CPROVER_OBJECT_SIZE(ptr) == size,
                   "rust_dealloc must be called on an object whose allocated size matches its layout");
     free(ptr);
+    return VoidUnit;
 }
 
 // This is a C implementation of the __rust_realloc function that has the following signature:

scripts/kani-regression.sh

@@ -87,16 +87,6 @@ fi
 # Check codegen of firecracker
 time "$SCRIPT_DIR"/codegen-firecracker.sh
 
-# Check that we can use Kani on crates with a diamond dependency graph,
-# with two different versions of the same crate.
-#
-#         dependency1
-#        /           \ v0.1.0
-#   main             dependency3
-#        \           / v0.1.1
-#         dependency2
-time "$KANI_DIR"/tests/kani-dependency-test/diamond-dependency/run-dependency-test.sh
-
 # Check that documentation compiles.
 cargo doc --workspace --no-deps --exclude std
 

tests/cargo-kani/dependency-test/diamond-dependency/harness.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/kani/ForeignItems/lib.c

@@ -7,6 +7,13 @@
 #include <stdio.h>
 #include <string.h>
 
+/// Mapping unit to `void` works for functions with no return type but not for
+/// variables with type unit. We treat both uniformly by declaring an empty
+/// struct type: `struct Unit {}` and a global variable `struct Unit VoidUnit`
+/// returned by all void functions (both declared by the Kani compiler).
+struct Unit;
+extern struct Unit VoidUnit;
+
 size_t my_add(size_t num, ...)
 {
     va_list argp;
@@ -48,7 +55,15 @@ struct Foo2 {
 
 uint32_t S = 12;
 
-void update_static() { S++; }
+// Note: We changed the return type from `void` to `struct Unit` when upgrading
+// to a newer CBMC version with stricter type-checking. This is a temporary
+// change until C-FFI support is added.
+// <https://github.com/model-checking/kani/issues/1817>
+struct Unit update_static()
+{
+    S++;
+    return VoidUnit;
+}
 
 uint32_t takes_int(uint32_t i) { return i + 2; }
 
@@ -63,7 +78,15 @@ uint32_t takes_ptr_option(uint32_t *p)
     }
 }
 
-void mutates_ptr(uint32_t *p) { *p -= 1; }
+// Note: We changed the return type from `void` to `struct Unit` when upgrading
+// to a newer CBMC version with stricter type-checking. This is a temporary
+// change until C-FFI support is added.
+// <https://github.com/model-checking/kani/issues/1817>
+struct Unit mutates_ptr(uint32_t *p)
+{
+    *p -= 1;
+    return VoidUnit;
+}
 
 uint32_t name_in_c(uint32_t i) { return i + 2; }