Coverage for trlc/trlc.py: 93%

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 

21import argparse 

22import json 

23import os 

24import re 

25import sys 

26from fractions import Fraction 

27 

28from trlc import ast, lint 

29from trlc.errors import Kind, Location, Message_Handler, TRLC_Error 

30from trlc.lexer import Token_Stream 

31from trlc.lexer_md import MD_Lexer 

32from trlc.parser import Parser 

33from trlc.trlc_markdown_parser import TrlcMarkdownParser 

34from trlc.version import BUGS_URL, TRLC_VERSION 

35 

36# pylint: disable=unused-import 

37try: 

38 import cvc5 

39 

40 VCG_API_AVAILABLE = True 

41except ImportError: # pragma: no cover 

42 VCG_API_AVAILABLE = False 

43 

44MARKDOWN_EXTENSION = ".trlc.md" 

45 

46 

47class Source_Manager: 

48 """Dependency and source manager for TRLC. 

49 

50 This is the main entry point when using the Python API. Create an 

51 instance of this, register the files you want to look at, and 

52 finally call the process method. 

53 

54 :param mh: The message handler to use 

55 :type mh: Message_Handler 

56 

57 :param error_recovery: If true attempts to continue parsing after \ 

58 errors. This may generate weird error messages since it's impossible \ 

59 to reliably recover the parse context in all cases. 

60 :type error_recovery: bool 

61 

62 :param lint_mode: If true enables additional warning messages. 

63 :type lint_mode: bool 

64 

65 :param verify_mode: If true performs in-depth static analysis for \ 

66 user-defined checks. Requires CVC5 and PyVCG to be installed. 

67 :type verify_mode: bool 

68 

69 :param parse_trlc: If true parses trlc files, otherwise they are \ 

70 ignored. 

71 :type parse_trlc: bool 

72 

73 :param debug_vcg: If true and verify_mode is also true, emit the \ 

74 individual SMTLIB2 VCs and generate a picture of the program \ 

75 graph. Requires Graphviz to be installed. 

76 :type debug_vcg: bool 

77 

78 """ 

79 

80 def __init__( 

81 self, 

82 mh, 

83 lint_mode=True, 

84 parse_trlc=True, 

85 verify_mode=False, 

86 debug_vcg=False, 

87 error_recovery=True, 

88 ): 

89 assert isinstance(mh, Message_Handler) 

90 assert isinstance(lint_mode, bool) 

91 assert isinstance(parse_trlc, bool) 

92 assert isinstance(verify_mode, bool) 

93 assert isinstance(debug_vcg, bool) 

94 

95 self.mh = mh 

96 self.mh.sm = self 

97 self.stab = ast.Symbol_Table.create_global_table(mh) 

98 self.includes = {} 

99 self.rsl_files = {} 

100 self.trlc_files = {} 

101 self.all_files = {} 

102 self.dep_graph = {} 

103 

104 self.files_with_preamble_errors = set() 

105 

106 self.lint_mode = lint_mode 

107 self.parse_trlc = parse_trlc 

108 self.verify_mode = verify_mode 

109 self.debug_vcg = debug_vcg 

110 self.error_recovery = error_recovery 

111 

112 self.exclude_patterns = [] 

113 self.common_root = None 

114 

115 self.progress_current = 0 

116 self.progress_final = 0 

117 

118 def callback_parse_begin(self): 

119 pass 

120 

121 def callback_parse_progress(self, progress): 

122 assert isinstance(progress, int) 

123 

124 def callback_parse_end(self): 

125 pass 

126 

127 def signal_progress(self): 

128 self.progress_current += 1 

129 if self.progress_final: 

130 progress = (self.progress_current * 100) // self.progress_final 

131 else: # pragma: no cover 

132 progress = 100 

133 self.callback_parse_progress(min(progress, 100)) 

134 

135 def cross_file_reference(self, location): 

136 assert isinstance(location, Location) 

137 

138 if self.common_root is None: 138 ↛ 139line 138 didn't jump to line 139 because the condition on line 138 was never true

139 return location.to_string(False) 

140 elif location.line_no is None: 

141 return os.path.relpath(location.file_name, self.common_root) 

142 else: 

143 return "%s:%u" % ( 

144 os.path.relpath(location.file_name, self.common_root), 

145 location.line_no, 

146 ) 

147 

148 def update_common_root(self, file_name): 

149 assert isinstance(file_name, str) 

150 

151 if self.common_root is None: 

152 self.common_root = os.path.dirname(os.path.abspath(file_name)) 

153 else: 

154 new_root = os.path.dirname(os.path.abspath(file_name)) 

155 for n, (char_a, char_b) in enumerate(zip(self.common_root, new_root)): 

156 if char_a != char_b: 

157 self.common_root = self.common_root[0:n] 

158 break 

159 

160 def create_parser(self, file_name, file_content=None, primary_file=True): 

161 assert os.path.isfile(file_name) 

162 assert isinstance(file_content, str) or file_content is None 

163 assert isinstance(primary_file, bool) 

164 

165 if file_name.endswith(MARKDOWN_EXTENSION): 

166 lexer = MD_Lexer(self.mh, file_name, file_content) 

167 return TrlcMarkdownParser( 

168 mh=self.mh, 

169 stab=self.stab, 

170 file_name=file_name, 

171 lint_mode=self.lint_mode, 

172 error_recovery=self.error_recovery, 

173 primary_file=primary_file, 

174 lexer=lexer, 

175 ) 

176 

177 lexer = Token_Stream(self.mh, file_name, file_content) 

178 

179 return Parser( 

180 mh=self.mh, 

181 stab=self.stab, 

182 file_name=file_name, 

183 lint_mode=self.lint_mode, 

184 error_recovery=self.error_recovery, 

185 primary_file=primary_file, 

186 lexer=lexer, 

187 ) 

188 

189 def register_include(self, dir_name): 

190 """Make contents of a directory available for automatic inclusion 

191 

192 :param dir_name: name of the directory 

193 :type dir_name: str 

194 :raise AssertionError: if dir_name is not a directory 

195 """ 

196 assert os.path.isdir(dir_name) 

197 

198 for path, dirs, files in os.walk(dir_name): 

199 for n, dirname in reversed(list(enumerate(dirs))): 199 ↛ 200line 199 didn't jump to line 200 because the loop on line 199 never started

200 keep = True 

201 for exclude_pattern in self.exclude_patterns: 

202 if exclude_pattern.match(dirname): 

203 keep = False 

204 break 

205 if not keep: 

206 del dirs[n] 

207 

208 self.includes.update( 

209 { 

210 os.path.abspath(full_name): full_name 

211 for full_name in ( 

212 os.path.join(path, file_name) 

213 for file_name in files 

214 if os.path.splitext(file_name)[1] in (".rsl", ".trlc") 

215 ) 

216 } 

217 ) 

218 

219 def register_file(self, file_name, file_content=None, primary=True): 

220 """Schedule a file for parsing. 

221 

222 :param file_name: name of the file 

223 :type file_name: str 

224 :raise AssertionError: if the file does not exist 

225 :raise AssertionError: if the file is registered more than once 

226 :raise TRLC_Error: if the file is not a rsl, trlc or trlc.md file 

227 

228 :param file_content: content of the file 

229 :type file_content: str 

230 :raise AssertionError: if the content is not of type string 

231 

232 :param primary: should be False if the file is a potential \ 

233 include file, and True otherwise. 

234 :type primary: bool 

235 

236 :return: true if the file could be registered without issues 

237 :rtype: bool 

238 """ 

239 assert os.path.isfile(file_name) 

240 assert isinstance(file_content, str) or file_content is None 

241 # lobster-trace: LRM.Layout 

242 

243 try: 

244 if file_name.endswith(".rsl"): 

245 self.register_rsl_file(file_name, file_content, primary) 

246 elif file_name.endswith(".trlc") or file_name.endswith(MARKDOWN_EXTENSION): 

247 self.register_trlc_file(file_name, file_content, primary) 

248 else: # pragma: no cover 

249 self.mh.error( 

250 Location(os.path.basename(file_name)), 

251 "is not a rsl, trlc or trlc.md file", 

252 fatal=False, 

253 ) 

254 return False 

255 

256 except TRLC_Error: 

257 return False 

258 

259 return True 

260 

261 def register_directory(self, dir_name): 

262 """Schedule a directory tree for parsing. 

263 

264 :param dir_name: name of the directory 

265 :type file_name: str 

266 :raise AssertionError: if the directory does not exist 

267 :raise AssertionError: if any item in the directory is already \ 

268 registered 

269 :raise TRLC_Error: on any parse errors 

270 

271 :return: true if the directory could be registered without issues 

272 :rtype: bool 

273 """ 

274 assert os.path.isdir(dir_name) 

275 # lobster-trace: LRM.Layout 

276 

277 ok = True 

278 for path, dirs, files in os.walk(dir_name): 

279 dirs.sort() 

280 

281 for n, dirname in reversed(list(enumerate(dirs))): 

282 keep = True 

283 for exclude_pattern in self.exclude_patterns: 

284 if exclude_pattern.match(dirname): 

285 keep = False 

286 break 

287 if not keep: 

288 del dirs[n] 

289 

290 for file_name in sorted(files): 

291 if os.path.splitext(file_name)[1] in ( 

292 ".rsl", 

293 ".trlc", 

294 ) or file_name.endswith(MARKDOWN_EXTENSION): 

295 ok &= self.register_file(os.path.join(path, file_name)) 

296 return ok 

297 

298 def register_rsl_file(self, file_name, file_content=None, primary=True): 

299 assert os.path.isfile(file_name) 

300 assert file_name not in self.rsl_files 

301 assert isinstance(file_content, str) or file_content is None 

302 assert isinstance(primary, bool) 

303 # lobster-trace: LRM.Preamble 

304 

305 self.update_common_root(file_name) 

306 parser = self.create_parser(file_name, file_content, primary) 

307 self.rsl_files[file_name] = parser 

308 self.all_files[file_name] = parser 

309 if os.path.abspath(file_name) in self.includes: 

310 del self.includes[os.path.abspath(file_name)] 

311 

312 def register_trlc_file(self, file_name, file_content=None, primary=True): 

313 # lobster-trace: LRM.TRLC_File 

314 assert os.path.isfile(file_name) 

315 assert file_name not in self.trlc_files 

316 assert isinstance(file_content, str) or file_content is None 

317 assert isinstance(primary, bool) 

318 # lobster-trace: LRM.Preamble 

319 

320 if not self.parse_trlc: # pragma: no cover 

321 # Not executed as process should exit before we attempt this. 

322 return 

323 

324 self.update_common_root(file_name) 

325 parser = self.create_parser(file_name, file_content, primary) 

326 self.trlc_files[file_name] = parser 

327 self.all_files[file_name] = parser 

328 if os.path.abspath(file_name) in self.includes: 

329 del self.includes[os.path.abspath(file_name)] 

330 

331 def build_graph(self): 

332 # lobster-trace: LRM.Preamble 

333 

334 # Register all include files not yet registered 

335 for file_name in list(sorted(self.includes.values())): 

336 self.register_file(file_name, primary=False) 

337 

338 # Parse preambles and build dependency graph 

339 ok = True 

340 graph = self.dep_graph 

341 files = {} 

342 for container, kind in ((self.rsl_files, "rsl"), (self.trlc_files, "trlc")): 

343 # First parse preamble and register packages in graph 

344 for file_name in sorted(container): 

345 try: 

346 parser = container[file_name] 

347 parser.parse_preamble(kind) 

348 pkg_name = parser.cu.package.name 

349 if (pkg_name, "rsl") not in graph: 

350 graph[(pkg_name, "rsl")] = set() 

351 graph[(pkg_name, "trlc")] = set([(pkg_name, "rsl")]) 

352 files[(pkg_name, "rsl")] = set() 

353 files[(pkg_name, "trlc")] = set() 

354 files[(pkg_name, kind)].add(file_name) 

355 except TRLC_Error: 

356 ok = False 

357 self.files_with_preamble_errors.add(file_name) 

358 

359 # Then parse all imports and add all valid links 

360 all_packages = list(self.stab.values(ast.Package)) 

361 for file_name in sorted(container): 

362 if file_name in self.files_with_preamble_errors: 

363 continue 

364 

365 parser = container[file_name] 

366 if parser.cu.package is None: 366 ↛ 367line 366 didn't jump to line 367 because the condition on line 366 was never true

367 continue 

368 pkg_name = parser.cu.package.name 

369 parser.cu.resolve_imports(self.mh, self.stab) 

370 

371 graph[(pkg_name, kind)] |= { 

372 (imported_pkg.name, kind) for imported_pkg in parser.cu.imports 

373 } 

374 

375 # A wildcard import depends on the whole subtree rooted at 

376 # the wildcard root, so the file-load closure pulls in every 

377 # descendant package. Two things are excluded: the current 

378 # package itself (a node may not depend on itself), and, 

379 # for rsl files only, the descendants of the current 

380 # package. An rsl file is always elaborated before the rsl 

381 # files of its sub-packages, so such an edge would be a 

382 # spurious cycle; see LRM.Self_Descendant_Reference, which 

383 # makes referring to those sub-packages illegal anyway. A 

384 # wildcard root that is a genuine descendant of the current 

385 # package must still create the dependency, so that a real 

386 # cycle is reported instead of silently ignored. 

387 # lobster-trace: LRM.Wildcard_Import 

388 # lobster-trace: LRM.Wildcard_Self_Cover 

389 # lobster-trace: LRM.Self_Descendant_Reference 

390 for root in parser.cu.wildcard_roots: 

391 self_cover = pkg_name == root.name or pkg_name.startswith( 

392 root.name + "." 

393 ) 

394 for other in all_packages: 

395 if other.name != root.name and not other.name.startswith( 

396 root.name + "." 

397 ): 

398 continue 

399 if other.name == pkg_name: 

400 continue 

401 if ( 

402 self_cover 

403 and kind == "rsl" 

404 and other.name.startswith(pkg_name + ".") 

405 ): 

406 continue 

407 graph[(pkg_name, kind)].add((other.name, kind)) 

408 

409 # Build the package hierarchy for nested packages. Parents are 

410 # always registered already (in the flat global table), so the 

411 # iteration order does not matter; we sort by name purely for 

412 # deterministic error output. 

413 # lobster-trace: LRM.Parent_Package_Required 

414 nested_packages = sorted( 

415 (pkg for pkg in self.stab.values(ast.Package) if "." in pkg.name), 

416 key=lambda p: p.name, 

417 ) 

418 for pkg in nested_packages: 

419 parent_name = pkg.name.rsplit(".", 1)[0] 

420 leaf_name = pkg.name.rsplit(".", 1)[1] 

421 parent_pkg = self.stab.lookup_sub_package(parent_name) 

422 if not isinstance(parent_pkg, ast.Package): 

423 ok = False 

424 self.mh.error( 

425 location=pkg.location, 

426 message=( 

427 "parent package %s of nested package %s" 

428 " has not been declared" % (parent_name, pkg.name) 

429 ), 

430 explanation=( 

431 "declare package %s (e.g. in its own " 

432 ".rsl file) before declaring %s" % (parent_name, pkg.name) 

433 ), 

434 fatal=False, 

435 ) 

436 continue 

437 try: 

438 parent_pkg.sub_packages.register_with_key(self.mh, pkg, leaf_name) 

439 except TRLC_Error: 

440 ok = False 

441 continue 

442 pkg.parent = parent_pkg 

443 # Add an implicit dependency: foo.bar rsl depends on foo rsl 

444 for kind in ("rsl", "trlc"): 

445 node = (pkg.name, kind) 

446 if node in graph: 

447 graph[node].add((parent_pkg.name, "rsl")) 

448 

449 # Build closure for our files 

450 work_list = { 

451 (parser.cu.package.name, "rsl") 

452 for parser in self.rsl_files.values() 

453 if parser.cu.package and parser.primary 

454 } 

455 work_list |= { 

456 (parser.cu.package.name, "trlc") 

457 for parser in self.trlc_files.values() 

458 if parser.cu.package and parser.primary 

459 } 

460 work_list &= set(graph) 

461 

462 required = set() 

463 while work_list: 

464 node = work_list.pop() 

465 required.add(node) 

466 work_list |= (graph[node] - required) & set(graph) 

467 

468 # Expand into actual file list and flag dependencies 

469 file_list = {file_name for node in required for file_name in files[node]} 

470 for file_name in file_list: 

471 if not self.all_files[file_name].primary: 

472 self.all_files[file_name].secondary = True 

473 

474 # Record total files that need parsing 

475 self.progress_final = len(file_list) 

476 

477 return ok 

478 

479 def parse_rsl_files(self) -> bool: 

480 # lobster-trace: LRM.Preamble 

481 # lobster-trace: LRM.RSL_File 

482 

483 ok = True 

484 

485 # Select RSL files that we should parse 

486 rsl_map = { 

487 (parser.cu.package.name, "rsl"): parser 

488 for parser in self.rsl_files.values() 

489 if parser.cu.package and (parser.primary or parser.secondary) 

490 } 

491 

492 # Parse packages that have no unparsed dependencies. Keep 

493 # doing it until we parse everything or until we have reached 

494 # a fix point (in which case we have a cycle in our 

495 # dependencies). 

496 work_list = set(rsl_map) 

497 processed = set() 

498 while work_list: 

499 candidates = { 

500 node 

501 for node in work_list 

502 if len(self.dep_graph.get(node, set()) - processed) == 0 

503 } 

504 if not candidates: 

505 # lobster-trace: LRM.Circular_Dependencies 

506 sorted_work_list = sorted(work_list) 

507 offender = rsl_map[sorted_work_list[0]] 

508 names = { 

509 rsl_map[node].cu.package.name: rsl_map[node].cu.location 

510 for node in sorted_work_list 

511 } 

512 self.mh.error( 

513 location=offender.cu.location, 

514 message=( 

515 "circular inheritance between %s" % " | ".join(sorted(names)) 

516 ), 

517 explanation="\n".join( 

518 sorted( 

519 "%s is declared in %s" 

520 % (name, self.mh.cross_file_reference(loc)) 

521 for name, loc in names.items() 

522 ) 

523 ), 

524 fatal=False, 

525 ) 

526 return False 

527 

528 for node in sorted(candidates): 

529 try: 

530 ok &= rsl_map[node].parse_rsl_file() 

531 self.signal_progress() 

532 except TRLC_Error: 

533 ok = False 

534 processed.add(node) 

535 

536 work_list -= candidates 

537 

538 return ok 

539 

540 def parse_trlc_files(self) -> bool: 

541 # lobster-trace: LRM.TRLC_File 

542 # lobster-trace: LRM.Preamble 

543 

544 ok = True 

545 

546 # Then actually parse 

547 for name in sorted(self.trlc_files): 

548 parser = self.trlc_files[name] 

549 if name in self.files_with_preamble_errors: 

550 continue 

551 if not (parser.primary or parser.secondary): 

552 continue 

553 

554 try: 

555 ok &= parser.parse_trlc_file() 

556 self.signal_progress() 

557 except TRLC_Error: 

558 ok = False 

559 

560 return ok 

561 

562 def resolve_record_references(self) -> bool: 

563 # lobster-trace: LRM.File_Parsing_References 

564 # lobster-trace: LRM.Markup_String_Late_Reference_Resolution 

565 # lobster-trace: LRM.Late_Reference_Checking 

566 ok = True 

567 for package in self.stab.values(ast.Package): 

568 for obj in package.symbols.values(ast.Record_Object): 

569 try: 

570 obj.resolve_references(self.mh) 

571 except TRLC_Error: 

572 ok = False 

573 

574 return ok 

575 

576 def verify_subpackage_distinctness(self) -> bool: 

577 """Check that sub-package leaf names are sufficiently distinct from 

578 types declared in the same parent package. 

579 

580 Must run after RSL parsing, once every package's ``symbols`` table 

581 is fully populated with types. Without this, the greedy 

582 qualified-name descent (which consults ``sub_packages`` first) 

583 would silently shadow a same-named member. Objects (declared in 

584 TRLC files) are checked separately, once they exist, by 

585 :meth:`verify_subpackage_object_distinctness`. 

586 

587 :rtype: bool 

588 """ 

589 # lobster-trace: LRM.Subpackage_Member_Distinct 

590 ok = True 

591 for pkg in self.stab.values(ast.Package): 

592 for child in pkg.sub_packages.table.values(): 

593 leaf_name = child.name.rsplit(".", 1)[1] 

594 simple_leaf = pkg.symbols.simplified_name(leaf_name) 

595 if pkg.symbols.contains_raw(simple_leaf): 

596 ok = False 

597 self.mh.error( 

598 location=child.location, 

599 message=( 

600 "sub-package %s clashes with a type or" 

601 " object of the same name in package %s" 

602 % (leaf_name, pkg.name) 

603 ), 

604 explanation=( 

605 "rename the sub-package or the " 

606 "conflicting type so that qualified" 

607 "-name resolution is unambiguous" 

608 ), 

609 fatal=False, 

610 ) 

611 return ok 

612 

613 def verify_subpackage_object_distinctness(self) -> bool: 

614 """Check that sub-package leaf names are sufficiently distinct from 

615 record objects declared in the same parent package. 

616 

617 Must run after TRLC files are parsed, since (unlike types) objects 

618 only exist from that point on. Type clashes were already reported 

619 by :meth:`verify_subpackage_distinctness`; this only looks at 

620 objects so the same clash is not reported twice. 

621 

622 :rtype: bool 

623 """ 

624 # lobster-trace: LRM.Subpackage_Member_Distinct 

625 ok = True 

626 for pkg in self.stab.values(ast.Package): 

627 for child in pkg.sub_packages.table.values(): 

628 leaf_name = child.name.rsplit(".", 1)[1] 

629 simple_leaf = pkg.symbols.simplified_name(leaf_name) 

630 existing = pkg.symbols.table.get(simple_leaf) 

631 if not isinstance(existing, ast.Record_Object): 631 ↛ 633line 631 didn't jump to line 633 because the condition on line 631 was always true

632 continue 

633 ok = False 

634 self.mh.error( 

635 location=existing.location, 

636 message=( 

637 "object %s clashes with a sub-package of" 

638 " the same name in package %s" % (existing.name, pkg.name) 

639 ), 

640 explanation=( 

641 "rename the object or the sub-package so" 

642 " that qualified-name resolution is" 

643 " unambiguous" 

644 ), 

645 fatal=False, 

646 ) 

647 return ok 

648 

649 def perform_checks(self) -> bool: 

650 # lobster-trace: LRM.Order_Of_Evaluation_Unordered 

651 ok = True 

652 for package in self.stab.values(ast.Package): 

653 for obj in package.symbols.values(ast.Record_Object): 

654 try: 

655 if not obj.perform_checks(self.mh, self.stab): 

656 ok = False 

657 except TRLC_Error: 

658 ok = False 

659 

660 return ok 

661 

662 def process(self): 

663 """Parse all registered files. 

664 

665 :return: a symbol table (or None if there were any errors) 

666 :rtype: Symbol_Table 

667 """ 

668 # lobster-trace: LRM.File_Parsing_Order 

669 # lobster-trace: LRM.File_Parsing_References 

670 

671 # Notify callback 

672 self.callback_parse_begin() 

673 self.progress_current = 0 

674 

675 # Build dependency graph 

676 ok = self.build_graph() 

677 

678 # Parse RSL files (topologically sorted, in order to deal with 

679 # dependencies) 

680 ok &= self.parse_rsl_files() 

681 

682 # Now that all type declarations are known, check that sub-package 

683 # names do not clash with members of their parent package. 

684 ok &= self.verify_subpackage_distinctness() 

685 

686 if not self.error_recovery and not ok: # pragma: no cover 

687 self.callback_parse_end() 

688 return None 

689 

690 # ───────────────────────────────────────────────────────────── 

691 # Phase 2: reprocess markdown files with RSL types available 

692 # ───────────────────────────────────────────────────────────── 

693 for _md_fname in sorted(self.trlc_files): 

694 if not _md_fname.endswith(MARKDOWN_EXTENSION): 

695 continue 

696 _md_parser = self.trlc_files[_md_fname] 

697 if not (_md_parser.primary or _md_parser.secondary): 697 ↛ 698line 697 didn't jump to line 698 because the condition on line 697 was never true

698 continue 

699 if _md_fname in self.files_with_preamble_errors: 

700 continue 

701 _md_lexer = getattr(_md_parser, "lexer", None) 

702 if isinstance(_md_lexer, MD_Lexer): 702 ↛ 693line 702 didn't jump to line 693 because the condition on line 702 was always true

703 _md_lexer.prepare_phase2(self.stab) # Rebuild tokens with types 

704 _md_parser.ct = None # Reset parser cursor 

705 _md_parser.advance() # Prime first body token 

706 

707 # Perform sanity checks (enabled by default). We only do this 

708 # if there were no errors so far. 

709 if self.lint_mode and ok: 

710 linter = lint.Linter( 

711 mh=self.mh, 

712 stab=self.stab, 

713 verify_checks=self.verify_mode, 

714 debug_vcg=self.debug_vcg, 

715 ) 

716 ok &= linter.perform_sanity_checks() 

717 # Stop here if we're not processing TRLC files. 

718 if not self.parse_trlc: # pragma: no cover 

719 self.callback_parse_end() 

720 if ok: 

721 return self.stab 

722 else: 

723 return None 

724 

725 # Parse TRLC files. Almost all the semantic analysis and name 

726 # resolution happens here, with the notable exception of resolving 

727 # record references (as we can have circularity here). 

728 trlc_files_ok = self.parse_trlc_files() 

729 

730 # Now that all objects are known, check that sub-package names do 

731 # not clash with objects declared in their parent package. This 

732 # runs even if some TRLC files failed to parse, so a distinctness 

733 # violation is still reported instead of being masked by an 

734 # unrelated parsing error. 

735 ok &= self.verify_subpackage_object_distinctness() 

736 

737 if not trlc_files_ok: # pragma: no cover 

738 self.callback_parse_end() 

739 return None 

740 

741 # Resolve record reference names and do the missing semantic 

742 # analysis. 

743 # lobster-trace: LRM.File_Parsing_References 

744 if not self.resolve_record_references(): 

745 self.callback_parse_end() 

746 return None 

747 

748 if not ok: 

749 self.callback_parse_end() 

750 return None 

751 

752 # Finally, apply user defined checks 

753 if not self.perform_checks(): 

754 self.callback_parse_end() 

755 return None 

756 

757 if self.lint_mode and ok: 

758 linter.verify_imports() 

759 

760 self.callback_parse_end() 

761 return self.stab 

762 

763 

764def trlc(): 

765 ap = argparse.ArgumentParser( 

766 prog="trlc", 

767 description="TRLC %s (Python reference implementation)" % TRLC_VERSION, 

768 epilog=("TRLC is licensed under the GPLv3. Report bugs here: %s" % BUGS_URL), 

769 allow_abbrev=False, 

770 ) 

771 og_lint = ap.add_argument_group("analysis options") 

772 og_lint.add_argument( 

773 "--no-lint", 

774 default=False, 

775 action="store_true", 

776 help="Disable additional, optional warnings.", 

777 ) 

778 og_lint.add_argument( 

779 "--skip-trlc-files", 

780 default=False, 

781 action="store_true", 

782 help=("Only process rsl files, do not process any trlc files."), 

783 ) 

784 og_lint.add_argument( 

785 "--verify", 

786 default=False, 

787 action="store_true", 

788 help=( 

789 "[EXPERIMENTAL] Attempt to statically" 

790 " verify absence of errors in user defined" 

791 " checks. Does not yet support all language" 

792 " constructs. Requires PyVCG to be " 

793 " installed." 

794 ), 

795 ) 

796 

797 og_input = ap.add_argument_group("input options") 

798 og_input.add_argument( 

799 "--include-bazel-dirs", 

800 action="store_true", 

801 help=("Enter bazel-* directories, which are excluded by default."), 

802 ) 

803 og_input.add_argument( 

804 "-I", 

805 action="append", 

806 dest="include_dirs", 

807 help=( 

808 "Add include path. Files from these" 

809 " directories are parsed only when needed." 

810 " Can be specified more than once." 

811 ), 

812 default=[], 

813 ) 

814 

815 og_output = ap.add_argument_group("output options") 

816 og_output.add_argument( 

817 "--version", 

818 default=False, 

819 action="store_true", 

820 help="Print TRLC version and exit.", 

821 ) 

822 og_output.add_argument( 

823 "--brief", 

824 default=False, 

825 action="store_true", 

826 help=( 

827 "Simpler output intended for CI. Does not" 

828 " show context or additional information," 

829 " but prints the usual summary at the end." 

830 ), 

831 ) 

832 og_output.add_argument( 

833 "--no-detailed-info", 

834 default=False, 

835 action="store_true", 

836 help=( 

837 "Do not print counter-examples and other" 

838 " supplemental information on failed" 

839 " checks. The specific values of" 

840 " counter-examples are unpredictable" 

841 " from system to system, so if you need" 

842 " perfectly reproducible output then use" 

843 " this option." 

844 ), 

845 ) 

846 og_output.add_argument( 

847 "--no-user-warnings", 

848 default=False, 

849 action="store_true", 

850 help=("Do not display any warnings from user defined checks, only errors."), 

851 ) 

852 og_output.add_argument( 

853 "--no-error-recovery", 

854 default=False, 

855 action="store_true", 

856 help=( 

857 "By default the tool attempts to recover" 

858 " from parse errors to show more errors, but" 

859 " this can occasionally generate weird" 

860 " errors. You can use this option to stop" 

861 " at the first real errors." 

862 ), 

863 ) 

864 og_output.add_argument( 

865 "--show-file-list", 

866 action="store_true", 

867 help=("If there are no errors, produce a summary naming every file processed."), 

868 ) 

869 og_output.add_argument( 

870 "--log", 

871 nargs="+", 

872 metavar=("FILE", "PREFIX"), 

873 default=None, 

874 help=( 

875 "Write all output to FILE, optionally" 

876 " strip PREFIX from file paths in" 

877 " messages. Intended for use as a" 

878 " Bazel build action." 

879 ), 

880 ) 

881 og_output.add_argument( 

882 "--error-on-warnings", 

883 action="store_true", 

884 help=("If there are warnings, return status code 1 instead of 0."),