From e4c5a4286c5807e45d2c7c9a9e31ad6050cbd16d Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Mon, 23 Dec 2024 10:41:11 -0800
Subject: [PATCH] Shockingly enough, local variables were not avoiding
 collisions with C keywords

---
 lib/AstToCStar.ml      |   2 +
 lib/GlobalNames.ml     | 225 +++++++++++++++++++++--------------------
 lib/GlobalNames.mli    |   2 +
 test/NameCollision.fst |   5 +-
 4 files changed, 121 insertions(+), 113 deletions(-)

diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml
index 2074fab50..c5910696b 100644
--- a/lib/AstToCStar.ml
+++ b/lib/AstToCStar.ml
@@ -146,6 +146,7 @@ let ensure_fresh env name body cont =
         !r
   in
   mk_fresh name (fun tentative ->
+    List.mem tentative GlobalNames.keywords ||
     tricky_shadowing_see_comment_above tentative body 0 ||
     List.exists (fun cont -> tricky_shadowing_see_comment_above tentative (Some cont) 1) cont ||
     List.mem tentative env.in_block ||
@@ -486,6 +487,7 @@ and mk_stmts env e ret_type =
     | ELet (b, e1, e2) ->
         let env, binder = mk_and_push_binder env b Local (Some e1) [ e2 ]
         and e1 = mk_expr env false e1 in
+        KPrint.bprintf "pushed %s; now %s\n" b.node.name (String.concat ", " env.names);
         let acc = CStar.Decl (binder, e1) :: comment (e.meta @ b.meta) @ acc in
         collect (env, acc) return_pos e2
 
diff --git a/lib/GlobalNames.ml b/lib/GlobalNames.ml
index 95f412fa3..4dc86af0f 100644
--- a/lib/GlobalNames.ml
+++ b/lib/GlobalNames.ml
@@ -19,119 +19,120 @@ let dump (env: t) =
     KPrint.bprintf "%s is used\n" c_name
   ) (snd env)
 
+let keywords = [
+  "_Alignas";
+  "_Alignof";
+  "_Atomic";
+  "_Bool";
+  "_Complex";
+  "_Generic";
+  "_Imaginary";
+  "_Noreturn";
+  "_Pragma";
+  "_Static_assert";
+  "_Thread_local";
+  "alignas";
+  "alignof";
+  "and";
+  "and_eq";
+  "asm";
+  "atomic_cancel";
+  "atomic_commit";
+  "atomic_noexcept";
+  "auto";
+  "bitand";
+  "bitor";
+  "bool";
+  "break";
+  "case";
+  "catch";
+  "char";
+  "char16_t";
+  "char32_t";
+  "char8_t";
+  "class";
+  "co_await";
+  "co_return";
+  "co_yield";
+  "compl";
+  "concept";
+  "const";
+  "const_cast";
+  "consteval";
+  "constexpr";
+  "constinit";
+  "continue";
+  "decltype";
+  "default";
+  "delete";
+  "do";
+  "double";
+  "dynamic_cast";
+  "else";
+  "enum";
+  "explicit";
+  "export";
+  "extern";
+  "false";
+  "float";
+  "for";
+  "fortran";
+  "friend";
+  "goto";
+  "if";
+  "inline";
+  "int";
+  "long";
+  "mutable";
+  "namespace";
+  "new";
+  "noexcept";
+  "not";
+  "not_eq";
+  "nullptr";
+  "operator";
+  "or";
+  "or_eq";
+  "private";
+  "protected";
+  "public";
+  "reflexpr";
+  "register";
+  "reinterpret_cast";
+  "requires";
+  "restrict";
+  "return";
+  "short";
+  "signed";
+  "sizeof";
+  "static";
+  "static_assert";
+  "static_cast";
+  "struct";
+  "switch";
+  "synchronized";
+  "template";
+  "this";
+  "thread_local";
+  "throw";
+  "true";
+  "try";
+  "typedef";
+  "typeid";
+  "typename";
+  "union";
+  "unsigned";
+  "using";
+  "virtual";
+  "void";
+  "volatile";
+  "wchar_t";
+  "while";
+  "xor";
+  "xor_eq";
+]
+
 let reserve_keywords used_c_names =
-  let keywords = [
-    "_Alignas";
-    "_Alignof";
-    "_Atomic";
-    "_Bool";
-    "_Complex";
-    "_Generic";
-    "_Imaginary";
-    "_Noreturn";
-    "_Pragma";
-    "_Static_assert";
-    "_Thread_local";
-    "alignas";
-    "alignof";
-    "and";
-    "and_eq";
-    "asm";
-    "atomic_cancel";
-    "atomic_commit";
-    "atomic_noexcept";
-    "auto";
-    "bitand";
-    "bitor";
-    "bool";
-    "break";
-    "case";
-    "catch";
-    "char";
-    "char16_t";
-    "char32_t";
-    "char8_t";
-    "class";
-    "co_await";
-    "co_return";
-    "co_yield";
-    "compl";
-    "concept";
-    "const";
-    "const_cast";
-    "consteval";
-    "constexpr";
-    "constinit";
-    "continue";
-    "decltype";
-    "default";
-    "delete";
-    "do";
-    "double";
-    "dynamic_cast";
-    "else";
-    "enum";
-    "explicit";
-    "export";
-    "extern";
-    "false";
-    "float";
-    "for";
-    "fortran";
-    "friend";
-    "goto";
-    "if";
-    "inline";
-    "int";
-    "long";
-    "mutable";
-    "namespace";
-    "new";
-    "noexcept";
-    "not";
-    "not_eq";
-    "nullptr";
-    "operator";
-    "or";
-    "or_eq";
-    "private";
-    "protected";
-    "public";
-    "reflexpr";
-    "register";
-    "reinterpret_cast";
-    "requires";
-    "restrict";
-    "return";
-    "short";
-    "signed";
-    "sizeof";
-    "static";
-    "static_assert";
-    "static_cast";
-    "struct";
-    "switch";
-    "synchronized";
-    "template";
-    "this";
-    "thread_local";
-    "throw";
-    "true";
-    "try";
-    "typedef";
-    "typeid";
-    "typename";
-    "union";
-    "unsigned";
-    "using";
-    "virtual";
-    "void";
-    "volatile";
-    "wchar_t";
-    "while";
-    "xor";
-    "xor_eq";
-  ] in
   List.iter (fun k -> Hashtbl.add used_c_names k ()) keywords;
   (* Some stuff that's already almost always in scope. *)
   let std = [
diff --git a/lib/GlobalNames.mli b/lib/GlobalNames.mli
index 2e1726eec..fc60213b0 100644
--- a/lib/GlobalNames.mli
+++ b/lib/GlobalNames.mli
@@ -32,3 +32,5 @@ val pascal_case: string -> string
 val camel_case: string -> string
 
 val skip_prefix: Ast.lident -> bool
+
+val keywords: string list
diff --git a/test/NameCollision.fst b/test/NameCollision.fst
index 9d52acb1e..1d5f84fe6 100644
--- a/test/NameCollision.fst
+++ b/test/NameCollision.fst
@@ -4,5 +4,8 @@ let mk = NameCollisionHelper.mk
 
 open NameCollisionHelper
 
+let f (): FStar.HyperStack.ST.St Int32.t = 0l
+
 let main () =
-  (mk 0l).y
+  let unsigned = f () in
+  (mk unsigned).y