diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index 0d3437cbc..dab1685c1 100644 --- a/engine/lib/ast_utils.ml +++ b/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 diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 90dd1c55f..b8919bdde 100644 --- a/engine/lib/import_thir.ml +++ b/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)) diff --git a/engine/lib/phases/phase_and_mut_defsite.ml b/engine/lib/phases/phase_and_mut_defsite.ml index 0dd707d0b..0437e3068 100644 --- a/engine/lib/phases/phase_and_mut_defsite.ml +++ b/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 diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index 87b76cb5c..66fed4fbf 100644 --- a/engine/lib/print_rust.ml +++ b/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)) diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml index c11884a59..7f3c48983 100644 --- a/engine/lib/utils.ml +++ b/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) diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index 79c31dd29..1f7cbb2eb 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/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; diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap index e4d1f617e..6a5a29918 100644 --- a/test-harness/src/snapshots/toolchain__naming into-coq.snap +++ b/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). diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index b311c2a54..709296796 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/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" diff --git a/tests/naming/src/lib.rs b/tests/naming/src/lib.rs index ce722cf71..2879be61b 100644 --- a/tests/naming/src/lib.rs +++ b/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() -> usize { ::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) + } +}