Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix an issue with infinite loops while typechecking some expressions #4274

Merged
merged 11 commits into from
Dec 23, 2022
21 changes: 21 additions & 0 deletions .release-notes/4274.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
## Fix some infinite loops during typechecking

Some recursive constraints could cause the typechecker to go into
an infinite loop while trying to check subtyping. These infinite
loops have now been fixed. An example program that demonstrates
the issue is below:

```
primitive Foo[T: (Unsigned & UnsignedInteger[T])]
fun boom() =>
iftype T <: U8 then
None
end

actor Main
new create(env: Env) =>
Foo[U8].boom()
```

The use of T: UnsignedInteger[T] is valid and expected, but wasn't
being handled correctly in this situation by the typechecker in this context.
70 changes: 39 additions & 31 deletions src/libponyc/type/subtype.c
Original file line number Diff line number Diff line change
Expand Up @@ -60,39 +60,15 @@ static bool exact_nominal(ast_t* a, ast_t* b, pass_opt_t* opt)
return (a_def == b_def) && is_eq_typeargs(a, b, NULL, opt);
}

static bool check_assume(ast_t* sub, ast_t* super, pass_opt_t* opt)
{
// Returns true if we have already assumed sub is a subtype of super.
if(subtype_assume != NULL)
{
ast_t* assumption = ast_child(subtype_assume);

while(assumption != NULL)
{
AST_GET_CHILDREN(assumption, assume_sub, assume_super);

if(exact_nominal(sub, assume_sub, opt) &&
exact_nominal(super, assume_super, opt))
return true;

assumption = ast_sibling(assumption);
}
}

return false;
}

static bool push_assume(ast_t* sub, ast_t* super, pass_opt_t* opt)
static ast_t* push_assume(ast_t* sub, ast_t* super, pass_opt_t* opt)
{
if(check_assume(sub, super, opt))
return true;

(void)opt;
if(subtype_assume == NULL)
subtype_assume = ast_from(sub, TK_NONE);

BUILD(assume, sub, NODE(TK_NONE, TREE(ast_dup(sub)) TREE(ast_dup(super))));
ast_add(subtype_assume, assume);
return false;
return assume;
}

static void pop_assume()
Expand All @@ -107,6 +83,37 @@ static void pop_assume()
}
}

static bool check_assume(ast_t* sub, ast_t* super, pass_opt_t* opt)
{
bool ret = false;
// Returns true if we have already assumed sub is a subtype of super.
if(subtype_assume != NULL)
{
ast_t* assumption = ast_child(subtype_assume);
ast_t* new_assume = NULL;
new_assume = push_assume(sub, super, opt);

while(assumption != NULL && assumption != new_assume)
{
AST_GET_CHILDREN(assumption, assume_sub, assume_super);

if(exact_nominal(sub, assume_sub, opt) &&
exact_nominal(super, assume_super, opt))
{
ret = true;
break;
}

assumption = ast_sibling(assumption);
}
pony_assert(ret || (assumption == NULL));
pony_assert(ast_child(subtype_assume) == new_assume);
pop_assume();
}

return ret;
}

static bool is_sub_cap_and_eph(ast_t* sub, ast_t* super, check_cap_t check_cap,
errorframe_t* errorf, pass_opt_t* opt)
{
Expand Down Expand Up @@ -1122,12 +1129,13 @@ static bool is_nominal_sub_trait(ast_t* sub, ast_t* super,
static bool is_nominal_sub_nominal(ast_t* sub, ast_t* super,
check_cap_t check_cap, errorframe_t* errorf, pass_opt_t* opt)
{
// Add an assumption: sub <: super
if(push_assume(sub, super, opt))
return true;

// N k <: N' k'
ast_t* super_def = (ast_t*)ast_data(super);
if(check_assume(sub, super, opt))
return true;
// Add an assumption: sub <: super
push_assume(sub, super, opt);

bool ret = false;

switch(ast_id(super_def))
Expand Down
16 changes: 16 additions & 0 deletions test/libponyc-run/regression-3658/main.pony
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
primitive Foo[T: (Unsigned & UnsignedInteger[T])]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add a comment at the top level of this file explaining in general that this is a compile time check so the "additional cases" are covered because this is compile time, not runtime checking?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added in f16a0ea

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Er, I added the comment locally, not at the top, is that fine?

fun boom() =>
iftype T <: U8 then
None
end
// more cases
// note that these method bodies are checked at their definition
// site so there's no need to call them
fun baam1[S: (Unsigned & UnsignedInteger[S] & U8)](t: S): U32 =>
t.u32()
fun baam2[S: (U8 & Unsigned & UnsignedInteger[S])](t: S): U32 =>
t.u32()

actor Main
new create(env: Env) =>
Foo[U8].boom()
1 change: 0 additions & 1 deletion test/libponyc/type_check_subtype.cc
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,6 @@ TEST_F(SubTypeTest, IsSubTypePrimitiveTrait)
pass_opt_init(&opt);
}


TEST_F(SubTypeTest, IsSubTypeUnion)
{
const char* src =
Expand Down