Segfault with UInt64 structs

Stream: lean4

[Geoffrey Irving]

Anyone know why this UInt64 computation segfaults? It has no imports, but seems fragile when I try to minimise it further. I'm on leanprover/lean4:v4.22.0-rc4.

structure UInt128 where
  lo : UInt64
  hi : UInt64

instance : Neg UInt128 where
  neg x := ⟨~~~x.lo + 1, ~~~x.hi + 1⟩

def add (x y : UInt128) : UInt128 :=
  ⟨x.lo + y.lo, 1 + x.hi + y.hi⟩

def of_lo (x : UInt64) : UInt128 := ⟨x, 0⟩

def exp (x t : UInt64) : UInt128 :=
  add (of_lo x) (-(of_lo t))

#eval (exp 9223372036854775748 2).lo  -- Segfault

It seems to be segfaulting trying to unbox something:

julia:interval% lake env lldb -- $(/usr/bin/which lean) test/segfault.lean
(lldb) target create "/opt/homebrew/bin/lean"
Current executable set to '/opt/homebrew/bin/lean' (arm64).
(lldb) settings set -- target.run-args  "test/segfault.lean"
(lldb) run
Process 22301 launched: '/opt/homebrew/bin/lean' (arm64)
Process 22301 stopped
* thread #2, stop reason = exec
    frame #0: 0x00000001000149c0 dyld`_dyld_start
dyld`_dyld_start:
->  0x1000149c0 <+0>:  mov    x0, sp
    0x1000149c4 <+4>:  and    sp, x0, #0xfffffffffffffff0
    0x1000149c8 <+8>:  mov    x29, #0x0 ; =0
    0x1000149cc <+12>: mov    x30, #0x0 ; =0
Target 0: (lean) stopped.
(lldb) c
Process 22301 resuming
Process 22301 stopped
* thread #4, stop reason = EXC_BAD_ACCESS (code=1, address=0x9)
    frame #0: 0x000000010c459860 libleanshared.dylib`lean::ir::unbox_t(lean_object*, lean::ir::type) + 48
libleanshared.dylib`lean::ir::unbox_t:
->  0x10c459860 <+48>: ldr    x0, [x0, #0x8]
    0x10c459864 <+52>: ldp    x29, x30, [sp, #0x10]
    0x10c459868 <+56>: ldp    x20, x19, [sp], #0x20
    0x10c45986c <+60>: ret
Target 0: (lean) stopped.
(lldb) bt
* thread #4, stop reason = EXC_BAD_ACCESS (code=1, address=0x9)
  * frame #0: 0x000000010c459860 libleanshared.dylib`lean::ir::unbox_t(lean_object*, lean::ir::type) + 48
    frame #1: 0x000000010c45f948 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3160
    frame #2: 0x000000010c45be94 libleanshared.dylib`lean::ir::interpreter::load(lean::name const&, lean::ir::type) + 488
    frame #3: 0x000000010c45f948 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3160
    frame #4: 0x000000010c45be94 libleanshared.dylib`lean::ir::interpreter::load(lean::name const&, lean::ir::type) + 488
    frame #5: 0x000000010c45f948 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3160
    frame #6: 0x000000010c46185c libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1224

[Eric Wieser]

This also fails:

structure UInt128 where
  lo : UInt64
  hi : UInt64

def zero : UInt128 := ⟨0, 0⟩

def exp : UInt64 := ~~~zero.hi

#eval exp

[Geoffrey Irving]

Replacing Neg with a plain function fixes it, but I don't know why type classes would matter.

[Aaron Liu]

typeclasses are inlined maybe?

[Aaron Liu]

what happens when you make Neg a plain function but also @[inline]?

[Eric Wieser]

Edited above, fails without any typeclasses

[Eric Wieser]

I think the issue is that 0 fits in a tagged pointer but ~~~0 does not

[Geoffrey Irving]

Oh, wild! Seems dangerous if the compiler is trying to unbox fully 64-bit values.

[Eric Wieser]

cc @Cameron Zwarich

[Robin Arnez]

Oh this is bad:

def exp._closed_0 : u64 :=
  let x_1 : obj := 0;
  let x_2 : u64 := UInt64.complement x_1;
  ret x_2

It should take (0 : UInt64) but is provided with (0 : Nat)

[Henrik Böving]

It should also be constant folded but that's more of a missing feature

[Geoffrey Irving]

^ Though that would have made it harder to minimise! :)

[Jovan Gerbscheid]

How do you know it isn't constant folded? exp and zero here are constants themselves, and I'd think at runtime they would be evaluated at most once.

[Robin Arnez]

This is probably too imprecise: https://github.com/leanprover/lean4/blob/8f575bf9868a11f7d74bbcf2e1b26c30a5b8a85e/src/Lean/Compiler/LCNF/ElimDeadBranches.lean#L177-L184

def ofLCNFLit : LCNF.LitValue → Value
| .nat n => ofNat n
-- TODO: We could make this much more precise but the payoff is questionable
| .str .. => .top
| .uint8 v => ofNat (UInt8.toNat v)
| .uint16 v => ofNat (UInt16.toNat v)
| .uint32 v => ofNat (UInt32.toNat v)
| .uint64 v | .usize v => ofNat (UInt64.toNat v)

[Henrik Böving]

Jovan Gerbscheid said:

How do you know it isn't constant folded? exp and zero here are constants themselves, and I'd think at runtime they would be evaluated at most once.

That closed term can obviously be evaluated to a constant right away instead of doing a function call.

[Henrik Böving]

Robin Arnez said:

This is probably too imprecise: https://github.com/leanprover/lean4/blob/8f575bf9868a11f7d74bbcf2e1b26c30a5b8a85e/src/Lean/Compiler/LCNF/ElimDeadBranches.lean#L177-L184

def ofLCNFLit : LCNF.LitValue → Value
| .nat n => ofNat n
-- TODO: We could make this much more precise but the payoff is questionable
| .str .. => .top
| .uint8 v => ofNat (UInt8.toNat v)
| .uint16 v => ofNat (UInt16.toNat v)
| .uint32 v => ofNat (UInt32.toNat v)
| .uint64 v | .usize v => ofNat (UInt64.toNat v)

This pass is not at all related to constant folding, it's an abstract interpreter for eliminating branches that can never be hit. Constant folding happens in the simplifier and doesn't trigger because UInt.complement didn't exist when I wrote it.

[Jovan Gerbscheid]

Henrik Böving said:

That closed term can obviously be evaluated to a constant right away instead of doing a function call.

Hmm, it was my understanding that that is what the compiler does: evaluate it to a constant, instead of doing the function call. This runtime behaviour just isn't reflected very clearly in the trace.

[Henrik Böving]

It is the job of the compiler to do that but it doesn't

[Robin Arnez]

Henrik Böving schrieb:

This pass is not at all related to constant folding, it's an abstract interpreter for eliminating branches that can never be hit.

You'd think but

  [floatLetIn] size: 4
      def exp : UInt64 :=
        let _x.1 := zero;
        cases _x.1 : UInt64
        | UInt128.mk lo hi =>
          let _x.2 := UInt64.complement hi;
          return _x.2
  [] new compiler phase: mono, pass: elimDeadBranches ▶
  [elimDeadBranches] size: 6
      def exp : UInt64 :=
        let _x.1 := zero;
        cases _x.1 : UInt64
        | UInt128.mk lo hi =>
          let _x.2 := 0;
          let _x.3 := 0;
          let _x.4 := UInt64.complement _x.2;
          return _x.4

I can't really look at the types of these but I'd guess _x.2 is typed Nat here

[Henrik Böving]

Oh I thought you meant to implement the constant folding, it's totally plausible that elim dead branches is at fault yeah, I wrote it blindly back when we had no means to execute LCNF so it's certainly not as well tested as it could be by now.

[Robin Arnez]

Actually yeah I can (pp.letVarTypes)

  [floatLetIn] size: 4
      def exp : UInt64 :=
        let _x.1 : UInt128 := zero;
        cases _x.1 : UInt64
        | UInt128.mk lo hi =>
          let _x.2 : UInt64 := UInt64.complement hi;
          return _x.2
  [] new compiler phase: mono, pass: elimDeadBranches ▶
  [elimDeadBranches] size: 6
      def exp : UInt64 :=
        let _x.1 : UInt128 := zero;
        cases _x.1 : UInt64
        | UInt128.mk lo hi =>
          let _x.2 : Nat := 0;
          let _x.3 : Nat := 0;
          let _x.4 : UInt64 := UInt64.complement _x.2;
          return _x.4

[Robin Arnez]

Yeah it's elimDeadBranches

[Cameron Zwarich]

Thanks for tracking it down, @Robin Arnez. This code is making an assumption that all boxed integer values are represented uniformly, but this is not actually the case: a boxed Nat 0 will be represented as 0x1, whereas a boxed UInt64 0 will be represented as an allocation containing a single 0 field. If we switched boxed UInt64 to use the same representation as Nat, this problem would go away.

[Robin Arnez]

Even if we're in mono, it should still not change the type though? UInt64 is an unboxed u64 and Nat is an obj.

[Cameron Zwarich]

While LCNF tries to preserve types (more in base than in mono), it is more for optimization hints. In mono, we would be okay if the two types had the same runtime representation. Another example where we do this is with constructors of inductives; we sometimes erase their parameters and can no longer distinguish between values that originated with those distinct parameters. This is acceptable because we use a uniform representation that never actually depends on the parameters.

[Cameron Zwarich]

lean4#9703

[Geoffrey Irving]

I'm excited this is merged! What's the ETA for it showing up in a Lean release? I'd be curious to see if there are any other compiler bugs uncovered by all of my UInt64 code.

Alternatively, is there an easy way for me to test prior to it showing up in a release?

[Robin Arnez]

Just selected "Lean Nightly" on https://live.lean-lang.org. For that you'll just need to wait one day.

[Geoffrey Irving]

Will Mathlib usually compile against nightly? (My code is dependently typed with types that depend on big chunks of Mathlib to get to the parts I want to run.)

[Eric Wieser]

No, it certainly won't

[Eric Wieser]

Perhaps @Cameron Zwarich has plans to backport to a 4.22.0-rc5?

[Cameron Zwarich]

I merged it to the 4.22.0 branch, but I don’t think there’s a need to spin another RC for this, since the fix I picked just disables the optimization for these literal types.

[Robin Arnez]

There is https://github.com/leanprover-community/mathlib4-nightly-testing/ but there is no "easy" way of getting it to run such as through live.lean-lang.org

[Eric Wieser]

By which you mean "this will land in the 4.22.0 release at the end of the release cycle, but there's no need to do an additional test release because it's not going to break anything"?

[Robin Arnez]

Turns out adding mathlib4-nightly-testing as a dependency works well enough (just tested):

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4-nightly-testing.git"

Note though that this revision does not fully build so you can't actually import Mathlib

[Robin Arnez]

If you want that then you can specify the revision 2938a33f27851461e335c0d0be408d976dddb0e3 which is the last one that built but then you're not going to get the fix

[Robin Arnez]

The last option would just be to wait

[Geoffrey Irving]

Yep, I may wait then. Might resurrect my attempt at the Koebe quarter theorem in the mean time.

[Kim Morrison]

Regarding using Mathlib on nightly releases: please look for the nightly-testing-YYYY-MM-DD tags that appear on the https://github.com/leanprover-community/mathlib4-nightly-testing fork. These don't necessarily get generated every day, but when they are generated they are guaranteed to work (and use the relevant Lean4 nightly toolchain).

[Geoffrey Irving]

Updating https://github.com/girving/interval to to leanprover/lean4:v4.23.0-rc2 fixes the problem, so that compiler bug was the only issue. :tada: