adds linter warnings on unused imports

Author: christophkloeffel

CHANGELOG.md

@@ -27,6 +27,8 @@ generated in the following situations:
 
 ### 2.0.2-dev
 
+* [TRLC] Add linter warning on unused imports.
+
 * [TRLC] Add support for Python 3.13.
 
 * [TRLC] Fix help message for command line argument `--no-detailed-info`.

tests-system/late-packages-2/output

@@ -1 +1,4 @@
-Processed 0 models and 2 requirement files and found no issues
+import Foo
+       ^^^ late-packages-2/bar.trlc:2: issue: unused import Foo [unused_imports]
+         | Consider deleting this import statement if not needed.
+Processed 0 models and 2 requirement files and found 1 warning

tests-system/late-packages-2/output.smtlib

@@ -1 +1,4 @@
-Processed 0 models and 2 requirement files and found no issues
+import Foo
+       ^^^ late-packages-2/bar.trlc:2: issue: unused import Foo [unused_imports]
+         | Consider deleting this import statement if not needed.
+Processed 0 models and 2 requirement files and found 1 warning

tests-system/rbt-late-package-declarations/output

@@ -1 +1,4 @@
-Processed 0 models and 3 requirement files and found no issues
+import Foo
+       ^^^ rbt-late-package-declarations/baz.trlc:3: issue: unused import Foo [unused_imports]
+         | Consider deleting this import statement if not needed.
+Processed 0 models and 3 requirement files and found 1 warning

tests-system/rbt-late-package-declarations/output.smtlib

@@ -1 +1,4 @@
-Processed 0 models and 3 requirement files and found no issues
+import Foo
+       ^^^ rbt-late-package-declarations/baz.trlc:3: issue: unused import Foo [unused_imports]
+         | Consider deleting this import statement if not needed.
+Processed 0 models and 3 requirement files and found 1 warning

trlc/lint.py

@@ -41,7 +41,7 @@ def __init__(self, mh, stab, verify_checks, debug_vcg, cvc5_binary):
         self.abstract_extensions = {}
         self.checked_types       = set()
 
-    def verify(self):
+    def perform_sanity_checks(self):
         # lobster-exclude: Not safety relevant
         ok = True
         for package in self.stab.values(ast.Package):
@@ -202,3 +202,35 @@ def verify_array_type(self, n_typ):
                           "An array with 0 to 1 components should just\n"
                           "be an optional %s instead." %
                           n_typ.element_type.name)
+
+    def markup_ref(self, item, string_literals):
+        for string_literal in string_literals:
+            for reference in string_literal.references:
+                if reference.package.name == item.name:
+                    return string_literal
+        return None
+
+    def verify_imports(self):
+        for file in self.mh.sm.all_files.values():
+            if not file.primary and not file.secondary:
+                continue
+            if not file.cu.imports:
+                continue
+            for item in file.cu.imports:
+                import_tokens = [t for t in file.lexer.tokens
+                                 if t.value == item.name]
+                markup = self.markup_ref(item,
+                                         (m.ast_link for m in
+                                          file.lexer.tokens if
+                                          isinstance(m.ast_link,
+                                                     ast.String_Literal) and
+                                          m.ast_link.has_references))
+                if markup is not None:
+                    import_tokens.append(markup)
+                if len(import_tokens) == 1:
+                    import_tk = import_tokens[0]
+                    self.mh.check(import_tk.location,
+                                    "unused import %s" % import_tk.value,
+                                    "unused_imports",
+                                    "Consider deleting this import"
+                                    " statement if not needed.")

trlc/trlc.py

@@ -480,14 +480,6 @@ def perform_checks(self):
 
         return ok
 
-    def perform_sanity_checks(self):
-        linter = lint.Linter(mh            = self.mh,
-                             stab          = self.stab,
-                             verify_checks = self.verify_mode,
-                             debug_vcg     = self.debug_vcg,
-                             cvc5_binary   = self.cvc5_binary)
-        return linter.verify()
-
     def process(self):
         """Parse all registered files.
 
@@ -514,8 +506,12 @@ def process(self):
         # Perform sanity checks (enabled by default). We only do this
         # if there were no errors so far.
         if self.lint_mode and ok:
-            ok &= self.perform_sanity_checks()
-
+            linter = lint.Linter(mh            = self.mh,
+                                 stab          = self.stab,
+                                 verify_checks = self.verify_mode,
+                                 debug_vcg     = self.debug_vcg,
+                                 cvc5_binary   = self.cvc5_binary)
+            ok &= linter.perform_sanity_checks()
         # Stop here if we're not processing TRLC files.
         if not self.parse_trlc:  # pragma: no cover
             self.callback_parse_end()
@@ -547,6 +543,9 @@ def process(self):
             self.callback_parse_end()
             return None
 
+        if self.lint_mode and ok:
+            linter.verify_imports()
+
         self.callback_parse_end()
         return self.stab