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)
     }

kani-compiler/src/main.rs

@@ -29,6 +29,7 @@ extern crate rustc_target;
 mod codegen_cprover_gotoc;
 mod parser;
 mod session;
+mod unsound_experiments;
 
 use crate::session::init_session;
 use clap::ArgMatches;
@@ -90,6 +91,11 @@ fn main() -> Result<(), &'static str> {
     queries.set_check_assertion_reachability(matches.is_present(parser::ASSERTION_REACH_CHECKS));
     queries.set_output_pretty_json(matches.is_present(parser::PRETTY_OUTPUT_FILES));
     queries.set_ignore_global_asm(matches.is_present(parser::IGNORE_GLOBAL_ASM));
+    #[cfg(feature = "unsound_experiments")]
+    crate::unsound_experiments::arg_parser::add_unsound_experiment_args_to_queries(
+        &mut queries,
+        &matches,
+    );
 
     // Generate rustc args.
     let rustc_args = generate_rustc_args(&matches);

kani-compiler/src/parser.rs

@@ -53,7 +53,7 @@ const KANI_ARGS_FLAG: &str = "--kani-flags";
 
 /// Configure command options for the Kani compiler.
 pub fn parser<'a, 'b>() -> App<'a, 'b> {
-    app_from_crate!()
+    let app = app_from_crate!()
         .setting(AppSettings::TrailingVarArg) // This allow us to fwd commands to rustc.
         .setting(clap::AppSettings::AllowLeadingHyphen)
         .version_short("?")
@@ -142,7 +142,11 @@ pub fn parser<'a, 'b>() -> App<'a, 'b> {
             Arg::with_name(IGNORE_GLOBAL_ASM)
                 .long("--ignore-global-asm")
                 .help("Suppress error due to the existence of global_asm in a crate"),
-        )
+        );
+    #[cfg(feature = "unsound_experiments")]
+    let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);
+
+    app
 }
 
 /// Retrieves the arguments from the command line and process hack to incorporate CARGO arguments.

kani-compiler/src/unsound_experiments/arg_parser.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![cfg(feature = "unsound_experiments")]
+use clap::{App, Arg, ArgMatches};
+use kani_queries::{QueryDb, UserInput};
+/// Option used for zero initilizing variables.
+const ZERO_INIT_VARS: &str = "unsound-experiment-zero-init-vars";
+
+pub fn add_unsound_experiments_to_parser<'a, 'b>(app: App<'a, 'b>) -> App<'a, 'b> {
+    app.arg(
+        Arg::with_name(ZERO_INIT_VARS)
+            .long(ZERO_INIT_VARS)
+            .help("POTENTIALLY UNSOUND EXPERIMENTAL FEATURE. Zero initialize variables"),
+    )
+}
+
+pub fn add_unsound_experiment_args_to_queries(queries: &mut QueryDb, matches: &ArgMatches) {
+    queries.get_unsound_experiments().lock().unwrap().zero_init_vars =
+        matches.is_present(ZERO_INIT_VARS);
+}

kani-compiler/src/unsound_experiments/mod.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![cfg(feature = "unsound_experiments")]
+
+pub mod arg_parser;
+mod zero_init;

kani-compiler/src/unsound_experiments/zero_init.rs

@@ -0,0 +1,45 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![cfg(feature = "unsound_experiments")]
+use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::unwrap_or_return_codegen_unimplemented_stmt;
+use cbmc::goto_program::{Expr, Location, Stmt};
+use kani_queries::UserInput;
+use rustc_middle::mir::Place;
+use rustc_middle::ty::layout::LayoutOf;
+
+impl<'tcx> GotocCtx<'tcx> {
+    /// Codegens the an initalizer for variables without one.
+    /// If the zero initilizer flag is set, does zero init (if possible).
+    /// Otherwise, returns `None` which leaves the variable uninitilized.
+    /// In CBMC, this translates to a NONDET value.
+    pub fn codegen_default_initializer(&mut self, e: &Expr) -> Option<Expr> {
+        if self.queries.get_unsound_experiments().lock().unwrap().zero_init_vars {
+            Some(e.typ().zero_initializer(&self.symbol_table))
+        } else {
+            None
+        }
+    }
+
+    /// 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.
+    pub 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);
+        let goto_place =
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)).goto_expr;
+        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 if self.queries.get_unsound_experiments().lock().unwrap().zero_init_vars {
+            let init = goto_place.typ().zero_initializer(&self.symbol_table);
+            goto_place.assign(init, loc)
+        } else {
+            goto_place.deinit(loc)
+        }
+    }
+}

kani-driver/Cargo.toml

@@ -11,6 +11,10 @@ homepage = "https://github.com/model-checking/kani"
 repository = "https://github.com/model-checking/kani"
 publish = false
 
+[features]
+unsound_experiments = []
+
+
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
 cargo_metadata = "0.15.0"

kani-driver/src/args.rs

@@ -1,6 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+#[cfg(feature = "unsound_experiments")]
+use crate::unsound_experiments::UnsoundExperimentArgs;
+
 use anyhow::bail;
 use clap::{arg_enum, Error, ErrorKind};
 use std::ffi::OsString;
@@ -95,6 +98,10 @@ pub struct KaniArgs {
     #[structopt(flatten)]
     pub checks: CheckArgs,
 
+    #[cfg(feature = "unsound_experiments")]
+    #[structopt(flatten)]
+    pub unsound_experiments: UnsoundExperimentArgs,
+
     /// Entry point for verification (symbol name).
     /// This is an unstable feature. Consider using --harness instead
     #[structopt(long, hidden = true, requires("enable-unstable"), conflicts_with("dry-run"))]

kani-driver/src/call_single_file.rs

@@ -121,6 +121,9 @@ impl KaniSession {
             flags.push("--ignore-global-asm".into());
         }
 
+        #[cfg(feature = "unsound_experiments")]
+        flags.extend(self.args.unsound_experiments.process_args());
+
         // Stratification point!
         // Above are arguments that should be parsed by kani-compiler
         // Below are arguments that should be parsed by the rustc call

kani-driver/src/main.rs

@@ -26,6 +26,9 @@ mod metadata;
 mod session;
 mod util;
 
+#[cfg(feature = "unsound_experiments")]
+mod unsound_experiments;
+
 fn main() -> Result<()> {
     match determine_invocation_type(Vec::from_iter(std::env::args_os())) {
         InvocationType::CargoKani(args) => cargokani_main(args),
@@ -180,6 +183,9 @@ impl KaniSession {
             );
         }
 
+        #[cfg(feature = "unsound_experiments")]
+        self.args.unsound_experiments.print_warnings();
+
         if !failed_harnesses.is_empty() {
             // Failure exit code without additional error message
             drop(self);