Skip to content

Commit

Permalink
Bump rustc.
Browse files Browse the repository at this point in the history
  • Loading branch information
jhjourdan committed Jan 31, 2025
1 parent 4a9678e commit 4398b14
Show file tree
Hide file tree
Showing 265 changed files with 17,954 additions and 16,185 deletions.
2 changes: 1 addition & 1 deletion creusot-contracts-proc/src/invariant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ fn filter_invariants(
let mut invariants = Vec::new();
parse_push_invariant(&mut invariants, tag, invariant)?;

let attrs = attrs.extract_if(|attr| {
let attrs = attrs.extract_if(0.., |attr| {
attr.path().get_ident().map_or(false, |i| i == "invariant" || i == "variant")
});
for attr in attrs {
Expand Down
3 changes: 1 addition & 2 deletions creusot-contracts/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@
allocator_api,
unboxed_closures,
tuple_trait,
strict_provenance,
panic_internals,
libstd_sys_internals,
rt,
Expand Down Expand Up @@ -359,7 +358,7 @@ pub mod macros {
/// #[ensures(result == x + 1)]
/// pub(super) fn foo(x: Int) -> Int {
/// // ...
/// # x + 1
/// # x + 1
/// }
/// }
///
Expand Down
6 changes: 3 additions & 3 deletions creusot-rustc/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ extern crate log;
use creusot::callbacks::*;
use creusot_args::CREUSOT_RUSTC_ARGS;
use options::CreusotArgs;
use rustc_driver::RunCompiler;
use rustc_driver::run_compiler;
use rustc_session::{config::ErrorOutputType, EarlyDiagCtxt};
use std::{env, panic, process::Command};

Expand Down Expand Up @@ -73,11 +73,11 @@ fn setup_plugin() {
Ok(opts) => opts,
Err(msg) => panic!("Error: {msg}"),
};
RunCompiler::new(&args, &mut ToWhy::new(opts)).run().unwrap();
run_compiler(&args, &mut ToWhy::new(opts))
}
_ => {
args.push("--cfg=creusot".to_string());
RunCompiler::new(&args, &mut DefaultCallbacks).run().unwrap()
run_compiler(&args, &mut DefaultCallbacks)
}
}
}
Expand Down
65 changes: 18 additions & 47 deletions creusot/src/analysis/borrows.rs
Original file line number Diff line number Diff line change
@@ -1,22 +1,18 @@
use rustc_borrowck::{
borrow_set::BorrowSet,
consumers::{
calculate_borrows_out_of_scope_at_location, BorrowIndex, PlaceConflictBias, PlaceExt,
RegionInferenceContext,
},
use rustc_borrowck::consumers::{
calculate_borrows_out_of_scope_at_location, BorrowIndex, BorrowSet, PlaceConflictBias,
PlaceExt, RegionInferenceContext,
};
use rustc_data_structures::fx::FxIndexMap;
use std::fmt;
use rustc_index::bit_set::MixedBitSet;
// This Source Code Form is subject to the terms of the Mozilla Public
// License, v. 2.0. If a copy of the MPL was not distributed with this
// file, You can obtain one at https://mozilla.org/MPL/2.0/.
//
use rustc_index::bit_set::BitSet;
use rustc_middle::{
mir::{self, Body, CallReturnPlaces, Location, Place, TerminatorEdges},
mir::{self, Body, Location, Place, TerminatorEdges},
ty::TyCtxt,
};
use rustc_mir_dataflow::{fmt::DebugWithContext, AnalysisDomain, GenKill, GenKillAnalysis};
use rustc_mir_dataflow::{Analysis, GenKill};

pub struct Borrows<'a, 'mir, 'tcx> {
tcx: TyCtxt<'tcx>,
Expand Down Expand Up @@ -46,10 +42,6 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
Borrows { tcx, body, borrow_set, borrows_out_of_scope_at_location }
}

pub fn location(&self, idx: BorrowIndex) -> &Location {
&self.borrow_set[idx].reserve_location
}

/// Add all borrows to the kill set, if those borrows are out of scope at `location`.
/// That means they went out of a nonlexical scope
fn kill_loans_out_of_scope_at_location(
Expand Down Expand Up @@ -79,7 +71,7 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {

let other_borrows_of_local = self
.borrow_set
.local_map
.local_map()
.get(&place.local)
.into_iter()
.flat_map(|bs| bs.iter())
Expand All @@ -103,7 +95,7 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
rustc_borrowck::consumers::places_conflict(
self.tcx,
self.body,
self.borrow_set[i].borrowed_place,
self.borrow_set[i].borrowed_place(),
place,
PlaceConflictBias::NoOverlap,
)
Expand All @@ -113,32 +105,24 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
}
}

impl<'tcx> AnalysisDomain<'tcx> for Borrows<'_, '_, 'tcx> {
type Domain = BitSet<BorrowIndex>;
impl<'tcx> Analysis<'tcx> for Borrows<'_, '_, 'tcx> {
type Domain = MixedBitSet<BorrowIndex>;

const NAME: &'static str = "borrows";

fn bottom_value(&self, _: &mir::Body<'tcx>) -> Self::Domain {
// bottom = nothing is reserved or activated yet;
BitSet::new_empty(self.borrow_set.len())
MixedBitSet::new_empty(self.borrow_set.location_map().len())
}

fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {
// no borrows of code region_scopes have been taken prior to
// function execution, so this method has no effect.
}
}

impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
type Idx = BorrowIndex;

fn domain_size(&self, _: &mir::Body<'tcx>) -> usize {
self.borrow_set.len()
}

fn statement_effect(
fn apply_primary_statement_effect(
&mut self,
trans: &mut impl GenKill<Self::Idx>,
trans: &mut Self::Domain,
stmt: &mir::Statement<'tcx>,
location: Location,
) {
Expand All @@ -150,11 +134,11 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
if !place.ignore_borrow(
self.tcx,
self.body,
&self.borrow_set.locals_state_at_exit,
&self.borrow_set.locals_state_at_exit(),
) {
let index = self
.borrow_set
.location_map
.location_map()
.get_index_of(&location)
.map(BorrowIndex::from)
.unwrap_or_else(|| {
Expand Down Expand Up @@ -185,11 +169,12 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
| mir::StatementKind::Coverage(..)
| mir::StatementKind::Intrinsic(..)
| mir::StatementKind::ConstEvalCounter
| mir::StatementKind::Nop => {}
| mir::StatementKind::Nop
| mir::StatementKind::BackwardIncompatibleDropHint { .. } => {}
}
}

fn terminator_effect<'mir>(
fn apply_primary_terminator_effect<'mir>(
&mut self,
trans: &mut Self::Domain,
terminator: &'mir mir::Terminator<'tcx>,
Expand All @@ -208,18 +193,4 @@ impl<'tcx> GenKillAnalysis<'tcx> for Borrows<'_, '_, 'tcx> {
}
terminator.edges()
}

fn call_return_effect(
&mut self,
_trans: &mut Self::Domain,
_block: mir::BasicBlock,
_return_places: CallReturnPlaces<'_, 'tcx>,
) {
}
}

impl DebugWithContext<Borrows<'_, '_, '_>> for BorrowIndex {
fn fmt_with(&self, ctxt: &Borrows<'_, '_, '_>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{:?}", ctxt.location(*self))
}
}
55 changes: 21 additions & 34 deletions creusot/src/analysis/liveness_no_drop.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use rustc_index::bit_set::ChunkedBitSet;
use rustc_index::bit_set::MixedBitSet;
use rustc_middle::{
mir::{
self,
Expand All @@ -9,7 +9,7 @@ use rustc_middle::{
};
use rustc_mir_dataflow::{
move_paths::{HasMoveData, LookupResult, MoveData, MovePathIndex},
on_all_children_bits, AnalysisDomain, Backward, GenKill, GenKillAnalysis, MoveDataParamEnv,
on_all_children_bits, Analysis, Backward, GenKill,
};

use crate::resolve::place_contains_borrow_deref;
Expand All @@ -29,59 +29,46 @@ use crate::resolve::place_contains_borrow_deref;
/// borrows for writing is still considered as a Use.
pub struct MaybeLiveExceptDrop<'a, 'tcx> {
body: &'a mir::Body<'tcx>,
mdpe: &'a MoveDataParamEnv<'tcx>,
move_data: &'a MoveData<'tcx>,
tcx: TyCtxt<'tcx>,
}

impl<'a, 'tcx> MaybeLiveExceptDrop<'a, 'tcx> {
pub fn new(
body: &'a mir::Body<'tcx>,
mdpe: &'a MoveDataParamEnv<'tcx>,
tcx: TyCtxt<'tcx>,
) -> Self {
MaybeLiveExceptDrop { body, mdpe, tcx }
pub fn new(tcx: TyCtxt<'tcx>, body: &'a mir::Body<'tcx>, mdpe: &'a MoveData<'tcx>) -> Self {
MaybeLiveExceptDrop { body, move_data: mdpe, tcx }
}
}

impl<'a, 'tcx> AnalysisDomain<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
type Domain = ChunkedBitSet<MovePathIndex>;
impl<'a, 'tcx> HasMoveData<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
fn move_data(&self) -> &MoveData<'tcx> {
&self.move_data
}
}

impl<'a, 'tcx> Analysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
type Domain = MixedBitSet<MovePathIndex>;
type Direction = Backward;

const NAME: &'static str = "liveness-two";

fn bottom_value(&self, _body: &mir::Body<'tcx>) -> Self::Domain {
// bottom = not live
ChunkedBitSet::new_empty(self.move_data().move_paths.len())
MixedBitSet::new_empty(self.move_data().move_paths.len())
}

fn initialize_start_block(&self, _: &mir::Body<'tcx>, _: &mut Self::Domain) {
// No variables are live until we observe a use
}
}

impl<'a, 'tcx> HasMoveData<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
fn move_data(&self) -> &MoveData<'tcx> {
&self.mdpe.move_data
}
}

impl<'a, 'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
type Idx = MovePathIndex;

fn domain_size(&self, _body: &mir::Body<'tcx>) -> usize {
self.move_data().move_paths.len()
}

fn statement_effect(
fn apply_primary_statement_effect(
&mut self,
trans: &mut impl GenKill<Self::Idx>,
trans: &mut Self::Domain,
statement: &mir::Statement<'tcx>,
location: Location,
) {
TransferFunction(trans, self).visit_statement(statement, location);
}

fn terminator_effect<'mir>(
fn apply_primary_terminator_effect<'mir>(
&mut self,
trans: &mut Self::Domain,
terminator: &'mir mir::Terminator<'tcx>,
Expand All @@ -91,7 +78,7 @@ impl<'a, 'tcx> GenKillAnalysis<'tcx> for MaybeLiveExceptDrop<'a, 'tcx> {
terminator.edges()
}

fn call_return_effect(
fn apply_call_return_effect(
&mut self,
trans: &mut Self::Domain,
_block: mir::BasicBlock,
Expand Down Expand Up @@ -130,7 +117,7 @@ where
()
}

DefUse::for_place(place, context, self.1).apply(self.0, place, &self.1.mdpe.move_data);
DefUse::for_place(place, context, self.1).apply(self.0, place, &self.1.move_data);

// Visit indices of arrays/slices, which appear as locals
self.visit_projection(place.as_ref(), context, location);
Expand Down Expand Up @@ -211,12 +198,12 @@ impl DefUse {

// All other contexts are uses...
PlaceContext::MutatingUse(
MutatingUseContext::AddressOf
MutatingUseContext::RawBorrow
| MutatingUseContext::Borrow
| MutatingUseContext::Retag,
)
| PlaceContext::NonMutatingUse(
NonMutatingUseContext::AddressOf
NonMutatingUseContext::RawBorrow
| NonMutatingUseContext::Copy
| NonMutatingUseContext::Inspect
| NonMutatingUseContext::Move
Expand Down
Loading

0 comments on commit 4398b14

Please sign in to comment.