fix: correctly handle duplicate projections in the IR expand_reset_reuse pass (#8023)

This PR fixes the IR expand_reset_reuse pass to correctly handle
duplicate projections from the same base/index. This does not occur (at
least easily) with the old compiler, but it occurs when bootstrapping
Lean with the new compiler.

Author: zwarich

src/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -49,11 +49,23 @@ partial def consumed (x : VarId) : FnBody → Bool
   | e => !e.isTerminal && consumed x e.body
 
 abbrev Mask := Array (Option VarId)
+abbrev ProjCounts := Std.HashMap (VarId × Nat) Nat
+
+partial def computeProjCounts (bs : Array FnBody) : ProjCounts :=
+  let incrementCountIfProj r b :=
+    if let .vdecl _ _ (.proj i v) _ := b then
+      r.alter (v, i) fun
+      | some n => some (n + 1)
+      | none => some 1
+    else
+      r
+  bs.foldl incrementCountIfProj Std.HashMap.emptyWithCapacity
 
 /-- Auxiliary function for eraseProjIncFor -/
-partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
+partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (projCounts : ProjCounts)
+    (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask :=
   let done (_ : Unit)        := (bs ++ keep.reverse, mask)
-  let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b)
+  let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop projCounts mask (keep.push b)
   if h : bs.size < 2 then done ()
   else
     let b := bs.back!
@@ -65,7 +77,10 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
       let b' := bs[bs.size - 2]
       match b' with
       | .vdecl w _ (.proj i x) _ =>
-        if w == z && y == x then
+        -- We disable the inc optimization if there are multiple projections with the same base
+        -- and index, because the downstream transformations are incapable of correctly handling
+        -- the aliasing.
+        if w == z && y == x && projCounts[(x, i)]! == 1 then
           /- Found
              ```
              let z := proj[i] y
@@ -77,15 +92,15 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
           let mask := mask.set! i (some z)
           let keep := keep.push b'
           let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c p FnBody.nil)
-          eraseProjIncForAux y bs mask keep
+          eraseProjIncForAux y bs projCounts mask keep
         else done ()
       | _ => done ()
     | _ => done ()
 
 /-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`.
    Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/
 def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask :=
-  eraseProjIncForAux y bs (.replicate n none) #[]
+  eraseProjIncForAux y bs (computeProjCounts bs) (.replicate n none) #[]
 
 /-- Replace `reuse x ctor ...` with `ctor ...`, and remove `dec x` -/
 partial def reuseToCtor (x : VarId) : FnBody → FnBody