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 9 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
31 changes: 19 additions & 12 deletions engine/lib/import_thir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,9 +82,10 @@ let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function
| Fake -> unimplemented [ span ] "Shallow borrows"
| Mut _ -> Mut W.mutable_reference

let c_binding_mode span : Thir.binding_mode -> binding_mode = function
| ByValue -> ByValue
| ByRef k -> ByRef (c_borrow_kind span k, W.reference)
let c_binding_mode : Thir.by_ref -> binding_mode = function
| No -> ByValue
| Yes true -> ByRef (Mut W.mutable_reference, W.reference)
| Yes false -> ByRef (Shared, W.reference)

let unit_typ : ty = TApp { ident = `TupleType 0; args = [] }

Expand Down Expand Up @@ -161,7 +162,7 @@ let c_lit' span negative (lit : Thir.lit_kind) (ty : ty) : extended_literal =
^ "] instead.")
in
match lit with
| Err ->
| Err _ ->
assertion_failure [ span ]
"[import_thir:literal] got an error literal: this means the Rust \
compiler or Hax's frontend probably reported errors above."
Expand Down Expand Up @@ -800,13 +801,13 @@ end) : EXPR = struct
let typ, typ_span = c_canonical_user_type_annotation annotation in
let pat = c_pat subpattern in
PAscription { typ; typ_span; pat }
| Binding { mode; mutability; subpattern; ty; var; _ } ->
let mut = c_mutability W.mutable_variable mutability in
| Binding { mode; subpattern; ty; var; _ } ->
let mut = c_mutability W.mutable_variable mode.mutability in
let subpat =
Option.map ~f:(c_pat &&& Fn.const W.as_pattern) subpattern
in
let typ = c_ty pat.span ty in
let mode = c_binding_mode pat.span mode in
let mode = c_binding_mode mode.by_ref in
let var = local_ident Expr var in
PBinding { mut; mode; var; typ; subpat }
| Variant { info; subpatterns; _ } ->
Expand Down Expand Up @@ -844,6 +845,8 @@ end) : EXPR = struct
| Or { pats } -> POr { subpats = List.map ~f:c_pat pats }
| Slice _ -> unimplemented [ pat.span ] "pat Slice"
| Range _ -> unimplemented [ pat.span ] "pat Range"
| DerefPattern _ -> unimplemented [ pat.span ] "pat DerefPattern"
| Never -> unimplemented [ pat.span ] "pat Never"
| Error _ -> unimplemented [ pat.span ] "pat Error"
in
{ p = v; span; typ }
Expand Down Expand Up @@ -917,7 +920,9 @@ end) : EXPR = struct
| Char -> TChar
| Int k -> TInt (c_int_ty k)
| Uint k -> TInt (c_uint_ty k)
| Float k -> TFloat (match k with F32 -> F32 | F64 -> F64)
| Float k ->
TFloat
(match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
| Arrow value ->
let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in
let inputs =
Expand Down Expand Up @@ -1359,19 +1364,21 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
List.for_all
~f:(fun { data; _ } ->
match data with
| Unit _ | Tuple ([], _, _) | Struct ([], _) -> true
| Unit _ | Tuple ([], _, _) | Struct { fields = []; _ } -> true
| _ -> false)
variants
in
let variants =
List.map
~f:
(fun ({ data; def_id = variant_id; attributes; _ } as original) ->
let is_record = [%matches? Types.Struct (_ :: _, _)] data in
let is_record =
[%matches? Types.Struct { fields = _ :: _; _ }] data
in
let name = Concrete_ident.of_def_id kind variant_id in
let arguments =
match data with
| Tuple (fields, _, _) | Struct (fields, _) ->
| Tuple (fields, _, _) | Struct { fields; _ } ->
List.map
~f:(fun { def_id = id; ty; span; attributes; _ } ->
( Concrete_ident.of_def_id Field id,
Expand Down Expand Up @@ -1415,7 +1422,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
in
match v with
| Tuple (fields, _, _) -> mk fields false
| Struct ((_ :: _ as fields), _) -> mk fields true
| Struct { fields = _ :: _ as fields; _ } -> mk fields true
| _ -> { name; arguments = []; is_record = false; attrs }
in
let variants = [ v ] in
Expand Down
6 changes: 2 additions & 4 deletions engine/lib/print_rust.ml
Original file line number Diff line number Diff line change
Expand Up @@ -76,10 +76,8 @@ module Raw = struct
| String s -> "\"" ^ String.escaped s ^ "\""
| Char c -> "'" ^ Char.to_string c ^ "'"
| Int { value; _ } -> value
| Float { value; kind = F32; negative } ->
pnegative negative ^ value ^ "f32"
| Float { value; kind = F64; negative } ->
pnegative negative ^ value ^ "f64"
| Float { value; kind; negative } ->
pnegative negative ^ value ^ show_float_kind kind
| Bool b -> Bool.to_string b

let pprimitive_ident span : _ -> AnnotatedString.t =
Expand Down
7 changes: 3 additions & 4 deletions engine/names/extract/build.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
use serde_json;
use serde_json::Value;
use std::process::{Command, Stdio};

Expand Down Expand Up @@ -46,11 +45,11 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
DefPathItem::ForeignMod => "ForeignMod".into(),
DefPathItem::Use => "Use".into(),
DefPathItem::GlobalAsm => "GlobalAsm".into(),
DefPathItem::ClosureExpr => "ClosureExpr".into(),
DefPathItem::Closure => "Closure".into(),
DefPathItem::Ctor => "Ctor".into(),
DefPathItem::AnonConst => "AnonConst".into(),
DefPathItem::ImplTrait => "ImplTrait".into(),
DefPathItem::ImplTraitAssocTy => "ImplTraitAssocTy".into(),
DefPathItem::OpaqueTy => "OpaqueTy".into(),
DefPathItem::AnonAdt => "AnonAdt".into(),
}
}

Expand Down
Loading
Loading