Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 29 insertions, 22 deletions

diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index ad34c48e..576b2809 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -4,23 +4,28 @@ open Expressions
 open Values
 open LlbcAst
 open SymbolicAst
+open Errors
 
-let mk_mplace (p : place) (ctx : Contexts.eval_ctx) : mplace =
-  let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in
+let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace
+    =
+  let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in
   { bv; projection = p.projection }
 
-let mk_opt_mplace (p : place option) (ctx : Contexts.eval_ctx) : mplace option =
-  Option.map (fun p -> mk_mplace p ctx) p
+let mk_opt_mplace (meta : Meta.meta) (p : place option)
+    (ctx : Contexts.eval_ctx) : mplace option =
+  Option.map (fun p -> mk_mplace meta p ctx) p
 
-let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) :
-    mplace option =
-  match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None
+let mk_opt_place_from_op (meta : Meta.meta) (op : operand)
+    (ctx : Contexts.eval_ctx) : mplace option =
+  match op with
+  | Copy p | Move p -> Some (mk_mplace meta p ctx)
+  | Constant _ -> None
 
 let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e)
 
-let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
-    (seel : symbolic_expansion option list) (el : expression list option) :
-    expression option =
+let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value)
+    (place : mplace option) (seel : symbolic_expansion option list)
+    (el : expression list option) : expression option =
   match el with
   | None -> None
   | Some el ->
@@ -36,7 +41,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
              (Some (SeLiteral (VBool false)), false_exp);
             ] ->
                 ExpandBool (true_exp, false_exp)
-            | _ -> raise (Failure "Ill-formed boolean expansion"))
+            | _ -> craise __FILE__ __LINE__ meta "Ill-formed boolean expansion")
         | TLiteral (TInteger int_ty) ->
             (* Switch over an integer: split between the "regular" branches
                and the "otherwise" branch (which should be the last branch) *)
@@ -46,9 +51,9 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             let get_scalar (see : symbolic_expansion option) : scalar_value =
               match see with
               | Some (SeLiteral (VScalar cv)) ->
-                  assert (cv.int_ty = int_ty);
+                  sanity_check __FILE__ __LINE__ (cv.int_ty = int_ty) meta;
                   cv
-              | _ -> raise (Failure "Unreachable")
+              | _ -> craise __FILE__ __LINE__ meta "Unreachable"
             in
             let branches =
               List.map (fun (see, exp) -> (get_scalar see, exp)) branches
@@ -56,7 +61,7 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             (* For the otherwise branch, the symbolic value should have been left
              * unchanged *)
             let otherwise_see, otherwise = otherwise in
-            assert (otherwise_see = None);
+            sanity_check __FILE__ __LINE__ (otherwise_see = None) meta;
             (* Return *)
             ExpandInt (int_ty, branches, otherwise)
         | TAdt (_, _) ->
@@ -65,7 +70,9 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
                 VariantId.id option * symbolic_value list =
               match see with
               | Some (SeAdt (vid, fields)) -> (vid, fields)
-              | _ -> raise (Failure "Ill-formed branching ADT expansion")
+              | _ ->
+                  craise __FILE__ __LINE__ meta
+                    "Ill-formed branching ADT expansion"
             in
             let exp =
               List.map
@@ -79,18 +86,18 @@ let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
             (* Reference expansion: there should be one branch *)
             match ls with
             | [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
-            | _ -> raise (Failure "Ill-formed borrow expansion"))
+            | _ -> craise __FILE__ __LINE__ meta "Ill-formed borrow expansion")
         | TVar _ | TLiteral TChar | TNever | TTraitType _ | TArrow _ | TRawPtr _
           ->
-            raise (Failure "Ill-formed symbolic expansion")
+            craise __FILE__ __LINE__ meta "Ill-formed symbolic expansion"
       in
       Some (Expansion (place, sv, expansion))
 
-let synthesize_symbolic_expansion_no_branching (sv : symbolic_value)
-    (place : mplace option) (see : symbolic_expansion) (e : expression option) :
-    expression option =
+let synthesize_symbolic_expansion_no_branching (meta : Meta.meta)
+    (sv : symbolic_value) (place : mplace option) (see : symbolic_expansion)
+    (e : expression option) : expression option =
   let el = Option.map (fun e -> [ e ]) e in
-  synthesize_symbolic_expansion sv place [ Some see ] el
+  synthesize_symbolic_expansion meta sv place [ Some see ] el
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
     (sg : fun_sig option) (regions_hierarchy : region_var_groups)
@@ -188,7 +195,7 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
              loop_expr;
              meta;
            })
-  | _ -> raise (Failure "Unreachable")
+  | _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
 let save_snapshot (ctx : Contexts.eval_ctx) (e : expression option) :
     expression option =