rename redefined variables

libASL/dis.ml

@@ -1499,6 +1499,7 @@ let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_cas
     let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in
     let stmts' = Transforms.CaseSimp.do_transform stmts' in
     let stmts' = Transforms.RemoveRegisters.run stmts' in
+    let stmts' = Transforms.FixRedefinitions.run (globals : IdentSet.t) stmts' in
 
     if !debug_level >= 2 then begin
         let stmts' = Asl_visitor.visit_stmts (new Asl_utils.resugarClass (!TC.binop_table)) stmts' in

libASL/symbolic_lifter.ml

@@ -314,6 +314,7 @@ let dis_wrapper fn fnsig env =
     let stmts' = Transforms.RemoveRegisters.run stmts' in
     let stmts' = Cleanup.run false stmts' in
     let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in
+    let stmts' = Transforms.FixRedefinitions.run (globals : IdentSet.t) stmts' in
     Some stmts'
   with
   | e ->

libASL/transforms.ml

@@ -1697,3 +1697,93 @@ module RemoveRegisters = struct
     visit_stmts v
 
 end
+
+
+
+module FixRedefinitions = struct
+  type index_name = {name: ident ; index: int}
+  type var_t =  index_name
+  module IdentMap = Map.Make(struct 
+    type t = ident
+    let compare = Stdlib.compare
+  end);;
+
+    let ident_for_v (e: var_t) : ident = 
+      if e.index = 0 then e.name else
+      match e.name with 
+      | Ident s -> Ident (s ^ "_" ^ (string_of_int e.index))
+      | FIdent (s, i) -> FIdent ((s ^ "_" ^ (string_of_int e.index), i))
+
+  class redef_renamer (globals) = object(this)
+    inherit Asl_visitor.nopAslVisitor
+
+    val mutable seen = IdentMap.empty
+    val scoped_bindings : (var_t IdentMap.t) Stack.t = 
+      let s = Stack.create () in 
+      let globals =  Seq.map (fun f -> (f, {name=f; index=0})) (IdentSet.to_seq globals) in
+      Stack.push (IdentMap.of_seq globals) s ; s
+
+    method push_scope (_:unit) : unit = Stack.push (IdentMap.empty) scoped_bindings
+    method pop_scope (_:unit) : unit = Stack.pop_opt scoped_bindings |> ignore
+    method add_bind (n: var_t) : unit = Stack.push (IdentMap.add n.name n (Stack.pop scoped_bindings)) scoped_bindings
+    method existing_binding (i: ident) : var_t option =  Stack.to_seq scoped_bindings 
+      |> Seq.find (fun s -> IdentMap.find_opt i s != None) 
+      |> Option.map (IdentMap.find i)
+
+    method incr_binding (i: ident) : var_t = 
+      let v = this#existing_binding i in
+      match v with 
+      | Some b -> {b with index = b.index + 1} 
+      | None -> {name=i; index=0}
+
+    method !vstmt s =
+      match s with 
+        | Stmt_VarDeclsNoInit(ty, vs, loc) -> 
+            let ns = List.map this#incr_binding vs in
+            List.iter this#add_bind ns;
+            ChangeTo (Stmt_VarDeclsNoInit(ty,List.map ident_for_v ns,loc))
+        | Stmt_VarDecl(ty, v, i, loc) -> 
+            let b = this#incr_binding v in 
+            this#add_bind b; ChangeTo (Stmt_VarDecl(ty, ident_for_v b, i, loc))
+        | Stmt_ConstDecl(ty, v, i, loc) ->
+            let b = this#incr_binding v in 
+            this#add_bind b; ChangeTo (Stmt_ConstDecl(ty, ident_for_v b, i, loc))
+        | Stmt_If (c, t, els, e, loc) -> 
+                    let c'   = visit_expr this c in
+                    this#push_scope () ;
+                    let t'   = visit_stmts this t in
+                    this#pop_scope (); this#push_scope () ;
+                    let els' = mapNoCopy (visit_s_elsif this ) els in
+                    this#pop_scope (); this#push_scope () ;
+                    let e'   = visit_stmts this e in
+                    this#pop_scope (); 
+                    ChangeTo (Stmt_If (c', t', els', e', loc))
+        (* Statements with child scopes that shouldn't appear towards the end of transform pipeline *)
+        | Stmt_Case _ -> failwith "(FixRedefinitions) case not expected"
+        | Stmt_For _ -> failwith "(FixRedefinitions) for not expected"
+        | Stmt_While _ -> failwith "(FixRedefinitions) while not expected"
+        | Stmt_Repeat _ -> failwith "(FixRedefinitions) repeat not expected"
+        | Stmt_Try _ -> failwith "(FixRedefinitions) try not expected"
+        | _ -> DoChildren
+
+    method !vlexpr e = 
+      match e with 
+        | LExpr_Var i -> (match (this#existing_binding i) with
+          | Some e -> ChangeTo (LExpr_Var (ident_for_v e))
+          | None -> SkipChildren)
+        | _ -> DoChildren
+
+    method !vexpr e = 
+      match e with 
+        | Expr_Var i -> (match (this#existing_binding i) with
+          | Some e -> ChangeTo (Expr_Var (ident_for_v e))
+          | None -> SkipChildren)
+      | _ -> DoChildren
+
+    end
+
+  let run (g: IdentSet.t) (s:stmt list) : stmt list =
+    let v = new redef_renamer g in
+    visit_stmts v s
+end
+