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.

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

Update rustc all at once #735

Merged
merged 18 commits into from
Jun 27, 2024
Merged
Show file tree
Hide file tree
Changes from 12 commits
Commits
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
2 changes: 1 addition & 1 deletion cli/driver/src/callbacks_wrapper.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ pub struct CallbacksWrapper<'a> {
impl<'a> Callbacks for CallbacksWrapper<'a> {
fn config(&mut self, config: &mut interface::Config) {
let options = self.options.clone();
config.parse_sess_created = Some(Box::new(move |parse_sess| {
config.psess_created = Some(Box::new(move |parse_sess| {
parse_sess.env_depinfo.get_mut().insert((
Symbol::intern(hax_cli_options::ENV_VAR_OPTIONS_FRONTEND),
Some(Symbol::intern(&serde_json::to_string(&options).unwrap())),
Expand Down
56 changes: 24 additions & 32 deletions cli/driver/src/exporter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,27 +11,26 @@ use rustc_middle::{
thir,
thir::{Block, BlockId, Expr, ExprId, ExprKind, Pat, PatKind, Stmt, StmtId, StmtKind, Thir},
};
use rustc_session::parse::ParseSess;
use rustc_span::symbol::Symbol;
use serde::Serialize;
use std::cell::RefCell;
use std::collections::{HashMap, HashSet};
use std::rc::Rc;

fn report_diagnostics(
tcx: TyCtxt<'_>,
output: &hax_cli_options_engine::Output,
session: &rustc_session::Session,
mapping: &Vec<(hax_frontend_exporter::Span, rustc_span::Span)>,
) {
for d in &output.diagnostics {
use hax_diagnostics::*;
session.span_hax_err(d.convert(mapping).into());
tcx.dcx().span_hax_err(d.convert(mapping).into());
}
}

fn write_files(
tcx: TyCtxt<'_>,
output: &hax_cli_options_engine::Output,
session: &rustc_session::Session,
backend: hax_cli_options::Backend,
) {
let manifest_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap();
Expand All @@ -43,9 +42,9 @@ fn write_files(
for file in output.files.clone() {
let path = out_dir.join(&file.path);
std::fs::create_dir_all(&path.parent().unwrap()).unwrap();
session.note_without_error(format!("Writing file {:#?}", path));
tcx.dcx().note(format!("Writing file {:#?}", path));
std::fs::write(&path, file.contents).unwrap_or_else(|e| {
session.fatal(format!(
tcx.dcx().fatal(format!(
"Unable to write to file {:#?}. Error: {:#?}",
path, e
))
Expand All @@ -55,17 +54,21 @@ fn write_files(

type ThirBundle<'tcx> = (Rc<rustc_middle::thir::Thir<'tcx>>, ExprId);
/// Generates a dummy THIR body with an error literal as first expression
fn dummy_thir_body<'tcx>(tcx: TyCtxt<'tcx>, span: rustc_span::Span) -> ThirBundle<'tcx> {
fn dummy_thir_body<'tcx>(
tcx: TyCtxt<'tcx>,
span: rustc_span::Span,
guar: rustc_errors::ErrorGuaranteed,
) -> ThirBundle<'tcx> {
use rustc_middle::thir::*;
let ty = tcx.mk_ty_from_kind(rustc_type_ir::TyKind::Never);
let mut thir = Thir::new(BodyTy::Const(ty));
const ERR_LITERAL: &'static rustc_hir::Lit = &rustc_span::source_map::Spanned {
node: rustc_ast::ast::LitKind::Err,
let lit_err = tcx.hir_arena.alloc(rustc_span::source_map::Spanned {
node: rustc_ast::ast::LitKind::Err(guar),
span: rustc_span::DUMMY_SP,
};
});
let expr = thir.exprs.push(Expr {
kind: ExprKind::Literal {
lit: ERR_LITERAL,
lit: lit_err,
neg: false,
},
ty,
Expand Down Expand Up @@ -127,24 +130,24 @@ fn precompute_local_thir_bodies<'tcx>(
.filter(|ldid| hir.maybe_body_owned_by(*ldid).is_some())
.map(|ldid| {
tracing::debug!("⏳ Type-checking THIR body for {:#?}", ldid);
let span = hir.span(hir.local_def_id_to_hir_id(ldid));
let span = hir.span(tcx.local_def_id_to_hir_id(ldid));
let (thir, expr) = match tcx.thir_body(ldid) {
Ok(x) => x,
Err(e) => {
tcx.sess.span_err(
let guar = tcx.dcx().span_err(
span,
"While trying to reach a body's THIR defintion, got a typechecking error.",
);
return (ldid, dummy_thir_body(tcx, span));
return (ldid, dummy_thir_body(tcx, span, guar));
}
};
let thir = match std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
thir.borrow().clone()
})) {
Ok(x) => x,
Err(e) => {
tcx.sess.span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
return (ldid, dummy_thir_body(tcx, span));
let guar = tcx.dcx().span_err(span, format!("The THIR body of item {:?} was stolen.\nThis is not supposed to happen.\nThis is a bug in Hax's frontend.\nThis is discussed in issue https://github.com/hacspec/hax/issues/27.\nPlease comment this issue if you see this error message!", ldid));
return (ldid, dummy_thir_body(tcx, span, guar));
}
};
tracing::debug!("✅ Type-checked THIR body for {:#?}", ldid);
Expand Down Expand Up @@ -298,7 +301,7 @@ impl Callbacks for ExtractionCallbacks {
.into_iter()
.map(|(k, v)| {
use hax_frontend_exporter::*;
let sess = compiler.session();
let sess = &compiler.sess;
(
translate_span(k, sess),
translate_span(argument_span_of_mac_call(&v), sess),
Expand Down Expand Up @@ -362,29 +365,19 @@ impl Callbacks for ExtractionCallbacks {
include_extra,
};
mod from {
pub use hax_cli_options::ExportBodyKind::{
MirBuilt as MB, MirConst as MC, Thir as T,
};
pub use hax_cli_options::ExportBodyKind::{MirBuilt as MB, Thir as T};
}
mod to {
pub type T = hax_frontend_exporter::ThirBody;
pub type MB =
hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Built>;
pub type MC =
hax_frontend_exporter::MirBody<hax_frontend_exporter::mir_kinds::Const>;
}
kind.sort();
kind.dedup();
match kind.as_slice() {
[from::MB] => driver.to_json::<to::MB>(),
[from::MC] => driver.to_json::<to::MC>(),
[from::T] => driver.to_json::<to::T>(),
[from::MB, from::MC] => driver.to_json::<(to::MB, to::MC)>(),
[from::T, from::MB] => driver.to_json::<(to::MB, to::T)>(),
[from::T, from::MC] => driver.to_json::<(to::MC, to::T)>(),
[from::T, from::MB, from::MC] => {
driver.to_json::<(to::MB, (to::MC, to::T))>()
}
[] => driver.to_json::<()>(),
_ => panic!("Unsupported kind {:#?}", kind),
}
Expand Down Expand Up @@ -432,9 +425,8 @@ impl Callbacks for ExtractionCallbacks {
.unwrap();

let out = engine_subprocess.wait_with_output().unwrap();
let session = compiler.session();
if !out.status.success() {
session.fatal(format!(
tcx.dcx().fatal(format!(
"{} exited with non-zero code {}\nstdout: {}\n stderr: {}",
ENGINE_BINARY_NAME,
out.status.code().unwrap_or(-1),
Expand All @@ -456,8 +448,8 @@ impl Callbacks for ExtractionCallbacks {
let state =
hax_frontend_exporter::state::State::new(tcx, options_frontend.clone());
report_diagnostics(
tcx,
&output,
&session,
&spans
.into_iter()
.map(|span| (span.sinto(&state), span.clone()))
Expand All @@ -467,7 +459,7 @@ impl Callbacks for ExtractionCallbacks {
serde_json::to_writer(std::io::BufWriter::new(std::io::stdout()), &output)
.unwrap()
} else {
write_files(&output, &session, backend.backend);
write_files(tcx, &output, backend.backend);
}
if let Some(debug_json) = &output.debug_json {
use hax_cli_options::DebugEngineMode;
Expand Down
3 changes: 1 addition & 2 deletions cli/driver/src/linter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,10 @@ impl Callbacks for LinterCallbacks {
compiler: &Compiler,
queries: &'tcx Queries<'tcx>,
) -> Compilation {
let session = compiler.session();
queries
.global_ctxt()
.unwrap()
.enter(|tcx| hax_lint::Linter::register(tcx, session, self.ltype));
.enter(|tcx| hax_lint::Linter::register(tcx, self.ltype));

Compilation::Continue
}
Expand Down
1 change: 0 additions & 1 deletion cli/options/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,6 @@ pub enum ExporterCommand {
pub enum ExportBodyKind {
Thir,
MirBuilt,
MirConst,
}

#[derive(JsonSchema, Subcommand, Debug, Clone, Serialize, Deserialize)]
Expand Down
9 changes: 7 additions & 2 deletions engine/lib/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,14 @@ let show_int_kind { size; signedness } =
|> Option.map ~f:Int.to_string
|> Option.value ~default:"size")

type float_kind = F32 | F64 [@@deriving show, yojson, hash, compare, eq]
type float_kind = F16 | F32 | F64 | F128
[@@deriving show, yojson, hash, compare, eq]

let show_float_kind = function F32 -> "f32" | F64 -> "f64"
let show_float_kind = function
| F16 -> "f16"
| F32 -> "f32"
| F64 -> "f64"
| F128 -> "f128"

type literal =
| String of string
Expand Down
12 changes: 6 additions & 6 deletions engine/lib/concrete_ident/concrete_ident.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@ module Imported = struct
| ForeignMod
| Use
| GlobalAsm
| ClosureExpr
| Closure
| Ctor
| AnonConst
| ImplTrait
| ImplTraitAssocTy
| AnonAdt
| OpaqueTy
| TypeNs of string
| ValueNs of string
| MacroNs of string
Expand All @@ -32,15 +32,15 @@ module Imported = struct
| ForeignMod -> ForeignMod
| Use -> Use
| GlobalAsm -> GlobalAsm
| ClosureExpr -> ClosureExpr
| Closure -> Closure
| Ctor -> Ctor
| AnonConst -> AnonConst
| ImplTrait -> ImplTrait
| ImplTraitAssocTy -> ImplTraitAssocTy
| OpaqueTy -> OpaqueTy
| TypeNs s -> TypeNs s
| ValueNs s -> ValueNs s
| MacroNs s -> MacroNs s
| LifetimeNs s -> LifetimeNs s
| AnonAdt -> AnonAdt

let of_disambiguated_def_path_item :
Types.disambiguated_def_path_item -> disambiguated_def_path_item =
Expand Down
6 changes: 2 additions & 4 deletions engine/lib/generic_printer/generic_printer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
| Float { value; kind; negative } ->
string value
|> precede (if negative then minus else empty)
|> terminate
(string (match kind with F32 -> "f32" | F64 -> "f64"))
|> terminate (string (show_float_kind kind))
| Bool b -> OCaml.bool b

method generic_value : generic_value fn =
Expand Down Expand Up @@ -101,8 +100,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
in
string signedness ^^ size

method ty_float : float_kind fn =
(function F32 -> "f32" | F64 -> "f64") >> string
method ty_float : float_kind fn = show_float_kind >> string

method generic_values : generic_value list fn =
function
Expand Down
Loading
Loading