Merge pull request #934 from hacspec/tag-error-with-issue-id-everywhere

chore: assign an issue id for every error in the engine
hacspec · Sep 30, 2024 · 39a2f0a · 39a2f0a
2 parents 4f0576e + 8f613fe
commit 39a2f0a
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 11 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -156,7 +156,8 @@ struct
             Some
               ( (match signedness with Signed -> Signed | Unsigned -> Unsigned),
                 size ) )
-    | Float _ -> Error.unimplemented ~details:"pliteral: Float" span
+    | Float _ ->
+        Error.unimplemented ~issue_id:230 ~details:"pliteral: Float" span
     | Bool b -> F.Const.Const_bool b
 
   let pliteral_as_expr span (e : literal) =
@@ -302,7 +303,7 @@ struct
         F.mk_e_app base args
     | TArrow (inputs, output) ->
         F.mk_e_arrow (List.map ~f:(pty span) inputs) (pty span output)
-    | TFloat _ -> Error.unimplemented ~details:"pty: Float" span
+    | TFloat _ -> Error.unimplemented ~issue_id:230 ~details:"pty: Float" span
     | TArray { typ; length } ->
         F.mk_e_app (F.term_of_lid [ "t_Array" ]) [ pty span typ; pexpr length ]
     | TParam i -> F.term @@ F.AST.Var (F.lid_of_id @@ plocal_ident i)
@@ -398,7 +399,7 @@ struct
     | POr { subpats } when shallow ->
         F.pat @@ F.AST.PatOr (List.map ~f:ppat subpats)
     | POr _ ->
-        Error.unimplemented p.span ~issue_id:463
+        Error.unimplemented ~issue_id:463 p.span
           ~details:"The F* backend doesn't support nested disjuntive patterns"
     | PArray { args } -> F.pat @@ F.AST.PatList (List.map ~f:ppat args)
     | PConstruct { name = `TupleCons 0; args = [] } ->

diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
@@ -291,7 +291,7 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
                         ^ "\n - free_variables: "
                         ^ [%show: string list] free_variables
                       in
-                      Error.unimplemented ~details span)
+                      Error.assertion_failure span details)
              in
              let v =
                U.Mappers.rename_local_idents (fun i ->

diff --git a/engine/lib/phases/phase_and_mut_defsite.ml b/engine/lib/phases/phase_and_mut_defsite.ml
@@ -59,9 +59,8 @@ struct
             in
             Some (var, typ, param.pat.span)
         | _ ->
-            (* TODO: nicer error! other pats are rejected, not unimplem! *)
-            Error.unimplemented
-              ~details:"Non-binding patterns for `&mut` inputs" param.pat.span
+            Error.raise
+              { kind = NonTrivialAndMutFnInput; span = param.pat.span }
 
       let rewrite_fn_sig (all_vars : local_ident list) (params : param list)
           (output : ty) :

diff --git a/engine/lib/phases/phase_functionalize_loops.ml b/engine/lib/phases/phase_functionalize_loops.ml
@@ -222,12 +222,12 @@ struct
           UB.call ~kind:(AssociatedItem Value) Rust_primitives__hax__while_loop
             [ condition; init; body ] span (dty span expr.typ)
       | Loop { state = None; _ } ->
-          Error.unimplemented ~details:"Loop without mutation?" span
+          Error.unimplemented ~issue_id:405 ~details:"Loop without mutation"
+            span
       | Loop _ ->
-          Error.unimplemented
-            ~details:"Only for loop are being functionalized for now" span
+          Error.unimplemented ~issue_id:933 ~details:"Unhandled loop kind" span
       | Break _ ->
-          Error.unimplemented
+          Error.unimplemented ~issue_id:15
             ~details:
               "For now, the AST node [Break] is feature gated only by [loop], \
                there is nothing for having loops but no breaks."

diff --git a/hax-types/src/diagnostics/mod.rs b/hax-types/src/diagnostics/mod.rs
@@ -64,6 +64,9 @@ impl std::fmt::Display for Diagnostics {
             Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
 
             Kind::AttributeRejected {reason} => write!(f, "Here, this attribute cannot be used: {reason}."),
+
+            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited. Onlu trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
+
             _ => write!(f, "{:?}", self.kind),
         }
     }
@@ -125,6 +128,9 @@ pub enum Kind {
 
     ExpectedMutRef = 10,
 
+    /// &mut inputs should be trivial patterns
+    NonTrivialAndMutFnInput = 11,
+
     /// An hax attribute (from `hax-lib-macros`) was rejected
     AttributeRejected {
         reason: String,