[vcg] add field-access support for record/union references

CHANGELOG.md

@@ -26,6 +26,9 @@ generated in the following situations:
 
 ### 2.0.5-dev
 
+* [TRLC] Add VCG support for field access on record/union references
+  (two-phase check analysis, #156 step 2/2).
+
 * [TRLC, API] Fix various typos in the documentation.
 
 * [TRLC, LRM] Allow union types as tuple field types:

documentation/TUTORIAL-CHECKS.md

@@ -181,7 +181,43 @@ checks Requirement {
 }
 ```
 
-## Current limitations and notes
+## Following references
 
-Right now it is not possible to "follow references" in the check
-language. We are considering to add this in a future release.
+It is possible to access fields of a referenced record directly in
+check expressions using the `.` operator. For example, given:
+
+```
+type Node {
+  value Integer
+  next  optional Node
+}
+
+checks Node {
+  next != null implies next.value > value, fatal "must be in order"
+}
+```
+
+You can also use field access inside quantifiers. For example, if you
+have an array of record references you can write:
+
+```
+type Item {
+  value Integer
+}
+
+type Container {
+  items Item [0 .. *]
+  limit Integer
+}
+
+checks Container {
+  (forall e in items => e.value < limit), fatal "all items must be below limit"
+}
+```
+
+Note that accessing a field on an optional reference without a null
+guard will produce a runtime error if the reference is null. The
+static analyser (VCG) will check for potential null dereferences and
+warn you accordingly. This extends to quantifier bodies: if `value`
+were declared `optional`, the VCG would warn about the dereference
+inside the `forall` expression.

documentation/architecture.md

@@ -977,6 +977,62 @@ that `fatal_error_1` could not have occurred. But we cannot make the
 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
+
+Checks within a type are split into two phases before building the VCG graph:
+
+* **Phase A — "at declaration"**: Checks whose expressions do *not*
+  dereference any record or union reference (i.e., the expression
+  tree contains no `Field_Access_Expression` with a `Record_Type` or
+  `Union_Type` prefix). These checks operate only on the type's own
+  components and are analyzed first.
+
+* **Phase B — "after references"**: Checks whose expressions *do*
+  dereference a record or union reference via a `Field_Access_Expression`.
+  These are analyzed after Phase A, so they benefit from any
+  knowledge accumulated by Phase A `fatal` checks.
+
+The classification is computed lazily and cached on each `Check` node
+via `Check.uses_field_access`. Note that on `Check` this is a
+`@property` (no parentheses), whereas the same-named method on
+`Expression` subclasses is a regular method (called with `()`).
+
+The asymmetry is intentional. `Check` is a stable, long-lived AST
+node; its expression tree never changes, so caching the result in
+`_uses_field_access` is safe and future-proofs against callers that
+may read the property more than once. `Expression` subclasses recurse
+into their children and are only ever called from within that `Check`
+property, so they execute at most once already — adding a backing
+field and lazy-init boilerplate to every one of the ~15 concrete
+expression classes would cost more than it saves.
+
+The split is implemented in `checks_on_composite_type` as two passes
+over `iter_checks()`, with Phase B having access to the
+`fatal`-accumulated state from Phase A.
+
+This ordering cannot be observed at runtime (all checks are evaluated
+in declaration order), but the VCG is more precise when
+non-reference checks have already contributed their `fatal` knowledge
+before reference-based checks are proved.
+
+The reason precision improves is rooted in how referenced records are
+modelled. A record reference (e.g. `parent optional Requirement`) is
+encoded as a bare integer (the record's unique ID). To access a field
+on it — say `parent.priority` — the VCG creates an *uninterpreted
+function* `access.Package.Requirement : Int → RecordSort` that maps
+the ID to a synthetic SMT record sort. An uninterpreted function is
+axiom-free: the solver can assign any field value it pleases unless we
+have added explicit assertions. Phase A `fatal` checks establish
+concrete facts about the type's *own* components (integers, booleans,
+etc.) without involving any UF. When those facts are in the SMT
+context before Phase B runs, they constrain what the solver can try
+when reasoning about UF results — for example, knowing `severity <= 3`
+(fatal, Phase A) means the solver cannot use `severity = 99` when
+trying to defeat a later Phase B check on `parent.priority >
+severity`. Without the split the Phase A knowledge would arrive too
+late and the solver would treat the component as unbounded, producing
+a false positive.
+
 #### Types
 
 We model types as follows

tests-system/vcg-field-access-basic/output

@@ -0,0 +1,18 @@
+c, "potato"
+^ vcg-field-access-basic/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
+| example record_type triggering error:
+|   T bad_potato {
+|     x = 0
+|     /* ref is null */
+|     /* c is null */
+|   }
+10 / len(ref.x) > 0, "potato"
+   ^ vcg-field-access-basic/test2.rsl:9: issue: divisor could be 0 [vcg-div-by-zero]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     x = [-1, -1]
+   |     ref = T_instance_0
+   |   }
+T bar {
+  ^^^ vcg-field-access-basic/test3.trlc:9: check error: potato
+Processed 3 models and 1 requirement file and found 2 warnings and 1 error

tests-system/vcg-field-access-basic/output.brief

@@ -0,0 +1,2 @@
+vcg-field-access-basic/test3.trlc:9:3: trlc check error: potato
+Processed 3 models and 1 requirement file and found 1 error

tests-system/vcg-field-access-basic/output.json

@@ -0,0 +1,3 @@
+T bar {
+  ^^^ vcg-field-access-basic/test3.trlc:9: check error: potato
+Processed 3 models and 1 requirement file and found 1 error

tests-system/vcg-field-access-basic/output.smtlib

@@ -0,0 +1,18 @@
+c, "potato"
+^ vcg-field-access-basic/test1.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
+| example record_type triggering error:
+|   T bad_potato {
+|     x = 0
+|     /* ref is null */
+|     /* c is null */
+|   }
+10 / len(ref.x) > 0, "potato"
+   ^ vcg-field-access-basic/test2.rsl:9: issue: divisor could be 0 [vcg-div-by-zero]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     x = [-1, -1]
+   |     ref = T_instance_0
+   |   }
+T bar {
+  ^^^ vcg-field-access-basic/test3.trlc:9: check error: potato
+Processed 3 models and 1 requirement file and found 2 warnings and 1 error

tests-system/vcg-field-access-basic/test1.rsl

@@ -0,0 +1,12 @@
+package Test1
+
+type T {
+  x          Integer
+  ref        optional T
+  c          optional Boolean
+}
+
+checks T {
+  ref != null implies ref.x < x, fatal "potato"
+  c, "potato"
+}

tests-system/vcg-field-access-basic/test2.rsl

@@ -0,0 +1,10 @@
+package Test2
+
+type T {
+  x   Integer [2 .. *]
+  ref T
+}
+
+checks T {
+  10 / len(ref.x) > 0, "potato"
+}

tests-system/vcg-field-access-basic/test3.rsl

@@ -0,0 +1,11 @@
+package Test3
+
+type T {
+  x     Integer
+  ref   T
+  extra Integer
+}
+
+checks T {
+  ref.x + extra > 0, fatal "potato"
+}

tests-system/vcg-field-access-basic/test3.trlc

@@ -0,0 +1,13 @@
+package Test3
+
+T foo {
+  x     = 5
+  ref   = foo
+  extra = 3
+}
+
+T bar {
+  x     = -10
+  ref   = bar
+  extra = 3
+}

tests-system/field-access-1/tracing → tests-system/vcg-field-access-basic/tracing

@@ -1,3 +1,6 @@
 LRM.File_Parsing_References
 LRM.Order_Of_Evaluation_Unordered
+LRM.Evaluation_Truly_Unordered
+LRM.Check_Evaluation_Order
+LRM.Check_Severity
 LRM.Dereference