Skip to content

Add Poison to the Kani-GotoC AST #1469

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
giltho merged 13 commits into from
Aug 23, 2022
Merged

Add Poison to the Kani-GotoC AST #1469

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8a386c2
Add a comment field to Location::Loc, set that field for Deinit
giltho Aug 6, 2022
8de20c0
Use a poison expression instead
giltho Aug 7, 2022
369c446
use "poison" instead of "deinit", fix various comments
giltho Aug 8, 2022
beba632
fix copy/paste mistake
giltho Aug 8, 2022
f9ab2bc
Deinit statement instead of Poison expression
giltho Aug 17, 2022
8a4a47e
Merge branch 'main' into comment-deinit
giltho Aug 17, 2022
791d877
fix remaining merge conflicts
giltho Aug 17, 2022
7d33ed2
regression tests not ran yet
giltho Aug 17, 2022
838a807
one test is broken in the regression test suite
giltho Aug 17, 2022
b2dbd39
add various comments
giltho Aug 18, 2022
73ae91c
more comments
giltho Aug 18, 2022
a758c38
Merge branch 'main' into comment-deinit
giltho Aug 23, 2022
7c76620
Merge branch 'main' into comment-deinit
giltho Aug 23, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions cprover_bindings/src/goto_program/expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Copy link
Contributor

@tedinski tedinski Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We definitely want a comment here, especially as "deinit" is not a c notion really, and this is "cprover_bindings"

That's kind of why I thought this should be called "poison" but I don't remember if that was decided against for some reason?

Also, I don't know if this is me reading it weird, but I have the comment note that this is a shorthand/helper (perhaps by example? Like: "Construct a deinit statement from an expression by writing expr.deinit()"

Copy link
Contributor Author

@giltho giltho Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's because @celinval (correct me if I'm wrong) pointed out that "poison" in this form is only intended to model uninitialized memory. So calling it poison is too vague and deinit makes more sense. I tend to agree with that

Stmt::deinit(self, loc)
Copy link
Contributor

@danielsn danielsn Aug 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Doesn't this require that expr be an lvalue?

Copy link
Contributor Author

@giltho giltho Aug 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but I don't know how to check for that.
Assignment checks for type equality but that's it, even though the left-hand side has to be an lvalue
image

Copy link
Contributor

@tedinski tedinski Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be nice to add an "is l-value" check to cprover bindings, but obviously not in this pr...

Copy link
Contributor

@danielsn danielsn Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

https://github.com/model-checking/kani/blob/main/cprover_bindings/src/goto_program/expr.rs#L385
It's called can_take_address_of()

Copy link
Contributor

@danielsn danielsn Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Annoyingly, enabling it on assign causes the stdlib test to crash. Investigating.

}

/// `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)
Expand Down
7 changes: 7 additions & 0 deletions cprover_bindings/src/goto_program/stmt.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}`
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 4 additions & 0 deletions cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/nondet_transformer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
7 changes: 6 additions & 1 deletion cprover_bindings/src/goto_program/symtab_transformer/transformer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down
7 changes: 7 additions & 0 deletions cprover_bindings/src/irep/irep.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Copy link
Contributor

@tedinski tedinski Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cool. doc comment? I know I'm the one who vaguely waved you in the direction of "putting a comment on an irep" but did you dig into exactly how this works? It'd be good to explain I think...

Copy link
Contributor Author

@giltho giltho Aug 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That one is a bit blurry actually. It will add a comment directly to the irep.
As of now, comments are usually in the "location" sub, and here I'm making the decision to put it outside.
Not sure that's the best option, but the location is handled by Expr::to_irep not ExprValue::to_irep, so I can't propagate it up without a big refactoring that would clutter the entire thing for one use case.

I do think we need a more standard way of writing comments like that for alternative back-ends

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);
Expand Down
7 changes: 7 additions & 0 deletions cprover_bindings/src/irep/to_irep.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
8 changes: 5 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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 } => {
Expand Down Expand Up @@ -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.
Expand Down