Propagate the changes to the place definition to the pure AST

compiler/Interpreter.ml

@@ -690,15 +690,19 @@ module Test = struct
     sanity_check __FILE__ __LINE__
       (fdef.signature.generics = empty_generic_params)
       fdef.item_meta.span;
-    sanity_check __FILE__ __LINE__ (body.locals.arg_count = 0) fdef.item_meta.span;
+    sanity_check __FILE__ __LINE__
+      (body.locals.arg_count = 0)
+      fdef.item_meta.span;
 
     (* Create the evaluation context *)
     let ctx =
       initialize_eval_ctx (Some fdef.item_meta.span) decls_ctx [] [] []
     in
 
     (* Insert the (uninitialized) local variables *)
-    let ctx = ctx_push_uninitialized_vars fdef.item_meta.span ctx body.locals.vars in
+    let ctx =
+      ctx_push_uninitialized_vars fdef.item_meta.span ctx body.locals.vars
+    in
 
     (* Create the continuation to check the function's result *)
     let config = mk_config ConcreteMode in

compiler/PrintPure.ml

@@ -262,40 +262,40 @@ let var_to_string (env : fmt_env) (v : var) : string =
   let varname = var_to_varname v in
   "(" ^ varname ^ " : " ^ ty_to_string env false v.ty ^ ")"
 
-let rec mprojection_to_string (env : fmt_env) (inside : string)
-    (p : mprojection) : string =
-  match p with
-  | [] -> inside
-  | pe :: p' -> (
-      let s = mprojection_to_string env inside p' in
-      match pe.pkind with
-      | E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
-      | E.ProjAdt (adt_id, opt_variant_id) -> (
-          let field_name =
-            match adt_field_to_string env adt_id opt_variant_id pe.field_id with
-            | Some field_name -> field_name
-            | None -> T.FieldId.to_string pe.field_id
+let mprojection_elem_to_string (env : fmt_env) (inside : string)
+    (pe : mprojection_elem) : string =
+  match pe.pkind with
+  | E.ProjTuple _ -> "(" ^ inside ^ ")." ^ T.FieldId.to_string pe.field_id
+  | E.ProjAdt (adt_id, opt_variant_id) -> (
+      let field_name =
+        match adt_field_to_string env adt_id opt_variant_id pe.field_id with
+        | Some field_name -> field_name
+        | None -> T.FieldId.to_string pe.field_id
+      in
+      match opt_variant_id with
+      | None -> "(" ^ inside ^ ")." ^ field_name
+      | Some variant_id ->
+          let variant_name =
+            adt_variant_from_type_decl_id_to_string env adt_id variant_id
           in
-          match opt_variant_id with
-          | None -> "(" ^ s ^ ")." ^ field_name
-          | Some variant_id ->
-              let variant_name =
-                adt_variant_from_type_decl_id_to_string env adt_id variant_id
-              in
-              "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
-
-let mplace_to_string (env : fmt_env) (p : mplace) : string =
-  let name =
-    match p.name with
-    | None -> ""
-    | Some name -> name
-  in
-  (* We add the "llbc" suffix to the variable index, because span-places
-   * use indices of the variables in the original LLBC program, while
-   * regular places use indices for the pure variables: we want to make
-   * this explicit, otherwise it is confusing. *)
-  let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in
-  mprojection_to_string env name p.projection
+          "(" ^ inside ^ " as " ^ variant_name ^ ")." ^ field_name)
+
+let rec mplace_to_string (env : fmt_env) (p : mplace) : string =
+  match p with
+  | PlaceBase (var_id, name) ->
+      let name =
+        match name with
+        | None -> ""
+        | Some name -> name
+      in
+      (* We add the "llbc" suffix to the variable index, because span-places
+       * use indices of the variables in the original LLBC program, while
+       * regular places use indices for the pure variables: we want to make
+       * this explicit, otherwise it is confusing. *)
+      name ^ "^" ^ E.VarId.to_string var_id ^ "llbc"
+  | PlaceProjection (p, pe) ->
+      let inside = mplace_to_string env p in
+      mprojection_elem_to_string env inside pe
 
 let adt_variant_to_string ?(span = None) (env : fmt_env) (adt_id : type_id)
     (variant_id : VariantId.id option) : string =

compiler/Pure.ml

@@ -556,19 +556,15 @@ type field_id = FieldId.id [@@deriving show, ord]
 type mprojection_elem = { pkind : field_proj_kind; field_id : field_id }
 [@@deriving show, ord]
 
-type mprojection = mprojection_elem list [@@deriving show, ord]
-
 (** "Meta" place.
 
     Meta-data retrieved from the symbolic execution, which gives provenance
     information about the values. We use this to generate names for the variables
     we introduce.
  *)
-type mplace = {
-  var_id : E.VarId.id;
-  name : string option;
-  projection : mprojection;
-}
+type mplace =
+  | PlaceBase of E.VarId.id * string option
+  | PlaceProjection of mplace * mprojection_elem
 [@@deriving show, ord]
 
 type variant_id = VariantId.id [@@deriving show, ord]

compiler/PureMicroPasses.ml

@@ -250,14 +250,14 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     | None -> (
         match VarId.Map.find_opt v.id ctx.pure_vars with
         | Some basename -> { v with basename = Some basename }
-        | None ->
-            if Option.is_some mp then
-              match
-                E.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
-              with
-              | None -> v
-              | Some basename -> { v with basename = Some basename }
-            else v)
+        | None -> (
+            match mp with
+            | None -> v
+            | Some mp -> (
+                let var_id, _, _ = decompose_mplace mp in
+                match E.VarId.Map.find_opt var_id ctx.llbc_vars with
+                | None -> v
+                | Some basename -> { v with basename = Some basename })))
   in
   (* Update an pattern - used to update an expression after we computed constraints *)
   let update_typed_pattern ctx (lv : typed_pattern) : typed_pattern =
@@ -272,9 +272,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
   (* Register an mplace the first time we find one *)
   let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx =
-    match (E.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
+    let var_id, name, _ = decompose_mplace mp in
+    match (E.VarId.Map.find_opt var_id ctx.llbc_vars, name) with
     | None, Some name ->
-        let llbc_vars = E.VarId.Map.add mp.var_id name ctx.llbc_vars in
+        let llbc_vars = E.VarId.Map.add var_id name ctx.llbc_vars in
         { ctx with llbc_vars }
     | _ -> ctx
   in
@@ -304,11 +305,11 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     (* Register the place *)
     let ctx = register_mplace mp ctx in
     (* Update the variable name *)
-    match (mp.name, mp.projection) with
-    | Some name, [] ->
+    match decompose_mplace mp with
+    | mp_var_id, Some name, [] ->
         (* Check if the variable already has a name - if not: insert the new name *)
         let ctx = add_pure_var_constraint var_id name ctx in
-        let ctx = add_llbc_var_constraint mp.var_id name ctx in
+        let ctx = add_llbc_var_constraint mp_var_id name ctx in
         ctx
     | _ -> ctx
   in
@@ -386,18 +387,21 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
             (* Add the constraint for the LLBC variable *)
             match lmp with
             | None -> ctx
-            | Some lmp -> add_llbc_var_constraint lmp.var_id name ctx
+            | Some lmp ->
+                let var_id, _, _ = decompose_mplace lmp in
+                add_llbc_var_constraint var_id name ctx
           in
           (* We try to use the right-place information *)
           let rmp, re = opt_unspan_mplace re in
           let ctx =
             match rmp with
-            | Some { var_id; name; projection = [] } -> (
+            | Some (PlaceBase (var_id, name)) ->
                 if Option.is_some name then add (Option.get name) ctx
-                else
+                else begin
                   match E.VarId.Map.find_opt var_id ctx.llbc_vars with
                   | None -> ctx
-                  | Some name -> add name ctx)
+                  | Some name -> add name ctx
+                end
             | _ -> ctx
           in
           (* We try to use the rvalue information, if it is a variable *)
@@ -541,16 +545,16 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | 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 = [] } -> (
+            match (mp, rmp) with
+            | PlaceBase (mp_var_id, _), Some (PlaceBase (var_id, name)) -> (
                 let name =
                   match name with
                   | Some name -> Some name
                   | None -> E.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)
+                | Some name -> add_llbc_var_constraint mp_var_id name ctx)
             | _ -> ctx
           in
           ctx

compiler/PureUtils.ml

@@ -137,10 +137,6 @@ let mk_tag (msg : string) (next_e : texpression) : texpression =
   let ty = next_e.ty in
   { e; ty }
 
-let mk_mplace (var_id : E.VarId.id) (name : string option)
-    (projection : mprojection) : mplace =
-  { var_id; name; projection }
-
 let empty_generic_params : generic_params =
   { types = []; const_generics = []; trait_clauses = [] }
 
@@ -872,3 +868,12 @@ let opt_destruct_ret (e : texpression) : texpression option =
         arg )
     when variant_id = Some result_ok_id -> Some arg
   | _ -> None
+
+let decompose_mplace (p : mplace) :
+    E.VarId.id * string option * mprojection_elem list =
+  let rec decompose (proj : mprojection_elem list) (p : mplace) =
+    match p with
+    | PlaceBase (id, name) -> (id, name, proj)
+    | PlaceProjection (p, pe) -> decompose (pe :: proj) p
+  in
+  decompose [] p

compiler/SymbolicAst.ml

@@ -17,15 +17,13 @@ open LlbcAst
     We later use this place information to generate meaningful name, to prettify
     the generated code.
  *)
-type mplace = {
-  bv : Contexts.var_binder;
+type mplace =
+  | PlaceBase of Contexts.var_binder
       (** It is important that we store the binder, and not just the variable id,
           because the most important information in a place is the name of the
           variable!
        *)
-  projection : projection_elem list;
-      (** We store the projection because we can, but it is actually not that useful *)
-}
+  | PlaceProjection of mplace * projection_elem
 [@@deriving show]
 
 type call_id =

compiler/SymbolicToPure.ml

@@ -1895,15 +1895,16 @@ let translate_mprojection_elem (pe : E.projection_elem) :
   | Deref -> None
   | Field (pkind, field_id) -> Some { pkind; field_id }
 
-let translate_mprojection (p : E.projection_elem list) : mprojection =
-  List.filter_map translate_mprojection_elem p
-
 (** Translate a "span"-place *)
-let translate_mplace (p : S.mplace) : mplace =
-  let var_id = p.bv.index in
-  let name = p.bv.name in
-  let projection = translate_mprojection p.projection in
-  { var_id; name; projection }
+let rec translate_mplace (p : S.mplace) : mplace =
+  match p with
+  | PlaceBase bv -> PlaceBase (bv.index, bv.name)
+  | PlaceProjection (p, pe) -> (
+      let p = translate_mplace p in
+      let pe = translate_mprojection_elem pe in
+      match pe with
+      | None -> p
+      | Some pe -> PlaceProjection (p, pe))
 
 let translate_opt_mplace (p : S.mplace option) : mplace option =
   match p with

compiler/SynthesizeSymbolic.ml

@@ -8,16 +8,14 @@ open Errors
 
 let mk_mplace (span : Meta.span) (p : place) (ctx : Contexts.eval_ctx) : mplace
     =
-  let rec place_to_projection_and_var (place : place)
-      (proj : projection_elem list) : var_id * projection_elem list =
+  let rec place_to_mplace (place : place) : mplace =
     match place.kind with
-    | PlaceBase var_id -> (var_id, proj)
+    | PlaceBase var_id ->
+        PlaceBase (Contexts.ctx_lookup_var_binder span ctx var_id)
     | PlaceProjection (subplace, pe) ->
-        place_to_projection_and_var subplace (pe :: proj)
+        PlaceProjection (place_to_mplace subplace, pe)
   in
-  let bv, proj = place_to_projection_and_var p [] in
-  let bv = Contexts.ctx_lookup_var_binder span ctx bv in
-  { bv; projection = proj }
+  place_to_mplace p
 
 let mk_opt_mplace (span : Meta.span) (p : place option)
     (ctx : Contexts.eval_ctx) : mplace option =