Merge pull request #368 from hacspec/local-id-disambiguation

feat(engine): local id disambiguation

engine/lib/ast_utils.ml

@@ -284,6 +284,112 @@ module Make (F : Features.T) = struct
         method! visit_local_ident _ x = Set.singleton (module Local_ident) x
       end
 
+    include struct
+      open struct
+        type env = Local_ident.t list
+
+        let id_shadows ~(env : env) (id : Local_ident.t) =
+          List.find env ~f:(fun x -> String.equal x.name id.name)
+          |> Option.value ~default:id
+          |> [%equal: Local_ident.t] id
+          |> not
+
+        let ( ++ ) = Set.union
+
+        let shadows' (type a) ~env vars (x : a) next =
+          (* account for shadowing within `vars` *)
+          List.filter ~f:(id_shadows ~env:vars) (List.rev vars)
+          |> Set.of_list (module Local_ident)
+          |> Set.union (next (vars @ env) x)
+
+        let shadows (type a) ~(env : env) (pats : pat list) (x : a)
+            (next : env -> a -> Sets.Local_ident.t) =
+          let vars =
+            List.map pats ~f:(collect_local_idents#visit_pat ())
+            |> Set.(union_list (module Local_ident) >> to_list)
+          in
+          shadows' ~env vars x next
+      end
+
+      let collect_ambiguous_local_idents =
+        object (self)
+          inherit [_] item_reduce as super
+          inherit [_] Sets.Local_ident.monoid as m
+          method visit_t (_ : env) _ = m#zero
+          method visit_mutability (_f : env -> _ -> _) _ _ = m#zero
+
+          method visit_arm' env { arm_pat; body } =
+            shadows ~env [ arm_pat ] body super#visit_expr
+
+          method visit_expr' env e =
+            match e with
+            | Let { monadic = _; lhs; rhs; body } ->
+                super#visit_expr env rhs
+                ++ shadows ~env [ lhs ] body super#visit_expr
+            | Loop { kind; state; body; _ } ->
+                let empty = Set.empty (module Local_ident) |> Fn.(id &&& id) in
+                let ikind, ukind =
+                  match kind with
+                  | UnconditionalLoop -> empty
+                  | ForLoop { pat; it; _ } ->
+                      ( collect_local_idents#visit_pat () pat,
+                        super#visit_expr env it )
+                  | ForIndexLoop { start; end_; var; _ } ->
+                      ( Set.singleton (module Local_ident) var,
+                        super#visit_expr (var :: env) start
+                        ++ super#visit_expr (var :: env) end_ )
+                in
+                let istate, ustate =
+                  match state with
+                  | Some { init; bpat; _ } ->
+                      ( collect_local_idents#visit_pat () bpat,
+                        super#visit_expr (Set.to_list ikind @ env) init )
+                  | _ -> empty
+                in
+                let intro = ikind ++ istate |> Set.to_list in
+                ukind ++ ustate ++ shadows' ~env intro body super#visit_expr
+            | Closure { params; body; _ } ->
+                shadows ~env params body super#visit_expr
+            | _ -> super#visit_expr' env e
+
+          method visit_IIFn = self#visit_function_like
+          method visit_Fn env _ _ = self#visit_function_like env
+
+          method visit_function_like env body params =
+            let f p = p.pat in
+            shadows ~env (List.map ~f params) body super#visit_expr
+
+          method visit_local_ident env id =
+            Set.(if id_shadows ~env id then Fn.flip singleton id else empty)
+              (module Local_ident)
+        end
+
+      let disambiguate_local_idents (item : item) =
+        let ambiguous = collect_ambiguous_local_idents#visit_item [] item in
+        let local_vars = collect_local_idents#visit_item () item |> ref in
+        let refresh env (id : Local_ident.t) : string =
+          let extract_suffix (id' : Local_ident.t) =
+            String.chop_prefix ~prefix:(id.name ^ "_") id'.name
+            |> Option.bind ~f:string_to_int
+          in
+          let suffix =
+            Set.filter_map (module Int) env ~f:extract_suffix
+            |> Set.max_elt |> Option.value ~default:0 |> ( + ) 1
+          in
+          id.name ^ "_" ^ Int.to_string suffix
+        in
+        let new_names =
+          ambiguous |> Set.to_list
+          |> List.map ~f:(fun (var : Local_ident.t) ->
+                 let var' = { var with name = refresh !local_vars var } in
+                 local_vars := Set.add !local_vars var';
+                 (var, var'))
+          |> Map.of_alist_exn (module Local_ident)
+        in
+        let rename var = Map.find new_names var |> Option.value ~default:var in
+        (Mappers.rename_local_idents rename)#visit_item () item
+    end
+
     let collect_global_idents =
       object
         inherit ['self] item_reduce as _super

engine/lib/import_thir.ml

@@ -46,7 +46,10 @@ let def_id kind (def_id : Thir.def_id) : global_ident =
   `Concrete (Concrete_ident.of_def_id kind def_id)
 
 let local_ident kind (ident : Thir.local_ident) : local_ident =
-  { name = ident.name; id = Local_ident.mk_id kind 123 (* todo! *) }
+  {
+    name = ident.name;
+    id = Local_ident.mk_id kind (Int.of_string ident.id.local_id);
+  }
 
 let int_ty_to_size : Thir.int_ty -> size = function
   | Isize -> SSize
@@ -1327,11 +1330,11 @@ let import_item (item : Thir.item) :
     concrete_ident * (item list * Diagnostics.t list) =
   let ident = Concrete_ident.of_def_id Value item.owner_id in
   let r, reports =
-    Diagnostics.Core.capture (fun _ ->
-        c_item item ~ident
-        |> List.map
-             ~f:
-               (U.Mappers.rename_generic_constraints#visit_item
-                  (Hashtbl.create (module String))))
+    let f =
+      U.Mappers.rename_generic_constraints#visit_item
+        (Hashtbl.create (module String))
+      >> U.Reducers.disambiguate_local_idents
+    in
+    Diagnostics.Core.capture (fun _ -> c_item item ~ident |> List.map ~f)
   in
   (ident, (r, reports))

engine/lib/phases/phase_and_mut_defsite.ml

@@ -100,7 +100,7 @@ struct
          into
           `(let … = … in)* let output = expr in output` *)
       let wrap_in_identity_let (e : expr) : expr =
-        let var = Local_ident.{ id = mk_id Expr 0; name = "output" } in
+        let var = Local_ident.{ id = mk_id Expr 0; name = "hax_temp_output" } in
         let f (e : expr) : expr =
           match e.e with
           | GlobalVar (`TupleCons 0) -> e

engine/lib/print_rust.ml

@@ -216,7 +216,7 @@ module Raw = struct
         let generic_args =
           let f = pgeneric_value e.span in
           if List.is_empty generic_args then !""
-          else !"<" & (concat ~sep:!"," @@ List.map ~f generic_args) & !">"
+          else !"::<" & (concat ~sep:!"," @@ List.map ~f generic_args) & !">"
         in
         pexpr f & generic_args & !"(" & args & !")"
     | Literal l -> pliteral e.span l
@@ -560,7 +560,6 @@ let rustfmt_annotated' (x : AnnotatedString.t) : AnnotatedString.t =
             (original, (Span.dummy (), s))
           else (
             Stdio.prerr_endline @@ "\n##### RUSTFMT TOKEN ERROR #####";
-            Stdio.prerr_endline @@ "prev=" ^ [%show: AnnotatedString.t] prev;
             Stdio.prerr_endline @@ "s=" ^ s;
             raise RetokenizationFailure)
       | _ -> (original, (last, s))

engine/lib/utils.ml

@@ -48,6 +48,7 @@ let is_uppercase s = String.equal s (String.uppercase s)
 let is_lowercase s = String.equal s (String.lowercase s)
 let start_uppercase = first_letter >> is_uppercase
 let start_lowercase = first_letter >> is_lowercase
+let string_to_int s = try Some (Int.of_string s) with _ -> None
 
 let split_str (s : string) ~(on : string) : string list =
   split_list ~equal:Char.equal ~needle:(String.to_list on) (String.to_list s)

test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap

@@ -184,14 +184,14 @@ let foo (lhs rhs: t_S) : t_S =
 let i (bar: t_Bar) : (t_Bar & u8) =
   let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in
   let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in
-  let output:u8 = bar.f_a +! bar.f_b in
-  bar, output <: (t_Bar & u8)
+  let hax_temp_output:u8 = bar.f_a +! bar.f_b in
+  bar, hax_temp_output <: (t_Bar & u8)
 
 let j (x: t_Bar) : (t_Bar & u8) =
   let tmp0, out:(t_Bar & u8) = i x in
   let x:t_Bar = tmp0 in
-  let output:u8 = out in
-  x, output <: (t_Bar & u8)
+  let hax_temp_output:u8 = out in
+  x, hax_temp_output <: (t_Bar & u8)
 
 type t_Pair (v_T: Type) {| _: Core.Marker.t_Sized v_T |} = {
   f_a:v_T;

test-harness/src/snapshots/toolchain__naming into-coq.snap

@@ -24,6 +24,44 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Naming.Ambiguous_names.v" = '''
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+(*Not implemented yet? todo(item)*)
+
+Definition debug (label : int32) (value : int32) : unit :=
+  let _ := (v__print (impl_2__new_v1 (unsize (array_from_list [[;
+      ] a=;
+
+])) (unsize (array_from_list [impl_1__new_display label;
+      impl_1__new_display value])))) : unit in
+  tt.
+
+Definition f : unit :=
+  let a_1 := ((@repr WORDSIZE32 104)) : int32 in
+  let a_2 := ((@repr WORDSIZE32 205)) : int32 in
+  let a_3 := ((@repr WORDSIZE32 306)) : int32 in
+  let a := ((@repr WORDSIZE32 123)) : int32 in
+  let _ := (debug (@repr WORDSIZE32 3) a_3) : unit in
+  let _ := (debug (@repr WORDSIZE32 2) a_2) : unit in
+  let _ := (debug (@repr WORDSIZE32 1) a_1) : unit in
+  debug (@repr WORDSIZE32 4) a.
+
+Definition ff_expand : unit :=
+  let a := ((@repr WORDSIZE32 104)) : int32 in
+  let a := ((@repr WORDSIZE32 205)) : int32 in
+  let a := ((@repr WORDSIZE32 306)) : int32 in
+  let a := ((@repr WORDSIZE32 123)) : int32 in
+  let _ := (debug (@repr WORDSIZE32 3) a) : unit in
+  let _ := (debug (@repr WORDSIZE32 2) a) : unit in
+  let _ := (debug (@repr WORDSIZE32 1) a) : unit in
+  debug (@repr WORDSIZE32 0) a.
+'''
 "Naming.F.G.Impl_1.G.Hello.v" = '''
 (* File automatically generated by Hacspec *)
 From Hacspec Require Import Hacspec_Lib MachineIntegers.
@@ -84,6 +122,8 @@ Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := {
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Definition v_INHERENT_CONSTANT : uint_size :=
   (@repr WORDSIZE32 3).
 

test-harness/src/snapshots/toolchain__naming into-fstar.snap

@@ -24,6 +24,56 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Naming.Ambiguous_names.fst" = '''
+module Naming.Ambiguous_names
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let debug (label value: u32) : Prims.unit =
+  let _:Prims.unit =
+    Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list =
+                  ["["; "] a="; "\n"]
+                in
+                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
+                Rust_primitives.Hax.array_of_list list)
+            <:
+            t_Slice string)
+          (Rust_primitives.unsize (let list =
+                  [
+                    Core.Fmt.Rt.impl_1__new_display label <: Core.Fmt.Rt.t_Argument;
+                    Core.Fmt.Rt.impl_1__new_display value <: Core.Fmt.Rt.t_Argument
+                  ]
+                in
+                FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+                Rust_primitives.Hax.array_of_list list)
+            <:
+            t_Slice Core.Fmt.Rt.t_Argument)
+        <:
+        Core.Fmt.t_Arguments)
+  in
+  ()
+
+let f: Prims.unit =
+  let a_1_:u32 = 104ul in
+  let a_2_:u32 = 205ul in
+  let a_3_:u32 = 306ul in
+  let a:u32 = 123ul in
+  let _:Prims.unit = debug 3ul a_3_ in
+  let _:Prims.unit = debug 2ul a_2_ in
+  let _:Prims.unit = debug 1ul a_1_ in
+  debug 4ul a
+
+let ff_expand: Prims.unit =
+  let a:i32 = 104l in
+  let a:i32 = 205l in
+  let a:i32 = 306l in
+  let a:u32 = 123ul in
+  let _:Prims.unit = debug 3ul a in
+  let _:Prims.unit = debug 2ul a in
+  let _:Prims.unit = debug 1ul a in
+  debug 0ul a
+'''
 "Naming.F.G.Impl_1.G.Hello.fst" = '''
 module Naming.F.G.Impl_1.G.Hello
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/naming/src/lib.rs

@@ -1,5 +1,5 @@
 #![allow(dead_code)]
-#![warn(non_camel_case_types)]
+#![allow(non_camel_case_types)]
 
 enum Foo {
     A,
@@ -105,3 +105,53 @@ trait FooTrait {
 fn constants<T: FooTrait>() -> usize {
     <T as FooTrait>::ASSOCIATED_CONSTANT + INHERENT_CONSTANT
 }
+
+/// Test for ambiguous local names renaming: when two local vars are
+/// ambiguous by name but not by their internal IDs.
+/// Such situation can occur playing with *hygenic* macros.
+/// Also, this happens with some internal Rustc rewrite. (e.g. assignment of tuples)
+mod ambiguous_names {
+    fn debug(label: u32, value: u32) {
+        println!("[{}] a={}", label, value)
+    }
+
+    /// This macro surround a given expression with a let binding for
+    /// an identifier `a` and a print of that `a`.
+    macro_rules! introduce_binding_to_new_name_a {
+        ($label:expr, $value:expr, $($e:tt)*) => {
+            let a = $value;
+            $($e)*
+            debug($label, a)
+        };
+    }
+
+    /// `f` stacks mutliple let bindings declaring different `a`s.
+    fn f() {
+        introduce_binding_to_new_name_a!(1, 104,
+               introduce_binding_to_new_name_a!(2, 205,
+                      introduce_binding_to_new_name_a!(3, 306, let a = 123;);
+               );
+        );
+        debug(4, a)
+    }
+
+    /// `f` is expanded into `f_expand` below, while the execution of `f` gives:
+    ///
+    /// ```plaintext
+    ///  [3] a=306
+    ///  [2] a=205
+    ///  [1] a=104
+    ///  [last] a=123
+    /// ```
+    #[allow(unused)]
+    fn f_expand() {
+        let a = 104;
+        let a = 205;
+        let a = 306;
+        let a = 123;
+        debug(3, a);
+        debug(2, a);
+        debug(1, a);
+        debug(0, a)
+    }
+}