diff options
| -rw-r--r-- | compiler/Contexts.ml | 18 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 10 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 60 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 31 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 50 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 36 | ||||
| -rw-r--r-- | compiler/Print.ml | 16 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 2 | ||||
| -rw-r--r-- | compiler/PureToExtract.ml | 26 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/Substitute.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 19 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 10 | ||||
| -rw-r--r-- | compiler/Translate.ml | 13 | ||||
| -rw-r--r-- | compiler/ValuesUtils.ml | 4 |
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 = |