Revert "Upgrade to CBMC 5.68.0 (with fixes) (#1811)"

This reverts commit 3007e84.

Author: adpaco-aws

cprover_bindings/src/env.rs

@@ -12,13 +12,6 @@ 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>,
 {
@@ -30,7 +23,7 @@ fn int_constant_from_bool(name: &str, value: bool) -> Symbol {
         name,
         name,
         name,
-        Expr::int_constant(if value { 1 } else { 0 }, Type::integer()),
+        Expr::int_constant(if value { 1 } else { 0 }, Type::c_int()),
         Location::none(),
     )
 }
@@ -65,9 +58,7 @@ 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),
-        // `__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),
+        int_constant("__CPROVER_rounding_mode", mm.rounding_mode),
     ]
 }
 

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -55,7 +55,6 @@ 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),
@@ -155,11 +154,6 @@ 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,8 +46,6 @@ 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*`
@@ -165,7 +163,6 @@ impl DatatypeComponent {
             | Double
             | FlexibleArray { .. }
             | Float
-            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -346,7 +343,6 @@ 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, .. } => {
@@ -531,7 +527,7 @@ impl Type {
     pub fn is_integer(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            CInteger(_) | Integer | Signedbv { .. } | Unsignedbv { .. } => true,
+            CInteger(_) | Signedbv { .. } | Unsignedbv { .. } => true,
             _ => false,
         }
     }
@@ -544,7 +540,6 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
-            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -600,7 +595,6 @@ impl Type {
             | Double
             | Empty
             | Float
-            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Unsignedbv { .. } => true,
@@ -883,7 +877,6 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
-            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Struct { .. }
@@ -1032,10 +1025,6 @@ impl Type {
         InfiniteArray { typ: Box::new(self) }
     }
 
-    pub fn integer() -> Self {
-        Integer
-    }
-
     /// self *
     pub fn to_pointer(self) -> Self {
         Pointer { typ: Box::new(self) }
@@ -1267,7 +1256,6 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
-            | Integer
             | Pointer { .. }
             | Signedbv { .. }
             | Unsignedbv { .. } => self.zero(),
@@ -1376,7 +1364,6 @@ 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,16 +140,14 @@ impl ToIrep for DatatypeComponent {
 impl ToIrep for Expr {
     fn to_irep(&self, mm: &MachineModel) -> Irep {
         if let ExprValue::IntConstant(i) = self.value() {
-            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())
-            };
+            let width = self.typ().native_width(mm).unwrap();
             Irep {
                 id: IrepId::Constant,
                 sub: vec![],
-                named_sub: linear_map![(IrepId::Value, irep_value,)],
+                named_sub: linear_map![(
+                    IrepId::Value,
+                    Irep::just_bitpattern_id(i.clone(), width, self.typ().is_signed(mm))
+                )],
             }
             .with_location(self.location(), mm)
             .with_type(self.typ(), mm)
@@ -654,7 +652,6 @@ 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,7 +174,6 @@ 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.69.1"
+CBMC_VERSION="5.67.0"
 # 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,17 +124,12 @@ impl KaniSession {
             args.push("--validate-ssa-equation".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.visualize
+            && self.args.concrete_playback.is_none()
+            && !self.args.no_slice_formula
+        {
+            args.push("--slice-formula".into());
+        }
 
         if self.args.concrete_playback.is_some() {
             args.push("--trace".into());

library/kani/kani_lib.c

@@ -11,13 +11,6 @@ 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 {                                    \
@@ -77,7 +70,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
-struct Unit __rust_dealloc(uint8_t *ptr, size_t size, size_t align)
+void __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
@@ -86,7 +79,6 @@ struct Unit __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,6 +87,16 @@ 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,53 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# We're explicitly checking output rather than failing if the test fails
+#set -eu
+
+echo
+echo "Starting Diamond Dependency Test..."
+echo
+
+# Test for platform
+PLATFORM=$(uname -sp)
+if [[ $PLATFORM == "Linux x86_64" ]]
+then
+  TARGET="x86_64-unknown-linux-gnu"
+elif [[ $PLATFORM == "Darwin i386" ]]
+then
+  TARGET="x86_64-apple-darwin"
+else
+  echo
+  echo "Test only works on Linux or OSX x86 platforms, skipping..."
+  echo
+  exit 0
+fi
+
+# Compile crates with Kani backend
+cd $(dirname $0)
+rm -rf build
+RUST_BACKTRACE=1 cargo kani --target-dir build --only-codegen --keep-temps --verbose --no-assertion-reach-checks
+
+# Convert from JSON to Gotoc
+cd build/${TARGET}/debug/deps/
+ls *.symtab.json | xargs symtab2gb
+
+# Add the entry point and remove unused functions
+goto-cc --function harness *.out -o a.out
+goto-instrument --drop-unused-functions a.out b.out
+
+# Run the solver
+RESULT="/tmp/dependency_test_result.txt"
+cbmc b.out &> $RESULT
+if ! grep -q "VERIFICATION SUCCESSFUL" $RESULT; then
+  cat $RESULT
+  echo
+  echo "Failed dependency test"
+  echo
+  exit 1
+fi
+
+echo
+echo "Finished Diamond Dependency Test successfully..."
+echo

tests/cargo-kani/dependency-test/dependency3/Cargo.toml renamed to tests/kani-dependency-test/dependency3/Cargo.toml

@@ -7,13 +7,6 @@
 #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;
@@ -55,15 +48,7 @@ struct Foo2 {
 
 uint32_t S = 12;
 
-// 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;
-}
+void update_static() { S++; }
 
 uint32_t takes_int(uint32_t i) { return i + 2; }
 
@@ -78,15 +63,7 @@ uint32_t takes_ptr_option(uint32_t *p)
     }
 }
 
-// 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;
-}
+void mutates_ptr(uint32_t *p) { *p -= 1; }
 
 uint32_t name_in_c(uint32_t i) { return i + 2; }