Merge pull request #1197 from hacspec/improve-parsers

Engine: get rid of most of exception throwing function calls, improve parsers and error reports

cli/driver/src/exporter.rs

@@ -286,6 +286,7 @@ impl Callbacks for ExtractionCallbacks {
                             .flatten()
                             .collect(),
                         def_ids,
+                        hax_version: hax_types::HAX_VERSION.into(),
                     };
                     haxmeta.write(&mut file, cache_map);
                 }

cli/subcommands/build.rs

@@ -14,7 +14,7 @@ fn rustc_version_env_var() {
 }
 
 fn json_schema_static_asset() {
-    let schema = schemars::schema_for!((
+    let mut schema = schemars::schema_for!((
         hax_frontend_exporter::Item<hax_frontend_exporter::ThirBody>,
         hax_types::cli_options::Options,
         hax_types::diagnostics::Diagnostics,
@@ -25,6 +25,7 @@ fn json_schema_static_asset() {
         hax_types::engine_api::protocol::ToEngine,
         hax_lib_macros_types::AttrPayload,
     ));
+    schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(
         std::fs::File::create(format!("{}/schema.json", std::env::var("OUT_DIR").unwrap()))
             .unwrap(),

cli/subcommands/src/cargo_hax.rs

@@ -240,6 +240,7 @@ fn run_engine(
     message_format: MessageFormat,
 ) -> bool {
     let engine_options = EngineOptions {
+        hax_version: haxmeta.hax_version,
         backend: backend.clone(),
         input: haxmeta.items,
         impl_infos: haxmeta.impl_infos,
@@ -532,6 +533,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, i32) {
     } else {
         0
     };
+
     (haxmeta_files, exit_code)
 }
 

engine/backends/fstar/fstar_backend.ml

@@ -111,6 +111,24 @@ module Make
 struct
   open Ctx
 
+  module StringToFStar = struct
+    let catch_parsing_error (type a b) kind span (f : a -> b) x =
+      try f x
+      with e ->
+        let kind =
+          Types.FStarParseError
+            {
+              fstar_snippet = "";
+              details =
+                "While parsing a " ^ kind ^ ", error: "
+                ^ Base.Error.to_string_hum (Base.Error.of_exn e);
+            }
+        in
+        Error.raise { span; kind }
+
+    let term span = catch_parsing_error "term" span F.term_of_string
+  end
+
   let doc_to_string : PPrint.document -> string =
     FStar_Pprint.pretty_string 1.0 (Z.of_int ctx.line_width)
 
@@ -667,7 +685,7 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote quote -> pquote e.span quote |> F.term_of_string
+    | Quote quote -> pquote e.span quote |> StringToFStar.term e.span
     | _ -> .
 
   (** Prints a `quote` to a string *)

engine/bin/lib.ml

@@ -186,10 +186,25 @@ let parse_options () =
   let table, json =
     Hax_io.read_json () |> Option.value_exn |> parse_id_table_node
   in
+  let version =
+    try Yojson.Safe.Util.(member "hax_version" json |> to_string)
+    with _ -> "unknown"
+  in
+  if String.equal version Types.hax_version |> not then (
+    prerr_endline
+      [%string
+        {|
+The versions of `hax-engine` and of `cargo-hax` are different:
+  - `hax-engine` version: %{Types.hax_version}
+  - `cargo-hax`  version: %{version}
+
+Please reinstall hax.
+|}];
+    Stdlib.exit 1);
   table
   |> List.iter ~f:(fun (id, json) ->
          Hashtbl.add_exn Types.cache_map ~key:id ~data:(`JSON json));
-  let options = Types.parse_engine_options json in
+  let options = [%of_yojson: Types.engine_options] json in
   Profiling.enabled := options.backend.profile;
   options
 

engine/lib/ast_builder.ml

@@ -210,7 +210,8 @@ module Make (F : Features.T) = struct
   end
 
   module type S = module type of Make0 (struct
-    let span = failwith "dummy"
+    (* This [failwith] is OK: this module is never actually used for computation. It is useful only for typing. *)
+    let span = failwith "type only module: this will never be computed"
   end)
 
   module Make (Span : sig

engine/lib/ast_utils.ml

@@ -952,8 +952,11 @@ module Make (F : Features.T) = struct
   module Debug : sig
     val expr : ?label:string -> AST.expr -> unit
     (** Prints an expression pretty-printed as Rust, with its full
-        AST encoded as JSON, available as a file, so that one can
-        `jless` or `jq` into it. *)
+    AST encoded as JSON, available as a file, so that one can
+    `jless` or `jq` into it. *)
+
+    val item' : ?label:string -> AST.item -> string
+    val item : ?label:string -> AST.item -> unit
   end = struct
     let expr ?(label = "") (e : AST.expr) : unit =
       let path = tempfile_path ~suffix:".json" in
@@ -964,6 +967,18 @@ module Make (F : Features.T) = struct
       ^ "\n```\x1b[34m JSON-encoded AST available at \x1b[1m" ^ path
       ^ "\x1b[0m (hint: use `jless " ^ path ^ "`)"
       |> Stdio.prerr_endline
+
+    let item' ?(label = "") (e : AST.item) : string =
+      let path = tempfile_path ~suffix:".json" in
+      Core.Out_channel.write_all path
+        ~data:([%yojson_of: AST.item] e |> Yojson.Safe.pretty_to_string);
+      let e = LiftToFullAst.item e in
+      "```rust " ^ label ^ "\n" ^ Print_rust.pitem_str e
+      ^ "\n```\x1b[34m JSON-encoded AST available at \x1b[1m" ^ path
+      ^ "\x1b[0m (hint: use `jless " ^ path ^ "`)"
+
+    let item ?(label = "") (e : AST.item) =
+      item' ~label e |> Stdio.prerr_endline
   end
 
   let unbox_expr' (next : expr -> expr) (e : expr) : expr =

engine/lib/attr_payloads.ml

@@ -6,7 +6,18 @@ let payloads : attrs -> (Types.ha_payload * span) list =
   let parse =
     (* we have to parse ["JSON"]: first a string, then a ha_payload *)
     function
-    | `String s -> Yojson.Safe.from_string s |> Types.parse_ha_payload
+    | `String s -> (
+        match Yojson.Safe.from_string s |> Types.safe_ha_payload_of_yojson with
+        | Error _ ->
+            Stdlib.prerr_endline
+              [%string
+                {|
+The hax engine could not parse a hax attribute.
+This means that the crate being extracted and the version of hax engine are incompatible.
+Please make sure the `hax-lib` dependency of the extracted crate matches hax-engine's version (%{Types.hax_version}).
+|}];
+            Stdlib.exit 1
+        | Ok value -> value)
     | x ->
         Stdlib.failwith
         @@ "Attr_payloads: payloads: expected a string while parsing JSON, got "
@@ -23,7 +34,7 @@ let payloads : attrs -> (Types.ha_payload * span) list =
 (** Create a attribute out of a [payload] *)
 let to_attr (payload : Types.ha_payload) (span : span) : attr =
   let json =
-    `String (Yojson.Safe.to_string (Types.to_json_ha_payload payload))
+    `String (Yojson.Safe.to_string ([%yojson_of: Types.ha_payload] payload))
   in
   let kind : attr_kind =
     Tool { path = "_hax::json"; tokens = Yojson.Safe.to_string json }

engine/lib/dependencies.ml

@@ -465,9 +465,19 @@ module Make (F : Features.T) = struct
                ])
       in
       let renamings =
-        Map.of_alist_exn
-          (module Concrete_ident)
-          (renamings @ variant_and_constructors_renamings)
+        match
+          Map.of_alist
+            (module Concrete_ident)
+            (renamings @ variant_and_constructors_renamings)
+        with
+        | `Duplicate_key dup ->
+            failwith
+              [%string
+                "Fatal error: in dependency analysis, we construct a renaming \
+                 key-value list with a guarantee of unicity in keys. However, \
+                 we found the following key twice:\n\
+                 %{[%show: concrete_ident] dup}"]
+        | `Ok value -> value
       in
       let rename =
         let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in
@@ -493,7 +503,15 @@ module Make (F : Features.T) = struct
       include Comparable.Make (T)
     end in
     let bundle_of_item =
-      Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms
+      match Hashtbl.of_alist (module ComparableItem) bundle_transforms with
+      | `Duplicate_key dup ->
+          failwith
+            [%string
+              "Fatal error: in dependency analysis, [bundles_transforms] is \
+               expected to be a key-value list with a guarantee of unicity in \
+               keys. However, we found the following key (an item) twice:\n\
+               %{U.Debug.item' dup}"]
+      | `Ok value -> value
     in
     let maybe_transform_item item =
       match Hashtbl.find bundle_of_item item with

engine/lib/hax_io.ml

@@ -36,10 +36,10 @@ include (
     end)
 
 let read () : Types.to_engine =
-  read_json () |> Option.value_exn |> Types.parse_to_engine
+  read_json () |> Option.value_exn |> [%of_yojson: Types.to_engine]
 
 let write (msg : Types.from_engine) : unit =
-  Types.to_json_from_engine msg |> write_json
+  [%yojson_of: Types.from_engine] msg |> write_json
 
 let close () : unit =
   write Exit;

engine/lib/import_thir.ml

@@ -24,7 +24,7 @@ let unimplemented ~issue_id (span : Thir.span list) (details : string) =
   let kind =
     T.Unimplemented
       {
-        issue_id = Some (MyInt64.of_int_exn issue_id);
+        issue_id = Some (MyInt64.of_int issue_id);
         details = String.(if details = "" then None else Some details);
       }
   in
@@ -676,7 +676,12 @@ end) : EXPR = struct
           LocalVar
             {
               name = id.name;
-              id = Local_ident.mk_id Cnst (MyInt64.to_int_exn id.index);
+              id =
+                Local_ident.mk_id Cnst
+                  (MyInt64.to_int id.index
+                  |> Option.value_or_thunk ~default:(fun _ ->
+                         assertion_failure [ e.span ]
+                           "Expected const id to fit in an OCaml native int"));
             }
       | Repeat { value; count } ->
           let value = c_expr value in
@@ -1038,7 +1043,16 @@ end) : EXPR = struct
         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) }
+        TParam
+          {
+            name;
+            id =
+              Local_ident.mk_id Typ
+                (MyInt64.to_int index
+                |> Option.value_or_thunk ~default:(fun _ ->
+                       assertion_failure [ span ]
+                         "Expected param id to fit in an OCaml native int"));
+          }
     | Error ->
         assertion_failure [ span ]
           "got type `Error`: Rust compilation probably failed."
@@ -1172,7 +1186,11 @@ end) : EXPR = struct
     {
       typ_span = Option.map ~f:Span.of_thir param.ty_span;
       typ = c_ty (Option.value ~default:span param.ty_span) param.ty;
-      pat = c_pat (Option.value_exn param.pat);
+      pat =
+        c_pat
+          (Option.value_or_thunk param.pat ~default:(fun _ ->
+               assertion_failure [ span ]
+                 "c_param: expected param.pat to be non-empty"));
       attrs = c_attrs param.attributes;
     }
 
@@ -1492,14 +1510,17 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
        |> not
   in
   let c_body = if drop_body then c_expr_drop_body else c_expr in
+  let assert_item_def_id () =
+    Option.value_or_thunk item.def_id ~default:(fun _ ->
+        assertion_failure [ item.span ] "Expected this item to have a `def_id`")
+  in
   (* TODO: things might be unnamed (e.g. constants) *)
   match (item.kind : Thir.item_kind) with
   | Const (_, generics, body) ->
       mk
       @@ Fn
            {
-             name =
-               Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
+             name = Concrete_ident.of_def_id Value (assert_item_def_id ());
              generics = c_generics generics;
              body = c_body body;
              params = [];
@@ -1509,16 +1530,15 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       mk
       @@ TyAlias
            {
-             name = Concrete_ident.of_def_id Type (Option.value_exn item.def_id);
+             name = Concrete_ident.of_def_id Type (assert_item_def_id ());
              generics = c_generics generics;
              ty = c_ty item.span ty;
            }
   | Fn (generics, { body; params; header = { safety; _ }; _ }) ->
       mk
       @@ Fn
            {
-             name =
-               Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
+             name = Concrete_ident.of_def_id Value (assert_item_def_id ());
              generics = c_generics generics;
              body = c_body body;
              params = c_fn_params item.span params;
@@ -1527,11 +1547,11 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   | (Enum (_, generics, _) | Struct (_, generics)) when erased ->
       let generics = c_generics generics in
       let is_struct = match item.kind with Struct _ -> true | _ -> false in
-      let def_id = Option.value_exn item.def_id in
+      let def_id = assert_item_def_id () in
       let name = Concrete_ident.of_def_id Type def_id in
       mk @@ Type { name; generics; variants = []; is_struct }
   | Enum (variants, generics, repr) ->
-      let def_id = Option.value_exn item.def_id in
+      let def_id = assert_item_def_id () in
       let generics = c_generics generics in
       let is_struct = false in
       let kind = Concrete_ident.Kind.Constructor { is_struct } in
@@ -1591,7 +1611,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
       if is_primitive then cast_fun :: result else result
   | Struct (v, generics) ->
       let generics = c_generics generics in
-      let def_id = Option.value_exn item.def_id in
+      let def_id = assert_item_def_id () in
       let is_struct = true in
       (* repeating the attributes of the item in the variant: TODO is that ok? *)
       let v =
@@ -1632,9 +1652,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
           ~f:(fun { attributes; _ } -> not (should_skip attributes))
           items
       in
-      let name =
-        Concrete_ident.of_def_id Trait (Option.value_exn item.def_id)
-      in
+      let name = Concrete_ident.of_def_id Trait (assert_item_def_id ()) in
       let { params; constraints } = c_generics generics in
       let self =
         let id = Local_ident.mk_id Typ 0 (* todo *) in

engine/lib/phases/phase_cf_into_monads.ml

@@ -171,18 +171,19 @@ struct
               arms
           in
           let arms =
-            if List.is_empty arms then []
-            else
-              let m =
-                List.map ~f:(fun ({ monad; _ }, _) -> monad) arms
-                |> List.reduce_exn ~f:(KnownMonads.lub span)
-              in
-              List.map
-                ~f:(fun (mself, (arm_pat, span, body, guard)) ->
-                  let body = KnownMonads.lift "Match" body mself.monad m in
-                  let arm_pat = { arm_pat with typ = body.typ } in
-                  ({ arm = { arm_pat; body; guard }; span } : B.arm))
-                arms
+            let m =
+              List.map ~f:(fun ({ monad; _ }, _) -> monad) arms
+              |> List.reduce ~f:(KnownMonads.lub span)
+            in
+            match m with
+            | None -> [] (* [arms] is empty *)
+            | Some m ->
+                List.map
+                  ~f:(fun (mself, (arm_pat, span, body, guard)) ->
+                    let body = KnownMonads.lift "Match" body mself.monad m in
+                    let arm_pat = { arm_pat with typ = body.typ } in
+                    ({ arm = { arm_pat; body; guard }; span } : B.arm))
+                  arms
           in
           let typ =
             match arms with [] -> UB.never_typ | hd :: _ -> hd.arm.body.typ

engine/lib/phases/phase_hoist_disjunctive_patterns.ml

@@ -72,6 +72,7 @@ module Make (F : Features.T) =
                   List.map (treat_args [ [] ] fields_as_pat)
                     ~f:(fun fields_as_pat ->
                       let fields =
+                        (* exn justification: `rev_map fields` and `fields` have the same length *)
                         List.map2_exn fields_as_pat fields
                           ~f:(fun pat { field; _ } -> { field; pat })
                       in