Skip to content
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