diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Identifiers.ml | 4 | ||||
| -rw-r--r-- | src/Interpreter.ml | 146 |
2 files changed, 80 insertions, 70 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index e75099d6..9b125161 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -23,6 +23,8 @@ module type Id = sig val vector_of_list : 'a list -> 'a vector + val nth : 'a vector -> id -> 'a + val nth_opt : 'a vector -> id -> 'a option val update_nth : 'a vector -> id -> 'a -> 'a vector @@ -65,6 +67,8 @@ module IdGen () : Id = struct let vector_of_list v = v + let nth v id = List.nth v id + let nth_opt v id = List.nth_opt v id let rec update_nth vec id v = diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 5cba4908..062c8214 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -117,14 +117,9 @@ let rec end_borrow_get_borrow_in_env (config : config) l env0 : let res, env' = end_borrow_get_borrow_in_env config l env in (res, Var (x, v') :: env') | res, v' -> (res, Var (x, v') :: env)) - | Abs _ :: _ -> ( - match config.mode with - | ConcreteMode -> - (* There can't be abstractions if we run in concrete mode *) - failwith "Unreachable" - | SymbolicMode -> - (* TODO *) - raise Unimplemented) + | Abs _ :: _ -> + assert (config.mode = SymbolicMode); + raise Unimplemented let rec give_back_value_to_value config bid (v : typed_value) (destv : typed_value) : typed_value = @@ -173,10 +168,9 @@ let give_back_value_to_abs (_config : config) _bid _v _abs : abs = 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 -> failwith "Unreachable" - | SymbolicMode -> Abs (give_back_value_to_abs config bid v abs)) + | Abs abs -> + assert (config.mode = SymbolicMode); + Abs (give_back_value_to_abs config bid v abs) let rec give_back_shared_to_value (config : config) bid (destv : typed_value) : typed_value = @@ -237,13 +231,13 @@ let give_back_shared_to_abs _config _bid _abs : abs = (* TODO *) raise Unimplemented +(* TODO: merge this in the other functions *) 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 -> failwith "Unreachable" - | SymbolicMode -> Abs (give_back_shared_to_abs config bid abs)) + | Abs abs -> + assert (config.mode = SymbolicMode); + Abs (give_back_shared_to_abs config bid abs) let give_back_value (config : config) (bid : BorrowId.id) (v : typed_value) (env : env) : env = @@ -262,10 +256,9 @@ let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env = match end_borrow_get_borrow_in_env config l env0 with (* It is possible that we can't find a borrow in symbolic mode (ending * an abstraction may end several borrows at once *) - | NotFound, env -> ( - match config.mode with - | ConcreteMode -> failwith "Unreachable" - | SymbolicMode -> env) + | NotFound, env -> + assert (config.mode = SymbolicMode); + env (* If we found outer borrows: end those borrows first *) | Outer outer_borrows, env -> let env' = @@ -309,10 +302,9 @@ let lookup_loan_in_env_value (config : config) (l : BorrowId.id) (ev : env_value) : loan_content option = match ev with | Var (_, v) -> lookup_loan_in_value config l v - | Abs _ -> ( - match config.mode with - | ConcreteMode -> failwith "Unreachable" - | SymbolicMode -> None) + | Abs _ -> + assert (config.mode = SymbolicMode); + None (** Lookup a loan content from a borrow id. Note that we never lookup loans in the abstractions. @@ -393,10 +385,9 @@ 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 failwith "Unreachable" - else - let borrowed, env' = promote_in_env env in - (borrowed, Abs abs :: env') + assert (config.mode = SymbolicMode); + let borrowed, env' = promote_in_env env in + (borrowed, Abs abs :: env') in (* Apply *) promote_in_env env0 @@ -432,7 +423,8 @@ 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 failwith "Unreachable" else Abs abs + assert (config.mode = SymbolicMode); + Abs abs in List.map promote_in_env_value env0 @@ -546,7 +538,7 @@ let rec read_projection (config : config) (access : path_access) (env : env) (* Match on the projection element and the value *) match (pe, v.value) with (* Field projection *) - | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> ( + | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> (* Check that the projection is consistent with the current value *) (match (opt_variant_id, adt.variant_id) with | None, None -> () @@ -554,18 +546,14 @@ let rec read_projection (config : config) (access : path_access) (env : env) if vid <> vid' then failwith "Unreachable" | _ -> failwith "Unreachable"); (* Actually project *) - match FieldId.nth_opt adt.field_values field_id with - | None -> failwith "Unreachable" - | Some fv -> read_projection config access env p fv) + let fv = FieldId.nth adt.field_values field_id in + read_projection config access env p fv (* Tuples *) - | Field (ProjTuple _, field_id), Tuple values -> ( - match FieldId.nth_opt values field_id with - | 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 *) - | Field (ProjAdt (_, Some _variant_id), _), Bottom -> - Error (FailBottom (1 + List.length p', pe, v.ty)) + | Field (ProjTuple _, field_id), Tuple values -> + let fv = FieldId.nth values field_id in + read_projection config access env p fv + (* We can expand [Bottom] values only while *writing* to places *) + | _, Bottom -> failwith "Unreachable" (* Symbolic value: needs to be expanded *) | _, Symbolic sp -> assert (config.mode = SymbolicMode); @@ -588,9 +576,7 @@ let rec read_projection (config : config) (access : path_access) (env : env) (* Remaining cases: error. We enumerate all the value variants * on purpose, to make sure we statically catch errors if we * modify the [value] definition. *) - | ( _, - ( Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _ - | Loan _ ) ) -> + | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _ | Loan _) -> failwith "Unreachable") (* Entering loans failed *) | res -> res) @@ -624,33 +610,27 @@ let rec write_projection (config : config) (new_value : typed_value) | 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 -> failwith "Unreachable" - | Some fv -> ( - (* Update the field value *) - match write_projection config new_value p fv with - | Error err -> Error err - | Ok nfv -> - (* Reinsert the field value *) - let nvalues = - FieldId.update_nth adt.field_values field_id nfv - in - let nadt = Adt { adt with field_values = nvalues } in - Ok { v with value = nadt })) + let fv = FieldId.nth adt.field_values field_id in + (* Update the field value *) + match write_projection config new_value p fv with + | Error err -> Error err + | Ok nfv -> + (* Reinsert the field value *) + let nvalues = FieldId.update_nth adt.field_values field_id nfv in + let nadt = Adt { adt with field_values = nvalues } in + Ok { v with value = nadt }) (* Tuples *) | Field (ProjTuple _, field_id), Tuple values -> ( (* Project *) - match FieldId.nth_opt values field_id with - | None -> failwith "Unreachable" - | Some fv -> ( - (* Update the field value *) - match write_projection config new_value p fv with - | Error err -> Error err - | Ok nfv -> - (* Reinsert the field value *) - let nvalues = FieldId.update_nth values field_id nfv in - let ntuple = Tuple nvalues in - Ok { v with value = ntuple })) + let fv = FieldId.nth values field_id in + (* Update the field value *) + match write_projection config new_value p fv with + | Error err -> Error err + | Ok nfv -> + (* Reinsert the field value *) + let nvalues = FieldId.update_nth values field_id nfv in + let ntuple = Tuple nvalues in + Ok { v with value = ntuple }) (* If we reach Bottom, it may mean we need to expand an uninitialized * enumeration value *) | Field (ProjAdt (_, Some _variant_id), _), Bottom -> @@ -710,6 +690,32 @@ let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) : in write_in_env env0 +(** Auxiliary function to expand [Bottom] values + + During compilation, rustc desaggregates the ADT initializations. The + consequence is that the following rust code: + ``` + let x = Cons a b; + ``` + + Looks like this in MIR: + ``` + (x as Cons).0 = a; + (x as Cons).1 = b; + set_discriminant(x, 0); // If `Cons` is the variant of index 0 + ``` + + The consequence is that we may sometimes need to write fields to values + which are currently [Bottom]. When doing this, we first expand the value + to, say, [Cons Bottom Bottom] (note that field projection contains information + about which variant we should project to, which is why we *can* set the + variant index when writing one of its fields). +*) +(*let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector) + (p : place) (env : env) (remaining_pes : int) (pe : projection_elem) + (ty : ety) : env = + let *) + (** Update the environment to be able to read a place. When reading a place, we may be stuck along the way because some value @@ -734,7 +740,7 @@ let rec update_env_along_read_place (config : config) (access : path_access) (* Expand the symbolic value *) raise Unimplemented | FailBottom (remaining_pes, pe, ty) -> - (* Expand the "bottom" value, if possible *) - raise Unimplemented + (* We can't expand [Bottom] values while reading them *) + failwith "Unreachable" in update_env_along_read_place config access p env' |