Skip to content

Commit

Permalink
Merge pull request #932 from hacspec/tag-error-with-issue-id-import_thir
Browse files Browse the repository at this point in the history 
chore: assign an issue for every error in `import_thir`
  • Loading branch information
@maximebuyse
maximebuyse authored Sep 30, 2024
2 parents c754fef + dfe5433 commit 4f0576e
Showing 1 changed file with 69 additions and 34 deletions.
103 changes: 69 additions & 34 deletions engine/lib/import_thir.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ let assertion_failure (span : Thir.span list) (details : string) =
let kind = T.AssertionFailure { details } in
Diagnostics.SpanFreeError.raise ~span ThirImport kind

let unimplemented ?issue_id (span : Thir.span list) (details : string) =
let unimplemented ~issue_id (span : Thir.span list) (details : string) =
let kind =
T.Unimplemented
{
issue_id = Option.map ~f:MyInt64.of_int_exn issue_id;
issue_id = Some (MyInt64.of_int_exn issue_id);
details = String.(if details = "" then None else Some details);
}
in
Expand Down Expand Up @@ -78,7 +78,11 @@ let c_mutability (witness : 'a) : bool -> 'a Ast.mutability = function

let c_borrow_kind span : Thir.borrow_kind -> borrow_kind = function
| Shared -> Shared
| Fake _ -> unimplemented [ span ] "Shallow borrows"
| Fake _ ->
assertion_failure [ span ]
"Got a shallow borrow node (`BorrowKind::Fake`). Those are generated \
by the borrow checker and should be discarded after borrow checking: \
we should never see such borrows."
| Mut _ -> Mut W.mutable_reference

let c_binding_mode : Thir.by_ref -> binding_mode = function
Expand Down Expand Up @@ -586,7 +590,9 @@ end) : EXPR = struct
let scrutinee = c_expr scrutinee in
let arms = List.map ~f:c_arm arms in
Match { scrutinee; arms }
| Let _ -> unimplemented [ e.span ] "Let"
| Let _ ->
assertion_failure [ e.span ]
"`Let` nodes are supposed to be pre-processed"
| Block { expr; span; stmts; safety_mode; _ } ->
let { e; _ } = c_block ~expr ~span ~stmts ~ty:e.ty ~safety_mode in
e
Expand Down Expand Up @@ -655,7 +661,7 @@ end) : EXPR = struct
let e = Option.map ~f:c_expr value in
let e = Option.value ~default:(unit_expr span) e in
Return { e; witness = W.early_exit }
| ConstBlock _ -> unimplemented [ e.span ] "ConstBlock"
| ConstBlock _ -> unimplemented ~issue_id:923 [ e.span ] "ConstBlock"
| ConstParam { param = id; _ } (* TODO: shadowing? *) | ConstRef { id } ->
LocalVar
{
Expand Down Expand Up @@ -735,11 +741,19 @@ end) : EXPR = struct
[ lhs; index ]
| StaticRef { def_id = id; _ } -> GlobalVar (def_id Value id)
| PlaceTypeAscription _ ->
unimplemented [ e.span ] "expression PlaceTypeAscription"
assertion_failure [ e.span ]
"Got a unexpected node `PlaceTypeAscription`. Please report, we \
were not able to figure out an expression yielding that node: a \
bug report would be very valuable here!"
| ValueTypeAscription { source; _ } -> (c_expr source).e
| ZstLiteral _ -> unimplemented [ e.span ] "expression ZstLiteral"
| Yield _ -> unimplemented [ e.span ] "expression Yield"
| Todo payload -> unimplemented [ e.span ] ("expression Todo\n" ^ payload)
| ZstLiteral _ ->
assertion_failure [ e.span ]
"`ZstLiteral` are expected to be handled before-hand"
| Yield _ ->
unimplemented ~issue_id:924 [ e.span ]
"Got expression `Yield`: coroutines are not supported by hax"
| Todo payload ->
assertion_failure [ e.span ] ("expression Todo\n" ^ payload)
in
{ e = v; span; typ }

Expand Down Expand Up @@ -807,10 +821,10 @@ end) : EXPR = struct
Borrow { arg = constant_expr_to_expr arg; borrow_kind = Thir.Shared }
| ConstRef { id } -> ConstRef { id }
| MutPtr _ | TraitConst _ | FnPtr _ ->
unimplemented [ span ]
assertion_failure [ span ]
"constant_lit_to_lit: TraitConst | FnPtr | MutPtr"
| Todo _ -> unimplemented [ span ] "ConstantExpr::Todo"
and constant_lit_to_lit (l : Thir.constant_literal) span :
| Todo _ -> assertion_failure [ span ] "ConstantExpr::Todo"
and constant_lit_to_lit (l : Thir.constant_literal) _span :
Thir.lit_kind * bool =
match l with
| Bool v -> (Bool v, false)
Expand All @@ -820,7 +834,10 @@ end) : EXPR = struct
| Some v -> (Int (v, Signed ty), true)
| None -> (Int (v, Signed ty), false))
| Int (Uint (v, ty)) -> (Int (v, Unsigned ty), false)
| Float _ -> unimplemented [ span ] "constant_lit_to_lit: Float"
| Float (v, ty) -> (
match String.chop_prefix v ~prefix:"-" with
| Some v -> (Float (v, Suffixed ty), true)
| None -> (Float (v, Suffixed ty), false))
| Str (v, style) -> (Str (v, style), false)
| ByteStr (v, style) -> (ByteStr (v, style), false)
and constant_field_expr ({ field; value } : Thir.constant_field_expr) :
Expand Down Expand Up @@ -879,13 +896,17 @@ end) : EXPR = struct
in
(c_constant_expr value |> pat_of_expr).p
| InlineConstant { subpattern; _ } -> (c_pat subpattern).p
| Array _ -> unimplemented [ pat.span ] "Pat:Array"
| Array _ -> unimplemented ~issue_id:804 [ pat.span ] "Pat:Array"
| 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"
| Slice _ -> unimplemented ~issue_id:804 [ pat.span ] "pat Slice"
| Range _ -> unimplemented ~issue_id:925 [ pat.span ] "pat Range"
| DerefPattern _ ->
unimplemented ~issue_id:926 [ pat.span ] "pat DerefPattern"
| Never -> unimplemented ~issue_id:927 [ pat.span ] "pat Never"
| Error _ ->
assertion_failure [ pat.span ]
"`Error` node: Rust compilation failed. If Rust compilation was \
fine, please file an issue."
in
{ p = v; span; typ }

Expand Down Expand Up @@ -949,7 +970,7 @@ end) : EXPR = struct
(* ^ "]\n\nThe expression is: " *)
(* ^ [%show: expr] source)) *)
| _ ->
unimplemented [ e.span ]
assertion_failure [ e.span ]
("Pointer, with [cast] being " ^ [%show: Thir.pointer_coercion] cast)

and c_ty (span : Thir.span) (ty : Thir.ty) : ty =
Expand All @@ -972,7 +993,7 @@ end) : EXPR = struct
let ident = def_id Type id in
let args = List.map ~f:(c_generic_value span) generic_args in
TApp { ident; args }
| Foreign _ -> unimplemented [ span ] "Foreign"
| Foreign _ -> unimplemented ~issue_id:928 [ span ] "Foreign"
| Str -> TStr
| Array (ty, len) ->
TArray { typ = c_ty span ty; length = c_constant_expr len }
Expand All @@ -995,12 +1016,15 @@ end) : EXPR = struct
| Alias { kind = Opaque; def_id; _ } ->
TOpaque (Concrete_ident.of_def_id Type def_id)
| Alias { kind = Inherent; _ } ->
unimplemented [ span ] "type Alias::Inherent"
| Alias { kind = Weak; _ } -> unimplemented [ span ] "type Alias::Weak"
assertion_failure [ span ] "Ty::Alias with AliasTyKind::Inherent"
| Alias { kind = Weak; _ } ->
assertion_failure [ span ] "Ty::Alias with AliasTyKind::Weak"
| Param { index; name } ->
(* TODO: [id] might not unique *)
TParam { name; id = Local_ident.mk_id Typ (MyInt64.to_int_exn index) }
| Error -> unimplemented [ span ] "type Error"
| Error ->
assertion_failure [ span ]
"got type `Error`: Rust compilation probably failed."
| Dynamic (predicates, _region, Dyn) -> (
let goals, non_traits =
List.partition_map
Expand All @@ -1019,13 +1043,22 @@ end) : EXPR = struct
in
match non_traits with
| [] -> TDyn { witness = W.dyn; goals }
| _ -> unimplemented [ span ] "type Dyn with non trait predicate")
| Dynamic (_, _, DynStar) -> unimplemented [ span ] "type DynStar"
| Coroutine _ -> unimplemented [ span ] "type Coroutine"
| Placeholder _ -> unimplemented [ span ] "type Placeholder"
| Bound _ -> unimplemented [ span ] "type Bound"
| Infer _ -> unimplemented [ span ] "type Infer"
| Todo _ -> unimplemented [ span ] "type Todo"
| _ -> assertion_failure [ span ] "type Dyn with non trait predicate")
| Dynamic (_, _, DynStar) ->
unimplemented ~issue_id:931 [ span ] "type DynStar"
| Coroutine _ ->
unimplemented ~issue_id:924 [ span ]
"Got type `Coroutine`: coroutines are not supported by hax"
| Placeholder _ ->
assertion_failure [ span ]
"type Placeholder: should be gone after typechecking"
| Bound _ ->
assertion_failure [ span ]
"type Bound: should be gone after typechecking"
| Infer _ ->
assertion_failure [ span ]
"type Infer: should be gone after typechecking"
| Todo _ -> assertion_failure [ span ] "type Todo"
(* fun _ -> Ok Bool *)

and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
Expand Down Expand Up @@ -1231,8 +1264,9 @@ end) : EXPR = struct
in
TIType bounds
| Type (_, Some _) ->
unimplemented [ span ]
"TODO: traits: no support for defaults in type for now"
unimplemented ~issue_id:929 [ span ]
"Associated types defaults are not supported by hax yet (it is a \
nightly feature)"
end

include struct
Expand Down Expand Up @@ -1565,7 +1599,8 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
let items = List.map ~f:c_trait_item items in
let safety = csafety safety in
mk @@ Trait { name; generics; items; safety }
| Trait (Yes, _, _, _, _) -> unimplemented [ item.span ] "Auto trait"
| Trait (Yes, _, _, _, _) ->
unimplemented ~issue_id:930 [ item.span ] "Auto trait"
| Impl { of_trait = None; generics; items; _ } ->
let items =
List.filter
Expand Down

0 comments on commit 4f0576e

Please sign in to comment.