Skip to content
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

Remove the usage of infix, overloaded syntax in why3 output #915

Closed
wants to merge 3 commits into from
Closed

Remove the usage of infix, overloaded syntax in why3 output #915

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
53a5177
wip
xldenis Jan 3, 2024
efe3cc8
Update tests
xldenis Jan 3, 2024
62c7ba3
Fix all tests except rbt and knights toru
xldenis Jan 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
8 changes: 4 additions & 4 deletions creusot-contracts/src/logic/ord.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,31 +149,31 @@ macro_rules! ord_logic_impl {
#[trusted]
#[open]
#[ghost]
#[creusot::builtins = "int.Int.(<=)"]
#[creusot::builtins = "prelude.Int.le"]
fn le_log(self, _: Self) -> bool {
true
}

#[trusted]
#[open]
#[ghost]
#[creusot::builtins = "int.Int.(<)"]
#[creusot::builtins = "prelude.Int.lt"]
fn lt_log(self, _: Self) -> bool {
true
}

#[trusted]
#[open]
#[ghost]
#[creusot::builtins = "int.Int.(>=)"]
#[creusot::builtins = "prelude.Int.ge"]
fn ge_log(self, _: Self) -> bool {
true
}

#[trusted]
#[open]
#[ghost]
#[creusot::builtins = "int.Int.(>)"]
#[creusot::builtins = "prelude.Int.gt"]
fn gt_log(self, _: Self) -> bool {
true
}
Expand Down
4 changes: 2 additions & 2 deletions creusot/src/backend/clone_map.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ use crate::{

// Prelude modules
#[allow(dead_code)]
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum PreludeModule {
Float32,
Float64,
Expand Down Expand Up @@ -58,7 +58,7 @@ pub enum PreludeModule {
}

impl PreludeModule {
fn qname(&self) -> QName {
pub(crate) fn qname(&self) -> QName {
match self {
PreludeModule::Float32 => QName::from_string("prelude.Float32").unwrap(),
PreludeModule::Float64 => QName::from_string("prelude.Float64").unwrap(),
Expand Down
120 changes: 94 additions & 26 deletions creusot/src/backend/program.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,25 +12,21 @@ use crate::{
},
ctx::{BodyId, CloneMap, TranslationCtx},
translation::{
binop_to_binop,
fmir::{
self, Block, Branches, Expr, ExprKind, LocalDecls, Place, RValue, Statement, Terminator,
},
fmir::{self, *},
function::{closure_contract, promoted, ClosureContract},
unop_to_unop,
},
util::{self, module_name, ItemType},
};
use rustc_hir::{def::DefKind, def_id::DefId, Unsafety};
use rustc_middle::{
mir::{BasicBlock, BinOp},
ty::TyKind,
mir::{self, BasicBlock, BinOp},
ty::{Ty, TyKind},
};
use rustc_span::DUMMY_SP;
use rustc_type_ir::{IntTy, UintTy};
use rustc_type_ir::{FloatTy, IntTy, UintTy};
use why3::{
declaration::{self, Attribute, CfgFunction, Decl, LetDecl, LetKind, Module, Predicate, Use},
exp::{Constant, Exp, Pattern},
exp::{Constant, Exp, Pattern, UnOp},
mlcfg,
mlcfg::BlockId,
Ident, QName,
Expand Down Expand Up @@ -336,15 +332,12 @@ impl<'tcx> Expr<'tcx> {
// Hack
translate_ty(ctx, names, DUMMY_SP, ty);

Exp::BinaryOp(
binop_to_binop(ctx, ty, op),
Box::new(l.to_why(ctx, names, locals)),
Box::new(r.to_why(ctx, names, locals)),
)
}
ExprKind::UnaryOp(op, ty, arg) => {
Exp::UnaryOp(unop_to_unop(ty, op), Box::new(arg.to_why(ctx, names, locals)))
let l = l.to_why(ctx, names, locals);
let r = r.to_why(ctx, names, locals);

binop_to_binop(ty, op, l, r)
}
ExprKind::UnaryOp(op, ty, arg) => unop_to_unop(ty, op, arg.to_why(ctx, names, locals)),
ExprKind::Constructor(id, subst, args) => {
let args = args.into_iter().map(|a| a.to_why(ctx, names, locals)).collect();

Expand Down Expand Up @@ -509,7 +502,7 @@ impl<'tcx> Terminator<'tcx> {
};
}
Terminator::Switch(_, brs) => match brs {
Branches::Int(brs, def) => {
Branches::Int(_, brs, def) => {
if *def == from {
*def = to
};
Expand All @@ -519,7 +512,7 @@ impl<'tcx> Terminator<'tcx> {
}
}
}
Branches::Uint(brs, def) => {
Branches::Uint(_, brs, def) => {
if *def == from {
*def = to
};
Expand Down Expand Up @@ -580,23 +573,32 @@ impl<'tcx> Branches<'tcx> {
discr: Exp,
) -> mlcfg::Terminator {
use why3::mlcfg::Terminator::*;

match self {
Branches::Int(brs, def) => {
Branches::Int(ty, brs, def) => {
brs.into_iter().rfold(Goto(BlockId(def.into())), |acc, (val, bb)| {
Switch(
discr.clone().eq(Exp::Const(why3::exp::Constant::Int(val, None))),
binop_to_binop(
ty,
BinOp::Eq,
discr.clone(),
Exp::Const(Constant::Int(val, None)),
),
vec![
(Pattern::mk_true(), Goto(BlockId(bb.into()))),
(Pattern::mk_false(), acc),
],
)
})
}
Branches::Uint(brs, def) => {
Branches::Uint(ty, brs, def) => {
brs.into_iter().rfold(Goto(BlockId(def.into())), |acc, (val, bb)| {
Switch(
discr.clone().eq(Exp::Const(why3::exp::Constant::Uint(val, None))),
binop_to_binop(
ty,
BinOp::Eq,
discr.clone(),
Exp::Const(Constant::Uint(val, None)),
),
vec![
(Pattern::mk_true(), Goto(BlockId(bb.into()))),
(Pattern::mk_false(), acc),
Expand Down Expand Up @@ -731,7 +733,73 @@ impl<'tcx> Statement<'tcx> {
}
}

fn int_to_prelude(ity: IntTy) -> PreludeModule {
pub(crate) fn binop_to_binop(ty: Ty, op: mir::BinOp, left: Exp, right: Exp) -> Exp {
let prelude: PreludeModule = match ty.kind() {
TyKind::Int(ity) => int_to_prelude(*ity),
TyKind::Uint(uty) => uint_to_prelude(*uty),
TyKind::Float(FloatTy::F32) => PreludeModule::Float32,
TyKind::Float(FloatTy::F64) => PreludeModule::Float64,
_ => unreachable!("non-primitive type for binary operation {ty:?}"),
};

let mut module = prelude.qname();

match op {
BinOp::Add => module.push_ident("add"),
BinOp::AddUnchecked => module.push_ident("add"),
BinOp::Sub => module.push_ident("sub"),
BinOp::SubUnchecked => module.push_ident("sub"),
BinOp::Mul => module.push_ident("mul"),
BinOp::MulUnchecked => module.push_ident("mul"),
BinOp::Div => module.push_ident("div"),
BinOp::Rem => module.push_ident("rem"),
BinOp::BitXor => module.push_ident("bw_xor"),
BinOp::BitAnd => module.push_ident("bw_and"),
BinOp::BitOr => module.push_ident("bw_or"),
BinOp::Shl => module.push_ident("shl"),
BinOp::ShlUnchecked => module.push_ident("shl"),
BinOp::Shr => module.push_ident("shr"),
BinOp::ShrUnchecked => module.push_ident("shr"),
BinOp::Eq => module.push_ident("eq"),
BinOp::Lt => module.push_ident("lt"),
BinOp::Le => module.push_ident("le"),
BinOp::Ne => module.push_ident("ne"),
BinOp::Ge => module.push_ident("ge"),
BinOp::Gt => module.push_ident("gt"),
BinOp::Offset => unimplemented!("pointer offsets are unsupported"),
};

module = module.without_search_path();
Exp::impure_qvar(module).app(vec![left, right])
}

pub(crate) fn unop_to_unop(ty: Ty, op: rustc_middle::mir::UnOp, e: Exp) -> Exp {
let prelude: PreludeModule = match ty.kind() {
TyKind::Int(ity) => int_to_prelude(*ity),
TyKind::Uint(uty) => uint_to_prelude(*uty),
TyKind::Float(FloatTy::F32) => PreludeModule::Float32,
TyKind::Float(FloatTy::F64) => PreludeModule::Float64,
TyKind::Bool => {
assert_eq!(op, mir::UnOp::Not);
PreludeModule::Bool
}
_ => unreachable!("non-primitive type for unary operation"),
};

let mut module = prelude.qname();

match op {
mir::UnOp::Not => Exp::UnaryOp(UnOp::Not, Box::new(e)),
mir::UnOp::Neg => {
module.push_ident("neg");

module = module.without_search_path();
Exp::impure_qvar(module).app_to(e)
}
}
}

pub(crate) fn int_to_prelude(ity: IntTy) -> PreludeModule {
match ity {
IntTy::Isize => PreludeModule::Isize,
IntTy::I8 => PreludeModule::Int8,
Expand All @@ -742,7 +810,7 @@ fn int_to_prelude(ity: IntTy) -> PreludeModule {
}
}

fn uint_to_prelude(ity: UintTy) -> PreludeModule {
pub(crate) fn uint_to_prelude(ity: UintTy) -> PreludeModule {
match ity {
UintTy::Usize => PreludeModule::Usize,
UintTy::U8 => PreludeModule::UInt8,
Expand Down
98 changes: 77 additions & 21 deletions creusot/src/backend/term.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ use crate::{
util::get_builtin,
};
use rustc_middle::ty::{EarlyBinder, Ty, TyKind};
use rustc_span::Symbol;
use rustc_type_ir::FloatTy;
use why3::{
exp::{BinOp, Binder, Constant, Exp, Pattern as Pat, Purity},
ty::Type,
Expand Down Expand Up @@ -62,6 +64,7 @@ impl<'tcx> Lower<'_, 'tcx> {
}
TermKind::Var(v) => Exp::pure_var(util::ident_of(v)),
TermKind::Binary { op, box lhs, box rhs } => {
let ty = lhs.ty;
let lhs = self.lower_term(lhs);
let rhs = self.lower_term(rhs);

Expand All @@ -71,8 +74,6 @@ impl<'tcx> Lower<'_, 'tcx> {
}

match (op, self.pure) {
(Div, _) => Exp::pure_var("div".into()).app(vec![lhs, rhs]),
(Rem, _) => Exp::pure_var("mod".into()).app(vec![lhs, rhs]),
(Eq | Ne | Lt | Le | Gt | Ge, Purity::Program) => {
let (a, lhs) = if lhs.is_pure() {
(lhs, None)
Expand All @@ -86,9 +87,11 @@ impl<'tcx> Lower<'_, 'tcx> {
(Exp::Var("b".into(), self.pure), Some(rhs))
};

let op = binop_to_binop(op, Purity::Logic);
let inner =
binop_to_binop(self.ctx.tcx, self.names, op, ty, Purity::Logic, a, b);

let mut inner =
Exp::Pure(Box::new(Exp::BinaryOp(op, Box::new(a), Box::new(b))));
Exp::Pure(Box::new(inner));

if let Some(lhs) = lhs {
inner = Exp::Let {
Expand All @@ -108,7 +111,7 @@ impl<'tcx> Lower<'_, 'tcx> {

inner
}
_ => Exp::BinaryOp(binop_to_binop(op, self.pure), Box::new(lhs), Box::new(rhs)),
_ => binop_to_binop(self.ctx.tcx, self.names, op, ty, self.pure, lhs, rhs),
}
}
TermKind::Unary { op, box arg } => {
Expand Down Expand Up @@ -338,7 +341,11 @@ impl<'tcx> Lower<'_, 'tcx> {
use rustc_hir::def_id::DefId;
use rustc_middle::ty::{subst::SubstsRef, TyCtxt};

use super::{dependency::Dependency, Why3Generator};
use super::{
dependency::Dependency,
program::{int_to_prelude, uint_to_prelude},
Why3Generator,
};

pub(crate) fn lower_literal<'tcx>(
ctx: &mut TranslationCtx<'tcx>,
Expand Down Expand Up @@ -377,23 +384,72 @@ pub(crate) fn lower_literal<'tcx>(
}
}

fn binop_to_binop(op: pearlite::BinOp, purity: Purity) -> why3::exp::BinOp {
fn binop_module<'tcx>(tcx: TyCtxt<'tcx>, ty: Ty<'tcx>, op: pearlite::BinOp) -> PreludeModule {
use pearlite::BinOp;
match ty.kind() {
TyKind::Int(ity) => int_to_prelude(*ity),
TyKind::Uint(uty) => uint_to_prelude(*uty),
TyKind::Float(FloatTy::F32) => PreludeModule::Float32,
TyKind::Float(FloatTy::F64) => PreludeModule::Float64,
TyKind::Adt(def, _) => {
if Some(def.did()) == tcx.get_diagnostic_item(Symbol::intern("creusot_int")) {
PreludeModule::Int
} else {
PreludeModule::Bool
}
}
TyKind::Bool => PreludeModule::Bool,
_ => {
assert!(matches!(op, BinOp::Eq | BinOp::Ne));
PreludeModule::Bool
}
}
}

fn binop_to_binop<'tcx>(
tcx: TyCtxt<'tcx>,
names: &mut CloneMap<'tcx>,
op: pearlite::BinOp,
ty: Ty<'tcx>,
purity: Purity,
left: Exp,
right: Exp,
) -> Exp {
let prelude = binop_module(tcx, ty, op);
names.import_prelude_module(prelude);

let mut module = prelude.qname();
match (op, purity) {
(pearlite::BinOp::Add, _) => BinOp::Add,
(pearlite::BinOp::Sub, _) => BinOp::Sub,
(pearlite::BinOp::Mul, _) => BinOp::Mul,
(pearlite::BinOp::Lt, _) => BinOp::Lt,
(pearlite::BinOp::Le, _) => BinOp::Le,
(pearlite::BinOp::Gt, _) => BinOp::Gt,
(pearlite::BinOp::Ge, _) => BinOp::Ge,
(pearlite::BinOp::Eq, Purity::Logic) => BinOp::Eq,
(pearlite::BinOp::Ne, Purity::Logic) => BinOp::Ne,
(pearlite::BinOp::And, Purity::Logic) => BinOp::LogAnd,
(pearlite::BinOp::And, Purity::Program) => BinOp::LazyAnd,
(pearlite::BinOp::Or, Purity::Logic) => BinOp::LogOr,
(pearlite::BinOp::Or, Purity::Program) => BinOp::LazyOr,
_ => unreachable!(),
(pearlite::BinOp::Add, _) => module.push_ident("add"),
(pearlite::BinOp::Sub, _) => module.push_ident("sub"),
(pearlite::BinOp::Mul, _) => module.push_ident("mul"),
(pearlite::BinOp::Div, _) => module.push_ident("div"),
(pearlite::BinOp::Rem, _) => module.push_ident("rem"),
(pearlite::BinOp::Lt, _) => module.push_ident("lt"),
(pearlite::BinOp::Le, _) => module.push_ident("le"),
(pearlite::BinOp::Gt, _) => module.push_ident("gt"),
(pearlite::BinOp::Ge, _) => module.push_ident("ge"),
(pearlite::BinOp::Eq, Purity::Program) => module.push_ident("eq"),
(pearlite::BinOp::Ne, Purity::Program) => module.push_ident("ne"),
(pearlite::BinOp::Eq, Purity::Logic) => return left.eq(right),
(pearlite::BinOp::Ne, Purity::Logic) => return left.neq(right),
(pearlite::BinOp::And, Purity::Logic) => {
return Exp::BinaryOp(BinOp::LogAnd, Box::new(left), Box::new(right))
}
(pearlite::BinOp::And, Purity::Program) => {
return Exp::BinaryOp(BinOp::LazyAnd, Box::new(left), Box::new(right))
}
(pearlite::BinOp::Or, Purity::Logic) => {
return Exp::BinaryOp(BinOp::LogOr, Box::new(left), Box::new(right))
}
(pearlite::BinOp::Or, Purity::Program) => {
return Exp::BinaryOp(BinOp::LazyOr, Box::new(left), Box::new(right))
}
_ => unreachable!("{op:?} {purity:?}"),
}

module = module.without_search_path();
Exp::pure_qvar(module).app(vec![left, right])
}

pub(super) fn mk_binders(func: Exp, args: Vec<Exp>) -> Exp {
Expand Down
Loading
Loading