Coverage for trlc/lint.py: 94%

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/>. 

20 

21from trlc import ast 

22from trlc.errors import Message_Handler, TRLC_Error 

23from trlc.vcg import VCG 

24 

25 

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 

34 

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 

40 

41 self.abstract_extensions = {} 

42 self.checked_types = set() 

43 

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 

53 

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") 

63 

64 return ok 

65 

66 def verify_type(self, n_typ): 

67 # lobster-exclude: Not safety relevant 

68 assert isinstance(n_typ, ast.Type) 

69 

70 if n_typ in self.checked_types: 

71 return 

72 else: 

73 self.checked_types.add(n_typ) 

74 

75 if isinstance(n_typ, ast.Record_Type): 

76 self.verify_record_type(n_typ) 

77 

78 elif isinstance(n_typ, ast.Tuple_Type): 

79 self.verify_tuple_type(n_typ) 

80 

81 elif isinstance(n_typ, ast.Array_Type): 

82 self.verify_array_type(n_typ) 

83 

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) 

104 

105 def verify_tuple_type(self, n_tuple_type): 

106 assert isinstance(n_tuple_type, ast.Tuple_Type) 

107 

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 ] 

134 

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)) 

141 

142 elif isinstance(n_item, ast.Composite_Component) and \ 

143 isinstance(n_item.n_typ, ast.Builtin_Integer): 

144 previous_was_int = True 

145 

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 

152 

153 else: 

154 previous_was_int = False 

155 previous_was_bad_sep = False 

156 

157 # Walk over components 

158 for n_component in n_tuple_type.components.values(): 

159 self.verify_type(n_component.n_typ) 

160 

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() 

169 

170 def verify_record_type(self, n_record_type): 

171 # lobster-exclude: Not safety relevant 

172 assert isinstance(n_record_type, ast.Record_Type) 

173 

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 and n_record_type.parent.is_abstract: 

179 if n_record_type.parent not in self.abstract_extensions: 

180 self.abstract_extensions[n_record_type.parent] = set() 

181 self.abstract_extensions[n_record_type.parent].add(n_record_type) 

182 

183 # Walk over components 

184 for n_component in n_record_type.components.values(): 

185 self.verify_type(n_component.n_typ) 

186 

187 # Verify checks 

188 if self.verify_checks: 

189 vcg = VCG(mh = self.mh, 

190 n_ctyp = n_record_type, 

191 debug = self.debug_vcg, 

192 use_api = self.cvc5_binary is None, 

193 cvc5_binary = self.cvc5_binary) 

194 vcg.analyze() 

195 

196 def verify_array_type(self, n_typ): 

197 # lobster-exclude: Not safety relevant 

198 assert isinstance(n_typ, ast.Array_Type) 

199 

200 if n_typ.upper_bound is None: 

201 pass 

202 elif n_typ.lower_bound > n_typ.upper_bound: 

203 self.mh.check(n_typ.loc_upper, 

204 "upper bound must be at least %u" % 

205 n_typ.lower_bound, 

206 "impossible_array_types") 

207 elif n_typ.upper_bound == 0: 

208 self.mh.check(n_typ.loc_upper, 

209 "this array makes no sense", 

210 "impossible_array_types") 

211 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 1: 

212 self.mh.check(n_typ.loc_upper, 

213 "array of fixed size 1 " 

214 "should not be an array", 

215 "weird_array_types", 

216 "An array with a fixed size of 1 should not\n" 

217 "be an array at all.") 

218 elif n_typ.upper_bound == 1 and n_typ.lower_bound == 0: 

219 self.mh.check(n_typ.loc_upper, 

220 "consider making this array an" 

221 " optional %s" % n_typ.element_type.name, 

222 "weird_array_types", 

223 "An array with 0 to 1 components should just\n" 

224 "be an optional %s instead." % 

225 n_typ.element_type.name) 

226 

227 def markup_ref(self, item, string_literals): 

228 for string_literal in string_literals: 228 ↛ 229line 228 didn't jump to line 229 because the loop on line 228 never started

229 for reference in string_literal.references: 

230 if reference.package.name == item.name: 

231 return string_literal 

232 return None 

233 

234 def verify_imports(self): 

235 for file in self.mh.sm.all_files.values(): 

236 if not file.primary and not file.secondary: 

237 continue 

238 if not file.cu.imports: 

239 continue 

240 for item in file.cu.imports: 

241 import_tokens = [t for t in file.lexer.tokens 

242 if t.value == item.name] 

243 markup = self.markup_ref(item, 

244 (m.ast_link for m in 

245 file.lexer.tokens if 

246 isinstance(m.ast_link, 

247 ast.String_Literal) and 

248 m.ast_link.has_references)) 

249 if markup is not None: 249 ↛ 250line 249 didn't jump to line 250 because the condition on line 249 was never true

250 import_tokens.append(markup) 

251 if len(import_tokens) == 1: 

252 import_tk = import_tokens[0] 

253 self.mh.check(import_tk.location, 

254 "unused import %s" % import_tk.value, 

255 "unused_imports", 

256 "Consider deleting this import" 

257 " statement if not needed.")