Coverage for trlc/lint.py: 93%
113 statements
« prev ^ index » next coverage.py v7.7.1, created at 2025-03-27 00:52 +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 for package in self.stab.values(ast.Package):
56 for n_typ in package.symbols.values(ast.Record_Type):
57 if n_typ.is_abstract and not self.abstract_extensions[n_typ]:
58 self.mh.check(
59 n_typ.location,
60 "abstract type %s does not have any extensions" %
61 n_typ.name,
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 def verify_tuple_type(self, n_tuple_type):
85 assert isinstance(n_tuple_type, ast.Tuple_Type)
87 # Detect confusing separators
88 # lobster-trace: LRM.Tuple_Based_Literal_Ambiguity
89 previous_was_int = False
90 previous_was_bad_sep = False
91 bad_separator = None
92 location = None
93 for n_item in n_tuple_type.iter_sequence():
94 if previous_was_bad_sep:
95 assert isinstance(n_item, ast.Composite_Component)
96 if isinstance(n_item.n_typ, ast.Builtin_Integer):
97 explanation = [
98 "For example 0%s100 would be a base %u literal" %
99 (bad_separator,
100 {"b" : 2, "x" : 16}[bad_separator]),
101 "instead of the tuple segment 0 %s 100." %
102 bad_separator
103 ]
104 else:
105 explanation = [
106 "For example 0%s%s would be a lexer error" %
107 (bad_separator,
108 n_item.n_typ.get_example_value()),
109 "instead of the tuple segment 0 %s %s." %
110 (bad_separator,
111 n_item.n_typ.get_example_value())
112 ]
114 self.mh.check(
115 location,
116 "%s separator after integer component"
117 " creates ambiguities" % bad_separator,
118 "separator_based_literal_ambiguity",
119 "\n".join(explanation))
121 elif isinstance(n_item, ast.Composite_Component) and \
122 isinstance(n_item.n_typ, ast.Builtin_Integer):
123 previous_was_int = True
125 elif isinstance(n_item, ast.Separator) and \
126 previous_was_int and \
127 n_item.to_string() in ("x", "b"):
128 previous_was_bad_sep = True
129 bad_separator = n_item.to_string()
130 location = n_item.location
132 else:
133 previous_was_int = False
134 previous_was_bad_sep = False
136 # Walk over components
137 for n_component in n_tuple_type.components.values():
138 self.verify_type(n_component.n_typ)
140 # Verify checks
141 if self.verify_checks: 141 ↛ exitline 141 didn't return from function 'verify_tuple_type' because the condition on line 141 was always true
142 vcg = VCG(mh = self.mh,
143 n_ctyp = n_tuple_type,
144 debug = self.debug_vcg,
145 use_api = self.cvc5_binary is None,
146 cvc5_binary = self.cvc5_binary)
147 vcg.analyze()
149 def verify_record_type(self, n_record_type):
150 # lobster-exclude: Not safety relevant
151 assert isinstance(n_record_type, ast.Record_Type)
153 # Mark abstract extensions
154 if n_record_type.is_abstract:
155 if n_record_type not in self.abstract_extensions:
156 self.abstract_extensions[n_record_type] = set()
157 elif n_record_type.parent and n_record_type.parent.is_abstract:
158 if n_record_type.parent not in self.abstract_extensions:
159 self.abstract_extensions[n_record_type.parent] = set()
160 self.abstract_extensions[n_record_type.parent].add(n_record_type)
162 # Walk over components
163 for n_component in n_record_type.components.values():
164 self.verify_type(n_component.n_typ)
166 # Verify checks
167 if self.verify_checks:
168 vcg = VCG(mh = self.mh,
169 n_ctyp = n_record_type,
170 debug = self.debug_vcg,
171 use_api = self.cvc5_binary is None,
172 cvc5_binary = self.cvc5_binary)
173 vcg.analyze()
175 def verify_array_type(self, n_typ):
176 # lobster-exclude: Not safety relevant
177 assert isinstance(n_typ, ast.Array_Type)
179 if n_typ.upper_bound is None:
180 pass
181 elif n_typ.lower_bound > n_typ.upper_bound:
182 self.mh.check(n_typ.loc_upper,
183 "upper bound must be at least %u" %
184 n_typ.lower_bound,
185 "impossible_array_types")
186 elif n_typ.upper_bound == 0:
187 self.mh.check(n_typ.loc_upper,
188 "this array makes no sense",
189 "impossible_array_types")
190 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 1:
191 self.mh.check(n_typ.loc_upper,
192 "array of fixed size 1 "
193 "should not be an array",
194 "weird_array_types",
195 "An array with a fixed size of 1 should not\n"
196 "be an array at all.")
197 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 0:
198 self.mh.check(n_typ.loc_upper,
199 "consider making this array an"
200 " optional %s" % n_typ.element_type.name,
201 "weird_array_types",
202 "An array with 0 to 1 components should just\n"
203 "be an optional %s instead." %
204 n_typ.element_type.name)
206 def markup_ref(self, item, string_literals):
207 for string_literal in string_literals: 207 ↛ 208line 207 didn't jump to line 208 because the loop on line 207 never started
208 for reference in string_literal.references:
209 if reference.package.name == item.name:
210 return string_literal
211 return None
213 def verify_imports(self):
214 for file in self.mh.sm.all_files.values():
215 if not file.primary and not file.secondary:
216 continue
217 if not file.cu.imports:
218 continue
219 for item in file.cu.imports:
220 import_tokens = [t for t in file.lexer.tokens
221 if t.value == item.name]
222 markup = self.markup_ref(item,
223 (m.ast_link for m in
224 file.lexer.tokens if
225 isinstance(m.ast_link,
226 ast.String_Literal) and
227 m.ast_link.has_references))
228 if markup is not None: 228 ↛ 229line 228 didn't jump to line 229 because the condition on line 228 was never true
229 import_tokens.append(markup)
230 if len(import_tokens) == 1:
231 import_tk = import_tokens[0]
232 self.mh.check(import_tk.location,
233 "unused import %s" % import_tk.value,
234 "unused_imports",
235 "Consider deleting this import"
236 " statement if not needed.")