Laurel: field-granular modifies frame#1404
Conversation
`modifies o#f` now frames only the (o, f) pair, so that field may change while all other fields and objects stay fixed. Before, it framed the whole owner object. - ModifiesEntry gains a `.field objExpr fieldConst` case. - matchModifiesFieldRead matches a lowered `readField($heap, o, f)`. - buildNotModifiedForEntry emits `!($obj == o && $fld == f)`.
Parse modifies refs at precedence 0 so `modifies o#f` works without parentheses, like whole-object targets.
Tests for the field-granular frame, each checking the modified field can change while other fields and objects stay fixed: caller/callee enforcement, cross-type calls, opaque stubs, multiple and mixed targets, and inherited fields.
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
We need to add more documentation to the modifies field in LaurelAST, explicitly stating the allowed modes:
- single object
- object set
- field of single object
I think we could also support a "field of object set", but given that Laurel doesn't have sets yet it seems hard to test that.
There was a problem hiding this comment.
Reviewed for soundness; built at 3e52bce1d (suite green). The field-granular frame is sound: it's a frame tightening (.field adds !($obj==o && $fld==f) to notModified, preserving strictly more), the gate is safe since fieldConst is the per-type DeclaringType.fieldName constant (a#x can't free b#x), and aliasing holds — T9_ChainedFieldAccess's chainedMayAliasFails confirms a write through a possible alias isn't framed away. Frame violations caught, valid writes pass.
Non-blocking, reinforcing @keyboardDrummer's suggestion to stop HeapParameterization translating field reads in modifies clauses: matchModifiesFieldRead matches by callee text ("readField", startsWith "Box"), coupling to HeapParameterization's names and single-Box wrapping depth. If that pass changes, an o#f target silently falls through with no diagnostic. That suggestion (or the structured ModifiesTarget it proposes) removes this; short of that, share those names as constants.
List the allowed modifies forms on Body.Opaque: single object, object set, field of an object (o#f), and the wildcard.
Factor the repeated diagnostic construction in filterBodyNonCompositeModifies into a single helper.
Keep o#f modifies targets symbolic through heap parameterization and match them directly, removing the readField/Box string matching.
Validate modifies entries during resolution and remove the separate filter pass.
|
@keyboardDrummer @fabiomadge updated with your suggestions; one commit per suggestion |
|
Beautiful! Thanks so much |
github-actions
Bot
added
Has 1 approval
Waiting-For-Review
and removed
Waiting-For-Review
Has 1 approval
labels
The merge of reviewed-kbd-will-merge-to-main into the field-granular modifies branch left two bad conflict resolutions that broke the build: - Dropped the stale 2-arg `buildNotModifiedForEntry obj` call (type mismatch); kept the field-granular 3-arg `(obj, fld, entry)` version. - Removed `filterNonCompositeModifiesPass`, which referenced the deleted `filterNonCompositeModifies` (the non-composite check now lives in `Resolution.resolveModifiesEntry`). Verified `lake build Strata.Languages.Laurel.ModifiesClauses` and the full Laurel pipeline compile.
dbc48c6 to
49c518d
Compare
3 participants
Makes
modifies o#fframe only the (o, f) pair instead of the whole owner object: that field may change while all other fields and every other object stay fixed.#1402