diff options
| -rw-r--r-- | src/Pure.ml | 86 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 73 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 4 | ||||
| -rw-r--r-- | src/Values.ml | 10 | ||||
| -rw-r--r-- | src/main.ml | 32 |
5 files changed, 75 insertions, 130 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 02b821ef..e7721b41 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -12,16 +12,6 @@ module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId module FunDeclId = A.FunDeclId -module MPlaceId = IdGen () -(** A meta-place identifier. See [mplace]. *) - -(** Some global counters - TODO: remove *) - -let mplace_id_counter, fresh_mplace_id = MPlaceId.fresh_stateful_generator () - -(** Reset the mplace counter *) -let reset_pure_counters () = mplace_id_counter := MPlaceId.generator_zero - module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward for group of regions 0, etc.) *) @@ -297,74 +287,6 @@ and typed_rvalue = { value : rvalue; ty : ty } polymorphic = false; }] -(** Meta destination place. - - Meta information for places used as assignment destinations. - Either a regular mplace, or an mplace derived from another mplace. - - The second case is used for values given back by backward function: we - remember the identifier of the place from which the input argument was - taken from. - - Ex.: - ==== - ``` - let y = f<'a>(&mut x); - ... - // end 'a - ... - ``` - gets translated to: - ``` - let y = f_fwd xv in - ... - let s = f_back xv y_i in // we want the introduced variable to be name "x" - ... - ``` - In order to compute a proper name for the variable introduced by the backward - call, we need to link `s` to `x`. However, because of desugaring, it may happen - that the fact `f` takes `x` as argument may have to be computed by propagating - naming information. We use place identifiers to link the output variables to the - input arguments: it allows us to propagate naming constraints "across" function - calls. - - The full details are given in [PureMicroPasses.compute_pretty_names] - *) -type mdplace = Regular of mplace | From of MPlaceId.id [@@deriving show] - -(** Ancestor for [iter_var_or_dummy] visitor *) -class ['self] iter_var_or_dummy_base = - object (_self : 'self) - inherit [_] iter_typed_rvalue - - method visit_mdplace : 'env -> mdplace -> unit = fun _ _ -> () - end - -(** Ancestor for [map_var_or_dummy] visitor *) -class ['self] map_var_or_dummy_base = - object (_self : 'self) - inherit [_] map_typed_rvalue - - method visit_mdplace : 'env -> mdplace -> mdplace = fun _ x -> x - end - -(** Ancestor for [reduce_var_or_dummy] visitor *) -class virtual ['self] reduce_var_or_dummy_base = - object (self : 'self) - inherit [_] reduce_typed_rvalue - - method visit_mdplace : 'env -> mdplace -> 'a = fun _ _ -> self#zero - end - -(** Ancestor for [mapreduce_var_or_dummy] visitor *) -class virtual ['self] mapreduce_var_or_dummy_base = - object (self : 'self) - inherit [_] mapreduce_typed_rvalue - - method visit_mdplace : 'env -> mdplace -> mdplace * 'a = - fun _ x -> (x, self#zero) - end - type var_or_dummy = | Var of var * mplace option (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections). @@ -379,7 +301,7 @@ type var_or_dummy = { name = "iter_var_or_dummy"; variety = "iter"; - ancestors = [ "iter_var_or_dummy_base" ]; + ancestors = [ "iter_typed_rvalue" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; @@ -388,7 +310,7 @@ type var_or_dummy = { name = "map_var_or_dummy"; variety = "map"; - ancestors = [ "map_var_or_dummy_base" ]; + ancestors = [ "map_typed_rvalue" ]; nude = true (* Don't inherit [VisitorsRuntime.map] *); concrete = true; polymorphic = false; @@ -397,7 +319,7 @@ type var_or_dummy = { name = "reduce_var_or_dummy"; variety = "reduce"; - ancestors = [ "reduce_var_or_dummy_base" ]; + ancestors = [ "reduce_typed_rvalue" ]; nude = true (* Don't inherit [VisitorsRuntime.reduce] *); polymorphic = false; }, @@ -405,7 +327,7 @@ type var_or_dummy = { name = "mapreduce_var_or_dummy"; variety = "mapreduce"; - ancestors = [ "mapreduce_var_or_dummy_base" ]; + ancestors = [ "mapreduce_typed_rvalue" ]; nude = true (* Don't inherit [VisitorsRuntime.reduce] *); polymorphic = false; }] diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index a963e628..bc4cdc3c 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -112,7 +112,9 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator = type pn_ctx = { pure_vars : string VarId.Map.t; + (** Information about the pure variables used in the synthesized program *) llbc_vars : string V.VarId.Map.t; + (** Information about the LLBC variables used in the original program *) } (** "pretty-name context": see [compute_pretty_names] *) @@ -125,9 +127,10 @@ type pn_ctx = { - whenever we see an rvalue/lvalue which is exactly an unnamed variable, and this value is linked to some meta-place information which contains a name and an empty path, we consider we should use this name - - for the values given back by backward functions, we link the given back - values to the places (identified by unique indices) where the input - arguments come from (see examples below) + - we try to propagate naming constraints on the pure variables use in the + synthesized programs, and also on the LLBC variables from the original + program (information about the LLBC variables is stored in the meta-places) + Something important is that, for every variable we find, the name of this variable can be influenced by the information we find *below* in the AST. @@ -176,6 +179,13 @@ type pn_ctx = { | Cons x hd -> ... | ... ``` + - Assignments: + `let x [@mplace=lp] = v [@mplace = rp} in ...` + + We propagate naming information across the assignments. This is important + because many reassignments using temporary, anonymous variables are + introduced during desugaring. + - Given back values (introduced by backward functions): Let's say we have the following Rust code: ``` @@ -204,15 +214,13 @@ type pn_ctx = { so we should use "x" as the basename (hence the resulting name "x1"). However, this is non-trivial, because after desugaring the input argument given to `id` is not `&mut x` but `move ^0` (i.e., it comes from a temporary, anonymous - variable). For this reason, we give unique identifiers to places, link - given back values to the places where the input arguments come from, and - propagate naming information between the places. + variable). For this reason, we use the meta-place "&mut x" as the meta-place + for the given back value (this is done during the synthesis), and propagate + naming information *also* on the LLBC variables (which are referenced by the + meta-places). This way, because of `^0 = &mut x`, we can propagate the name "x" to the place `^0`, then to the given back variable across the function call. - - - TODO: inputs and end abstraction... - *) let compute_pretty_names (def : fun_decl) : fun_decl = @@ -252,7 +260,20 @@ let compute_pretty_names (def : fun_decl) : fun_decl = List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs in - let add_var (ctx : pn_ctx) (v : var) : pn_ctx = + (* + * The way we do is as follows: + * - we explore the expressions + * - we register the variables introduced by the let-bindings + * - we use the naming information we find (through the variables and the + * meta-places) to update our context (i.e., maps from variable ids to + * names) + * - we use this information to update the names of the variables used in the + * expressions + *) + + (* Register a variable for constraints propagation - used when an variable is + * introduced (left-hand side of a left binding) *) + let register_var (ctx : pn_ctx) (v : var) : pn_ctx = assert (not (VarId.Map.mem v.id ctx.pure_vars)); match v.basename with | None -> ctx @@ -260,6 +281,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let pure_vars = VarId.Map.add v.id name ctx.pure_vars in { ctx with pure_vars } in + (* Update a variable - used to update an expression after we computed constraints *) let update_var (ctx : pn_ctx) (v : var) (mp : mplace option) : var = match v.basename with | Some _ -> v @@ -275,6 +297,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Some basename -> { v with basename = Some basename } else v) in + (* Update an lvalue - used to update an expression after we computed constraints *) let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue = let obj = object @@ -286,6 +309,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = obj#visit_typed_lvalue () lv in + (* Register an mplace the first time we find one *) let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx = match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with | None, Some name -> @@ -294,6 +318,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | _ -> ctx in + (* Register the fact that [name] can be used for the pure variable identified + * by [var_id] (will add this name in the map if the variable is anonymous) *) let add_pure_var_constraint (var_id : VarId.id) (name : string) (ctx : pn_ctx) : pn_ctx = let pure_vars = @@ -302,6 +328,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = in { ctx with pure_vars } in + (* Similar to [add_pure_var_constraint], but for LLBC variables *) let add_llbc_var_constraint (var_id : V.VarId.id) (name : string) (ctx : pn_ctx) : pn_ctx = let llbc_vars = @@ -310,6 +337,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl = in { ctx with llbc_vars } in + (* Add a constraint: given a variable id and an associated meta-place, try to + * extract naming information from the meta-place and save it *) let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx = (* Register the place *) let ctx = register_mplace mp ctx in @@ -322,6 +351,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = ctx | _ -> ctx in + (* Specific case of constraint on rvalues *) let add_right_constraint (mp : mplace) (rv : typed_rvalue) (ctx : pn_ctx) : pn_ctx = (* Register the place *) @@ -333,6 +363,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (ctx : pn_ctx) : pn_ctx = match mp with None -> ctx | Some mp -> add_right_constraint mp rv ctx in + (* Specific case of constraint on left values *) let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx = let obj = object (self) @@ -344,7 +375,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = method! visit_Var _ v mp () = (* Register the variable *) - let ctx = add_var (self#zero ()) v in + let ctx = register_var (self#zero ()) v in (* Register the mplace information if there is such information *) match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx end @@ -354,7 +385,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl = in (* This is used to propagate constraint information about places in case of - * assignments *) + * variable reassignments: we try to propagate the information from the + * rvalue to the left *) let add_left_right_constraint (lv : typed_lvalue) (re : texpression) (ctx : pn_ctx) : pn_ctx = (* We propagate constraints across variable reassignments: `^0 = x`, @@ -403,23 +435,6 @@ let compute_pretty_names (def : fun_decl) : fun_decl = ctx | _ -> ctx) | _ -> ctx - (* match (lv.value, re.e) with - (* Case 1: *) - | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), - Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) -> - (* Use the meta-information on the right *) - add_constraint rmp lvar.id ctx - (* Case 2: *) - | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), - Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _) - ) -> ( - (* Use the variable name *) - match - (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx) - with - | None, Some name -> VarId.Map.add lvar.id name ctx - | _ -> ctx) - | _ -> (* Nothing to propagate *) ctx *) in (* *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 65bdcf9c..e32e28d6 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -640,7 +640,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (translate mv).value | V.InactivatedMutBorrow (mv, _) -> (* Same as for shared borrows. However, note that we use inactivated borrows - * only in meta-data: a value actually used in the translation can't come + * only in meta-data: a value actually *used in the translation* can't come * from an unpromoted inactivated borrow *) (translate mv).value | V.MutBorrow (_, v) -> @@ -1451,8 +1451,6 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let translate_fun_decl (config : config) (ctx : bs_ctx) (body : S.expression option) : fun_decl = - (* Reset the counters *) - reset_pure_counters (); (* Translate *) let def = ctx.fun_decl in let bid = ctx.bid in diff --git a/src/Values.ml b/src/Values.ml index 3f1fc0bd..4799f3b9 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -173,6 +173,16 @@ and borrow_content = The meta-value is used for the same purposes as with shared borrows, at the exception that in case of inactivated borrows it is not *necessary* for the synthesis: we keep it only as meta-information. + To be more precise: + - when generating the synthesized program, we may need to convert + shared borrows to pure values + - we never need to do so for inactivated borrows: such borrows must + be activated at the moment we use them (meaning we convert a *mutable* + borrow to a pure value). However, we save meta-data about the assignments, + which is used to make the code cleaner: when generating this meta-data, + we may need to convert inactivated borrows to pure values, in which + situation we convert the meta-value we stored in the inactivated + borrow. *) and loan_content = diff --git a/src/main.ml b/src/main.ml index 943689be..00693890 100644 --- a/src/main.ml +++ b/src/main.ml @@ -122,22 +122,22 @@ let () = (* Set up the logging - for now we use default values - TODO: use the * command-line arguments *) - Easy_logging.Handlers.set_level main_logger_handler EL.Debug; - main_log#set_level EL.Debug; - llbc_of_json_logger#set_level EL.Debug; - pre_passes_log#set_level EL.Debug; - interpreter_log#set_level EL.Debug; - statements_log#set_level EL.Debug; - paths_log#set_level EL.Debug; - expressions_log#set_level EL.Debug; - expansion_log#set_level EL.Debug; - borrows_log#set_level EL.Debug; - invariants_log#set_level EL.Debug; - pure_utils_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; - translate_log#set_level EL.Debug; + Easy_logging.Handlers.set_level main_logger_handler EL.Info; + main_log#set_level EL.Info; + llbc_of_json_logger#set_level EL.Info; + pre_passes_log#set_level EL.Info; + interpreter_log#set_level EL.Info; + statements_log#set_level EL.Info; + paths_log#set_level EL.Info; + expressions_log#set_level EL.Info; + expansion_log#set_level EL.Info; + borrows_log#set_level EL.Info; + invariants_log#set_level EL.Info; + pure_utils_log#set_level EL.Info; + symbolic_to_pure_log#set_level EL.Info; + pure_micro_passes_log#set_level EL.Info; + pure_to_extract_log#set_level EL.Info; + translate_log#set_level EL.Info; (* Load the module *) let json = Yojson.Basic.from_file filename in match llbc_module_of_json json with |