Fix CI and allow record field access

.github/workflows/ci.yml

@@ -28,16 +28,13 @@ jobs:
     needs: lint
     strategy:
       matrix:
-        os: [ubuntu-24.04, windows-2022, macos-13, macos-14]
+        os: [ubuntu-24.04, windows-2022, macos-14]
         py-version: ["3.8", "3.9", "3.10", "3.11", "3.12", "3.13"]
         include:
           - os: ubuntu-24.04
             cvc5-plat: "linux"
           - os: windows-2022
             cvc5-plat: "windows"
-          - os: macos-13
-            brew: "/usr/local"
-            cvc5-plat: "osx13"
           - os: macos-14
             brew: "/opt/homebrew"
             cvc5-plat: "osx14"
@@ -65,7 +62,7 @@ jobs:
           echo "${{ matrix.brew }}/opt/make/libexec/gnubin" >> $GITHUB_PATH
       - name: Fetch CVC5
         run: |
-          util/fetch_cvc5.py 1.2.0 ${{ matrix.cvc5-plat }}
+          util/fetch_cvc5.py 1.3.1 ${{ matrix.cvc5-plat }}
           echo "$GITHUB_WORKSPACE" >> $GITHUB_PATH
       - name: Executing unit tests
         run: |

language-reference-manual/lrm.trlc

@@ -2,7 +2,7 @@ package LRM
 
 Versioning Version {
   major = 3
-  minor = 1
+  minor = 2
 }
 
 GFDL_License License {
@@ -216,17 +216,43 @@ section "Layout and file structure" {
   }
 
   Dynamic_Semantics File_Parsing_Order {
-    text = '''
-First, all `.rsl` files are parsed. Then, if no errors
-are raised, all `.trlc` files are parsed.
-'''
+    text = '''First, all `.rsl` files are parsed. Then, if no errors
+              are raised, all `.trlc` files are parsed.
+           '''
   }
 
   Dynamic_Semantics File_Parsing_References {
-    text = '''
-After all files are parsed, references are resolved and
-user-defined checks are applied.
-'''
+    text = '''After all files are parsed, references are resolved,
+              in unspecified order.'''
+  }
+
+  Dynamic_Semantics Order_Of_Evaluation_Unordered {
+    text = '''After references are resolved, used-defined checks are
+              resolved on record objects. The order of record objects
+              is unspecified.'''
+  }
+
+  Note Evaluation_Truly_Unordered {
+    text = '''Note that this means that any record accessed through a
+              field access does not necessarily pass all of its checks,
+              since they have not been evaluated yet. Only properties
+              that are checked before checks are evaluated can be assumed
+              to hold (e.g. array length).
+           '''
+  }
+
+  Note Evaluation_Truly_Unordered_Across_Packages {
+    text = '''Note that this unspecified order even extends to packages.
+              If you have package A and B, it is not valid to assume that
+              all objects from A will be evaluated before B, nor is it
+              valid to assume that all objects from B are evaluated before A.
+           '''
+  }
+
+  Note Parallel_Evaluation {
+    text = '''This also means that it's possible to check two or more
+              record objects in parallel.
+           '''
   }
 
   Recommendation Errors_In_TRLC_Files {
@@ -1065,7 +1091,8 @@ section "Names" {
     bullets = [
       '''A qualified name referring to either some object, a component
          (in a record) or field (in a tuple), or an enumeration type.''',
-      '''A tuple field or enumeration literal.''',
+      """A contained tuple's field, a referenced record's component,
+         or enumeration literal.""",
       '''An index into an array.''',
       '''A (builtin) function call.'''
     ]
@@ -1082,10 +1109,13 @@ section "Names" {
     text = '''If the prefix of a dot (`.`) access resolves to an
               enumeration type, then the identifier must be
               a valid literal of that type. If the prefix of
-              a dot (`.`) access resolves to a tuple, then
-              the identifier must be a valid field of the
-              type of that tuple. Any other prefix is an
-              error.
+              a dot (`.`) access resolves to component
+              containing a tuple, then the identifier must
+              be a valid field of the type of that tuple. If
+              the prefix of a dot (`.`) access resolves to a
+              component referencing another record, then the
+              identifier must be a valid component of that
+              record. Any other prefix is an error.
            '''
   }
 
@@ -1101,7 +1131,6 @@ section "Names" {
            '''
   }
 
-
   Static_Semantics Signature_Len {
     text = '''The builtin function `len` is of arity 1. Its parameter must
               be of type `String` or an array type. Its
@@ -1150,6 +1179,13 @@ section "Names" {
               a true rational type, or a floating point type.)*'''
   }
 
+  Dynamic_Semantics Dereference {
+    text = '''Evaluating the dot (`.`) operator to access a
+              field of a referenced record requires the
+              prefix to be not null. Dereferencing null is
+              undefined behaviour.'''
+  }
+
   Dynamic_Semantics Len_Semantics {
     text = '''The `len` function computes the length of the given string
               or array.'''
@@ -1223,6 +1259,9 @@ section "Names" {
 
         cb_link.item >= 50000, warning "cb item value is oddly low"
         // you can obtain a tuple's values
+
+        bar.asil == asil, warning "mismatch in ASIL levels"
+        // you can peek into a referenced record
       }
     '''
   }
@@ -1561,7 +1600,7 @@ section "Quantification" {
     text = '''During evaluation of the quantified expression, each element
               of the array is evaluated in sequence and its
               value is bound to the declared name. The
-              predicated is then evaluated with this
+              predicate is then evaluated with this
               binding.'''
   }
 

pylint3.cfg

@@ -2,31 +2,32 @@
 persistent=no
 disable=
  bad-indentation,
- missing-docstring,
+ consider-using-f-string,
  fixme,
+ inconsistent-return-statements,
+ len-as-condition,
  locally-disabled,
+ missing-docstring,
+ no-else-break,
+ no-else-continue,
+ no-else-raise,
+ no-else-return,
  similarities,
+ too-few-public-methods,
  too-many-ancestors,
+ too-many-arguments,
+ too-many-boolean-expressions,
+ too-many-branches,
  too-many-instance-attributes,
- too-few-public-methods,
+ too-many-lines,
+ too-many-locals,
+ too-many-nested-blocks,
+ too-many-positional-arguments,
  too-many-public-methods,
  too-many-return-statements,
- too-many-branches,
- too-many-arguments,
- too-many-locals,
  too-many-statements,
- too-many-boolean-expressions,
- too-many-nested-blocks,
- too-many-lines,
- len-as-condition,
- no-else-return,
- inconsistent-return-statements,
- wildcard-import,
  unused-wildcard-import,
- no-else-raise,
- no-else-break,
- no-else-continue,
- consider-using-f-string
+ wildcard-import
 
 [REPORTS]
 output-format=text

requirements.txt

@@ -1,2 +1,2 @@
-pyvcg==1.0.8
-cvc5>=1.2.0
+pyvcg==1.0.9
+cvc5>=1.3.1

tests-system/field-access-1/output

@@ -0,0 +1,33 @@
+goal, "potato"
+^^^^ field-access-1/test_1.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     value = 0
+   |     /* ref is null */
+   |     /* goal is null */
+   |   }
+goal, "potato"
+^^^^ field-access-1/test_2.rsl:13: issue: expression could be null [vcg-evaluation-of-null]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     value = 0
+   |     /* ref_a is null */
+   |     ref_b = T_instance_0
+   |     /* goal is null */
+   |   }
+10 / len(ref.arr) > 0, "potato"
+   ^ field-access-1/test_3.rsl:9: issue: divisor could be 0 [vcg-div-by-zero]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     arr = [-1, -1]
+   |     ref = T_instance_0
+   |   }
+(forall e in arr => e.value < value), fatal "potato"
+                      ^^^^^ field-access-1/test_4.rsl:9: warning: functional evaluation of field access not yet supported in VCG
+first.value < second.value, fatal "potato"
+      ^^^^^ field-access-1/test_5.rsl:13: warning: functional evaluation of field access not yet supported in VCG
+Q test_5_1 {
+  ^^^^^^^^ field-access-1/test_5.trlc:11: error: check goal (test_5.rsl:23) evaluates to null
+pair = (two, one)
+       ^ field-access-1/test_5.trlc:16: check error: potato
+Processed 5 models and 1 requirement file and found 5 warnings and 2 errors

tests-system/field-access-1/output.brief

@@ -0,0 +1,3 @@
+field-access-1/test_5.trlc:11:3: trlc error: check goal (test_5.rsl:23) evaluates to null
+field-access-1/test_5.trlc:16:10: trlc check error: potato
+Processed 5 models and 1 requirement file and found 2 errors

tests-system/field-access-1/output.json

@@ -0,0 +1,5 @@
+Q test_5_1 {
+  ^^^^^^^^ field-access-1/test_5.trlc:11: error: check goal (test_5.rsl:23) evaluates to null
+pair = (two, one)
+       ^ field-access-1/test_5.trlc:16: check error: potato
+Processed 5 models and 1 requirement file and found 2 errors

tests-system/field-access-1/output.smtlib

@@ -0,0 +1,33 @@
+goal, "potato"
+^^^^ field-access-1/test_1.rsl:11: issue: expression could be null [vcg-evaluation-of-null]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     value = 0
+   |     /* ref is null */
+   |     /* goal is null */
+   |   }
+goal, "potato"
+^^^^ field-access-1/test_2.rsl:13: issue: expression could be null [vcg-evaluation-of-null]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     value = 0
+   |     /* ref_a is null */
+   |     ref_b = T_instance_0
+   |     /* goal is null */
+   |   }
+10 / len(ref.arr) > 0, "potato"
+   ^ field-access-1/test_3.rsl:9: issue: divisor could be 0 [vcg-div-by-zero]
+   | example record_type triggering error:
+   |   T bad_potato {
+   |     arr = [-1, -1]
+   |     ref = T_instance_0
+   |   }
+(forall e in arr => e.value < value), fatal "potato"
+                      ^^^^^ field-access-1/test_4.rsl:9: warning: functional evaluation of field access not yet supported in VCG
+first.value < second.value, fatal "potato"
+      ^^^^^ field-access-1/test_5.rsl:13: warning: functional evaluation of field access not yet supported in VCG
+Q test_5_1 {
+  ^^^^^^^^ field-access-1/test_5.trlc:11: error: check goal (test_5.rsl:23) evaluates to null
+pair = (two, one)
+       ^ field-access-1/test_5.trlc:16: check error: potato
+Processed 5 models and 1 requirement file and found 5 warnings and 2 errors

tests-system/field-access-1/test_1.rsl

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

tests-system/field-access-1/test_2.rsl

@@ -0,0 +1,14 @@
+package Test_2
+
+type T {
+  value            Integer
+  ref_a   optional T
+  ref_b   optional T
+
+  goal optional Boolean
+}
+
+checks T {
+  ref_a != ref_b, fatal "potato"
+  goal, "potato"
+}

tests-system/field-access-1/test_3.rsl

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

tests-system/field-access-1/test_4.rsl

@@ -0,0 +1,11 @@
+package Test_4
+
+type T {
+  value Integer
+  arr T [0 .. *]
+}
+
+checks T {
+  (forall e in arr => e.value < value), fatal "potato"
+  0 / (len(arr) - 5) == 0, "potato"
+}

tests-system/field-access-1/test_5.rsl

@@ -0,0 +1,24 @@
+package Test_5
+
+type R {
+  value Integer
+}
+
+tuple T {
+  first  R
+  second R
+}
+
+checks T {
+  first.value < second.value, fatal "potato"
+}
+
+type Q {
+  pair T
+  goal optional Boolean
+}
+
+checks Q {
+  pair.first.value >= 0, fatal "kitten"
+  goal, "goal"
+}

tests-system/field-access-1/test_5.trlc

@@ -0,0 +1,17 @@
+package Test_5
+
+R one {
+  value = 1
+}
+
+R two {
+  value = 2
+}
+
+Q test_5_1 {
+  pair = (one, two)
+}
+
+Q test_5_2 {
+  pair = (two, one)
+}

tests-system/field-access-1/tracing

@@ -0,0 +1,3 @@
+LRM.File_Parsing_References
+LRM.Order_Of_Evaluation_Unordered
+LRM.Dereference

tests-system/lint-vcg-tuple/output.smtlib

@@ -5,7 +5,7 @@ c, "potato"
 |     x = 1
 |     y = 2
 |     p = -1
-|     q = -3
+|     q = -2
 |     /* c is null */
 |   }
 then x.version > 5