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

Jump to bottom

Update hax and rustc #222

Merged
merged 3 commits into from
Jun 5, 2024
Merged

Update hax and rustc #222

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
23697a9
Bump hax
Nadrieril May 28, 2024
08935cf
Move the rustc-tests definition to its own file
Nadrieril Jun 3, 2024
01bc90d
No need to force the rustc tests to match the rustc version we're using
Nadrieril Jun 3, 2024
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
6 changes: 3 additions & 3 deletions charon/Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions charon/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,8 +56,8 @@ which = "6.0.1"

hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main" }
hax-frontend-exporter-options = { git = "https://github.com/hacspec/hax", branch = "main" }
# hax-frontend-exporter = { path = "../../hacspec-v2/frontend/exporter" }
# hax-frontend-exporter-options = { path = "../../hacspec-v2/frontend/exporter/options" }
# hax-frontend-exporter = { path = "../../hax/frontend/exporter" }
# hax-frontend-exporter-options = { path = "../../hax/frontend/exporter/options" }
macros = { path = "./macros" }

[dev-dependencies]
Expand Down
26 changes: 13 additions & 13 deletions charon/src/ast/names_utils.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -313,27 +313,27 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
let def_id = item.owner_id.to_def_id();

let name = match &item.kind {
ItemKind::OpaqueTy(_) => unimplemented!(),
ItemKind::Union(_, _) => unimplemented!(),
ItemKind::ExternCrate(_) => {
ItemKind::OpaqueTy(..) => unimplemented!(),
ItemKind::Union(..) => unimplemented!(),
ItemKind::ExternCrate(..) => {
// We ignore this -
// TODO: investigate when extern crates appear, and why
Option::None
}
ItemKind::Use(_, _) => Option::None,
ItemKind::TyAlias(_, _) => {
ItemKind::Use(..) => Option::None,
ItemKind::TyAlias(..) => {
// We ignore the type aliases - it seems they are inlined
Option::None
}
ItemKind::Enum(_, _)
| ItemKind::Struct(_, _)
| ItemKind::Fn(_, _, _)
| ItemKind::Impl(_)
| ItemKind::Mod(_)
ItemKind::Enum(..)
| ItemKind::Struct(..)
| ItemKind::Fn(..)
| ItemKind::Impl(..)
| ItemKind::Mod(..)
| ItemKind::ForeignMod { .. }
| ItemKind::Const(_, _)
| ItemKind::Static(_, _, _)
| ItemKind::Macro(_, _)
| ItemKind::Const(..)
| ItemKind::Static(..)
| ItemKind::Macro(..)
| ItemKind::Trait(..) => Option::Some(self.def_id_to_name(def_id)?),
_ => {
unimplemented!("{:?}", item.kind);
Expand Down
6 changes: 5 additions & 1 deletion charon/src/bin/charon-driver/driver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,11 @@ impl Callbacks for CharonCallbacks {
/// For this reason, and as we may want to plug ourselves at different
/// phases of the compilation process, we query the context as early as
/// possible (i.e., after parsing). See [charon_lib::get_mir].
fn after_parsing<'tcx>(&mut self, c: &Compiler, queries: &'tcx Queries<'tcx>) -> Compilation {
fn after_crate_root_parsing<'tcx>(
&mut self,
c: &Compiler,
queries: &'tcx Queries<'tcx>,
) -> Compilation {
// Set up our own `DefId` debug routine.
rustc_hir::def_id::DEF_ID_DEBUG
.swap(&(def_id_debug as fn(_, &mut fmt::Formatter<'_>) -> _));
Expand Down
2 changes: 1 addition & 1 deletion charon/src/export.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ impl<FD: Serialize + Clone, GD: Serialize + Clone> GCrateData<FD, GD> {
};

// Create the file.
let std::io::Result::Ok(outfile) = File::create(target_filename.clone()) else {
let std::io::Result::Ok(outfile) = File::create(target_filename) else {
error!("Could not open: {:?}", target_filename);
return Err(());
};
Expand Down
2 changes: 1 addition & 1 deletion charon/src/translate/translate_ctx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -587,7 +587,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
| Struct
| Trait
| TraitAlias
| TyAlias
| TyAlias { .. }
| Union
| Use => Some(self.tcx.visibility(id).is_public()),
// These kinds don't have visibility modifiers (which would cause `visibility` to panic).
Expand Down
47 changes: 19 additions & 28 deletions charon/src/translate/translate_functions_to_ullbc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,18 +67,16 @@ fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp {
/// Small utility
pub(crate) fn check_impl_item(impl_item: &rustc_hir::Impl<'_>) {
// TODO: make proper error messages
use rustc_hir::{Constness, Defaultness, ImplPolarity, Unsafety};
use rustc_hir::{Defaultness, ImplPolarity, Unsafety};
assert!(impl_item.unsafety == Unsafety::Normal);
// About polarity:
// [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html]
// Not sure about what I should do about it. Should I do anything, actually?
// This seems useful to enforce some discipline on the user-side, but not
// necessary for analysis purposes.
assert!(impl_item.polarity == ImplPolarity::Positive);
// Note sure what this is about
// Not sure what this is about
assert!(impl_item.defaultness == Defaultness::Final);
// Note sure what this is about
assert!(impl_item.constness == Constness::NotConst);
}

impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
Expand Down Expand Up @@ -552,7 +550,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
span: rustc_span::Span,
rvalue: &hax::Rvalue,
) -> Result<Rvalue, Error> {
use std::ops::Deref;
let erase_regions = true;
match rvalue {
hax::Rvalue::Use(operand) => Ok(Rvalue::Use(self.translate_operand(span, operand)?)),
Expand Down Expand Up @@ -697,15 +694,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}
}
}
hax::Rvalue::BinaryOp(binop, operands) => {
let (left, right) = operands.deref();
Ok(Rvalue::BinaryOp(
self.t_ctx.translate_binaryop_kind(span, *binop)?,
self.translate_operand(span, left)?,
self.translate_operand(span, right)?,
))
}
hax::Rvalue::CheckedBinaryOp(binop, operands) => {
hax::Rvalue::BinaryOp(binop, (left, right)) => Ok(Rvalue::BinaryOp(
self.t_ctx.translate_binaryop_kind(span, *binop)?,
self.translate_operand(span, left)?,
self.translate_operand(span, right)?,
)),
hax::Rvalue::CheckedBinaryOp(binop, (left, right)) => {
let binop = match binop {
hax::BinOp::Add => BinOp::CheckedAdd,
hax::BinOp::Sub => BinOp::CheckedSub,
Expand All @@ -714,7 +708,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}");
}
};
let (left, right) = operands.deref();
Ok(Rvalue::BinaryOp(
binop,
self.translate_operand(span, left)?,
Expand Down Expand Up @@ -767,7 +760,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
.map(|op| self.translate_operand(span, op))
.try_collect()?;

match aggregate_kind.deref() {
match aggregate_kind {
hax::AggregateKind::Array(ty) => {
let t_ty = self.translate_ty(span, erase_regions, ty)?;
let cg = ConstGeneric::Value(Literal::Scalar(ScalarValue::Usize(
Expand Down Expand Up @@ -1082,12 +1075,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trace!("About to translate statement (MIR) {:?}", statement);
let span = statement.source_info.span.rust_span_data.unwrap().span();

use std::ops::Deref;

use hax::StatementKind;
let t_statement: Option<RawStatement> = match &*statement.kind {
StatementKind::Assign(assign) => {
let (place, rvalue) = assign.deref();
StatementKind::Assign((place, rvalue)) => {
let t_place = self.translate_place(span, place)?;
let t_rvalue = self.translate_rvalue(
statement.source_info.span.rust_span_data.unwrap().span(),
Expand All @@ -1096,8 +1086,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

Some(RawStatement::Assign(t_place, t_rvalue))
}
StatementKind::FakeRead(info) => {
let (_read_cause, place) = info.deref();
StatementKind::FakeRead((_read_cause, place)) => {
let t_place = self.translate_place(span, place)?;

Some(RawStatement::FakeRead(t_place))
Expand Down Expand Up @@ -1203,14 +1192,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

RawTerminator::Switch { discr, targets }
}
TerminatorKind::Resume => {
TerminatorKind::UnwindResume => {
// This is used to correctly unwind. We shouldn't get there: if
// we panic, the state gets stuck.
error_or_panic!(self, rustc_span, "Unexpected terminator: resume");
error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindResume");
}
TerminatorKind::UnwindTerminate { .. } => {
error_or_panic!(self, rustc_span, "Unexpected terminator: UnwindTerminate")
}
TerminatorKind::Return => RawTerminator::Return,
TerminatorKind::Unreachable => RawTerminator::Unreachable,
TerminatorKind::Terminate => unimplemented!(),
TerminatorKind::Drop {
place,
target,
Expand Down Expand Up @@ -1574,7 +1565,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let (substs, signature, closure_info): (
Vec<hax::GenericArg>,
rustc_middle::ty::Binder<'tcx, rustc_middle::ty::FnSig<'tcx>>,
Option<(ClosureKind, Vec<rustc_middle::ty::Ty<'tcx>>)>,
Option<(ClosureKind, &ty::List<rustc_middle::ty::Ty<'tcx>>)>,
) = if is_closure {
// Closures have a peculiar handling in Rust: we can't call
// `TyCtxt::fn_sig`.
Expand Down Expand Up @@ -1604,8 +1595,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
rustc_middle::ty::ClosureKind::FnOnce => ClosureKind::FnOnce,
};

// Retrieve the type of the captured stated
let state: Vec<rustc_middle::ty::Ty<'tcx>> = closure.upvar_tys().collect();
// Retrieve the type of the captured state
let state: &ty::List<rustc_middle::ty::Ty<'tcx>> = closure.upvar_tys();

let substs = substs.sinto(&self.hax_state);

Expand Down
2 changes: 0 additions & 2 deletions charon/src/translate/translate_traits.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,8 +166,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
// the parent and item predicates.
let trait_pred = rustc_middle::ty::TraitPredicate {
trait_ref,
// Not really necessary (dummy value)
constness: rustc_middle::ty::BoundConstness::NotConst,
// Not really necessary
polarity: rustc_middle::ty::ImplPolarity::Positive,
};
Expand Down
71 changes: 35 additions & 36 deletions charon/tests/cargo/dependencies.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,18 +75,17 @@ fn test_cargo_dependencies::main()
let left_val@10: &'_ (u32); // local
let right_val@11: &'_ (u32); // local
let @12: bool; // anonymous local
let @13: bool; // anonymous local
let @13: u32; // anonymous local
let @14: u32; // anonymous local
let @15: u32; // anonymous local
let kind@16: core::panicking::AssertKind; // local
let @17: core::panicking::AssertKind; // anonymous local
let kind@15: core::panicking::AssertKind; // local
let @16: core::panicking::AssertKind; // anonymous local
let @17: &'_ (u32); // anonymous local
let @18: &'_ (u32); // anonymous local
let @19: &'_ (u32); // anonymous local
let @20: &'_ (u32); // anonymous local
let @21: &'_ (u32); // anonymous local
let @22: core::option::Option<core::fmt::Arguments<'_>>; // anonymous local
let @21: core::option::Option<core::fmt::Arguments<'_>>; // anonymous local
let @22: (); // anonymous local
let @23: (); // anonymous local
let @24: (); // anonymous local

x@1 := const (0 : u32)
@fake_read(x@1)
Expand All @@ -105,40 +104,40 @@ fn test_cargo_dependencies::main()
@fake_read(@6)
left_val@10 := copy ((@6).0)
right_val@11 := copy ((@6).1)
@14 := copy (*(left_val@10))
@15 := copy (*(right_val@11))
@13 := move (@14) == move (@15)
drop @15
drop @14
@12 := ~(move (@13))
drop @13
@13 := copy (*(left_val@10))
@14 := copy (*(right_val@11))
@12 := move (@13) == move (@14)
if move (@12) {
nop
}
else {
@23 := ()
@5 := move (@23)
drop @12
drop right_val@11
drop left_val@10
drop @9
drop @6
drop @5
@24 := ()
@0 := move (@24)
drop x@1
@0 := ()
return
drop @14
drop @13
kind@15 := core::panicking::AssertKind::Eq { }
@fake_read(kind@15)
@16 := move (kind@15)
@18 := &*(left_val@10)
@17 := &*(@18)
@20 := &*(right_val@11)
@19 := &*(@20)
@21 := core::option::Option::None { }
panic
}
kind@16 := core::panicking::AssertKind::Eq { }
@fake_read(kind@16)
@17 := move (kind@16)
@19 := &*(left_val@10)
@18 := &*(@19)
@21 := &*(right_val@11)
@20 := &*(@21)
@22 := core::option::Option::None { }
panic
drop @14
drop @13
@22 := ()
@5 := move (@22)
drop @12
drop right_val@11
drop left_val@10
drop @9
drop @6
drop @5
@23 := ()
@0 := move (@23)
drop x@1
@0 := ()
return
}

fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
Expand Down
Loading