diff --git a/documentation/TUTORIAL-ADVANCED-TYPES.md b/documentation/TUTORIAL-ADVANCED-TYPES.md index f414a3fd..03c5c50b 100644 --- a/documentation/TUTORIAL-ADVANCED-TYPES.md +++ b/documentation/TUTORIAL-ADVANCED-TYPES.md @@ -52,3 +52,40 @@ type ACME_Requirement extends Supplier_Requirement { This makes sure that any and all supplier requirements are completely uniform, and nobody adds new fields that may be confusing or unexpected to the suppliers. + +### Type Checks + +A field within a type can also reference another type. +You can access fields of a referenced type using the `.` notation: + +``` +type BaseType { + name String +} + +type MyType { + name String + link BaseType +} + +checks MyType { + link.name != name, "cannot link the type with the same name." +} +``` + +Self-referencing (recursive) type definitions are also supported. +To prevent infinite recursion, any recursive field must be declared as `optional`: + +``` +type MyType { + name String + link optional MyType +} + +checks MyType { + link != null implies link.name != name, + "link status must be the same as status" +} +``` +Excessive recursion may lead to performance degradation, +so complex recursive designs are not recommended. diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index 7401d276..74ff4a6f 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1084,8 +1084,13 @@ section "Names" { 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. + type of that tuple. If the prefix of a dot (`.`) + access resolves to a record object, then the identifier + must be the name of a component declared inside + that record. Optional components are represented as a + pair `(valid, value)`, and may be accessed using + `record.field.valid` and `record.field.value`. Nested + field access is allowed. Any other prefix is an error. ''' } @@ -1101,7 +1106,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 @@ -1197,14 +1201,16 @@ section "Names" { separator @ version optional Integer } + type Name_Base { + description string + } type Name_Examples { - foo Boolean - bar Name_Examples - asil ASIL - potato Integer [0 .. *] - wibble Decimal - field String - cb_link Codebeamer_Item + foo Boolean + bar Name_Base + asil ASIL + potato Integer [0 .. *] + field String + cb_link Codebeamer_Item } ''' rsl = ''' @@ -1223,6 +1229,9 @@ section "Names" { cb_link.item >= 50000, warning "cb item value is oddly low" // you can obtain a tuple's values + + bar.description, "foo" + // you can obtain a record's component } ''' } diff --git a/requirements.txt b/requirements.txt index 8e75d070..77dff34a 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ -pyvcg==1.0.8 +pyvcg==1.0.9 cvc5>=1.2.0 diff --git a/setup.py b/setup.py index b6b0f282..b263baa2 100644 --- a/setup.py +++ b/setup.py @@ -42,7 +42,7 @@ project_urls=project_urls, license="GNU General Public License v3", packages=setuptools.find_packages(), - install_requires="PyVCG[api]==1.0.8", + install_requires="PyVCG[api]==1.0.9", python_requires=">=3.8, <3.14", classifiers=[ "Development Status :: 5 - Production/Stable", diff --git a/tests-system/Makefile b/tests-system/Makefile index ef9e06db..9171710b 100644 --- a/tests-system/Makefile +++ b/tests-system/Makefile @@ -1,4 +1,4 @@ -RAW_TARGETS=$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth 1 -type d))) +RAW_TARGETS=$(if $(TARGET),$(TARGET),$(filter-out bulk, $(subst ./,,$(shell find . -mindepth 1 -maxdepth 1 -type d)))) TARGETS=\ $(addsuffix /output, $(RAW_TARGETS)) \ diff --git a/tests-system/checks-5/output b/tests-system/checks-5/output index ccfa4f52..fda2b640 100644 --- a/tests-system/checks-5/output +++ b/tests-system/checks-5/output @@ -1,6 +1,3 @@ -Requirement Potato { - ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect - | You must either link this requirement to other requirements - | using the derived_from attribute, or you need to set - | top_level to true. +type Requirement { + ^^^^^^^^^^^ checks-5/foo.rsl:3: error: Complex recursive is not supported. Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/checks-5/output.smtlib b/tests-system/checks-5/output.smtlib index ccfa4f52..fda2b640 100644 --- a/tests-system/checks-5/output.smtlib +++ b/tests-system/checks-5/output.smtlib @@ -1,6 +1,3 @@ -Requirement Potato { - ^^^^^^ checks-5/foo.trlc:3: check error: linkage incorrect - | You must either link this requirement to other requirements - | using the derived_from attribute, or you need to set - | top_level to true. +type Requirement { + ^^^^^^^^^^^ checks-5/foo.rsl:3: error: Complex recursive is not supported. Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/lint-record-refs/output b/tests-system/lint-record-refs/output index 71bc2a18..c7ec3370 100644 --- a/tests-system/lint-record-refs/output +++ b/tests-system/lint-record-refs/output @@ -10,32 +10,32 @@ a != b implies x, "potato" ^ lint-record-refs/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = T_instance_1 - | b = T_instance_0 + | a = None + | b = None | /* x is null */ | } a == b implies x, "potato" ^ lint-record-refs/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = T_instance_0 - | b = T_instance_0 + | a = None + | b = None | /* x is null */ | } a != b implies x, "potato" ^ lint-record-refs/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = Other.T_instance_1 - | b = Other.T_instance_0 + | a = ("") + | b = ("A") | /* x is null */ | } a == b implies x, "potato" ^ lint-record-refs/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = Other.T_instance_0 - | b = Other.T_instance_0 + | a = ("") + | b = ("") | /* x is null */ | } Processed 4 models and 0 requirement files and found 5 warnings diff --git a/tests-system/lint-record-refs/output.smtlib b/tests-system/lint-record-refs/output.smtlib index 71bc2a18..c7ec3370 100644 --- a/tests-system/lint-record-refs/output.smtlib +++ b/tests-system/lint-record-refs/output.smtlib @@ -10,32 +10,32 @@ a != b implies x, "potato" ^ lint-record-refs/test2.rsl:10: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = T_instance_1 - | b = T_instance_0 + | a = None + | b = None | /* x is null */ | } a == b implies x, "potato" ^ lint-record-refs/test2.rsl:11: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = T_instance_0 - | b = T_instance_0 + | a = None + | b = None | /* x is null */ | } a != b implies x, "potato" ^ lint-record-refs/test3.rsl:11: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = Other.T_instance_1 - | b = Other.T_instance_0 + | a = ("") + | b = ("A") | /* x is null */ | } a == b implies x, "potato" ^ lint-record-refs/test3.rsl:12: issue: expression could be null [vcg-evaluation-of-null] | example record_type triggering error: | T bad_potato { - | a = Other.T_instance_0 - | b = Other.T_instance_0 + | a = ("") + | b = ("") | /* x is null */ | } Processed 4 models and 0 requirement files and found 5 warnings diff --git a/tests-system/tuples-4/output b/tests-system/tuples-4/output index c0917998..35dcb09a 100644 --- a/tests-system/tuples-4/output +++ b/tests-system/tuples-4/output @@ -2,7 +2,7 @@ f2 >= 0, warning "potato2", f2 ^^ tuples-4/foo.rsl:12: issue: expression could be null [vcg-evaluation-of-null] | example tuple_type triggering error: | T bad_potato { - | f1 = R1_instance_0 + | f1 = None | /* f2 is null */ | } t = potato diff --git a/tests-system/tuples-4/output.smtlib b/tests-system/tuples-4/output.smtlib index c0917998..35dcb09a 100644 --- a/tests-system/tuples-4/output.smtlib +++ b/tests-system/tuples-4/output.smtlib @@ -2,7 +2,7 @@ f2 >= 0, warning "potato2", f2 ^^ tuples-4/foo.rsl:12: issue: expression could be null [vcg-evaluation-of-null] | example tuple_type triggering error: | T bad_potato { - | f1 = R1_instance_0 + | f1 = None | /* f2 is null */ | } t = potato diff --git a/tests-system/tuples-use-type/bar.rsl b/tests-system/tuples-use-type/bar.rsl new file mode 100644 index 00000000..3e4caf5e --- /dev/null +++ b/tests-system/tuples-use-type/bar.rsl @@ -0,0 +1,29 @@ +package bar + +enum Status { + NEW + OLD + DEPRECATED +} + +type BaseType { + name String + status Status +} + +tuple LinkMy2Base { + link_type BaseType + separator @ + version Integer +} + +type MyType { + name String + status Status + derived_from optional LinkMy2Base[0 .. *] +} + +checks MyType { + derived_from != null implies (forall elem in derived_from => elem.link_type.status == status), + error "link status must be the same as status" +} diff --git a/tests-system/tuples-use-type/instances.trlc b/tests-system/tuples-use-type/instances.trlc new file mode 100644 index 00000000..5c524ccc --- /dev/null +++ b/tests-system/tuples-use-type/instances.trlc @@ -0,0 +1,14 @@ +package instances + +import bar + +bar.BaseType DeprecatedR { + name = "base" // does start with Q + status = bar.Status.NEW +} + +bar.MyType NewXR { + name = "new" + status = bar.Status.NEW + derived_from = [ DeprecatedR@1 ] +} diff --git a/tests-system/tuples-use-type/output b/tests-system/tuples-use-type/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/tuples-use-type/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/tuples-use-type/output.brief b/tests-system/tuples-use-type/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/tuples-use-type/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/tuples-use-type/output.json b/tests-system/tuples-use-type/output.json new file mode 100644 index 00000000..54ddd207 --- /dev/null +++ b/tests-system/tuples-use-type/output.json @@ -0,0 +1,17 @@ +{ + "DeprecatedR": { + "name": "base", + "status": "NEW" + }, + "NewXR": { + "derived_from": [ + { + "link_type": "instances.DeprecatedR", + "version": 1 + } + ], + "name": "new", + "status": "NEW" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/tuples-use-type/output.smtlib b/tests-system/tuples-use-type/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/tuples-use-type/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-2/TODO b/tests-system/xref-2/TODO deleted file mode 100644 index e9bea3e3..00000000 --- a/tests-system/xref-2/TODO +++ /dev/null @@ -1 +0,0 @@ -better message on attempting to derefence links? diff --git a/tests-system/xref-2/bar.rsl b/tests-system/xref-2/bar.rsl deleted file mode 100644 index 55714439..00000000 --- a/tests-system/xref-2/bar.rsl +++ /dev/null @@ -1,17 +0,0 @@ -package bar - -enum Status { - NEW - OLD - DEPRECATED -} - -type MyType { - name String - status optional Status - link optional MyType -} - -checks MyType { - link != null implies link.status == bar.Status.NEW, "Must be linked to new" -} diff --git a/tests-system/xref-2/instances.trlc b/tests-system/xref-2/instances.trlc deleted file mode 100644 index 0fcceef1..00000000 --- a/tests-system/xref-2/instances.trlc +++ /dev/null @@ -1,15 +0,0 @@ - package instances - import bar - - bar.MyType DeprecatedR { - name = "dep" // does start with Q - // status = bar.Status.DEPRECATED - - } - - bar.MyType NewXR { - name = "new" // does start with Q -// status = bar.Status.NEW - - link = DeprecatedR - } diff --git a/tests-system/xref-2/output b/tests-system/xref-2/output deleted file mode 100644 index ed4ffa59..00000000 --- a/tests-system/xref-2/output +++ /dev/null @@ -1,3 +0,0 @@ -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 -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 deleted file mode 100644 index 9d56a927..00000000 --- a/tests-system/xref-2/output.brief +++ /dev/null @@ -1,2 +0,0 @@ -xref-2/bar.rsl:16:24: trlc error: expression 'link' has type MyType, which is not a tuple -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 deleted file mode 100644 index ed4ffa59..00000000 --- a/tests-system/xref-2/output.json +++ /dev/null @@ -1,3 +0,0 @@ -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 -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 deleted file mode 100644 index ed4ffa59..00000000 --- a/tests-system/xref-2/output.smtlib +++ /dev/null @@ -1,3 +0,0 @@ -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 -Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref-expressions/f1.trlc b/tests-system/xref-expressions/f1.trlc index 1aa766db..f6f9f63d 100644 --- a/tests-system/xref-expressions/f1.trlc +++ b/tests-system/xref-expressions/f1.trlc @@ -7,4 +7,4 @@ A.L L1 { A.L Localref { l = L1 -} \ No newline at end of file +} diff --git a/tests-system/xref-no-recursion/bar.rsl b/tests-system/xref-no-recursion/bar.rsl new file mode 100644 index 00000000..28443c60 --- /dev/null +++ b/tests-system/xref-no-recursion/bar.rsl @@ -0,0 +1,22 @@ +package bar + +enum Status { + NEW + OLD + DEPRECATED +} + +type BaseType { + name String + status Status +} + +type MyType { + name String + status Status + link optional BaseType +} + +checks MyType { + link != null implies link.status == status, "link status must be the same as status" +} diff --git a/tests-system/xref-no-recursion/instances.trlc b/tests-system/xref-no-recursion/instances.trlc new file mode 100644 index 00000000..f53cf8b9 --- /dev/null +++ b/tests-system/xref-no-recursion/instances.trlc @@ -0,0 +1,14 @@ +package instances +import bar + +bar.BaseType DeprecatedR { + name = "base" // does start with Q + status = bar.Status.NEW +} + +bar.MyType NewXR { + name = "new" + status = bar.Status.NEW + link = DeprecatedR +} + diff --git a/tests-system/xref-no-recursion/output b/tests-system/xref-no-recursion/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-no-recursion/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-no-recursion/output.brief b/tests-system/xref-no-recursion/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-no-recursion/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-no-recursion/output.json b/tests-system/xref-no-recursion/output.json new file mode 100644 index 00000000..8a8a4907 --- /dev/null +++ b/tests-system/xref-no-recursion/output.json @@ -0,0 +1,12 @@ +{ + "DeprecatedR": { + "name": "base", + "status": "NEW" + }, + "NewXR": { + "link": "instances.DeprecatedR", + "name": "new", + "status": "NEW" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-no-recursion/output.smtlib b/tests-system/xref-no-recursion/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-no-recursion/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref/bar.rsl b/tests-system/xref-recursion/bar.rsl similarity index 64% rename from tests-system/xref/bar.rsl rename to tests-system/xref-recursion/bar.rsl index 619c7f0b..9f93db0e 100644 --- a/tests-system/xref/bar.rsl +++ b/tests-system/xref-recursion/bar.rsl @@ -13,5 +13,5 @@ type MyType { } checks MyType { - link != null , "Must be linked" + link != null implies link.status == status, "link status must be the same as status" } diff --git a/tests-system/xref-recursion/instance.trlc b/tests-system/xref-recursion/instance.trlc new file mode 100644 index 00000000..31ee3e1c --- /dev/null +++ b/tests-system/xref-recursion/instance.trlc @@ -0,0 +1,12 @@ +package bar + +bar.MyType DeprecatedR { + name = "dep" + status = bar.Status.DEPRECATED +} + +bar.MyType NewXR { + name = "new" + status = bar.Status.DEPRECATED + link = bar.DeprecatedR +} diff --git a/tests-system/xref-recursion/output b/tests-system/xref-recursion/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-recursion/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-recursion/output.brief b/tests-system/xref-recursion/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-recursion/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-recursion/output.json b/tests-system/xref-recursion/output.json new file mode 100644 index 00000000..db07230c --- /dev/null +++ b/tests-system/xref-recursion/output.json @@ -0,0 +1,13 @@ +{ + "DeprecatedR": { + "link": null, + "name": "dep", + "status": "DEPRECATED" + }, + "NewXR": { + "link": "bar.DeprecatedR", + "name": "new", + "status": "DEPRECATED" + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref-recursion/output.smtlib b/tests-system/xref-recursion/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/xref-recursion/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/xref/instances.trlc b/tests-system/xref/instances.trlc deleted file mode 100644 index 04cf6008..00000000 --- a/tests-system/xref/instances.trlc +++ /dev/null @@ -1,15 +0,0 @@ - package bar - - bar.MyType DeprecatedR { - name = "dep" // does start with Q - // status = bar.Status.DEPRECATED - - } - - bar.MyType NewXR { - name = "new" // does start with Q -// status = bar.Status.NEW - - link = bar.DeprecatedR - } - \ No newline at end of file diff --git a/tests-system/xref/output b/tests-system/xref/output deleted file mode 100644 index d7ae0701..00000000 --- a/tests-system/xref/output +++ /dev/null @@ -1,3 +0,0 @@ -bar.MyType DeprecatedR { - ^^^^^^^^^^^ xref/instances.trlc:3: check error: Must be linked -Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref/output.brief b/tests-system/xref/output.brief deleted file mode 100644 index 7c056849..00000000 --- a/tests-system/xref/output.brief +++ /dev/null @@ -1,2 +0,0 @@ -xref/instances.trlc:3:16: trlc check error: Must be linked -Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref/output.json b/tests-system/xref/output.json deleted file mode 100644 index d7ae0701..00000000 --- a/tests-system/xref/output.json +++ /dev/null @@ -1,3 +0,0 @@ -bar.MyType DeprecatedR { - ^^^^^^^^^^^ xref/instances.trlc:3: check error: Must be linked -Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/xref/output.smtlib b/tests-system/xref/output.smtlib deleted file mode 100644 index d7ae0701..00000000 --- a/tests-system/xref/output.smtlib +++ /dev/null @@ -1,3 +0,0 @@ -bar.MyType DeprecatedR { - ^^^^^^^^^^^ xref/instances.trlc:3: check error: Must be linked -Processed 1 model and 1 requirement file and found 1 error diff --git a/trlc/ast.py b/trlc/ast.py index b1bfcbe0..0cec2d88 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -74,7 +74,7 @@ def __init__(self, location, value, typ): int, bool, list, # for arrays - dict, # for tuples + dict, # for tuples and records Fraction, Record_Reference, Enumeration_Literal_Spec)) @@ -369,17 +369,18 @@ 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, stab): # 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(stab, 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), stab) else: - result = self.n_expr.evaluate(mh, copy(composite_object.value)) + result = self.n_expr.evaluate(mh, copy(composite_object.value), stab) assert isinstance(result.value, bool) if not result.value: @@ -462,7 +463,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, stab): # pragma: no cover """Evaluate the expression in the given context The context can be None, in which case the expression is @@ -479,6 +480,7 @@ def evaluate(self, mh, context): # pragma: no cover :rtype: Value """ assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) assert False, "evaluate not implemented for %s" % \ self.__class__.__name__ @@ -564,9 +566,10 @@ def __init__(self, composite_object, composite_component): def to_string(self): return "null" - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab=None): # lobster-trace: LRM.Unspecified_Optional_Components assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, None, None) @@ -621,8 +624,9 @@ def dump(self, indent=0): # pragma: no cover def to_string(self): return "null" - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, None, None) @@ -668,8 +672,9 @@ 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, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, self.value, self.typ) @@ -715,8 +720,9 @@ 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, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, self.value, self.typ) @@ -767,8 +773,9 @@ 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, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, self.value, self.typ) @@ -807,8 +814,9 @@ 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, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, self.value, self.typ) @@ -854,8 +862,9 @@ 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, stab=None): assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, self.value, self.typ) @@ -908,11 +917,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, stab): assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, - list(element.evaluate(mh, context) + list(element.evaluate(mh, context, stab) for element in self.value), self.typ) @@ -999,11 +1009,12 @@ def to_string(self): rv = ")" return rv - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab): assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) return Value(self.location, - {name : element.evaluate(mh, context) + {name : element.evaluate(mh, context, stab) for name, element in self.value.items()}, self.typ) @@ -1073,10 +1084,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, stab): assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - return Value(self.location, self, self.typ) + return Value(self.location, self.target.field, self.typ) def resolve_references(self, mh): # lobster-trace: LRM.References_To_Extensions @@ -1137,8 +1149,9 @@ 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, stab): assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) if context is None: @@ -1146,7 +1159,7 @@ def evaluate(self, mh, context): "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, stab) def can_be_null(self): # The only way we could generate null here (without raising @@ -1244,7 +1257,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, stab): # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Signature_Len # lobster-trace: LRM.Signature_Type_Conversion @@ -1253,9 +1266,10 @@ def evaluate(self, mh, context): # lobster-trace: LRM.Decimal_Conversion_Semantics assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - v_operand = self.n_operand.evaluate(mh, context) + v_operand = self.n_operand.evaluate(mh, context, stab) if v_operand.value is None: mh.error(v_operand.location, "input to unary expression %s (%s) must not be null" % @@ -1493,7 +1507,7 @@ def to_string(self): else: assert False - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab=None): # lobster-trace: LRM.Null_Equivalence # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Signature_String_End_Functions @@ -1503,9 +1517,10 @@ def evaluate(self, mh, context): # lobster-trace: LRM.Matches_Semantics assert isinstance(mh, Message_Handler) + assert stab is None or isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - v_lhs = self.n_lhs.evaluate(mh, context) + v_lhs = self.n_lhs.evaluate(mh, context, stab) if v_lhs.value is None and \ self.operator not in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ): @@ -1518,7 +1533,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, stab) else: return v_lhs @@ -1527,19 +1542,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, stab) 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, stab) 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, stab) if v_rhs.value is None and \ self.operator not in (Binary_Operator.COMP_EQ, Binary_Operator.COMP_NEQ): @@ -1744,11 +1759,12 @@ 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, stab): assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - return self.n_prefix.evaluate(mh, context).value[self.n_field.name] + return self.n_prefix.evaluate(mh, context, stab).value[self.n_field.name] def can_be_null(self): return False @@ -1803,26 +1819,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, stab): # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - v_lhs = self.n_lhs.evaluate(mh, context) + v_lhs = self.n_lhs.evaluate(mh, context, stab) 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, stab) 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, stab) if v_upper.value is None: mh.error(v_upper.location, "upper bound of range check %s (%s) must not be null" % @@ -1872,12 +1889,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, stab): # lobster-trace: LRM.OneOf_Semantics assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) - v_choices = [n_choice.evaluate(mh, context).value + v_choices = [n_choice.evaluate(mh, context, stab).value for n_choice in self.choices] return Value(location = self.location, @@ -2006,24 +2024,25 @@ def to_string(self): rv += ")" return rv - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab): # lobster-trace: LRM.Conditional_Expression_Else # lobster-trace: LRM.Conditional_Expression_Evaluation # lobster-trace: LRM.Null_Is_Invalid assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) for action in self.actions: - v_cond = action.n_cond.evaluate(mh, context) + v_cond = action.n_cond.evaluate(mh, context, stab) 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, stab) - return self.else_expr.evaluate(mh, context) + return self.else_expr.evaluate(mh, context, stab) def can_be_null(self): if self.else_expr and self.else_expr.can_be_null(): @@ -2096,11 +2115,12 @@ def to_string(self): self.n_source.to_string(), self.n_expr.to_string()) - def evaluate(self, mh, context): + def evaluate(self, mh, context, stab): # lobster-trace: LRM.Null_Is_Invalid # lobster-trace: LRM.Universal_Quantification_Semantics # lobster-trace: LRM.Existential_Quantification_Semantics assert isinstance(mh, Message_Handler) + assert isinstance(stab, Symbol_Table) assert context is None or isinstance(context, dict) if context is None: @@ -2127,7 +2147,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, stab) assert isinstance(result.value, bool) if self.universal and not result.value: rv = False @@ -2212,9 +2232,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, stab): assert isinstance(mh, Message_Handler) assert isinstance(value, Expression) + assert isinstance(stab, Symbol_Table) return True def get_example_value(self): @@ -2373,10 +2394,10 @@ 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, stab): assert isinstance(mh, Message_Handler) 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, stab) for v in value.value) else: assert isinstance(value, Implicit_Null) @@ -2794,13 +2815,13 @@ 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, stab): # lobster-trace: LRM.Check_Evaluation_Order assert isinstance(mh, Message_Handler) 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, stab): ok = False return ok else: @@ -3028,24 +3049,26 @@ 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, stab): # lobster-trace: LRM.Check_Evaluation_Order # lobster-trace: LRM.Evaluation_Of_Checks assert isinstance(mh, Message_Handler) + assert isinstance(stab, 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], + stab): ok = False # 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, stab): ok = False return ok diff --git a/trlc/parser.py b/trlc/parser.py index cf74ddd1..9c141469 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1000,7 +1000,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, self.stab) a_binary = ast.Binary_Operator.POWER t_op.ast_link = a_binary n_lhs = ast.Binary_Expression( @@ -1252,7 +1252,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, self.stab) assert isinstance(value.typ, ast.Builtin_String) re.compile(value.value) except re.error as err: @@ -1382,11 +1382,11 @@ 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 neither a tuple nor a type" % (n_name.to_string(), n_name.typ.name)) self.match("DOT") diff --git a/trlc/trlc.py b/trlc/trlc.py index 8e2412b6..b0407073 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -76,7 +76,7 @@ def __init__(self, mh, lint_mode = True, parse_trlc = True, verify_mode = False, - debug_vcg = False, + debug_vcg = True, error_recovery = True, cvc5_binary = None): assert isinstance(mh, Message_Handler) @@ -473,7 +473,7 @@ def perform_checks(self): 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 diff --git a/trlc/vcg.py b/trlc/vcg.py index 19899810..d40babbe 100644 --- a/trlc/vcg.py +++ b/trlc/vcg.py @@ -104,6 +104,7 @@ def __init__(self, mh, n_ctyp, debug, use_api=True, cvc5_binary=None): self.enumerations = {} self.tuples = {} self.arrays = {} + self.records = {} self.bound_vars = {} self.qe_vars = {} self.tuple_base = {} @@ -353,7 +354,11 @@ def checks_on_composite_type(self, n_ctyp): encoding = "UTF-8") # Generate VCs - self.vcg.generate() + try: + self.vcg.generate() + except smt.Recursion: # pragma: no cover + self.mh.error(self.n_ctyp.location, + "Complex recursive is not supported.") # Solve VCs and provide feedback nok_feasibility_checks = [] @@ -496,16 +501,17 @@ def value_to_trlc(self, n_typ, value): return '"%s"' % value elif isinstance(n_typ, Record_Type): - if value < 0: - instance_id = value * -2 - 1 - else: - instance_id = value * 2 - if n_typ.n_package is self.n_ctyp.n_package: - return "%s_instance_%i" % (n_typ.name, instance_id) - else: - return "%s.%s_instance_%i" % (n_typ.n_package.name, - n_typ.name, - instance_id) + if value and isinstance(value, dict): + parts = [] + for n_item in n_typ.all_components(): + if n_item.optional and not value[n_item.name + ".valid"]: + continue + if sub_val := self.value_to_trlc(n_item.n_typ, + value[n_item.name + ".value"]): + parts.append(sub_val) + if parts: + return "(%s)" % ", ".join(parts) + return None elif isinstance(n_typ, Tuple_Type): parts = [] @@ -697,13 +703,15 @@ def tr_type(self, n_type): if n_type not in self.tuples: s_sort = smt.Record(n_type.n_package.name + "." + n_type.name) + self.tuples[n_type] = s_sort + for n_component in n_type.all_components(): s_sort.add_component(n_component.name + ".value", self.tr_type(n_component.n_typ)) if n_component.optional: s_sort.add_component(n_component.name + ".valid", smt.BUILTIN_BOOLEAN) - self.tuples[n_type] = s_sort + self.start.add_statement( smt.Record_Declaration( s_sort, @@ -722,11 +730,26 @@ 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 - return smt.BUILTIN_INTEGER + if n_type not in self.records: + s_sort = smt.Record(n_type.n_package.name + + "." + n_type.name) + self.records[n_type] = s_sort + + for n_component in n_type.all_components(): + s_sort.add_component(n_component.name + ".value", + self.tr_type(n_component.n_typ)) + if n_component.optional: + s_sort.add_component(n_component.name + ".valid", + smt.BUILTIN_BOOLEAN) + + self.start.add_statement( + smt.Record_Declaration( + s_sort, + "reocrd %s from %s" % ( + n_type.name, + n_type.location.to_string()))) + + return self.records[n_type] else: # pragma: no cover self.flag_unsupported(n_type) @@ -1465,7 +1488,8 @@ def tr_field_access_expression(self, n_expr): assert isinstance(n_expr, Field_Access_Expression) prefix_value, prefix_valid = self.tr_expression(n_expr.n_prefix) - self.attach_validity_check(prefix_valid, n_expr.n_prefix) + if not self.functional: + self.attach_validity_check(prefix_valid, n_expr.n_prefix) field_value = smt.Record_Access(prefix_value, n_expr.n_field.name + ".value")