Extend linter to check module dependencies #2196

peterschrammel · 2018-05-17T17:18:44Z

To use it just put a module_dependencies.txt into a directory,
which lists all modules that it is allowed to include header
files from.

It will emit messages such as

src/analyses/does_remove_const.cpp:19:  Module `analyses` must not use `ansi-c/c_qualifiers.h`  [build/include] [4]

If this is an acceptable solution, I'll populate the remaining module dependency definitions.

martin-cs

I like the idea of automatically checking policy rather than just having to tell people.

peterschrammel · 2018-05-17T21:10:16Z

This contains full annotated module dependency information now.

tautschnig · 2018-05-17T21:16:40Z

So how did you generate the dependency files? Is there a way of auto-generating them from Makefiles? Is that desirable or is it actually a bad idea to attempt to auto-generate them?
add git shortened sha1sum to CBMC version for unique id #668 would solve the cbmc/version.h problem that we currently have.
Should we first do some cleanup or merge this one and log all the cleanup to-be-done in some issue?

peterschrammel · 2018-05-17T21:29:05Z

I generated them from the error messages that the linter reported and annotated them manually. I don't think that the specification should be auto-adapted to the implementation.
We might still want to have a place to define human readable version numbers. The cbmc directory is certainly not the right place for it.
I prefer to merge this one and then do the cleanup separately.

peterschrammel · 2018-05-17T21:51:08Z

Observed issues collected here: #571

thk123

Seems reasonable - though I'm not sure the module_dependencies.txt is quite the right place for the commentary on the dependencies.

I also like the idea of it being driven by the Makefiles but not a blocker.

Is it worth having a warning for any folder that doesn't have a module_dependencies.txt (as people might wrongly assume that a subfolder will inherit the parents dependencies)

thk123 · 2018-05-18T08:43:04Z

scripts/cpplint.py

+    module_name = os.path.dirname(filename)
+    has_src = module_name.find('src/')
+    if has_src >= 0:
+        module_name = module_name[has_src+4:]


Should this be a warning as well?

I don't think it's worth a warning. It will only affect the module name printed in the error message.

thk123 · 2018-05-18T08:45:08Z

scripts/cpplint.py

@@ -6365,6 +6380,23 @@ def ProcessFileData(filename, file_extension, lines, error,

  ResetNolintSuppressions()

+  # Load module dependencies
+  module_deps_file = os.path.join(os.path.dirname(filename), 'module_dependencies.txt')


For src/ansi-c/literals/convert_float_literal.cpp this will go looking in src/ansi-c/literalsl/module_dependencies.txt no? Which presumably isn't quite right? I guess we need to find the last src/ and then the folder immediately below that?

My mistake - I see sub folders get their own dependencies.

thk123 · 2018-05-18T08:47:34Z

src/clobber/module_dependencies.txt

+cpp
+goto-programs
+goto-instrument
+java_bytecode # will go away


What's the difference between "will go away" and "should go away"?

'will go away' has already a PR filed ;)

peterschrammel · 2018-05-18T09:06:38Z

Is it worth having a warning for any folder that doesn't have a module_dependencies.txt (as people might wrongly assume that a subfolder will inherit the parents dependencies)

Good idea, @thk123, added this and caught two problems ;)

chrisr-diffblue

I like this a lot, and I would definitely agree that these module_dependencies.txt files should not be autogenerated seeing as these are policy documents.

smowton

Some Python style tips otherwise lgtm

smowton · 2018-05-18T14:09:06Z

scripts/cpplint.py

+        module_name = module_name[has_src+4:]
+    deps_name = os.path.dirname(include)
+    if deps_name and module_deps:
+        found = False


found = any(deps_name.startswith(module) for module in module_deps)

smowton · 2018-05-18T14:11:11Z

scripts/cpplint.py

+          has_comment = s.find('#')
+          if has_comment >= 0:
+              s = s[:has_comment]
+          s = s.lstrip().rstrip()


s = s.strip()

smowton · 2018-05-18T14:11:46Z

scripts/cpplint.py

+          module_deps = f.read().splitlines()
+      # strip off comments and whitespace
+      def strip_off_comments(s):
+          has_comment = s.find('#')


s/has_comment/comment_index/

smowton · 2018-05-18T14:12:32Z

scripts/cpplint.py

+              s = s[:has_comment]
+          s = s.lstrip().rstrip()
+          return s
+      module_deps = [ strip_off_comments(module) for module in module_deps]


Odd spacing -- [ x ] or [x] not [ x]

Also perhaps module_deps = map(strip_off_comments, module_deps)

smowton · 2018-05-18T14:17:49Z

scripts/cpplint.py

+          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 module]


Recommend if len(module) != 0 to make clear you're expecting strings not booleans

cesaro

Looks good, in particular regarding the upcoming changes wrt Java threading.

To use it just put a module_dependencies.txt into a directory, which lists all modules that it is allowed to include header files from.

Required for cpplint, cf. diffblue#2196

779fa71 Merge pull request diffblue#2253 from peterschrammel/documentation/override2 40ecff8 Merge pull request diffblue#2250 from tautschnig/expr-iterator-deque 050b344 Re-enable enforcement of override without virtual b5dec9c Get legalistic about use of override without virtual b51e2a8 Merge pull request diffblue#2196 from peterschrammel/check-module-includes d5eabdf expr_iterator: use a std::deque to implement the stack fada0af Add module dependency definition files a90ea44 Add module dependency check to CPP-LINT 88f8cfc Remove unnecessary includes d6986d8 Fix relative include paths 0f9c202 Merge pull request diffblue#2242 from diffblue/section-name-warning b7f5886 Merge pull request diffblue#2241 from diffblue/ld_mode 5c11eb7 Merge pull request diffblue#2245 from mgudemann/fix/warning/clang_self_assign f7e5fb5 Merge pull request diffblue#2229 from diffblue/ssize_t 1a504c9 Merge pull request diffblue#2244 from diffblue/solver-Makefile-fix 4bb1bf0 Fix clang++'s warning about self-assign 9a0aa9c Merge pull request diffblue#2235 from thomasspriggs/test-pl-colour 4c2cb3a remove linker mode from gcc_mode 303908f add separate path for ld 524091f factor out creation of hybrid binaries b9127f3 linker_script_merget now takes exactly one ELF + goto binary cd967db update year + add Michael 0d95cc5 missing const method qualifiers 6f04d98 fix ordering problem in solvers/Makefile 8f6bae0 remove a warning about section names 8befd02 Merge pull request diffblue#2238 from owen-jones-diffblue/owen-jones-diffblue/doc/irep_id 34b0ac6 Merge pull request diffblue#2236 from diffblue/show-class-hierarchy 8e8e450 Merge pull request diffblue#2232 from owen-jones-diffblue/owen-jones-diffblue/generic-bounded-types 01dc76b Add section on irep_idt and dstringt 2f4c6ad Add and unify --show-class-hierarchy command line option 56256f1 Minor typos in irept documentation 3cf4e3a Merge pull request diffblue#2178 from thomasspriggs/remove_java_bytecode_parse_treet_swap 1a7235d use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET a018e2f Add JSON output for class hierarchy 68c45ed Improve class hierarchy output eeb732f Switch `push_back` to `emplace_back` when constructing `parse_trees`. f154840 Delete copy constructor of `class java_bytecode_parse_treet`. c5cbcec Fix instances where copying was being used instead of moving. 52a669f Remove `java_bytecode::swap` and return using `optionalt` instead. fabbd04 Give up parsing generic method signature with bound 77f8162 Colour code tests passing vs failing. e5e0897 Merge pull request diffblue#2126 from danpoe/refactor/sharing-map-small-nodes f55bd96 Merge pull request diffblue#2231 from smowton/smowton/fix/jbmc-tests af02973 Merge pull request diffblue#2202 from smowton/smowton/fix/java-lang-class-fields 42a78af JBMC tests: suffix logfiles when using symex-driven loading af2defd Removed obsolete sharing map unit test 1d7fbd3 Refactor sharing map nodes to reduce memory consumption 5235938 Restore testing of jbmc 8a59f6f Object factory: permit null pointers within java.lang.Class 8412eb0 Merge pull request diffblue#2228 from peterschrammel/move-remaining-java-tests 369577a Move remaining java tests to jbmc/regression/ bfe3d3d Merge pull request diffblue#2226 from tautschnig/inline-get-str-cont 2b00973 Merge pull request diffblue#2227 from tautschnig/fptr-removal 3f7685f Merge pull request diffblue#2223 from diffblue/fp-builtins 3b3dc71 Distinct names of return-value symbols 4f7fade Cleanup: use symbolt::symbol_expr 8372862 function-pointer removal: Set the mode of a return symbol 272cde0 Inline get_string_container 72a0379 test __builtin_isinf, __builtin_isinf_sign, __builtin_isnormal f156ef0 Merge pull request diffblue#2222 from tautschnig/attributes a69c603 add __builtin_isnormal 83aeddd added __builtin_isinf_sign 87d467e fix return types of various __builtin_is* functions 61af061 added typecast_exprt::conditional_cast e1b906a Support GCC's fallthrough attribute d6d0a49 C front-end: support alias attributes on variables 376beab Merge pull request diffblue#2218 from diffblue/builtin_fpclassify c3603e3 added a test for raw __builtin_fpclassify 52595bd add support for __builtin_fpclassify 50d1c79 Merge pull request diffblue#2214 from tautschnig/tg-only 3c59312 Remove unused substitute.{h,cpp} d3e131c Revert "Set memory limit utility" a4389fe Merge pull request diffblue#2210 from tautschnig/verbosity-cleanup c250880 Merge pull request diffblue#2211 from tautschnig/travis-osx-cleanup c8597a4 Merge pull request diffblue#2174 from romainbrenguier/bugfix/not_contains#TG-3150 b08ef94 Merge pull request diffblue#2216 from peterschrammel/update-codeowners 471ab0f Merge pull request diffblue#2207 from diffblue/remove-solvers-cvc 215cd69 Use enum entries instead of numeric values when comparing verbosity 6344b4f Warn if user-specified verbosity is out of range bf04bcb Use a single implementation of eval_verbosity b4731eb Do not redundantly set the message handler 42ec63a Clean up .gitignore 19200bf Update CODEOWNERS for /jbmc 0487376 Merge pull request diffblue#2173 from svorenova/gs_tg1121 6af2270 Update regression test that no longer throws an exception bc17328 Enable previously failing regression tests 146bb29 Adding debug information to dereference type comparison 7b9a20a Allow pointers to be dereferenced to void types 108129c Merge pull request diffblue#2118 from diffblue/remove-jbmc 11411e4 Travis/OSX follow-up cleanup: remove unnecessary environment variables 386faa8 Test for String.contains and very large strings 9e73699 Refactor negation of not contains constraints 29a8818 Build jbmc on CI f196e74 Update compilation instructions 1b7c84a Add JBMC README 03d6f5b Shorten goto-analyzer-taint-ansi-c tests to goto-analyzer-taint 8dc0d74 Remove obsolete jbmc-cover tests f36da08 Move Java regression tests b6742ca Move Java unit tests e247458 Add JANALYZER tool 4588753 Add JDIFF tool a20f2c1 Move java_bytecode, jbmc and miniz to jbmc/src 987106f Make unit test independent of java_bytecode d945452 Adapt cpplint header guard check 28907b2 remove (pre-SMT-LIB) CVC interface git-subtree-dir: cbmc git-subtree-split: 779fa71

peterschrammel requested review from chrisr-diffblue, forejtv, kroening, martin-cs, smowton, tautschnig and thk123 as code owners May 17, 2018 17:18

martin-cs approved these changes May 17, 2018

View reviewed changes

peterschrammel force-pushed the check-module-includes branch from 702f8d6 to ba17e35 Compare May 17, 2018 20:57

peterschrammel requested review from cesaro, mgudemann and romainbrenguier as code owners May 17, 2018 20:57

peterschrammel force-pushed the check-module-includes branch from ba17e35 to 0df597e Compare May 17, 2018 21:08

tautschnig approved these changes May 17, 2018

View reviewed changes

peterschrammel mentioned this pull request May 17, 2018

Cleanup unwanted dependencies between CBMC modules #571

Open

peterschrammel assigned cesaro, smowton, thk123, kroening, mgudemann and forejtv May 18, 2018

thk123 reviewed May 18, 2018

View reviewed changes

peterschrammel force-pushed the check-module-includes branch from 0df597e to 63493cf Compare May 18, 2018 10:05

chrisr-diffblue approved these changes May 18, 2018

View reviewed changes

smowton approved these changes May 18, 2018

View reviewed changes

cesaro approved these changes May 18, 2018

View reviewed changes

romainbrenguier approved these changes May 21, 2018

View reviewed changes

peterschrammel force-pushed the check-module-includes branch from 63493cf to 29cf186 Compare May 21, 2018 16:23

peterschrammel added 2 commits May 29, 2018 13:56

Fix relative include paths

d6986d8

Remove unnecessary includes

88f8cfc

peterschrammel force-pushed the check-module-includes branch 2 times, most recently from 41e6642 to 4fb755c Compare May 29, 2018 13:01

peterschrammel added 2 commits May 29, 2018 14:05

Add module dependency check to CPP-LINT

a90ea44

To use it just put a module_dependencies.txt into a directory, which lists all modules that it is allowed to include header files from.

Add module dependency definition files

fada0af

peterschrammel force-pushed the check-module-includes branch from 4fb755c to fada0af Compare May 29, 2018 13:05

peterschrammel merged commit b51e2a8 into diffblue:develop May 29, 2018

peterschrammel deleted the check-module-includes branch May 29, 2018 14:53

mgudemann pushed a commit to mgudemann/cbmc that referenced this pull request May 30, 2018

Add module_dependencies.txt file

33610a5

Required for cpplint, cf. diffblue#2196

tautschnig mentioned this pull request May 30, 2018

C++ front end fixes [blocks: #2554] #1260

Merged

38 tasks

mgudemann pushed a commit to mgudemann/cbmc that referenced this pull request Jun 5, 2018

Add module_dependencies.txt file

a200834

Required for cpplint, cf. diffblue#2196

mgudemann pushed a commit to mgudemann/cbmc that referenced this pull request Jun 5, 2018

Add module_dependencies.txt file

b2fa10b

Required for cpplint, cf. diffblue#2196

mgudemann pushed a commit to mgudemann/cbmc that referenced this pull request Jun 5, 2018

Add module_dependencies.txt file

5c077b2

Required for cpplint, cf. diffblue#2196

mgudemann pushed a commit to mgudemann/cbmc that referenced this pull request Jun 6, 2018

Add module_dependencies.txt file

bbc2bac

Required for cpplint, cf. diffblue#2196

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extend linter to check module dependencies #2196

Extend linter to check module dependencies #2196

peterschrammel commented May 17, 2018

martin-cs left a comment

peterschrammel commented May 17, 2018

tautschnig commented May 17, 2018

peterschrammel commented May 17, 2018 •

edited

Loading

peterschrammel commented May 17, 2018

thk123 left a comment

thk123 May 18, 2018

peterschrammel May 18, 2018

thk123 May 18, 2018

thk123 May 18, 2018

thk123 May 18, 2018

peterschrammel May 18, 2018

peterschrammel commented May 18, 2018 •

edited

Loading

chrisr-diffblue left a comment

smowton left a comment

smowton May 18, 2018

smowton May 18, 2018

smowton May 18, 2018

smowton May 18, 2018

smowton May 18, 2018

smowton May 18, 2018

cesaro left a comment

Extend linter to check module dependencies #2196

Extend linter to check module dependencies #2196

Conversation

peterschrammel commented May 17, 2018

martin-cs left a comment

Choose a reason for hiding this comment

peterschrammel commented May 17, 2018

tautschnig commented May 17, 2018

peterschrammel commented May 17, 2018 • edited Loading

peterschrammel commented May 17, 2018

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 18, 2018 • edited Loading

chrisr-diffblue left a comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cesaro left a comment

Choose a reason for hiding this comment

peterschrammel commented May 17, 2018 •

edited

Loading

peterschrammel commented May 18, 2018 •

edited

Loading