Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 36 insertions, 27 deletions

diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index a1f6ce33..9fa07029 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -3,6 +3,7 @@
 open Pure
 open PureUtils
 open TranslateCore
+open Errors
 
 (** The local logger *)
 let log = Logging.pure_micro_passes_log
@@ -221,7 +222,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   (* Register a variable for constraints propagation - used when an variable is
    * introduced (left-hand side of a left binding) *)
   let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
-    assert (not (VarId.Map.mem v.id ctx.pure_vars));
+    sanity_check __FILE__ __LINE__
+      (not (VarId.Map.mem v.id ctx.pure_vars))
+      def.meta;
     match v.basename with
     | None -> ctx
     | Some name ->
@@ -610,7 +613,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
         | App _ -> (
             let app, args = destruct_apps e in
             let ignore () =
-              mk_apps
+              mk_apps def.meta
                 (self#visit_texpression env app)
                 (List.map (self#visit_texpression env) args)
             in
@@ -755,7 +758,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
             else if variant_id = result_fail_id then
               (* Fail case *)
               self#visit_expression env rv.e
-            else raise (Failure "Unexpected")
+            else craise __FILE__ __LINE__ def.meta "Unexpected"
         | App _ ->
             (* This might be the tuple case *)
             if not monadic then
@@ -910,7 +913,7 @@ let inline_useless_var_reassignments (ctx : trans_ctx) ~(inline_named : bool)
               } ) ->
             (* Second case: we deconstruct a structure with one field that we will
                extract as tuple. *)
-            let adt_id, _ = PureUtils.ty_as_adt re.ty in
+            let adt_id, _ = PureUtils.ty_as_adt def.meta re.ty in
             (* Update the rhs (we may perform substitutions inside, and it is
              * better to do them *before* we inline it *)
             let re = self#visit_texpression env re in
@@ -1091,7 +1094,7 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
       f y
     ]}
  *)
-let simplify_let_then_return _ctx def =
+let simplify_let_then_return _ctx (def : fun_decl) =
   (* Match a pattern and an expression: evaluates to [true] if the expression
      is actually exactly the pattern *)
   let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool
@@ -1147,7 +1150,7 @@ let simplify_let_then_return _ctx def =
               | Some e ->
                   if match_pattern_and_expr lv e then
                     (* We need to wrap the right-value in a ret *)
-                    (mk_result_return_texpression rv).e
+                    (mk_result_return_texpression def.meta rv).e
                   else not_simpl_e
               | None ->
                   if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1197,13 +1200,14 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 in
                 let fields =
                   match adt_decl.kind with
-                  | Enum _ | Opaque -> raise (Failure "Unreachable")
+                  | Enum _ | Opaque ->
+                      craise __FILE__ __LINE__ def.meta "Unreachable"
                   | Struct fields -> fields
                 in
                 let num_fields = List.length fields in
                 (* In order to simplify, there must be as many arguments as
                  * there are fields *)
-                assert (num_fields > 0);
+                sanity_check __FILE__ __LINE__ (num_fields > 0) def.meta;
                 if num_fields = List.length args then
                   (* We now need to check that all the arguments are of the form:
                    * [x.field] for some variable [x], and where the projection
@@ -1239,10 +1243,11 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     if List.for_all (fun (_, y) -> y = x) end_args then (
                       (* We can substitute *)
                       (* Sanity check: all types correct *)
-                      assert (
-                        List.for_all
-                          (fun (generics1, _) -> generics1 = generics)
-                          args);
+                      sanity_check __FILE__ __LINE__
+                        (List.for_all
+                           (fun (generics1, _) -> generics1 = generics)
+                           args)
+                        def.meta;
                       { e with e = Var x })
                     else super#visit_texpression env e
                   else super#visit_texpression env e
@@ -1397,7 +1402,9 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               { fwd_info; effect_info = loop_fwd_effect_info; ignore_output }
             in
-            assert (fun_sig_info_is_wf loop_fwd_sig_info);
+            sanity_check __FILE__ __LINE__
+              (fun_sig_info_is_wf loop_fwd_sig_info)
+              def.meta;
 
             let inputs_tys =
               let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
@@ -1437,9 +1444,10 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
 
               (* Introduce the forward input state *)
               let fwd_state_var, fwd_state_lvs =
-                assert (
-                  loop_fwd_effect_info.stateful
-                  = Option.is_some loop.input_state);
+                sanity_check __FILE__ __LINE__
+                  (loop_fwd_effect_info.stateful
+                  = Option.is_some loop.input_state)
+                  def.meta;
                 match loop.input_state with
                 | None -> ([], [])
                 | Some input_state ->
@@ -1476,7 +1484,8 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
               match fuel_vars with
               | None -> loop.loop_body
               | Some (fuel0, fuel) ->
-                  SymbolicToPure.wrap_in_match_fuel fuel0 fuel loop.loop_body
+                  SymbolicToPure.wrap_in_match_fuel def.meta fuel0 fuel
+                    loop.loop_body
             in
 
             let loop_body = { inputs; inputs_lvs; body = loop_body } in
@@ -1569,9 +1578,9 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 match aid with
                 | BoxNew ->
                     let arg, args = Collections.List.pop args in
-                    mk_apps arg args
+                    mk_apps def.meta arg args
                 | BoxFree ->
-                    assert (args = []);
+                    sanity_check __FILE__ __LINE__ (args = []) def.meta;
                     mk_unit_rvalue
                 | SliceIndexShared | SliceIndexMut | ArrayIndexShared
                 | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
@@ -1765,8 +1774,8 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               *)
               (* TODO: this information should be computed in SymbolicToPure and
                * store in an enum ("monadic" should be an enum, not a bool). *)
-              let re_ty = Option.get (opt_destruct_result re.ty) in
-              assert (lv.ty = re_ty);
+              let re_ty = Option.get (opt_destruct_result def.meta re.ty) in
+              sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.meta;
               let err_vid = fresh_id () in
               let err_var : var =
                 {
@@ -1778,7 +1787,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
               let err_pat = mk_typed_pattern_from_var err_var None in
               let fail_pat = mk_result_fail_pattern err_pat.value lv.ty in
               let err_v = mk_texpression_from_var err_var in
-              let fail_value = mk_result_fail_texpression err_v e.ty in
+              let fail_value = mk_result_fail_texpression def.meta err_v e.ty in
               let fail_branch = { pat = fail_pat; branch = fail_value } in
               let success_pat = mk_result_return_pattern lv in
               let success_branch = { pat = success_pat; branch = e } in
@@ -2020,7 +2029,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
         ^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
         ^ "\n"));
     let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
-    assert (Option.is_some decl.loop_id);
+    sanity_check __FILE__ __LINE__ (Option.is_some decl.loop_id) decl.meta;
 
     let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
 
@@ -2172,7 +2181,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
           in
 
           let fwd_info = { fwd_info; effect_info; ignore_output } in
-          assert (fun_sig_info_is_wf fwd_info);
+          sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf fwd_info) decl.meta;
           let signature =
             {
               generics;
@@ -2238,17 +2247,17 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
                                 in
 
                                 (* Rebuild *)
-                                mk_apps e_app args)
+                                mk_apps decl.meta e_app args)
                         | _ ->
                             let e_app = self#visit_texpression env e_app in
                             let args =
                               List.map (self#visit_texpression env) args
                             in
-                            mk_apps e_app args)
+                            mk_apps decl.meta e_app args)
                     | _ ->
                         let e_app = self#visit_texpression env e_app in
                         let args = List.map (self#visit_texpression env) args in
-                        mk_apps e_app args)
+                        mk_apps decl.meta e_app args)
                 | _ -> super#visit_texpression env e
             end
           in