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 subprocess 

26import sys 

27from fractions import Fraction 

28 

29from trlc import ast, lint 

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

31from trlc.lexer import Token_Stream 

32from trlc.parser import Parser 

33from trlc.version import BUGS_URL, TRLC_VERSION 

34 

35# pylint: disable=unused-import 

36try: 

37 import cvc5 

38 VCG_API_AVAILABLE = True 

39except ImportError: # pragma: no cover 

40 VCG_API_AVAILABLE = False 

41 

42 

43class Source_Manager: 

44 """Dependency and source manager for TRLC. 

45 

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

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

48 finally call the process method. 

49 

50 :param mh: The message handler to use 

51 :type mh: Message_Handler 

52 

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

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

55 to reliably recover the parse context in all cases. 

56 :type error_recovery: bool 

57 

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

59 :type lint_mode: bool 

60 

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

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

63 :type verify_mode: bool 

64 

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

66 ignored. 

67 :type parse_trlc: bool 

68 

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

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

71 graph. Requires Graphviz to be installed. 

72 :type debug_vcg: bool 

73 

74 """ 

75 def __init__(self, mh, 

76 lint_mode = True, 

77 parse_trlc = True, 

78 verify_mode = False, 

79 debug_vcg = False, 

80 error_recovery = True, 

81 cvc5_binary = None): 

82 assert isinstance(mh, Message_Handler) 

83 assert isinstance(lint_mode, bool) 

84 assert isinstance(parse_trlc, bool) 

85 assert isinstance(verify_mode, bool) 

86 assert isinstance(debug_vcg, bool) 

87 assert isinstance(cvc5_binary, str) or cvc5_binary is None 

88 

89 self.mh = mh 

90 self.mh.sm = self 

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

92 self.includes = {} 

93 self.rsl_files = {} 

94 self.trlc_files = {} 

95 self.all_files = {} 

96 self.dep_graph = {} 

97 

98 self.files_with_preamble_errors = set() 

99 

100 self.lint_mode = lint_mode 

101 self.parse_trlc = parse_trlc 

102 self.verify_mode = verify_mode 

103 self.debug_vcg = debug_vcg 

104 self.error_recovery = error_recovery 

105 self.cvc5_binary = cvc5_binary 

106 

107 self.exclude_patterns = [] 

108 self.common_root = None 

109 

110 self.progress_current = 0 

111 self.progress_final = 0 

112 

113 def callback_parse_begin(self): 

114 pass 

115 

116 def callback_parse_progress(self, progress): 

117 assert isinstance(progress, int) 

118 

119 def callback_parse_end(self): 

120 pass 

121 

122 def signal_progress(self): 

123 self.progress_current += 1 

124 if self.progress_final: 

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

126 else: # pragma: no cover 

127 progress = 100 

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

129 

130 def cross_file_reference(self, location): 

131 assert isinstance(location, Location) 

132 

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

134 return location.to_string(False) 

135 elif location.line_no is None: 

136 return os.path.relpath(location.file_name, 

137 self.common_root) 

138 else: 

139 return "%s:%u" % (os.path.relpath(location.file_name, 

140 self.common_root), 

141 location.line_no) 

142 

143 def update_common_root(self, file_name): 

144 assert isinstance(file_name, str) 

145 

146 if self.common_root is None: 

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

148 else: 

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

150 for n, (char_a, char_b) in enumerate(zip(self.common_root, 

151 new_root)): 

152 if char_a != char_b: 

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

154 break 

155 

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

157 assert os.path.isfile(file_name) 

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

159 assert isinstance(primary_file, bool) 

160 

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

162 

163 return Parser(mh = self.mh, 

164 stab = self.stab, 

165 file_name = file_name, 

166 lint_mode = self.lint_mode, 

167 error_recovery = self.error_recovery, 

168 primary_file = primary_file, 

169 lexer = lexer) 

170 

171 def register_include(self, dir_name): 

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

173 

174 :param dir_name: name of the directory 

175 :type dir_name: str 

176 :raise AssertionError: if dir_name is not a directory 

177 """ 

178 assert os.path.isdir(dir_name) 

179 

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

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

182 keep = True 

183 for exclude_pattern in self.exclude_patterns: 

184 if exclude_pattern.match(dirname): 

185 keep = False 

186 break 

187 if not keep: 

188 del dirs[n] 

189 

190 self.includes.update( 

191 {os.path.abspath(full_name): full_name 

192 for full_name in 

193 (os.path.join(path, file_name) 

194 for file_name in files 

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

196 ".trlc"))}) 

197 

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

199 """Schedule a file for parsing. 

200 

201 :param file_name: name of the file 

202 :type file_name: str 

203 :raise AssertionError: if the file does not exist 

204 :raise AssertionError: if the file is registed more than once 

205 :raise TRLC_Error: if the file is not a rsl/trlc file 

206 

207 :param file_content: content of the file 

208 :type file_content: str 

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

210 

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

212 include file, and True otherwise. 

213 :type primary: bool 

214 

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

216 :rtype: bool 

217 """ 

218 assert os.path.isfile(file_name) 

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

220 # lobster-trace: LRM.Layout 

221 

222 ok = True 

223 try: 

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

225 self.register_rsl_file(file_name, file_content, primary) 

226 elif file_name.endswith(".trlc"): 

227 self.register_trlc_file(file_name, file_content, primary) 

228 else: # pragma: no cover 

229 ok = False 

230 self.mh.error(Location(os.path.basename(file_name)), 

231 "is not a rsl or trlc file", 

232 fatal = False) 

233 except TRLC_Error: 

234 ok = False 

235 

236 return ok 

237 

238 def register_directory(self, dir_name): 

239 """Schedule a directory tree for parsing. 

240 

241 :param dir_name: name of the directory 

242 :type file_name: str 

243 :raise AssertionError: if the directory does not exist 

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

245 registered 

246 :raise TRLC_Error: on any parse errors 

247 

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

249 :rtype: bool 

250 """ 

251 assert os.path.isdir(dir_name) 

252 # lobster-trace: LRM.Layout 

253 

254 ok = True 

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

256 dirs.sort() 

257 

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

259 keep = True 

260 for exclude_pattern in self.exclude_patterns: 

261 if exclude_pattern.match(dirname): 

262 keep = False 

263 break 

264 if not keep: 

265 del dirs[n] 

266 

267 for file_name in sorted(files): 

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

269 ".trlc"): 

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

271 return ok 

272 

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

274 assert os.path.isfile(file_name) 

275 assert file_name not in self.rsl_files 

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

277 assert isinstance(primary, bool) 

278 # lobster-trace: LRM.Preamble 

279 

280 self.update_common_root(file_name) 

281 parser = self.create_parser(file_name, 

282 file_content, 

283 primary) 

284 self.rsl_files[file_name] = parser 

285 self.all_files[file_name] = parser 

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

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

288 

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

290 # lobster-trace: LRM.TRLC_File 

291 assert os.path.isfile(file_name) 

292 assert file_name not in self.trlc_files 

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

294 assert isinstance(primary, bool) 

295 # lobster-trace: LRM.Preamble 

296 

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

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

299 return 

300 

301 self.update_common_root(file_name) 

302 parser = self.create_parser(file_name, 

303 file_content, 

304 primary) 

305 self.trlc_files[file_name] = parser 

306 self.all_files[file_name] = parser 

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

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

309 

310 def build_graph(self): 

311 # lobster-trace: LRM.Preamble 

312 

313 # Register all include files not yet registered 

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

315 self.register_file(file_name, primary=False) 

316 

317 # Parse preambles and build dependency graph 

318 ok = True 

319 graph = self.dep_graph 

320 files = {} 

321 for container, kind in ((self.rsl_files, "rsl"), 

322 (self.trlc_files, "trlc")): 

323 # First parse preamble and register packages in graph 

324 for file_name in sorted(container): 

325 try: 

326 parser = container[file_name] 

327 parser.parse_preamble(kind) 

328 pkg_name = parser.cu.package.name 

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

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

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

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

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

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

335 except TRLC_Error: 

336 ok = False 

337 self.files_with_preamble_errors.add(file_name) 

338 

339 # Then parse all imports and add all valid links 

340 for file_name in sorted(container): 

341 if file_name in self.files_with_preamble_errors: 

342 continue 

343 

344 parser = container[file_name] 

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

346 continue 

347 pkg_name = parser.cu.package.name 

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

349 

350 graph[(pkg_name , kind)] |= \ 

351 {(imported_pkg.name , kind) 

352 for imported_pkg in parser.cu.imports} 

353 

354 # Build closure for our files 

355 work_list = {(parser.cu.package.name , "rsl") 

356 for parser in self.rsl_files.values() 

357 if parser.cu.package and parser.primary} 

358 work_list |= {(parser.cu.package.name , "trlc") 

359 for parser in self.trlc_files.values() 

360 if parser.cu.package and parser.primary} 

361 work_list &= set(graph) 

362 

363 required = set() 

364 while work_list: 

365 node = work_list.pop() 

366 required.add(node) 

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

368 

369 # Expand into actual file list and flag dependencies 

370 file_list = {file_name 

371 for node in required 

372 for file_name in files[node]} 

373 for file_name in file_list: 

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

375 self.all_files[file_name].secondary = True 

376 

377 # Record total files that need parsing 

378 self.progress_final = len(file_list) 

379 

380 return ok 

381 

382 def parse_rsl_files(self): 

383 # lobster-trace: LRM.Preamble 

384 # lobster-trace: LRM.RSL_File 

385 

386 ok = True 

387 

388 # Select RSL files that we should parse 

389 rsl_map = {(parser.cu.package.name , "rsl"): parser 

390 for parser in self.rsl_files.values() 

391 if parser.cu.package and (parser.primary or 

392 parser.secondary)} 

393 

394 # Parse packages that have no unparsed dependencies. Keep 

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

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

397 # dependencies). 

398 work_list = set(rsl_map) 

399 processed = set() 

400 while work_list: 

401 candidates = {node 

402 for node in work_list 

403 if len(self.dep_graph.get(node, set()) - 

404 processed) == 0} 

405 if not candidates: 

406 # lobster-trace: LRM.Circular_Dependencies 

407 sorted_work_list = sorted(work_list) 

408 offender = rsl_map[sorted_work_list[0]] 

409 names = {rsl_map[node].cu.package.name: 

410 rsl_map[node].cu.location 

411 for node in sorted_work_list[1:]} 

412 self.mh.error( 

413 location = offender.cu.location, 

414 message = ("circular inheritence between %s" % 

415 " | ".join(sorted(names))), 

416 explanation = "\n".join( 

417 sorted("%s is declared in %s" % 

418 (name, 

419 self.mh.cross_file_reference(loc)) 

420 for name, loc in names.items())), 

421 fatal = False) 

422 return False 

423 

424 for node in sorted(candidates): 

425 try: 

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

427 self.signal_progress() 

428 except TRLC_Error: 

429 ok = False 

430 processed.add(node) 

431 

432 work_list -= candidates 

433 

434 return ok 

435 

436 def parse_trlc_files(self): 

437 # lobster-trace: LRM.TRLC_File 

438 # lobster-trace: LRM.Preamble 

439 

440 ok = True 

441 

442 # Then actually parse 

443 for name in sorted(self.trlc_files): 

444 parser = self.trlc_files[name] 

445 if name in self.files_with_preamble_errors: 

446 continue 

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

448 continue 

449 

450 try: 

451 ok &= parser.parse_trlc_file() 

452 self.signal_progress() 

453 except TRLC_Error: 

454 ok = False 

455 

456 return ok 

457 

458 def resolve_record_references(self): 

459 # lobster-trace: LRM.File_Parsing_References 

460 # lobster-trace: LRM.Markup_String_Late_Reference_Resolution 

461 # lobster-trace: LRM.Late_Reference_Checking 

462 ok = True 

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

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

465 try: 

466 obj.resolve_references(self.mh) 

467 except TRLC_Error: 

468 ok = False 

469 

470 return ok 

471 

472 def perform_checks(self): 

473 # lobster-trace: LRM.Order_Of_Evaluation_Unordered 

474 ok = True 

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

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

477 try: 

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

479 ok = False 

480 except TRLC_Error: 

481 ok = False 

482 

483 return ok 

484 

485 def process(self): 

486 """Parse all registered files. 

487 

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

489 :rtype: Symbol_Table 

490 """ 

491 # lobster-trace: LRM.File_Parsing_Order 

492 # lobster-trace: LRM.File_Parsing_References 

493 

494 # Notify callback 

495 self.callback_parse_begin() 

496 self.progress_current = 0 

497 

498 # Build dependency graph 

499 ok = self.build_graph() 

500 

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

502 # dependencies) 

503 ok &= self.parse_rsl_files() 

504 

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

506 self.callback_parse_end() 

507 return None 

508 

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

510 # if there were no errors so far. 

511 if self.lint_mode and ok: 

512 linter = lint.Linter(mh = self.mh, 

513 stab = self.stab, 

514 verify_checks = self.verify_mode, 

515 debug_vcg = self.debug_vcg, 

516 cvc5_binary = self.cvc5_binary) 

517 ok &= linter.perform_sanity_checks() 

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

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

520 self.callback_parse_end() 

521 if ok: 

522 return self.stab 

523 else: 

524 return None 

525 

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

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

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

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

530 self.callback_parse_end() 

531 return None 

532 

533 # Resolve record reference names and do the missing semantic 

534 # analysis. 

535 # lobster-trace: LRM.File_Parsing_References 

536 if not self.resolve_record_references(): 

537 self.callback_parse_end() 

538 return None 

539 

540 if not ok: 

541 self.callback_parse_end() 

542 return None 

543 

544 # Finally, apply user defined checks 

545 if not self.perform_checks(): 

546 self.callback_parse_end() 

547 return None 

548 

549 if self.lint_mode and ok: 

550 linter.verify_imports() 

551 

552 self.callback_parse_end() 

553 return self.stab 

554 

555 

556def trlc(): 

557 ap = argparse.ArgumentParser( 

558 prog="trlc", 

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

560 epilog=("TRLC is licensed under the GPLv3." 

561 " Report bugs here: %s" % BUGS_URL), 

562 allow_abbrev=False, 

563 ) 

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

565 og_lint.add_argument("--no-lint", 

566 default=False, 

567 action="store_true", 

568 help="Disable additional, optional warnings.") 

569 og_lint.add_argument("--skip-trlc-files", 

570 default=False, 

571 action="store_true", 

572 help=("Only process rsl files," 

573 " do not process any trlc files.")) 

574 og_lint.add_argument("--verify", 

575 default=False, 

576 action="store_true", 

577 help=("[EXPERIMENTAL] Attempt to statically" 

578 " verify absence of errors in user defined" 

579 " checks. Does not yet support all language" 

580 " constructs. Requires PyVCG to be " 

581 " installed.")) 

582 og_lint.add_argument("--use-cvc5-binary", 

583 default=None, 

584 help=("[EXPERIMENTAL] Drive the given CVC5 solver" 

585 " with SMTLIB2 input instead of using the" 

586 " API.")) 

587 

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

589 og_input.add_argument("--include-bazel-dirs", 

590 action="store_true", 

591 help=("Enter bazel-* directories, which are" 

592 " excluded by default.")) 

593 og_input.add_argument("-I", 

594 action="append", 

595 dest="include_dirs", 

596 help=("Add include path. Files from these" 

597 " directories are parsed only when needed." 

598 " Can be specified more than once."), 

599 default=[]) 

600 

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

602 og_output.add_argument("--version", 

603 default=False, 

604 action="store_true", 

605 help="Print TRLC version and exit.") 

606 og_output.add_argument("--brief", 

607 default=False, 

608 action="store_true", 

609 help=("Simpler output intended for CI. Does not" 

610 " show context or additional information," 

611 " but prints the usual summary at the end.")) 

612 og_output.add_argument("--no-detailed-info", 

613 default=False, 

614 action="store_true", 

615 help=("Do not print counter-examples and other" 

616 " supplemental information on failed" 

617 " checks. The specific values of" 

618 " counter-examples are unpredictable" 

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

620 " perfectly reproducible output then use" 

621 " this option.")) 

622 og_output.add_argument("--no-user-warnings", 

623 default=False, 

624 action="store_true", 

625 help=("Do not display any warnings from user" 

626 " defined checks, only errors.")) 

627 og_output.add_argument("--no-error-recovery", 

628 default=False, 

629 action="store_true", 

630 help=("By default the tool attempts to recover" 

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

632 " this can occasionally generate weird" 

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

634 " at the first real errors.")) 

635 og_output.add_argument("--show-file-list", 

636 action="store_true", 

637 help=("If there are no errors, produce a summary" 

638 " naming every file processed.")) 

639 og_output.add_argument("--log", 

640 nargs = '+', 

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

642 default = None, 

643 help = ("Write all output to FILE, optionally" 

644 " strip PREFIX from file paths in" 

645 " messages. Intended for use as a" 

646 " Bazel build action.")) 

647 og_output.add_argument("--error-on-warnings", 

648 action="store_true", 

649 help=("If there are warnings, return status code" 

650 " 1 instead of 0.")) 

651 

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

653 og_debug.add_argument("--debug-dump", 

654 default=False, 

655 action="store_true", 

656 help="Dump symbol table.") 

657 og_debug.add_argument("--debug-api-dump", 

658 default=False, 

659 action="store_true", 

660 help=("Dump json of to_python_object() for all" 

661 " objects.")) 

662 og_debug.add_argument("--debug-vcg", 

663 default=False, 

664 action="store_true", 

665 help=("Emit graph and individual VCs. Requires" 

666 " graphviz to be installed.")) 

667 

668 ap.add_argument("items", 

669 nargs="*", 

670 metavar="DIR|FILE") 

671 options = ap.parse_args() 

672 

673 if options.log: 

674 if len(options.log) > 2: 

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

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

677 options.log.append(None) 

678 

679 if options.version: # pragma: no cover 

680 print(TRLC_VERSION) 

681 sys.exit(0) 

682 

683 if options.verify and not (options.use_cvc5_binary or 

684 VCG_API_AVAILABLE): # pragma: no cover 

685 ap.error("The --verify option requires the optional dependency" 

686 " CVC5 or use of the --use-cvc5-binary option") 

687 

688 if options.use_cvc5_binary: # pragma: no cover 

689 if not options.verify: 

690 ap.error("The --use-cvc5-binary requires the --verify option") 

691 try: 

692 result = subprocess.run([options.use_cvc5_binary, 

693 "--version"], 

694 check = True, 

695 capture_output = True, 

696 encoding = "UTF-8") 

697 if not result.stdout.startswith("This is cvc5"): 

698 ap.error("selected binary does not appear to be CVC5") 

699 except OSError as err: 

700 ap.error("cannot run %s: %s" % (options.use_cvc5_binary, 

701 str(err))) 

702 except subprocess.CalledProcessError: 

703 ap.error("cannot run %s" % options.use_cvc5_binary) 

704 

705 mh = Message_Handler(options.brief, 

706 not options.no_detailed_info, 

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

708 strip_prefix = options.log[1] if options.log else None) 

709 

710 if options.no_user_warnings: # pragma: no cover 

711 mh.suppress(Kind.USER_WARNING) 

712 

713 sm = Source_Manager(mh = mh, 

714 lint_mode = not options.no_lint, 

715 parse_trlc = not options.skip_trlc_files, 

716 verify_mode = options.verify, 

717 debug_vcg = options.debug_vcg, 

718 error_recovery = not options.no_error_recovery, 

719 cvc5_binary = options.use_cvc5_binary) 

720 

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

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

723 

724 # Process includes 

725 ok = True 

726 for path_name in options.include_dirs: 

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

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

729 for path_name in options.include_dirs: 

730 sm.register_include(path_name) 

731 

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

733 # given. 

734 for path_name in options.items: 

735 if not (os.path.isdir(path_name) or 

736 os.path.isfile(path_name)): # pragma: no cover 

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

738 if options.items: 

739 for path_name in options.items: 

740 if os.path.isdir(path_name): 

741 ok &= sm.register_directory(path_name) 

742 else: # pragma: no cover 

743 try: 

744 ok &= sm.register_file(path_name) 

745 except TRLC_Error: 

746 ok = False 

747 else: # pragma: no cover 

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

749 

750 if not ok: 

751 mh.close() 

752 return 1 

753 

754 if sm.process() is None: 

755 ok = False 

756 

757 if ok: 

758 if options.debug_dump: # pragma: no cover 

759 sm.stab.dump() 

760 if options.debug_api_dump: 

761 tmp = {} 

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

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

764 for key in tmp[obj.name]: 

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

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

767 

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

769 

770 total_models = len(sm.rsl_files) 

771 parsed_models = len([item 

772 for item in sm.rsl_files.values() 

773 if item.primary or item.secondary]) 

774 total_trlc = len(sm.trlc_files) 

775 parsed_trlc = len([item 

776 for item in sm.trlc_files.values() 

777 if item.primary or item.secondary]) 

778 

779 def count(parsed, total, what): 

780 rv = str(parsed) 

781 if parsed < total: 

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

783 rv += " " + what 

784 if total == 0 or total > 1: 

785 rv += "s" 

786 return rv 

787 

788 summary = "Processed %s" % count(parsed_models, 

789 total_models, 

790 "model") 

791 

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

793 summary += " and %s" % count(parsed_trlc, 

794 total_trlc, 

795 "requirement file") 

796 

797 summary += " and found" 

798 

799 if mh.errors and mh.warnings: 

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

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

802 elif mh.warnings: 

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

804 elif mh.errors: 

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

806 else: 

807 summary += " no issues" 

808 

809 if mh.suppressed: # pragma: no cover 

810 summary += " with %u supressed messages" % mh.suppressed 

811 

812 print(summary, file=mh.out) 

813 

814 if options.show_file_list and ok: # pragma: no cover 

815 def get_status(parser): 

816 if parser.primary: 

817 return "[Primary] " 

818 elif parser.secondary: 

819 return "[Included]" 

820 else: 

821 return "[Excluded]" 

822 

823 for filename in sorted(sm.rsl_files): 

824 parser = sm.rsl_files[filename] 

825 print("> %s Model %s (Package %s)" % 

826 (get_status(parser), 

827 filename, 

828 parser.cu.package.name), file=mh.out) 

829 if not options.skip_trlc_files: 

830 for filename in sorted(sm.trlc_files): 

831 parser = sm.trlc_files[filename] 

832 print("> %s Requirements %s (Package %s)" % 

833 (get_status(parser),