Add option to run CBMC sanity checks + set is_param for function para…

…meters (#1387)

1. Add an unstable hidden option to kani-driver to run sanity checks that are available in CBMC to perform consistency checks on the GOTO model.
2. Fix consistency checks related to missing is_parameter flag. We were not setting this parameter at all. CBMC expects all symbols that are function parameters to have this flag set to true.

cprover_bindings/src/goto_program/symbol.rs

@@ -287,6 +287,11 @@ impl Symbol {
         self
     }
 
+    pub fn with_is_parameter(mut self, v: bool) -> Symbol {
+        self.is_parameter = v;
+        self
+    }
+
     pub fn with_is_static_lifetime(mut self, v: bool) -> Symbol {
         self.is_static_lifetime = v;
         self

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

@@ -41,10 +41,24 @@ impl<'tcx> GotocCtx<'tcx> {
 
 /// Codegen MIR functions into gotoc
 impl<'tcx> GotocCtx<'tcx> {
+    /// Get the number of parameters that the current function expects.
+    fn get_params_size(&self) -> usize {
+        let sig = self.current_fn().sig();
+        let sig =
+            self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap());
+        // we don't call [codegen_function_sig] because we want to get a bit more metainformation.
+        sig.inputs().len()
+    }
+
+    /// Declare variables according to their index.
+    /// - Index 0 represents the return value.
+    /// - Indices [1, N] represent the function parameters where N is the number of parameters.
+    /// - Indices that are greater than N represent local variables.
     fn codegen_declare_variables(&mut self) {
         let mir = self.current_fn().mir();
         let ldecls = mir.local_decls();
-        ldecls.indices().for_each(|lc| {
+        let num_args = self.get_params_size();
+        ldecls.indices().enumerate().for_each(|(idx, lc)| {
             if Some(lc) == mir.spread_arg {
                 // We have already added this local in the function prelude, so
                 // skip adding it again here.
@@ -56,9 +70,11 @@ impl<'tcx> GotocCtx<'tcx> {
             let t = self.monomorphize(ldata.ty);
             let t = self.codegen_ty(t);
             let loc = self.codegen_span(&ldata.source_info.span);
+            // Indices [1, N] represent the function parameters where N is the number of parameters.
             let sym =
                 Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span))
-                    .with_is_hidden(!ldata.is_user_variable());
+                    .with_is_hidden(!ldata.is_user_variable())
+                    .with_is_parameter(idx > 0 && idx <= num_args);
             let sym_e = sym.to_expr();
             self.symbol_table.insert(sym);
 
@@ -206,7 +222,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 let lc = Local::from_usize(arg_i + starting_idx);
                 let (name, base_name) = self.codegen_spread_arg_name(&lc);
                 let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc)
-                    .with_is_hidden(false);
+                    .with_is_hidden(false)
+                    .with_is_parameter(true);
                 // The spread arguments are additional function paramaters that are patched in
                 // They are to the function signature added in the `fn_typ` function.
                 // But they were never added to the symbol table, which we currently do here.

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

@@ -320,7 +320,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let cgt = self.codegen_ty(ty);
         self.ensure(&func_name, |tcx, _| {
             let target_ty = init.typ().clone(); // N
-            let param = tcx.gen_function_local_variable(1, &func_name, target_ty);
+            let param = tcx.gen_function_parameter(1, &func_name, target_ty);
             let var = tcx.gen_function_local_variable(2, &func_name, cgt.clone()).to_expr();
             let body = vec![
                 Stmt::decl(var.clone(), None, Location::none()),
@@ -607,7 +607,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let pretty_name = format!("init_niche<{}>", self.ty_pretty_name(ty));
         self.ensure(&fname, |tcx, _| {
             let target_ty = init.typ().clone(); // N
-            let param = tcx.gen_function_local_variable(1, &fname, target_ty.clone());
+            let param = tcx.gen_function_parameter(1, &fname, target_ty.clone());
             let var = tcx.gen_function_local_variable(2, &fname, cgt.clone()).to_expr();
             let body = vec![
                 Stmt::decl(var.clone(), None, Location::none()),

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

@@ -214,7 +214,7 @@ impl<'tcx> GotocCtx<'tcx> {
         self.ensure(&func_name, |tcx, _| {
             let paramt = tcx.codegen_ty(tcx.operand_ty(op));
             let res_t = tcx.codegen_ty(res_ty);
-            let inp = tcx.gen_function_local_variable(1, &func_name, paramt);
+            let inp = tcx.gen_function_parameter(1, &func_name, paramt);
             let res = tcx.gen_function_local_variable(2, &func_name, res_t.clone()).to_expr();
             let idx = tcx.gen_function_local_variable(3, &func_name, Type::size_t()).to_expr();
             let mut body = vec![
@@ -866,14 +866,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     .as_stmt(Location::none());
 
                 // Declare symbol for the single, self parameter
-                let param_name = format!("{}::1::var{:?}", drop_sym_name, 0);
-                let param_sym = Symbol::variable(
-                    param_name.clone(),
-                    param_name,
-                    ctx.codegen_ty(trait_ty).to_pointer(),
-                    Location::none(),
-                );
-                ctx.symbol_table.insert(param_sym.clone());
+                let param_typ = ctx.codegen_ty(trait_ty).to_pointer();
+                let param_sym = ctx.gen_function_parameter(0, &drop_sym_name, param_typ);
 
                 // Build and insert the function itself
                 Symbol::function(

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

@@ -124,7 +124,12 @@ impl<'tcx> GotocCtx<'tcx> {
 
     // Generate a Symbol Expression representing a function variable from the MIR
     pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, Location::none())
+        self.gen_stack_variable(c, fname, "var", t, Location::none(), false)
+    }
+
+    // Generate a Symbol Expression representing a function parameter from the MIR
+    pub fn gen_function_parameter(&mut self, c: u64, fname: &str, t: Type) -> Symbol {
+        self.gen_stack_variable(c, fname, "var", t, Location::none(), true)
     }
 
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
@@ -136,10 +141,11 @@ impl<'tcx> GotocCtx<'tcx> {
         prefix: &str,
         t: Type,
         loc: Location,
+        is_param: bool,
     ) -> Symbol {
         let base_name = format!("{}_{}", prefix, c);
         let name = format!("{}::1::{}", fname, base_name);
-        let symbol = Symbol::variable(name, base_name, t, loc);
+        let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param);
         self.symbol_table.insert(symbol.clone());
         symbol
     }
@@ -153,7 +159,8 @@ impl<'tcx> GotocCtx<'tcx> {
         loc: Location,
     ) -> (Expr, Stmt) {
         let c = self.current_fn_mut().get_and_incr_counter();
-        let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr();
+        let var =
+            self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr();
         let decl = Stmt::decl(var.clone(), value, loc);
         (var, decl)
     }

kani-driver/src/args.rs

@@ -148,6 +148,10 @@ pub struct KaniArgs {
     /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples
     #[structopt(long, hidden_short_help(true), requires("enable-unstable"))]
     pub ignore_global_asm: bool,
+
+    /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct.
+    #[structopt(long, hidden_short_help(true), requires("enable-unstable"))]
+    pub run_sanity_checks: bool,
     /*
     The below is a "TODO list" of things not yet implemented from the kani_flags.py script.
 

kani-driver/src/call_cbmc.rs

@@ -95,6 +95,11 @@ impl KaniSession {
             args.push(unwind_value.to_string().into());
         }
 
+        if self.args.run_sanity_checks {
+            args.push("--validate-goto-model".into());
+            args.push("--validate-ssa-equation".into());
+        }
+
         args.push("--slice-formula".into());
 
         args.extend(self.args.cbmc_args.iter().cloned());

kani-driver/src/call_goto_instrument.rs

@@ -24,6 +24,12 @@ impl KaniSession {
         // We actually start by calling goto-cc to start the specialization:
         self.specialize_to_proof_harness(input, output, function)?;
 
+        // Run sanity checks in the model generated by kani-compiler before any goto-instrument
+        // transformation.
+        if self.args.run_sanity_checks {
+            self.goto_sanity_check(output)?;
+        }
+
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
             self.undefined_functions(output)?;
@@ -130,6 +136,16 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    fn goto_sanity_check(&self, file: &Path) -> Result<()> {
+        let args: Vec<OsString> = vec![
+            "--validate-goto-model".into(),
+            file.to_owned().into_os_string(), // input
+            file.to_owned().into_os_string(), // output
+        ];
+
+        self.call_goto_instrument(args)
+    }
+
     /// Generate a .c file from a goto binary (i.e. --gen-c)
     pub fn gen_c(&self, file: &Path, output_file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![