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

Added MIR optimization to avoid unnecessary re-borrows #907

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Added MIR optimization to avoid unnecessary re-borrows #907

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
3 changes: 2 additions & 1 deletion creusot/src/callbacks.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use rustc_middle::ty::TyCtxt;

use std::{cell::RefCell, collections::HashMap, thread_local};

use crate::{cleanup_spec_closures::*, options::Options};
use crate::{cleanup_spec_closures::*, options::Options, remove_mir_reborrows::*};

pub struct ToWhy {
opts: Options,
Expand All @@ -32,6 +32,7 @@ impl Callbacks for ToWhy {
let mir = (rustc_interface::DEFAULT_QUERY_PROVIDERS.mir_built)(tcx, def_id);
let mut mir = mir.steal();
cleanup_spec_closures(tcx, def_id.to_def_id(), &mut mir);
remove_mir_reborrows(tcx, &mut mir);
tcx.alloc_steal_mir(mir)
};

Expand Down
1 change: 1 addition & 0 deletions creusot/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,5 +48,6 @@ use translation::*;
mod error;
pub(crate) mod lints;
pub(crate) mod metadata;
mod remove_mir_reborrows;
mod translated_item;
mod validate;
59 changes: 59 additions & 0 deletions creusot/src/remove_mir_reborrows.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
use rustc_ast::Mutability;
use rustc_middle::{
mir::{
Body, BorrowKind, Location, Operand, Place, PlaceElem, Rvalue, Statement, StatementKind,
},
ty::{List, TyCtxt},
};
use rustc_mir_dataflow::{
impls::MaybeLiveLocals, Analysis, AnalysisDomain, Results, ResultsVisitor,
};

struct Visitor<'mir, 'tcx> {
patch: Vec<(Location, Statement<'tcx>)>,
mir: &'mir Body<'tcx>,
}

impl<'mir, 'tcx> ResultsVisitor<'mir, 'tcx, Results<'tcx, MaybeLiveLocals>>
for Visitor<'mir, 'tcx>
{
type FlowState = <MaybeLiveLocals as AnalysisDomain<'tcx>>::Domain;
fn visit_statement_before_primary_effect(
&mut self,
_: &Results<'tcx, MaybeLiveLocals>,
state: &Self::FlowState,
statement: &'mir Statement<'tcx>,
location: Location,
) {
match &statement.kind {
StatementKind::Assign(box (place, Rvalue::Ref(_, BorrowKind::Mut { .. }, rplace)))
if rplace.projection.iter().eq([PlaceElem::Deref])
&& !state.contains(rplace.local)
&& self.mir.local_decls[rplace.local].ty.ref_mutability() // don't convert raw-pointers
== Some(Mutability::Mut) =>
{
// place = &mut * local => place = move local
let new_rplace = Place { local: rplace.local, projection: List::empty() };
let new_rplace = Rvalue::Use(Operand::Move(new_rplace));
let kind = StatementKind::Assign(Box::new((*place, new_rplace)));
let source_info = statement.source_info.clone();
self.patch.push((location, Statement { kind, source_info }))
}
_ => {}
}
}
}

/// Cleans up unnecessary reborrows
/// x = &mut * y => x = move y
/// when y is dead afterwards
pub(crate) fn remove_mir_reborrows<'tcx>(tcx: TyCtxt<'tcx>, mir: &mut Body<'tcx>) {
let mut vistor = Visitor { patch: Vec::new(), mir };
MaybeLiveLocals
.into_engine(tcx, mir)
.iterate_to_fixpoint()
.visit_reachable_with(mir, &mut vistor);
for (loc, statement) in vistor.patch {
mir.basic_blocks.as_mut()[loc.block].statements[loc.statement_index] = statement;
}
}
82 changes: 32 additions & 50 deletions creusot/tests/should_fail/bug/492.mlcfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,28 +17,6 @@ module CreusotContracts_Invariant_Inv
val inv (_x : t) : bool
ensures { result = inv _x }

end
module CreusotContracts_Resolve_Impl1_Resolve_Stub
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
end
module CreusotContracts_Resolve_Impl1_Resolve_Interface
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl1_Resolve
type t
use prelude.Borrow
predicate resolve (self : borrowed t) =
[#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module TyInv_Trivial
type t
Expand Down Expand Up @@ -66,46 +44,32 @@ module C492_ReborrowTuple
use prelude.Int
use prelude.UInt32
use prelude.Borrow
clone CreusotContracts_Invariant_Inv_Interface as Inv2 with
type t = (borrowed t, uint32)
clone TyInv_Trivial as TyInv_Trivial2 with
type t = (borrowed t, uint32),
predicate Inv0.inv = Inv2.inv,
axiom .
clone CreusotContracts_Invariant_Inv_Interface as Inv1 with
type t = borrowed t
type t = (borrowed t, uint32)
clone TyInv_Trivial as TyInv_Trivial1 with
type t = borrowed t,
type t = (borrowed t, uint32),
predicate Inv0.inv = Inv1.inv,
axiom .
clone CreusotContracts_Invariant_Inv_Interface as Inv0 with
type t = t
type t = borrowed t
clone TyInv_Trivial as TyInv_Trivial0 with
type t = t,
type t = borrowed t,
predicate Inv0.inv = Inv0.inv,
axiom .
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with
type t = t
let rec cfg reborrow_tuple [#"../492.rs" 5 0 5 52] [@cfg:stackify] [@cfg:subregion_analysis] (x : borrowed t) : (borrowed t, uint32)
requires {[#"../492.rs" 5 25 5 26] Inv1.inv x}
requires {[#"../492.rs" 5 25 5 26] Inv0.inv x}
ensures { [#"../492.rs" 4 10 4 27] * (let (a, _) = result in a) = * x }
ensures { [#"../492.rs" 5 39 5 52] Inv2.inv result }
ensures { [#"../492.rs" 5 39 5 52] Inv1.inv result }

= [@vc:do_not_keep_trace] [@vc:sp]
var _0 : (borrowed t, uint32);
var x : borrowed t = x;
var _3 : borrowed t;
{
goto BB0
}
BB0 {
_3 <- Borrow.borrow_mut ( * x);
x <- { x with current = ( ^ _3) };
assume { Inv0.inv ( ^ _3) };
_0 <- (_3, [#"../492.rs" 6 8 6 10] (32 : uint32));
_3 <- any borrowed t;
assert { [@expl:type invariant] Inv1.inv x };
assume { Resolve0.resolve x };
_0 <- (x, [#"../492.rs" 6 8 6 10] (32 : uint32));
x <- any borrowed t;
return _0
}

Expand Down Expand Up @@ -153,6 +117,28 @@ module CreusotContracts_Resolve_Impl0_Resolve
val resolve (self : (t1, t2)) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl1_Resolve_Stub
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
end
module CreusotContracts_Resolve_Impl1_Resolve_Interface
type t
use prelude.Borrow
predicate resolve (self : borrowed t)
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl1_Resolve
type t
use prelude.Borrow
predicate resolve (self : borrowed t) =
[#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34] ^ self = * self
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module CreusotContracts_Resolve_Impl2_Resolve_Stub
type t
Expand Down Expand Up @@ -216,7 +202,6 @@ module C492_Test
var x : int32;
var res : borrowed int32;
var _4 : (borrowed int32, uint32);
var _5 : borrowed int32;
var _6 : borrowed int32;
{
goto BB0
Expand All @@ -225,17 +210,14 @@ module C492_Test
x <- ([#"../492.rs" 11 16 11 17] (5 : int32));
_6 <- Borrow.borrow_mut x;
x <- ^ _6;
_5 <- Borrow.borrow_mut ( * _6);
_6 <- { _6 with current = ( ^ _5) };
_4 <- ([#"../492.rs" 12 19 12 41] ReborrowTuple0.reborrow_tuple _5);
_5 <- any borrowed int32;
_4 <- ([#"../492.rs" 12 19 12 41] ReborrowTuple0.reborrow_tuple _6);
_6 <- any borrowed int32;
goto BB1
}
BB1 {
res <- (let (a, _) = _4 in a);
_4 <- (let (a, b) = _4 in (any borrowed int32, b));
assume { Resolve0.resolve _4 };
assume { Resolve1.resolve _6 };
assert { [@expl:assertion] [#"../492.rs" 13 18 13 30] ^ res = (5 : int32) };
res <- { res with current = ([#"../492.rs" 14 11 14 13] (10 : int32)) };
assume { Resolve1.resolve res };
Expand Down
60 changes: 28 additions & 32 deletions creusot/tests/should_succeed/100doors.mlcfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,22 @@ module CreusotContracts_Std1_Vec_Impl0_ShallowModel

axiom shallow_model_spec : forall self : Alloc_Vec_Vec_Type.t_vec t a . ([#"../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] Inv0.inv self) -> ([#"../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] Inv1.inv (shallow_model self)) && ([#"../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model self) <= UIntSize.to_int Max0.mAX')
end
module Core_Option_Option_Type
type t_option 't =
| C_None
| C_Some 't

let function some_0 (self : t_option 't) : 't = [@vc:do_not_keep_trace] [@vc:sp]
match (self) with
| C_None -> any 't
| C_Some a -> a
end
end
module Alloc_Alloc_Global_Type
type t_global =
| C_Global

end
module CreusotContracts_Resolve_Impl1_Resolve_Stub
type t
use prelude.Borrow
Expand All @@ -218,22 +234,6 @@ module CreusotContracts_Resolve_Impl1_Resolve
val resolve (self : borrowed t) : bool
ensures { result = resolve self }

end
module Core_Option_Option_Type
type t_option 't =
| C_None
| C_Some 't

let function some_0 (self : t_option 't) : 't = [@vc:do_not_keep_trace] [@vc:sp]
match (self) with
| C_None -> any 't
| C_Some a -> a
end
end
module Alloc_Alloc_Global_Type
type t_global =
| C_Global

end
module CreusotContracts_Logic_Ops_Impl0_IndexLogic_Stub
type t
Expand Down Expand Up @@ -1162,6 +1162,8 @@ module C100doors_F
predicate Inv0.inv = Inv5.inv,
axiom .
use Core_Ops_Range_Range_Type as Core_Ops_Range_Range_Type
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve3 with
type t = Core_Ops_Range_Range_Type.t_range usize
clone CreusotContracts_Invariant_Inv_Interface as Inv4 with
type t = borrowed (Core_Ops_Range_Range_Type.t_range usize)
clone TyInv_Trivial as TyInv_Trivial4 with
Expand All @@ -1186,7 +1188,7 @@ module C100doors_F
type t = bool,
predicate Inv0.inv = Inv1.inv,
axiom .
clone CreusotContracts_Resolve_Impl2_Resolve as Resolve3 with
clone CreusotContracts_Resolve_Impl2_Resolve as Resolve2 with
type t = bool
clone CreusotContracts_Std1_Slice_Impl5_ResolveElswhere as ResolveElswhere0 with
type t = bool
Expand All @@ -1212,11 +1214,9 @@ module C100doors_F
function ShallowModel0.shallow_model = ShallowModel0.shallow_model
use prelude.Int
clone CreusotContracts_Std1_Num_Impl16_DeepModel as DeepModel0
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with
type t = Core_Ops_Range_Range_Type.t_range usize
clone CreusotContracts_Std1_Iter_Range_Impl0_Completed as Completed0 with
type idx = usize,
predicate Resolve0.resolve = Resolve0.resolve,
predicate Resolve0.resolve = Resolve3.resolve,
function DeepModel0.deep_model = DeepModel0.deep_model
clone CreusotContracts_Invariant_Inv_Interface as Inv0 with
type t = Core_Ops_Range_Range_Type.t_range usize
Expand Down Expand Up @@ -1249,15 +1249,15 @@ module C100doors_F
predicate Inv0.inv = Inv2.inv,
val Max0.mAX' = Max0.mAX',
predicate Inv1.inv = Inv3.inv
clone CreusotContracts_Std1_Vec_Impl10_Resolve as Resolve2 with
clone CreusotContracts_Std1_Vec_Impl10_Resolve as Resolve1 with
type t = bool,
function ShallowModel0.shallow_model = ShallowModel0.shallow_model,
function IndexLogic0.index_logic = IndexLogic0.index_logic,
predicate Resolve0.resolve = Resolve3.resolve,
predicate Resolve0.resolve = Resolve2.resolve,
predicate Inv0.inv = Inv2.inv,
val Max0.mAX' = Max0.mAX',
predicate Inv1.inv = Inv3.inv
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with
clone CreusotContracts_Resolve_Impl1_Resolve as Resolve0 with
type t = bool
clone Alloc_Vec_Impl13_IndexMut_Interface as IndexMut0 with
type t = bool,
Expand Down Expand Up @@ -1314,7 +1314,6 @@ module C100doors_F
var produced : Ghost.ghost_ty (Seq.seq usize);
var _11 : ();
var _12 : Core_Option_Option_Type.t_option usize;
var _13 : borrowed (Core_Ops_Range_Range_Type.t_range usize);
var _14 : borrowed (Core_Ops_Range_Range_Type.t_range usize);
var __creusot_proc_iter_elem : usize;
var _17 : Ghost.ghost_ty (Seq.seq usize);
Expand Down Expand Up @@ -1357,29 +1356,26 @@ module C100doors_F
BB7 {
_14 <- Borrow.borrow_mut iter;
iter <- ^ _14;
_13 <- Borrow.borrow_mut ( * _14);
_14 <- { _14 with current = ( ^ _13) };
_12 <- ([#"../100doors.rs" 20 4 20 41] Next0.next _13);
_13 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize);
_12 <- ([#"../100doors.rs" 20 4 20 41] Next0.next _14);
_14 <- any borrowed (Core_Ops_Range_Range_Type.t_range usize);
goto BB8
}
BB8 {
assume { Resolve0.resolve _14 };
switch (_12)
| Core_Option_Option_Type.C_None -> goto BB9
| Core_Option_Option_Type.C_Some _ -> goto BB10
end
}
BB9 {
assume { Resolve2.resolve door_open };
assume { Resolve1.resolve door_open };
_0 <- ();
goto BB21
}
BB10 {
goto BB12
}
BB11 {
assume { Resolve2.resolve door_open };
assume { Resolve1.resolve door_open };
absurd
}
BB12 {
Expand Down Expand Up @@ -1421,7 +1417,7 @@ module C100doors_F
}
BB19 {
_30 <- { _30 with current = (not _26) };
assume { Resolve1.resolve _30 };
assume { Resolve0.resolve _30 };
door <- ([#"../100doors.rs" 27 12 27 24] door + pass);
_11 <- ();
goto BB15
Expand Down
Loading
Loading