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

Various improvements #422

Merged
merged 6 commits into from
Oct 16, 2024
Merged

Various improvements #422

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e8ae892
Disable all MIR optimization passes by default
Nadrieril Sep 16, 2024
469ef6c
Update hax
Nadrieril Oct 15, 2024
de20cd6
Emit a good error message for complex expressions in const generics
Nadrieril Oct 15, 2024
0c053c5
Emit a proper error message for GATs
Nadrieril Oct 15, 2024
5818d1e
Remove leftover code path
Nadrieril Oct 15, 2024
a1566c0
Improve some error messages
Nadrieril Oct 15, 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.

47 changes: 47 additions & 0 deletions charon/src/bin/charon-driver/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ use crate::driver::{
use charon_lib::logger;
use charon_lib::options;
use charon_lib::trace;
use itertools::Itertools;

fn main() {
// Initialize the logger
Expand Down Expand Up @@ -191,6 +192,52 @@ fn main() {
compiler_args.push(extra_flag);
}

let disabled_mir_passes = [
"AfterConstProp",
"AfterGVN",
"AfterUnreachableEnumBranching)",
"BeforeConstProp",
"CheckAlignment",
"CopyProp",
"CriticalCallEdges",
"DataflowConstProp",
"DeduplicateBlocks",
"DestinationPropagation",
"EarlyOtherwiseBranch",
"EnumSizeOpt",
"GVN",
"Initial",
"Inline",
"InstSimplify",
"JumpThreading",
"LowerSliceLenCalls",
"MatchBranchSimplification",
"MentionedItems",
"MultipleReturnTerminators",
"ReferencePropagation",
"RemoveNoopLandingPads",
"RemoveStorageMarkers",
"RemoveUnneededDrops",
"RemoveZsts",
"RenameReturnPlace",
"ReorderBasicBlocks",
"ReorderLocals",
"ScalarReplacementOfAggregates",
"SimplifyComparisonIntegral",
"SimplifyLocals",
"SingleUseConsts",
"UnreachableEnumBranching",
"UnreachablePropagation",
];
// Disable all these mir passes.
compiler_args.push(format!(
"-Zmir-enable-passes={}",
disabled_mir_passes
.iter()
.map(|p| format!("-{p}"))
.format(",")
));

trace!("Compiler arguments: {:?}", compiler_args);

// Call the Rust compiler with our custom callback.
Expand Down
3 changes: 0 additions & 3 deletions charon/src/bin/charon-driver/translate/translate_constants.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,9 +111,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
}
ConstantExprKind::TraitConst { impl_expr, name } => {
let trait_ref = self.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
// The trait ref should be Some(...): trait markers (that we
// may eliminate) don't have constants.
let trait_ref = trait_ref.unwrap();
let name = TraitItemName(name.clone());
RawConstantExpr::TraitConst(trait_ref, name)
}
Expand Down
5 changes: 5 additions & 0 deletions charon/src/bin/charon-driver/translate/translate_ctx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -397,6 +397,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
// block.
None
}
DefPathData::Ctor => {
// Do nothing, the constructor of a struct/variant has the same name as the
// struct/variant.
None
}
_ => {
error_or_panic!(
self,
Expand Down
44 changes: 23 additions & 21 deletions charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,14 +55,6 @@ fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind {
}
}

fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp {
match binop {
hax::UnOp::Not => UnOp::Not,
hax::UnOp::Neg => UnOp::Neg,
hax::UnOp::PtrMetadata => unimplemented!("Unop::PtrMetadata"),
}
}

impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
fn translate_binaryop_kind(&mut self, span: Span, binop: hax::BinOp) -> Result<BinOp, Error> {
Ok(match binop {
Expand Down Expand Up @@ -601,10 +593,19 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
};
Ok(Rvalue::NullaryOp(op, ty))
}
hax::Rvalue::UnaryOp(unop, operand) => Ok(Rvalue::UnaryOp(
translate_unaryop_kind(*unop),
self.translate_operand(span, operand)?,
)),
hax::Rvalue::UnaryOp(unop, operand) => {
let unop = match unop {
hax::UnOp::Not => UnOp::Not,
hax::UnOp::Neg => UnOp::Neg,
hax::UnOp::PtrMetadata => {
error_or_panic!(self, span, "Unsupported operation: PtrMetadata")
}
};
Ok(Rvalue::UnaryOp(
unop,
self.translate_operand(span, operand)?,
))
}
hax::Rvalue::Discriminant(place) => {
let (place, ty) = self.translate_place_with_type(span, place)?;
if let TyKind::Adt(TypeId::Adt(adt_id), _) = ty.kind() {
Expand Down Expand Up @@ -848,18 +849,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
let fun_id = self.register_fun_decl_id(span, def_id);
// Two cases depending on whether we call a trait method or not
match trait_info {
None => {
// "Regular" function call
FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id))
}
// Direct function call
None => FunIdOrTraitMethodRef::Fun(FunId::Regular(fun_id)),
// Trait method
Some(trait_info) => {
// Trait method
let impl_expr =
self.translate_trait_impl_expr(span, erase_regions, trait_info)?;
// The impl source should be Some(...): trait markers (that we may
// eliminate) don't have methods.
let impl_expr = impl_expr.unwrap();

let method_name = self.t_ctx.translate_trait_item_name(def_id)?;
FunIdOrTraitMethodRef::Trait(impl_expr, method_name, fun_id)
}
Expand Down Expand Up @@ -1368,6 +1363,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
hax::FullDefKind::Closure { args, .. } => &args.sig,
hax::FullDefKind::Fn { sig, .. } => sig,
hax::FullDefKind::AssocFn { sig, .. } => sig,
hax::FullDefKind::Ctor { .. } => {
error_or_panic!(
self,
span,
"Casting constructors to function pointers is not supported"
)
}
_ => panic!("Unexpected definition for function: {def:?}"),
};

Expand Down
64 changes: 36 additions & 28 deletions charon/src/bin/charon-driver/translate/translate_predicates.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
use super::translate_ctx::*;
use super::translate_traits::PredicateLocation;
use charon_lib::ast::*;
use charon_lib::formatter::IntoFormatter;
use charon_lib::ids::Vector;
use charon_lib::pretty::FmtWithCtx;
use hax_frontend_exporter as hax;

impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
Expand Down Expand Up @@ -79,14 +81,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
Ok(())
}

/// Returns an [Option] because we may filter trait refs about builtin or
/// auto traits like [core::marker::Sized] and [core::marker::Sync].
pub(crate) fn translate_trait_decl_ref(
&mut self,
span: Span,
erase_regions: bool,
bound_trait_ref: &hax::Binder<hax::TraitRef>,
) -> Result<Option<PolyTraitDeclRef>, Error> {
) -> Result<PolyTraitDeclRef, Error> {
let binder = bound_trait_ref.rebind(());
self.with_locally_bound_regions_group(span, binder, move |ctx| {
let trait_ref = bound_trait_ref.hax_skip_binder_ref();
Expand All @@ -100,10 +100,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
&parent_trait_refs,
)?;

Ok(Some(RegionBinder {
Ok(RegionBinder {
regions: ctx.region_vars[0].clone(),
skip_binder: TraitDeclRef { trait_id, generics },
}))
})
})
}

Expand Down Expand Up @@ -223,10 +223,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {

let trait_ref =
ctx.translate_trait_impl_expr(span, erase_regions, impl_expr)?;
// The trait ref should be Some(...): the marker traits (that
// we may filter) don't have associated types.
let trait_ref = trait_ref.unwrap();
let ty = ctx.translate_ty(span, erase_regions, ty).unwrap();
let ty = ctx.translate_ty(span, erase_regions, ty)?;
let type_name = TraitItemName(assoc_item.name.clone().into());
ctx.generic_params
.trait_type_constraints
Expand All @@ -244,7 +241,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
// the type information in the const generic parameters
// directly? For now we just ignore it.
}
ClauseKind::WellFormed(_) | ClauseKind::ConstEvaluatable(_) => {
ClauseKind::WellFormed(_) => {
error_or_panic!(
ctx,
span,
format!("Well-formedness clauses are unsupported")
)
}
ClauseKind::ConstEvaluatable(_) => {
error_or_panic!(ctx, span, format!("Unsupported clause: {:?}", kind))
}
}
Expand All @@ -270,27 +274,21 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
erase_regions: bool,
impl_sources: &[hax::ImplExpr],
) -> Result<Vector<TraitClauseId, TraitRef>, Error> {
let res: Vec<_> = impl_sources
impl_sources
.iter()
.map(|x| self.translate_trait_impl_expr(span, erase_regions, x))
.try_collect()?;
Ok(res.into_iter().flatten().collect())
.try_collect()
}

/// Returns an [Option] because we may ignore some builtin or auto traits
/// like [core::marker::Sized] or [core::marker::Sync].
#[tracing::instrument(skip(self, span, erase_regions, impl_expr))]
pub(crate) fn translate_trait_impl_expr(
&mut self,
span: Span,
erase_regions: bool,
impl_expr: &hax::ImplExpr,
) -> Result<Option<TraitRef>, Error> {
) -> Result<TraitRef, Error> {
let trait_decl_ref =
match self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)? {
None => return Ok(None),
Some(tr) => tr,
};
self.translate_trait_decl_ref(span, erase_regions, &impl_expr.r#trait)?;

match self.translate_trait_impl_expr_aux(
span,
Expand All @@ -305,10 +303,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
} else {
let msg = format!("Error during trait resolution: {}", &err.msg);
self.span_err(span, &msg);
Ok(Some(TraitRef {
Ok(TraitRef {
kind: TraitRefKind::Unknown(err.msg),
trait_decl_ref,
}))
})
}
}
}
Expand All @@ -320,7 +318,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
erase_regions: bool,
impl_source: &hax::ImplExpr,
trait_decl_ref: PolyTraitDeclRef,
) -> Result<Option<TraitRef>, Error> {
) -> Result<TraitRef, Error> {
trace!("impl_expr: {:#?}", impl_source);
use hax::ImplExprAtom;

Expand Down Expand Up @@ -378,10 +376,22 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
match path_elem {
AssocItem {
item,
generic_args,
predicate,
index,
predicate_id: _,
..
} => {
if !generic_args.is_empty() {
error_or_panic!(
self,
span,
format!(
"Found unsupported GAT `{}` when resolving trait `{}`",
item.name,
trait_decl_ref.fmt_with_ctx(&self.into_fmt())
)
)
}
trait_id = TraitRefKind::ItemClause(
Box::new(trait_id),
current_trait_decl_id,
Expand All @@ -394,9 +404,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
);
}
Parent {
predicate,
index,
predicate_id: _,
predicate, index, ..
} => {
trait_id = TraitRefKind::ParentClause(
Box::new(trait_id),
Expand Down Expand Up @@ -441,6 +449,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
trait_ref
}
};
Ok(Some(trait_ref))
Ok(trait_ref)
}
}
Loading