Coverage for trlc/lint.py: 94%
125 statements
« prev ^ index » next coverage.py v7.10.7, created at 2026-05-21 07:21 +0000
1#!/usr/bin/env python3
2#
3# TRLC - Treat Requirements Like Code
4# Copyright (C) 2022-2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG)
5#
6# This file is part of the TRLC Python Reference Implementation.
7#
8# TRLC is free software: you can redistribute it and/or modify it
9# under the terms of the GNU General Public License as published by
10# the Free Software Foundation, either version 3 of the License, or
11# (at your option) any later version.
12#
13# TRLC is distributed in the hope that it will be useful, but WITHOUT
14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
15# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
16# License for more details.
17#
18# You should have received a copy of the GNU General Public License
19# along with TRLC. If not, see <https://www.gnu.org/licenses/>.
21from trlc import ast
22from trlc.errors import Message_Handler, TRLC_Error
23from trlc.vcg import VCG
26class Linter:
27 def __init__(self, mh, stab, verify_checks, debug_vcg, cvc5_binary):
28 # lobster-exclude: Not safety relevant
29 assert isinstance(mh, Message_Handler)
30 assert isinstance(stab, ast.Symbol_Table)
31 assert isinstance(verify_checks, bool)
32 assert isinstance(debug_vcg, bool)
33 assert isinstance(cvc5_binary, str) or cvc5_binary is None
35 self.mh = mh
36 self.stab = stab
37 self.verify_checks = verify_checks
38 self.debug_vcg = debug_vcg
39 self.cvc5_binary = cvc5_binary
41 self.abstract_extensions = {}
42 self.checked_types = set()
44 def perform_sanity_checks(self):
45 # lobster-exclude: Not safety relevant
46 ok = True
47 for package in self.stab.values(ast.Package):
48 for n_typ in package.symbols.values(ast.Type):
49 try:
50 self.verify_type(n_typ)
51 except TRLC_Error:
52 ok = False
54 # Complain about abstract types without extensions
55 # lobster-trace: LRM.Abstract_Type_Not_Extended
56 for package in self.stab.values(ast.Package):
57 for n_typ in package.symbols.values(ast.Record_Type):
58 if n_typ.is_abstract and not self.abstract_extensions[n_typ]:
59 self.mh.check(
60 n_typ.location,
61 f"abstract type {n_typ.name} does not have any extensions",
62 "abstract_leaf_types")
64 return ok
66 def verify_type(self, n_typ):
67 # lobster-exclude: Not safety relevant
68 assert isinstance(n_typ, ast.Type)
70 if n_typ in self.checked_types:
71 return
72 else:
73 self.checked_types.add(n_typ)
75 if isinstance(n_typ, ast.Record_Type):
76 self.verify_record_type(n_typ)
78 elif isinstance(n_typ, ast.Tuple_Type):
79 self.verify_tuple_type(n_typ)
81 elif isinstance(n_typ, ast.Array_Type):
82 self.verify_array_type(n_typ)
84 elif isinstance(n_typ, ast.Union_Type):
85 # lobster-trace: LRM.Union_Type_Minimum_Members
86 if len(n_typ.types) == 1:
87 self.mh.check(
88 n_typ.location,
89 "union type with a single member is equivalent to a"
90 " plain record reference",
91 "union_single_type")
92 # lobster-trace: LRM.Union_Type_No_Subtype_Relations
93 for i, t_i in enumerate(n_typ.types):
94 for j, t_j in enumerate(n_typ.types):
95 if i != j and t_i is not t_j and \
96 t_i.is_subclass_of(t_j):
97 self.mh.check(
98 n_typ.location,
99 "%s is a subtype of %s which is already"
100 " in this union" % (t_i.name, t_j.name),
101 "union_redundant_subtype")
102 for member_type in n_typ.types:
103 self.verify_type(member_type)
105 def verify_tuple_type(self, n_tuple_type):
106 assert isinstance(n_tuple_type, ast.Tuple_Type)
108 # Detect confusing separators
109 # lobster-trace: LRM.Tuple_Based_Literal_Ambiguity
110 previous_was_int = False
111 previous_was_bad_sep = False
112 bad_separator = None
113 location = None
114 for n_item in n_tuple_type.iter_sequence():
115 if previous_was_bad_sep:
116 assert isinstance(n_item, ast.Composite_Component)
117 if isinstance(n_item.n_typ, ast.Builtin_Integer):
118 explanation = [
119 "For example 0%s100 would be a base %u literal" %
120 (bad_separator,
121 {"b" : 2, "x" : 16}[bad_separator]),
122 "instead of the tuple segment 0 %s 100." %
123 bad_separator
124 ]
125 else:
126 explanation = [
127 "For example 0%s%s would be a lexer error" %
128 (bad_separator,
129 n_item.n_typ.get_example_value()),
130 "instead of the tuple segment 0 %s %s." %
131 (bad_separator,
132 n_item.n_typ.get_example_value())
133 ]
135 self.mh.check(
136 location,
137 "%s separator after integer component"
138 " creates ambiguities" % bad_separator,
139 "separator_based_literal_ambiguity",
140 "\n".join(explanation))
142 elif isinstance(n_item, ast.Composite_Component) and \
143 isinstance(n_item.n_typ, ast.Builtin_Integer):
144 previous_was_int = True
146 elif isinstance(n_item, ast.Separator) and \
147 previous_was_int and \
148 n_item.to_string() in ("x", "b"):
149 previous_was_bad_sep = True
150 bad_separator = n_item.to_string()
151 location = n_item.location
153 else:
154 previous_was_int = False
155 previous_was_bad_sep = False
157 # Walk over components
158 for n_component in n_tuple_type.components.values():
159 self.verify_type(n_component.n_typ)
161 # Verify checks
162 if self.verify_checks: 162 ↛ exitline 162 didn't return from function 'verify_tuple_type' because the condition on line 162 was always true
163 vcg = VCG(mh = self.mh,
164 n_ctyp = n_tuple_type,
165 debug = self.debug_vcg,
166 use_api = self.cvc5_binary is None,
167 cvc5_binary = self.cvc5_binary)
168 vcg.analyze()
170 def verify_record_type(self, n_record_type):
171 # lobster-exclude: Not safety relevant
172 assert isinstance(n_record_type, ast.Record_Type)
174 # Mark abstract extensions
175 if n_record_type.is_abstract:
176 if n_record_type not in self.abstract_extensions:
177 self.abstract_extensions[n_record_type] = set()
178 elif n_record_type.parent:
179 ancestor = n_record_type.parent
180 while ancestor is not None and ancestor.is_abstract:
181 if ancestor not in self.abstract_extensions:
182 self.abstract_extensions[ancestor] = set()
183 self.abstract_extensions[ancestor].add(n_record_type)
184 ancestor = ancestor.parent
186 # Walk over components
187 for n_component in n_record_type.components.values():
188 self.verify_type(n_component.n_typ)
190 # Verify checks
191 if self.verify_checks:
192 vcg = VCG(mh = self.mh,
193 n_ctyp = n_record_type,
194 debug = self.debug_vcg,
195 use_api = self.cvc5_binary is None,
196 cvc5_binary = self.cvc5_binary)
197 vcg.analyze()
199 def verify_array_type(self, n_typ):
200 # lobster-exclude: Not safety relevant
201 assert isinstance(n_typ, ast.Array_Type)
203 if n_typ.upper_bound is None:
204 pass
205 elif n_typ.lower_bound > n_typ.upper_bound:
206 self.mh.check(n_typ.loc_upper,
207 "upper bound must be at least %u" %
208 n_typ.lower_bound,
209 "impossible_array_types")
210 elif n_typ.upper_bound == 0:
211 self.mh.check(n_typ.loc_upper,
212 "this array makes no sense",
213 "impossible_array_types")
214 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 1:
215 self.mh.check(n_typ.loc_upper,
216 "array of fixed size 1 "
217 "should not be an array",
218 "weird_array_types",
219 "An array with a fixed size of 1 should not\n"
220 "be an array at all.")
221 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 0:
222 self.mh.check(n_typ.loc_upper,
223 "consider making this array an"
224 " optional %s" % n_typ.element_type.name,
225 "weird_array_types",
226 "An array with 0 to 1 components should just\n"
227 "be an optional %s instead." %
228 n_typ.element_type.name)
230 def markup_ref(self, item, string_literals):
231 for string_literal in string_literals: 231 ↛ 232line 231 didn't jump to line 232 because the loop on line 231 never started
232 for reference in string_literal.references:
233 if reference.package.name == item.name:
234 return string_literal
235 return None
237 def verify_imports(self):
238 for file in self.mh.sm.all_files.values():
239 if not file.primary and not file.secondary:
240 continue
241 if not file.cu.imports:
242 continue
243 for item in file.cu.imports:
244 import_tokens = [t for t in file.lexer.tokens
245 if t.value == item.name]
246 markup = self.markup_ref(item,
247 (m.ast_link for m in
248 file.lexer.tokens if
249 isinstance(m.ast_link,
250 ast.String_Literal) and
251 m.ast_link.has_references))
252 if markup is not None: 252 ↛ 253line 252 didn't jump to line 253 because the condition on line 252 was never true
253 import_tokens.append(markup)
254 if len(import_tokens) == 1:
255 import_tk = import_tokens[0]
256 self.mh.check(import_tk.location,
257 "unused import %s" % import_tk.value,
258 "unused_imports",
259 "Consider deleting this import"
260 " statement if not needed.")