Runtime segfault when matching on capabilities via generics

[jasoncarr0]

This program uses generics to match on capabilities and causes the compiler to segfault as of release 0.42.0

class Weird[S, T]
  new create(out: OutStream, x: (S | T)) =>
    match x
    | let _: T => out.print("Was a T")
    | let _: S => out.print("Was an S")
    end

actor Main
  new create(env: Env) =>
    let s1: String ref = String
    Weird[String ref, String val](env.out, s1)

The segfault occurs regardless of branch order

[jasoncarr0]

Using lldb on a debug version of the compiler

* thread #1, name = 'ponyc', stop reason = signal SIGSEGV: invalid address (fault address: 0x0)
  * frame #0: 0x00000000007e9cc0 ponyc`llvm::BasicBlock::getContext() const
    frame #1: 0x00000000008a9d59 ponyc`llvm::BranchInst::BranchInst(llvm::BasicBlock*, llvm::Instruction*) + 25
    frame #2: 0x00000000008116ae ponyc`LLVMBuildBr + 62
    frame #3: 0x000000000073183f ponyc`gen_match(c=0x00007fffffffd400, ast=<unavailable>) at genmatch.c:825:7
    frame #4: 0x000000000072e6cf ponyc`gen_expr(c=0x00007fffffffd400, ast=0x00007ffff72b6700) at genexpr.c:88:13
    frame #5: 0x00000000007b147b ponyc`gen_seq(c=0x00007fffffffd400, ast=<unavailable>) at gencontrol.c:22:13
    frame #6: 0x000000000072e802 ponyc`gen_expr(c=0x00007fffffffd400, ast=0x00007ffff72b4a00) at genexpr.c:26:13
    frame #7: 0x00000000007b460e ponyc`genfun_method_bodies [inlined] genfun_new(c=0x00007fffffffd400, t=0x00007ffff392b400, m=<unavailable>) at genfun.c:539:24
    frame #8: 0x00000000007b4511 ponyc`genfun_method_bodies [inlined] genfun_method(c=0x00007fffffffd400, t=0x00007ffff392b400, n=<unavailable>, m=<unavailable>) at genfun.c:773:15
    frame #9: 0x00000000007b3d5d ponyc`genfun_method_bodies(c=0x00007fffffffd400, t=0x00007ffff392b400) at genfun.c:932:11
    frame #10: 0x000000000074246c ponyc`gentypes(c=0x00007fffffffd400) at gentype.c:817:9
    frame #11: 0x000000000072df56 ponyc`genexe(c=0x00007fffffffd400, program=0x00007ffff7c12cc0) at genexe.c:571:7
    frame #12: 0x00000000007254bd ponyc`codegen(program=0x00007ffff7c12cc0, opt=<unavailable>) at codegen.c:899:10
    frame #13: 0x000000000071aac8 ponyc`compile_package(path=<unavailable>, opt=0x00007fffffffd880, print_program_ast=<unavailable>, print_package_ast=false) at main.c:67:13
    frame #14: 0x000000000071a9a1 ponyc`main(argc=<unavailable>, argv=0x00007fffffffda88) at main.c:133:13
    frame #15: 0x00007ffff7c7c780 libc.so.6`__libc_start_main + 208
    frame #16: 0x000000000071a69a ponyc`_start at start.S:120

[jasoncarr0]

Actually, this may just be a duplicate of https://github.com/ponylang/ponyc/issues/3447

[jasoncarr0]

I'll stop re-opening and closing this. This seems to have some unique value in that it depends on the capabilities involved. If the val is changed to box then it doesn't result in a crash. It may still be an instance though

[jemc]

Discussed in today's sync call.

This needs to be rejected by the compiler, but it's unfortunate we can't actually reject it during type checking because we have no concept of disjointness constraints on type parameters in Pony.

So in the short term, to fix the segfault, we'd need to modify the codegen pass to print a helpful error for this, such as:

String ref and String val type are not disjoint at runtime, so this match can violate capabilities

However, the bigger problem here is that this case reveals that it is possible to write a generic in Pony which passes its own type-checks, but there exists an instantiation of it that would not be sound to execute at runtime. Pony generics were designed to not behave this way (type-checking the generic symbolically once should be sufficient to prove soundness) but this is a case where that design fails to work.

This bigger problem is not necessarily an obscure edge case - there probably exist many generics even in the standard library that could trigger this segfault (or if not for the segfault, unsound cap-breaking runtime behavior) if instantiated in the "wrong" way. Anything that matches on something like (A | None val) without proving the runtime-disjointness of A from None val are open to this kind of attack if A is given as something like None ref, potentially allowing you to obtain a None ref from a None val. The particular example of None is not so scary on its own, since None has no mutable methods, so None ref is more nonsensical than dangerous. However, it illustrates how widespread this kind of unsound matching is.

If we wish to fix that bigger problem, we'd have to go down one of two paths:

• :one: Encode cap information in all object pointers, so that we can successfully match by cap at runtime.

• :two: Add disjointness constraints to the language for type parameters, and either require them to be explicitly by any generic code that needs it (for example, in many places in the standard library), or make them implicit when the compiler detects such a possibly-problematic match (such that the compiler could enforce the constraint, but not make the user type it). The latter is likely "too magic" though it would make this a (mostly) non-breaking change for Pony source code bases.

[jasoncarr0]

At this point, I'm convinced that :two: might be untenable because private types need to be exposed in disjointness constraints due to the potential to escape into interfaces. Imagine (_Private val | T) where we instantiate T with Any ref and it happens to hold a _Private ref.

Other options here:

• :three: Restrict the capabilities that can appear together in a match involving generics. This already happens sometimes, as far as I'm aware, but it's not clear when, including with some variations on the example below.

• :four: Force some encoding that ensures that they're treated like ADTs, this could get confusing if not reflected in the language. This is a solution to the issue with :two: , in effect, as it re-enables encapsulation. This already happens sometimes, as the example below shows.

It's not sufficient to avoid matching on generic types themselves. Of course this example seems to be mis-compiled so that else branch is taken. This is a variation on solution :four: that's been already implemented, but a particularly confusing one. I was originally in favor of disjoint types because I recalled some need to match on concrete types first for this reason.

class Worse[T]
  new create(out: OutStream, x: (String | T)) =>
    match x
    | let s: String val => out.print(s)
    else
      out.print("If x was a String you bet the compiler acted weirdly")
    end

actor Main
  new create(env: Env) =>
    let s1: String ref = String
    Worse[String ref](env.out, s1) // replace with String iso argument if desired
    s1.append("Ohno")

[jemc]

I'm convinced that :two: might be untenable because private types need to be exposed in disjointness constraints due to the potential to escape into interfaces. Imagine (_Private val | T) where we instantiate T with Any ref and it happens to hold a _Private ref.

I don't understand the problem here - can you elaborate?

That is, I see no problem with the compiler enforcing disjointness of a private type with a public interface.

What am I missing?

[jasoncarr0]

Sorry, yes it's possible, but it does mean that all of the uses of private types have to appear in disjointness constraints, or the disjointness constraints need to have a complicated and hard to explain relation with capabilities.

Simply that it gets confusing when we have a constraint: T # _Private when the name _Private isn't even a visible member at all. But it's necessary just in case another method somewhere returns an interface I, including Any, which happens to itself overlap with _Private, and then someone instantiates T with I, so it now overlaps with _Private.

[SeanTAllen]

Was this a compiler segfault or a runtime segfault? With 0.53.0, this compiles and segfaults when run.

[jasoncarr0]

@SeanTAllen This was originally a compiler segfault, when generating the code. See the comment https://github.com/ponylang/ponyc/issues/3952#issuecomment-998482907

We could rename the issue