From 7ff59a3ff5daae9e88e9ff15f8a3452536c94628 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 23 Nov 2021 09:27:30 +0100 Subject: Change the way exceptions are used --- src/Errors.ml | 9 +-------- src/Identifiers.ml | 2 +- src/Interpreter.ml | 59 +++++++++++++++++++++++++++--------------------------- src/Print.ml | 4 ++-- 4 files changed, 34 insertions(+), 40 deletions(-) diff --git a/src/Errors.ml b/src/Errors.ml index d732e1f3..69a030b1 100644 --- a/src/Errors.ml +++ b/src/Errors.ml @@ -1,10 +1,3 @@ exception IntegerOverflow of unit -(* TODO: remove those *) -exception Unimplemented of string - -let unimplemented msg = raise (Unimplemented ("unimplemented: " ^ msg)) - -exception Unreachable of string - -let unreachable msg = raise (Unreachable ("unreachable: " ^ msg)) +exception Unimplemented diff --git a/src/Identifiers.ml b/src/Identifiers.ml index dbe2ae83..e75099d6 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -69,7 +69,7 @@ module IdGen () : Id = struct let rec update_nth vec id v = match (vec, id) with - | [], _ -> unreachable __LOC__ + | [], _ -> failwith "Unreachable" | _ :: vec', 0 -> v :: vec' | x :: vec', _ -> x :: update_nth vec' (id - 1) v diff --git a/src/Interpreter.ml b/src/Interpreter.ml index f63354ac..8ed1a68c 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -121,10 +121,10 @@ let rec end_borrow_get_borrow_in_env (config : config) l env0 : match config.mode with | ConcreteMode -> (* There can't be abstractions if we run in concrete mode *) - unreachable __LOC__ + failwith "Unreachable" | SymbolicMode -> (* TODO *) - unimplemented __LOC__) + raise Unimplemented) let rec give_back_value_to_value config bid (v : typed_value) (destv : typed_value) : typed_value = @@ -168,14 +168,14 @@ let rec give_back_value_to_value config bid (v : typed_value) let give_back_value_to_abs (_config : config) _bid _v _abs : abs = (* TODO *) - unimplemented __LOC__ + raise Unimplemented let give_back_value_to_env_value config bid v ev : env_value = match ev with | Var (vid, destv) -> Var (vid, give_back_value_to_value config bid v destv) | Abs abs -> ( match config.mode with - | ConcreteMode -> unreachable __LOC__ + | ConcreteMode -> failwith "Unreachable" | SymbolicMode -> Abs (give_back_value_to_abs config bid v abs)) let rec give_back_shared_to_value (config : config) bid (destv : typed_value) : @@ -235,14 +235,14 @@ let rec give_back_shared_to_value (config : config) bid (destv : typed_value) : let give_back_shared_to_abs _config _bid _abs : abs = (* TODO *) - unimplemented __LOC__ + raise Unimplemented let give_back_shared_to_env_value (config : config) bid ev : env_value = match ev with | Var (vid, destv) -> Var (vid, give_back_shared_to_value config bid destv) | Abs abs -> ( match config.mode with - | ConcreteMode -> unreachable __LOC__ + | ConcreteMode -> failwith "Unreachable" | SymbolicMode -> Abs (give_back_shared_to_abs config bid abs)) let give_back_value (config : config) (bid : BorrowId.id) (v : typed_value) @@ -264,7 +264,7 @@ let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env = * an abstraction may end several borrows at once *) | NotFound, env -> ( match config.mode with - | ConcreteMode -> unreachable __LOC__ + | ConcreteMode -> failwith "Unreachable" | SymbolicMode -> env) (* If we found outer borrows: end those borrows first *) | Outer outer_borrows, env -> @@ -311,7 +311,7 @@ let lookup_loan_in_env_value (config : config) (l : BorrowId.id) | Var (_, v) -> lookup_loan_in_value config l v | Abs _ -> ( match config.mode with - | ConcreteMode -> unreachable __LOC__ + | ConcreteMode -> failwith "Unreachable" | SymbolicMode -> None) (** Lookup a loan content from a borrow id. @@ -320,7 +320,7 @@ let lookup_loan_in_env_value (config : config) (l : BorrowId.id) let lookup_loan_from_borrow_id (config : config) (l : BorrowId.id) (env : env) : loan_content = match List.find_map (lookup_loan_in_env_value config l) env with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some lc -> lc (** If a shared value is borrowed exactly once, we can promote this shared loan @@ -384,7 +384,7 @@ let promote_shared_loan_to_mut_loan (config : config) (l : BorrowId.id) (* Promote in the environment *) let rec promote_in_env (env0 : env) : typed_value * env = match env0 with - | [] -> unreachable __LOC__ + | [] -> failwith "Unreachable" | Var (vid, v) :: env -> ( match promote_in_value v with | None -> @@ -393,7 +393,7 @@ let promote_shared_loan_to_mut_loan (config : config) (l : BorrowId.id) | Some (borrowed, new_v) -> (borrowed, Var (vid, new_v) :: env)) | Abs abs :: env -> (* We don't promote inside abstractions *) - if config.mode = ConcreteMode then unreachable __LOC__ + if config.mode = ConcreteMode then failwith "Unreachable" else let borrowed, env' = promote_in_env env in (borrowed, Abs abs :: env') @@ -432,7 +432,7 @@ let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id) match ev with | Var (name, v) -> Var (name, promote_in_value v) | Abs abs -> - if config.mode = ConcreteMode then unreachable __LOC__ else Abs abs + if config.mode = ConcreteMode then failwith "Unreachable" else Abs abs in List.map promote_in_env_value env0 @@ -443,7 +443,7 @@ let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id) let activate_inactivated_mut_borrow (config : config) (l : BorrowId.id) (env : env) : env = match lookup_loan_from_borrow_id config l env with - | MutLoan _ -> unreachable __LOC__ + | MutLoan _ -> failwith "Unreachable" | SharedLoan (bids, _) -> (* End the borrows which borrow from the value, at the exception of the borrow * we want to promote *) @@ -515,10 +515,10 @@ let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) : let lookup_in_env_value (ev : env_value) : typed_value option = match ev with | Var (_, v) -> lookup_in_value v - | Abs _ -> unimplemented __LOC__ + | Abs _ -> raise Unimplemented in match List.find_map lookup_in_env_value env with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some v -> v (** Read the value at the end of a projection *) @@ -550,16 +550,17 @@ let rec read_projection (config : config) (access : path_access) (env : env) (* Check that the projection is consistent with the current value *) (match (opt_variant_id, adt.variant_id) with | None, None -> () - | Some vid, Some vid' -> if vid <> vid' then unreachable __LOC__ - | _ -> unreachable __LOC__); + | Some vid, Some vid' -> + if vid <> vid' then failwith "Unreachable" + | _ -> failwith "Unreachable"); (* Actually project *) match FieldId.nth_opt adt.field_values field_id with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some fv -> read_projection config access env p fv) (* Tuples *) | Field (ProjTuple _, field_id), Tuple values -> ( match FieldId.nth_opt values field_id with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some fv -> read_projection config access env p fv) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *) @@ -579,7 +580,7 @@ let rec read_projection (config : config) (access : path_access) (env : env) | Read, SharedBorrow bid -> let sv = lookup_shared_value_from_borrow_id bid env in read_projection config access env p' sv - | Write, SharedBorrow _ -> unreachable __LOC__ + | Write, SharedBorrow _ -> failwith "Unreachable" | _, MutBorrow (_, bv) -> read_projection config access env p' bv (* We need to activate inactivated mutable borrows *) | _, InactivatedMutBorrow bid -> @@ -590,7 +591,7 @@ let rec read_projection (config : config) (access : path_access) (env : env) | ( _, ( Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _ | Loan _ ) ) -> - unreachable __LOC__) + failwith "Unreachable") (* Entering loans failed *) | res -> res) @@ -599,7 +600,7 @@ let read_place (config : config) (access : path_access) (p : place) (env0 : env) : typed_value path_access_result = let rec read_in_env env : typed_value path_access_result = match env with - | [] -> unreachable __LOC__ + | [] -> failwith "Unreachable" | Var (vid, v) :: env' -> if vid = p.var_id then read_projection config access env0 p.projection v else read_in_env env' @@ -620,11 +621,11 @@ let rec write_projection (config : config) (new_value : typed_value) (* Check that the projection is consistent with the current value *) (match (opt_variant_id, adt.variant_id) with | None, None -> () - | Some vid, Some vid' -> if vid <> vid' then unreachable __LOC__ - | _ -> unreachable __LOC__); + | Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable" + | _ -> failwith "Unreachable"); (* Actually project *) match FieldId.nth_opt adt.field_values field_id with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some fv -> ( (* Update the field value *) match write_projection config new_value p fv with @@ -640,7 +641,7 @@ let rec write_projection (config : config) (new_value : typed_value) | Field (ProjTuple _, field_id), Tuple values -> ( (* Project *) match FieldId.nth_opt values field_id with - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" | Some fv -> ( (* Update the field value *) match write_projection config new_value p fv with @@ -670,7 +671,7 @@ let rec write_projection (config : config) (new_value : typed_value) match bc with | SharedBorrow _ -> (* We can't update inside shared borrows *) - unreachable __LOC__ + failwith "Unreachable" | MutBorrow (bid, bv) -> ( match write_projection config new_value p' bv with | Error err -> Error err @@ -685,14 +686,14 @@ let rec write_projection (config : config) (new_value : typed_value) * on purpose, to make sure we statically catch errors if we * modify the [value] definition. *) | _, (Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _) -> - unreachable __LOC__) + failwith "Unreachable") (** Update the value at the end of a place *) let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) : env path_access_result = let rec write_in_env env : env path_access_result = match env with - | [] -> unreachable __LOC__ + | [] -> failwith "Unreachable" | Var (vid, v) :: env' -> ( if vid = p.var_id then match write_projection config nv p.projection v with diff --git a/src/Print.ml b/src/Print.ml index 874d19fb..c8296754 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -105,13 +105,13 @@ module Types = struct let rid_to_string rid = match List.find_opt (fun rv -> rv.rv_index = rid) regions with | Some rv -> region_var_to_string rv - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" in let r_to_string = region_to_string rid_to_string in let type_var_id_to_string id = match List.find_opt (fun tv -> tv.tv_index = id) types with | Some tv -> type_var_to_string tv - | None -> unreachable __LOC__ + | None -> failwith "Unreachable" in let fmt = { r_to_string; type_var_id_to_string; type_def_id_to_string } in let name = name_to_string def.name in -- cgit v1.2.3