From f509a756ac4075f60162c83e8b2f5e25c751f93c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 14 Mar 2019 14:20:55 +0100
Subject: [PATCH] [typing] Refactor handling of alpha conversion

Do not use two distinct undo stacks for taking care of which symbols are in use
at a given program point. Let `Alpha` manages everything internally.
---
 src/kernel_internals/typing/cabs2cil.ml | 68 +++++++------------------
 tests/syntax/oracle/rename.res.oracle   | 11 +++-
 2 files changed, 27 insertions(+), 52 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 31b0267bff2..a66624a0fd6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -867,9 +867,7 @@ let remove_label_env lab =
  * hash table easily *)
 type undoScope =
     UndoRemoveFromEnv of string
-  | UndoResetAlphaCounter of location Alpha.alphaTableData ref *
-                             location Alpha.alphaTableData
-  | UndoRemoveFromAlphaTable of string * string
+  | UndoAlphaEnv of location Alpha.undoAlphaElement list
 
 let scopes :  undoScope list ref list ref = ref []
 
@@ -881,14 +879,10 @@ let declared_in_current_scope s =
   | cur_scope :: _ ->
     let names_declared_in_current_scope =
       Extlib.filter_map
-        (fun us ->
-           match us with
-           | UndoRemoveFromEnv _ | UndoRemoveFromAlphaTable _ -> true
-           | UndoResetAlphaCounter _ -> false)
-        (fun us ->
-           match us with
-           | UndoRemoveFromEnv s | UndoRemoveFromAlphaTable (s,_) -> s
-           | UndoResetAlphaCounter _ -> assert false (* already filtered *)
+        (function UndoRemoveFromEnv _  -> true | UndoAlphaEnv _ -> false)
+        (function
+          | UndoRemoveFromEnv s -> s
+          | UndoAlphaEnv _ -> assert false (* already filtered *)
         ) !cur_scope
     in
     List.mem s names_declared_in_current_scope
@@ -973,29 +967,24 @@ let newAlphaName (globalscope: bool) (* The name should have global scope *)
    * the top-most scope (that of the enclosing function) *)
   let rec findEnclosingFun = function
       [] -> (* At global scope *) None
-    | [s] -> begin
-        let prefix, infix = Alpha.getAlphaPrefix lookupname in
-        try
-          let infixes = H.find alphaTable prefix in
-          let countref = H.find infixes infix in
-          s := (UndoResetAlphaCounter (countref, !countref)) :: !s; Some s
-        with Not_found ->
-          s := (UndoRemoveFromAlphaTable (prefix, infix)) :: !s; Some s;
-      end
+    | [s] -> Some s
     | _ :: rest -> findEnclosingFun rest
   in
   let undo_scope =
     if not globalscope then findEnclosingFun !scopes else None
   in
+  let undolist =
+    match undo_scope with None -> None | Some _ -> Some (ref [])
+  in
+  let data = CurrentLoc.get () in
   let newname, oldloc =
-    Alpha.newAlphaName alphaTable lookupname (CurrentLoc.get ())
+    Alpha.newAlphaName ~alphaTable ?undolist ~lookupname ~data
   in
+  (match undo_scope, undolist with
+   | None, None -> ()
+   | Some s, Some l -> s := (UndoAlphaEnv !l) :: !s
+   | _ -> assert false (* by construction, both options have the same status*));
   if newname <> lookupname then begin
-    (match undo_scope with
-     | None -> ()
-     | Some s ->
-       let newpre, newinf = Alpha.getAlphaPrefix newname in
-       s := (UndoRemoveFromAlphaTable (newpre, newinf)) :: !s);
     try
       let info =
         if !scopes = [] then begin
@@ -3840,31 +3829,8 @@ let exitScope () =
       [] -> ()
     | UndoRemoveFromEnv n :: t ->
       H.remove env n; loop t
-    | UndoRemoveFromAlphaTable (p,i) :: t ->
-      Kernel.(
-        debug ~dkey:dkey_alpha_undo
-          "Removing %s %s from alpha table\n" p i);
-      (try
-         let h = H.find alphaTable p in
-         H.remove h i;
-         let l = H.length h in
-         if l = 0 then begin
-           H.remove alphaTable p;
-           Kernel.(
-             debug ~dkey:dkey_alpha_undo "No suffix for %s anymore" p)
-         end else begin
-           Kernel.(
-             debug ~dkey:dkey_alpha_undo "%d suffixes remaining@\n%t" l
-               (fun fmt ->
-                  H.iter (fun i _ -> Format.fprintf fmt "%s@ " i) h))
-         end
-       with Not_found ->
-         Kernel.warning
-           "prefix (%s,%s) not in alpha conversion table. \
-            undo stack is inconsistent"
-           p i); loop t
-    | UndoResetAlphaCounter (vref, oldv) :: t ->
-      vref := oldv;
+    | UndoAlphaEnv undolist :: t ->
+      Alpha.undoAlphaChanges ~alphaTable ~undolist;
       loop t
   in
   loop !this;
diff --git a/tests/syntax/oracle/rename.res.oracle b/tests/syntax/oracle/rename.res.oracle
index a672348b232..3014a97f930 100644
--- a/tests/syntax/oracle/rename.res.oracle
+++ b/tests/syntax/oracle/rename.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/syntax/rename.i (no preprocessing)
-[kernel] tests/syntax/rename.i:48: Warning: 
+[kernel] tests/syntax/rename.i:69: Warning: 
   unnamed fields are a C11 extension (use -c11 to avoid this warning)
 /* Generated by Frama-C */
 struct not_anon {
@@ -89,7 +89,16 @@ void f6(void)
 }
 
 int y_1;
+void f7(void)
+{
+  {
+    int __constr_expr_1 = 0;
+  }
+  int __constr_expr_2 = 0;
+  return;
+}
 
+int __constr_expr_0 = 0;
 struct not_anon s = {.__anonCompField1 = 0};
 struct anon a = {.__anonCompField1 = {.inner_i = 0}};
 
-- 
GitLab