Comment and Refactor a few files (rust-lang#1398)

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

@@ -1,9 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This file contains the code that acts as a wrapper to create the new assert and related statements
+//! This module is the central location for handling assertions and assumptions in Kani.
+
+use crate::codegen_cprover_gotoc::utils;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Expr, Location, Stmt};
+use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt};
+use rustc_span::Span;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
 
@@ -39,6 +42,7 @@ impl PropertyClass {
 }
 
 impl<'tcx> GotocCtx<'tcx> {
+    /// Generates a CBMC assertion. Note: Does _NOT_ assume.
     pub fn codegen_assert(
         &self,
         cond: Expr,
@@ -51,6 +55,7 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::assert(cond, property_name, message, loc)
     }
 
+    /// Generates a CBMC assertion, followed by an assumption of the same condition.
     pub fn codegen_assert_assume(
         &self,
         cond: Expr,
@@ -66,6 +71,7 @@ impl<'tcx> GotocCtx<'tcx> {
         )
     }
 
+    /// A shorthand for generating a CBMC assert-false. TODO: This should probably be eliminated!
     pub fn codegen_assert_false(
         &self,
         property_class: PropertyClass,
@@ -76,4 +82,49 @@ impl<'tcx> GotocCtx<'tcx> {
         let property_name = property_class.as_str();
         Stmt::assert_false(property_name, message, loc)
     }
+
+    /// Kani hooks function calls to `panic` and calls this intead.
+    pub fn codegen_panic(&self, span: Option<Span>, fargs: Vec<Expr>) -> Stmt {
+        // CBMC requires that the argument to the assertion must be a string constant.
+        // If there is one in the MIR, use it; otherwise, explain that we can't.
+        assert!(!fargs.is_empty(), "Panic requires a string message");
+        let msg = utils::extract_const_message(&fargs[0]).unwrap_or(String::from(
+            "This is a placeholder message; Kani doesn't support message formatted at runtime",
+        ));
+
+        self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
+    }
+
+    /// Generate code for fatal error which should trigger an assertion failure and abort the
+    /// execution.
+    pub fn codegen_fatal_error(
+        &self,
+        property_class: PropertyClass,
+        msg: &str,
+        span: Option<Span>,
+    ) -> Stmt {
+        let loc = self.codegen_caller_span(&span);
+        Stmt::block(
+            vec![
+                self.codegen_assert_false(property_class, msg, loc),
+                BuiltinFn::Abort.call(vec![], loc).as_stmt(loc),
+            ],
+            loc,
+        )
+    }
+
+    /// Generate code to cover the given condition at the current location
+    pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option<Span>) -> Stmt {
+        let loc = self.codegen_caller_span(&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(!cond).
+        self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
+    }
+
+    /// Generate code to cover the current location
+    pub fn codegen_cover_loc(&self, msg: &str, span: Option<Span>) -> Stmt {
+        self.codegen_cover(Expr::bool_true(), msg, span)
+    }
 }

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

@@ -1,12 +1,16 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This file contains functions related to codegenning MIR blocks into gotoc
-
 use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
 
 impl<'tcx> GotocCtx<'tcx> {
+    /// Generates Goto-C for a basic block.
+    ///
+    /// A MIR basic block consists of 0 or more statements followed by a terminator.
+    ///
+    /// This function does not return a value, but mutates state with
+    /// `self.current_fn_mut().push_onto_block(...)`
     pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
         self.current_fn_mut().set_current_bb(bb);
         let label: String = self.current_fn().find_label(&bb);

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

@@ -26,7 +26,7 @@ impl<'tcx> GotocCtx<'tcx> {
         trace!(operand=?o, "codegen_operand");
         match o {
             Operand::Copy(d) | Operand::Move(d) =>
-            // TODO: move shouldn't be the same as copy
+            // TODO: move is an opportunity to poison/nondet the original memory.
             {
                 let projection =
                     unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(d));