Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@xldenis
xldenis committed Jan 3, 2024
1 parent 0a53c27 commit 26e2da1
Show file tree
Hide file tree
Showing 14 changed files with 658 additions and 189 deletions.
8 changes: 4 additions & 4 deletions creusot-contracts/src/logic/ord.rs
View file
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
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
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
91 changes: 71 additions & 20 deletions creusot/src/backend/term.rs
View file
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,8 @@ impl<'tcx> Lower<'_, 'tcx> {
(Exp::Var("b".into(), self.pure), Some(rhs))
};

let op = binop_to_binop(op, Purity::Logic);
let mut inner =
Exp::Pure(Box::new(Exp::BinaryOp(op, Box::new(a), Box::new(b))));
binop_to_binop(self.ctx.tcx, self.names, op, ty, Purity::Logic, a, b);

if let Some(lhs) = lhs {
inner = Exp::Let {
Expand All @@ -108,7 +108,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 +338,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 +381,70 @@ 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,
(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::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!(),
}

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

0 comments on commit 26e2da1

Please sign in to comment.