From de73787cfdec38e2b9522a6ad440ddcc1b9150c3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 28 Oct 2019 11:07:18 +0100
Subject: [PATCH] [ghost] prefer renaming a ghost local in case of name clash

---
 src/kernel_internals/typing/cabs2cil.ml       | 19 +++++++++++++++----
 src/kernel_services/ast_queries/cil.ml        | 11 +++++++----
 .../oracle/ghost_local_capture.res.oracle     | 14 +++++++-------
 3 files changed, 29 insertions(+), 15 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 6d268f2117d..c0aa7ec4d8c 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1130,10 +1130,21 @@ let alphaConvertVarAndAddToEnv addtoenv vi =
                 vi.vname newname Cil_printer.pp_location oldloc;
           end
       end else begin
-        (* We have changed the name of a local variable. Can we try to detect
-         * if the other variable was also local in the same scope? Not for
-         * now. *)
-        copyVarinfo vi newname
+        (* favor renaming ghost variables over non-ghost ones *)
+        if not vi.vghost then begin
+          let siblings =
+            fst @@ List.split @@
+            Datatype.String.Hashtbl.find_all ghost_env vi.vname
+          in
+          let check = function
+            | EnvVar vi' -> vi!=vi' && vi.vname = vi'.vname
+            | _ -> false
+          in
+          match List.find_opt check siblings with
+          | Some (EnvVar ({ vghost = true } as oldvi)) ->
+            oldvi.vname <- newname; vi
+          | _ -> copyVarinfo vi newname
+        end else copyVarinfo vi newname
       end
     end
   in
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 14b0d96135b..d52be341225 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6450,12 +6450,15 @@ let uniqueVarNames (f: file) : unit =
                 newname Location.pretty oldloc ;
             v.vname <- newname
           in
-          (* Do the formals first *)
-          List.iter processLocal fdec.sformals;
+          let ghost vi = vi.vghost in
+          let formals_ghost, formals = List.partition ghost fdec.sformals in
+          let locals_ghost, locals = List.partition ghost fdec.slocals in
+          List.iter processLocal formals;
+          List.iter processLocal locals;
+          List.iter processLocal formals_ghost;
+          List.iter processLocal locals_ghost;
           (* Fix the type again *)
           setFormals fdec fdec.sformals;
-          (* And now the locals *)
-          List.iter processLocal fdec.slocals;
           (* Undo the changes to the global table *)
           Alpha.undoAlphaChanges gAlphaTable !undolist;
           ()
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index 648e40245cd..9ec3c5e8a40 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -18,17 +18,17 @@ void titi(void)
 
 void toto(void)
 {
-  /*@ ghost int c = 1; */
+  /*@ ghost int c_0 = 1; */
   {
     L0: ;
-    int c_0 = 0;
+    int c = 0;
     L1: ;
-    c_0 = 2;
-    /*@ assert c_0 ≡ 2; */ ;
-    /*@ assert \at(c,L0) ≡ 1; */ ;
-    /*@ assert \at(c_0,L1) ≡ 0; */ ;
+    c = 2;
+    /*@ assert c ≡ 2; */ ;
+    /*@ assert \at(c_0,L0) ≡ 1; */ ;
+    /*@ assert \at(c,L1) ≡ 0; */ ;
   }
-  /*@ assert c ≡ 1; */ ;
+  /*@ assert c_0 ≡ 1; */ ;
   return;
 }
 
-- 
GitLab