Add Poison to the Kani-GotoC AST (#1469)

* Add a comment field to Location::Loc, set that field for Deinit

* Use a poison expression instead

* use "poison" instead of "deinit", fix various comments

* fix copy/paste mistake

* Deinit statement instead of Poison expression

* fix remaining merge conflicts

* regression tests not ran yet

* one test is broken in the regression test suite

* add various comments

* more comments

Author: giltho

cprover_bindings/src/goto_program/expr.rs

@@ -1493,6 +1493,11 @@ impl Expr {
         Stmt::assign(self, rhs, loc)
     }
 
+    /// Shorthand to build a `Deinit(self)` statement. See `StmtBody::Deinit`
+    pub fn deinit(self, loc: Location) -> Stmt {
+        Stmt::deinit(self, loc)
+    }
+
     /// `if (self) { t } else { e }` or `if (self) { t }`
     pub fn if_then_else(self, t: Stmt, e: Option<Stmt>, loc: Location) -> Stmt {
         Stmt::if_then_else(self, t, e, loc)

cprover_bindings/src/goto_program/stmt.rs

@@ -62,6 +62,8 @@ pub enum StmtBody {
         lhs: Expr, // SymbolExpr
         value: Option<Expr>,
     },
+    /// Marks the target place as uninitialized.
+    Deinit(Expr),
     /// `e;`
     Expression(Expr),
     // `for (init; cond; update) {body}`
@@ -237,6 +239,11 @@ impl Stmt {
         stmt!(Decl { lhs, value }, loc)
     }
 
+    /// `Deinit(place)`, see `StmtBody::Deinit`.
+    pub fn deinit(place: Expr, loc: Location) -> Self {
+        stmt!(Deinit(place), loc)
+    }
+
     /// `e;`
     pub fn code_expression(e: Expr, loc: Location) -> Self {
         stmt!(Expression(e), loc)

cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs

@@ -11,6 +11,10 @@ pub struct NondetTransformer {
     nondet_types: HashMap<String, Type>,
 }
 
+// Note: this replaces every occurence of a Nondet expression by an equivalent function call.
+// Since the introduction of StmtBody::Deinit, some Nondet expressions only appear
+// at Irep generating time. Such expressions will not be substituted by this transformer.
+
 impl NondetTransformer {
     /// Transform all identifiers in the symbol table to be valid C identifiers;
     /// perform other clean-up operations to make valid C code.

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -412,7 +412,6 @@ pub trait Transformer: Sized {
         transformed_lhs.member(field, self.symbol_table())
     }
 
-    /// Transforms a CPROVER nondet call (`__nondet()`)
     fn transform_expr_nondet(&mut self, typ: &Type) -> Expr {
         let transformed_typ = self.transform_type(typ);
         Expr::nondet(transformed_typ)
@@ -520,6 +519,7 @@ pub trait Transformer: Sized {
             StmtBody::Break => self.transform_stmt_break(),
             StmtBody::Continue => self.transform_stmt_continue(),
             StmtBody::Decl { lhs, value } => self.transform_stmt_decl(lhs, value),
+            StmtBody::Deinit(place) => self.transform_stmt_deinit(place),
             StmtBody::Expression(expr) => self.transform_stmt_expression(expr),
             StmtBody::For { init, cond, update, body } => {
                 self.transform_stmt_for(init, cond, update, body)
@@ -598,6 +598,11 @@ pub trait Transformer: Sized {
         Stmt::decl(transformed_lhs, transformed_value, Location::none())
     }
 
+    fn transform_stmt_deinit(&mut self, place: &Expr) -> Stmt {
+        let transformed_place = self.transform_expr(place);
+        Stmt::deinit(transformed_place, Location::none())
+    }
+
     /// Transform an expression stmt (`e;`)
     fn transform_stmt_expression(&mut self, expr: &Expr) -> Stmt {
         let transformed_expr = self.transform_expr(expr);

cprover_bindings/src/irep/irep.rs

@@ -44,6 +44,13 @@ impl Irep {
         }
     }
 
+    /// Adds a `comment` sub to the irep.
+    /// Note that there might be comments both on the irep itself and
+    /// inside the location sub of the irep.
+    pub fn with_comment<T: Into<InternedString>>(self, c: T) -> Self {
+        self.with_named_sub(IrepId::Comment, Irep::just_string_id(c))
+    }
+
     pub fn with_named_sub(mut self, key: IrepId, value: Irep) -> Self {
         if !value.is_nil() {
             self.named_sub.insert(key, value);

cprover_bindings/src/irep/to_irep.rs

@@ -430,6 +430,13 @@ impl ToIrep for StmtBody {
                     code_irep(IrepId::Decl, vec![lhs.to_irep(mm)])
                 }
             }
+            StmtBody::Deinit(place) => {
+                // CBMC doesn't yet have a notion of poison (https://github.com/diffblue/cbmc/issues/7014)
+                // So we translate identically to `nondet` here, but add a comment noting we wish it were poison
+                // potentially for other backends to pick up and treat specially.
+                code_irep(IrepId::Assign, vec![place.to_irep(mm), place.typ().nondet().to_irep(mm)])
+                    .with_comment("deinit")
+            }
             StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]),
             StmtBody::For { init, cond, update, body } => code_irep(
                 IrepId::For,

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

@@ -58,7 +58,9 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             StatementKind::Deinit(place) => {
                 // From rustc doc: "This writes `uninit` bytes to the entire place."
-                // Thus, we assign nondet() value 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);
@@ -68,7 +70,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 } else {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
                         .goto_expr
-                        .assign(dst_type.nondet(), location)
+                        .deinit(location)
                 }
             }
             StatementKind::SetDiscriminant { place, variant_index } => {
@@ -157,7 +159,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | StatementKind::Nop
             | StatementKind::Coverage { .. } => Stmt::skip(location),
         }
-        .with_location(self.codegen_span(&stmt.source_info.span))
+        .with_location(location)
     }
 
     /// Generate Goto-c for MIR [Terminator] statements.