diff --git a/tests-system/unresolved-1/foo.rsl b/tests-system/unresolved-1/foo.rsl new file mode 100644 index 00000000..a32be820 --- /dev/null +++ b/tests-system/unresolved-1/foo.rsl @@ -0,0 +1,11 @@ +package Example + +type T { + linked optional ReqId +} + +tuple ReqId { + item T + separator @ + LinkVersion Integer +} diff --git a/tests-system/unresolved-1/foo.trlc b/tests-system/unresolved-1/foo.trlc new file mode 100644 index 00000000..2a884819 --- /dev/null +++ b/tests-system/unresolved-1/foo.trlc @@ -0,0 +1,5 @@ +package Example + +T Test { + +} \ No newline at end of file diff --git a/tests-system/unresolved-1/output b/tests-system/unresolved-1/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-1/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-1/output.brief b/tests-system/unresolved-1/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-1/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-1/output.json b/tests-system/unresolved-1/output.json new file mode 100644 index 00000000..146863d7 --- /dev/null +++ b/tests-system/unresolved-1/output.json @@ -0,0 +1,6 @@ +{ + "Test": { + "linked": null + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-1/output.smtlib b/tests-system/unresolved-1/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-1/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-2/foo.rsl b/tests-system/unresolved-2/foo.rsl new file mode 100644 index 00000000..029176b9 --- /dev/null +++ b/tests-system/unresolved-2/foo.rsl @@ -0,0 +1,11 @@ +package Example + +type T { + linked ReqId +} + +tuple ReqId { + item T + separator @ + LinkVersion Integer +} diff --git a/tests-system/unresolved-2/foo.trlc b/tests-system/unresolved-2/foo.trlc new file mode 100644 index 00000000..3789a939 --- /dev/null +++ b/tests-system/unresolved-2/foo.trlc @@ -0,0 +1,9 @@ +package Example + +T Test_1 { + linked = Test_2@1 +} + +T Test_2 { + linked = Test_1@1 +} \ No newline at end of file diff --git a/tests-system/unresolved-2/output b/tests-system/unresolved-2/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-2/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-2/output.brief b/tests-system/unresolved-2/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-2/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-2/output.json b/tests-system/unresolved-2/output.json new file mode 100644 index 00000000..0b260143 --- /dev/null +++ b/tests-system/unresolved-2/output.json @@ -0,0 +1,15 @@ +{ + "Test_1": { + "linked": { + "LinkVersion": 1, + "item": "Example.Test_2" + } + }, + "Test_2": { + "linked": { + "LinkVersion": 1, + "item": "Example.Test_1" + } + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-2/output.smtlib b/tests-system/unresolved-2/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-2/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-3/foo.rsl b/tests-system/unresolved-3/foo.rsl new file mode 100644 index 00000000..7261b360 --- /dev/null +++ b/tests-system/unresolved-3/foo.rsl @@ -0,0 +1,11 @@ +package Example + +type Requirement { + linked ReqId[0 .. *] +} + +tuple ReqId { + item Requirement + separator @ + LinkVersion Integer +} diff --git a/tests-system/unresolved-3/foo.trlc b/tests-system/unresolved-3/foo.trlc new file mode 100644 index 00000000..4ef5c682 --- /dev/null +++ b/tests-system/unresolved-3/foo.trlc @@ -0,0 +1,9 @@ +package Example + +Requirement Test_1 { + linked = [] +} + +Requirement Test_2 { + linked = [Test_1@1] +} \ No newline at end of file diff --git a/tests-system/unresolved-3/output b/tests-system/unresolved-3/output new file mode 100644 index 00000000..d9000c17 --- /dev/null +++ b/tests-system/unresolved-3/output @@ -0,0 +1,3 @@ +linked = [Test_1@1] + ^ unresolved-3/foo.trlc:8: error: unknown symbol ReqId +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/unresolved-3/output.brief b/tests-system/unresolved-3/output.brief new file mode 100644 index 00000000..c9d696d7 --- /dev/null +++ b/tests-system/unresolved-3/output.brief @@ -0,0 +1,2 @@ +unresolved-3/foo.trlc:8:14: trlc error: unknown symbol ReqId +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/unresolved-3/output.json b/tests-system/unresolved-3/output.json new file mode 100644 index 00000000..d9000c17 --- /dev/null +++ b/tests-system/unresolved-3/output.json @@ -0,0 +1,3 @@ +linked = [Test_1@1] + ^ unresolved-3/foo.trlc:8: error: unknown symbol ReqId +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/unresolved-3/output.smtlib b/tests-system/unresolved-3/output.smtlib new file mode 100644 index 00000000..d9000c17 --- /dev/null +++ b/tests-system/unresolved-3/output.smtlib @@ -0,0 +1,3 @@ +linked = [Test_1@1] + ^ unresolved-3/foo.trlc:8: error: unknown symbol ReqId +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/unresolved-4/foo.rsl b/tests-system/unresolved-4/foo.rsl new file mode 100644 index 00000000..45c5932f --- /dev/null +++ b/tests-system/unresolved-4/foo.rsl @@ -0,0 +1,11 @@ +package Example + +tuple ReqId { + item Requirement + separator @ + LinkVersion Integer +} + +type Requirement { + linked ReqId +} diff --git a/tests-system/unresolved-4/foo.trlc b/tests-system/unresolved-4/foo.trlc new file mode 100644 index 00000000..2a20b3a1 --- /dev/null +++ b/tests-system/unresolved-4/foo.trlc @@ -0,0 +1,9 @@ +package Example + +Requirement Test_1 { + linked = Test_2@2 +} + +Requirement Test_2 { + linked = Test_1@1 +} diff --git a/tests-system/unresolved-4/output b/tests-system/unresolved-4/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-4/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-4/output.brief b/tests-system/unresolved-4/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-4/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-4/output.json b/tests-system/unresolved-4/output.json new file mode 100644 index 00000000..82944965 --- /dev/null +++ b/tests-system/unresolved-4/output.json @@ -0,0 +1,15 @@ +{ + "Test_1": { + "linked": { + "LinkVersion": 2, + "item": "Example.Test_2" + } + }, + "Test_2": { + "linked": { + "LinkVersion": 1, + "item": "Example.Test_1" + } + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-4/output.smtlib b/tests-system/unresolved-4/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-4/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-5/foo.rsl b/tests-system/unresolved-5/foo.rsl new file mode 100644 index 00000000..1110f7f2 --- /dev/null +++ b/tests-system/unresolved-5/foo.rsl @@ -0,0 +1,11 @@ +package Example + +tuple ReqId { + item Requirement + separator @ + LinkVersion Integer +} + +type Requirement { + linked ReqId[0 .. *] +} diff --git a/tests-system/unresolved-5/foo.trlc b/tests-system/unresolved-5/foo.trlc new file mode 100644 index 00000000..466a1008 --- /dev/null +++ b/tests-system/unresolved-5/foo.trlc @@ -0,0 +1,9 @@ +package Example + +Requirement Test_1 { + linked = [] +} + +Requirement Test_2 { + linked = [Test_1@1] +} diff --git a/tests-system/unresolved-5/output b/tests-system/unresolved-5/output new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-5/output @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-5/output.brief b/tests-system/unresolved-5/output.brief new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-5/output.brief @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-5/output.json b/tests-system/unresolved-5/output.json new file mode 100644 index 00000000..2b1b59f7 --- /dev/null +++ b/tests-system/unresolved-5/output.json @@ -0,0 +1,14 @@ +{ + "Test_1": { + "linked": [] + }, + "Test_2": { + "linked": [ + { + "LinkVersion": 1, + "item": "Example.Test_1" + } + ] + } +} +Processed 1 model and 1 requirement file and found no issues diff --git a/tests-system/unresolved-5/output.smtlib b/tests-system/unresolved-5/output.smtlib new file mode 100644 index 00000000..a36e3bac --- /dev/null +++ b/tests-system/unresolved-5/output.smtlib @@ -0,0 +1 @@ +Processed 1 model and 1 requirement file and found no issues diff --git a/trlc/ast.py b/trlc/ast.py index 7977b9a7..9158e96c 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -928,6 +928,10 @@ def to_python_object(self): def can_be_null(self): return False + def update_fields(self, parent): + for value in self.value: + if isinstance(value, (Tuple_Aggregate, Array_Aggregate)): + value.update_fields(parent) class Tuple_Aggregate(Expression): """Instances of a tuple @@ -1020,6 +1024,69 @@ def to_python_object(self): def can_be_null(self): return False + def update_fields(self, parent): + """ + Update `self.value` dictionary with resolved values for each optional field + that has a valid `description` in `self.typ`. + + Resolution supports: + - Nested paths using '@' as a separator. + - Special reference `$parent` pointing to the parent object. + + Example for two supported forms:: + type A { + field int + } + tuple LinkB2A { + derived A + separator @ + field_A "derived@field" optional int + ^^^^^^^^^^^^^1 + separator @ + field_B "$parent@field" optional int + ^^^^^^^^^^^^^2 + } + type B { + field int + derived_from LinkB2A[1 .. *] + } + + :form 1: `@` (see 1) + `field_A` resolves to the referenced field in type A. + + :form 2: `$parent@` (see 2) + `field_B` resolves to the field in the parent type B. + + Note that only fields with valid `description` are eligible for this resolution, + and shall be declared as "optional". + + """ + for n_item in self.typ.iter_sequence(): + if not isinstance(n_item, Composite_Component): + continue + desc = n_item.description + if desc is None or ("@" not in desc and "$parent" not in desc): + continue + + current = self.value + parts = desc.split("@") + if parts[0] == "$parent": + current, parts = parent, parts[1:] + elif "$parent" in parts: + raise KeyError(f"Invalid description '{desc}': $parent only allowed at beginning") + + for part in parts: + if isinstance(current, dict): + current = current.get(part) + elif isinstance(current, Record_Object): + current = current.field.get(part) + else: + raise KeyError(f"Invalid traversal at '{part}' in {desc}") + if current is None: + raise KeyError(f"Cannot resolve '{part}' in '{desc}'") + if isinstance(current, Record_Reference): + current = current.target + self.value[n_item.name] = current class Record_Reference(Expression): """Reference to another record object @@ -1087,6 +1154,11 @@ def resolve_references(self, mh): name = self.name, error_location = self.location, required_subclass = Record_Object) + if isinstance(self.target, Unresolved_Type): + mh.error( + self.location, + self.target.error_msg + ) if self.typ is None: self.typ = self.target.n_typ elif not self.target.n_typ.is_subclass_of(self.typ): @@ -2820,6 +2892,13 @@ def get_example_value(self): else: return "(%s)" % ", ".join(parts) +class Unresolved_Type(Composite_Type): + def __init__(self, name, description, location, package): + super().__init__(name, description, location, package) + self.error_msg = None + + def dump(self): + pass class Separator(Node): # lobster-trace: LRM.Tuple_Declaration @@ -3028,6 +3107,11 @@ def resolve_references(self, mh): for val in self.field.values(): val.resolve_references(mh) + def update_items(self): + for value in self.field.values(): + if isinstance(value, (Tuple_Aggregate, Array_Aggregate)): + value.update_fields(self) + def perform_checks(self, mh): # lobster-trace: LRM.Check_Evaluation_Order # lobster-trace: LRM.Evaluation_Of_Checks @@ -3382,13 +3466,35 @@ def lookup_direct(self, n = 1) if matches: - mh.error(error_location, - "unknown symbol %s, did you mean %s?" % - (name, - matches[0])) + pkg_dummy = Package( + "__unresolved__", + error_location, + Symbol_Table(), + declared_late=True + ) + n_unresolved = Unresolved_Type( + name=name, + description=None, + location=error_location, + package=pkg_dummy + ) + n_unresolved.error_msg = "unknown symbol %s, did you mean %s?" % (name, matches[0]) + return n_unresolved else: - mh.error(error_location, - "unknown symbol %s" % name) + pkg_dummy = Package( + "__unresolved__", + error_location, + Symbol_Table(), + declared_late=True + ) + n_unresolved = Unresolved_Type( + name=name, + description=None, + location=error_location, + package=pkg_dummy + ) + n_unresolved.error_msg = "unknown symbol %s" % name + return n_unresolved def lookup(self, mh, referencing_token, required_subclass=None): # lobster-trace: LRM.Described_Name_Equality diff --git a/trlc/lint.py b/trlc/lint.py index 2f9f7a68..25288a59 100644 --- a/trlc/lint.py +++ b/trlc/lint.py @@ -154,7 +154,7 @@ def verify_record_type(self, n_record_type): if n_record_type.is_abstract: if n_record_type not in self.abstract_extensions: self.abstract_extensions[n_record_type] = set() - elif n_record_type.parent and n_record_type.parent.is_abstract: + if n_record_type.parent and n_record_type.parent.is_abstract: if n_record_type.parent not in self.abstract_extensions: self.abstract_extensions[n_record_type.parent] = set() self.abstract_extensions[n_record_type.parent].add(n_record_type) diff --git a/trlc/parser.py b/trlc/parser.py index cf74ddd1..a533b0ef 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -638,6 +638,12 @@ def parse_record_declaration(self): else: root_record = None + if isinstance(root_record, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + root_record.error_msg + ) + if self.lint_mode and \ root_record and root_record.is_final and \ not is_final: @@ -1097,6 +1103,11 @@ def parse_quantified_expression(self, scope): t_in = self.ct self.match("IDENTIFIER") field = scope.lookup(self.mh, self.ct, ast.Composite_Component) + if isinstance(field, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + field.error_msg + ) n_source = ast.Name_Reference(self.ct.location, field) n_source.set_ast_link(self.ct) @@ -1328,6 +1339,11 @@ def parse_name(self, scope): # immediately, we have a builtin function call. n_name = self.stab.lookup(self.mh, self.ct) + if isinstance(n_name, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + n_name.error_msg + ) if not isinstance(n_name, (ast.Builtin_Function, ast.Builtin_Numeric_Type)): self.mh.error(self.ct.location, @@ -1351,6 +1367,12 @@ def parse_name(self, scope): enum_lit.set_ast_link(self.ct) return enum_lit + if isinstance(n_name, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + n_name.error_msg + ) + # Anything that remains is either a function call or an actual # name. Let's just enforce this for sanity. if not isinstance(n_name, (ast.Builtin_Function, @@ -1395,6 +1417,11 @@ def parse_name(self, scope): n_field = n_name.typ.components.lookup(self.mh, self.ct, ast.Composite_Component) + if isinstance(n_field, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + n_field.error_msg + ) n_field.set_ast_link(self.ct) n_name = ast.Field_Access_Expression( mh = self.mh, @@ -1440,6 +1467,11 @@ def parse_check_block(self): n_ctype = self.cu.package.symbols.lookup(self.mh, self.ct, ast.Composite_Type) + if isinstance(n_ctype, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + n_ctype.error_msg + ) n_check_block = ast.Check_Block(location = self.ct.location, n_typ = n_ctype) n_check_block.set_ast_link(t_checks) @@ -1669,6 +1701,11 @@ def parse_value(self, typ): elif isinstance(typ, ast.Enumeration_Type): enum = self.parse_qualified_name(self.default_scope, ast.Enumeration_Type) + if isinstance(enum, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + enum.error_msg + ) enum.set_ast_link(self.ct) if enum != typ: self.mh.error(self.ct.location, @@ -1679,6 +1716,11 @@ def parse_value(self, typ): lit = enum.literals.lookup(self.mh, self.ct, ast.Enumeration_Literal_Spec) + if isinstance(lit, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + lit.error_msg + ) return ast.Enumeration_Literal(self.ct.location, lit) @@ -1763,6 +1805,12 @@ def parse_value(self, typ): rv.set_ast_link(self.ct) return rv + elif isinstance(typ, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + typ.error_msg + ) + else: self.mh.ice_loc(self.ct.location, "logic error: unexpected type %s" % @@ -1788,6 +1836,11 @@ def parse_record_object_declaration(self): r_typ = self.parse_qualified_name(self.default_scope, ast.Record_Type) + if isinstance(r_typ, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + r_typ.error_msg + ) r_typ.set_ast_link(self.ct) if r_typ.is_abstract: self.mh.error(self.ct.location, @@ -1811,6 +1864,11 @@ def parse_record_object_declaration(self): comp = r_typ.components.lookup(self.mh, self.ct, ast.Composite_Component) + if isinstance(comp, ast.Unresolved_Type): + self.mh.error( + self.ct.location, + comp.error_msg + ) if obj.is_component_implicit_null(comp): self.mh.error(self.ct.location, "component '%s' already assigned at line %i" % @@ -1926,6 +1984,8 @@ def parse_rsl_file(self): break self.advance() self.skip_until_newline() + # Try to resolve any Unresolved_Type placeholders collected during parsing + self.resolve_unresolved_types() self.match_eof() @@ -1934,6 +1994,38 @@ def parse_rsl_file(self): self.cu.package.set_ast_link(tok) return ok + + def resolve_unresolved_types(self, fail_on_unresolved=True): + if len(getattr(self.default_scope, "scope", [])) > 1: + pkg_stab = self.default_scope.scope[1] + pkg_table = getattr(pkg_stab, "table", {}) + for n_item in self.cu.items: + if isinstance(n_item, ast.Tuple_Type) or isinstance(n_item, ast.Record_Type): + for comp_name in list(n_item.components.table.keys()): + comp = n_item.components.table[comp_name] + if not isinstance(comp.n_typ, ast.Unresolved_Type): + continue + for sym_key in list(pkg_table.keys()): + sym = pkg_table[sym_key] + if comp.n_typ.name == getattr(sym, "name", None): + n_item.components.table[comp_name].n_typ = sym + break + + if not fail_on_unresolved: + return + + remaining = [] + for item in self.cu.items: + if isinstance(item, (ast.Tuple_Type, ast.Record_Type)): + for comp in item.components.table.values(): + if isinstance(comp.n_typ, ast.Unresolved_Type): + remaining.append((item, comp)) + + if remaining: + names = ", ".join("%s.%s" % (it.name, comp.name) for it, comp in remaining) + first_loc = remaining[0][1].n_typ.location + self.mh.error(first_loc, + comp.n_typ.error_msg) def parse_trlc_file(self): # lobster-trace: LRM.TRLC_File diff --git a/trlc/trlc.py b/trlc/trlc.py index 4f6d64ff..f02de1ab 100644 --- a/trlc/trlc.py +++ b/trlc/trlc.py @@ -463,6 +463,7 @@ def resolve_record_references(self): for obj in package.symbols.values(ast.Record_Object): try: obj.resolve_references(self.mh) + obj.update_items() except TRLC_Error: ok = False diff --git a/trlc/vcg.py b/trlc/vcg.py index 19899810..c9314726 100644 --- a/trlc/vcg.py +++ b/trlc/vcg.py @@ -537,6 +537,18 @@ def value_to_trlc(self, n_typ, value): item) for item in value) + elif isinstance(n_typ, Unresolved_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) + else: # pragma: no cover self.flag_unsupported(n_typ, "back-conversion from %s" % n_typ.name) @@ -728,6 +740,9 @@ def tr_type(self, n_type): # arbitrary fictional record names return smt.BUILTIN_INTEGER + elif isinstance(n_type, Unresolved_Type): + return smt.BUILTIN_INTEGER + else: # pragma: no cover self.flag_unsupported(n_type)