Add Poison to the Kani-GotoC AST

cprover_bindings/src/goto_program/expr.rs

@@ -111,6 +111,9 @@ pub enum ExprValue {
     },
     /// `__nondet()`
     Nondet,
+    /// Poison comes from the Deinit statement of Rust
+    /// CBMC doesn't model it (as of now)
+    Poison,
     /// `NULL`
     PointerConstant(u64),
     // `op++` etc
@@ -616,6 +619,10 @@ impl Expr {
         expr!(Nondet, typ)
     }
 
+    pub fn poison(typ: Type) -> Self {
+        expr!(Poison, typ)
+    }
+
     /// `e.g. NULL`
     pub fn pointer_constant(c: u64, typ: Type) -> Self {
         assert!(typ.is_pointer());

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

@@ -9,21 +9,30 @@ use std::collections::HashMap;
 pub struct NondetTransformer {
     new_symbol_table: SymbolTable,
     nondet_types: HashMap<String, Type>,
+    poison_types: HashMap<String, Type>,
 }
 
 impl NondetTransformer {
     /// Transform all identifiers in the symbol table to be valid C identifiers;
     /// perform other clean-up operations to make valid C code.
     pub fn transform(original_symbol_table: &SymbolTable) -> SymbolTable {
         let new_symbol_table = SymbolTable::new(original_symbol_table.machine_model().clone());
-        NondetTransformer { new_symbol_table, nondet_types: HashMap::default() }
-            .transform_symbol_table(original_symbol_table)
+        NondetTransformer {
+            new_symbol_table,
+            nondet_types: HashMap::default(),
+            poison_types: HashMap::default(),
+        }
+        .transform_symbol_table(original_symbol_table)
     }
 
     /// Extract `nondet_types` map for final processing.
     pub fn nondet_types_owned(&mut self) -> HashMap<String, Type> {
         std::mem::take(&mut self.nondet_types)
     }
+
+    pub fn poison_types_owned(&mut self) -> HashMap<String, Type> {
+        std::mem::take(&mut self.nondet_types)
+    }
 }
 
 impl Transformer for NondetTransformer {
@@ -65,6 +74,16 @@ impl Transformer for NondetTransformer {
         Expr::symbol_expression(identifier, function_type).call(vec![])
     }
 
+    fn transform_expr_poison(&mut self, typ: &Type) -> Expr {
+        let transformed_type = self.transform_type(typ);
+        let identifier = format!("poison_{}", transformed_type.to_identifier());
+        let function_type = Type::code(vec![], transformed_type);
+
+        self.poison_types.insert(identifier.clone(), function_type.clone());
+
+        Expr::symbol_expression(identifier, function_type).call(vec![])
+    }
+
     /// Don't transform padding fields so that they are ignored by CBMC --dump-c.
     /// If we don't ignore padding fields, we get code that looks like
     /// ```
@@ -104,7 +123,9 @@ impl Transformer for NondetTransformer {
 
     /// Create non_det functions which return default value for type.
     fn postprocess(&mut self) {
-        for (identifier, typ) in self.nondet_types_owned() {
+        for (identifier, typ) in
+            self.nondet_types_owned().into_iter().chain(self.poison_types_owned().into_iter())
+        {
             // Create function body which initializes variable and returns it
             let ret_type = typ.return_type().unwrap();
             assert!(!ret_type.is_empty(), "Cannot generate nondet of type `void`.");

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -267,6 +267,7 @@ pub trait Transformer: Sized {
             ExprValue::IntConstant(value) => self.transform_expr_int_constant(typ, value),
             ExprValue::Member { lhs, field } => self.transform_expr_member(typ, lhs, *field),
             ExprValue::Nondet => self.transform_expr_nondet(typ),
+            ExprValue::Poison => self.transform_expr_poison(typ),
             ExprValue::PointerConstant(value) => self.transform_expr_pointer_constant(typ, value),
             ExprValue::SelfOp { op, e } => self.transform_expr_self_op(typ, op, e),
             ExprValue::StatementExpression { statements } => {
@@ -406,8 +407,13 @@ 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::poison(transformed_typ)
+    }
+
+    /// Transforms a CPROVER nondet call (`__nondet()`)
+    fn transform_expr_poison(&mut self, typ: &Type) -> Expr {
         let transformed_typ = self.transform_type(typ);
         Expr::nondet(transformed_typ)
     }

cprover_bindings/src/goto_program/typ.rs

@@ -1206,6 +1206,10 @@ impl Type {
         Expr::nondet(self.clone())
     }
 
+    pub fn poison(&self) -> Expr {
+        Expr::poison(self.clone())
+    }
+
     /// null pointer of self type
     /// (t)NULL
     pub fn null(&self) -> Expr {

cprover_bindings/src/irep/irep.rs

@@ -44,6 +44,11 @@ impl Irep {
         }
     }
 
+    pub fn with_comment<T: Into<InternedString>>(self, c: T) -> Self {
+        // Using Irep::
+        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

@@ -253,6 +253,11 @@ impl ToIrep for ExprValue {
                 ],
             },
             ExprValue::Nondet => side_effect_irep(IrepId::Nondet, vec![]),
+            ExprValue::Poison => {
+                // For  now, Poison is lowered to Nondet with a comment.
+                // In the future, CBMC might handle poison expressions directly
+                side_effect_irep(IrepId::Nondet, vec![]).with_comment("deinit")
+            }
             ExprValue::PointerConstant(0) => Irep {
                 id: IrepId::Constant,
                 sub: vec![],

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

@@ -659,7 +659,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 } else {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
                         .goto_expr
-                        .assign(dst_type.nondet(), location)
+                        .assign(dst_type.poison(), location)
                 }
             }
             StatementKind::SetDiscriminant { place, variant_index } => {
@@ -763,6 +763,6 @@ impl<'tcx> GotocCtx<'tcx> {
             | StatementKind::Nop
             | StatementKind::Coverage { .. } => Stmt::skip(location),
         }
-        .with_location(self.codegen_span(&stmt.source_info.span))
+        .with_location(location)
     }
 }