diff options
| -rw-r--r-- | TODO.md | 3 | ||||
| -rw-r--r-- | src/InterpreterBorrowsCore.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 13 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 59 | ||||
| -rw-r--r-- | src/main.ml | 8 |
5 files changed, 52 insertions, 33 deletions
@@ -1,5 +1,8 @@ # TODO +0. replace all the `failwith` with `raise (Failure ...)`: in CPS, it messes + up with provenance tracking + 0. In SymbolicToPure we do a few simplifications on types and values (simplification of box type, removal of tuples which contain exactly one field - some fields may have been filtered for the backward functions...): there are already a diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 941ac140..30314307 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -268,7 +268,7 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) with FoundGLoanContent lc -> ( match !abs_or_var with | Some abs_or_var -> Some (abs_or_var, lc) - | None -> failwith "Inconsistent state") + | None -> raise (Failure "Inconsistent state")) (** Lookup a loan content. diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 49f261c7..4a7d8dc8 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -373,12 +373,15 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_def T.TypeDefId.Map.t) (** Compute an expanded Option bottom value *) let compute_expanded_bottom_option_value (variant_id : T.VariantId.id) (param_ty : T.ety) : V.typed_value = - (* The variant should be `Some` - `None` has no field, so there is no way - * we expand an Option bottom value to `None` (it happens when writing a field) *) + (* Note that the variant can be `Some` or `None`: we expand bottom values + * when writing to fields or setting discriminants *) assert (variant_id = T.option_some_id); - - let av = mk_bottom param_ty in - let av = V.Adt { variant_id = Some variant_id; field_values = [ av ] } in + let field_values = + if variant_id = T.option_some_id then [ mk_bottom param_ty ] + else if variant_id = T.option_none_id then [] + else raise (Failure "Unreachable") + in + let av = V.Adt { variant_id = Some variant_id; field_values } in let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ]) in { V.value = av; ty } diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 5565a98f..d36c653e 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -122,7 +122,9 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) : | Concrete (Bool b) -> (* Branch *) if b = assertion.expected then cf Unit ctx else cf Panic ctx - | _ -> failwith ("Expected a boolean, got: " ^ typed_value_to_string ctx v) + | _ -> + raise + (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) in (* Compose and apply *) comp eval_op eval_assert cf ctx @@ -164,7 +166,9 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = (S.mk_opt_place_from_op assertion.cond ctx) in comp expand (eval_assertion_concrete config assertion) cf ctx - | _ -> failwith ("Expected a boolean, got: " ^ typed_value_to_string ctx v) + | _ -> + raise + (Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v)) in (* Compose and apply *) comp prepare eval cf ctx @@ -192,7 +196,8 @@ let set_discriminant (config : C.config) (p : E.place) let update_value cf (v : V.typed_value) : m_fun = fun ctx -> match (v.V.ty, v.V.value) with - | T.Adt (T.AdtId def_id, regions, types), V.Adt av -> ( + | ( T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types), + V.Adt av ) -> ( (* There are two situations: - either the discriminant is already the proper one (in which case we don't do anything) @@ -200,15 +205,22 @@ let set_discriminant (config : C.config) (p : E.place) a variant with all its fields set to [Bottom] *) match av.variant_id with - | None -> failwith "Found a struct value while expected an enum" + | None -> raise (Failure "Found a struct value while expected an enum") | Some variant_id' -> if variant_id' = variant_id then (* Nothing to do *) cf Unit ctx else (* Replace the value *) let bottom_v = - compute_expanded_bottom_adt_value ctx.type_context.type_defs - def_id (Some variant_id) regions types + match type_id with + | T.AdtId def_id -> + compute_expanded_bottom_adt_value ctx.type_context.type_defs + def_id (Some variant_id) regions types + | T.Assumed T.Option -> + assert (regions = []); + compute_expanded_bottom_option_value variant_id + (Collections.List.to_cons_nil types) + | _ -> raise (Failure "Unreachable") in assign_to_place config bottom_v p (cf Unit) ctx) | T.Adt (T.AdtId def_id, regions, types), V.Bottom -> @@ -226,9 +238,10 @@ let set_discriminant (config : C.config) (p : E.place) * For now, we forbid setting the discriminant of a symbolic value: * setting a discriminant should only be used to initialize a value, * or reset an already initialized value, really. *) - failwith "Unexpected value" - | _, (V.Adt _ | V.Bottom) -> failwith "Inconsistent state" - | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> failwith "Unexpected value" + raise (Failure "Unexpected value") + | _, (V.Adt _ | V.Bottom) -> raise (Failure "Inconsistent state") + | _, (V.Concrete _ | V.Borrow _ | V.Loan _) -> + raise (Failure "Unexpected value") in (* Compose and apply *) comp cc update_value cf ctx @@ -250,7 +263,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id) | A.BoxDeref, [], [ bty ] -> T.Ref (T.Erased, bty, T.Shared) | A.BoxDerefMut, [], [ bty ] -> T.Ref (T.Erased, bty, T.Mut) | A.BoxFree, [], [ _ ] -> mk_unit_ty - | _ -> failwith "Inconsistent state" + | _ -> raise (Failure "Inconsistent state") let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = @@ -277,7 +290,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = let ret_vid = V.VarId.zero in let rec list_locals env = match env with - | [] -> failwith "Inconsistent environment" + | [] -> raise (Failure "Inconsistent environment") | C.Abs _ :: env -> list_locals env | C.Var (None, _) :: env -> list_locals env | C.Var (Some var, _) :: env -> @@ -331,7 +344,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = * no outer loans) as dummy variables in the caller frame *) let rec pop env = match env with - | [] -> failwith "Inconsistent environment" + | [] -> raise (Failure "Inconsistent environment") | C.Abs abs :: env -> C.Abs abs :: pop env | C.Var (_, v) :: env -> C.Var (None, v) :: pop env | C.Frame :: env -> (* Stop here *) env @@ -396,7 +409,7 @@ let eval_box_new_concrete (config : C.config) (* Compose and apply *) comp cf_move cf_create cf ctx - | _ -> failwith "Inconsistent state" + | _ -> raise (Failure "Inconsistent state") (** Auxiliary function which factorizes code to evaluate `std::Deref::deref` and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) @@ -433,7 +446,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) match res with | Error EPanic -> (* We can't get there by borrowing a value *) - failwith "Unreachable" + raise (Failure "Unreachable") | Ok borrowed_value -> (* Move and continue *) let destp = mk_place_from_var_id V.VarId.zero in @@ -442,7 +455,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config) (* Compose and apply *) comp cf_borrow cf_move cf ctx - | _ -> failwith "Inconsistent state" + | _ -> raise (Failure "Inconsistent state") (** Auxiliary function - see [eval_non_local_function_call] *) let eval_box_deref_concrete (config : C.config) @@ -494,7 +507,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) (* Continue *) cc cf ctx - | _ -> failwith "Inconsistent state" + | _ -> raise (Failure "Inconsistent state") (** Auxiliary function - see [eval_non_local_function_call] *) let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id) @@ -561,7 +574,7 @@ let eval_non_local_function_call_concrete (config : C.config) | BoxDerefMut -> eval_box_deref_mut_concrete config region_params type_params | BoxFree -> - (* Should have been treated above *) failwith "Unreachable" + (* Should have been treated above *) raise (Failure "Unreachable") | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut -> eval_vec_function_concrete config fid region_params type_params in @@ -828,7 +841,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = * [Unit] would account for the first iteration of the loop. * We prefer to write it this way for consistency and sanity, * though. *) - failwith "Unreachable" + raise (Failure "Unreachable") in (* Apply *) eval_statement config loop_body reeval_loop_body ctx @@ -881,7 +894,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : let cf_eval_if cf = eval_switch config op tgts cf in (* Compose *) comp cf_expand cf_eval_if cf ctx - | _ -> failwith "Inconsistent state") + | _ -> raise (Failure "Inconsistent state")) | A.SwitchInt (int_ty, stgts, otherwise) -> ( match op_v.value with | V.Concrete (V.Scalar sv) -> @@ -914,7 +927,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : expand_symbolic_int config sv (S.mk_opt_place_from_op op ctx) int_ty stgts otherwise ctx - | _ -> failwith "Inconsistent state") + | _ -> raise (Failure "Inconsistent state")) in (* Compose the continuations *) comp cf_prepare_op cf_match cf ctx @@ -963,7 +976,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id) let ret_var, locals = match locals with | ret_ty :: locals -> (ret_ty, locals) - | _ -> failwith "Unreachable" + | _ -> raise (Failure "Unreachable") in let input_locals, locals = Collections.List.split_at locals def.A.arg_count in @@ -988,7 +1001,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDefId.id) let cf_finish cf res = match res with | Panic -> cf Panic - | Break _ | Continue _ | Unit -> failwith "Unreachable" + | Break _ | Continue _ | Unit -> raise (Failure "Unreachable") | Return -> (* Pop the stack frame, retrieve the return value, move it to * its destination and continue *) @@ -1136,7 +1149,7 @@ and eval_non_local_function_call_symbolic (config : C.config) match fid with | A.BoxFree -> (* should have been treated above *) - failwith "Unreachable" + raise (Failure "Unreachable") | _ -> instantiate_fun_sig type_params (Assumed.get_assumed_sig fid) in diff --git a/src/main.ml b/src/main.ml index 79a04c4e..d42a4f02 100644 --- a/src/main.ml +++ b/src/main.ml @@ -94,11 +94,11 @@ let () = main_log#set_level EL.Debug; interpreter_log#set_level EL.Debug; statements_log#set_level EL.Debug; - paths_log#set_level EL.Warning; + paths_log#set_level EL.Debug; expressions_log#set_level EL.Debug; - expansion_log#set_level EL.Warning; - borrows_log#set_level EL.Warning; - invariants_log#set_level EL.Warning; + expansion_log#set_level EL.Debug; + borrows_log#set_level EL.Debug; + invariants_log#set_level EL.Debug; symbolic_to_pure_log#set_level EL.Debug; pure_micro_passes_log#set_level EL.Debug; pure_to_extract_log#set_level EL.Debug; |