Coverage for trlc/trlc.py: 92%

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 registed 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 for file_name in sorted(container): 

361 if file_name in self.files_with_preamble_errors: 

362 continue 

363 

364 parser = container[file_name] 

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

366 continue 

367 pkg_name = parser.cu.package.name 

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

369 

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

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

372 } 

373 

374 # Build closure for our files 

375 work_list = { 

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

377 for parser in self.rsl_files.values() 

378 if parser.cu.package and parser.primary 

379 } 

380 work_list |= { 

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

382 for parser in self.trlc_files.values() 

383 if parser.cu.package and parser.primary 

384 } 

385 work_list &= set(graph) 

386 

387 required = set() 

388 while work_list: 

389 node = work_list.pop() 

390 required.add(node) 

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

392 

393 # Expand into actual file list and flag dependencies 

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

395 for file_name in file_list: 

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

397 self.all_files[file_name].secondary = True 

398 

399 # Record total files that need parsing 

400 self.progress_final = len(file_list) 

401 

402 return ok 

403 

404 def parse_rsl_files(self) -> bool: 

405 # lobster-trace: LRM.Preamble 

406 # lobster-trace: LRM.RSL_File 

407 

408 ok = True 

409 

410 # Select RSL files that we should parse 

411 rsl_map = { 

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

413 for parser in self.rsl_files.values() 

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

415 } 

416 

417 # Parse packages that have no unparsed dependencies. Keep 

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

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

420 # dependencies). 

421 work_list = set(rsl_map) 

422 processed = set() 

423 while work_list: 

424 candidates = { 

425 node 

426 for node in work_list 

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

428 } 

429 if not candidates: 

430 # lobster-trace: LRM.Circular_Dependencies 

431 sorted_work_list = sorted(work_list) 

432 offender = rsl_map[sorted_work_list[0]] 

433 names = { 

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

435 for node in sorted_work_list[1:] 

436 } 

437 self.mh.error( 

438 location=offender.cu.location, 

439 message=( 

440 "circular inheritence between %s" % " | ".join(sorted(names)) 

441 ), 

442 explanation="\n".join( 

443 sorted( 

444 "%s is declared in %s" 

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

446 for name, loc in names.items() 

447 ) 

448 ), 

449 fatal=False, 

450 ) 

451 return False 

452 

453 for node in sorted(candidates): 

454 try: 

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

456 self.signal_progress() 

457 except TRLC_Error: 

458 ok = False 

459 processed.add(node) 

460 

461 work_list -= candidates 

462 

463 return ok 

464 

465 def parse_trlc_files(self) -> bool: 

466 # lobster-trace: LRM.TRLC_File 

467 # lobster-trace: LRM.Preamble 

468 

469 ok = True 

470 

471 # Then actually parse 

472 for name in sorted(self.trlc_files): 

473 parser = self.trlc_files[name] 

474 if name in self.files_with_preamble_errors: 

475 continue 

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

477 continue 

478 

479 try: 

480 ok &= parser.parse_trlc_file() 

481 self.signal_progress() 

482 except TRLC_Error: 

483 ok = False 

484 

485 return ok 

486 

487 def resolve_record_references(self) -> bool: 

488 # lobster-trace: LRM.File_Parsing_References 

489 # lobster-trace: LRM.Markup_String_Late_Reference_Resolution 

490 # lobster-trace: LRM.Late_Reference_Checking 

491 ok = True 

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

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

494 try: 

495 obj.resolve_references(self.mh) 

496 except TRLC_Error: 

497 ok = False 

498 

499 return ok 

500 

501 def perform_checks(self) -> bool: 

502 # lobster-trace: LRM.Order_Of_Evaluation_Unordered 

503 ok = True 

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

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

506 try: 

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

508 ok = False 

509 except TRLC_Error: 

510 ok = False 

511 

512 return ok 

513 

514 def process(self): 

515 """Parse all registered files. 

516 

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

518 :rtype: Symbol_Table 

519 """ 

520 # lobster-trace: LRM.File_Parsing_Order 

521 # lobster-trace: LRM.File_Parsing_References 

522 

523 # Notify callback 

524 self.callback_parse_begin() 

525 self.progress_current = 0 

526 

527 # Build dependency graph 

528 ok = self.build_graph() 

529 

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

531 # dependencies) 

532 ok &= self.parse_rsl_files() 

533 

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

535 self.callback_parse_end() 

536 return None 

537 

538 # ───────────────────────────────────────────────────────────── 

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

540 # ───────────────────────────────────────────────────────────── 

541 for _md_fname in sorted(self.trlc_files): 

542 if not _md_fname.endswith(MARKDOWN_EXTENSION): 

543 continue 

544 _md_parser = self.trlc_files[_md_fname] 

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

546 continue 

547 if _md_fname in self.files_with_preamble_errors: 547 ↛ 548line 547 didn't jump to line 548 because the condition on line 547 was never true

548 continue 

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

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

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

552 _md_parser.ct = None # Reset parser cursor 

553 _md_parser.advance() # Prime first body token 

554 

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

556 # if there were no errors so far. 

557 if self.lint_mode and ok: 

558 linter = lint.Linter( 

559 mh=self.mh, 

560 stab=self.stab, 

561 verify_checks=self.verify_mode, 

562 debug_vcg=self.debug_vcg, 

563 ) 

564 ok &= linter.perform_sanity_checks() 

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

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

567 self.callback_parse_end() 

568 if ok: 

569 return self.stab 

570 else: 

571 return None 

572 

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

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

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

576 if not self.parse_trlc_files(): # pragma: no cover 

577 self.callback_parse_end() 

578 return None 

579 

580 # Resolve record reference names and do the missing semantic 

581 # analysis. 

582 # lobster-trace: LRM.File_Parsing_References 

583 if not self.resolve_record_references(): 

584 self.callback_parse_end() 

585 return None 

586 

587 if not ok: 

588 self.callback_parse_end() 

589 return None 

590 

591 # Finally, apply user defined checks 

592 if not self.perform_checks(): 

593 self.callback_parse_end() 

594 return None 

595 

596 if self.lint_mode and ok: 

597 linter.verify_imports() 

598 

599 self.callback_parse_end() 

600 return self.stab 

601 

602 

603def trlc(): 

604 ap = argparse.ArgumentParser( 

605 prog="trlc", 

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

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

608 allow_abbrev=False, 

609 ) 

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

611 og_lint.add_argument( 

612 "--no-lint", 

613 default=False, 

614 action="store_true", 

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

616 ) 

617 og_lint.add_argument( 

618 "--skip-trlc-files", 

619 default=False, 

620 action="store_true", 

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

622 ) 

623 og_lint.add_argument( 

624 "--verify", 

625 default=False, 

626 action="store_true", 

627 help=( 

628 "[EXPERIMENTAL] Attempt to statically" 

629 " verify absence of errors in user defined" 

630 " checks. Does not yet support all language" 

631 " constructs. Requires PyVCG to be " 

632 " installed." 

633 ), 

634 ) 

635 

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

637 og_input.add_argument( 

638 "--include-bazel-dirs", 

639 action="store_true", 

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

641 ) 

642 og_input.add_argument( 

643 "-I", 

644 action="append", 

645 dest="include_dirs", 

646 help=( 

647 "Add include path. Files from these" 

648 " directories are parsed only when needed." 

649 " Can be specified more than once." 

650 ), 

651 default=[], 

652 ) 

653 

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

655 og_output.add_argument( 

656 "--version", 

657 default=False, 

658 action="store_true", 

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

660 ) 

661 og_output.add_argument( 

662 "--brief", 

663 default=False, 

664 action="store_true", 

665 help=( 

666 "Simpler output intended for CI. Does not" 

667 " show context or additional information," 

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

669 ), 

670 ) 

671 og_output.add_argument( 

672 "--no-detailed-info", 

673 default=False, 

674 action="store_true", 

675 help=( 

676 "Do not print counter-examples and other" 

677 " supplemental information on failed" 

678 " checks. The specific values of" 

679 " counter-examples are unpredictable" 

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

681 " perfectly reproducible output then use" 

682 " this option." 

683 ), 

684 ) 

685 og_output.add_argument( 

686 "--no-user-warnings", 

687 default=False, 

688 action="store_true", 

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

690 ) 

691 og_output.add_argument( 

692 "--no-error-recovery", 

693 default=False, 

694 action="store_true", 

695 help=( 

696 "By default the tool attempts to recover" 

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

698 " this can occasionally generate weird" 

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

700 " at the first real errors." 

701 ), 

702 ) 

703 og_output.add_argument( 

704 "--show-file-list", 

705 action="store_true", 

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

707 ) 

708 og_output.add_argument( 

709 "--log", 

710 nargs="+", 

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

712 default=None, 

713 help=( 

714 "Write all output to FILE, optionally" 

715 " strip PREFIX from file paths in" 

716 " messages. Intended for use as a" 

717 " Bazel build action." 

718 ), 

719 ) 

720 og_output.add_argument( 

721 "--error-on-warnings", 

722 action="store_true", 

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

724 ) 

725 

726 og_debug = ap.add_argument_group("debug options") 

727 og_debug.add_argument( 

728 "--debug-dump", default=False, action="store_true", help="Dump symbol table." 

729 ) 

730 og_debug.add_argument( 

731 "--debug-api-dump", 

732 default=False, 

733 action="store_true", 

734 help=("Dump json of to_python_object() for all objects."), 

735 ) 

736 og_debug.add_argument( 

737 "--debug-vcg", 

738 default=False, 

739 action="store_true", 

740 help=("Emit graph and individual VCs. Requires graphviz to be installed."), 

741 ) 

742 

743 ap.add_argument("items", nargs="*", metavar="DIR|FILE") 

744 options = ap.parse_args() 

745 

746 if options.log: 

747 if len(options.log) > 2: 

748 ap.error("--log accepts at most 2 values: FILE and optionally PREFIX") 

749 if len(options.log) == 1: 

750 options.log.append(None) 

751 

752 if options.version: # pragma: no cover 

753 print(TRLC_VERSION) 

754 sys.exit(0) 

755 

756 if options.verify and not VCG_API_AVAILABLE: # pragma: no cover 

757 ap.error("The --verify option requires the optional dependency CVC5") 

758 

759 mh = Message_Handler( 

760 options.brief, 

761 not options.no_detailed_info, 

762 out_path=options.log[0] if options.log else None, 

763 strip_prefix=options.log[1] if options.log else None, 

764 ) 

765 

766 if options.no_user_warnings: # pragma: no cover 

767 mh.suppress(Kind.USER_WARNING) 

768 

769 sm = Source_Manager( 

770 mh=mh, 

771 lint_mode=not options.no_lint, 

772 parse_trlc=not options.skip_trlc_files, 

773 verify_mode=options.verify, 

774 debug_vcg=options.debug_vcg, 

775 error_recovery=not options.no_error_recovery, 

776 ) 

777 

778 if not options.include_bazel_dirs: # pragma: no cover 

779 sm.exclude_patterns.append(re.compile("^bazel-.*$")) 

780 

781 # Process includes 

782 ok = True 

783 for path_name in options.include_dirs: 

784 if not os.path.isdir(path_name): 784 ↛ 785line 784 didn't jump to line 785 because the condition on line 784 was never true

785 ap.error("include path %s is not a directory" % path_name) 

786 for path_name in options.include_dirs: 

787 sm.register_include(path_name) 

788 

789 # Process input files, defaulting to the current directory if none 

790 # given. 

791 for path_name in options.items: 

792 if not ( 

793 os.path.isdir(path_name) or os.path.isfile(path_name) 

794 ): # pragma: no cover 

795 ap.error("%s is not a file or directory" % path_name) 

796 if options.items: 

797 for path_name in options.items: 

798 if os.path.isdir(path_name): 

799 ok &= sm.register_directory(path_name) 

800 else: # pragma: no cover 

801 try: 

802 ok &= sm.register_file(path_name) 

803 except TRLC_Error: 

804 ok = False 

805 else: # pragma: no cover 

806 ok &= sm.register_directory(".") 

807 

808 if not ok: 

809 mh.close() 

810 return 1 

811 

812 if sm.process() is None: 

813 ok = False 

814 

815 if ok: 

816 if options.debug_dump: # pragma: no cover 

817 sm.stab.dump() 

818 if options.debug_api_dump: 

819 tmp = {} 

820 for obj in sm.stab.iter_record_objects(): 

821 tmp[obj.name] = obj.to_python_dict() 

822 for key in tmp[obj.name]: 

823 if isinstance(tmp[obj.name][key], Fraction): 823 ↛ 824line 823 didn't jump to line 824 because the condition on line 823 was never true

824 tmp[obj.name][key] = float(tmp[obj.name][key]) 

825 

826 print(json.dumps(tmp, indent=2, sort_keys=True), file=mh.out) 

827 

828 total_models = len(sm.rsl_files) 

829 parsed_models = len( 

830 [item for item in sm.rsl_files.values() if item.primary or item.secondary] 

831 ) 

832 total_trlc = len(sm.trlc_files) 

833 parsed_trlc = len( 

834 [item for item in sm.trlc_files.values() if item.primary or item.secondary] 

835 ) 

836 

837 def count(parsed, total, what): 

838 rv = str(parsed) 

839 if parsed < total: 

840 rv += " (of %u)" % total 

841 rv += " " + what 

842 if total == 0 or total > 1: 

843 rv += "s" 

844 return rv 

845 

846 summary = "Processed %s" % count(parsed_models, total_models, "model") 

847 

848 if not options.skip_trlc_files: # pragma: no cover 

849 summary += " and %s" % count(parsed_trlc, total_trlc, "requirement file") 

850 

851 summary += " and found" 

852 

853 if mh.errors and mh.warnings: 

854 summary += " %s" % count(mh.warnings, mh.warnings, "warning") 

855 summary += " and %s" % count(mh.errors, mh.errors, "error") 

856 elif mh.warnings: 

857 summary += " %s" % count(mh.warnings, mh.warnings, "warning")