Skip to content

Commit

Permalink
Rewrite QP desugaring, tweak SwichInt terminator encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
@vfukala
vfukala committed Jul 9, 2023
1 parent 281e5b7 commit 8eeaf4c
Show file tree
Hide file tree
Showing 2 changed files with 99 additions and 70 deletions.
111 changes: 61 additions & 50 deletions prusti-common/src/vir/optimizations/functions/simplifier.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -207,11 +207,12 @@ impl ExprSimplifier {
right: Box::new(Self::apply_rules(op2)),
position: pos,
}),
// added to satisfy Viper because we don't do desugaring of quantified permissions
// elsewhere; consider calling the Viper functions that does that instead
// the following transformations of foralls are necessary because the verifier backends rely on them (they are normally done by Silver when traslating the parse AST into real Viper AST);
// alternatively, consider calling the Silver functions that do this
// transform (forall A ==> B ==> C) into (forall (A && B) ==> C)
ast::Expr::ForAll(ast::ForAll {
variables: vars,
triggers: trigs,
variables,
triggers,
body:
box ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
Expand All @@ -223,29 +224,46 @@ impl ExprSimplifier {
right: box ex,
..
}),
position: pos0,
position: pos_body,
}),
position: pos_quant,
}) if !ex.is_pure() => Self::apply_rules(ast::Expr::ForAll(ast::ForAll {
variables: vars,
triggers: trigs,
body: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
left: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::And,
left: Box::new(c0),
right: Box::new(c1),
position: pos0,
})),
right: Box::new(ex),
position: pos0,
})),
position: pos_quant,
})),
// same comment as above
}) if !ex.is_pure() => Self::apply_rules(
ast::Expr::forall(
variables,
triggers,
ast::Expr::implies(ast::Expr::and(c0, c1).set_pos(pos_body), ex)
.set_pos(pos_body),
)
.set_pos(pos_quant),
),
// transform (forall A) into (forall true ==> A) if A is not an implication
ast::Expr::ForAll(ast::ForAll {
variables,
triggers,
body: box body,
position,
}) if !body.is_pure()
&& !matches!(
body,
ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
..
})
) =>
{
Self::apply_rules(
ast::Expr::forall(
variables,
triggers,
ast::Expr::implies(true.into(), body.clone()).set_pos(body.pos()),
)
.set_pos(position),
)
}
// transform (forall A ==> (B && C)) into ((forall A ==> B) && (forall A ==> C))
ast::Expr::ForAll(ast::ForAll {
variables: vars,
triggers: trigs,
variables,
triggers,
body:
box ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
Expand All @@ -260,32 +278,25 @@ impl ExprSimplifier {
position: pos_body,
}),
position: pos_quant,
}) if !part0.is_pure() || !part1.is_pure() => ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::And,
left: Box::new(Self::apply_rules(ast::Expr::ForAll(ast::ForAll {
variables: vars.clone(),
triggers: trigs.clone(),
body: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
left: Box::new(cond.clone()),
right: Box::new(part0),
position: pos_body,
})),
position: pos_quant,
}))),
right: Box::new(Self::apply_rules(ast::Expr::ForAll(ast::ForAll {
variables: vars,
triggers: trigs,
body: Box::new(ast::Expr::BinOp(ast::BinOp {
op_kind: ast::BinaryOpKind::Implies,
left: Box::new(cond),
right: Box::new(part1),
position: pos_body,
})),
position: pos_quant,
}))),
position: pos_quant,
}),
}) if !part0.is_pure() || !part1.is_pure() => ast::Expr::and(
Self::apply_rules(
ast::Expr::forall(
variables.clone(),
triggers.clone(),
ast::Expr::implies(cond.clone(), part0).set_pos(pos_body),
)
.set_pos(pos_quant),
),
Self::apply_rules(
ast::Expr::forall(
variables,
triggers,
ast::Expr::implies(cond, part1).set_pos(pos_body),
)
.set_pos(pos_quant),
),
)
.set_pos(pos_quant),
r => r,
}
}
Expand Down
58 changes: 38 additions & 20 deletions prusti-viper/src/encoder/mir/pure/interpreter/interpreter_poly.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -334,29 +334,47 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
.mir_encoder
.encode_operand_expr(discr)
.with_span(span)?;
for (value, target) in targets.iter() {
// Convert int to bool, if required
let viper_guard = match switch_ty.kind() {
ty::TyKind::Bool => {
if value == 0 {
// If discr is 0 (false)
vir::Expr::not(discr_val.clone())
} else {
// If discr is not 0 (true)
discr_val.clone()
let default_target = if matches!(switch_ty.kind(), ty::TyKind::Bool)
&& targets.iter().count() == 1
&& targets.iter().next().unwrap().0 == 0
{
// This a special case for a more natural encoding:
// Given that A is bool variable in Rust,
// if A { ...BB1... } else { ...BB2... }
// would have
// discr = A
// targets = BB2 for value 0, BB1 otherwise
// So using the general algorithm (see the else branch below), this would
// get encoded as (!A ? ...BB2... : ...BB1...).
// However (e.g. for error reporting), it is beneficial to produce the more natural
// encoding (A ? ...BB1... : ...BB2...), which is what we do on the two lines below.
cfg_targets.push((discr_val, targets.otherwise()));
targets.iter().next().unwrap().1
} else {
for (value, target) in targets.iter() {
// Convert int to bool, if required
let viper_guard = match switch_ty.kind() {
ty::TyKind::Bool => {
if value == 0 {
// If discr is 0 (false)
vir::Expr::not(discr_val.clone())
} else {
// If discr is not 0 (true)
discr_val.clone()
}
}
}

ty::TyKind::Int(_) | ty::TyKind::Uint(_) => vir::Expr::eq_cmp(
discr_val.clone(),
self.encoder.encode_int_cast(value, switch_ty),
),
ty::TyKind::Int(_) | ty::TyKind::Uint(_) => vir::Expr::eq_cmp(
discr_val.clone(),
self.encoder.encode_int_cast(value, switch_ty),
),

ref x => unreachable!("{:?}", x),
};
cfg_targets.push((viper_guard, target))
}
let default_target = targets.otherwise();
ref x => unreachable!("{:?}", x),
};
cfg_targets.push((viper_guard, target))
}
targets.otherwise()
};

let default_target_terminator = self.mir.basic_blocks[default_target]
.terminator
Expand Down

0 comments on commit 8eeaf4c

Please sign in to comment.