[vcg] add field-access support for record/union references#176
Conversation
| same assumption about `normal_error_1`, any checks under | ||
| `fatal_error_1` do *not* get the truth of `normal_error_1` asserted. | ||
|
|
||
| #### Two-phase check analysis |
There was a problem hiding this comment.
Check.uses_field_access is a @Property (no parentheses) but on Expression subclasses it is a regular method (with ()). Could we add a note about this or make them consistent? It is easy to miss when reading the code.
|
|
||
| This ordering cannot be observed at runtime (all checks are evaluated | ||
| in declaration order), but it is important for the VCG because the | ||
| uninterpreted-function model for referenced records requires that |
There was a problem hiding this comment.
"requires" feels too strong here the VCG is still sound without this ordering, it just produces more false positives. Suggest changing to "is more precise when" to avoid implying it would be broken without it.
| } | ||
|
|
||
| checks Container { | ||
| (forall e in items => e.value < limit), fatal "all items must be below limit" |
There was a problem hiding this comment.
The quantifier example (forall e in items => e.value < limit) currently produces a VCG warning "functional evaluation of field access not yet supported" — so the VCG does not analyse it. The docs should mention this limitation, otherwise users will expect VCG coverage they are not getting.
|
No test covers an unguarded optional ref in Phase B every Phase B optional test is either behind an implies guard or a Phase A fatal check. Please check a case like ref optional T; checks U { ref.x > 0, "potato" } where VCG should warn vcg-evaluation-of-null its needed or we can skip this |
|
The Phase B fatal quantifier (forall e in arr => e.x < x) is followed by a div-by-zero check on [len(arr) - 5] which has nothing to do with the quantifier result. So this test does not show that Phase B fatal knowledge actually helps a later check. it is necessary to add a second check that would give a false positive if the quantifier knowledge is missing, but passes when it is there? |
|
and please also add description |
hoe-jo
changed the title
hoe-jo
force-pushed
the
joho_enable_foreach
branch
from
1c17f75 to
17d848e
Compare
2 participants
The VCG previously had no support for checks that dereference a record
or union reference (e.g.
parent.priority > 0). This commit implementsthe full pipeline:
ast.py:
Expression.uses_field_access()base method: determine Field_Access_Expressionwhose prefix is a Record_Type or Union_Type.
Check.uses_field_accessas a @Property that lazily evaluatesand caches the result from the expression tree.
field value is any Expression, not just Implicit_Null.
vcg.py:
covers checks with no record/union field dereference and runs first.
Phase B ("after references") runs second, so it can exploit the
fatal-check knowledge accumulated by Phase A.