Skip to content

Commit

Permalink
Added MIR optimization to avoid unnecessary re-borrows
Browse files Browse the repository at this point in the history
  • Loading branch information
dewert99 committed Nov 10, 2023
1 parent 8453699 commit 8cd3c63
Show file tree
Hide file tree
Showing 53 changed files with 2,128 additions and 3,224 deletions.
3 changes: 2 additions & 1 deletion creusot/src/callbacks.rs
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
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
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
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
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

0 comments on commit 8cd3c63

Please sign in to comment.