Merge remote-tracking branch 'origin/main' into issue-3612-can-deref-2

Conflicts: - kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs - kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs - kani-compiler/src/kani_middle/abi.rs - kani-compiler/src/kani_middle/attributes.rs - kani-compiler/src/kani_middle/kani_functions.rs - kani-compiler/src/kani_middle/transform/check_uninit/mod.rs - kani-compiler/src/kani_middle/transform/kani_intrinsics.rs - kani-compiler/src/kani_middle/transform/mod.rs - kani-compiler/src/kani_queries/mod.rs - library/kani_core/src/mem.rs - library/kani_core/src/mem_init.rs
model-checking · Nov 18, 2024 · f5c2135 · f5c2135
2 parents 61ea50b + df1550a
commit f5c2135
Show file tree

Hide file tree

Showing 48 changed files with 916 additions and 575 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -166,12 +166,12 @@ dependencies = [
 
 [[package]]
 name = "bstr"
-version = "1.10.0"
+version = "1.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "40723b8fb387abc38f4f4a37c09073622e41dd12327033091ef8950659e6dc0c"
+checksum = "1a68f1f47cdf0ec8ee4b941b2eee2a80cb796db73118c0dd09ac63fbe405be22"
 dependencies = [
  "memchr",
- "regex-automata 0.4.8",
+ "regex-automata 0.4.9",
  "serde",
 ]
 
@@ -231,9 +231,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.1.37"
+version = "1.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "40545c26d092346d8a8dab71ee48e7685a7a9cba76e634790c215b41a4a7b4cf"
+checksum = "fd9de9f2205d5ef3fd67e685b0df337994ddd4495e2a28d185500d0e1edfea47"
 dependencies = [
  "shlex",
 ]
@@ -253,7 +253,6 @@ dependencies = [
  "clap",
  "colored",
  "convert_case 0.6.0",
- "derivative",
  "derive-visitor",
  "env_logger",
  "hashlink",
@@ -285,19 +284,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.20"
+version = "4.5.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b97f376d85a664d5837dbae44bf546e6477a679ff6610010f17276f686d867e8"
+checksum = "fb3b4b9e5a7c7514dfa52869339ee98b3156b0bfb4e8a77c4ff4babb64b1604f"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.20"
+version = "4.5.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "19bc80abd44e4bed93ca373a0704ccbd1b710dc5749406201bb018272808dc54"
+checksum = "b17a95aa67cc7b5ebd32aa5370189aa0d79069ef1c64ce893bd30fb24bff20ec"
 dependencies = [
  "anstream",
  "anstyle",
@@ -319,9 +318,9 @@ dependencies = [
 
 [[package]]
 name = "clap_lex"
-version = "0.7.2"
+version = "0.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"
+checksum = "afb84c814227b90d6895e01398aee0d8033c00e7466aca416fb6a8e0eb19d8a7"
 
 [[package]]
 name = "colorchoice"
@@ -350,14 +349,14 @@ dependencies = [
 
 [[package]]
 name = "comfy-table"
-version = "7.1.1"
+version = "7.1.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b34115915337defe99b2aff5c2ce6771e5fbc4079f4b506301f5cf394c8452f7"
+checksum = "24f165e7b643266ea80cb858aed492ad9280e3e05ce24d4a99d7d7b889b6a4d9"
 dependencies = [
  "crossterm",
  "strum",
  "strum_macros",
- "unicode-width",
+ "unicode-width 0.2.0",
 ]
 
 [[package]]
@@ -386,7 +385,7 @@ dependencies = [
  "encode_unicode",
  "lazy_static",
  "libc",
- "unicode-width",
+ "unicode-width 0.1.14",
  "windows-sys 0.52.0",
 ]
 
@@ -447,14 +446,14 @@ checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80"
 
 [[package]]
 name = "crossterm"
-version = "0.27.0"
+version = "0.28.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df"
+checksum = "829d955a0bb380ef178a640b91779e3987da38c9aea133b20614cfed8cdea9c6"
 dependencies = [
  "bitflags 2.6.0",
  "crossterm_winapi",
- "libc",
  "parking_lot",
+ "rustix",
  "winapi",
 ]
 
@@ -497,17 +496,6 @@ dependencies = [
  "powerfmt",
 ]
 
-[[package]]
-name = "derivative"
-version = "2.2.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "derive-visitor"
 version = "0.4.0"
@@ -611,7 +599,7 @@ version = "0.2.21"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "14dbbfd5c71d70241ecf9e6f13737f7b5ce823821063188d7e46c41d371eebd5"
 dependencies = [
- "unicode-width",
+ "unicode-width 0.1.14",
 ]
 
 [[package]]
@@ -890,9 +878,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
 
 [[package]]
 name = "libc"
-version = "0.2.162"
+version = "0.2.164"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398"
+checksum = "433bfe06b8c75da9b2e3fbea6e5329ff87748f0b144ef75306e674c3f6f7c13f"
 
 [[package]]
 name = "linear-map"
@@ -1239,7 +1227,7 @@ checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579"
 dependencies = [
  "arrayvec 0.5.2",
  "typed-arena",
- "unicode-width",
+ "unicode-width 0.1.14",
 ]
 
 [[package]]
@@ -1275,9 +1263,9 @@ dependencies = [
 
 [[package]]
 name = "psm"
-version = "0.1.23"
+version = "0.1.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aa37f80ca58604976033fae9515a8a2989fc13797d953f7c04fb8fa36a11f205"
+checksum = "200b9ff220857e53e184257720a14553b2f4aa02577d2ed9842d45d4b9654810"
 dependencies = [
  "cc",
 ]
@@ -1358,7 +1346,7 @@ checksum = "b544ef1b4eac5dc2db33ea63606ae9ffcfac26c1416a2806ae0bf5f56b201191"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata 0.4.8",
+ "regex-automata 0.4.9",
  "regex-syntax 0.8.5",
 ]
 
@@ -1373,9 +1361,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.8"
+version = "0.4.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "368758f23274712b504848e9d5a6f010445cc8b87a7cdb4d7cbee666c1288da3"
+checksum = "809e8dc61f6de73b46c85f4c96486310fe304c434cfa43669d7b40f711150908"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -1482,9 +1470,9 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.214"
+version = "1.0.215"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5"
+checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f"
 dependencies = [
  "serde_derive",
 ]
@@ -1500,9 +1488,9 @@ dependencies = [
 
 [[package]]
 name = "serde_derive"
-version = "1.0.214"
+version = "1.0.215"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766"
+checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1511,9 +1499,9 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.132"
+version = "1.0.133"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d726bfaff4b320266d395898905d0eba0345aae23b54aee3a737e260fd46db03"
+checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377"
 dependencies = [
  "indexmap",
  "itoa",
@@ -1965,6 +1953,12 @@ version = "0.1.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
 
+[[package]]
+name = "unicode-width"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fc81956842c57dac11422a97c3b8195a1ff727f06e85c84ed2e8aa277c9a0fd"
+
 [[package]]
 name = "unsafe-libyaml"
 version = "0.2.11"

diff --git a/charon b/charon
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
@@ -898,13 +898,9 @@ impl Type {
         } else if concrete_self.is_scalar() && concrete_other.is_scalar() {
             concrete_self == concrete_other
         } else if concrete_self.is_struct_like() && concrete_other.is_scalar() {
-            concrete_self
-                .unwrap_transparent_type(st)
-                .map_or(false, |wrapped| wrapped == *concrete_other)
+            concrete_self.unwrap_transparent_type(st) == Some(concrete_other.clone())
         } else if concrete_self.is_scalar() && concrete_other.is_struct_like() {
-            concrete_other
-                .unwrap_transparent_type(st)
-                .map_or(false, |wrapped| wrapped == *concrete_self)
+            concrete_other.unwrap_transparent_type(st) == Some(concrete_self.clone())
         } else if concrete_self.is_struct_like() && concrete_other.is_struct_like() {
             let self_components = concrete_self.get_non_empty_components(st).unwrap();
             let other_components = concrete_other.get_non_empty_components(st).unwrap();

diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs
@@ -704,10 +704,7 @@ where
     /// Reads a reference encoded string from the byte stream.
     fn read_numbered_string_ref(&mut self) -> io::Result<NumberedString> {
         let string_number_result = self.read_usize_varenc();
-        let string_number = match string_number_result {
-            Ok(number) => number,
-            Err(error) => return Err(error),
-        };
+        let string_number = string_number_result?;
         if self.is_first_read_string(string_number) {
             // read raw string
             let mut string_buf: Vec<u8> = Vec::new();
@@ -779,10 +776,7 @@ where
     /// Reads a NumberedIrep from the byte stream.
     fn read_numbered_irep_ref(&mut self) -> io::Result<NumberedIrep> {
         let irep_number_result = self.read_usize_varenc();
-        let irep_number = match irep_number_result {
-            Ok(number) => number,
-            Err(error) => return Err(error),
-        };
+        let irep_number = irep_number_result?;
 
         if self.is_first_read_irep(irep_number) {
             let id = self.read_numbered_string_ref()?.number;

diff --git a/deny.toml b/deny.toml
@@ -1,12 +1,6 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-[graph]
-# derivative is marked as unmaintained by RUSTSEC but still used in
-# Charon. We exclude it from the deny check until derivative is replaced
-# from Charon (https://github.com/AeneasVerif/charon/pull/459).
-exclude = ["derivative"]
-
 # This section is considered when running `cargo deny check advisories`
 # More documentation for the advisories section can be found here:
 # https://embarkstudios.github.io/cargo-deny/checks/advisories/cfg.html

diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -326,19 +326,16 @@ impl CodegenBackend for LlbcCodegenBackend {
         codegen_results: CodegenResults,
         outputs: &OutputFilenames,
     ) -> Result<(), ErrorGuaranteed> {
-        let requested_crate_types = &codegen_results.crate_info.crate_types;
+        let requested_crate_types = &codegen_results.crate_info.crate_types.clone();
+        let local_crate_name = codegen_results.crate_info.local_crate_name;
+        let link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs);
         for crate_type in requested_crate_types {
-            let out_fname = out_filename(
-                sess,
-                *crate_type,
-                outputs,
-                codegen_results.crate_info.local_crate_name,
-            );
+            let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name);
             let out_path = out_fname.as_path();
             debug!(?crate_type, ?out_path, "link");
             if *crate_type == CrateType::Rlib {
                 // Emit the `rlib` that contains just one file: `<crate>.rmeta`
-                link_binary(sess, &ArArchiveBuilderBuilder, &codegen_results, outputs)?
+                link_result?
             } else {
                 // Write the location of the kani metadata file in the requested compiler output file.
                 let base_filepath = outputs.path(OutputType::Object);

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -156,13 +156,14 @@ impl GotocCtx<'_> {
         counter_data: &str,
         span: SpanStable,
         source_region: SourceRegion,
+        file_name: &str,
     ) -> Stmt {
         let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
         // `assert(false)`.
-        let msg = format!("{counter_data} - {source_region:?}");
+        let msg = format!("{counter_data} - {file_name}:{source_region:?}");
         self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
     }
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -223,8 +223,9 @@ pub mod rustc_smir {
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::mir::coverage::SourceRegion;
     use rustc_middle::ty::TyCtxt;
-    use stable_mir::Opaque;
+    use rustc_smir::rustc_internal;
     use stable_mir::mir::mono::Instance;
+    use stable_mir::{Filename, Opaque};
 
     type CoverageOpaque = stable_mir::Opaque;
 
@@ -234,7 +235,7 @@ pub mod rustc_smir {
         tcx: TyCtxt,
         coverage_opaque: &CoverageOpaque,
         instance: Instance,
-    ) -> Option<SourceRegion> {
+    ) -> Option<(SourceRegion, Filename)> {
         let cov_term = parse_coverage_opaque(coverage_opaque);
         region_from_coverage(tcx, cov_term, instance)
     }
@@ -246,7 +247,7 @@ pub mod rustc_smir {
         tcx: TyCtxt<'_>,
         coverage: CovTerm,
         instance: Instance,
-    ) -> Option<SourceRegion> {
+    ) -> Option<(SourceRegion, Filename)> {
         // We need to pull the coverage info from the internal MIR instance.
         let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
         let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));
@@ -258,7 +259,10 @@ pub mod rustc_smir {
             for mapping in &cov_info.mappings {
                 let Code(term) = mapping.kind else { unreachable!() };
                 if term == coverage {
-                    return Some(mapping.source_region.clone());
+                    return Some((
+                        mapping.source_region.clone(),
+                        rustc_internal::stable(cov_info.body_span).get_filename(),
+                    ));
                 }
             }
         }

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -165,9 +165,9 @@ impl GotocCtx<'_> {
                 let counter_data = format!("{coverage_opaque:?} ${function_name}$");
                 let maybe_source_region =
                     region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
-                if let Some(source_region) = maybe_source_region {
+                if let Some((source_region, file_name)) = maybe_source_region {
                     let coverage_stmt =
-                        self.codegen_coverage(&counter_data, stmt.span, source_region);
+                        self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name);
                     // TODO: Avoid single-statement blocks when conversion of
                     // standalone statements to the irep format is fixed.
                     // More details in <https://github.com/model-checking/kani/issues/3012>
+10 −27		.github/workflows/ci.yml
+5 −1		README.md
+10 −0		charon-ml/src/Collections.ml
+4 −8		charon-ml/src/LlbcAstUtils.ml
+16 −10		charon-ml/src/MetaUtils.ml
+0 −12		charon/Cargo.lock
+0 −1		charon/Cargo.toml
+93 −0		charon/src/ast/expressions_utils.rs
+9 −6		charon/src/ast/types.rs
+100 −0		charon/src/ast/types_utils.rs
+5 −19		charon/src/bin/charon-driver/translate/translate_constants.rs
+1 −3		charon/src/bin/charon-driver/translate/translate_ctx.rs
+17 −38		charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+13 −36		charon/src/bin/charon-driver/translate/translate_predicates.rs
+7 −13		charon/src/bin/charon-driver/translate/translate_traits.rs
+56 −79		charon/src/bin/charon-driver/translate/translate_types.rs
+138 −0		charon/src/transform/index_intermediate_assigns.rs
+4 −0		charon/src/transform/mod.rs
+52 −0		charon/tests/ui/arrays.out
+8 −0		charon/tests/ui/arrays.rs