Coverage for trlc/trlc.py: 95%
465 statements
« prev ^ index » next coverage.py v7.16.2, created at 2026-10-23 10:23 +0000
1#!/usr/bin/env python3
2#
3# TRLC - Treat Requirements Like Code
4# Copyright (C) 2022-2023 Bayerische Motoren Werke Aktiengesellschaft (BMW AG)
5#
6# This file is part of the TRLC Python Reference Implementation.
7#
8# TRLC is free software: you can redistribute it and/or modify it
9# under the terms of the GNU General Public License as published by
10# the Free Software Foundation, either version 3 of the License, or
11# (at your option) any later version.
12#
13# TRLC is distributed in the hope that it will be useful, but WITHOUT
14# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
15# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
16# License for more details.
17#
18# You should have received a copy of the GNU General Public License
19# along with TRLC. If not, see <https://www.gnu.org/licenses/>.
21import argparse
22import json
23import os
24import re
25import sys
26from fractions import Fraction
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
36# pylint: disable=unused-import
37try:
38 import cvc5
40 VCG_API_AVAILABLE = True
41except ImportError: # pragma: no cover
42 VCG_API_AVAILABLE = False
44MARKDOWN_EXTENSION = ".trlc.md"
47class Source_Manager:
48 """Dependency and source manager for TRLC.
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.
54 :param mh: The message handler to use
55 :type mh: Message_Handler
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
62 :param lint_mode: If true enables additional warning messages.
63 :type lint_mode: bool
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
69 :param parse_trlc: If true parses trlc files, otherwise they are \
70 ignored.
71 :type parse_trlc: bool
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
78 """
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)
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 = {}
104 self.files_with_preamble_errors = set()
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
112 self.exclude_patterns = []
113 self.excluded_paths = set()
114 self.common_root = None
116 self.progress_current = 0
117 self.progress_final = 0
119 def callback_parse_begin(self):
120 pass
122 def callback_parse_progress(self, progress):
123 assert isinstance(progress, int)
125 def callback_parse_end(self):
126 pass
128 def signal_progress(self):
129 self.progress_current += 1
130 if self.progress_final:
131 progress = (self.progress_current * 100) // self.progress_final
132 else: # pragma: no cover
133 progress = 100
134 self.callback_parse_progress(min(progress, 100))
136 def cross_file_reference(self, location):
137 assert isinstance(location, Location)
139 if self.common_root is None: 139 ↛ 140line 139 didn't jump to line 140 because the condition on line 139 was never true
140 return location.to_string(False)
141 elif location.line_no is None:
142 return os.path.relpath(location.file_name, self.common_root)
143 else:
144 return "%s:%u" % (
145 os.path.relpath(location.file_name, self.common_root),
146 location.line_no,
147 )
149 def update_common_root(self, file_name):
150 assert isinstance(file_name, str)
152 if self.common_root is None:
153 self.common_root = os.path.dirname(os.path.abspath(file_name))
154 else:
155 new_root = os.path.dirname(os.path.abspath(file_name))
156 for n, (char_a, char_b) in enumerate(zip(self.common_root, new_root)):
157 if char_a != char_b:
158 self.common_root = self.common_root[0:n]
159 break
161 def create_parser(self, file_name, file_content=None, primary_file=True):
162 assert os.path.isfile(file_name)
163 assert isinstance(file_content, str) or file_content is None
164 assert isinstance(primary_file, bool)
166 if file_name.endswith(MARKDOWN_EXTENSION):
167 lexer = MD_Lexer(self.mh, file_name, file_content)
168 return TrlcMarkdownParser(
169 mh=self.mh,
170 stab=self.stab,
171 file_name=file_name,
172 lint_mode=self.lint_mode,
173 error_recovery=self.error_recovery,
174 primary_file=primary_file,
175 lexer=lexer,
176 )
178 lexer = Token_Stream(self.mh, file_name, file_content)
180 return Parser(
181 mh=self.mh,
182 stab=self.stab,
183 file_name=file_name,
184 lint_mode=self.lint_mode,
185 error_recovery=self.error_recovery,
186 primary_file=primary_file,
187 lexer=lexer,
188 )
190 def exclude_path(self, path_name):
191 """Exclude a file or directory from processing.
193 Anything under an excluded directory is skipped as well.
195 :param path_name: name of the file or directory to exclude
196 :type path_name: str
197 """
198 if not isinstance(path_name, str):
199 raise TypeError("path_name must be a string")
200 self.excluded_paths.add(os.path.normpath(os.path.abspath(path_name)))
202 def is_path_excluded(self, path_name):
203 """Check if a file or directory was excluded.
205 :param path_name: name of the file or directory to check
206 :type path_name: str
207 :rtype: bool
208 """
209 if not isinstance(path_name, str):
210 raise TypeError("path_name must be a string")
211 abs_path = os.path.normpath(os.path.abspath(path_name))
212 return any(
213 abs_path == excluded or abs_path.startswith(excluded + os.sep)
214 for excluded in self.excluded_paths
215 )
217 def register_include(self, dir_name):
218 """Make contents of a directory available for automatic inclusion
220 :param dir_name: name of the directory
221 :type dir_name: str
222 :raise AssertionError: if dir_name is not a directory
223 :return: true if no explicitly excluded paths were encountered
224 :rtype: bool
225 """
226 assert os.path.isdir(dir_name)
228 for path, dirs, files in os.walk(dir_name):
229 for n, dirname in reversed(list(enumerate(dirs))):
230 keep = True
231 for exclude_pattern in self.exclude_patterns:
232 if exclude_pattern.match(dirname): 232 ↛ 233line 232 didn't jump to line 233 because the condition on line 232 was never true
233 keep = False
234 break
235 full_name = os.path.join(path, dirname)
236 if keep and self.is_path_excluded(full_name):
237 self.mh.error(
238 Location(full_name),
239 "include directory contains an excluded path",
240 explanation=(
241 "remove this path from the exclude list or remove "
242 "the include directory"
243 ),
244 fatal=False,
245 )
246 return False
247 if not keep: 247 ↛ 248line 247 didn't jump to line 248 because the condition on line 247 was never true
248 del dirs[n]
250 for file_name in files:
251 full_name = os.path.join(path, file_name)
252 if os.path.splitext(file_name)[1] not in (".rsl", ".trlc"): 252 ↛ 253line 252 didn't jump to line 253 because the condition on line 252 was never true
253 continue
254 if self.is_path_excluded(full_name):
255 self.mh.error(
256 Location(full_name),
257 "include directory contains an excluded path",
258 explanation=(
259 "remove this path from the exclude list or remove "
260 "the include directory"
261 ),
262 fatal=False,
263 )
264 return False
265 self.includes[os.path.abspath(full_name)] = full_name
267 return True
269 def register_file(self, file_name, file_content=None, primary=True):
270 """Schedule a file for parsing.
272 :param file_name: name of the file
273 :type file_name: str
274 :raise AssertionError: if the file does not exist
275 :raise AssertionError: if the file is registered more than once
276 :raise TRLC_Error: if the file is not a rsl, trlc or trlc.md file
278 :param file_content: content of the file
279 :type file_content: str
280 :raise AssertionError: if the content is not of type string
282 :param primary: should be False if the file is a potential \
283 include file, and True otherwise.
284 :type primary: bool
286 :return: true if the file could be registered without issues
287 :rtype: bool
288 """
289 assert os.path.isfile(file_name)
290 assert isinstance(file_content, str) or file_content is None
291 # lobster-trace: LRM.Layout
293 try:
294 if file_name.endswith(".rsl"):
295 self.register_rsl_file(file_name, file_content, primary)
296 elif file_name.endswith(".trlc") or file_name.endswith(MARKDOWN_EXTENSION):
297 self.register_trlc_file(file_name, file_content, primary)
298 else: # pragma: no cover
299 self.mh.error(
300 Location(os.path.basename(file_name)),
301 "is not a rsl, trlc or trlc.md file",
302 fatal=False,
303 )
304 return False
306 except TRLC_Error:
307 return False
309 return True
311 def register_directory(self, dir_name):
312 """Schedule a directory tree for parsing.
314 :param dir_name: name of the directory
315 :type file_name: str
316 :raise AssertionError: if the directory does not exist
317 :raise AssertionError: if any item in the directory is already \
318 registered
319 :raise TRLC_Error: on any parse errors
321 :return: true if the directory could be registered without issues
322 :rtype: bool
323 """
324 assert os.path.isdir(dir_name)
325 # lobster-trace: LRM.Layout
327 ok = True
328 for path, dirs, files in os.walk(dir_name):
329 dirs.sort()
331 for n, dirname in reversed(list(enumerate(dirs))):
332 keep = True
333 for exclude_pattern in self.exclude_patterns:
334 if exclude_pattern.match(dirname):
335 keep = False
336 break
337 if keep and self.is_path_excluded(os.path.join(path, dirname)):
338 keep = False
339 if not keep:
340 del dirs[n]
342 for file_name in sorted(files):
343 full_name = os.path.join(path, file_name)
344 if self.is_path_excluded(full_name):
345 continue
346 if os.path.splitext(file_name)[1] in (
347 ".rsl",
348 ".trlc",
349 ) or file_name.endswith(MARKDOWN_EXTENSION):
350 ok &= self.register_file(full_name)
351 return ok
353 def register_rsl_file(self, file_name, file_content=None, primary=True):
354 assert os.path.isfile(file_name)
355 assert file_name not in self.rsl_files
356 assert isinstance(file_content, str) or file_content is None
357 assert isinstance(primary, bool)
358 # lobster-trace: LRM.Preamble
360 self.update_common_root(file_name)
361 parser = self.create_parser(file_name, file_content, primary)
362 self.rsl_files[file_name] = parser
363 self.all_files[file_name] = parser
364 if os.path.abspath(file_name) in self.includes:
365 del self.includes[os.path.abspath(file_name)]
367 def register_trlc_file(self, file_name, file_content=None, primary=True):
368 # lobster-trace: LRM.TRLC_File
369 assert os.path.isfile(file_name)
370 assert file_name not in self.trlc_files
371 assert isinstance(file_content, str) or file_content is None
372 assert isinstance(primary, bool)
373 # lobster-trace: LRM.Preamble
375 if not self.parse_trlc: # pragma: no cover
376 # Not executed as process should exit before we attempt this.
377 return
379 self.update_common_root(file_name)
380 parser = self.create_parser(file_name, file_content, primary)
381 self.trlc_files[file_name] = parser
382 self.all_files[file_name] = parser
383 if os.path.abspath(file_name) in self.includes:
384 del self.includes[os.path.abspath(file_name)]
386 def build_graph(self):
387 # lobster-trace: LRM.Preamble
389 # Register all include files not yet registered
390 for file_name in list(sorted(self.includes.values())):
391 self.register_file(file_name, primary=False)
393 # Parse preambles and build dependency graph
394 ok = True
395 graph = self.dep_graph
396 files = {}
397 for container, kind in ((self.rsl_files, "rsl"), (self.trlc_files, "trlc")):
398 # First parse preamble and register packages in graph
399 for file_name in sorted(container):
400 try:
401 parser = container[file_name]
402 parser.parse_preamble(kind)
403 pkg_name = parser.cu.package.name
404 if (pkg_name, "rsl") not in graph:
405 graph[(pkg_name, "rsl")] = set()
406 graph[(pkg_name, "trlc")] = set([(pkg_name, "rsl")])
407 files[(pkg_name, "rsl")] = set()
408 files[(pkg_name, "trlc")] = set()
409 files[(pkg_name, kind)].add(file_name)
410 except TRLC_Error:
411 ok = False
412 self.files_with_preamble_errors.add(file_name)
414 # Then parse all imports and add all valid links
415 all_packages = list(self.stab.values(ast.Package))
416 for file_name in sorted(container):
417 if file_name in self.files_with_preamble_errors:
418 continue
420 parser = container[file_name]
421 if parser.cu.package is None: 421 ↛ 422line 421 didn't jump to line 422 because the condition on line 421 was never true
422 continue
423 pkg_name = parser.cu.package.name
424 parser.cu.resolve_imports(self.mh, self.stab)
426 graph[(pkg_name, kind)] |= {
427 (imported_pkg.name, kind) for imported_pkg in parser.cu.imports
428 }
430 # A wildcard import depends on the whole subtree rooted at
431 # the wildcard root, so the file-load closure pulls in every
432 # descendant package. Two things are excluded: the current
433 # package itself (a node may not depend on itself), and,
434 # for rsl files only, the descendants of the current
435 # package. An rsl file is always elaborated before the rsl
436 # files of its sub-packages, so such an edge would be a
437 # spurious cycle; see LRM.Self_Descendant_Reference, which
438 # makes referring to those sub-packages illegal anyway. A
439 # wildcard root that is a genuine descendant of the current
440 # package must still create the dependency, so that a real
441 # cycle is reported instead of silently ignored.
442 # lobster-trace: LRM.Wildcard_Import
443 # lobster-trace: LRM.Wildcard_Self_Cover
444 # lobster-trace: LRM.Self_Descendant_Reference
445 for root in parser.cu.wildcard_roots:
446 self_cover = pkg_name == root.name or pkg_name.startswith(
447 root.name + "."
448 )
449 for other in all_packages:
450 if other.name != root.name and not other.name.startswith(
451 root.name + "."
452 ):
453 continue
454 if other.name == pkg_name:
455 continue
456 if (
457 self_cover
458 and kind == "rsl"
459 and other.name.startswith(pkg_name + ".")
460 ):
461 continue
462 graph[(pkg_name, kind)].add((other.name, kind))
464 # Build the package hierarchy for nested packages. Parents are
465 # always registered already (in the flat global table), so the
466 # iteration order does not matter; we sort by name purely for
467 # deterministic error output.
468 # lobster-trace: LRM.Parent_Package_Required
469 nested_packages = sorted(
470 (pkg for pkg in self.stab.values(ast.Package) if "." in pkg.name),
471 key=lambda p: p.name,
472 )
473 for pkg in nested_packages:
474 parent_name = pkg.name.rsplit(".", 1)[0]
475 leaf_name = pkg.name.rsplit(".", 1)[1]
476 parent_pkg = self.stab.lookup_sub_package(parent_name)
477 if not isinstance(parent_pkg, ast.Package):
478 ok = False
479 self.mh.error(
480 location=pkg.location,
481 message=(
482 "parent package %s of nested package %s"
483 " has not been declared" % (parent_name, pkg.name)
484 ),
485 explanation=(
486 "declare package %s (e.g. in its own "
487 ".rsl file) before declaring %s" % (parent_name, pkg.name)
488 ),
489 fatal=False,
490 )
491 continue
492 try:
493 parent_pkg.sub_packages.register_with_key(self.mh, pkg, leaf_name)
494 except TRLC_Error:
495 ok = False
496 continue
497 pkg.parent = parent_pkg
498 # Add an implicit dependency: foo.bar rsl depends on foo rsl
499 for kind in ("rsl", "trlc"):
500 node = (pkg.name, kind)
501 if node in graph:
502 graph[node].add((parent_pkg.name, "rsl"))
504 # Build closure for our files
505 work_list = {
506 (parser.cu.package.name, "rsl")
507 for parser in self.rsl_files.values()
508 if parser.cu.package and parser.primary
509 }
510 work_list |= {
511 (parser.cu.package.name, "trlc")
512 for parser in self.trlc_files.values()
513 if parser.cu.package and parser.primary
514 }
515 work_list &= set(graph)
517 required = set()
518 while work_list:
519 node = work_list.pop()
520 required.add(node)
521 work_list |= (graph[node] - required) & set(graph)
523 # Expand into actual file list and flag dependencies
524 file_list = {file_name for node in required for file_name in files[node]}
525 for file_name in file_list:
526 if not self.all_files[file_name].primary:
527 self.all_files[file_name].secondary = True
529 # Record total files that need parsing
530 self.progress_final = len(file_list)
532 return ok
534 def parse_rsl_files(self) -> bool:
535 # lobster-trace: LRM.Preamble
536 # lobster-trace: LRM.RSL_File
538 ok = True
540 # Select RSL files that we should parse
541 rsl_map = {
542 (parser.cu.package.name, "rsl"): parser
543 for parser in self.rsl_files.values()
544 if parser.cu.package and (parser.primary or parser.secondary)
545 }
547 # Parse packages that have no unparsed dependencies. Keep
548 # doing it until we parse everything or until we have reached
549 # a fix point (in which case we have a cycle in our
550 # dependencies).
551 work_list = set(rsl_map)
552 processed = set()
553 while work_list:
554 candidates = {
555 node
556 for node in work_list
557 if len(self.dep_graph.get(node, set()) - processed) == 0
558 }
559 if not candidates:
560 # lobster-trace: LRM.Circular_Dependencies
561 sorted_work_list = sorted(work_list)
562 offender = rsl_map[sorted_work_list[0]]
563 names = {
564 rsl_map[node].cu.package.name: rsl_map[node].cu.location
565 for node in sorted_work_list
566 }
567 self.mh.error(
568 location=offender.cu.location,
569 message=(
570 "circular inheritance between %s" % " | ".join(sorted(names))
571 ),
572 explanation="\n".join(
573 sorted(
574 "%s is declared in %s"
575 % (name, self.mh.cross_file_reference(loc))
576 for name, loc in names.items()
577 )
578 ),
579 fatal=False,
580 )
581 return False
583 for node in sorted(candidates):
584 try:
585 ok &= rsl_map[node].parse_rsl_file()
586 self.signal_progress()
587 except TRLC_Error:
588 ok = False
589 processed.add(node)
591 work_list -= candidates
593 return ok
595 def parse_trlc_files(self) -> bool:
596 # lobster-trace: LRM.TRLC_File
597 # lobster-trace: LRM.Preamble
599 ok = True
601 # Then actually parse
602 for name in sorted(self.trlc_files):
603 parser = self.trlc_files[name]
604 if name in self.files_with_preamble_errors:
605 continue
606 if not (parser.primary or parser.secondary):
607 continue
609 try:
610 ok &= parser.parse_trlc_file()
611 self.signal_progress()
612 except TRLC_Error:
613 ok = False
615 return ok
617 def resolve_record_references(self) -> bool:
618 # lobster-trace: LRM.File_Parsing_References
619 # lobster-trace: LRM.Markup_String_Late_Reference_Resolution
620 # lobster-trace: LRM.Late_Reference_Checking
621 ok = True
622 for package in self.stab.values(ast.Package):
623 for obj in package.symbols.values(ast.Record_Object):
624 try:
625 obj.resolve_references(self.mh)
626 except TRLC_Error:
627 ok = False
629 return ok
631 def verify_subpackage_distinctness(self) -> bool:
632 """Check that sub-package leaf names are sufficiently distinct from
633 types declared in the same parent package.
635 Must run after RSL parsing, once every package's ``symbols`` table
636 is fully populated with types. Without this, the greedy
637 qualified-name descent (which consults ``sub_packages`` first)
638 would silently shadow a same-named member. Objects (declared in
639 TRLC files) are checked separately, once they exist, by
640 :meth:`verify_subpackage_object_distinctness`.
642 :rtype: bool
643 """
644 # lobster-trace: LRM.Subpackage_Member_Distinct
645 ok = True
646 for pkg in self.stab.values(ast.Package):
647 for child in pkg.sub_packages.table.values():
648 leaf_name = child.name.rsplit(".", 1)[1]
649 simple_leaf = pkg.symbols.simplified_name(leaf_name)
650 if pkg.symbols.contains_raw(simple_leaf):
651 ok = False
652 self.mh.error(
653 location=child.location,
654 message=(
655 "sub-package %s clashes with a type or"
656 " object of the same name in package %s"
657 % (leaf_name, pkg.name)
658 ),
659 explanation=(
660 "rename the sub-package or the "
661 "conflicting type so that qualified"
662 "-name resolution is unambiguous"
663 ),
664 fatal=False,
665 )
666 return ok
668 def verify_subpackage_object_distinctness(self) -> bool:
669 """Check that sub-package leaf names are sufficiently distinct from
670 record objects declared in the same parent package.
672 Must run after TRLC files are parsed, since (unlike types) objects
673 only exist from that point on. Type clashes were already reported
674 by :meth:`verify_subpackage_distinctness`; this only looks at
675 objects so the same clash is not reported twice.
677 :rtype: bool
678 """
679 # lobster-trace: LRM.Subpackage_Member_Distinct
680 ok = True
681 for pkg in self.stab.values(ast.Package):
682 for child in pkg.sub_packages.table.values():
683 leaf_name = child.name.rsplit(".", 1)[1]
684 simple_leaf = pkg.symbols.simplified_name(leaf_name)
685 existing = pkg.symbols.table.get(simple_leaf)
686 if not isinstance(existing, ast.Record_Object): 686 ↛ 688line 686 didn't jump to line 688 because the condition on line 686 was always true
687 continue
688 ok = False
689 self.mh.error(
690 location=existing.location,
691 message=(
692 "object %s clashes with a sub-package of"
693 " the same name in package %s" % (existing.name, pkg.name)
694 ),
695 explanation=(
696 "rename the object or the sub-package so"
697 " that qualified-name resolution is"
698 " unambiguous"
699 ),
700 fatal=False,
701 )
702 return ok
704 def perform_checks(self) -> bool:
705 # lobster-trace: LRM.Order_Of_Evaluation_Unordered
706 ok = True
707 for package in self.stab.values(ast.Package):
708 for obj in package.symbols.values(ast.Record_Object):
709 try:
710 if not obj.perform_checks(self.mh, self.stab):
711 ok = False
712 except TRLC_Error:
713 ok = False
715 return ok
717 def process(self):
718 """Parse all registered files.
720 :return: a symbol table (or None if there were any errors)
721 :rtype: Symbol_Table
722 """
723 # lobster-trace: LRM.File_Parsing_Order
724 # lobster-trace: LRM.File_Parsing_References
726 # Notify callback
727 self.callback_parse_begin()
728 self.progress_current = 0
730 # Build dependency graph
731 ok = self.build_graph()
733 # Parse RSL files (topologically sorted, in order to deal with
734 # dependencies)
735 ok &= self.parse_rsl_files()
737 # Now that all type declarations are known, check that sub-package
738 # names do not clash with members of their parent package.
739 ok &= self.verify_subpackage_distinctness()
741 if not self.error_recovery and not ok: # pragma: no cover
742 self.callback_parse_end()
743 return None
745 # ─────────────────────────────────────────────────────────────
746 # Phase 2: reprocess markdown files with RSL types available
747 # ─────────────────────────────────────────────────────────────
748 for _md_fname in sorted(self.trlc_files):
749 if not _md_fname.endswith(MARKDOWN_EXTENSION):
750 continue
751 _md_parser = self.trlc_files[_md_fname]
752 if not (_md_parser.primary or _md_parser.secondary): 752 ↛ 753line 752 didn't jump to line 753 because the condition on line 752 was never true
753 continue
754 if _md_fname in self.files_with_preamble_errors:
755 continue
756 _md_lexer = getattr(_md_parser, "lexer", None)
757 if isinstance(_md_lexer, MD_Lexer): 757 ↛ 748line 757 didn't jump to line 748 because the condition on line 757 was always true
758 _md_lexer.prepare_phase2(self.stab) # Rebuild tokens with types
759 _md_parser.ct = None # Reset parser cursor
760 _md_parser.advance() # Prime first body token
762 # Perform sanity checks (enabled by default). We only do this
763 # if there were no errors so far.
764 if self.lint_mode and ok:
765 linter = lint.Linter(
766 mh=self.mh,
767 stab=self.stab,
768 verify_checks=self.verify_mode,
769 debug_vcg=self.debug_vcg,
770 )
771 ok &= linter.perform_sanity_checks()
772 # Stop here if we're not processing TRLC files.
773 if not self.parse_trlc: # pragma: no cover
774 self.callback_parse_end()
775 if ok:
776 return self.stab
777 else:
778 return None
780 # Parse TRLC files. Almost all the semantic analysis and name
781 # resolution happens here, with the notable exception of resolving
782 # record references (as we can have circularity here).
783 trlc_files_ok = self.parse_trlc_files()
785 # Now that all objects are known, check that sub-package names do
786 # not clash with objects declared in their parent package. This
787 # runs even if some TRLC files failed to parse, so a distinctness
788 # violation is still reported instead of being masked by an
789 # unrelated parsing error.
790 ok &= self.verify_subpackage_object_distinctness()
792 if not trlc_files_ok: # pragma: no cover
793 self.callback_parse_end()
794 return None
796 # Resolve record reference names and do the missing semantic
797 # analysis.
798 # lobster-trace: LRM.File_Parsing_References
799 if not self.resolve_record_references():
800 self.callback_parse_end()
801 return None
803 if not ok:
804 self.callback_parse_end()
805 return None
807 # Finally, apply user defined checks
808 if not self.perform_checks():
809 self.callback_parse_end()
810 return None
812 if self.lint_mode and ok:
813 linter.verify_imports()
815 self.callback_parse_end()
816 return self.stab
819def trlc():
820 ap = argparse.ArgumentParser(
821 prog="trlc",
822 description="TRLC %s (Python reference implementation)" % TRLC_VERSION,
823 epilog=("TRLC is licensed under the GPLv3. Report bugs here: %s" % BUGS_URL),
824 allow_abbrev=False,
825 )
826 og_lint = ap.add_argument_group("analysis options")
827 og_lint.add_argument(
828 "--no-lint",
829 default=False,
830 action="store_true",
831 help="Disable additional, optional warnings.",
832 )
833 og_lint.add_argument(
834 "--skip-trlc-files",
835 default=False,
836 action="store_true",
837 help=("Only process rsl files, do not process any trlc files."),
838 )
839 og_lint.add_argument(
840 "--verify",
841 default=False,
842 action="store_true",
843 help=(
844 "[EXPERIMENTAL] Attempt to statically"
845 " verify absence of errors in user defined"
846 " checks. Does not yet support all language"
847 " constructs. Requires PyVCG to be "
848 " installed."
849 ),
850 )
852 og_input = ap.add_argument_group("input options")
853 og_input.add_argument(
854 "--include-bazel-dirs",
855 action="store_true",
856 help=("Enter bazel-* directories, which are excluded by default."),
857 )
858 og_input.add_argument(
859 "-I",
860 action="append",
861 dest="include_dirs",
862 help=(
863 "Add include path. Files from these"
864 " directories are parsed only when needed."
865 " Can be specified more than once."
866 ),
867 default=[],
868 )
869 og_input.add_argument(
870 "--exclude",
871 action="append",
872 dest="exclude_file_or_dir",
873 metavar="PATH",
874 help=(
875 "Exclude a file or directory from processing."
876 " Anything under an excluded directory is skipped"
877 " as well. Can be specified more than once."
878 ),
879 default=[],
880 )
881 og_input.add_argument(
882 "--exclude-from-file",
883 action="append",
884 dest="exclude_from_files",
885 metavar="FILE",
886 help=(
887 "Read paths to exclude from a text file, one per"
888 " line. Empty lines and lines starting with #"
889 " are ignored. Can be specified more than once."
890 ),
891 default=[],
892 )
894 og_output = ap.add_argument_group("output options")
895 og_output.add_argument(
896 "--version",
897 default=False,
898 action="store_true",
899 help="Print TRLC version and exit.",
900 )
901 og_output.add_argument(
902 "--brief",
903 default=False,
904 action="store_true",
905 help=(
906 "Simpler output intended for CI. Does not"
907 " show context or additional information,"
908 " but prints the usual summary at the end."
909 ),
910 )
911 og_output.add_argument(
912 "--no-detailed-info",
913 default=False,
914 action="store_true",
915 help=(
916 "Do not print counter-examples and other"
917 " supplemental information on failed"
918 " checks. The specific values of"
919 " counter-examples are unpredictable"
920 " from system to system, so if you need"
921 " perfectly reproducible output then use"
922 " this option."
923 ),
924 )
925 og_output.add_argument(
926 "--no-user-warnings",
927 default=False,
928 action="store_true",
929 help=("Do not display any warnings from user defined checks, only errors."),
930 )
931 og_output.add_argument(
932 "--no-error-recovery",
933 default=False,
934 action="store_true",
935 help=(
936 "By default the tool attempts to recover"
937 " from parse errors to show more errors, but"
938 " this can occasionally generate weird"
939 " errors. You can use this option to stop"
940 " at the first real errors."
941 ),
942 )
943 og_output.add_argument(
944 "--show-file-list",
945 action="store_true",
946 help=("If there are no errors, produce a summary naming every file processed."),
947 )
948 og_output.add_argument(
949 "--log",
950 nargs="+",
951 metavar=("FILE", "PREFIX"),
952 default=None,
953 help=(
954 "Write all output to FILE, optionally"
955 " strip PREFIX from file paths in"
956 " messages. Intended for use as a"
957 " Bazel build action."
958 ),
959 )
960 og_output.add_argument(
961 "--error-on-warnings",
962 action="store_true",
963 help=("If there are warnings, return status code 1 instead of 0."),
964 )
966 og_debug = ap.add_argument_group("debug options")
967 og_debug.add_argument(
968 "--debug-dump", default=False, action="store_true", help="Dump symbol table."
969 )
970 og_debug.add_argument(
971 "--debug-api-dump",
972 default=False,
973 action="store_true",
974 help=("Dump json of to_python_object() for all objects."),
975 )
976 og_debug.add_argument(
977 "--debug-vcg",
978 default=False,
979 action="store_true",
980 help=("Emit graph and individual VCs. Requires graphviz to be installed."),
981 )
983 ap.add_argument("items", nargs="*", metavar="DIR|FILE")
984 options = ap.parse_args()
986 if options.log:
987 if len(options.log) > 2:
988 ap.error("--log accepts at most 2 values: FILE and optionally PREFIX")
989 if len(options.log) == 1:
990 options.log.append(None)
992 if options.version: # pragma: no cover
993 print(TRLC_VERSION)
994 sys.exit(0)
996 if options.verify and not VCG_API_AVAILABLE: # pragma: no cover
997 ap.error("The --verify option requires the optional dependency CVC5")
999 mh = Message_Handler(
1000 options.brief,
1001 not options.no_detailed_info,
1002 out_path=options.log[0] if options.log else None,
1003 strip_prefix=options.log[1] if options.log else None,
1004 )
1006 if options.no_user_warnings: # pragma: no cover
1007 mh.suppress(Kind.USER_WARNING)
1009 sm = Source_Manager(
1010 mh=mh,
1011 lint_mode=not options.no_lint,
1012 parse_trlc=not options.skip_trlc_files,
1013 verify_mode=options.verify,
1014 debug_vcg=options.debug_vcg,
1015 error_recovery=not options.no_error_recovery,
1016 )
1018 if not options.include_bazel_dirs: # pragma: no cover
1019 sm.exclude_patterns.append(re.compile("^bazel-.*$"))
1021 # Process excludes
1022 for list_name in options.exclude_from_files:
1023 if not os.path.isfile(list_name):
1024 ap.error("exclude list %s is not a file" % list_name)
1025 with open(list_name, encoding="UTF-8") as list_file:
1026 for line in list_file:
1027 line = line.strip()
1028 if line and not line.startswith("#"):
1029 options.exclude_file_or_dir.append(line)
1030 for path_name in options.exclude_file_or_dir:
1031 if not (os.path.isdir(path_name) or os.path.isfile(path_name)):
1032 ap.error("exclude path %s is not a file or directory" % path_name)
1033 for path_name in options.exclude_file_or_dir:
1034 sm.exclude_path(path_name)
1036 # Process includes
1037 ok = True
1038 for path_name in options.include_dirs:
1039 if not os.path.isdir(path_name): 1039 ↛ 1040line 1039 didn't jump to line 1040 because the condition on line 1039 was never true
1040 ap.error("include path %s is not a directory" % path_name)
1041 for path_name in options.include_dirs:
1042 if not sm.register_include(path_name):
1043 mh.close()
1044 return 1
1046 # Process input files, defaulting to the current directory if none
1047 # given.
1048 for path_name in options.items:
1049 if not (
1050 os.path.isdir(path_name) or os.path.isfile(path_name)
1051 ): # pragma: no cover
1052 ap.error("%s is not a file or directory" % path_name)
1053 if options.items:
1054 for path_name in options.items:
1055 if sm.is_path_excluded(path_name): 1055 ↛ 1056line 1055 didn't jump to line 1056 because the condition on line 1055 was never true
1056 continue
1057 if os.path.isdir(path_name):
1058 ok &= sm.register_directory(path_name)
1059 else: # pragma: no cover
1060 try:
1061 ok &= sm.register_file(path_name)
1062 except TRLC_Error:
1063 ok = False
1064 else: # pragma: no cover
1065 ok &= sm.register_directory(".")
1067 if not ok:
1068 mh.close()
1069 return 1
1071 if sm.process() is None:
1072 ok = False
1074 if ok:
1075 if options.debug_dump: # pragma: no cover
1076 sm.stab.dump()
1077 if options.debug_api_dump:
1078 tmp = {}
1079 for obj in sm.stab.iter_record_objects():
1080 tmp[obj.name] = obj.to_python_dict()
1081 for key in tmp[obj.name]:
1082 if isinstance(tmp[obj.name][key], Fraction): 1082 ↛ 1083line 1082 didn't jump to line 1083 because the condition on line 1082 was never true
1083 tmp[obj.name][key] = float(tmp[obj.name][key])
1085 print(json.dumps(tmp, indent=2, sort_keys=True), file=mh.out)
1087 total_models = len(sm.rsl_files)
1088 parsed_models = len(
1089 [item for item in sm.rsl_files.values() if item.primary or item.secondary]
1090 )
1091 total_trlc = len(sm.trlc_files)
1092 parsed_trlc = len(
1093 [item for item in sm.trlc_files.values() if item.primary or item.secondary]
1094 )
1096 def count(parsed, total, what):
1097 rv = str(parsed)
1098 if parsed < total:
1099 rv += " (of %u)" % total
1100 rv += " " + what
1101 if total == 0 or total > 1:
1102 rv += "s"
1103 return rv
1105 summary = "Processed %s" % count(parsed_models, total_models, "model")
1107 if not options.skip_trlc_files: # pragma: no cover
1108 summary += " and %s" % count(parsed_trlc, total_trlc, "requirement file")
1110 summary += " and found"
1112 if mh.errors and mh.warnings:
1113 summary += " %s" % count(mh.warnings, mh.warnings, "warning")
1114 summary += " and %s" % count(mh.errors, mh.errors, "error")
1115 elif mh.warnings:
1116 summary += " %s" % count(mh.warnings, mh.warnings, "warning")
1117 elif mh.errors:
1118 summary += " %s" % count(mh.errors, mh.errors, "error")
1119 else:
1120 summary += " no issues"
1122 if mh.suppressed: # pragma: no cover
1123 summary += " with %u supressed messages" % mh.suppressed
1125 print(summary, file=mh.out)
1127 if options.show_file_list and ok: # pragma: no cover
1129 def get_status(parser):
1130 if parser.primary:
1131 return "[Primary] "
1132 elif parser.secondary:
1133 return "[Included]"
1134 else:
1135 return "[Excluded]"
1137 for filename in sorted(sm.rsl_files):
1138 parser = sm.rsl_files[filename]
1139 print(
1140 "> %s Model %s (Package %s)"
1141 % (get_status(parser), filename, parser.cu.package.name),
1142 file=mh.out,
1143 )
1144 if not options.skip_trlc_files:
1145 for filename in sorted(sm.trlc_files):
1146 parser = sm.trlc_files[filename]
1147 print(
1148 "> %s Requirements %s (Package %s)"
1149 % (get_status(parser), filename, parser.cu.package.name),
1150 file=mh.out,
1151 )
1153 if ok:
1154 if (options.error_on_warnings and mh.warnings) or mh.errors: # pragma: no cover
1155 rv = 1
1156 else:
1157 rv = 0
1158 else:
1159 rv = 1
1160 mh.close()
1161 return rv
1164def main():
1165 try:
1166 return trlc()
1167 except BrokenPipeError:
1168 # Python flushes standard streams on exit; redirect remaining output
1169 # to devnull to avoid another BrokenPipeError at shutdown
1170 devnull = os.open(os.devnull, os.O_WRONLY)
1171 os.dup2(devnull, sys.stdout.fileno())
1172 return 141
1175if __name__ == "__main__":
1176 sys.exit(main())