Implement a micro pass to filter the box functions

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