Skip to content

Commit

Permalink
[move-prover] parenthesis the ITE expression when translating to boogie
Browse files Browse the repository at this point in the history
This is motivated by the following expression generated by the spec
simplifier, which causes a type error in Boogie (but no type error in
our AST):

```boogie
(x > 0) && if (true) then (0) else (1) >= 0;
```

In this case, Boogie complains that the then-else branches return
different types which is int (for the then branch) and bool (for the
else branch).

This is caused by the fact that the ITE expression itself is not
enclosed in a parenthesis. The correct encoding should be:

```boogie
(x > 0) && (if (true) then (0) else (1)) >= 0;
```

This commit fixes this issue by wrapping the ITE expression with ().

Closes: #9686
  • Loading branch information
meng-xu-cs authored and bors-libra committed Nov 10, 2021
1 parent fdace17 commit bc9436e
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions language/move-prover/boogie-backend/src/spec_translator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -583,12 +583,15 @@ impl<'env> SpecTranslator<'env> {
}
ExpData::IfElse(node_id, cond, on_true, on_false) => {
self.set_writer_location(*node_id);
emit!(self.writer, "if (");
self.translate_exp(cond);
emit!(self.writer, ") then ");
// The whole ITE is one expression so we wrap it with a parenthesis
emit!(self.writer, "(");
emit!(self.writer, "if ");
self.translate_exp_parenthesised(cond);
emit!(self.writer, " then ");
self.translate_exp_parenthesised(on_true);
emit!(self.writer, " else ");
self.translate_exp_parenthesised(on_false);
emit!(self.writer, ")");
}
ExpData::Invalid(_) => panic!("unexpected error expression"),
}
Expand Down

0 comments on commit bc9436e

Please sign in to comment.