-
Notifications
You must be signed in to change notification settings - Fork 38
feat!: Explicit effects system, prevent calls from annotated funcs to those with fewer effects #1723
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
feat!: Explicit effects system, prevent calls from annotated funcs to those with fewer effects #1723
Changes from all commits
66a397e
d5815fc
b28cdbd
96b9346
9a71a83
d8632ba
2afa232
4d256e5
706f062
1067f5c
10b682c
6f92edb
595e0bb
c1b6439
dd1245d
28454b4
be231e0
6ee59a3
dbc5fcb
87959e6
8782e3e
6224053
4284ee9
8965c2e
5cf12c7
ba705c8
797c20b
ab10061
39c6c8c
a307f02
028b8d5
4e97214
c6c8d47
93535dd
5a8053e
622cfbf
078c2c8
2aae8da
5c761ed
af1b7f2
0173ac0
645b10c
339389d
cba65d5
b1488a3
9fabd5c
442033e
5f22a66
279a4ab
8b662c5
06533b2
dcfe743
8cbd11a
6163444
328f8de
7e80ed8
6976d3b
4689bd4
af1f2e5
51745bf
4523d81
78f12ed
db75029
7b26c25
63a5b4e
8659f75
31b3a69
e532548
458de9a
dac0e57
33948ec
fa3ab4e
1f5ff09
74d1453
3810760
975bb02
4e64ea8
d5b45af
281501f
d7665a2
8ef3a39
1ffbeb1
01d26e4
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,7 +15,13 @@ | |
| from guppylang_internals.cfg.bb import BB | ||
| from guppylang_internals.cfg.builder import CFGBuilder | ||
| from guppylang_internals.checker.cfg_checker import CheckedCFG, check_cfg | ||
| from guppylang_internals.checker.core import Context, Globals, Place, Variable | ||
| from guppylang_internals.checker.core import ( | ||
| Context, | ||
| EffectLimitDecl, | ||
| Globals, | ||
| Place, | ||
| Variable, | ||
| ) | ||
| from guppylang_internals.checker.errors.generic import UnsupportedError | ||
| from guppylang_internals.checker.unitary_checker import check_invalid_under_dagger | ||
| from guppylang_internals.definition.common import DefId | ||
|
|
@@ -159,7 +165,16 @@ def check_global_func_def( | |
| generic_args = { | ||
| param.name: arg for param, arg in zip(generic_ty.params, type_args, strict=True) | ||
| } | ||
| return check_cfg(cfg, inputs, ty.output, generic_args, func_def.name, globals) | ||
| max_effects_from = EffectLimitDecl.for_def(ty, func_def) | ||
| return check_cfg( | ||
| cfg, | ||
| inputs, | ||
| ty.output, | ||
| generic_args, | ||
| func_def.name, | ||
| globals, | ||
| max_effects_from=max_effects_from, | ||
| ) | ||
|
|
||
|
|
||
| def check_nested_func_def( | ||
|
|
@@ -168,7 +183,13 @@ def check_nested_func_def( | |
| ctx: Context, | ||
| ) -> CheckedNestedFunctionDef: | ||
| """Type checks a local (nested) function definition.""" | ||
| func_ty = check_signature(func_def, ctx.globals) | ||
| # For now we assume the nested function has the same effects as that enclosing. | ||
| # We could do better by allowing a separate annotation (rather than a parameter | ||
| # to @guppy), but we will wait for callgraph analysis to compute precisely: | ||
| # nested functions are not part of any public API, so changes are not breaking. | ||
|
Comment on lines
+186
to
+189
Collaborator
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Does this guarantee that programs that compile with this version will still compile once we do callgraph analysis?
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Not if they do things with Callable, e.g. callgraph analysis figures out that inner is pure, but Callable is invariant. However with #1760 and existentials for the effects of the returned Callable then you could make it work if you declared |
||
| func_ty = check_signature(func_def, ctx.globals).with_effects( | ||
| None if ctx.max_effects_from is None else ctx.max_effects_from.effects | ||
| ) | ||
| assert func_ty.input_names is not None | ||
|
|
||
| if func_ty.parametrized: | ||
|
|
@@ -247,7 +268,17 @@ def check_nested_func_def( | |
| # Otherwise, we treat it like a local name | ||
| inputs.append(Variable(func_def.name, func_def.ty, func_def)) | ||
|
|
||
| checked_cfg = check_cfg(cfg, inputs, func_ty.output, {}, func_def.name, globals) | ||
| checked_cfg = check_cfg( | ||
| cfg, | ||
| inputs, | ||
| func_ty.output, | ||
| {}, | ||
| func_def.name, | ||
| globals, | ||
| # As comment above, assume nested func has same effects as enclosing | ||
| # (hence the decl giving the effects is that of the enclosing func too). | ||
| max_effects_from=ctx.max_effects_from, | ||
| ) | ||
| checked_def = CheckedNestedFunctionDef( | ||
| def_id, | ||
| checked_cfg, | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Instead of determining the callee this way, maybe accept an optional
DefIdto_check_effects? Or theCallableDefdirectly? I guess it would need to be threaded throughsynthesize_callthough :/There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, this is significantly better, but is quite a change to
check_call/synthesize_call. I've raised #1846 for this...