summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/PureMicroPasses.ml286
-rw-r--r--src/PureUtils.ml26
2 files changed, 143 insertions, 169 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 3c25e7b6..b4f4462b 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -95,7 +95,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
method! visit_var _ v _ = v.id
(** For the lvalues *)
- method! visit_place _ p _ = p.var
+ method! visit_Local _ vid _ = vid
(** For the rvalues *)
end
in
@@ -345,16 +345,12 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| _ -> ctx
in
(* Specific case of constraint on rvalues *)
- let add_right_constraint (mp : mplace) (rv : typed_rvalue) (ctx : pn_ctx) :
+ let add_right_constraint (mp : mplace) (rv : texpression) (ctx : pn_ctx) :
pn_ctx =
(* Register the place *)
let ctx = register_mplace mp ctx in
(* Add the constraint *)
- match rv.value with RvPlace p -> add_constraint mp p.var ctx | _ -> ctx
- in
- let add_opt_right_constraint (mp : mplace option) (rv : typed_rvalue)
- (ctx : pn_ctx) : pn_ctx =
- match mp with None -> ctx | Some mp -> add_right_constraint mp rv ctx
+ match (unmeta rv).e with Local vid -> add_constraint mp vid ctx | _ -> ctx
in
(* Specific case of constraint on left values *)
let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx =
@@ -385,9 +381,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(* We propagate constraints across variable reassignments: `^0 = x`,
* if the destination doesn't have naming information *)
match lv.value with
- | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) -> (
+ | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) ->
if
- (* Check that there is not already a name for teh variable *)
+ (* Check that there is not already a name for the variable *)
VarId.Map.mem lvar.id ctx.pure_vars
then ctx
else
@@ -402,31 +398,28 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| None -> ctx
| Some lmp -> add_llbc_var_constraint lmp.var_id name ctx
in
- match re.e with
- | Value (rv, rmp) ->
- (* We try to use the right-place information *)
- let ctx =
- match rmp with
- | Some { var_id; name; projection = [] } -> (
- if Option.is_some name then add (Option.get name) ctx
- else
- match V.VarId.Map.find_opt var_id ctx.llbc_vars with
- | None -> ctx
- | Some name -> add name ctx)
- | _ -> ctx
- in
- (* We try to use the rvalue information *)
- let ctx =
- match rv with
- | { value = RvPlace { var = rvar_id; projection = [] }; ty = _ }
- -> (
- match VarId.Map.find_opt rvar_id ctx.pure_vars with
- | None -> ctx
- | Some name -> add name ctx)
- | _ -> ctx
- in
- ctx
- | _ -> ctx)
+ (* We try to use the right-place information *)
+ let rmp, re = opt_unmeta_mplace re in
+ let ctx =
+ match rmp with
+ | Some { var_id; name; projection = [] } -> (
+ if Option.is_some name then add (Option.get name) ctx
+ else
+ match V.VarId.Map.find_opt var_id ctx.llbc_vars with
+ | None -> ctx
+ | Some name -> add name ctx)
+ | _ -> ctx
+ in
+ (* We try to use the rvalue information, if it is a variable *)
+ let ctx =
+ match (unmeta re).e with
+ | Local rvar_id -> (
+ match VarId.Map.find_opt rvar_id ctx.pure_vars with
+ | None -> ctx
+ | Some name -> add name ctx)
+ | _ -> ctx
+ in
+ ctx
| _ -> ctx
in
@@ -436,25 +429,21 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ty = e.ty in
let ctx, e =
match e.e with
- | Value (v, mp) -> update_value v mp ctx
+ | Local _ -> (* Nothing to do *) (ctx, e.e)
+ | Const _ -> (* Nothing to do *) (ctx, e.e)
| App (app, arg) ->
let ctx, app = update_texpression app ctx in
let ctx, arg = update_texpression arg ctx in
let e = App (app, arg) in
(ctx, e)
| Abs (x, e) -> update_abs x e ctx
- | Func _ -> (* nothing to do *) (ctx, e.e)
+ | Qualif _ -> (* nothing to do *) (ctx, e.e)
| Let (monadic, lb, re, e) -> update_let monadic lb re e ctx
| Switch (scrut, body) -> update_switch_body scrut body ctx
| Meta (meta, e) -> update_meta meta e ctx
in
(ctx, { e; ty })
(* *)
- and update_value (v : typed_rvalue) (mp : mplace option) (ctx : pn_ctx) :
- pn_ctx * expression =
- let ctx = add_opt_right_constraint mp v ctx in
- (ctx, Value (v, mp))
- (* *)
and update_abs (x : typed_lvalue) (e : texpression) (ctx : pn_ctx) :
pn_ctx * expression =
(* We first add the left-constraint *)
@@ -507,24 +496,29 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(* *)
and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) :
pn_ctx * expression =
- match meta with
- | Assignment (mp, rvalue, rmp) ->
- let ctx = add_right_constraint mp rvalue ctx in
- let ctx =
- match (mp.projection, rmp) with
- | [], Some { var_id; name; projection = [] } -> (
- let name =
+ let ctx =
+ match meta with
+ | Assignment (mp, rvalue, rmp) ->
+ let ctx = add_right_constraint mp rvalue ctx in
+ let ctx =
+ match (mp.projection, rmp) with
+ | [], Some { var_id; name; projection = [] } -> (
+ let name =
+ match name with
+ | Some name -> Some name
+ | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars
+ in
match name with
- | Some name -> Some name
- | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars
- in
- match name with
- | None -> ctx
- | Some name -> add_llbc_var_constraint mp.var_id name ctx)
- | _ -> ctx
- in
- let ctx, e = update_texpression e ctx in
- (ctx, e.e)
+ | None -> ctx
+ | Some name -> add_llbc_var_constraint mp.var_id name ctx)
+ | _ -> ctx
+ in
+ ctx
+ | MPlace mp -> add_right_constraint mp e ctx
+ in
+ let ctx, e = update_texpression e ctx in
+ let e = mk_meta meta e in
+ (ctx, e.e)
in
let body =
@@ -552,17 +546,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(** Remove the meta-information *)
let remove_meta (def : fun_decl) : fun_decl =
- let obj =
- object
- inherit [_] map_expression as super
-
- method! visit_Meta env _ e = super#visit_expression env e.e
- end
- in
match def.body with
| None -> def
| Some body ->
- let body = { body with body = obj#visit_texpression () body.body } in
+ let body = { body with body = PureUtils.remove_meta body.body } in
{ def with body = Some body }
(** Inline the useless variable (re-)assignments:
@@ -597,7 +584,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
object (self)
inherit [_] map_expression as super
- method! visit_Let env monadic lv re e =
+ method! visit_Let (env : texpression VarId.Map.t) monadic lv re e =
(* In order to filter, we need to check first that:
* - the let-binding is not monadic
* - the left-value is a variable
@@ -621,16 +608,16 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
*)
let filter =
if inline_pure then
- match re.e with
- | Value _ -> true
- | App _ -> (
- (* Application: decompose, and check that function call *)
- match opt_destruct_function_call re with
- | Some (func, _) -> (
- match func.func with
- | Regular _ -> false
- | Unop _ | Binop _ -> true)
- | _ -> false)
+ let app, _ = destruct_apps re in
+ match app.e with
+ | Const _ | Local _ -> true (* constant or variable *)
+ | Qualif qualif -> (
+ match qualif.id with
+ | AdtCons _ | Proj _ -> true (* ADT constructor *)
+ | Func (Unop _ | Binop _) ->
+ true (* primitive function call *)
+ | Func (Regular _) ->
+ false (* non-primitive function call *))
| _ -> filter
else false
in
@@ -648,44 +635,17 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
(** Visit the let-bindings to filter the useless ones (and update
the substitution map while doing so *)
- method! visit_Value env v mp =
- (* Check if we need to substitute *)
- match v.value with
- | RvPlace p -> (
- match VarId.Map.find_opt p.var env with
- | None -> (* No substitution *) super#visit_Value env v mp
- | Some ne ->
- (* Substitute - note that we need to reexplore, because
- * there may be stacked substitutions, if we have:
- * var0 --> var1
- * var1 --> var2.
- *
- * Also: we can always substitute if we substitute with
- * a variable. If we substitute with a value we need to
- * check that the path is empty.
- * TODO: actually do a projection *)
- if is_var ne then
- let var = as_var ne in
- let p = { p with var } in
- let nv = { v with value = RvPlace p } in
- self#visit_Value env nv mp
- else if p.projection = [] then self#visit_expression env ne.e
- else super#visit_Value env v mp)
- | _ -> (* No substitution *) super#visit_Value env v mp
- (** Visit the values, to substitute them if possible *)
-
- method! visit_RvPlace env p =
- if p.projection = [] then
- match VarId.Map.find_opt p.var env with
- | None -> (* No substitution *) super#visit_RvPlace env p
- | Some ne -> (
- (* Substitute if the new expression is a value *)
- match ne.e with
- | Value (nv, _) -> self#visit_rvalue env nv.value
- | _ -> (* Not a value *) super#visit_RvPlace env p)
- else (* TODO: project *)
- super#visit_RvPlace env p
- (** Visit the places used as rvalues, to substitute them if possible *)
+ method! visit_Local (env : texpression VarId.Map.t) (vid : VarId.id) =
+ match VarId.Map.find_opt vid env with
+ | None -> (* No substitution *) super#visit_Local env vid
+ | Some ne ->
+ (* Substitute - note that we need to reexplore, because
+ * there may be stacked substitutions, if we have:
+ * var0 --> var1
+ * var1 --> var2.
+ *)
+ self#visit_expression env ne.e
+ (** Substitute the variables *)
end
in
match def.body with
@@ -721,11 +681,13 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
In this situation, we can remove the call `f x`.
*)
-let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (func0 : func)
- (args0 : texpression list) (e : texpression) : bool =
- let check_call (func1 : func) (args1 : texpression list) : bool =
- (* Check the func_ids, to see if call1's function is a child of call0's function *)
- match (func0.func, func1.func) with
+let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
+ (fun_id0 : fun_id) (tys0 : ty list) (args0 : texpression list)
+ (e : texpression) : bool =
+ let check_call (fun_id1 : fun_id) (tys1 : ty list) (args1 : texpression list)
+ : bool =
+ (* Check the fun_ids, to see if call1's function is a child of call0's function *)
+ match (fun_id0, fun_id1) with
| Regular (id0, rg_id0), Regular (id1, rg_id1) ->
(* Both are "regular" calls: check if they come from the same rust function *)
if id0 = id1 then
@@ -765,15 +727,12 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (func0 : func)
in
let args = List.combine args0 call1_args in
(* Note that the input values are expressions, *which may contain
- * meta-values* (which we need to ignore). We only consider the
- * case where both expressions are actually values. *)
+ * meta-values* (which we need to ignore). *)
let input_eq (v0, v1) =
- match (v0.e, v1.e) with
- | Value (v0, _), Value (v1, _) -> v0 = v1
- | _ -> false
+ PureUtils.remove_meta v0 = PureUtils.remove_meta v1
in
(* Compare the input types and the prefix of the input arguments *)
- func0.type_params = func1.type_params && List.for_all input_eq args
+ tys0 = tys1 && List.for_all input_eq args
else (* Not a child *)
false
else (* Not the same function *)
@@ -791,21 +750,23 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (func0 : func)
method! visit_texpression env e =
match e.e with
- | Value (_, _) -> fun _ -> false
+ | Local _ | Const _ -> fun _ -> false
| Let (_, _, re, e) -> (
match opt_destruct_function_call re with
| None -> fun () -> self#visit_texpression env e ()
- | Some (func1, args1) ->
- let call_is_child = check_call func1 args1 in
+ | Some (func1, tys1, args1) ->
+ let call_is_child = check_call func1 tys1 args1 in
if call_is_child then fun () -> true
else fun () -> self#visit_texpression env e ())
| App _ -> (
fun () ->
match opt_destruct_function_call e with
- | Some (func1, args1) -> check_call func1 args1
+ | Some (func1, tys1, args1) -> check_call func1 tys1 args1
| None -> false)
| Abs (_, e) -> self#visit_texpression env e
- | Func _ -> fun () -> false
+ | Qualif _ ->
+ (* Note that this case includes functions without arguments *)
+ fun () -> false
| Meta (_, e) -> self#visit_texpression env e
| Switch (_, body) -> self#visit_switch_body env body
@@ -878,12 +839,15 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
method plus s0 s1 _ = VarId.Set.union (s0 ()) (s1 ())
- method! visit_place _ p = (p, fun _ -> VarId.Set.singleton p.var)
- (** Whenever we visit a place, we need to register the used variable *)
+ method! visit_Local _ vid = (Local vid, fun _ -> VarId.Set.singleton vid)
+ (** Whenever we visit a variable, we need to register the used variable *)
method! visit_expression env e =
match e with
- | Value (_, _) | App _ | Func _ | Switch (_, _) | Meta (_, _) | Abs _ ->
+ | Local _ | Const _ | App _ | Qualif _
+ | Switch (_, _)
+ | Meta (_, _)
+ | Abs _ ->
super#visit_expression env e
| Let (monadic, lv, re, e) ->
(* Compute the set of values used in the next expression *)
@@ -907,13 +871,13 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
* We can filter if the right-expression is a function call,
* under some conditions. *)
match (filter_monadic_calls, opt_destruct_function_call re) with
- | true, Some (func, args) ->
+ | true, Some (func, tys, args) ->
(* We need to check if there is a child call - see
* the comments for:
* [expression_contains_child_call_in_all_paths] *)
let has_child_call =
- expression_contains_child_call_in_all_paths ctx func args
- e
+ expression_contains_child_call_in_all_paths ctx func tys
+ args e
in
if has_child_call then (* Filter *)
(e.e, fun _ -> used)
@@ -1012,9 +976,11 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
| Var (v, mp) -> if v.ty = unit_ty then Dummy else Var (v, mp)
(** Replace in lvalues *)
- method! visit_typed_rvalue env rv =
- if rv.ty = unit_ty then unit_rvalue else super#visit_typed_rvalue env rv
- (** Replace in rvalues *)
+ method! visit_texpression env e =
+ if e.ty = unit_ty then unit_rvalue else super#visit_texpression env e
+ (** Replace in "regular" expressions - note that we could limit ourselves
+ to variables, but this is more powerful
+ *)
end
in
(* Update the body *)
@@ -1046,8 +1012,8 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
method! visit_texpression env e =
match opt_destruct_function_call e with
- | Some (func, args) -> (
- match func.func with
+ | Some (fun_id, _tys, args) -> (
+ match fun_id with
| Regular (A.Assumed aid, rg_id) -> (
(* Below, when dealing with the arguments: we consider the very
* general case, where functions could be boxed (meaning we
@@ -1065,7 +1031,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
| A.BoxDeref, Some _ ->
(* `Box::deref` backward is `()` (doesn't give back anything) *)
assert (args = []);
- mk_value_expression unit_rvalue None
+ unit_rvalue
| A.BoxDerefMut, None ->
(* `Box::deref_mut` forward is the identity *)
let arg, args = Collections.List.pop args in
@@ -1082,7 +1048,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
mk_apps arg args
| A.BoxFree, _ ->
assert (args = []);
- mk_value_expression unit_rvalue None
+ unit_rvalue
| ( ( A.Replace | A.VecNew | A.VecPush | A.VecInsert | A.VecLen
| A.VecIndex | A.VecIndexMut ),
_ ) ->
@@ -1133,8 +1099,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
let vid = fresh_id () in
let tmp : var = { id = vid; basename = None; ty = lv.ty } in
let ltmp = mk_typed_lvalue_from_var tmp None in
- let rtmp = mk_typed_rvalue_from_var tmp in
- let rtmp = mk_value_expression rtmp None in
+ let rtmp = mk_texpression_from_var tmp in
(* Visit the next expression *)
let next_e = self#visit_texpression env next_e in
(* Create the let-bindings *)
@@ -1189,8 +1154,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
if Option.is_some (opt_destruct_state_monad_result sb_ty) then
(* Generate a fresh state variable *)
let state_var = fresh_state_var () in
- let state_value = mk_typed_rvalue_from_var state_var in
- let state_value = mk_value_expression state_value None in
+ let state_value = mk_texpression_from_var state_var in
let state_lvar = mk_typed_lvalue_from_var state_var None in
(* Apply in all the branches and reconstruct the switch *)
let mk_app e = mk_app e state_value in
@@ -1251,19 +1215,13 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
let re_no_monad_ty = destruct_result re_no_arrow_ty in
(* Add the state argument on the right-expression *)
let re =
- let state_value = mk_typed_rvalue_from_var state_var in
- let state_value = mk_value_expression state_value None in
+ let state_value = mk_texpression_from_var state_var in
mk_app re state_value
in
(* Create the match *)
let fail_pat = mk_result_fail_lvalue re_no_monad_ty in
let fail_value = mk_result_fail_rvalue e_no_monad_ty in
- let fail_branch =
- {
- pat = fail_pat;
- branch = mk_value_expression fail_value None;
- }
- in
+ let fail_branch = { pat = fail_pat; branch = fail_value } in
(* The `Success` branch introduces a fresh state variable *)
let pat_state_var = fresh_state_var () in
let pat_state_lvalue =
@@ -1273,10 +1231,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
mk_result_return_lvalue
(mk_simpl_tuple_lvalue [ pat_state_lvalue; lv ])
in
- let pat_state_rvalue = mk_typed_rvalue_from_var pat_state_var in
- let pat_state_rvalue =
- mk_value_expression pat_state_rvalue None
- in
+ let pat_state_rvalue = mk_texpression_from_var pat_state_var in
(* TODO: write a utility to create matches (and perform
* type-checking, etc.) *)
let success_branch =
@@ -1297,12 +1252,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
assert (lv.ty = re_ty);
let fail_pat = mk_result_fail_lvalue lv.ty in
let fail_value = mk_result_fail_rvalue e.ty in
- let fail_branch =
- {
- pat = fail_pat;
- branch = mk_value_expression fail_value None;
- }
- in
+ let fail_branch = { pat = fail_pat; branch = fail_value } in
let success_pat = mk_result_return_lvalue lv in
let success_branch = { pat = success_pat; branch = e } in
let switch_body = Match [ fail_branch; success_branch ] in
@@ -1319,8 +1269,8 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
(* Then, add a "state" input variable if necessary: *)
if config.use_state_monad then
(* - in the body *)
- let state_rvalue = mk_typed_rvalue_from_var state_var in
- let body_e = mk_app body_e (mk_value_expression state_rvalue None) in
+ let state_rvalue = mk_texpression_from_var state_var in
+ let body_e = mk_app body_e state_rvalue in
(* - in the signature *)
let sg = def.signature in
(* Input types *)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 21f39c0e..b6676db4 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -196,6 +196,17 @@ let as_var (e : texpression) : VarId.id =
let rec unmeta (e : texpression) : texpression =
match e.e with Meta (_, e) -> unmeta e | _ -> e
+(** Remove *all* the meta information *)
+let remove_meta (e : texpression) : texpression =
+ let obj =
+ object
+ inherit [_] map_expression as super
+
+ method! visit_Meta env _ e = super#visit_expression env e.e
+ end
+ in
+ obj#visit_texpression () e
+
let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1)
(** Construct a type as a list of arrows: ty1 -> ... tyn *)
@@ -238,10 +249,20 @@ let opt_destruct_qualif_app (e : texpression) :
let app, args = destruct_apps e in
match app.e with Qualif qualif -> Some (qualif, args) | _ -> None
-(** Destruct an expression into a function identifier and a list of arguments *)
+(** Destruct an expression into a qualif identifier and a list of arguments *)
let destruct_qualif_app (e : texpression) : qualif * texpression list =
Option.get (opt_destruct_qualif_app e)
+(** Destruct an expression into a function call, if possible *)
+let opt_destruct_function_call (e : texpression) :
+ (fun_id * ty list * texpression list) option =
+ match opt_destruct_qualif_app e with
+ | None -> None
+ | Some (qualif, args) -> (
+ match qualif.id with
+ | Func fun_id -> Some (fun_id, qualif.type_params, args)
+ | _ -> None)
+
let opt_destruct_result (ty : ty) : ty option =
match ty with
| Adt (Assumed Result, tys) -> Some (Collections.List.to_cons_nil tys)
@@ -453,6 +474,9 @@ let opt_destruct_state_monad_result (ty : ty) : ty option =
else None
| _ -> None
+let opt_unmeta_mplace (e : texpression) : mplace option * texpression =
+ match e.e with Meta (MPlace mp, e) -> (Some mp, e) | _ -> (None, e)
+
(** Utility function, used for type checking - TODO: move *)
let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
(type_id : type_id) (variant_id : VariantId.id option) (tys : ty list) :