remove usage of Java bytecode frontend #2118

kroening · 2018-04-26T09:37:10Z

Do not merge yet -- we'll give test-gen time to switch to the jbmc repository.

chrisr-diffblue · 2018-04-27T13:28:16Z

I've pushed what I think should be a fix to get the CMake builds passing again (I can now build CMake builds locally). I have to say it's a bit of a hack, mostly to work around the fact the the CMake builds are currently using file globing - but also because I'm not entirely sure what the full intent of this PR is - are you intending to entirely move the java_bytecode source out of the repo? Or still keep it in the repo, but not build it by default? If the code is going to stay in the repo then it may be a better idea to refactor the directory structure a bit so that all the java_bytecode + it's unit/regression tests are in their own sub-directory. This would make it then possible to have CMake cleanly ignore the java_bytecode stuff.

tautschnig

Documentation (at the very least: COMPILING.md) needs to be updated as well.
The changes to regression and unit tests seem wrong as indicated.

tautschnig · 2018-04-27T13:33:45Z

regression/Makefile

       cbmc-cover \
       goto-instrument-typedef \
       smt2_solver \
       strings \
       invariants \
-       goto-diff \


This seems wrong. If there are Java-only bits then there should be a goto-diff-java directory instead.

It looks like it's 11 out of 17 tests in goto-diff that use java, but I agree, it seems wrong to be disabling non-java tests in this PR! I've replicated this particular change in the CMakeFile fix up commit, but that doesn't mean I agree with that change :-)

tautschnig · 2018-04-27T13:36:27Z

unit/Makefile

@@ -13,47 +13,26 @@ SRC += unit_tests.cpp \
       analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
       analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
       goto-programs/goto_trace_output.cpp \
-       goto-programs/class_hierarchy_output.cpp \
-       goto-programs/class_hierarchy_graph.cpp \
-       goto-programs/remove_virtual_functions_without_fallback.cpp \


If those three depend on Java then the implementation ought to move to the java_bytecode folder.

tautschnig · 2018-04-27T13:36:46Z

unit/Makefile

-       java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
-       java_bytecode/java_utils_test.cpp \
-       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
-       pointer-analysis/custom_value_set_analysis.cpp \


Why is this being removed?

tautschnig · 2018-04-27T13:37:11Z

unit/Makefile

       solvers/refinement/string_refinement/sparse_array.cpp \
       solvers/refinement/string_refinement/union_find_replace.cpp \
       util/expr_cast/expr_cast.cpp \
       util/expr_iterator.cpp \
-       util/has_subtype.cpp \


Change the test, don't remove it.

tautschnig · 2018-04-27T13:37:42Z

unit/Makefile

       util/irep.cpp \
       util/irep_sharing.cpp \
       util/message.cpp \
       util/optional.cpp \
-       util/parameter_indices.cpp \
-       util/simplify_expr.cpp \


Either the test is inappropriate or it shouldn't be removed.

chrisr-diffblue

While I've 'fixed up' the cmake builds so that they pass CI, I strongly agree with @tautschnig that the unit/regression test changes are wrong - there's useful non-java tests being disabled. It would also help reviewing if there was a clear statement as to what the strategy is for the java front-end now - if the java_bytecode stuff is going to be removed, then why is that removal not just part of this PR? Although it would be a 'bigger' PR, it would probably also be cleaner.

peterschrammel

This is passing now on all platforms with all build systems. I've seen passing builds of TG on Friday.

I don't think we have to wait for any other PRs to be merged before, because they can now be more easily rebased (since everything remains in the same repo).

I would appreciate a second eye pair to sanity check the PR before merging, though. There have been quite some changes since the approving reviews.

The addition of jdiff and janalyzer suffers from the same shortcomings as #2144, but cannot be postponed. I suggest to apply the required simplifications in a later step as soon as we have a solution for 2144.

kroening · 2018-05-20T17:41:20Z

jbmc/README.md

+======
+
+Compiling produces an executable called symex which by default can be found in `jbmc/src/jbmc/jbmc`
+


The executable is called jbmc, not symex.

kroening · 2018-05-20T17:43:29Z

jbmc/src/CMakeLists.txt

+        COMPILE_FLAGS "-Pyy${name}"
+    )
+endmacro(generic_flex)
+


Does jbmc need bison/flex at all?

kroening · 2018-05-20T17:44:49Z

jbmc/src/janalyzer/Makefile

+      ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/assembler/assembler$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \


The assembler front-end isn't needed.

kroening · 2018-05-20T17:45:57Z

jbmc/src/janalyzer/janalyzer_parse_options.h

+#define JANALYZER_OPTIONS \
+  OPT_FUNCTIONS \
+  "D:I:(std89)(std99)(std11)" \
+  "(classpath):(cp):(main-class):" \


No need for D:I: etc. in janalyzer.

kroening · 2018-05-20T17:46:24Z

jbmc/src/janalyzer/janalyzer_parse_options.h

+  "(show-reachable-properties)(property):" \
+  "(verbosity):(version)" \
+  "(gcc)(arch):" \
+  "(taint):(show-taint)" \


No need for --gcc option.

kroening · 2018-05-20T17:47:57Z

jbmc/src/jbmc/CMakeLists.txt

+    analyses
+    ansi-c
+    assembler
+    big-int


No need for assembler.

kroening · 2018-05-20T17:48:08Z

jbmc/src/jbmc/CMakeLists.txt

+    big-int
+    cbmc-lib
+    cpp
+    goto-instrument-lib


No need for cpp.

kroening · 2018-05-20T17:49:11Z

jbmc/src/jdiff/CMakeLists.txt

+    util
+    solvers
+)
+


Same remove assembler, cpp

to deal with non-top-level `src` and `unit` directories

tautschnig · 2018-05-21T10:23:45Z

Should janalyzer and jdiff really even exist? I'm aware that goto-analyzer currently does support C programs as input, but I don't think it actually should. There's a front-end tool (goto-cc) to build goto binaries and working with those ought to be completely sufficient. Now of course I don't actually know about the Java story. Since lazy loading doesn't seem to make as much sense for goto-analyzer (or goto-diff), shouldn't there just be an equivalent of goto-cc for Java? As far as I can tell there is no need for goto-analyzer (or goto-diff) to produce any language-specific output, and consequently these could safely be used without any linking to C/Java/other front-end languages?

peterschrammel · 2018-05-21T10:47:50Z

janalyzer and jdiff should only provide a Java-friendly command line interface (eventually); they shouldn't provide any core algorithms. This is currently suboptimal (I essentially copied them) and needs to be improved to avoid code duplication in *_parse_options. I agree that there should be goto-cc for Java, but that's orthogonal. You could argue in the same way that CBMC need not accept any .c files. The current problem that is solved here is that at the time of merging this PR we need a goto-diff variant that accepts jar files.

tautschnig · 2018-05-21T10:54:42Z

janalyzer and jdiff should only provide a Java-friendly command line interface (eventually); they shouldn't provide any core algorithms. This is currently suboptimal (I essentially copied them) and needs to be improved to avoid code duplication in *_parse_options. I agree that there should be goto-cc for Java, but that's orthogonal. You could argue in the same way that CBMC need not accept any .c files. The current problem that is solved here is that at the time of merging this PR we need a goto-diff variant that accepts jar files.

I accept that you might have an immediate business need for a working goto-diff for jar files, hence a copy&paste jdiff is a short-term workaround.

In the medium term: It's not clear to me what constitutes a "Java-friendly command line interface?" As I said, I don't see why any of those tools should have anything to do with the input language at all, and thus I don't really know why such a command-line interface would be needed? Of course any of that only applies when we have a goto-cc equivalent for Java, which in turn I thus do not see as orthogonal but rather as a necessary dependency to enable language-independence of goto-analyzer/goto-diff (and ideally also goto-instrument, but that requires a lot more cleanup).

Edit: yes, I would indeed argue that CBMC need to accept any .c files. It's just that a lot of people out there have gotten used to using it in that way, so it requires a slightly longer transition period.

peterschrammel

TG build is passing. I'm fine to get this merged now.
@kroening, @smowton, @thk123, any objections?

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

kroening added do not merge cleanup labels Apr 26, 2018

kroening requested a review from peterschrammel April 26, 2018 09:37

kroening requested review from chrisr-diffblue, martin-cs, smowton and tautschnig as code owners April 26, 2018 09:37

kroening force-pushed the remove-jbmc branch 10 times, most recently from 68d54ed to 9c03c0a Compare April 26, 2018 16:49

kroening requested review from cesaro and mgudemann as code owners April 27, 2018 13:24

tautschnig requested changes Apr 27, 2018

View reviewed changes

chrisr-diffblue force-pushed the remove-jbmc branch from 28a3190 to 8ab471d Compare April 27, 2018 13:48

chrisr-diffblue suggested changes Apr 27, 2018

View reviewed changes

kroening force-pushed the remove-jbmc branch from 8ab471d to c4b82ea Compare April 27, 2018 15:05

peterschrammel added the Java Front End label Apr 28, 2018

kroening force-pushed the remove-jbmc branch from c4b82ea to 23dab33 Compare April 28, 2018 16:27

tautschnig assigned kroening May 5, 2018

chrisr-diffblue force-pushed the remove-jbmc branch 3 times, most recently from 1c1748d to 87770c2 Compare May 10, 2018 10:27

peterschrammel requested changes May 20, 2018

View reviewed changes

kroening commented May 20, 2018

View reviewed changes

jbmc/src/CMakeLists.txt Outdated

COMPILE_FLAGS "-Pyy${name}"

)

endmacro(generic_flex)

Copy link

Member Author

kroening May 20, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does jbmc need bison/flex at all?

kroening commented May 20, 2018

View reviewed changes

jbmc/src/jbmc/CMakeLists.txt Outdated

analyses

ansi-c

assembler

big-int

Copy link

Member Author

kroening May 20, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need for assembler.

kroening commented May 20, 2018

View reviewed changes

jbmc/src/jbmc/CMakeLists.txt Outdated

big-int

cbmc-lib

cpp

goto-instrument-lib

Copy link

Member Author

kroening May 20, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need for cpp.

kroening commented May 20, 2018

View reviewed changes

jbmc/src/jdiff/CMakeLists.txt Outdated

util

solvers

)

Copy link

Member Author

kroening May 20, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same remove assembler, cpp

peterschrammel added 12 commits May 20, 2018 23:00

Adapt cpplint header guard check

d945452

to deal with non-top-level `src` and `unit` directories

Make unit test independent of java_bytecode

987106f

Move java_bytecode, jbmc and miniz to jbmc/src

a20f2c1

Add JDIFF tool

4588753

Add JANALYZER tool

e247458

Move Java unit tests

b6742ca

Move Java regression tests

f36da08

Remove obsolete jbmc-cover tests

8dc0d74

Shorten goto-analyzer-taint-ansi-c tests to goto-analyzer-taint

03d6f5b

Add JBMC README

1b7c84a

Update compilation instructions

f196e74

Build jbmc on CI

29a8818

peterschrammel force-pushed the remove-jbmc branch from 6bbe698 to 29a8818 Compare May 20, 2018 22:04

peterschrammel approved these changes May 21, 2018

View reviewed changes

peterschrammel merged commit 108129c into develop May 21, 2018

peterschrammel deleted the remove-jbmc branch May 21, 2018 13:58

tautschnig mentioned this pull request May 21, 2018

Post-jbmc move cleanup #2215

Open

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

remove usage of Java bytecode frontend #2118

remove usage of Java bytecode frontend #2118

kroening commented Apr 26, 2018

chrisr-diffblue commented Apr 27, 2018

tautschnig left a comment

tautschnig Apr 27, 2018

chrisr-diffblue Apr 27, 2018

tautschnig Apr 27, 2018

tautschnig Apr 27, 2018

tautschnig Apr 27, 2018

tautschnig Apr 27, 2018

chrisr-diffblue left a comment

peterschrammel left a comment •

edited

Loading

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

kroening May 20, 2018

tautschnig commented May 21, 2018

peterschrammel commented May 21, 2018 •

edited

Loading

tautschnig commented May 21, 2018 •

edited

Loading

peterschrammel left a comment

		======

		Compiling produces an executable called symex which by default can be found in `jbmc/src/jbmc/jbmc`

remove usage of Java bytecode frontend #2118

remove usage of Java bytecode frontend #2118

Conversation

kroening commented Apr 26, 2018

chrisr-diffblue commented Apr 27, 2018

tautschnig 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

chrisr-diffblue left a comment

Choose a reason for hiding this comment

peterschrammel left a comment • edited Loading

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented May 21, 2018

peterschrammel commented May 21, 2018 • edited Loading

tautschnig commented May 21, 2018 • edited Loading

peterschrammel left a comment

Choose a reason for hiding this comment

peterschrammel left a comment •

edited

Loading

peterschrammel commented May 21, 2018 •

edited

Loading

tautschnig commented May 21, 2018 •

edited

Loading