Skip to content

Commit

Permalink
Bump rustc. (#1334)
Browse files Browse the repository at this point in the history
  • Loading branch information
jhjourdan authored Feb 3, 2025
2 parents cb81007 + fd2236a commit 6546583
Show file tree
Hide file tree
Showing 423 changed files with 12,000 additions and 11,849 deletions.
727 changes: 350 additions & 377 deletions Cargo.lock

Large diffs are not rendered by default.

16 changes: 8 additions & 8 deletions cargo-creusot/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,17 +7,17 @@ publish = false
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
clap = { version = "4.2.5", features = ["derive", "env"] }
serde_json = { version = "1.0" }
toml = { version = "0.5.8" }
env_logger = "0.10"
clap = { version = "4.5", features = ["derive", "env"] }
serde_json = "1.0"
toml = "0.8"
env_logger = "0.11"
serde = { version = "1.0", features = ["derive"] }
why3 = { path = "../why3", features = ["serialize"] }
creusot-args = {path = "../creusot-args"}
creusot-setup = {path = "../creusot-setup"}
anyhow = "1.0"
cargo_metadata = "0.18.1"
include_dir = "0.7.3"
tempdir = "0.3.7"
glob = "0.3.1"
cargo_metadata = "0.19"
include_dir = "0.7"
tempdir = "0.3"
glob = "0.3"

6 changes: 3 additions & 3 deletions cargo-creusot/src/helpers.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use std::path::PathBuf;

use anyhow::Error;
use cargo_metadata;
use cargo_metadata::{self, CrateType};
use creusot_args::options::CommonOptions;
pub type Result<T> = anyhow::Result<T>;

Expand All @@ -27,8 +27,8 @@ pub(crate) fn get_crate(m: &cargo_metadata::Metadata) -> Result<String> {
let target = package.targets.first().ok_or(Error::msg("No target found"))?;
let krate_name = target.name.replace("-", "_");
let krate_type = target.crate_types.first().ok_or(Error::msg("No crate type found"))?;
let krate_type = if krate_type == "lib" { "rlib" } else { krate_type };
Ok(krate_name + "_" + krate_type)
let krate_type = if krate_type == &CrateType::Lib { &CrateType::RLib } else { krate_type };
Ok(krate_name + "_" + &krate_type.to_string())
}

fn get_crate_() -> Result<String> {
Expand Down
4 changes: 2 additions & 2 deletions creusot-args/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,6 @@ publish = false
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
clap = { version = "4.2.5", features = ["derive", "env"] }
serde = { version = "1.0.195", features = ["derive"] }
clap = { version = "4.5", features = ["derive", "env"] }
serde = { version = "1.0", features = ["derive"] }

4 changes: 2 additions & 2 deletions creusot-contracts-dummy/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,6 @@ proc-macro = true
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
quote = "1.0.35"
proc-macro2 = "1.0.29"
quote = "1.0"
proc-macro2 = "1.0"

8 changes: 4 additions & 4 deletions creusot-contracts-proc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,9 @@ proc-macro = true
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
quote = "1.0.35"
uuid = { version = "1.3", features = ["v4"] }
quote = "1.0"
uuid = { version = "1.12", features = ["v4"] }
pearlite-syn = { version = "0.3", path = "../pearlite-syn", features = ["full"] }
syn = { version = "2.0.15"}
proc-macro2 = "1.0.29"
syn = { version = "2.0"}
proc-macro2 = "1.0"

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
2 changes: 1 addition & 1 deletion creusot-contracts/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ description = "Provides contracts and logic helpers for Creusot"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[target.'cfg(creusot)'.dependencies]
num-rational = "0.3.2"
num-rational = "0.4"
creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.3.0" }

[target.'cfg(not(creusot))'.dependencies]
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
2 changes: 1 addition & 1 deletion creusot-dev-config/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,5 @@ publish = false
[dependencies]
creusot-setup = { path = "../creusot-setup" }
anyhow = "1.0"
which = "6.0"
which = "7.0"

2 changes: 1 addition & 1 deletion creusot-metadata/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ publish = false
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
indexmap = "2.7.0"
indexmap = "2.7"

[package.metadata.rust-analyzer]
# This crate uses #[feature(rustc_private)].
Expand Down
4 changes: 2 additions & 2 deletions creusot-rustc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ publish = false
[dependencies]
serde_json = { version = "1.0" }
creusot = { path = "../creusot", version = "0.3" }
toml = "0.5.8"
env_logger = "0.10"
toml = "0.8"
env_logger = "0.11"
serde = { version = "1.0", features = ["derive"] }
creusot-args = { path = "../creusot-args" }

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
8 changes: 4 additions & 4 deletions creusot-setup/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ publish = false
[dependencies]
creusot-args = {path = "../creusot-args"}
serde = { version = "1.0", features = ["derive"] }
toml = { version = "0.5.8", features = ["preserve_order"] }
directories = "5.0"
which = "6.0"
toml = { version = "0.8", features = ["preserve_order"] }
directories = "6.0"
which = "7.0"
anyhow = "1.0"
reqwest = { version = "0.12", features = ["blocking"] }
zip = "2.2"
hex = "0.4"
sha2 = "0.10"
indoc = "2.0.5"
indoc = "2.0"

28 changes: 14 additions & 14 deletions creusot/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,32 +7,32 @@ license = "LGPL-2.1-or-later"
publish = false

[dependencies]
itertools = "0.10"
itertools = "0.14"
log = "0.4"
serde = { version = "1.0", features = ["derive"] }
# Necessary as this introduces a version of `GraphMap` with no `Ord` bound.
# If https://github.com/petgraph/petgraph/issues/646 is solved, go back to upstream.
petgraph = { version = "0.6", git = "https://github.com/xldenis/petgraph", rev = "04cecb7" }
indexmap = { version = "2.7.0", features = ["serde"] }
toml = "0.5.8"
indexmap = { version = "2.7", features = ["serde"] }
toml = "0.8"
why3 = { path = "../why3", features = ["serialize"] }
creusot-metadata = { path = "../creusot-metadata" }
include_dir = "0.7.3"
tempdir = "0.3.7"
serde_json = { version = "1.0" }
lazy_static = "1.4.0"
include_dir = "0.7"
tempdir = "0.3"
serde_json = "1.0"
lazy_static = "1.5"
pathdiff = "0.2"

[dev-dependencies]
clap = { version = "4.2", features = ["derive", "env"] }
regex = "1.10.5"
clap = { version = "4.5", features = ["derive", "env"] }
regex = "1.11"
glob = "*"
assert_cmd = "1.0"
similar = "2.2"
termcolor = "1.1"
arraydeque = "0.4"
assert_cmd = "2.0"
similar = "2.7"
termcolor = "1.4"
arraydeque = "0.5"
creusot-contracts = { path = "../creusot-contracts", features = ["typechecker"] }
escargot = { version = "0.5" }
escargot = "0.5"
creusot-setup = { path = "../creusot-setup" }
libc = "0.2"

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))
}
}
Loading

0 comments on commit 6546583

Please sign in to comment.