diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4abad470..87be9542 100644 --- a/.github/workflows/ci.yml +++ b/.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: | diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 7401d276..edda32d7 100644 --- a/language-reference-manual/lrm.trlc +++ b/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.''' } diff --git a/pylint3.cfg b/pylint3.cfg index bc88caec..aa11080a 100644 --- a/pylint3.cfg +++ b/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 diff --git a/requirements.txt b/requirements.txt index 8e75d070..d3d533aa 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ -pyvcg==1.0.8 -cvc5>=1.2.0 +pyvcg==1.0.9 +cvc5>=1.3.1 diff --git a/tests-system/field-access-1/output b/tests-system/field-access-1/output new file mode 100644 index 00000000..4b1c9bc1 --- /dev/null +++ b/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 diff --git a/tests-system/field-access-1/output.brief b/tests-system/field-access-1/output.brief new file mode 100644 index 00000000..d58e8373 --- /dev/null +++ b/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 diff --git a/tests-system/field-access-1/output.json b/tests-system/field-access-1/output.json new file mode 100644 index 00000000..32b70ccd --- /dev/null +++ b/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 diff --git a/tests-system/field-access-1/output.smtlib b/tests-system/field-access-1/output.smtlib new file mode 100644 index 00000000..4b1c9bc1 --- /dev/null +++ b/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 diff --git a/tests-system/field-access-1/test_1.rsl b/tests-system/field-access-1/test_1.rsl new file mode 100644 index 00000000..3fd9b359 --- /dev/null +++ b/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" +} diff --git a/tests-system/field-access-1/test_2.rsl b/tests-system/field-access-1/test_2.rsl new file mode 100644 index 00000000..182f1a56 --- /dev/null +++ b/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" +} diff --git a/tests-system/field-access-1/test_3.rsl b/tests-system/field-access-1/test_3.rsl new file mode 100644 index 00000000..b5a83df1 --- /dev/null +++ b/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" +} diff --git a/tests-system/field-access-1/test_4.rsl b/tests-system/field-access-1/test_4.rsl new file mode 100644 index 00000000..383f73fc --- /dev/null +++ b/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" +} diff --git a/tests-system/field-access-1/test_5.rsl b/tests-system/field-access-1/test_5.rsl new file mode 100644 index 00000000..973aeee6 --- /dev/null +++ b/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" +} diff --git a/tests-system/field-access-1/test_5.trlc b/tests-system/field-access-1/test_5.trlc new file mode 100644 index 00000000..7176fb00 --- /dev/null +++ b/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) +} diff --git a/tests-system/field-access-1/tracing b/tests-system/field-access-1/tracing new file mode 100644 index 00000000..f428e74b --- /dev/null +++ b/tests-system/field-access-1/tracing @@ -0,0 +1,3 @@ +LRM.File_Parsing_References +LRM.Order_Of_Evaluation_Unordered +LRM.Dereference diff --git a/tests-system/lint-vcg-tuple/output.smtlib b/tests-system/lint-vcg-tuple/output.smtlib index b6f169f4..537318b6 100644 --- a/tests-system/lint-vcg-tuple/output.smtlib +++ b/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 diff --git a/tests-system/record-reference-1/output b/tests-system/record-reference-1/output new file mode 100644 index 00000000..f996192b --- /dev/null +++ b/tests-system/record-reference-1/output @@ -0,0 +1,14 @@ +link.value == value, "potato" +^^^^ record-reference-1/test.rsl:9: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | value = 0 + | /* link is null */ + | } +T R1 { + ^^ record-reference-1/test.trlc:3: check error: potato +T R2 { + ^^ record-reference-1/test.trlc:8: check error: potato +link.value == value, "potato" +^^^^ record-reference-1/test.rsl:9: error: null dereference +Processed 1 model and 1 requirement file and found 1 warning and 3 errors diff --git a/tests-system/record-reference-1/output.brief b/tests-system/record-reference-1/output.brief new file mode 100644 index 00000000..2f295b0d --- /dev/null +++ b/tests-system/record-reference-1/output.brief @@ -0,0 +1,4 @@ +record-reference-1/test.trlc:3:3: trlc check error: potato +record-reference-1/test.trlc:8:3: trlc check error: potato +record-reference-1/test.rsl:9:3: trlc error: null dereference +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/record-reference-1/output.json b/tests-system/record-reference-1/output.json new file mode 100644 index 00000000..a1da037f --- /dev/null +++ b/tests-system/record-reference-1/output.json @@ -0,0 +1,7 @@ +T R1 { + ^^ record-reference-1/test.trlc:3: check error: potato +T R2 { + ^^ record-reference-1/test.trlc:8: check error: potato +link.value == value, "potato" +^^^^ record-reference-1/test.rsl:9: error: null dereference +Processed 1 model and 1 requirement file and found 3 errors diff --git a/tests-system/record-reference-1/output.smtlib b/tests-system/record-reference-1/output.smtlib new file mode 100644 index 00000000..f996192b --- /dev/null +++ b/tests-system/record-reference-1/output.smtlib @@ -0,0 +1,14 @@ +link.value == value, "potato" +^^^^ record-reference-1/test.rsl:9: issue: expression could be null [vcg-evaluation-of-null] + | example record_type triggering error: + | T bad_potato { + | value = 0 + | /* link is null */ + | } +T R1 { + ^^ record-reference-1/test.trlc:3: check error: potato +T R2 { + ^^ record-reference-1/test.trlc:8: check error: potato +link.value == value, "potato" +^^^^ record-reference-1/test.rsl:9: error: null dereference +Processed 1 model and 1 requirement file and found 1 warning and 3 errors diff --git a/tests-system/record-reference-1/test.rsl b/tests-system/record-reference-1/test.rsl new file mode 100644 index 00000000..b29baac8 --- /dev/null +++ b/tests-system/record-reference-1/test.rsl @@ -0,0 +1,10 @@ +package Test + +type T { + value Integer + link optional T +} + +checks T { + link.value == value, "potato" +} diff --git a/tests-system/record-reference-1/test.trlc b/tests-system/record-reference-1/test.trlc new file mode 100644 index 00000000..9454927b --- /dev/null +++ b/tests-system/record-reference-1/test.trlc @@ -0,0 +1,25 @@ +package Test + +T R1 { + value = 23 + link = R2 +} + +T R2 { + value = 11 + link = R1 +} + +T R3 { + value = 123 + link = R3 +} + +T R4 { + value = 23 + link = R1 +} + +T R5 { + value = 0 +} diff --git a/tests-system/xref-2/output b/tests-system/xref-2/output index ed4ffa59..9c66d005 100644 --- a/tests-system/xref-2/output +++ b/tests-system/xref-2/output @@ -1,3 +1,3 @@ -link != null implies link.status == bar.Status.NEW, "Must be linked to new" - ^^^^ xref-2/bar.rsl:16: error: expression 'link' has type MyType, which is not a tuple +bar.MyType NewXR { + ^^^^^ xref-2/instances.trlc:10: check error: Must be linked to new Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref-2/output.brief b/tests-system/xref-2/output.brief index 9d56a927..ae310075 100644 --- a/tests-system/xref-2/output.brief +++ b/tests-system/xref-2/output.brief @@ -1,2 +1,2 @@ -xref-2/bar.rsl:16:24: trlc error: expression 'link' has type MyType, which is not a tuple +xref-2/instances.trlc:10:17: trlc check error: Must be linked to new Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref-2/output.json b/tests-system/xref-2/output.json index ed4ffa59..9c66d005 100644 --- a/tests-system/xref-2/output.json +++ b/tests-system/xref-2/output.json @@ -1,3 +1,3 @@ -link != null implies link.status == bar.Status.NEW, "Must be linked to new" - ^^^^ xref-2/bar.rsl:16: error: expression 'link' has type MyType, which is not a tuple +bar.MyType NewXR { + ^^^^^ xref-2/instances.trlc:10: check error: Must be linked to new Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref-2/output.smtlib b/tests-system/xref-2/output.smtlib index ed4ffa59..9c66d005 100644 --- a/tests-system/xref-2/output.smtlib +++ b/tests-system/xref-2/output.smtlib @@ -1,3 +1,3 @@ -link != null implies link.status == bar.Status.NEW, "Must be linked to new" - ^^^^ xref-2/bar.rsl:16: error: expression 'link' has type MyType, which is not a tuple +bar.MyType NewXR { + ^^^^^ xref-2/instances.trlc:10: check error: Must be linked to new Processed 1 model and 1 requirement file and found 1 error diff --git a/trlc/ast.py b/trlc/ast.py index b1bfcbe0..d5129481 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -2,7 +2,7 @@ # # TRLC - Treat Requirements Like Code # Copyright (C) 2022-2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG) -# Copyright (C) 2024 Florian Schanda +# Copyright (C) 2024-2025 Florian Schanda # # This file is part of the TRLC Python Reference Implementation. # @@ -369,17 +369,29 @@ def get_real_location(self, composite_object): else: return fields[self.n_anchor.name].location - def perform(self, mh, composite_object): + def perform(self, mh, composite_object, gstab): # lobster-trace: LRM.Check_Messages # lobster-trace: LRM.Check_Severity assert isinstance(mh, Message_Handler) assert isinstance(composite_object, (Record_Object, Tuple_Aggregate)) + assert isinstance(gstab, Symbol_Table) if isinstance(composite_object, Record_Object): - result = self.n_expr.evaluate(mh, copy(composite_object.field)) + result = self.n_expr.evaluate(mh, + copy(composite_object.field), + gstab) else: - result = self.n_expr.evaluate(mh, copy(composite_object.value)) + result = self.n_expr.evaluate(mh, + copy(composite_object.value), + gstab) + if result.value is None: + loc = self.get_real_location(composite_object) + mh.error(loc, + "check %s (%s) evaluates to null" % + (self.n_expr.to_string(), + mh.cross_file_reference(self.location))) + assert isinstance(result.value, bool) if not result.value: @@ -462,7 +474,7 @@ def __init__(self, location, typ): assert typ is None or isinstance(typ, Type) self.typ = typ - def evaluate(self, mh, context): # pragma: no cover + def evaluate(self, mh, context, gstab): # pragma: no cover """Evaluate the expression in the given context The context can be None, in which case the expression is @@ -470,6 +482,10 @@ def evaluate(self, mh, context): # pragma: no cover dictionary that maps names (such as record fields or quantified variables) to expressions. + The global symbol table must be None (for static context + evaluations), otherwise it must contain the global symbol + table to resolve record references. + :param mh: the message handler to use :type mh: Message_Handler :param context: name mapping or None (for a static context) @@ -477,9 +493,11 @@ def evaluate(self, mh, context): # pragma: no cover :raise TRLC_Error: if the expression cannot be evaluated :return: result of the evaluation :rtype: Value + """ assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) assert False, "evaluate not implemented for %s" % \ self.__class__.__name__ @@ -564,10 +582,11 @@ def __init__(self, composite_object, composite_component): def to_string(self): return "null" - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Unspecified_Optional_Components assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, None, None) def to_python_object(self): @@ -621,9 +640,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return "null" - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, None, None) def to_python_object(self): @@ -668,9 +688,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return str(self.value) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, self.value, self.typ) def to_python_object(self): @@ -715,9 +736,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return str(self.value) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, self.value, self.typ) def to_python_object(self): @@ -767,9 +789,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return self.value - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, self.value, self.typ) def to_python_object(self): @@ -807,9 +830,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return str(self.value) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, self.value, self.typ) def to_python_object(self): @@ -854,9 +878,10 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return self.typ.name + "." + self.value.name - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, self.value, self.typ) def to_python_object(self): @@ -908,11 +933,12 @@ def append(self, value): def to_string(self): return "[" + ", ".join(x.to_string() for x in self.value) + "]" - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, - list(element.evaluate(mh, context) + list(element.evaluate(mh, context, gstab) for element in self.value), self.typ) @@ -999,11 +1025,12 @@ def to_string(self): rv = ")" return rv - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) return Value(self.location, - {name : element.evaluate(mh, context) + {name : element.evaluate(mh, context, gstab) for name, element in self.value.items()}, self.typ) @@ -1073,10 +1100,11 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return self.name - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) - return Value(self.location, self, self.typ) + assert gstab is None or isinstance(gstab, Symbol_Table) + return Value(self.location, copy(self.target.field), self.typ) def resolve_references(self, mh): # lobster-trace: LRM.References_To_Extensions @@ -1137,16 +1165,17 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return self.entity.name - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) if context is None: mh.error(self.location, "cannot be used in a static context") assert self.entity.name in context - return context[self.entity.name].evaluate(mh, context) + return context[self.entity.name].evaluate(mh, context, gstab) def can_be_null(self): # The only way we could generate null here (without raising @@ -1244,7 +1273,7 @@ def dump(self, indent=0): # pragma: no cover self.write_indent(indent + 1, f"Type: {self.typ.name}") self.n_operand.dump(indent + 1) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Signature_Len # lobster-trace: LRM.Signature_Type_Conversion @@ -1254,8 +1283,9 @@ def evaluate(self, mh, context): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) - v_operand = self.n_operand.evaluate(mh, context) + v_operand = self.n_operand.evaluate(mh, context, gstab) if v_operand.value is None: mh.error(v_operand.location, "input to unary expression %s (%s) must not be null" % @@ -1493,7 +1523,7 @@ def to_string(self): else: assert False - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Null_Equivalence # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Signature_String_End_Functions @@ -1504,8 +1534,9 @@ def evaluate(self, mh, context): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) - v_lhs = self.n_lhs.evaluate(mh, context) + v_lhs = self.n_lhs.evaluate(mh, context, gstab) if v_lhs.value is None and \ self.operator not in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ): @@ -1518,7 +1549,7 @@ def evaluate(self, mh, context): if self.operator == Binary_Operator.LOGICAL_AND: assert isinstance(v_lhs.value, bool) if v_lhs.value: - return self.n_rhs.evaluate(mh, context) + return self.n_rhs.evaluate(mh, context, gstab) else: return v_lhs @@ -1527,19 +1558,19 @@ def evaluate(self, mh, context): if v_lhs.value: return v_lhs else: - return self.n_rhs.evaluate(mh, context) + return self.n_rhs.evaluate(mh, context, gstab) elif self.operator == Binary_Operator.LOGICAL_IMPLIES: assert isinstance(v_lhs.value, bool) if v_lhs.value: - return self.n_rhs.evaluate(mh, context) + return self.n_rhs.evaluate(mh, context, gstab) else: return Value(location = self.location, value = True, typ = self.typ) # Otherwise, evaluate RHS and do the operation - v_rhs = self.n_rhs.evaluate(mh, context) + v_rhs = self.n_rhs.evaluate(mh, context, gstab) if v_rhs.value is None and \ self.operator not in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ): @@ -1712,14 +1743,14 @@ def can_be_null(self): class Field_Access_Expression(Expression): - """Tuple field access + """Tuple or Record field access For example in:: foo.bar ^1 ^2 - :attribute n_prefix: expression with tuple type (see 1) + :attribute n_prefix: expression with tuple or record type (see 1) :type: Expression :attribute n_field: a tuple field to dereference (see 2) @@ -1744,11 +1775,24 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return self.n_prefix.to_string() + "." + self.n_field.name - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) - - return self.n_prefix.evaluate(mh, context).value[self.n_field.name] + assert gstab is None or isinstance(gstab, Symbol_Table) + + v_prefix = self.n_prefix.evaluate(mh, + context, + gstab).value + if v_prefix is None: + # lobster-trace: LRM.Dereference + mh.error(self.n_prefix.location, + "null dereference") + + v_field = v_prefix[self.n_field.name] + if isinstance(v_field, Implicit_Null): + return v_field.evaluate(mh, context, gstab) + else: + return v_field def can_be_null(self): return False @@ -1803,26 +1847,27 @@ def dump(self, indent=0): # pragma: no cover self.n_lower.dump(indent + 1) self.n_upper.dump(indent + 1) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) - v_lhs = self.n_lhs.evaluate(mh, context) + v_lhs = self.n_lhs.evaluate(mh, context, gstab) if v_lhs.value is None: mh.error(v_lhs.location, "lhs of range check %s (%s) see must not be null" % (self.to_string(), mh.cross_file_reference(self.location))) - v_lower = self.n_lower.evaluate(mh, context) + v_lower = self.n_lower.evaluate(mh, context, gstab) if v_lower.value is None: mh.error(v_lower.location, "lower bound of range check %s (%s) must not be null" % (self.to_string(), mh.cross_file_reference(self.location))) - v_upper = self.n_upper.evaluate(mh, context) + v_upper = self.n_upper.evaluate(mh, context, gstab) if v_upper.value is None: mh.error(v_upper.location, "upper bound of range check %s (%s) must not be null" % @@ -1872,12 +1917,13 @@ def dump(self, indent=0): # pragma: no cover for n_choice in self.choices: n_choice.dump(indent + 1) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.OneOf_Semantics assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) - v_choices = [n_choice.evaluate(mh, context).value + v_choices = [n_choice.evaluate(mh, context, gstab).value for n_choice in self.choices] return Value(location = self.location, @@ -2006,24 +2052,25 @@ def to_string(self): rv += ")" return rv - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Conditional_Expression_Else # lobster-trace: LRM.Conditional_Expression_Evaluation # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) for action in self.actions: - v_cond = action.n_cond.evaluate(mh, context) + v_cond = action.n_cond.evaluate(mh, context, gstab) if v_cond.value is None: mh.error(v_cond.location, "condition of %s (%s) must not be null" % (action.to_string(), mh.cross_file_reference(self.location))) if v_cond.value: - return action.n_expr.evaluate(mh, context) + return action.n_expr.evaluate(mh, context, gstab) - return self.else_expr.evaluate(mh, context) + return self.else_expr.evaluate(mh, context, gstab) def can_be_null(self): if self.else_expr and self.else_expr.can_be_null(): @@ -2096,12 +2143,13 @@ def to_string(self): self.n_source.to_string(), self.n_expr.to_string()) - def evaluate(self, mh, context): + def evaluate(self, mh, context, gstab): # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Universal_Quantification_Semantics # lobster-trace: LRM.Existential_Quantification_Semantics assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) + assert gstab is None or isinstance(gstab, Symbol_Table) if context is None: new_ctx = {} @@ -2127,7 +2175,7 @@ def evaluate(self, mh, context): loc = self.location for binding in array_values.value: new_ctx[self.n_var.name] = binding - result = self.n_expr.evaluate(mh, new_ctx) + result = self.n_expr.evaluate(mh, new_ctx, gstab) assert isinstance(result.value, bool) if self.universal and not result.value: rv = False @@ -2212,9 +2260,10 @@ class Type(Entity, metaclass=ABCMeta): """Abstract base class for all types. """ - def perform_type_checks(self, mh, value): + def perform_type_checks(self, mh, value, gstab): assert isinstance(mh, Message_Handler) assert isinstance(value, Expression) + assert isinstance(gstab, Symbol_Table) return True def get_example_value(self): @@ -2373,10 +2422,12 @@ def dump(self, indent=0): # pragma: no cover self.write_indent(indent + 1, f"Upper bound: {self.upper_bound}") self.write_indent(indent + 1, f"Element type: {self.element_type.name}") - def perform_type_checks(self, mh, value): + def perform_type_checks(self, mh, value, gstab): assert isinstance(mh, Message_Handler) + assert isinstance(gstab, Symbol_Table) + if isinstance(value, Array_Aggregate): - return all(self.element_type.perform_type_checks(mh, v) + return all(self.element_type.perform_type_checks(mh, v, gstab) for v in value.value) else: assert isinstance(value, Implicit_Null) @@ -2794,13 +2845,15 @@ def dump(self, indent=0): # pragma: no cover else: self.write_indent(indent + 1, "Checks: None") - def perform_type_checks(self, mh, value): + def perform_type_checks(self, mh, value, gstab): # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(mh, Message_Handler) + assert isinstance(gstab, Symbol_Table) + if isinstance(value, Tuple_Aggregate): ok = True for check in self.iter_checks(): - if not check.perform(mh, value): + if not check.perform(mh, value, gstab): ok = False return ok else: @@ -3028,24 +3081,28 @@ def resolve_references(self, mh): for val in self.field.values(): val.resolve_references(mh) - def perform_checks(self, mh): + def perform_checks(self, mh, gstab): # lobster-trace: LRM.Check_Evaluation_Order # lobster-trace: LRM.Evaluation_Of_Checks assert isinstance(mh, Message_Handler) + assert isinstance(gstab, Symbol_Table) ok = True # First evaluate all tuple checks for n_comp in self.n_typ.all_components(): if not n_comp.n_typ.perform_type_checks(mh, - self.field[n_comp.name]): + self.field[n_comp.name], + gstab): ok = False + # TODO: Is there a bug here (a check relies on a tuple check)? + # Then evaluate all record checks for check in self.n_typ.iter_checks(): # Prints messages, if applicable. Raises exception on # fatal checks, which causes this to abort. - if not check.perform(mh, self): + if not check.perform(mh, self, gstab): ok = False return ok diff --git a/trlc/parser.py b/trlc/parser.py index cf74ddd1..babd213e 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -2,6 +2,7 @@ # # TRLC - Treat Requirements Like Code # Copyright (C) 2022-2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG) +# Copyright (C) 2025 Florian Schanda # # This file is part of the TRLC Python Reference Implementation. # @@ -1000,7 +1001,7 @@ def parse_factor(self, scope): self.match("OPERATOR") t_op = self.ct n_rhs = self.parse_primary(scope) - rhs_value = n_rhs.evaluate(self.mh, None) + rhs_value = n_rhs.evaluate(self.mh, None, None) a_binary = ast.Binary_Operator.POWER t_op.ast_link = a_binary n_lhs = ast.Binary_Expression( @@ -1252,7 +1253,7 @@ def parse_builtin(self, scope, n_name, t_name): try: # lobster-trace: LRM.Static_Regular_Expression # scope is None on purpose to enforce static context - value = parameters[1].evaluate(self.mh, None) + value = parameters[1].evaluate(self.mh, None, None) assert isinstance(value.typ, ast.Builtin_String) re.compile(value.value) except re.error as err: @@ -1382,11 +1383,12 @@ def parse_name(self, scope): n_name.set_ast_link(self.ct) while self.peek("DOT") or self.peek("S_BRA"): if self.peek("DOT"): - if not isinstance(n_name.typ, ast.Tuple_Type): + if not isinstance(n_name.typ, (ast.Tuple_Type, + ast.Record_Type)): # lobster-trace: LRM.Valid_Index_Prefixes self.mh.error(n_name.location, "expression '%s' has type %s, " - "which is not a tuple" % + "which is not a tuple or record" % (n_name.to_string(), n_name.typ.name)) self.match("DOT") diff --git a/trlc/trlc.py b/trlc/trlc.py index 8e2412b6..85fc269d 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -456,6 +456,7 @@ def parse_trlc_files(self): return ok def resolve_record_references(self): + # lobster-trace: LRM.File_Parsing_References # lobster-trace: LRM.Markup_String_Late_Reference_Resolution # lobster-trace: LRM.Late_Reference_Checking ok = True @@ -469,11 +470,12 @@ def resolve_record_references(self): return ok def perform_checks(self): + # lobster-trace: LRM.Order_Of_Evaluation_Unordered ok = True for package in self.stab.values(ast.Package): for obj in package.symbols.values(ast.Record_Object): try: - if not obj.perform_checks(self.mh): + if not obj.perform_checks(self.mh, self.stab): ok = False except TRLC_Error: ok = False @@ -487,6 +489,7 @@ def process(self): :rtype: Symbol_Table """ # lobster-trace: LRM.File_Parsing_Order + # lobster-trace: LRM.File_Parsing_References # Notify callback self.callback_parse_begin() diff --git a/trlc/vcg.py b/trlc/vcg.py index 19899810..ba3882bd 100644 --- a/trlc/vcg.py +++ b/trlc/vcg.py @@ -2,7 +2,7 @@ # # TRLC - Treat Requirements Like Code # Copyright (C) 2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG) -# Copyright (C) 2023 Florian Schanda +# Copyright (C) 2023-2025 Florian Schanda # # This file is part of the TRLC Python Reference Implementation. # @@ -103,10 +103,12 @@ def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None): self.constants = {} self.enumerations = {} self.tuples = {} + self.records = {} self.arrays = {} self.bound_vars = {} self.qe_vars = {} self.tuple_base = {} + self.uf_records = {} self.uf_matches = None # Pointer to the UF we use for matches. We only generate it @@ -722,10 +724,12 @@ def tr_type(self, n_type): return self.arrays[n_type] elif isinstance(n_type, Record_Type): - # Record references are modelled as a free integer, since - # we can't really _do_ anything with them. We just need a - # variable with infinite range so we can generate - # arbitrary fictional record names + # Record references are modelled as a free integer. If we + # access their field then we use an uninterpreted + # function. Some of these have special meaning: + # 0 - the null reference + # 1 - the self reference + # anything else - uninterpreted return smt.BUILTIN_INTEGER else: # pragma: no cover @@ -736,7 +740,7 @@ def tr_check(self, n_check): # If the check belongs to a different type then we are looking # at a type extension. In this case we do not create checks - # again, because if a check would failt it would already have + # again, because if a check would fail it would already have # failed. if n_check.n_type is not self.n_ctyp: old_emit, self.emit_checks = self.emit_checks, False @@ -987,7 +991,7 @@ def tr_binary_expression(self, n_expr): lhs_value) elif n_expr.operator == Binary_Operator.STRING_REGEX: - rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None).value + rhs_evaluation = n_expr.n_rhs.evaluate(self.mh, None, None).value assert isinstance(rhs_evaluation, str) sym_value = smt.Function_Application( @@ -1005,7 +1009,7 @@ def tr_binary_expression(self, n_expr): elif n_expr.operator == Binary_Operator.POWER: # LRM says that the exponent is always static and an # integer - static_value = n_expr.n_rhs.evaluate(self.mh, None).value + static_value = n_expr.n_rhs.evaluate(self.mh, None, None).value assert isinstance(static_value, int) and static_value >= 0 if static_value == 0: @@ -1464,15 +1468,73 @@ def tr_quantified_expression(self, n_expr): def tr_field_access_expression(self, n_expr): assert isinstance(n_expr, Field_Access_Expression) + if self.functional: # pragma: no cover + self.flag_unsupported(n_expr, + "functional evaluation of field access") + prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix) + prefix_typ = n_expr.n_prefix.typ self.attach_validity_check(prefix_valid, n_expr.n_prefix) - field_value = smt.Record_Access(prefix_value, - n_expr.n_field.name + ".value") - if n_expr.n_field.optional: - field_valid = smt.Record_Access(prefix_value, - n_expr.n_field.name + ".valid") + if isinstance(prefix_typ, Tuple_Type): + field_value = smt.Record_Access(prefix_value, + n_expr.n_field.name + ".value") + if n_expr.n_field.optional: + field_valid = smt.Record_Access(prefix_value, + n_expr.n_field.name + ".valid") + else: + field_valid = smt.Boolean_Literal(True) + + elif isinstance(prefix_typ, Record_Type): + # We need a sort for the record instance + a UF to convert + # the int values into instances of this sort. + if prefix_typ in self.records: + record_sort = self.records[prefix_typ] + to_record_uf = self.uf_records[prefix_typ] + else: + record_sort = smt.Record(prefix_typ.n_package.name + + "." + prefix_typ.name) + for n_component in prefix_typ.all_components(): + record_sort.add_component(n_component.name + ".value", + self.tr_type(n_component.n_typ)) + if n_component.optional: + record_sort.add_component(n_component.name + ".valid", + smt.BUILTIN_BOOLEAN) + self.records[prefix_typ] = record_sort + self.preamble.add_statement( + smt.Record_Declaration( + record_sort, + "record %s from %s" % ( + prefix_typ.name, + prefix_typ.location.to_string()))) + + to_record_uf = smt.Function( + "access.%s.%s" % + (prefix_typ.n_package.name, prefix_typ.name), + record_sort, + smt.Bound_Variable(smt.BUILTIN_INTEGER, "ref")) + self.preamble.add_statement( + smt.Function_Declaration(to_record_uf)) + + self.uf_records[prefix_typ] = to_record_uf + + # We can now apply the magic int to the UF to get a record + # value + dereference = smt.Function_Application(to_record_uf, prefix_value) + + # We can now perform the access on the record value + field_value = smt.Record_Access(dereference, + n_expr.n_field.name + ".value") + if n_expr.n_field.optional: + field_valid = smt.Record_Access(dereference, + n_expr.n_field.name + ".valid") + else: + field_valid = smt.Boolean_Literal(True) + else: - field_valid = smt.Boolean_Literal(True) + self.mh.ice_loc(n_expr.n_prefix.location, + "unexpected type %s as prefix of field access" % + n_expr.n_prefix.typ.__class__.__name__) + # pylint: disable=possibly-used-before-assignment return field_value, field_valid diff --git a/util/fetch_cvc5.py b/util/fetch_cvc5.py index 1f4973e8..49e21b9b 100755 --- a/util/fetch_cvc5.py +++ b/util/fetch_cvc5.py @@ -41,8 +41,6 @@ if options.platform == "linux": CVC5_PLATFORM = "Linux-x86_64-static" -elif options.platform == "osx13": - CVC5_PLATFORM = "macOS-x86_64-static" elif options.platform == "osx14": CVC5_PLATFORM = "macOS-arm64-static" elif options.platform == "windows":