summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Contexts.ml18
-rw-r--r--compiler/Interpreter.ml10
-rw-r--r--compiler/InterpreterBorrows.ml60
-rw-r--r--compiler/InterpreterBorrowsCore.ml31
-rw-r--r--compiler/InterpreterExpressions.ml8
-rw-r--r--compiler/InterpreterPaths.ml12
-rw-r--r--compiler/InterpreterProjectors.ml50
-rw-r--r--compiler/Invariants.ml36
-rw-r--r--compiler/Print.ml16
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/PureToExtract.ml26
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/Substitute.ml2
-rw-r--r--compiler/SymbolicToPure.ml19
-rw-r--r--compiler/SynthesizeSymbolic.ml10
-rw-r--r--compiler/Translate.ml13
-rw-r--r--compiler/ValuesUtils.ml4
17 files changed, 171 insertions, 148 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2d5fd907..8fb7053b 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -270,11 +270,11 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
*)
let rec lookup env =
match env with
- | [] -> failwith "Unexpected"
+ | [] -> raise (Failure "Unexpected")
| Var (var, v) :: env' ->
if opt_binder_has_vid var vid then v else lookup env'
| Abs _ :: env' -> lookup env'
- | Frame :: _ -> failwith "End of frame"
+ | Frame :: _ -> raise (Failure "End of frame")
in
lookup env
@@ -293,12 +293,12 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
*)
let rec update env =
match env with
- | [] -> failwith "Unexpected"
+ | [] -> raise (Failure "Unexpected")
| Var (var, v) :: env' ->
if opt_binder_has_vid var vid then Var (var, nv) :: env'
else Var (var, v) :: update env'
| Abs abs :: env' -> Abs abs :: update env'
- | Frame :: _ -> failwith "End of frame"
+ | Frame :: _ -> raise (Failure "End of frame")
in
update env
@@ -348,7 +348,7 @@ let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value =
let rec pop_var (env : env) : env * typed_value =
match env with
- | [] -> failwith "Could not find a dummy variable"
+ | [] -> raise (Failure "Could not find a dummy variable")
| Var (None, v) :: env -> (env, v)
| ee :: env ->
let env, v = pop_var env in
@@ -361,7 +361,7 @@ let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value =
let ctx_read_first_dummy_var (ctx : eval_ctx) : typed_value =
let rec read_var (env : env) : typed_value =
match env with
- | [] -> failwith "Could not find a dummy variable"
+ | [] -> raise (Failure "Could not find a dummy variable")
| Var (None, v) :: _env -> v
| _ :: env -> read_var env
in
@@ -379,7 +379,7 @@ let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs =
let rec lookup env =
match env with
- | [] -> failwith "Unexpected"
+ | [] -> raise (Failure "Unexpected")
| Var (_, _) :: env' -> lookup env'
| Abs abs :: env' -> if abs.abs_id = abs_id then abs else lookup env'
| Frame :: env' -> lookup env'
@@ -409,7 +409,7 @@ class ['self] iter_frame =
match em with
| Var (vid, v) -> self#visit_Var acc vid v
| Abs abs -> self#visit_Abs acc abs
- | Frame -> failwith "Unreachable"
+ | Frame -> raise (Failure "Unreachable")
method visit_env : 'acc -> env -> unit =
fun acc env ->
@@ -439,7 +439,7 @@ class ['self] map_frame_concrete =
match em with
| Var (vid, v) -> self#visit_Var acc vid v
| Abs abs -> self#visit_Abs acc abs
- | Frame -> failwith "Unreachable"
+ | Frame -> raise (Failure "Unreachable")
method visit_env : 'acc -> env -> env =
fun acc env ->
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index f92473f7..cf40c5b8 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -261,7 +261,8 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
* the executions can lead to a panic *)
if synthesize then Some SA.Panic else None
| _ ->
- failwith ("evaluate_function_symbolic failed on: " ^ name_to_string ())
+ raise
+ (Failure ("evaluate_function_symbolic failed on: " ^ name_to_string ()))
in
(* Evaluate the function *)
@@ -310,9 +311,10 @@ module Test = struct
(* Ok: drop the local variables and finish *)
ctx_pop_frame config (fun _ _ -> None) ctx
| _ ->
- failwith
- ("Unit test failed (concrete execution) on: "
- ^ Print.fun_name_to_string fdef.A.name)
+ raise
+ (Failure
+ ("Unit test failed (concrete execution) on: "
+ ^ Print.fun_name_to_string fdef.A.name))
in
(* Evaluate the function *)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e2d2bb0a..16aaf60a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -289,7 +289,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
("give_back_value: improper type:\n- expected: "
^ ety_to_string ctx ty ^ "\n- received: "
^ ety_to_string ctx nv.V.ty);
- failwith "Value given back doesn't have the proper type");
+ raise (Failure "Value given back doesn't have the proper type"));
(* Replace *)
set_replaced ();
nv.V.value)
@@ -335,7 +335,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
V.ABorrow
(V.AEndedIgnoredMutBorrow
{ given_back_loans_proj; child; given_back_meta })
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
else
(* Continue exploring *)
V.ABorrow (super#visit_AIgnoredMutBorrow opt_abs bid' child)
@@ -350,7 +350,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
(* Preparing a bit *)
let regions, ancestors_regions =
match opt_abs with
- | None -> failwith "Unreachable"
+ | None -> raise (Failure "Unreachable")
| Some abs -> (abs.V.regions, abs.V.ancestors_regions)
in
(* Rk.: there is a small issue with the types of the aloan values.
@@ -436,7 +436,7 @@ let give_back_symbolic_value (_config : C.config)
assert (sv.sv_id <> nsv.sv_id);
(match nsv.sv_kind with
| V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
- | V.FunCallRet | V.SynthInput | V.Global -> failwith "Unrechable");
+ | V.FunCallRet | V.SynthInput | V.Global -> raise (Failure "Unrechable"));
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -469,7 +469,7 @@ let give_back_symbolic_value (_config : C.config)
type [T]! We thus *mustn't* introduce a projector here.
*)
V.AProjBorrows (nsv, sv.V.sv_ty)
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
in
V.AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
@@ -530,7 +530,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
("give_back_avalue_to_same_abstraction: improper type:\n\
- expected: " ^ rty_to_string ctx ty ^ "\n- received: "
^ rty_to_string ctx nv.V.ty);
- failwith "Value given back doesn't have the proper type");
+ raise (Failure "Value given back doesn't have the proper type"));
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
* an ended loan *)
@@ -759,7 +759,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
| Abstract
( V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _ | V.AEndedIgnoredMutBorrow _
| V.AEndedSharedBorrow ) ->
- failwith "Unreachable"
+ raise (Failure "Unreachable")
(** Convert an {!type:V.avalue} to a {!type:V.value}.
@@ -851,7 +851,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
^ ": borrow didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
^ eval_ctx_to_string ctx));
- failwith "Borrow not eliminated"
+ raise (Failure "Borrow not eliminated")
in
match lookup_loan_opt ek_all l ctx with
| None -> () (* Ok *)
@@ -862,7 +862,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
^ ": loan didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n"
^ eval_ctx_to_string ctx));
- failwith "Loan not eliminated"
+ raise (Failure "Loan not eliminated")
in
let cf_check_disappeared : cm_fun = unit_to_cm_fun check_disappeared in
(* The complete sanity check: also check that after we ended a borrow,
@@ -1137,7 +1137,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
method! visit_aproj env sproj =
(match sproj with
- | V.AProjLoans _ -> failwith "Unexpected"
+ | V.AProjLoans _ -> raise (Failure "Unexpected")
| V.AProjBorrows (sv, proj_ty) ->
raise (FoundAProjBorrows (sv, proj_ty))
| V.AEndedProjLoans _ | V.AEndedProjBorrows _ | V.AIgnoredProjBorrows ->
@@ -1149,7 +1149,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
match bc with
| V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
raise (FoundBorrowContent bc)
- | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+ | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable")
end
in
(* Lookup the abstraction *)
@@ -1209,7 +1209,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
ctx
| V.AEndedMutBorrow _ | V.AIgnoredMutBorrow _
| V.AEndedIgnoredMutBorrow _ | V.AEndedSharedBorrow ->
- failwith "Unexpected"
+ raise (Failure "Unexpected")
in
(* Reexplore *)
end_abstraction_borrows config chain abs_id cf ctx
@@ -1241,19 +1241,19 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
| V.SharedBorrow (_, bid) -> (
(* Replace the shared borrow with bottom *)
match end_borrow_get_borrow (Some abs_id) bid ctx with
- | Error _ -> failwith "Unreachable"
+ | Error _ -> raise (Failure "Unreachable")
| Ok (ctx, _) ->
(* Give back *)
give_back_shared config bid ctx)
| V.MutBorrow (bid, v) -> (
(* Replace the mut borrow with bottom *)
match end_borrow_get_borrow (Some abs_id) bid ctx with
- | Error _ -> failwith "Unreachable"
+ | Error _ -> raise (Failure "Unreachable")
| Ok (ctx, _) ->
(* Give the value back - note that the mut borrow was below a
* shared borrow: the value is thus unchanged *)
give_back_value config bid v ctx)
- | V.InactivatedMutBorrow _ -> failwith "Unreachable"
+ | V.InactivatedMutBorrow _ -> raise (Failure "Unreachable")
in
(* Reexplore *)
end_abstraction_borrows config chain abs_id cf ctx
@@ -1264,7 +1264,7 @@ and end_abstraction_remove_from_context (_config : C.config)
fun cf ctx ->
let rec remove_from_env (env : C.env) : C.env * V.abs option =
match env with
- | [] -> failwith "Unreachable"
+ | [] -> raise (Failure "Unreachable")
| C.Frame :: _ -> (env, None)
| Var (bv, v) :: env ->
let env, abs_opt = remove_from_env env in
@@ -1463,7 +1463,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
in
match lookup_loan ek l ctx with
| _, Concrete (V.MutLoan _) ->
- failwith "Expected a shared loan, found a mut loan"
+ raise (Failure "Expected a shared loan, found a mut loan")
| _, Concrete (V.SharedLoan (bids, sv)) ->
(* Check that there is only one borrow id (l) and update the loan *)
assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1);
@@ -1482,9 +1482,10 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
| _, Abstract _ ->
(* I don't think it is possible to have two-phase borrows involving borrows
* returned by abstractions. I'm not sure how we could handle that anyway. *)
- failwith
- "Can't promote a shared loan to a mutable loan if the loan is inside \
- an abstraction"
+ raise
+ (Failure
+ "Can't promote a shared loan to a mutable loan if the loan is \
+ inside an abstraction")
(** Helper function: see {!activate_inactivated_mut_borrow}.
@@ -1502,15 +1503,16 @@ let promote_inactivated_borrow_to_mut_borrow (l : V.BorrowId.id) (cf : m_fun)
let ctx =
match lookup_borrow ek l ctx with
| Concrete (V.SharedBorrow _ | V.MutBorrow (_, _)) ->
- failwith "Expected an inactivated mutable borrow"
+ raise (Failure "Expected an inactivated mutable borrow")
| Concrete (V.InactivatedMutBorrow _) ->
(* Update it *)
update_borrow ek l (V.MutBorrow (l, borrowed_value)) ctx
| Abstract _ ->
(* This can't happen for sure *)
- failwith
- "Can't promote a shared borrow to a mutable borrow if the borrow is \
- inside an abstraction"
+ raise
+ (Failure
+ "Can't promote a shared borrow to a mutable borrow if the borrow \
+ is inside an abstraction")
in
(* Continue *)
cf ctx
@@ -1527,7 +1529,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
{ enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
in
match lookup_loan ek l ctx with
- | _, Concrete (V.MutLoan _) -> failwith "Unreachable"
+ | _, Concrete (V.MutLoan _) -> raise (Failure "Unreachable")
| _, Concrete (V.SharedLoan (bids, sv)) -> (
(* If there are loans inside the value, end them. Note that there can't be
inactivated borrows inside the value.
@@ -1575,6 +1577,8 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
| _, Abstract _ ->
(* I don't think it is possible to have two-phase borrows involving borrows
* returned by abstractions. I'm not sure how we could handle that anyway. *)
- failwith
- "Can't activate an inactivated mutable borrow referencing a loan inside\n\
- \ an abstraction"
+ raise
+ (Failure
+ "Can't activate an inactivated mutable borrow referencing a loan \
+ inside\n\
+ \ an abstraction")
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index a5501712..89c22f18 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -78,9 +78,10 @@ let borrow_or_abs_ids_chain_to_string (ids : borrow_or_abs_ids) : string =
let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id)
(ids : borrow_or_abs_ids) : borrow_or_abs_ids =
if List.mem id ids then
- failwith
- (msg ^ "detected a loop in the chain of ids: "
- ^ borrow_or_abs_ids_chain_to_string (id :: ids))
+ raise
+ (Failure
+ (msg ^ "detected a loop in the chain of ids: "
+ ^ borrow_or_abs_ids_chain_to_string (id :: ids)))
else id :: ids
(** Helper function.
@@ -150,7 +151,7 @@ let rec compare_rtys (default : bool) (combine : bool -> bool -> bool)
(lazy
("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ T.show_rty ty1
^ "\n- ty2: " ^ T.show_rty ty2));
- failwith "Unreachable"
+ raise (Failure "Unreachable")
(** Check if two different projections intersect. This is necessary when
giving a symbolic value to an abstraction: we need to check that
@@ -283,7 +284,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
let lookup_loan (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx) :
abs_or_var_id * g_loan_content =
match lookup_loan_opt ek l ctx with
- | None -> failwith "Unreachable"
+ | None -> raise (Failure "Unreachable")
| Some res -> res
(** Update a loan content.
@@ -464,7 +465,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
let lookup_borrow (ek : exploration_kind) (l : V.BorrowId.id) (ctx : C.eval_ctx)
: g_borrow_content =
match lookup_borrow_opt ek l ctx with
- | None -> failwith "Unreachable"
+ | None -> raise (Failure "Unreachable")
| Some lc -> lc
(** Update a borrow content.
@@ -677,13 +678,13 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
let set_non_shared ((id, ty) : V.AbstractionId.id * T.rty) : unit =
match !found with
| None -> found := Some (NonSharedProj (id, ty))
- | Some _ -> failwith "Unreachable"
+ | Some _ -> raise (Failure "Unreachable")
in
let add_shared (x : V.AbstractionId.id * T.rty) : unit =
match !found with
| None -> found := Some (SharedProjs [ x ])
| Some (SharedProjs pl) -> found := Some (SharedProjs (x :: pl))
- | Some (NonSharedProj _) -> failwith "Unreachable"
+ | Some (NonSharedProj _) -> raise (Failure "Unreachable")
in
let check_add_proj_borrows (is_shared : bool) abs sv' proj_ty =
if
@@ -703,7 +704,7 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
method! visit_abstract_shared_borrows abs asb =
(* Sanity check *)
(match !found with
- | Some (NonSharedProj _) -> failwith "Unreachable"
+ | Some (NonSharedProj _) -> raise (Failure "Unreachable")
| _ -> ());
(* Explore *)
if lookup_shared then
@@ -752,7 +753,7 @@ let lookup_intersecting_aproj_borrows_not_shared_opt
match lookup_intersecting_aproj_borrows_opt lookup_shared regions sv ctx with
| None -> None
| Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty)
- | _ -> failwith "Unexpected"
+ | _ -> raise (Failure "Unexpected")
(** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the
values.
@@ -772,7 +773,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
let set_non_shared () =
match !shared with
| None -> shared := Some false
- | Some _ -> failwith "Found unexpected intersecting proj_borrows"
+ | Some _ -> raise (Failure "Found unexpected intersecting proj_borrows")
in
let check_proj_borrows is_shared abs sv' proj_ty =
if
@@ -840,7 +841,7 @@ let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t)
(sv : V.symbolic_value) (nv : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
(* Small helpers *)
let can_update_shared = false in
- let update_shared _ _ = failwith "Unexpected" in
+ let update_shared _ _ = raise (Failure "Unexpected") in
let updated = ref false in
let update_non_shared _ _ =
(* We can update more than one borrow! *)
@@ -867,7 +868,7 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
(* Small helpers *)
let can_update_shared = true in
let update_shared _ _ = [] in
- let update_non_shared _ _ = failwith "Unexpected" in
+ let update_non_shared _ _ = raise (Failure "Unexpected") in
(* Update *)
update_intersecting_aproj_borrows can_update_shared update_shared
update_non_shared regions sv ctx
@@ -1118,7 +1119,7 @@ let no_aproj_over_symbolic_in_context (sv : V.symbolic_value) (ctx : C.eval_ctx)
in
(* Apply *)
try obj#visit_eval_ctx () ctx
- with Found -> failwith "update_aproj_loans_to_ended: failed"
+ with Found -> raise (Failure "update_aproj_loans_to_ended: failed")
(** Helper function
@@ -1156,7 +1157,7 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
| V.MutLoan _ ->
(* The mut loan linked to the mutable borrow present in a shared
* value in an abstraction should be in an AProjBorrows *)
- failwith "Unreachable"
+ raise (Failure "Unreachable")
| V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
method! visit_aproj env sproj =
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index fbe36b6a..c604bb00 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -129,7 +129,7 @@ let primitive_to_typed_value (ty : T.ety) (cv : V.primitive_value) :
assert (check_scalar_value_in_range v);
{ V.value = V.Primitive (PV.Scalar v); ty }
(* Remaining cases (invalid) *)
- | _, _ -> failwith "Improperly typed constant value"
+ | _, _ -> raise (Failure "Improperly typed constant value")
(** Reorganize the environment in preparation for the evaluation of an operand.
@@ -235,7 +235,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
assert (not (bottom_in_value ctx.ended_regions v));
let bottom : V.typed_value = { V.value = Bottom; ty = v.ty } in
match write_place config access p bottom ctx with
- | Error _ -> failwith "Unreachable"
+ | Error _ -> raise (Failure "Unreachable")
| Ok ctx -> cf v ctx
in
(* Compose and apply *)
@@ -289,7 +289,9 @@ let eval_two_operands (config : C.config) (op1 : E.operand) (op2 : E.operand)
(cf : V.typed_value * V.typed_value -> m_fun) : m_fun =
let eval_op = eval_operands config [ op1; op2 ] in
let use_res cf res =
- match res with [ v1; v2 ] -> cf (v1, v2) | _ -> failwith "Unreachable"
+ match res with
+ | [ v1; v2 ] -> cf (v1, v2)
+ | _ -> raise (Failure "Unreachable")
in
comp eval_op use_res cf
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 33062df3..4dea4c91 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -88,9 +88,10 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
(lazy
("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
^ T.show_ety v.ty));
- failwith
- "Assertion failed: new value doesn't have the same type as its \
- destination");
+ raise
+ (Failure
+ "Assertion failed: new value doesn't have the same type as its \
+ destination"));
Ok (ctx, { read = v; updated = nv })
| pe :: p' -> (
(* Match on the projection element and the value *)
@@ -463,8 +464,9 @@ let expand_bottom_value_from_projection (config : C.config)
(* Generate the field values *)
compute_expanded_bottom_tuple_value tys
| _ ->
- failwith
- ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty)
+ raise
+ (Failure
+ ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty))
in
(* Update the context by inserting the expanded value at the proper place *)
match write_place config access p' nv ctx with
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6dc8b402..b77a94c4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -43,7 +43,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
fields_types
in
List.concat proj_fields
- | V.Bottom, _ -> failwith "Unreachable"
+ | V.Bottom, _ -> raise (Failure "Unreachable")
| V.Borrow bc, T.Ref (r, ref_ty, kind) ->
(* Retrieve the bid of the borrow and the asb of the projected borrowed value *)
let bid, asb =
@@ -66,13 +66,15 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
| _, Abstract (V.ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
regions sv ref_ty
- | _ -> failwith "Unexpected"
+ | _ -> raise (Failure "Unexpected")
in
(bid, asb)
| V.InactivatedMutBorrow _, _ ->
- failwith
- "Can't apply a proj_borrow over an inactivated mutable borrow"
- | _ -> failwith "Unreachable"
+ raise
+ (Failure
+ "Can't apply a proj_borrow over an inactivated mutable \
+ borrow")
+ | _ -> raise (Failure "Unreachable")
in
let asb =
(* Check if the region is in the set of projected regions (note that
@@ -83,13 +85,13 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
else asb
in
asb
- | V.Loan _, _ -> failwith "Unreachable"
+ | V.Loan _, _ -> raise (Failure "Unreachable")
| V.Symbolic s, _ ->
(* Check that the projection doesn't contain ended regions *)
assert (
not (projections_intersect s.V.sv_ty ctx.ended_regions ty regions));
[ V.AsbProjReborrows (s, ty) ]
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
(** Apply (and reduce) a projector over borrows to a value.
@@ -154,7 +156,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
fields_types
in
V.AAdt { V.variant_id = adt.V.variant_id; field_values = proj_fields }
- | V.Bottom, _ -> failwith "Unreachable"
+ | V.Bottom, _ -> raise (Failure "Unreachable")
| V.Borrow bc, T.Ref (r, ref_ty, kind) ->
if
(* Check if the region is in the set of projected regions (note that
@@ -175,10 +177,11 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
V.AMutBorrow (mv, bid, bv)
| V.SharedBorrow (_, bid), T.Shared -> V.ASharedBorrow bid
| V.InactivatedMutBorrow _, _ ->
- failwith
- "Can't apply a proj_borrow over an inactivated mutable \
- borrow"
- | _ -> failwith "Unreachable"
+ raise
+ (Failure
+ "Can't apply a proj_borrow over an inactivated mutable \
+ borrow")
+ | _ -> raise (Failure "Unreachable")
in
V.ABorrow bc
else
@@ -208,17 +211,18 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
| _, Abstract (V.ASharedLoan (_, sv, _)) ->
apply_proj_borrows_on_shared_borrow ctx fresh_reborrow
regions sv ref_ty
- | _ -> failwith "Unexpected"
+ | _ -> raise (Failure "Unexpected")
in
V.AProjSharedBorrow asb
| V.InactivatedMutBorrow _, _ ->
- failwith
- "Can't apply a proj_borrow over an inactivated mutable \
- borrow"
- | _ -> failwith "Unreachable"
+ raise
+ (Failure
+ "Can't apply a proj_borrow over an inactivated mutable \
+ borrow")
+ | _ -> raise (Failure "Unreachable")
in
V.ABorrow bc
- | V.Loan _, _ -> failwith "Unreachable"
+ | V.Loan _, _ -> raise (Failure "Unreachable")
| V.Symbolic s, _ ->
(* Check that the projection doesn't contain already ended regions,
* if necessary *)
@@ -243,7 +247,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
("apply_proj_borrows: unexpected inputs:\n- input value: "
^ typed_value_to_string ctx v
^ "\n- proj rty: " ^ rty_to_string ctx ty));
- failwith "Unreachable"
+ raise (Failure "Unreachable")
in
{ V.value; V.ty }
@@ -260,7 +264,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
in
V.Adt { V.variant_id; V.field_values }
| SeMutRef (_, _) | SeSharedRef (_, _) ->
- failwith "Unexpected symbolic reference expansion"
+ raise (Failure "Unexpected symbolic reference expansion")
in
{ V.value; V.ty }
@@ -279,7 +283,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value)
let value = V.Borrow (V.MutBorrow (bid, bv)) in
{ V.value; ty }
| SeSharedRef (_, _) ->
- failwith "Unexpected symbolic shared reference expansion"
+ raise (Failure "Unexpected symbolic shared reference expansion")
| _ -> symbolic_expansion_non_borrow_to_value sv see
(** Apply (and reduce) a projector over loans to a value.
@@ -331,7 +335,7 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
else
(* Not in the set: ignore *)
(V.ALoan (V.AIgnoredSharedLoan child_av), ref_ty)
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
in
{ V.value; V.ty }
@@ -510,7 +514,7 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) :
let bid' = C.fresh_borrow_id () in
reborrows := (bid, bid') :: !reborrows;
bid')
- else failwith "Unexpected reborrow"
+ else raise (Failure "Unexpected reborrow")
in
(* The function to apply the reborrows in a context *)
let apply_registered_reborrows (ctx : C.eval_ctx) : C.eval_ctx =
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index bd577d8d..18a1c835 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -192,7 +192,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
^ V.BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
in
log#serror err;
- failwith err
+ raise (Failure err)
in
let update_info (bid : V.BorrowId.id) (info : borrow_info) : unit =
@@ -202,7 +202,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
let infos =
V.BorrowId.Map.update repr_bid
(fun x ->
- match x with Some _ -> Some info | None -> failwith "Unreachable")
+ match x with
+ | Some _ -> Some info
+ | None -> raise (Failure "Unreachable"))
!borrows_infos
in
borrows_infos := infos
@@ -216,7 +218,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Check that the borrow kind is consistent *)
(match (info.loan_kind, kind) with
| T.Shared, (Shared | Inactivated) | T.Mut, Mut -> ()
- | _ -> failwith "Invariant not satisfied");
+ | _ -> raise (Failure "Invariant not satisfied"));
(* An inactivated borrow can't point to a value inside an abstraction *)
assert (kind <> Inactivated || not info.loan_in_abs);
(* Insert the borrow id *)
@@ -382,7 +384,7 @@ let check_primitive_value_type (cv : V.primitive_value) (ty : T.ety) : unit =
match (cv, ty) with
| PV.Scalar sv, T.Integer int_ty -> assert (sv.int_ty = int_ty)
| PV.Bool _, T.Bool | PV.Char _, T.Char | PV.String _, T.Str -> ()
- | _ -> failwith "Erroneous typing"
+ | _ -> raise (Failure "Erroneous typing")
let check_typing_invariant (ctx : C.eval_ctx) : unit =
(* TODO: the type of aloans doens't make sense: they have a type
@@ -419,7 +421,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Some variant_id, T.Enum variants ->
assert (T.VariantId.to_int variant_id < List.length variants)
| None, T.Struct _ -> ()
- | _ -> failwith "Erroneous typing");
+ | _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
Subst.type_decl_get_instantiated_field_etypes def av.V.variant_id
@@ -456,7 +458,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
List.iter
(fun (v : V.typed_value) -> assert (v.ty = vec_ty))
fvs
- | _ -> failwith "Erroneous type")
+ | _ -> raise (Failure "Erroneous type"))
| V.Bottom, _ -> (* Nothing to check *) ()
| V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
match (bc, rkind) with
@@ -468,12 +470,12 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Concrete (V.SharedLoan (_, sv))
| Abstract (V.ASharedLoan (_, sv, _)) ->
assert (sv.V.ty = ref_ty)
- | _ -> failwith "Inconsistent context")
+ | _ -> raise (Failure "Inconsistent context"))
| V.MutBorrow (_, bv), T.Mut ->
assert (
(* Check that the borrowed value has the proper type *)
bv.V.ty = ref_ty)
- | _ -> failwith "Erroneous typing")
+ | _ -> raise (Failure "Erroneous typing"))
| V.Loan lc, ty -> (
match lc with
| V.SharedLoan (_, sv) -> assert (sv.V.ty = ty)
@@ -484,11 +486,11 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Concrete (V.MutBorrow (_, bv)) -> assert (bv.V.ty = ty)
| Abstract (V.AMutBorrow (_, _, sv)) ->
assert (Subst.erase_regions sv.V.ty = ty)
- | _ -> failwith "Inconsistent context"))
+ | _ -> raise (Failure "Inconsistent context")))
| V.Symbolic sv, ty ->
let ty' = Subst.erase_regions sv.V.sv_ty in
assert (ty' = ty)
- | _ -> failwith "Erroneous typing");
+ | _ -> raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
super#visit_typed_value info tv
@@ -518,7 +520,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Some variant_id, T.Enum variants ->
assert (T.VariantId.to_int variant_id < List.length variants)
| None, T.Struct _ -> ()
- | _ -> failwith "Erroneous typing");
+ | _ -> raise (Failure "Erroneous typing"));
(* Check that the field types are correct *)
let field_types =
Subst.type_decl_get_instantiated_field_rtypes def av.V.variant_id
@@ -547,7 +549,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
(* Box *)
| T.Box, [ boxed_value ], [], [ boxed_ty ] ->
assert (boxed_value.V.ty = boxed_ty)
- | _ -> failwith "Erroneous type")
+ | _ -> raise (Failure "Erroneous type"))
| V.ABottom, _ -> (* Nothing to check *) ()
| V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> (
match (bc, rkind) with
@@ -561,7 +563,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| Concrete (V.SharedLoan (_, sv))
| Abstract (V.ASharedLoan (_, sv, _)) ->
assert (sv.V.ty = Subst.erase_regions ref_ty)
- | _ -> failwith "Inconsistent context")
+ | _ -> raise (Failure "Inconsistent context"))
| V.AIgnoredMutBorrow (_opt_bid, av), T.Mut ->
assert (av.V.ty = ref_ty)
| ( V.AEndedIgnoredMutBorrow
@@ -570,7 +572,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
assert (given_back_loans_proj.V.ty = ref_ty);
assert (child.V.ty = ref_ty)
| V.AProjSharedBorrow _, T.Shared -> ()
- | _ -> failwith "Inconsistent context")
+ | _ -> raise (Failure "Inconsistent context"))
| V.ALoan lc, aty -> (
match lc with
| V.AMutLoan (bid, child_av) | V.AIgnoredMutLoan (bid, child_av)
@@ -586,7 +588,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
assert (
Subst.erase_regions sv.V.ty
= Subst.erase_regions borrowed_aty)
- | _ -> failwith "Inconsistent context")
+ | _ -> raise (Failure "Inconsistent context"))
| V.ASharedLoan (_, sv, child_av) | V.AEndedSharedLoan (sv, child_av)
->
let borrowed_aty = aloan_get_expected_child_type aty in
@@ -624,11 +626,11 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
match proj with
| V.AProjBorrows (_sv, ty') -> assert (ty' = ty)
| V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ()
- | _ -> failwith "Unexpected")
+ | _ -> raise (Failure "Unexpected"))
given_back_ls
| V.AEndedProjBorrows _ | V.AIgnoredProjBorrows -> ())
| V.AIgnored, _ -> ()
- | _ -> failwith "Erroneous typing");
+ | _ -> raise (Failure "Erroneous typing"));
(* Continue exploring to inspect the subterms *)
super#visit_typed_avalue info atv
end
diff --git a/compiler/Print.ml b/compiler/Print.ml
index c22f9171..dc73b572 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -110,10 +110,10 @@ module Values = struct
else if av.variant_id = Some T.option_none_id then (
assert (field_values = []);
"@Option::None")
- else failwith "Unreachable"
+ else raise (Failure "Unreachable")
| Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
- | _ -> failwith "Inconsistent value")
- | _ -> failwith "Inconsistent typed value")
+ | _ -> raise (Failure "Inconsistent value"))
+ | _ -> raise (Failure "Inconsistent typed value"))
| Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
| Borrow bc -> borrow_content_to_string fmt bc
| Loan lc -> loan_content_to_string fmt lc
@@ -214,8 +214,8 @@ module Values = struct
(* Assumed type *)
match (aty, field_values) with
| Box, [ bv ] -> "@Box(" ^ bv ^ ")"
- | _ -> failwith "Inconsistent value")
- | _ -> failwith "Inconsistent typed value")
+ | _ -> raise (Failure "Inconsistent value"))
+ | _ -> raise (Failure "Inconsistent typed value"))
| ABottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
| ABorrow bc -> aborrow_content_to_string fmt bc
| ALoan lc -> aloan_content_to_string fmt lc
@@ -324,7 +324,7 @@ module Contexts = struct
in
indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
| Abs abs -> PV.abs_to_string fmt indent indent_incr abs
- | Frame -> failwith "Can't print a Frame element"
+ | Frame -> raise (Failure "Can't print a Frame element")
let opt_env_elem_to_string (fmt : PV.value_formatter) (indent : string)
(indent_incr : string) (ev : C.env_elem option) : string =
@@ -402,7 +402,9 @@ module Contexts = struct
let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
(* We shouldn't use rvar_to_string *)
- let rvar_to_string _r = failwith "Unexpected use of rvar_to_string" in
+ let rvar_to_string _r =
+ raise (Failure "Unexpected use of rvar_to_string")
+ in
let r_to_string r = PT.region_id_to_string r in
let type_var_id_to_string vid =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9899cfcf..239b0b4f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1117,7 +1117,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let arg, args =
match args with
| _ :: given_back :: args -> (given_back, args)
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
in
mk_apps arg args
| A.BoxFree, _ ->
diff --git a/compiler/PureToExtract.ml b/compiler/PureToExtract.ml
index 7f79aa88..e38a92db 100644
--- a/compiler/PureToExtract.ml
+++ b/compiler/PureToExtract.ml
@@ -267,7 +267,7 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
name \"" ^ name ^ "\":" ^ id1 ^ id2
in
log#serror err;
- failwith err);
+ raise (Failure err));
(* Sanity check *)
assert (not (StringSet.mem name nm.names_set));
(* Insert *)
@@ -353,7 +353,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
let def = TypeDeclId.Map.find id type_decls in
Print.name_to_string def.name
| Assumed aty -> show_assumed_ty aty
- | Tuple -> failwith "Unreachable"
+ | Tuple -> raise (Failure "Unreachable")
in
match id with
| GlobalId gid ->
@@ -385,21 +385,21 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| VariantId (id, variant_id) ->
let variant_name =
match id with
- | Tuple -> failwith "Unreachable"
- | Assumed State -> failwith "Unreachable"
+ | Tuple -> raise (Failure "Unreachable")
+ | Assumed State -> raise (Failure "Unreachable")
| Assumed Result ->
if variant_id = result_return_id then "@result::Return"
else if variant_id = result_fail_id then "@result::Fail"
- else failwith "Unreachable"
+ else raise (Failure "Unreachable")
| Assumed Option ->
if variant_id = option_some_id then "@option::Some"
else if variant_id = option_none_id then "@option::None"
- else failwith "Unreachable"
- | Assumed Vec -> failwith "Unreachable"
+ else raise (Failure "Unreachable")
+ | Assumed Vec -> raise (Failure "Unreachable")
| AdtId id -> (
let def = TypeDeclId.Map.find id type_decls in
match def.kind with
- | Struct _ | Opaque -> failwith "Unreachable"
+ | Struct _ | Opaque -> raise (Failure "Unreachable")
| Enum variants ->
let variant = VariantId.nth variants variant_id in
Print.name_to_string def.name ^ "::" ^ variant.variant_name)
@@ -408,15 +408,15 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| FieldId (id, field_id) ->
let field_name =
match id with
- | Tuple -> failwith "Unreachable"
- | Assumed (State | Result | Option) -> failwith "Unreachable"
+ | Tuple -> raise (Failure "Unreachable")
+ | Assumed (State | Result | Option) -> raise (Failure "Unreachable")
| Assumed Vec ->
(* We can't directly have access to the fields of a vector *)
- failwith "Unreachable"
+ raise (Failure "Unreachable")
| AdtId id -> (
let def = TypeDeclId.Map.find id type_decls in
match def.kind with
- | Enum _ | Opaque -> failwith "Unreachable"
+ | Enum _ | Opaque -> raise (Failure "Unreachable")
| Struct fields ->
let field = FieldId.nth fields field_id in
let field_name =
@@ -431,7 +431,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| TypeVarId _ | VarId _ ->
(* We should never get there: we add indices to make sure variable
* names are unique *)
- failwith "Unreachable"
+ raise (Failure "Unreachable")
let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
(* The id_to_string function to print nice debugging messages if there are
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 30a89fee..2ef97e59 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -409,7 +409,7 @@ let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ])
let unwrap_result_ty (ty : ty) : ty =
match ty with
| Adt (Assumed Result, [ ty ]) -> ty
- | _ -> failwith "not a result type"
+ | _ -> raise (Failure "not a result type")
let mk_result_fail_texpression (ty : ty) : texpression =
let type_args = [ ty ] in
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index bc5febdc..30469c2f 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -182,7 +182,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
assert (List.length type_params = 1);
if adt.V.variant_id = Some T.option_some_id then type_params
else if adt.V.variant_id = Some T.option_none_id then []
- else failwith "Unrechable")
+ else raise (Failure "Unreachable"))
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6e60acc2..54f14d30 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -284,8 +284,10 @@ let rec translate_sty (ty : T.sty) : ty =
match tys with
| [ ty ] -> ty
| _ ->
- failwith
- "Box/vec/option type with incorrect number of arguments")))
+ raise
+ (Failure
+ "Box/vec/option type with incorrect number of arguments")
+ )))
| TypeVar vid -> TypeVar vid
| Bool -> Bool
| Char -> Char
@@ -370,9 +372,10 @@ let rec translate_fwd_ty (types_infos : TA.type_infos) (ty : 'r T.ty) : ty =
match t_tys with
| [ bty ] -> bty
| _ ->
- failwith
- "Unreachable: box/vec/option receives exactly one type \
- parameter"))
+ raise
+ (Failure
+ "Unreachable: box/vec/option receives exactly one type \
+ parameter")))
| TypeVar vid -> TypeVar vid
| Bool -> Bool
| Char -> Char
@@ -427,7 +430,9 @@ let rec translate_back_ty (types_infos : TA.type_infos)
match tys with
| [ bty ] -> translate bty
| _ ->
- failwith "Unreachable: boxes receive exactly one type parameter")
+ raise
+ (Failure "Unreachable: boxes receive exactly one type parameter")
+ )
| T.Tuple -> (
(* Tuples can contain borrows (which we eliminated) *)
let tys_t = List.filter_map translate tys in
@@ -1584,7 +1589,7 @@ and translate_expansion (config : config) (p : S.mplace option)
* through the functions provided by the API (note that we don't
* know how to expand a vector, because it has a variable number
* of fields!) *)
- failwith "Can't expand a vector value"
+ raise (Failure "Can't expand a vector value")
| T.Assumed T.Option ->
(* We shouldn't get there in the "one-branch" case: options have
* two variants *)
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index b4d2ae25..383ff15e 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -38,7 +38,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
(Some (V.SePrimitive (PV.Bool false)), false_exp);
] ->
ExpandBool (true_exp, false_exp)
- | _ -> failwith "Ill-formed boolean expansion")
+ | _ -> raise (Failure "Ill-formed boolean expansion"))
| T.Integer int_ty ->
(* Switch over an integer: split between the "regular" branches
and the "otherwise" branch (which should be the last branch) *)
@@ -51,7 +51,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
| Some (V.SePrimitive (PV.Scalar cv)) ->
assert (cv.PV.int_ty = int_ty);
cv
- | _ -> failwith "Unreachable"
+ | _ -> raise (Failure "Unreachable")
in
let branches =
List.map (fun (see, exp) -> (get_scalar see, exp)) branches
@@ -68,7 +68,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
T.VariantId.id option * V.symbolic_value list =
match see with
| Some (V.SeAdt (vid, fields)) -> (vid, fields)
- | _ -> failwith "Ill-formed branching ADT expansion"
+ | _ -> raise (Failure "Ill-formed branching ADT expansion")
in
let exp =
List.map
@@ -82,9 +82,9 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
(* Reference expansion: there should be one branch *)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
- | _ -> failwith "Ill-formed borrow expansion")
+ | _ -> raise (Failure "Ill-formed borrow expansion"))
| T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
- failwith "Ill-formed symbolic expansion"
+ raise (Failure "Ill-formed symbolic expansion")
in
Some (Expansion (place, sv, expansion))
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 35633d29..46f8172a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -653,8 +653,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
A.FunDeclId.Set.of_list
(List.concat
(List.map
- (fun decl ->
- match decl with A.Fun (Rec ids) -> ids | _ -> [])
+ (fun decl -> match decl with A.Fun (Rec ids) -> ids | _ -> [])
crate.declarations))
in
@@ -697,7 +696,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
match Filename.chop_suffix_opt ~suffix:".llbc" filename with
| None ->
(* Note that we already checked the suffix upon opening the file *)
- failwith "Unreachable"
+ raise (Failure "Unreachable")
| Some filename ->
(* Retrieve the file basename *)
let basename = Filename.basename filename in
@@ -794,8 +793,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
interface = has_opaque_types;
}
in
- extract_file types_config gen_ctx types_filename crate.A.name
- types_module ": type definitions" [] [];
+ extract_file types_config gen_ctx types_filename crate.A.name types_module
+ ": type definitions" [] [];
(* Extract the template clauses *)
let needs_clauses_module =
@@ -867,5 +866,5 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
in
(* Add the extension for F* *)
let extract_filename = extract_filebasename ^ ".fst" in
- extract_file gen_config gen_ctx extract_filename crate.A.name
- module_name "" [] []
+ extract_file gen_config gen_ctx extract_filename crate.A.name module_name ""
+ [] []
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 72d7abe0..0e1714a8 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -25,12 +25,12 @@ let is_symbolic (v : value) : bool =
match v with Symbolic _ -> true | _ -> false
let as_symbolic (v : value) : symbolic_value =
- match v with Symbolic s -> s | _ -> failwith "Unexpected"
+ match v with Symbolic s -> s | _ -> raise (Failure "Unexpected")
let as_mut_borrow (v : typed_value) : BorrowId.id * typed_value =
match v.value with
| Borrow (MutBorrow (bid, bv)) -> (bid, bv)
- | _ -> failwith "Unexpected"
+ | _ -> raise (Failure "Unexpected")
(** Check if a value contains a borrow *)
let borrows_in_value (v : typed_value) : bool =
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 13:42:10 +0000