Extend linter to check module dependencies

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -17,9 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <ansi-c/ansi_c_language.h>
-#include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
-#include <jsil/jsil_language.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>

jbmc/src/janalyzer/module_dependencies.txt

@@ -0,0 +1,9 @@
+analyses
+ansi-c # should go away
+cbmc # version.h
+java_bytecode
+jdiff
+goto-analyzer
+goto-programs
+langapi # should go away
+util

jbmc/src/java_bytecode/library/module_dependencies.txt

@@ -0,0 +1 @@
+java_bytecode/library

jbmc/src/java_bytecode/module_dependencies.txt

@@ -0,0 +1,10 @@
+analyses
+ansi-c # should go away
+goto-programs
+java_bytecode
+json
+langapi # should go away
+library
+linking
+miniz
+util

jbmc/src/jbmc/module_dependencies.txt

@@ -0,0 +1,12 @@
+analyses
+ansi-c # should go away
+cbmc # version.h and bmc.h
+goto-instrument
+goto-programs
+goto-symex
+java_bytecode
+jbmc
+langapi # should go away
+linking
+pointer-analysis
+util

jbmc/src/jdiff/module_dependencies.txt

@@ -0,0 +1,11 @@
+analyses
+cbmc # version.h
+java_bytecode
+jdiff
+goto-diff
+goto-instrument
+goto-programs
+goto-symex # dubious - rewrite_union
+langapi # should go away
+pointer-analysis
+util

jbmc/src/miniz/module_dependencies.txt

@@ -0,0 +1,2 @@
+miniz
+sys # system

scripts/cpplint.py

@@ -4981,7 +4981,7 @@ def _ClassifyInclude(fileinfo, include, is_system):
 
 
 
-def CheckIncludeLine(filename, clean_lines, linenum, include_state, error):
+def CheckIncludeLine(filename, clean_lines, linenum, include_state, error, module_deps):
   """Check rules that are applicable to #include lines.
 
   Strings on #include lines are NOT removed from elided line, to make
@@ -5029,6 +5029,18 @@ def CheckIncludeLine(filename, clean_lines, linenum, include_state, error):
     elif not _THIRD_PARTY_HEADERS_PATTERN.match(include):
       include_state.include_list[-1].append((include, linenum))
 
+    # Check module dependencies
+    module_name = os.path.dirname(filename)
+    has_src = module_name.find('src/')
+    if has_src >= 0:
+        module_name = module_name[has_src+4:]
+    deps_name = os.path.dirname(include)
+    if deps_name and module_deps:
+        may_use = any(deps_name.startswith(module) for module in module_deps)
+        if not may_use:
+            error(filename, linenum, 'build/include', 4,
+                  'Module `'+module_name+'` must not use `'+include+'`')
+
       # We want to ensure that headers appear in the right order:
       # 1) for foo.cc, foo.h  (preferred location)
       # 2) c system files
@@ -5141,7 +5153,7 @@ def _GetTextInside(text, start_pattern):
 
 
 def CheckLanguage(filename, clean_lines, linenum, file_extension,
-                  include_state, nesting_state, error):
+                  include_state, nesting_state, error, module_deps):
   """Checks rules from the 'C++ language rules' section of cppguide.html.
 
   Some of these rules are hard to test (function overloading, using
@@ -5165,7 +5177,7 @@ def CheckLanguage(filename, clean_lines, linenum, file_extension,
 
   match = _RE_PATTERN_INCLUDE.search(line)
   if match:
-    CheckIncludeLine(filename, clean_lines, linenum, include_state, error)
+    CheckIncludeLine(filename, clean_lines, linenum, include_state, error, module_deps)
     return
 
   # Reset include state across preprocessor directives.  This is meant
@@ -6246,7 +6258,7 @@ def CheckForEndl(filename, clean_lines, linenum, error):
     error(filename, linenum, 'runtime/endl', 4, 'Do not use std::endl')
 
 def ProcessLine(filename, file_extension, clean_lines, line,
-                include_state, function_state, nesting_state, error,
+                include_state, function_state, nesting_state, error, module_deps,
                 extra_check_functions=[]):
   """Processes a single line in the file.
 
@@ -6276,7 +6288,7 @@ def ProcessLine(filename, file_extension, clean_lines, line,
   CheckForMultilineCommentsAndStrings(filename, clean_lines, line, error)
   CheckStyle(filename, clean_lines, line, file_extension, nesting_state, error)
   CheckLanguage(filename, clean_lines, line, file_extension, include_state,
-                nesting_state, error)
+                nesting_state, error, module_deps)
   CheckForNonConstReference(filename, clean_lines, line, nesting_state, error)
   CheckForNonStandardConstructs(filename, clean_lines, line,
                                 nesting_state, error)
@@ -6370,6 +6382,27 @@ def ProcessFileData(filename, file_extension, lines, error,
 
   ResetNolintSuppressions()
 
+  # Load module dependencies
+  module_deps_file = os.path.join(os.path.dirname(filename), 'module_dependencies.txt')
+  module_deps = []
+  if os.path.isfile(module_deps_file):
+      with open(module_deps_file, 'r') as f:
+          module_deps = f.read().splitlines()
+      # strip off comments and whitespace
+      def strip_off_comments(s):
+          comment_index = s.find('#')
+          if comment_index >= 0:
+              s = s[:comment_index]
+          s = s.strip()
+          return s
+      module_deps = [strip_off_comments(module) for module in module_deps]
+      # remove empty lines
+      module_deps = [module for module in module_deps if len(module) != 0]
+  else:
+      error(filename, 0, 'build/include', 4,
+            'module_dependencies.txt not found in `' +
+                os.path.dirname(filename) + '`')
+
   CheckForCopyright(filename, lines, error)
   CheckForFunctionCommentHeaders(filename, lines, error)
   ProcessGlobalSuppresions(lines)
@@ -6381,7 +6414,7 @@ def ProcessFileData(filename, file_extension, lines, error,
 
   for line in xrange(clean_lines.NumLines()):
     ProcessLine(filename, file_extension, clean_lines, line,
-                include_state, function_state, nesting_state, error,
+                include_state, function_state, nesting_state, error, module_deps,
                 extra_check_functions)
     FlagCxx11Features(filename, clean_lines, line, error)
   nesting_state.CheckCompletedBlocks(filename, error)

src/analyses/module_dependencies.txt

@@ -0,0 +1,6 @@
+analyses
+ansi-c # should go away
+goto-programs
+langapi # should go away
+pointer-analysis
+util

src/ansi-c/library/module_dependencies.txt

@@ -0,0 +1,2 @@
+ansi-c
+ansi-c/library

src/ansi-c/literals/convert_float_literal.cpp

@@ -21,8 +21,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/string2int.h>
 
+#include <ansi-c/gcc_types.h>
+
 #include "parse_float.h"
-#include "../gcc_types.h"
 
 exprt convert_float_literal(const std::string &src)
 {

src/ansi-c/literals/module_dependencies.txt

@@ -0,0 +1,3 @@
+ansi-c
+ansi-c/literals
+util

src/ansi-c/module_dependencies.txt

@@ -0,0 +1,6 @@
+ansi-c
+goto-programs
+langapi # should go away
+linking
+literals
+util

src/assembler/module_dependencies.txt

@@ -0,0 +1,2 @@
+assembler
+util

src/big-int/module_dependencies.txt

@@ -0,0 +1 @@
+big-int

src/cbmc/module_dependencies.txt

@@ -0,0 +1,13 @@
+analyses
+ansi-c
+cpp
+goto-instrument
+goto-programs
+goto-symex
+jsil
+langapi # should go away
+linking
+pointer-analysis
+solvers
+xmllang
+util

src/clobber/module_dependencies.txt

@@ -0,0 +1,10 @@
+analyses
+ansi-c
+cbmc
+clobber
+cpp
+goto-programs
+goto-instrument
+java_bytecode # will go away
+langapi # should go away
+util

src/cpp/module_dependencies.txt

@@ -0,0 +1,5 @@
+ansi-c
+cpp
+langapi # should go away
+linking
+util

src/goto-analyzer/module_dependencies.txt

@@ -0,0 +1,11 @@
+ansi-c
+analyses
+cbmc # version.h
+cpp
+goto-analyzer
+goto-programs
+java_bytecode # will go away
+langapi # should go away
+jsil
+json
+util

src/goto-cc/module_dependencies.txt

@@ -0,0 +1,10 @@
+ansi-c
+cbmc # version.h
+cpp
+goto-cc
+goto-programs
+jsil
+json
+langapi # should go away
+linking
+util

src/goto-diff/module_dependencies.txt

@@ -0,0 +1,12 @@
+analyses
+ansi-c
+cbmc # version.h
+cpp
+goto-diff
+goto-instrument
+goto-programs
+goto-symex # dubious - rewrite_union and adjust_float should be moved to goto-programs
+java_bytecode # will go away
+langapi # should go away
+pointer-analysis
+util

src/goto-instrument/accelerate/module_dependencies.txt

@@ -0,0 +1,7 @@
+analyses
+ansi-c # should go away
+goto-instrument/accelerate
+goto-programs
+goto-symex
+solvers
+util

src/goto-instrument/module_dependencies.txt

@@ -0,0 +1,12 @@
+accelerate
+analyses
+ansi-c
+cbmc # version.h
+cpp
+goto-instrument
+goto-programs
+langapi # should go away
+linking
+pointer-analysis
+util
+wmm

src/goto-instrument/wmm/goto2graph.cpp

@@ -21,7 +21,8 @@ Date: 2012
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
+
 #include "fence.h"
 
 // #define PRINT_UNSAFES

src/goto-instrument/wmm/module_dependencies.txt

@@ -0,0 +1,5 @@
+goto-instrument
+goto-instrument/wmm
+goto-programs
+linking
+util

src/goto-instrument/wmm/shared_buffers.cpp

@@ -12,7 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
+
 #include "fence.h"
 
 /// returns a unique id (for fresh variables)

src/goto-instrument/wmm/weak_memory.cpp

@@ -27,7 +27,7 @@ Date: September 2011
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
 
 #include "shared_buffers.h"
 #include "goto2graph.h"

src/goto-programs/module_dependencies.txt

@@ -0,0 +1,11 @@
+analyses # dubious - concerns call_graph and does_remove_const
+ansi-c # should go away
+assembler # should go away
+goto-programs
+goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
+json
+langapi # should go away
+linking
+mach-o # system
+util
+xmllang

src/goto-symex/module_dependencies.txt

@@ -0,0 +1,8 @@
+analyses
+goto-programs
+goto-symex
+langapi # should go away
+linking
+pointer-analysis
+solvers
+util

src/jsil/module_dependencies.txt

@@ -0,0 +1,6 @@
+ansi-c # should go away
+goto-programs
+jsil
+langapi # should go away
+linking
+util

src/json/module_dependencies.txt

@@ -0,0 +1,2 @@
+json
+util

src/langapi/module_dependencies.txt

@@ -0,0 +1,3 @@
+goto-programs
+langapi
+util

src/linking/module_dependencies.txt

@@ -0,0 +1,5 @@
+ansi-c # should go away
+goto-programs
+langapi # should go away
+linking
+util

src/memory-models/module_dependencies.txt

@@ -0,0 +1,4 @@
+cbmc # version.h
+memory-models
+langapi # should go away
+util

src/miniz/module_dependencies.txt

@@ -0,0 +1,2 @@
+miniz
+sys # system

src/nonstd/module_dependencies.txt

@@ -0,0 +1 @@
+nonstd

src/pointer-analysis/module_dependencies.txt

@@ -0,0 +1,6 @@
+analyses
+ansi-c # should go away
+goto-programs
+langapi # should go away
+pointer-analysis
+util

src/solvers/cvc/module_dependencies.txt

@@ -0,0 +1,4 @@
+solvers/cvc
+solvers/flattening # pointer_logic.h
+solvers/prop
+util

src/solvers/flattening/boolbv.cpp

@@ -26,8 +26,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv_type.h"
 
-#include "../floatbv/float_utils.h"
-#include "../lowering/expr_lowering.h"
+#include <solvers/floatbv/float_utils.h>
+#include <solvers/lowering/expr_lowering.h>
 
 bool boolbvt::literal(
   const exprt &expr,