5949ae8664
This PR fixes an issue in the expand reset reuse pass that causes segfaults in very rare situations. This bug occurs in situations where two projections from the same field happen right before a reset, for example: ``` let x.2 := oproj[0] _x.1; inc x.2; let x.3 := oproj[0] _x.1; inc x.3; let _x.4 := reset[1] _x.1; ``` when expand reset reuse we optimize situations like this to only `inc` on the cold path as on the hot path we are going to keep the projectees alive until at least `reuse` by just not `dec`-ing the resetee. However, the algorithm for this assumed that we do not project more than once from each field and thus removed both `inc x.2` and `inc x.3` which is too much. The bug was masked compared to the original #13407 that was reproducible in 4.29, because the presented code relied on semantics of global constants which were changed in 4.30. The PR contains a modified (and more consistent) reproducer. Closes: #13407 Co investigated with @Rob23oba
64 lines
2.3 KiB
Text
64 lines
2.3 KiB
Text
module
|
||
|
||
/-! Regression test for issue 13407 -/
|
||
|
||
inductive Result (α : Type) where | ok (x : α) | err
|
||
instance : Monad Result where
|
||
pure x := .ok x
|
||
bind s f := match s with | .ok x => f x | .err => .err
|
||
instance : Coe α (Result α) where coe x := .ok x
|
||
|
||
structure Int' (bits : Nat) where val : Nat
|
||
|
||
def Int'.wrap (n : Int) (bits : Nat) : Int' bits := ⟨(n % (2^bits : Int)).toNat⟩
|
||
|
||
def Int'.toInt (x : Int' bits) : Int :=
|
||
if x.val < 2^(bits - 1) then ↑x.val else ↑x.val - ↑(2^bits)
|
||
|
||
instance (n : Nat) : OfNat (Int' bits) n where ofNat := ⟨n % (2^bits)⟩
|
||
instance : Neg (Int' bits) where neg x := Int'.wrap (-Int'.toInt x) bits
|
||
instance : Repr (Int' bits) := ⟨fun x _ => repr (Int'.toInt x)⟩
|
||
|
||
class BinOp1 (α β : Type) (γ : outParam Type) where binOp1 : α → β → γ
|
||
class BinOp2 (α β : Type) (γ : outParam Type) where binOp2 : α → β → γ
|
||
class UnaryOp (α : Type) (β : outParam Type) where unaryOp : α → β
|
||
class Cast (α β : Type) where cast : α → Result β
|
||
|
||
instance : BinOp1 (Int' b) (Int' b) (Result (Int' b)) where
|
||
binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
|
||
|
||
instance : BinOp1 (Int' l) (Int' r) (Result (Int' l)) where
|
||
binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) l)
|
||
|
||
instance : BinOp2 (Int' b) (Int' b) (Result (Int' b)) where
|
||
binOp2 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
|
||
|
||
instance : UnaryOp (Int' b) (Result (Int' b)) where
|
||
unaryOp a := .ok (Int'.wrap (-(a.toInt + 1)) b)
|
||
|
||
instance : Cast (Int' n) (Int' m) where
|
||
cast x := .ok (Int'.wrap x.toInt m)
|
||
|
||
set_option linter.unusedVariables false
|
||
|
||
def helper (_ : Nat) : Result (Int' 64) := UnaryOp.unaryOp (1 : Int' 64)
|
||
|
||
def test (a : Nat) : Result (Int' 16) := do
|
||
let x ← UnaryOp.unaryOp (1 : Int' 16)
|
||
let y ← BinOp2.binOp2
|
||
(← (Cast.cast (← helper a) : Result (Int' 128)))
|
||
(← BinOp1.binOp1
|
||
(← (Cast.cast (← helper a) : Result (Int' 128)))
|
||
(← BinOp2.binOp2
|
||
(← BinOp1.binOp1 (10 : Int' 128) (1 : Int' 128))
|
||
(← BinOp2.binOp2 (7 : Int' 128) (3 : Int' 128))))
|
||
BinOp1.binOp1
|
||
(← (Cast.cast (← (Cast.cast y : Result (Int' 128))) : Result (Int' 16)))
|
||
(← BinOp2.binOp2 x (← BinOp2.binOp2 x x))
|
||
|
||
/-- info: 11 -/
|
||
#guard_msgs in
|
||
#eval do
|
||
match test 0 with
|
||
| .ok v => IO.println (repr v)
|
||
| .err => IO.println "ERR"
|