diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 8 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 35 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 8 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 10 | ||||
| -rw-r--r-- | src/Values.ml | 28 |
7 files changed, 65 insertions, 30 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2f0f52af..8cab8c47 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -67,7 +67,9 @@ module Test = struct let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in (* Create fresh symbolic values for the inputs *) let input_svs = - List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs + List.map + (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) + inst_sg.inputs in (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let empty_absl = diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index faa63c0a..9d332543 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -746,8 +746,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) be expanded (because expanding this symbolic value would require expanding a reference whose region has already ended). *) -let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value = - mk_fresh_symbolic_typed_value av.V.ty +let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value = + mk_fresh_symbolic_typed_value V.FunCallGivenBack av.V.ty (** End a borrow identified by its borrow id in a context @@ -1129,7 +1129,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) match bc with | V.AMutBorrow (bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) - let v = convert_avalue_to_value av in + let v = convert_avalue_to_given_back_value av in give_back_value config bid v ctx | V.ASharedBorrow bid -> give_back_shared config bid ctx | V.AProjSharedBorrow _ -> @@ -1148,7 +1148,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) V.AEndedProjBorrows ctx in (* Give back a fresh symbolic value *) - let nsv = mk_fresh_symbolic_value proj_ty in + let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in let ctx = give_back_symbolic_value config abs.regions proj_ty sv nsv ctx in diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 8f560083..8b039510 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -217,8 +217,9 @@ let apply_symbolic_expansion_non_borrow (config : C.config) doesn't allow the expansion of enumerations *containing several variants*. *) let compute_expanded_symbolic_adt_value (expand_enumerations : bool) - (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list) - (types : T.rty list) (ctx : C.eval_ctx) : symbolic_expansion list = + (kind : V.sv_kind) (def_id : T.TypeDefId.id) + (regions : T.RegionId.id T.region list) (types : T.rty list) + (ctx : C.eval_ctx) : symbolic_expansion list = (* Lookup the definition and check if it is an enumeration with several * variants *) let def = C.ctx_lookup_type_def ctx def_id in @@ -235,7 +236,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) ((variant_id, field_types) : T.VariantId.id option * T.rty list) : symbolic_expansion = let field_values = - List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value ty) field_types + List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types in let see = SeAdt (variant_id, field_values) in see @@ -243,20 +244,20 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (* Initialize all the expanded values of all the variants *) List.map initialize variants_fields_types -let compute_expanded_symbolic_tuple_value (field_types : T.rty list) : - symbolic_expansion = +let compute_expanded_symbolic_tuple_value (kind : V.sv_kind) + (field_types : T.rty list) : symbolic_expansion = (* Generate the field values *) let field_values = - List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types + List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types in let variant_id = None in let see = SeAdt (variant_id, field_values) in see -let compute_expanded_symbolic_box_value (boxed_ty : T.rty) : symbolic_expansion - = +let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : + symbolic_expansion = (* Introduce a fresh symbolic value *) - let boxed_value = mk_fresh_symbolic_value boxed_ty in + let boxed_value = mk_fresh_symbolic_value kind boxed_ty in let see = SeAdt (None, [ boxed_value ]) in see @@ -360,7 +361,7 @@ let expand_symbolic_value_shared_borrow (config : C.config) (* Finally, replace the projectors on loans *) let bids = !borrows in assert (not (V.BorrowId.Set.is_empty bids)); - let shared_sv = mk_fresh_symbolic_value ref_ty in + let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in let see = SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = @@ -382,7 +383,7 @@ let expand_symbolic_value_borrow (config : C.config) | T.Mut -> (* Simple case: simply create a fresh symbolic value and a fresh * borrow id *) - let sv = mk_fresh_symbolic_value ref_ty in + let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in let bid = C.fresh_borrow_id () in let see = SeMutRef (bid, sv) in (* Expand the symbolic values - we simply perform a substitution (and @@ -424,8 +425,8 @@ let expand_symbolic_value_no_branching (config : C.config) * don't allow to expand enumerations with strictly more than one variant *) let expand_enumerations = false in match - compute_expanded_symbolic_adt_value expand_enumerations def_id regions - types ctx + compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind + def_id regions types ctx with | [ see ] -> (* Apply in the context *) @@ -443,7 +444,7 @@ let expand_symbolic_value_no_branching (config : C.config) (* Tuples *) | T.Adt (T.Tuple, [], tys) -> (* Generate the field values *) - let see = compute_expanded_symbolic_tuple_value tys in + let see = compute_expanded_symbolic_tuple_value sp.sv_kind tys in (* Apply in the context *) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx @@ -454,7 +455,7 @@ let expand_symbolic_value_no_branching (config : C.config) ctx (* Boxes *) | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - let see = compute_expanded_symbolic_box_value boxed_ty in + let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in (* Apply in the context *) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx @@ -500,8 +501,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value) * don't allow to expand enumerations with strictly more than one variant *) let expand_enumerations = true in let seel = - compute_expanded_symbolic_adt_value expand_enumerations def_id regions - types ctx + compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind + def_id regions types ctx in (* Update the synthesized program *) S.synthesize_symbolic_expansion_enum_branching original_sv seel; diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index f577a190..2390aa48 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -242,7 +242,9 @@ let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx) | E.Neg, T.Integer int_ty -> T.Integer int_ty | _ -> failwith "Invalid input for unop" in - let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in + let res_sv = + { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + in (* Synthesize *) S.synthesize_unary_op unop v res_sv; (* Return *) @@ -360,7 +362,9 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx) | E.Ne | E.Eq -> failwith "Unreachable") | _ -> failwith "Invalid inputs for binop" in - let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in + let res_sv = + { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty } + in (* Synthesize *) S.synthesize_binary_op binop v1 v2 res_sv; (* Return *) diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 8b29bac9..e92b1c0b 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -885,7 +885,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (args : E.operand list) (dest : E.place) : C.eval_ctx = (* Generate a fresh symbolic value for the return value *) let ret_sv_ty = inst_sg.A.output in - let ret_spc = mk_fresh_symbolic_value ret_sv_ty in + let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in let ret_value = mk_typed_value_from_symbolic_value ret_spc in let ret_av regions = mk_aproj_loans_value_from_symbolic_value regions ret_spc diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 971dc801..e00e7dcf 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -53,16 +53,18 @@ let mk_place_from_var_id (var_id : V.VarId.id) : E.place = { var_id; projection = [] } (** Create a fresh symbolic value *) -let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value = +let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.rty) : + V.symbolic_value = let sv_id = C.fresh_symbolic_value_id () in - let svalue = { V.sv_id; V.sv_ty = ty } in + let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in svalue (** Create a fresh symbolic value *) -let mk_fresh_symbolic_typed_value (rty : T.rty) : V.typed_value = +let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) : + V.typed_value = let ty = Subst.erase_regions rty in (* Generate the fresh a symbolic value *) - let value = mk_fresh_symbolic_value rty in + let value = mk_fresh_symbolic_value sv_kind rty in let value = V.Symbolic value in { V.value; V.ty } diff --git a/src/Values.ml b/src/Values.ml index 59cfbdca..856ccb6f 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -45,7 +45,33 @@ type constant_value = | String of string [@@deriving show] -type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty } +(** The kind of a symbolic value, which precises how the value was generated *) +type sv_kind = + | FunCallRet (** The value is the return value of a function call *) + | FunCallGivenBack + (** The value is a borrowed value given back by an abstraction + (happens when giving a borrow to a function: when the abstraction + introduced to model the function call ends we reintroduce a symbolic + value in the context for the value modified by the abstraction through + the borrow). + *) + | SynthInput + (** The value is an input value of the function whose body we are + currently synthesizing. + *) + | SynthGivenBack + (** The value is a borrowed value that the function whose body we are + synthesizing returned, and which was given back because we ended + one of the lifetimes of this function (we do this to synthesize + the backward functions). + *) +[@@deriving show] + +type symbolic_value = { + sv_kind : sv_kind; + sv_id : SymbolicValueId.id; + sv_ty : rty; +} [@@deriving show] (** A symbolic value *) |