Refactor java_bytecode_convert_methodt::convert_instructions #2069

romainbrenguier · 2018-04-16T09:27:41Z

The goal of this PR is to reduce the size of this huge method without changing its behaviour, mainly by extracting some bits into new methods.

tautschnig

The last two commits are rather impossible to review for me at the moment (requires a big screen); detailed comments for the first two only.

tautschnig · 2018-04-16T09:48:10Z

src/util/invariant.h

+    if(!(CONDITION))                                                           \
+      invariant_violated_string(                                               \
+        __FILE__, __this_function__, __LINE__, (REASON)); /* NOLINT */         \
+  } while(false)


Which are these "some" warnings? 2) The previous code even worked within C code, while this is now C++; is that really necessary? 3) Please place this commit in a separate PR.

CLion warnings when INVARIANT is used 2. false is already used in this file, so I don't think this changes anything. 3. done here: Use bool literal in while loop #2078

tautschnig · 2018-04-16T09:53:05Z

src/java_bytecode/java_bytecode_convert_method.cpp

-    address_mapt::iterator a_it=address_map.find(*cur);
-    CHECK_RETURN(a_it != address_map.end());
+    auto cur = working_set.begin();
+    auto a = address_map.at(*cur);


I don't think this is semantics preserving: the previous code would result in modifications to the mapped element, while all those now happen on a copy. auto is dangerous.

tautschnig · 2018-04-16T09:53:53Z

src/java_bytecode/java_bytecode_convert_method.cpp

-      i_it=instructions.begin();
-      i_it!=instructions.end();
-      i_it++)
+  for(auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)


I'm not sure I see much value in this change.

tautschnig · 2018-04-16T09:57:06Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  java_bytecode_convert_methodt::address_mapt &address_map,
+  std::vector<unsigned int> &jsr_ret_targets,
+  const std::vector<
+    std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>


Please introduce a typedef, this is very hard to parse for humans, and the same type is used multiple times.

tautschnig · 2018-04-16T09:58:48Z

src/java_bytecode/java_bytecode_convert_method.cpp

+    &i_it,
+  const std::pair<
+    std::map<unsigned int,
+             java_bytecode_convert_methodt::converted_instructiont>::iterator,


You only ever use a_entry.first->second, so pass some simpler member.

romainbrenguier · 2018-04-17T08:00:07Z

@tautschnig

The last two commits are rather impossible to review for me at the moment (requires a big screen); detailed comments for the first two only.

I currently trying to split these commits, so if you wait a bit, it should become easier to review

peterschrammel · 2018-05-10T11:49:41Z

@romainbrenguier, what's the status of this?

romainbrenguier · 2018-06-01T12:43:30Z

@peterschrammel I just rebased

peterschrammel

Thanks @romainbrenguier for this extensive piece of work. Please check all methods that you have added whether you can make them or some of their parameters const.

peterschrammel · 2018-06-11T09:57:49Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+void java_bytecode_convert_methodt::convert_multianewarray(
+  const std::vector<java_bytecode_parse_treet::instructiont>::const_iterator
+    &i_it,
+  exprt &arg0,


Make parameters const where possible

peterschrammel · 2018-06-11T09:58:44Z

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

+    exprt &arg0,
+    exprt::operandst &op,
+    codet &c,
+    exprt::operandst &results);


Make methods const where possible.

LAJW

Good extracting, the only complaint I have is that it's a little bit too greedy - functions you've extracted take in too much state. Rather than passing in an [out] parameter(s), you should return the value. Many times you're using only a single field/object from the object being passed in. The function becomes unnecessarily complex, and if anyone were to write unit tests for it, he'd have to create a huge object, where only a single sub element of it is tested and actually matters. Also variable names could be expanded c, a, arg0.

LAJW · 2018-06-05T10:29:07Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

        assert(
          next!=instructions.end() &&
          "jsr without valid return address?");
+        auto next = i_it + 1;


FYI: You could replace that with std::next(i_it).

LAJW · 2018-06-11T10:53:11Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2720,6 +2710,22 @@ codet java_bytecode_convert_methodt::convert_instructions(
  return code;
 }

+void java_bytecode_convert_methodt::add_try_catch_handler_to_target(
+  const java_bytecode_convert_methodt::methodt &method,


Passing the entire method might not be necessary, you're just using the exception_table in the function body.

LAJW · 2018-06-11T10:56:42Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    if(address >= exception_row.start_pc && address < exception_row.end_pc)
+    {
+      instruction.successors.push_back(exception_row.handler_pc);
+      targets.insert(exception_row.handler_pc);


Thought: this method could've returned a vector of unsigned ints, rather than storing results to two seemingly unrelated containers. Those containers only make sense from the point of view of the outer algorithm, but not necessarily from here.

LAJW · 2018-06-11T10:58:20Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+    &ret_instructions) const
+{ // Draw edges from every `ret` to every `jsr` successor. Could do better with
+  // flow analysis to distinguish multiple subroutines within the same function.
+  for(const auto retinst : ret_instructions)


Unnecessary copying. Use const auto&.

LAJW · 2018-06-11T11:00:05Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

    auto cur = working_set.begin();
+    auto &a = address_map.at(*cur);


A more descriptive name would be appreciated.

Also, keep in mind, that .at throws on failure. If you want this to behave like an invariant, you have to mark this function noexcept. And the thing to keep in mind about noexcept it doesn't work in Visual Studio 2013 IIRC, so you'll have to resort to some kind of macro.

LAJW · 2018-06-11T11:04:09Z

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+  {
+    results.resize(1);
+    results[0] = zero_initializer(
+      return_type, location, namespacet(symbol_table), get_message_handler());


This looks like an ideal candidate for an optional return.

peterschrammel

LGTM modulo TG bump passing

e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d

romainbrenguier requested review from cesaro, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners April 16, 2018 09:27

romainbrenguier force-pushed the refactor/convert_instruction branch from 7501cb7 to fd8ff2f Compare April 16, 2018 09:42

tautschnig reviewed Apr 16, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/convert_instruction branch from fd8ff2f to 6d4e243 Compare April 16, 2018 10:23

romainbrenguier added the In progress label Apr 17, 2018

romainbrenguier force-pushed the refactor/convert_instruction branch 6 times, most recently from ebfa42b to 9bcd5f0 Compare April 18, 2018 09:05

romainbrenguier removed the In progress label Apr 18, 2018

peterschrammel added the Java Front End label Apr 28, 2018

peterschrammel added the Needs rebase label May 10, 2018

tautschnig assigned romainbrenguier May 15, 2018

romainbrenguier force-pushed the refactor/convert_instruction branch from 9bcd5f0 to 8a4ed59 Compare June 1, 2018 10:03

romainbrenguier requested a review from LAJW June 1, 2018 10:04

romainbrenguier force-pushed the refactor/convert_instruction branch from 8a4ed59 to 55580d2 Compare June 1, 2018 12:45

romainbrenguier removed the Needs rebase label Jun 1, 2018

peterschrammel reviewed Jun 11, 2018

View reviewed changes

LAJW approved these changes Jun 11, 2018

View reviewed changes

romainbrenguier added 24 commits June 13, 2018 09:07

Extract convert_iinc function

305ede8

Extract convert_ushr function

5a5788c

Extract convert_cmp function

3049281

Extract convert_cmp2 function

6f0f3fb

Remove redundant assert

68bddf1

Extract convert_getstatic function

f1edff9

Extract convert_putfield function

27af4a2

Extract convert_putstatic function

b846798

Extract convert_new function

f8d00f6

Extract convert_newarray function

edc4a28

Extract convert_multianewarray function

48dd97f

Extract convert_monitorenter function

0aa1c8e

Extract do_exception_handling function

a7bbf53

Extract convert_monitorexit function

21e37a8

Extract convert_athrow function

4c28f99

Extract convert_checkcast function

0a521a4

Extract replace_calls_to_cprover_assume function

fcfca08

Extract convert_invoke function

d627638

Extract convert_const function

51f53ca

Extract convert_dup2 function

e0735af

Extract convert_dup2_x1 function

66cf709

Extract convert_dup2_x2 function

f2acb00

Extract convert_switch function

cd98a1f

Extract convert_pop function

67081d5

romainbrenguier force-pushed the refactor/convert_instruction branch 2 times, most recently from 110461d to 67081d5 Compare June 13, 2018 08:18

peterschrammel approved these changes Jun 13, 2018

View reviewed changes

romainbrenguier merged commit 8fac5ed into diffblue:develop Jun 13, 2018

romainbrenguier deleted the refactor/convert_instruction branch June 13, 2018 19:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor java_bytecode_convert_methodt::convert_instructions #2069

Refactor java_bytecode_convert_methodt::convert_instructions #2069

romainbrenguier commented Apr 16, 2018

tautschnig left a comment

tautschnig Apr 16, 2018

romainbrenguier Apr 17, 2018

tautschnig Apr 16, 2018

tautschnig Apr 16, 2018

tautschnig Apr 16, 2018

tautschnig Apr 16, 2018

romainbrenguier commented Apr 17, 2018

peterschrammel commented May 10, 2018

romainbrenguier commented Jun 1, 2018

peterschrammel left a comment

peterschrammel Jun 11, 2018

peterschrammel Jun 11, 2018

LAJW left a comment •

edited

Loading

LAJW Jun 5, 2018

LAJW Jun 11, 2018

LAJW Jun 11, 2018

LAJW Jun 11, 2018

LAJW Jun 11, 2018

LAJW Jun 11, 2018

peterschrammel left a comment

		auto cur = working_set.begin();
		auto &a = address_map.at(*cur);

Refactor java_bytecode_convert_methodt::convert_instructions #2069

Refactor java_bytecode_convert_methodt::convert_instructions #2069

Conversation

romainbrenguier commented Apr 16, 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

romainbrenguier commented Apr 17, 2018

peterschrammel commented May 10, 2018

romainbrenguier commented Jun 1, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LAJW 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

peterschrammel left a comment

Choose a reason for hiding this comment

LAJW left a comment •

edited

Loading