Add zero-init, and put it behind an unsound feature flag (rust-lang#1521)

Author: danielsn

.github/workflows/kani.yml

@@ -33,6 +33,25 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
+  experimental-features-regression:
+    runs-on: ubuntu-20.04
+    env: 
+      KANI_ENABLE_UNSOUND_EXPERIMENTS: 1
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v2
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+            os: ubuntu-20.04
+
+      - name: Build Kani
+        run: cargo build
+
+      - name: Execute Kani regression
+        run: ./scripts/kani-regression.sh
+
   perf:
     runs-on: ubuntu-20.04
     steps:

cprover_bindings/src/goto_program/typ.rs

@@ -185,13 +185,13 @@ impl DatatypeComponent {
     }
 
     pub fn field<T: Into<InternedString>>(name: T, typ: Type) -> Self {
+        let name = name.into();
         assert!(
             Self::typecheck_datatype_field(&typ),
             "Illegal field.\n\tName: {}\n\tType: {:?}",
-            name.into(),
+            name,
             typ
         );
-        let name = name.into();
         Field { name, typ }
     }
 

kani-compiler/Cargo.toml

@@ -35,6 +35,7 @@ tracing-tree = "0.2.0"
 default = ['cprover']
 cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde',
     'serde_json', "strum", "strum_macros"]
+unsound_experiments = ["kani_queries/unsound_experiments"]
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

kani-compiler/kani_queries/Cargo.toml

@@ -8,5 +8,8 @@ edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
 
+[features]
+unsound_experiments = []
+
 [dependencies]
 tracing = {version = "0.1"}

kani-compiler/kani_queries/src/lib.rs

@@ -3,6 +3,15 @@
 
 use std::sync::atomic::{AtomicBool, Ordering};
 
+#[cfg(feature = "unsound_experiments")]
+mod unsound_experiments;
+
+#[cfg(feature = "unsound_experiments")]
+use {
+    crate::unsound_experiments::UnsoundExperiments,
+    std::sync::{Arc, Mutex},
+};
+
 pub trait UserInput {
     fn set_symbol_table_passes(&mut self, passes: Vec<String>);
     fn get_symbol_table_passes(&self) -> Vec<String>;
@@ -18,6 +27,9 @@ pub trait UserInput {
 
     fn set_ignore_global_asm(&mut self, global_asm: bool);
     fn get_ignore_global_asm(&self) -> bool;
+
+    #[cfg(feature = "unsound_experiments")]
+    fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>>;
 }
 
 #[derive(Debug, Default)]
@@ -27,6 +39,8 @@ pub struct QueryDb {
     symbol_table_passes: Vec<String>,
     json_pretty_print: AtomicBool,
     ignore_global_asm: AtomicBool,
+    #[cfg(feature = "unsound_experiments")]
+    unsound_experiments: Arc<Mutex<UnsoundExperiments>>,
 }
 
 impl UserInput for QueryDb {
@@ -69,4 +83,9 @@ impl UserInput for QueryDb {
     fn get_ignore_global_asm(&self) -> bool {
         self.ignore_global_asm.load(Ordering::Relaxed)
     }
+
+    #[cfg(feature = "unsound_experiments")]
+    fn get_unsound_experiments(&self) -> Arc<Mutex<UnsoundExperiments>> {
+        self.unsound_experiments.clone()
+    }
 }

kani-compiler/kani_queries/src/unsound_experiments.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![cfg(feature = "unsound_experiments")]
+
+#[derive(Debug, Default)]
+pub struct UnsoundExperiments {
+    /// Zero initilize variables.
+    /// This is useful for experiments to see whether assigning constant values produces better
+    /// performance by allowing CBMC to do more constant propegation.
+    /// Unfortunatly, it is unsafe to use for production code, since it may unsoundly hide bugs.
+    pub zero_init_vars: bool,
+}

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

@@ -77,7 +77,8 @@ impl<'tcx> GotocCtx<'tcx> {
             // Index 0 represents the return value, which does not need to be
             // declared in the first block
             if lc.index() < 1 || lc.index() > mir.arg_count {
-                self.current_fn_mut().push_onto_block(Stmt::decl(sym_e, None, loc));
+                let init = self.codegen_default_initializer(&sym_e);
+                self.current_fn_mut().push_onto_block(Stmt::decl(sym_e, init, loc));
             }
         });
     }

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

@@ -56,23 +56,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         .assign(self.codegen_rvalue(r, location), location)
                 }
             }
-            StatementKind::Deinit(place) => {
-                // From rustc doc: "This writes `uninit` bytes to the entire place."
-                // Our model of GotoC has a similar statement, which is later lowered
-                // to assigning a Nondet in CBMC, with a comment specifying that it
-                // corresponds to a Deinit.
-                let dst_mir_ty = self.place_ty(place);
-                let dst_type = self.codegen_ty(dst_mir_ty);
-                let layout = self.layout_of(dst_mir_ty);
-                if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
-                    // We ignore assignment for all zero size types
-                    Stmt::skip(location)
-                } else {
-                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
-                        .goto_expr
-                        .deinit(location)
-                }
-            }
+            StatementKind::Deinit(place) => self.codegen_deinit(place, location),
             StatementKind::SetDiscriminant { place, variant_index } => {
                 // this requires place points to an enum type.
                 let pt = self.place_ty(place);
@@ -277,6 +261,25 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// From rustc doc: "This writes `uninit` bytes to the entire place."
+    /// Our model of GotoC has a similar statement, which is later lowered
+    /// to assigning a Nondet in CBMC, with a comment specifying that it
+    /// corresponds to a Deinit.
+    #[cfg(not(feature = "unsound_experiments"))]
+    fn codegen_deinit(&mut self, place: &Place<'tcx>, loc: Location) -> Stmt {
+        let dst_mir_ty = self.place_ty(place);
+        let dst_type = self.codegen_ty(dst_mir_ty);
+        let layout = self.layout_of(dst_mir_ty);
+        if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
+            // We ignore assignment for all zero size types
+            Stmt::skip(loc)
+        } else {
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
+                .goto_expr
+                .deinit(loc)
+        }
+    }
+
     /// A special case handler to codegen `return ();`
     fn codegen_ret_unit(&mut self) -> Stmt {
         let is_file_local = false;

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

@@ -676,6 +676,15 @@ impl<'tcx> GotocCtx<'tcx> {
         Type::struct_tag(name)
     }
 
+    /// Codegens the an initalizer for variables without one.
+    /// By default, returns `None` which leaves the variable uninitilized.
+    /// In CBMC, this translates to a NONDET value.
+    /// In the future, we might want to replace this with `Poison`.
+    #[cfg(not(feature = "unsound_experiments"))]
+    pub fn codegen_default_initializer(&self, _e: &Expr) -> Option<Expr> {
+        None
+    }
+
     /// The unit type in Rust is an empty struct in gotoc
     pub fn codegen_ty_unit(&mut self) -> Type {
         self.ensure_struct(UNIT_TYPE_EMPTY_STRUCT_NAME, "()", |_, _| vec![])

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -161,6 +161,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let c = self.current_fn_mut().get_and_incr_counter();
         let var =
             self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
+        let value = value.or_else(|| self.codegen_default_initializer(&var));
         let decl = Stmt::decl(var.clone(), value, loc);
         (var, decl)
     }