diff options
| -rw-r--r-- | src/Interpreter.ml | 2 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 70 | ||||
| -rw-r--r-- | src/Values.ml | 10 |
3 files changed, 76 insertions, 6 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index a9a44b0f..fbb7ef9b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -81,7 +81,7 @@ module Test = struct let call_id = C.fresh_fun_call_id () in assert (call_id = V.FunCallId.zero); let empty_absl = - create_empty_abstractions_from_abs_region_groups call_id V.Synth + create_empty_abstractions_from_abs_region_groups call_id V.SynthInput inst_sg.A.regions_hierarchy in (* Add the avalues to the abstractions and insert them in the context *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 57f43b4e..be2231a3 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -273,6 +273,18 @@ let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : in parents +(** Small utility: same as [list_parent_region_groups], but returns an ordered list *) +let list_ordered_parent_region_groups (def : A.fun_def) + (gid : T.RegionGroupId.id) : T.RegionGroupId.id list = + let pset = list_parent_region_groups def gid in + let parents = + List.filter + (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset) + def.signature.regions_hierarchy + in + let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in + parents + let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) (bid : V.BackwardFunctionId.id option) : fun_sig = let sg = def.signature in @@ -348,6 +360,19 @@ let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) (* Return *) { type_params; inputs; outputs } +(** Translate a typed value. + + **IMPORTANT**: this function makes the assumption that the typed value + doesn't contain ⊥. This means in particular that symbolic values don't + contain ended regions. + + TODO: we might want to remember in the symbolic AST the set of ended + regions, at the points where we need it, for sanity checks. + The points where we need this set so far: + - function call + - end abstraction + - return + *) let translate_typed_value (ctx : bs_ctx) (v : V.typed_value) : typed_value = raise Unimplemented @@ -369,6 +394,29 @@ let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } let type_def_is_enum (def : type_def) : bool = match def.kind with Struct _ -> false | Enum _ -> true +let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) : + typed_value option = + raise Unimplemented + +let typed_avalue_to_given_back (ctx : bs_ctx) (av : V.typed_avalue) : + typed_value option = + raise Unimplemented + +let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_value list = + List.filter_map (typed_avalue_to_consumed ctx) abs.avalues + +let abs_to_given_back (ctx : bs_ctx) (abs : V.abs) : typed_value list = + List.filter_map (typed_avalue_to_given_back ctx) abs.avalues + +(** Return the ordered list of the (transitive) parents of a given abstraction. + + Is used for instance when collecting the input values given to all the + parent functions, in order to properly instantiate an + *) +let get_abs_ordered_parents (ctx : bs_ctx) (call_id : S.call_id) + (gid : T.RegionGroupId.id) : S.call * V.abs list = + raise Unimplemented + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = match e with | S.Return v -> @@ -393,12 +441,32 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = let e = translate_expression e ctx in (* Put together *) Let (Call ([ Var dest ], call), e) - | EndAbstraction (abs, e) -> raise Unimplemented + | EndAbstraction (abs, e) -> translate_end_abstraction abs e | Expansion (sv, exp) -> translate_expansion sv exp ctx | Meta (_, e) -> (* We ignore the meta information *) translate_expression e ctx +and translate_end_abstraction (abs : V.abs) (e : S.expression) : expression = + match abs.kind with + | V.SynthInput -> + (* There are no nested borrows for now: we shouldn't get there *) + raise Unimplemented + | V.FunCall -> + (* Retrive the orignal call and the parent abstractions *) + (* Retrieve the values consumed when we called the forward function and + * ended the parent backward functions: those give us part of the input + * values *) + (* Retrieve the values consumed upon ending the loans inside this + * abstraction: those give us the remaining input values *) + (* Retrieve the values given back by this function: those are the output + * values *) + (* Put everything together *) + raise Unimplemented + | V.SynthRet -> + (* *) + raise Unimplemented + and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : expression = (* Translate the scrutinee *) diff --git a/src/Values.ml b/src/Values.ml index bccb5134..a905c8d3 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -722,10 +722,12 @@ and typed_avalue = { value : avalue; ty : rty } (** The kind of an abstraction, which keeps track of its origin *) type abs_kind = | FunCall (** The abstraction was introduced because of a function call *) - | Synth - (** The abstraction is used to keep track of the input/return value of - the function we are currently synthesizing. - *) + | SynthInput + (** The abstraction keeps track of the input values of the function + we are currently synthesizing. *) + | SynthRet + (** The abstraction "absorbed" the value returned by the function we + are currently synthesizing *) [@@deriving show] type abs = { |