diff options
| -rw-r--r-- | src/Collections.ml | 5 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 1 | ||||
| -rw-r--r-- | src/Pure.ml | 89 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 55 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 25 |
5 files changed, 108 insertions, 67 deletions
diff --git a/src/Collections.ml b/src/Collections.ml index 2bfdd18b..2d7a8787 100644 --- a/src/Collections.ml +++ b/src/Collections.ml @@ -72,6 +72,11 @@ module List = struct fold acc (y :: ls) in fold init ls + + let to_cons_nil (ls : 'a list) : 'a = + match ls with + | [ x ] -> x + | _ -> raise (Failure "The list should have length exactly one") end module type OrderedType = sig diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2994d95f..a3972578 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -692,6 +692,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) let _ = extract_typed_rvalue ctx fmt inside rv in () | Call call -> ( + log#ldebug (lazy ("ctx_get_function: " ^ show_fun_id call.func)); match (call.func, call.args) with | Unop unop, [ arg ] -> ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg diff --git a/src/Pure.ml b/src/Pure.ml index c1dbaa13..428246dd 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -117,9 +117,9 @@ type type_def = { } [@@deriving show] -type scalar_value = V.scalar_value +type scalar_value = V.scalar_value [@@deriving show] -type constant_value = V.constant_value +type constant_value = V.constant_value [@@deriving show] type var = { id : VarId.id; @@ -129,6 +129,7 @@ type var = { *) ty : ty; } +[@@deriving show] (** Because we introduce a lot of temporary variables, the list of variables is not fixed: we thus must carry all its information with the variable itself. @@ -138,10 +139,12 @@ type var = { * on enumerations. * Also: tuples... *) type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id } +[@@deriving show] -type projection = projection_elem list +type projection = projection_elem list [@@deriving show] type mplace = { name : string option; projection : projection } +[@@deriving show] (** "Meta" place. Meta-data retrieved from the symbolic execution, which gives provenance @@ -149,7 +152,7 @@ type mplace = { name : string option; projection : projection } we introduce. *) -type place = { var : VarId.id; projection : projection } +type place = { var : VarId.id; projection : projection } [@@deriving show] (** Ancestor for [iter_var_or_dummy] visitor *) class ['self] iter_value_base = @@ -224,15 +227,16 @@ type var_or_dummy = | Var of var * mplace option | Dummy (** Ignored value: `_`. *) [@@deriving - visitors - { - name = "iter_var_or_dummy"; - variety = "iter"; - ancestors = [ "iter_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - polymorphic = false; - }, + show, + visitors + { + name = "iter_var_or_dummy"; + variety = "iter"; + ancestors = [ "iter_value_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + polymorphic = false; + }, visitors { name = "map_var_or_dummy"; @@ -269,15 +273,16 @@ and adt_lvalue = { and typed_lvalue = { value : lvalue; ty : ty } [@@deriving - visitors - { - name = "iter_typed_lvalue"; - variety = "iter"; - ancestors = [ "iter_var_or_dummy" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - polymorphic = false; - }, + show, + visitors + { + name = "iter_typed_lvalue"; + variety = "iter"; + ancestors = [ "iter_var_or_dummy" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + polymorphic = false; + }, visitors { name = "map_typed_lvalue"; @@ -316,15 +321,16 @@ and adt_rvalue = { and typed_rvalue = { value : rvalue; ty : ty } [@@deriving - visitors - { - name = "iter_typed_rvalue"; - variety = "iter"; - ancestors = [ "iter_typed_lvalue" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - polymorphic = false; - }, + show, + visitors + { + name = "iter_typed_rvalue"; + variety = "iter"; + ancestors = [ "iter_typed_lvalue" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + polymorphic = false; + }, visitors { name = "map_typed_rvalue"; @@ -353,8 +359,6 @@ and typed_rvalue = { value : rvalue; ty : ty } type unop = Not | Neg of integer_type [@@deriving show, ord] -(* TODO: redefine assumed_fun_id (we need to get rid of box! *) - type fun_id = | Regular of A.fun_id * T.RegionGroupId.id option (** Backward id: `Some` if the function is a backward function, `None` @@ -364,7 +368,7 @@ type fun_id = [@@deriving show, ord] (** Meta-information stored in the AST *) -type meta = Assignment of mplace * typed_rvalue +type meta = Assignment of mplace * typed_rvalue [@@deriving show] (** Ancestor for [iter_expression] visitor *) class ['self] iter_expression_base = @@ -512,14 +516,15 @@ and match_branch = { pat : typed_lvalue; branch : texpression } and texpression = { e : expression; ty : ty } [@@deriving - visitors - { - name = "iter_expression"; - variety = "iter"; - ancestors = [ "iter_expression_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - }, + show, + visitors + { + name = "iter_expression"; + variety = "iter"; + ancestors = [ "iter_expression_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }, visitors { name = "map_expression"; diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 66442ec7..cbc2409d 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -677,6 +677,56 @@ let unit_vars_to_unit (def : fun_def) : fun_def = (* Return *) { def with body; inputs_lvs } +(** Eliminate the box functions like `Box::new`, `Box::deref`, etc. Most of them + are translated to identity, and `Box::free` is translated to `()`. + + Note that the box types have already been eliminated during the translation + from symbolic to pure. + The reason why we don't eliminate the box functions at the same time is + that we would need to eliminate them in two different places: when translating + function calls, and when translating end abstractions. Here, we can do + something simpler, in one micro-pass. + *) +let eliminate_box_functions (_ctx : trans_ctx) (def : fun_def) : fun_def = + (* The map visitor *) + let obj = + object + inherit [_] map_expression as super + + method! visit_Call env call = + match call.func with + | Regular (A.Assumed aid, rg_id) -> ( + match (aid, rg_id) with + | A.BoxNew, _ -> + let arg = Collections.List.to_cons_nil call.args in + arg.e + | A.BoxDeref, None -> + (* `Box::deref` forward is the identity *) + let arg = Collections.List.to_cons_nil call.args in + arg.e + | A.BoxDeref, Some _ -> + (* `Box::deref` backward is `()` (doesn't give back anything) *) + (mk_value_expression unit_rvalue None).e + | A.BoxDerefMut, None -> + (* `Box::deref_mut` forward is the identity *) + let arg = Collections.List.to_cons_nil call.args in + arg.e + | A.BoxDerefMut, Some _ -> + (* `Box::deref_mut` back is the identity *) + let arg = + match call.args with + | [ _; given_back ] -> given_back + | _ -> failwith "Unreachable" + in + arg.e + | A.BoxFree, _ -> (mk_value_expression unit_rvalue None).e) + | _ -> super#visit_Call env call + end + in + (* Update the body *) + let body = obj#visit_texpression () def.body in + { def with body } + (** Unfold the monadic let-bindings to explicit matches. *) let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_def) : fun_def = (* It is a very simple map *) @@ -753,6 +803,11 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) : (lazy ("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + (* Eliminate the box functions *) + let def = eliminate_box_functions ctx def in + log#ldebug + (lazy ("eliminate_box_functions:\n\n" ^ fun_def_to_string ctx def ^ "\n")); + (* Filter the unused variables, assignments, function calls, etc. *) let def = filter_unused config.filter_unused_monadic_calls ctx def in log#ldebug (lazy ("filter_unused:\n\n" ^ fun_def_to_string ctx def ^ "\n")); diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index bd69837a..6a1bcc2a 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -240,31 +240,6 @@ let names_map_add_assumed_function (fid : A.assumed_fun_id) names_map = names_map_add (FunId (A.Assumed fid, rg_id)) name nm -(* TODO: remove those functions? We use the ones of extraction_ctx *) -let names_map_get (id : id) (nm : names_map) : string = - IdMap.find id nm.id_to_name - -let names_map_get_function (id : A.fun_id) (rg : RegionGroupId.id option) - (nm : names_map) : string = - names_map_get (FunId (id, rg)) nm - -let names_map_get_local_function (id : FunDefId.id) - (rg : RegionGroupId.id option) (nm : names_map) : string = - names_map_get_function (A.Local id) rg nm - -let names_map_get_type (id : type_id) (nm : names_map) : string = - assert (id <> Tuple); - names_map_get (TypeId id) nm - -let names_map_get_local_type (id : TypeDefId.id) (nm : names_map) : string = - names_map_get_type (AdtId id) nm - -let names_map_get_var (id : VarId.id) (nm : names_map) : string = - names_map_get (VarId id) nm - -let names_map_get_type_var (id : TypeVarId.id) (nm : names_map) : string = - names_map_get (TypeVarId id) nm - (** Make a (variable) basename unique (by adding an index). We do this in an inefficient manner (by testing all indices starting from |