Refactoring in specialization of generic classes #1664

majakusber · 2017-12-11T12:32:55Z

Refactoring the building of the specialized name of a class.

smowton

A few comments on comments; otherwise LGTM.

smowton · 2017-12-11T13:27:00Z

src/java_bytecode/generic_arguments_name_buildert.cpp

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+ Module: Generic Arguments Name Builder - A class to aid in building the name


Normally this is a short name (probably Generic Arguments Name Builder) then there is a /// file comment below giving the more verbose description

smowton · 2017-12-11T13:29:14Z

src/java_bytecode/generate_java_generic_type.cpp

+        ++generic_argument_p;
+        ++implicit_generic_type_p;
+        if(
+          implicit_generic_type_p ==


Add this to the while condition instead?

smowton · 2017-12-11T13:29:41Z

src/java_bytecode/generate_java_generic_type.cpp

    std::string current_outer_class_name;

-    while(implicit_generic_type_p != implicit_generic_types_end)
+    while(implicit_generic_type_p !=


These nested loops are quite complicated; suggest adding comments including a short example of what's going on.

smowton · 2017-12-11T13:30:16Z

src/java_bytecode/generate_java_generic_type.cpp

 /// Build a unique name for the generic to be instantiated.
 /// \param existing_generic_type The type we want to concretise
 /// \param original_class
 /// \return A name for the new generic we want a unique name for.
-irep_idt generate_java_generic_typet::build_generic_name(
+std::string generate_java_generic_typet::build_generic_name(


Add a short example of what sort of name this can produce to the doxy comments

mgudemann · 2017-12-12T12:17:57Z

src/java_bytecode/Makefile

@@ -3,6 +3,7 @@ SRC = bytecode_info.cpp \
      ci_lazy_methods.cpp \
      ci_lazy_methods_needed.cpp \
      expr2java.cpp \
+      generic_arguments_name_buildert.cpp \


I think in general the files do not end on t, only the types

Originally I had it without the t but Linter was complaining about it. It said something like - class names need to end with t.

The linter is wrong if it requires the file to end in a t, but the type definitely should (i.e. the type and the file end up with different names)

I see, will do, thanks!

mgudemann · 2017-12-12T12:18:57Z

src/java_bytecode/generic_arguments_name_buildert.h

+{
+public:
+  generic_arguments_name_buildert(
+    const std::function<std::string(reference_typet)> &argument_name_builder)


this seems to be problematic for Appveyor, does #include <functional> help?

Thank you, I will try that.

mgudemann · 2017-12-12T12:20:15Z

src/java_bytecode/generate_java_generic_type.cpp

+      if(is_java_array_tag(id))
+      {
+        std::string name;
+        name.append(pretty_print_java_type(id2string(id)));


why create an empty string and append to it? Better create the initial string with that content.

thk123

Thanks for doing this clean up, can I ask for a TG pointer bump to just verify we've not inadvertently broken anything!

The main change I'd like to see is my comment regarding the nested while loop

thk123 · 2017-12-12T15:34:48Z

src/java_bytecode/generate_java_generic_type.cpp

-    build_generic_name(existing_generic_type, class_definition);
+  // Small auxiliary function, to print a single argument name.
+  std::function<std::string(reference_typet)> build_argument_name =
+    [&](const reference_typet &argument)


I think best practise here is to specify what you are capturing by reference, whereas & on its own captures everything. I think in this case, nothing is being captured and you can simply to [](const ref...). In fact, it might be best to pull this into a static function and just pass that in?

Removing &, thank you for catching that. For pulling it out into a static function - there is another lambda function below it, I thought for the consistency it may make sense to keep it here. Or is it extensive enough to pull out?

I don't have a strong preference. It is quite long but I also agree about the consistency - as you think best :)

I agree it would be best to pull it in a static function: it's quite long for a lambda and the function it's in is getting too long. Regarding the other lambda below, I think it should go directly in the for_each argument since it is used only once.

Pulling out as a static function.

thk123 · 2017-12-12T15:43:49Z

src/java_bytecode/generate_java_generic_type.cpp

-        implicit_generic_types_end,
-        current_outer_class_name);
+      // build the list of generic arguments using a helper class
+      generic_arguments_name_buildert build_generic_arguments(


If you move the creation of the name builder outside the while loop and instead each loop check whether the name has changed and if it has, finalise the builder (which should empty the vector), it has the advantages that:

You can do away with nested loop

Your main loop can be a regular range based for loop rather than using iterators

The downside is that you can't use the constructor to set the name, but probably some useful function names like start_building_generic_type_list(const irep_idt &type name); would help wit this.

I think the main advantage is actually it means that each step of the outer loop deals with precisely one variable, which is what it is stepping over, rather than an arbitrary number.

Thank you, I was thinking how to get rid of those two loops. The constructor for arguments list does not require a class name, it only holds a vector of arguments at prints them at finalize() so no additional function needed.

thk123 · 2017-12-12T15:45:34Z

src/java_bytecode/generate_java_generic_type.cpp

+      while(
+        implicit_generic_type_p !=
+          implicitly_generic_original_class.implicit_generic_types().end() &&
+        (*implicit_generic_type_p).get_parameter_class_name() ==


With above comment should be able to get rid of the iterators, but for future reference, prefer the -> syntax:

implicit_generic_type_p->get_parameter_class_name()

As reduces noise on the line (two vs four non-alphanumeric characters) and reads more naturally (I don't have to first evaluate the bracket then the dot).

thk123 · 2017-12-12T15:58:16Z

src/java_bytecode/generate_java_generic_type.cpp

+      // and the next implicit generic type is `Class1$Class2$Class3$Class4::T`
+      // with class name `Class1$Class2$Class3$Class4` then this adds
+      // `$Class3$Class4` to the buffer
+      generic_name_buffer << (*implicit_generic_type_p)


I consider this to be a little "clever", which I think is best avoided where possible. If you can't think of a simpler way to achieve this (I can't), I think adding some assertions to check this is reasonable (e.g. get_parameter_class_name().substr(0, substr(current_outer_class_name.length()) == current_outer_class_name) might make it a little more obvious what you are trying to do.

Also consider pulling it into a function add_non_generic_classes_to_name so simplifies this code.

I added a local variable previous_outer_class_name and check using has_prefix that the previous is a prefix of the current name. This also has the advantage that is aids checking that implicit generic types are indeed ordered as expected.

thk123 · 2017-12-12T16:00:27Z

src/java_bytecode/generate_java_generic_type.cpp

+    generic_arguments_name_buildert build_generic_arguments(
+      build_argument_name);
+
+    while(generic_argument_p !=


This can definitely be a range based for loop

for(const reference_typet &generic_argument : existing_generic_type.generic_type_arguments()) { build_generic_arguments.add_argument(generic_argument); }

Unfortunately not. generic_argument_p is an iterator over the concrete arguments we want to add, including the ones for outer classes. So by the time the execution reaches this point, the iterator may not be at the beginning of the list but rather somewhere in the middle because some of the arguments have already been used in the loop for implicitly generic case above. There is an invariant few lines above that checks that we still have enough arguments at this point to add to the name.

thk123 · 2017-12-12T16:01:32Z

src/java_bytecode/generate_java_generic_type.h

    const java_generic_typet &existing_generic_type,
-    const java_class_typet &original_class) const;
+    const java_class_typet &original_class,
+    const std::function<std::string(reference_typet)> build_argument_name)


I think you can do const reference_typet & as the argument for the function parameter.

thk123 · 2017-12-12T16:04:53Z

src/java_bytecode/generic_arguments_name_builder.h

+class generic_arguments_name_buildert
+{
+public:
+  generic_arguments_name_buildert(


Since constructor takes one argument it should be marked as explicit.

You may also like to typedef the function type (e.g. typedef std::function<std::string(reference_typet)> type_printert as this documents the intent of the function, allows for you to easily change it (e.g. ad const & to the input param 😉) and makes the code more concise and therefore easier to read.

majakusber · 2017-12-12T16:35:48Z

@thk123 The pointer bump is here: https://github.com/diffblue/test-gen/pull/1293

thk123

I have some suggestions, but none require a re-review - let me know when you're happy to have this merged.

thk123 · 2017-12-13T13:44:59Z

src/java_bytecode/generate_java_generic_type.cpp

@@ -19,6 +20,34 @@ generate_java_generic_typet::generate_java_generic_typet(
    message_handler(message_handler)
 {}

+// Small auxiliary function, to print a single generic argument name.


No reason not to use doxygen style here (just an extra /)

thk123 · 2017-12-13T13:48:47Z

src/java_bytecode/generate_java_generic_type.cpp

+        generic_arguments_name_buildert build_generic_arguments(
+          argument_name_printer);
+
+        // precondition to check that the implicit generic types are ordered


Preconditions are supposed to be preconditions for a function call, instead, since you've already written a message that explains why this must be true, consider:

INVARIANT( has_prefix(current_outer_class_name, previous_outer_class_name), "Implicit generic types must be ordered from the outermost outer class inwards");

thk123 · 2017-12-13T13:53:29Z

src/java_bytecode/generate_java_generic_type.h

    const java_generic_typet &existing_generic_type,
-    const java_class_typet &original_class) const;
+    const java_class_typet &original_class,
+    const std::function<std::string(const reference_typet &)>


I think using generic_arguments_name_buildert::name_printert might be clearer, even if not to many fewer characters

thk123 · 2017-12-13T13:53:52Z

src/java_bytecode/generate_java_generic_type.cpp

  const java_generic_typet &existing_generic_type,
-  const java_class_typet &original_class) const
+  const java_class_typet &original_class,
+  const std::function<std::string(const reference_typet &)>


I think using generic_arguments_name_buildert::name_printert might be clearer, even if not to many fewer characters

thk123 · 2017-12-13T13:58:37Z

src/java_bytecode/generate_java_generic_type.cpp

+        // add the arguments of the previous generic outer class to the
+        // buffer and reset the builder
+        generic_name_buffer << build_generic_arguments.finalize();
+        generic_arguments_name_buildert build_generic_arguments(


You are declaring a new generic_arguments_name_buildert which hides the previously declared one and is being destructed at the end of the if statement which I think is not intentional - I think this line can just be removed.

thk123 · 2017-12-13T14:21:48Z

src/java_bytecode/generate_java_generic_type.cpp

+
+        // add the remaining part of the current generic outer class name to
+        // the buffer
+        generic_name_buffer << current_outer_class_name.substr(


Consider adding an examples of what original_class_name, current_class_name will be so people can see how this is working.

E.g

// current_outer_class = A.B.C // previous_outer_class = A // Then substr of current, starting at the length of previous is .B.C

thk123 · 2017-12-13T14:42:02Z

src/java_bytecode/generate_java_generic_type.cpp

  }
  else
  {
    generic_name_buffer << original_class_name;
  }

-  // if the original class is generic, add tag for the class itself
+  // if the original class is generic, add generic arguments for the class
+  // itself
  if(is_java_generic_class_type(original_class))


Suggestion for further improvement: I think you can squash the two loops (implicitly generic and the explicitly generic) together by iterating of the instantiated list and storing an iterator into the implicitly generic types. Then when the implicitly generic iterator reaches the end, you know you are at the real class

Something like:

current_inner_class inner_class_param_p = implicitly_generic_original_class.implicit_generic_types().begin(); for(const reference_typet &instantiated_param : existing_generic_type.generic_type_arguments()) { if(inner_class_param_p == end) append the rest of the type if(inner_class_param->get_class_name() != old_name) finalize the last list add the substring part of the name add_argument(param); if(inner_class_param_p != end) ++inner_class_param_p; }

Let me know if that doesn't make sense.

Nice! I needed to first create a vector containing all implicit generic and generic types, so that I can iterate over them all, but this still reduced the length of the function by quite a bit and made it more readable I think. Thank you.

Refactoring the building of the specialized name of a class

thk123

This looks great, will merge pending CI

67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104 fabc99e Merge pull request diffblue#1563 from NathanJPhillips/feature/lazy-loading 2d67e42 Merge pull request diffblue#1692 from NathanJPhillips/feature/numbering-at 5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212 4f4a9c7 Add at method to template_numberingt d9cc0c0 Merge pull request diffblue#1685 from peterschrammel/remove-existing-coverage-goals f13c871 Update a comment in instrument_cover_goals 6c39443 Remove existing coverage goals a2cf16d Store symbol type instead of followed type when clean casting f96efb4 Change template parameter name to not clash with existing type b0cd57b Encapsulate lazy_goto_modelt::goto_functions ef02f4d Update test to handle changed symbol creation order 441d269 Reset counter used by get_fresh_aux_symbol in unit tests f759f25 Fix new test to run remove_java_new pass cb09d8e Fix new tests to use lazy loading 166563f Do lowering of java_new as a function-level pass 3779782 Always convert the main function from bytecode into the symbol_table 7e52e22 Always allow the main function not to have a body c938b08 Encapsulate maps in language_filest 87c6b28 Don't erase symbol in java_bytecode_convert_methodt::convert e3e44c8 Do type-checking as a function pass 2ba1364 Update load_all_functions 5f06e36 Recreate initialize in final aa5440b Moved call to final to lazy_goto_modelt::finalize a659bc0 Add lazy_goto_functions_mapt 7e1ecc9 Allow post-processing functions to run on a function-by-function basis 0c05be6 Allow convert_lazy_method on functions that don't have a lazy body 05a8da2 Make goto_convert_functions not add directly to function map c078858 Introduce lazy_goto_modelt a22dd1c Merge pull request diffblue#1671 from thk123/bugfix/TG-1278/correct-access-level 5b6eb00 Merge pull request diffblue#1668 from romainbrenguier/bugfix/string-index-of#TG-1846 9062853 Tidied up the generic specalised class copying the base class visibility f934ca3 String classes should be public 7b06a00 Merge pull request diffblue#1498 from smowton/smowton/feature/call_graph_improvements f3b4c9b Test for verification of the indexOf method 9a7fa2d Correct lower bound in String indexOf 682cd1a Use a symbol generator to avoid name clashes 28a2ada Access in empty array should be unconstrained d41403f Merge pull request diffblue#1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808 ac7e649 Use CProverString function in jbmc tests 22dc353 Add CProverString class for jbmc-strings tests ef610b3 Use CProverString functions in strings-smoke-tests 5c716c1 Add a CProverString class for string-smoke-tests 6b619e0 Deactivate preprocessing of charAt and substring bcfaaa4 Merge pull request diffblue#1664 from svorenova/refactoring_tg1190 c2a8bae Refactoring in specialization of generic classes 7a98e15 Rename call graph constructors 6228ed3 Slice global inits: use improved call graph d136bbc Expose limited call graph via goto-instrument 9c29bee Improve call graph unit tests 8ed3ccb Add documentation to call graph 8f6f429 Add call graph helpers 3b06a16 Call graph: add constructors that only include reachable functions 9b65862 grapht: add get_reachable function aaa8513 Call graph -> grapht transformation 8115248 Call graph: optionally record callsites git-subtree-dir: cbmc git-subtree-split: 67ec6f2

majakusber requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners December 11, 2017 12:32

majakusber force-pushed the refactoring_tg1190 branch 3 times, most recently from f52efd3 to beef7aa Compare December 11, 2017 12:38

smowton approved these changes Dec 11, 2017

View reviewed changes

majakusber force-pushed the refactoring_tg1190 branch from beef7aa to e289a37 Compare December 12, 2017 11:39

mgudemann suggested changes Dec 12, 2017

View reviewed changes

majakusber force-pushed the refactoring_tg1190 branch 3 times, most recently from 36ea7a9 to 19fd872 Compare December 12, 2017 15:51

thk123 suggested changes Dec 12, 2017

View reviewed changes

majakusber force-pushed the refactoring_tg1190 branch 2 times, most recently from a6c39f1 to 1da5a90 Compare December 13, 2017 11:16

mgudemann approved these changes Dec 13, 2017

View reviewed changes

thk123 reviewed Dec 13, 2017

View reviewed changes

Refactoring in specialization of generic classes

c2a8bae

Refactoring the building of the specialized name of a class

majakusber force-pushed the refactoring_tg1190 branch from 1da5a90 to c2a8bae Compare December 13, 2017 15:49

thk123 approved these changes Dec 13, 2017

View reviewed changes

thk123 merged commit bcfaaa4 into diffblue:develop Dec 14, 2017

majakusber deleted the refactoring_tg1190 branch December 14, 2017 10:23

		@@ -0,0 +1,37 @@
		/*******************************************************************\

		Module: Generic Arguments Name Builder - A class to aid in building the name

Refactoring in specialization of generic classes #1664

Refactoring in specialization of generic classes #1664

Conversation

majakusber commented Dec 11, 2017

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

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

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

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

majakusber commented Dec 12, 2017

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 left a comment

Choose a reason for hiding this comment