ponyc
ponyc copied to clipboard
ponylang
Crash with iftype and generic constraint
primitive Foo[T: (Unsigned & UnsignedInteger[T])]
fun boom() =>
iftype T <: U8 then
None
end
actor Main
new create(env: Env) =>
Foo[U8].boom()
@jemc found this.
It compiles correctly if the UnsignedInteger trait is not used as a constraint.
It appears any constraint that takes a [T] like Integer[T] causes the crash.
* thread #1, name = 'ponyc', stop reason = signal SIGSEGV: invalid address (fault address: 0x7fffff7feff8)
frame #0: 0x00000000007cee20 ponyc`pool_block_get(size=1024) at pool.c:602:41
599 // block info inside the block instead of using another data structure.
600 size_t rem = block->size - size;
601 block->size = rem;
-> 602 pool_block_header.total_size -= size;
603
604 if((block->prev != NULL) && (block->prev->size > block->size))
605 {
backtrace goes on and on... looks like a recursion issue.
here's a random grab on my part of what I saw repeating,
frame #11341: 0x000000000076b2cc ponyc`is_nominal_sub_nominal(sub=0x00007ffff3f44e80, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1115:6
frame #11342: 0x000000000076a515 ponyc`is_nominal_sub_x(sub=0x00007ffff3f44e80, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1284:14
frame #11343: 0x0000000000767daa ponyc`is_x_sub_x(sub=0x00007ffff3f44e80, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1672:14
frame #11344: 0x000000000076a06a ponyc`is_isect_sub_x(sub=0x00007ffff3f46500, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:642:8
frame #11345: 0x0000000000767d66 ponyc`is_x_sub_x(sub=0x00007ffff3f46500, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1666:14
frame #11346: 0x000000000076a72a ponyc`is_typeparam_sub_x(sub=0x00007ffff3f46e00, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1468:13
frame #11347: 0x0000000000767dcc ponyc`is_x_sub_x(sub=0x00007ffff3f46e00, super=0x00007ffff6982b80, check_cap=CHECK_CAP_SUB, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1675:14
frame #11348: 0x0000000000767bd1 ponyc`is_subtype(sub=0x00007ffff3f46e00, super=0x00007ffff6982b80, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1695:10
frame #11349: 0x000000000076881d ponyc`is_eqtype(a=0x00007ffff3f46e00, b=0x00007ffff6982b80, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:1718:10
frame #11350: 0x000000000076bc90 ponyc`is_eq_typeargs(a=0x00007ffff3f46c00, b=0x00007ffff6982980, errorf=0x0000000000000000, opt=0x00007fffffffe7d8) at subtype.c:202:9
frame #11351: 0x000000000076bb6f ponyc`exact_nominal(a=0x00007ffff3f46c00, b=0x00007ffff6982980, opt=0x00007fffffffe7d8) at subtype.c:60:30
frame #11352: 0x000000000076ba03 ponyc`check_assume(sub=0x00007ffff3f46c00, super=0x00007ffff6982b80, opt=0x00007fffffffe7d8) at subtype.c:74:10
frame #11353: 0x000000000076b408 ponyc`push_assume(sub=0x00007ffff3f46c00, super=0x00007ffff6982b80, opt=0x00007fffffffe7d8) at subtype.c:87:6
Did some grunt work in gdb that might be helpful. This is the sequence of calls in the loop, in execution order, with the first two AST args for each. I've "unparsed" the AST args to make it more readable.
is_typeparam_sub_x( T, U8 )
is_x_sub_x( ((U8|U16|U32|U64|U128|ULong|USize) & UnsignedInteger[T] & U8), U8 )
is_isect_sub_x( ((U8|U16|U32|U64|U128|ULong|USize) & UnsignedInteger[T] & U8), U8 )
is_x_sub_x( UnsignedInteger[T], U8 )
is_nominal_sub_x( UnsignedInteger[T], U8 )
is_nominal_sub_nominal( UnsignedInteger[T], U8 )
push_assume( UnsignedInteger[T], U8 )
check_assume( UnsignedInteger[T], U8 )
exact_nominal( UnsignedInteger[T], UnsignedInteger[U8] )
is_eq_typeargs( UnsignedInteger[T], UnsignedInteger[U8] )
is_eqtype( T, U8 )
is_subtype( T, U8 )
is_x_sub_x( T, U8 )
is_typeparam_sub_x( T, U8 )
At office hours a couple weeks ago, @jasoncarr0 with a little bit of input from me went through part of this issue with @adrianboyko. I believe that Adrian might reappear with a fix for this.
@mfelsche and I are continuing to look into this issue.
I've found that the troublesome infinite recursion can be avoided (at least for the particular Pony code cited in this issue) if the following code in make_iftype_typeparam:
BUILD(isect, new_constraint,
NODE(TK_ISECTTYPE,
TREE(ast_dup(current_constraint))
TREE(new_constraint)));
is changed to:
BUILD(isect, new_constraint,
NODE(TK_ISECTTYPE,
TREE(new_constraint)
TREE(ast_dup(current_constraint))));
I.e. the order of new_constraint and current_constraint is reversed in the created intersection type. This works because new_constraint satisfies an is_isect_sub_x test in the scenario but current_constraint leads to infinite recursion.
Since the order of the intersected types in the constructed type doesn't matter from a semantic perspective, I think this is probably a safe change (I'll try running it through the tests, to verify).
This stop-gap fix lets me continue work on the project that this bug blocked, but it doesn't actually address the possibility of infinite recursions in subtype checking. Here's a more detailed trace of the infinite recursion:
is_subtype_constraint: T / UnsignedInteger[T]
is_x_sub_x: T / UnsignedInteger[T]
is_typeparam_sub_x: T / UnsignedInteger[T]
is_typeparam_base_sub_x: T / UnsignedInteger[T]
is_typeparam_base_sub_x returned 0
is_x_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / UnsignedInteger[T]
is_isect_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / UnsignedInteger[T]
is_x_sub_x: (U8|...|USize) / UnsignedInteger[T]
is_union_sub_x: (U8|...|USize) / UnsignedInteger[T]
is_x_sub_x: U8 / UnsignedInteger[T]
is_nominal_sub_x: U8 / UnsignedInteger[T]
is_nominal_sub_nominal: U8 / UnsignedInteger[T]
push_assume: U8 / UnsignedInteger[T]
check_assume: U8 / UnsignedInteger[T]
check_assume returned 0
push_assume returned 0
is_nominal_sub_trait: U8 / UnsignedInteger[T]
is_x_sub_x: UnsignedInteger[U8] / UnsignedInteger[T]
is_nominal_sub_x: UnsignedInteger[U8] / UnsignedInteger[T]
is_nominal_sub_nominal: UnsignedInteger[U8] / UnsignedInteger[T]
push_assume: UnsignedInteger[U8] / UnsignedInteger[T]
check_assume: UnsignedInteger[U8] / UnsignedInteger[T]
exact_nominal: UnsignedInteger[U8] / U8
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_trait: UnsignedInteger[U8] / UnsignedInteger[T]
is_trait_sub_trait: UnsignedInteger[U8] / UnsignedInteger[T]
is_eq_typeargs: UnsignedInteger[U8] / UnsignedInteger[T]
is_eqtype: U8 / T
is_subtype: U8 / T
is_x_sub_x: U8 / T
is_nominal_sub_x: U8 / T
is_x_sub_typeparam: U8 / T
is_x_sub_x: U8 / (& (U8|...|USize) UnsignedInteger[T] U8)
is_nominal_sub_x: U8 / (& (U8|...|USize) UnsignedInteger[T] U8)
is_x_sub_isect: U8 / (& (U8|...|USize) UnsignedInteger[T] U8)
is_x_sub_x: U8 / (U8|...|USize)
is_nominal_sub_x: U8 / (U8|...|USize)
is_x_sub_union: U8 / (U8|...|USize)
is_x_sub_x: U8 / U8
is_nominal_sub_x: U8 / U8
is_nominal_sub_nominal: U8 / U8
push_assume: U8 / U8
check_assume: U8 / U8
exact_nominal: U8 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
exact_nominal returned 1
exact_nominal: U8 / UnsignedInteger[T]
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
is_nominal_sub_entity returned 1
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_union returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_x: U8 / UnsignedInteger[T]
is_nominal_sub_x: U8 / UnsignedInteger[T]
is_nominal_sub_nominal: U8 / UnsignedInteger[T]
push_assume: U8 / UnsignedInteger[T]
check_assume: U8 / UnsignedInteger[T]
exact_nominal: U8 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
exact_nominal returned 1
exact_nominal: UnsignedInteger[T] / UnsignedInteger[T]
is_eq_typeargs: UnsignedInteger[T] / UnsignedInteger[T]
is_eqtype: T / T
is_subtype: T / T
is_x_sub_x: T / T
is_typeparam_sub_x: T / T
is_typeparam_base_sub_x: T / T
is_typeparam_sub_typeparam: T / T
is_typeparam_sub_typeparam returned 1
is_typeparam_base_sub_x returned 1
is_typeparam_sub_x returned 1
is_x_sub_x returned 1
is_subtype returned 1
is_subtype: T / T
is_x_sub_x: T / T
is_typeparam_sub_x: T / T
is_typeparam_base_sub_x: T / T
is_typeparam_sub_typeparam: T / T
is_typeparam_sub_typeparam returned 1
is_typeparam_base_sub_x returned 1
is_typeparam_sub_x returned 1
is_x_sub_x returned 1
is_subtype returned 1
is_eqtype returned 1
is_eq_typeargs returned 1
exact_nominal returned 1
check_assume returned 1
push_assume returned 1
is_nominal_sub_nominal returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_x: U8 / U8
is_nominal_sub_x: U8 / U8
is_nominal_sub_nominal: U8 / U8
push_assume: U8 / U8
check_assume: U8 / U8
exact_nominal: U8 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
exact_nominal returned 1
exact_nominal: U8 / UnsignedInteger[T]
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
is_nominal_sub_entity returned 1
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_isect returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_typeparam returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_subtype returned 1
is_subtype: T / U8
is_x_sub_x: T / U8
is_typeparam_sub_x: T / U8
is_typeparam_base_sub_x: T / U8
is_typeparam_base_sub_x returned 0
is_x_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / U8
is_isect_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / U8
is_x_sub_x: (U8|...|USize) / U8
is_union_sub_x: (U8|...|USize) / U8
is_x_sub_x: U8 / U8
is_nominal_sub_x: U8 / U8
is_nominal_sub_nominal: U8 / U8
push_assume: U8 / U8
check_assume: U8 / U8
exact_nominal: U8 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
exact_nominal returned 1
exact_nominal: U8 / UnsignedInteger[T]
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
is_nominal_sub_entity returned 1
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_x: U16 / U8
is_nominal_sub_x: U16 / U8
is_nominal_sub_nominal: U16 / U8
push_assume: U16 / U8
check_assume: U16 / U8
exact_nominal: U16 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U16 / U8
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U16 / U8
is_nominal_sub_entity returned 0
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 0
is_nominal_sub_x returned 0
is_x_sub_x returned 0
is_union_sub_x returned 0
is_x_sub_x returned 0
INFINITE RECURSION BEGINS HERE
is_x_sub_x: UnsignedInteger[T] / U8
is_nominal_sub_x: UnsignedInteger[T] / U8
is_nominal_sub_nominal: UnsignedInteger[T] / U8
push_assume: UnsignedInteger[T] / U8
check_assume: UnsignedInteger[T] / U8
exact_nominal: UnsignedInteger[T] / UnsignedInteger[U8]
is_eq_typeargs: UnsignedInteger[T] / UnsignedInteger[U8]
is_eqtype: T / U8
is_subtype: T / U8
is_x_sub_x: T / U8
is_typeparam_sub_x: T / U8
is_typeparam_base_sub_x: T / U8
is_typeparam_base_sub_x returned 0
is_x_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / U8
is_isect_sub_x: (& (U8|...|USize) UnsignedInteger[T] U8) / U8
is_x_sub_x: (U8|...|USize) / U8
is_union_sub_x: (U8|...|USize) / U8
is_x_sub_x: U8 / U8
is_nominal_sub_x: U8 / U8
is_nominal_sub_nominal: U8 / U8
push_assume: U8 / U8
check_assume: U8 / U8
exact_nominal: U8 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
exact_nominal returned 1
exact_nominal: U8 / UnsignedInteger[T]
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U8 / U8
is_eq_typeargs: U8 / U8
is_eq_typeargs returned 1
is_nominal_sub_entity returned 1
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 1
is_nominal_sub_x returned 1
is_x_sub_x returned 1
is_x_sub_x: U16 / U8
is_nominal_sub_x: U16 / U8
is_nominal_sub_nominal: U16 / U8
push_assume: U16 / U8
check_assume: U16 / U8
exact_nominal: U16 / UnsignedInteger[U8]
exact_nominal returned 0
exact_nominal: U16 / U8
exact_nominal returned 0
check_assume returned 0
push_assume returned 0
is_nominal_sub_entity: U16 / U8
is_nominal_sub_entity returned 0
pop_assume
pop_assume returned -
is_nominal_sub_nominal returned 0
is_nominal_sub_x returned 0
is_x_sub_x returned 0
is_union_sub_x returned 0
is_x_sub_x returned 0
NEXT CYCLE THROUGH THE RECURSION STARTS HERE
is_x_sub_x: UnsignedInteger[T] / U8
...
@adrianboyko just for my understanding, was there an issue with changing to syntactic equality to fix it, did that not stop the loop?
The suggestion was to replace the eq_typeargs call in exact_nominal with a while loop copied from elsewhere in the code. The while loop was supposed to perform basic syntactic comparison of any typeargs. I did try this proposed fix but it didn't work for me. Looking at the stack traces now, I'm not even sure why we thought it would help. I think I had a bad idea about how the pushed assumptions are used, and that sent us in the wrong direction.
Since you mentioned that check_assume is just an optimization, I also tried commenting it out to see if the problem vanished with it -- the reasoning being that exact_nominal is only ever called by check_assume. The problem persisted after check_assume was removed, so I decided that any proposed fix to exact_nominal would not suffice. I then started my analysis over, from scratch.
@adrianboyko I'm not sure I understand. The listed infinite loop in the comment just above here includes check_assume in it, is there a separate infinite loop besides that first one? I believe we tested during the office hours call and if I remember correctly (a tall order) then removing check_assume was sufficient to make it terminate.
@jasoncarr0, I think that push_assume and pop_assume are virtually no-ops without check_assume, so I restored it and didn't produce any traces that don't include check_assume.
I just went back to the beginning and tried to fix exact_nominal, again. What do you think of the following?
This seems to work, as far as I've tested it, so far. I doubt that ast_print_type is the most efficient way to do the syntactic comparison, but it was easy for this experiment.
@adrianboyko noooo push_assume and pop_assume do a whole lot of things regardless of check_assume. check_assume does only one thing: it's seeing if a specific assumption has already been pushed. The entire thing that comes from having an assumption is still important: it's still used for typechecking more.
That code diff is almost right, "syntactic equality" is synonymous with the "exact equal" function name. In this case, instead of your ast_print_type line, you can use the check if (!exact_nominal(a_arg, b_arg))
Oh, actually you are a bit right here with check_assume. The naming/usage is very confusing so it may also be that there's some incorrect info here, it definitely can't be removed because the existing code returns true or false as to whether it can already prove subtyping, that's an unfortunate entanglement and there may need to be more extensive changes overall to make sure everything is sound.
Interestingly this is also reproducible without iftype:
actor Main
// ponyc is failing with checking this constraint, which is also what is artificially constructed in the iftype example above
fun baam[T: (Unsigned & UnsignedInteger[T] & U8)](t: T): U32 =>
t.u32()
new create(env: Env) =>
None
Interestingly when changing the order, it works terminates successfully:
actor Main
// when ordered as (Unsigned & U8 & UnsignedInteger[T]) it works as well
fun baam[T: (U8 & Unsigned & UnsignedInteger[T])](t: T): U32 =>
t.u32()
new create(env: Env) =>
None
@mfelsche, The order matters because the subtyping rules for intersections don't necessarily need to check all types that are intersected to determine that a subtype relation does or does not exist. Whether or not the intersection code has to deal with the type that causes the infinite recursion will sometimes depend on the order of the intersected types.
@jasoncarr0, the typeargs are sometimes typeparamrefs, but exact_nominal expects nominals.
Right, I need to take a second look at this. Worst case we can talk more on it during office hours this week. The intersection hack might work in the short term but seems extremely fragile and could possibly break other code?
@adrianboyko you can adjust it to support type param refs as well, by just checking that they're identical.
I believe this will work, although I'm suddenly no longer convinced that our current implementation is fully correct, but this will work to cover most of the current.