From 42da25ddae3deb8df125ca5d1963a0b40d683c2a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 25 Jan 2022 18:49:11 +0100 Subject: Make progress on SymbolicToPure.translate_end_abstraction --- src/InterpreterStatements.ml | 6 +- src/Pure.ml | 8 +- src/SymbolicAst.ml | 1 + src/SymbolicToPure.ml | 192 ++++++++++++++++++++++++++++++++++--------- src/SynthesizeSymbolic.ml | 19 +++-- src/Values.ml | 8 +- 6 files changed, 182 insertions(+), 52 deletions(-) (limited to 'src') diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index ef2c069d..59d2c4da 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -673,6 +673,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) V.abs = let abs_id = rg.T.id in let back_id = Some back_id in + let original_parents = rg.parents in let parents = List.fold_left (fun s pid -> V.AbstractionId.Set.add pid s) @@ -703,6 +704,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) back_id; kind; parents; + original_parents; regions; ancestors_regions; avalues = []; @@ -1060,7 +1062,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let expr = cf ctx in (* Synthesize the symbolic AST *) - S.synthesize_regular_function_call fid call_id type_params args ret_spc expr + let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in + S.synthesize_regular_function_call fid call_id abs_ids type_params args + ret_spc expr in let cc = comp cc cf_call in diff --git a/src/Pure.ml b/src/Pure.ml index a0c8d70c..869729a1 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -95,6 +95,7 @@ type projection = projection_elem list type place = { var : VarId.id; projection : projection } +(* TODO: this doesn't make sense: value can contain variables... *) type operand = Value of typed_value | Place of place (* type assertion = { cond : operand; expected : bool } *) @@ -112,9 +113,12 @@ type call = { func : fun_id; type_params : ty list; args : operand list } type left_value = unit (** TODO: assignment left value *) +type lvalue = typed_value +(* TODO: define that *) + type let_bindings = - | Call of var_or_dummy list * call - (** The called function and the tuple of returned values *) + | Call of lvalue list * call + (** The called function and the tuple of returned values. *) | Assignment of var * operand (** Variable assignment: the introduced variable and the place we read *) | Deconstruct of diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 45cdc4b2..9dc20468 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -18,6 +18,7 @@ type call_id = type call = { call_id : call_id; + abstractions : V.AbstractionId.id list; type_params : T.ety list; args : V.typed_value list; dest : V.symbolic_value; diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 11d7a657..97d9baf1 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -99,10 +99,14 @@ let translate_type_name (def : T.type_def) : Id.name = def.T.name type type_context = { types_infos : TA.type_infos; + cfim_type_defs : T.type_def TypeDefId.Map.t; type_defs : type_def TypeDefId.Map.t; } -type fun_context = { fun_defs : fun_def FunDefId.Map.t } +type fun_context = { + cfim_fun_defs : A.fun_def FunDefId.Map.t; + fun_defs : fun_def FunDefId.Map.t; +} (* TODO: do we really need that actually? *) type synth_ctx = { @@ -113,15 +117,57 @@ type synth_ctx = { declarations : M.declaration_group list; } +type call_info = { + forward : S.call; + backwards : V.abs T.RegionGroupId.Map.t; + (** TODO: not sure we need this anymore *) +} +(** Whenever we translate a function call or an ended abstraction, we + store the related information (this is useful when translating ended + children abstractions) + *) + type bs_ctx = { type_context : type_context; + fun_context : fun_context; fun_def : A.fun_def; bid : T.RegionGroupId.id option; + calls : call_info V.FunCallId.Map.t; + abstractions : V.abs V.AbstractionId.Map.t; } (** Body synthesis context *) -let bs_ctx_lookup_type_def (id : TypeDefId.id) (ctx : bs_ctx) : type_def = - TypeDefId.Map.find id ctx.type_context.type_defs +(*let bs_ctx_lookup_type_def (id : TypeDefId.id) (ctx : bs_ctx) : type_def = + TypeDefId.Map.find id ctx.type_context.type_defs*) +let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def + = + TypeDefId.Map.find id ctx.type_context.cfim_type_defs + +let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def = + FunDefId.Map.find id ctx.fun_context.cfim_fun_defs + +let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) + (ctx : bs_ctx) : bs_ctx = + let calls = ctx.calls in + assert (not (V.FunCallId.Map.mem call_id calls)); + let info = { forward; backwards = T.RegionGroupId.Map.empty } in + let calls = V.FunCallId.Map.add call_id info calls in + { ctx with calls } + +let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx = + (* Insert the abstraction in the call informations *) + let back_id = Option.get abs.back_id in + let info = V.FunCallId.Map.find abs.call_id ctx.calls in + assert (not (T.RegionGroupId.Map.mem back_id info.backwards)); + let backwards = T.RegionGroupId.Map.add back_id abs info.backwards in + let info = { info with backwards } in + let calls = V.FunCallId.Map.add abs.call_id info ctx.calls in + (* Insert the abstraction in the abstractions map *) + let abstractions = ctx.abstractions in + assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions)); + let abstractions = V.AbstractionId.Map.add abs.abs_id abs abstractions in + (* Update the context *) + { ctx with calls; abstractions } let rec translate_sty (ty : T.sty) : ty = let translate = translate_sty in @@ -256,6 +302,8 @@ let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) (** Small utility: list the transitive parents of a region var group. We don't do that in an efficient manner, but it doesn't matter. + + TODO: remove? *) let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) : T.RegionGroupId.Set.t = @@ -273,7 +321,10 @@ 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 *) +(** Small utility: same as [list_parent_region_groups], but returns an ordered list. + + TODO: remove? + *) 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 @@ -285,6 +336,30 @@ let list_ordered_parent_region_groups (def : A.fun_def) let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in parents +let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) : + V.AbstractionId.id list = + (* We could do something more "elegant" without references, but it is + * so much simpler to use references... *) + let abs_set = ref V.AbstractionId.Set.empty in + let rec gather (abs_id : V.AbstractionId.id) : unit = + if V.AbstractionId.Set.mem abs_id !abs_set then () + else ( + abs_set := V.AbstractionId.Set.add abs_id !abs_set; + let abs = V.AbstractionId.Map.find abs_id ctx.abstractions in + List.iter gather abs.original_parents) + in + gather abs.abs_id; + let ids = !abs_set in + (* List the ancestors, in the proper order *) + let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in + List.filter + (fun id -> V.AbstractionId.Set.mem id ids) + call_info.forward.abstractions + +let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : V.abs list = + let abs_ids = list_ancestor_abstractions_ids ctx abs in + List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids + let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def) (bid : T.RegionGroupId.id option) : fun_sig = let sg = def.signature in @@ -390,31 +465,38 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } (* TODO: move *) -let type_def_is_enum (def : type_def) : bool = - match def.kind with Struct _ -> false | Enum _ -> true +let type_def_is_enum (def : T.type_def) : bool = + match def.kind with T.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 +let typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) : + bs_ctx * lvalue option = + raise Unimplemented + +let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * lvalue list = + let ctx, values = + List.fold_left_map + (fun ctx av -> typed_avalue_to_given_back av ctx) + ctx abs.avalues + in + let values = List.filter_map (fun x -> x) values in + (ctx, values) (** 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 get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list = + let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in + let abs_ancestors = list_ancestor_abstractions ctx abs in + (call_info.forward, abs_ancestors) let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = match e with @@ -422,46 +504,71 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression = let v = translate_typed_value ctx v in Return (Value v) | Panic -> Panic - | FunCall (call, e) -> - (* Translate the function call *) - let type_params = List.map (translate_fwd_ty ctx) call.type_params in - let args = List.map (translate_typed_value ctx) call.args in - let args = List.map (fun v -> Value v) args in - let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in - let func = - match call.call_id with - | S.Fun (A.Local fid, _) -> Local (fid, None) - | S.Fun (A.Assumed fid, _) -> Assumed fid - | S.Unop unop -> Unop unop - | S.Binop binop -> Binop binop - in - let call = { func; type_params; args } in - (* Translate the next expression *) - let e = translate_expression e ctx in - (* Put together *) - Let (Call ([ Var dest ], call), e) - | EndAbstraction (abs, e) -> translate_end_abstraction abs e + | FunCall (call, e) -> translate_function_call call e ctx + | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx | 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 = +and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : + expression = + (* Translate the function call *) + let type_params = List.map (translate_fwd_ty ctx) call.type_params in + let args = List.map (translate_typed_value ctx) call.args in + let args = List.map (fun v -> Value v) args in + let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in + (* Retrieve the function id, and register the function call in the context + * if necessary *) + let ctx, func = + match call.call_id with + | S.Fun (fid, call_id) -> + let ctx = bs_ctx_register_forward_call call_id call ctx in + let func = + match fid with + | A.Local fid -> Local (fid, None) + | A.Assumed fid -> Assumed fid + in + (ctx, func) + | S.Unop unop -> (ctx, Unop unop) + | S.Binop binop -> (ctx, Binop binop) + in + let call = { func; type_params; args } in + (* Translate the next expression *) + let e = translate_expression e ctx in + (* Put together *) + Let (Call ([ Var dest ], call), e) + +and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : + 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 *) + let forward, backwards = get_abs_ancestors ctx abs in (* Retrieve the values consumed when we called the forward function and * ended the parent backward functions: those give us part of the input * values *) + let fwd_inputs = List.map (translate_typed_value ctx) forward.args in + let back_ancestors_inputs = + List.concat (List.map abs_to_consumed backwards) + in (* Retrieve the values consumed upon ending the loans inside this * abstraction: those give us the remaining input values *) + let back_inputs = abs_to_consumed abs in + let inputs = + List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ] + in (* Retrieve the values given back by this function: those are the output * values *) + let ctx, outputs = abs_to_given_back abs ctx in + (* Translate the next expression *) + let e = translate_expression e ctx in (* Put everything together *) - raise Unimplemented + let call = { func; type_params; args = inputs } in + Let (Call (outputs, call), e) | V.SynthRet -> (* *) raise Unimplemented @@ -499,7 +606,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) match type_id with | T.AdtId adt_id -> (* Detect if this is an enumeration or not *) - let tdef = bs_ctx_lookup_type_def adt_id ctx in + let tdef = bs_ctx_lookup_cfim_type_def adt_id ctx in let is_enum = type_def_is_enum tdef in if is_enum then (* This is an enumeration: introduce an [ExpandEnum] let-binding *) @@ -568,9 +675,14 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) let otherwise = translate_expression otherwise ctx in Switch (scrutinee, SwitchInt (int_ty, branches, otherwise)) -let translate_fun_def (type_context : type_context) (def : A.fun_def) - (bid : T.RegionGroupId.id option) (body : S.expression) : fun_def = - let bs_ctx = { type_context; fun_def = def; bid } in +let translate_fun_def (type_context : type_context) (fun_context : fun_context) + (def : A.fun_def) (bid : T.RegionGroupId.id option) (body : S.expression) : + fun_def = + let calls = V.FunCallId.Map.empty in + let abstractions = V.AbstractionId.Map.empty in + let bs_ctx = + { type_context; fun_context; fun_def = def; bid; calls; abstractions } + in (* Translate the function *) let def_id = def.A.def_id in let name = translate_fun_name def bid in diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml index c0d4489c..d578a13e 100644 --- a/src/SynthesizeSymbolic.ml +++ b/src/SynthesizeSymbolic.ml @@ -81,29 +81,32 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) let exprl = match expr with None -> None | Some expr -> Some [ expr ] in synthesize_symbolic_expansion sv [ Some see ] exprl -let synthesize_function_call (call_id : call_id) (type_params : T.ety list) +let synthesize_function_call (call_id : call_id) + (abstractions : V.AbstractionId.id list) (type_params : T.ety list) (args : V.typed_value list) (dest : V.symbolic_value) (expr : expression option) : expression option = match expr with | None -> None | Some expr -> - let call = { call_id; type_params; args; dest } in + let call = { call_id; abstractions; type_params; args; dest } in Some (FunCall (call, expr)) let synthesize_regular_function_call (fun_id : A.fun_id) - (call_id : V.FunCallId.id) (type_params : T.ety list) - (args : V.typed_value list) (dest : V.symbolic_value) - (expr : expression option) : expression option = - synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr + (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list) + (type_params : T.ety list) (args : V.typed_value list) + (dest : V.symbolic_value) (expr : expression option) : expression option = + synthesize_function_call + (Fun (fun_id, call_id)) + abstractions type_params args dest expr let synthesize_unary_op (unop : E.unop) (arg : V.typed_value) (dest : V.symbolic_value) (expr : expression option) : expression option = - synthesize_function_call (Unop unop) [] [ arg ] dest expr + synthesize_function_call (Unop unop) [] [] [ arg ] dest expr let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value) (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option) : expression option = - synthesize_function_call (Binop binop) [] [ arg0; arg1 ] dest expr + synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr let synthesize_aggregated_value (aggr_v : V.typed_value) (expr : expression option) : expression option = diff --git a/src/Values.ml b/src/Values.ml index cc458bca..6378269f 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -737,12 +737,18 @@ type abs = { symbolic AST, generated by the symbolic execution. *) back_id : (RegionGroupId.id option[@opaque]); - (** The id of the backward function to which this abstraction is linked. + (** The id of the backward function to which this abstraction is linked, + if there is one. Note that it may not be the case, when introducing + abstractions to handle the input values for the function we are + synthesizing for instance. TODO: actually should never be None. + This is not used by the symbolic execution: it is a utility for the symbolic AST, generated by the symbolic execution. *) kind : (abs_kind[@opaque]); parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *) + original_parents : (AbstractionId.id list[@opaque]); + (** The original list of parents, ordered. This is used for synthesis. *) regions : (RegionId.Set.t[@opaque]); (** Regions owned by this abstraction *) ancestors_regions : (RegionId.Set.t[@opaque]); (** Union of the regions owned by this abstraction's ancestors (not -- cgit v1.2.3