Merge branch 'main' into kanicov-tool

adpaco-aws · Sep 24, 2024 · eba08bb · eba08bb
2 parents 94bb87a + 9dc09e7
commit eba08bb
Show file tree

Hide file tree

Showing 133 changed files with 831 additions and 550 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -257,6 +257,15 @@ dependencies = [
  "tracing",
 ]
 
+[[package]]
+name = "crc32fast"
+version = "1.4.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3"
+dependencies = [
+ "cfg-if",
+]
+
 [[package]]
 name = "crossbeam-deque"
 version = "0.8.5"
@@ -485,6 +494,7 @@ dependencies = [
  "kani_metadata",
  "lazy_static",
  "num",
+ "object",
  "quote",
  "regex",
  "serde",
@@ -741,6 +751,19 @@ dependencies = [
  "autocfg",
 ]
 
+[[package]]
+name = "object"
+version = "0.36.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "084f1a5821ac4c651660a94a7153d27ac9d8a53736203f58b31945ded098070a"
+dependencies = [
+ "crc32fast",
+ "hashbrown",
+ "indexmap",
+ "memchr",
+ "wasmparser",
+]
+
 [[package]]
 name = "once_cell"
 version = "1.19.0"
@@ -1461,6 +1484,15 @@ version = "0.11.0+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
 
+[[package]]
+name = "wasmparser"
+version = "0.216.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bcdee6bea3619d311fb4b299721e89a986c3470f804b6d534340e412589028e3"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "which"
 version = "6.0.3"

diff --git a/cprover_bindings/src/cbmc_string.rs b/cprover_bindings/src/cbmc_string.rs
@@ -3,9 +3,9 @@
 
 use lazy_static::lazy_static;
 use std::sync::Mutex;
+use string_interner::StringInterner;
 use string_interner::backend::StringBackend;
 use string_interner::symbol::SymbolU32;
-use string_interner::StringInterner;
 
 /// This class implements an interner for Strings.
 /// CBMC objects to have a large number of strings which refer to names: symbols, files, etc.

diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs
@@ -8,8 +8,8 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
 where

diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
@@ -285,13 +285,10 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type {
     // give the struct the name "overflow_result_<type>", e.g.
     // "overflow_result_Unsignedbv"
     let name: InternedString = format!("overflow_result_{operand_type:?}").into();
-    Type::struct_type(
-        name,
-        vec![
-            DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
-            DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
-        ],
-    )
+    Type::struct_type(name, vec![
+        DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type),
+        DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()),
+    ])
 }
 
 ///////////////////////////////////////////////////////////////////////////////////////////////

diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs
@@ -17,8 +17,8 @@ mod typ;
 
 pub use builtin::BuiltinFn;
 pub use expr::{
-    arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue,
-    SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, ArithmeticOverflowResult,
+    BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, arithmetic_overflow_result_type,
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};

diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use super::super::{env, MachineModel};
+use super::super::{MachineModel, env};
 use super::{BuiltinFn, FunctionContract, Stmt, Symbol};
 use crate::InternedString;
 use std::collections::BTreeMap;

diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use self::DatatypeComponent::*;
 use self::Type::*;
-use super::super::utils::{aggr_tag, max_int, min_int};
 use super::super::MachineModel;
+use super::super::utils::{aggr_tag, max_int, min_int};
 use super::{Expr, SymbolTable};
 use crate::cbmc_string::InternedString;
 use std::collections::BTreeMap;
@@ -1598,10 +1598,10 @@ mod type_tests {
     fn check_typedef_struct_properties() {
         // Create a struct with a random field.
         let struct_name: InternedString = "MyStruct".into();
-        let struct_type = Type::struct_type(
-            struct_name,
-            vec![DatatypeComponent::Field { name: "field".into(), typ: Double }],
-        );
+        let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field {
+            name: "field".into(),
+            typ: Double,
+        }]);
         // Insert a field to the sym table to represent the struct field.
         let mut sym_table = SymbolTable::new(machine_model_test_stub());
         sym_table.ensure(struct_type.type_name().unwrap(), |_, name| {

diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -1205,12 +1205,12 @@ mod sharing_stats {
 mod tests {
     use super::GotoBinarySerializer;
     use super::IrepNumbering;
+    use crate::InternedString;
     use crate::cbmc_string::InternString;
-    use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
     use crate::irep::Irep;
     use crate::irep::IrepId;
+    use crate::irep::goto_binary_serde::GotoBinaryDeserializer;
     use crate::linear_map;
-    use crate::InternedString;
     use linear_map::LinearMap;
     use std::io::BufWriter;
     /// Utility function : creates a Irep representing a single symbol.

diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! The actual `Irep` structure, and associated constructors, getters, and setters.
 
-use super::super::goto_program::{Location, Type};
 use super::super::MachineModel;
+use super::super::goto_program::{Location, Type};
 use super::{IrepId, ToIrep};
 use crate::cbmc_string::InternedString;
 use crate::linear_map;