[TG-1419] Specialization of generics #1877

majakusber · 2018-02-22T18:02:32Z

This re-implements the specialization of generics - instead of creating new symbols in the symbol table for a specialized generic type, we usep a map of pairs: generic parameter -> stack of types, to keep track of the concrete type of parameters in each context (and context depth). Moreover, the implementation also works with generic superclasses and interfaces, which was not the case in the old version.

mgudemann

one question, why are some of the unit test class / java files deleted ?

mgudemann · 2018-02-23T06:49:32Z

src/java_bytecode/ci_lazy_methods.cpp

+  // we pass an empty map to convert pointer type as we do not need to
+  // record the mapping of generic parameters to concrete types in the
+  // current context at this point (we are not initializing objects, just
+  // loading necessary classes). all the types that we need to load for


typo . all -> . All

mgudemann · 2018-02-23T06:50:48Z

src/java_bytecode/java_object_factory.cpp

+  /// Note that in different depths of the scope the parameters can be
+  /// specialized with different types so we keep a stack of types
+  /// for each parameter.
+  std::unordered_map<irep_idt, std::stack<reference_typet>, irep_id_hash>


please use a typedef for this

mgudemann · 2018-02-23T06:53:33Z

src/java_bytecode/java_object_factory.cpp

+  /// controlled map.
+  ~generic_recursion_map_keyst()
+  {
+    for(const auto key : erase_keys)


I would prefer a std::remove_if here

I'm not quite sure how to use it here. For each key we just pop from its stack, but don't remove the key itself from the map (unless the stack becomes empty).

mgudemann · 2018-02-23T07:22:37Z

src/java_bytecode/java_object_factory.cpp

+    }
+  }
+
+  generic_recursion_map_keyst(const generic_recursion_map_keyst &) = delete;


would you mind adding a comment here to explain what this does?

mgudemann · 2018-02-23T07:24:14Z

src/java_bytecode/java_object_factory.cpp

+    const std::vector<reference_typet> &types)
+  {
+    INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
+    PRECONDITION((parameters.size() == types.size()) && parameters.size() > 0);


!parameters.empty() && ( ..size() == ...size())

mgudemann · 2018-02-23T07:25:05Z

src/java_bytecode/java_object_factory.cpp

+  {
+    INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
+    PRECONDITION((parameters.size() == types.size()) && parameters.size() > 0);
+    for(size_t i = 0; i < parameters.size(); i++)


why not ranged for over parameters ?

I need the index of the current parameter to retrieve the type at the same index from types.

mgudemann · 2018-02-23T07:31:31Z

src/java_bytecode/java_types.h

+  void replace(const typet &argument, const typet &type)
+  {
+    PRECONDITION(is_reference(type));
+    for(auto &arg : generic_type_arguments())


std::replace_if ?

mgudemann · 2018-02-23T07:42:24Z

src/java_bytecode/java_types.h

+/// generic class type, false otherwise
+inline const bool is_java_any_generic_class_type(const typet &type)
+{
+  const bool value = is_java_generic_class_type(type) ||


the intermediate variable isn't needed here

majakusber · 2018-02-23T09:43:50Z

@mgudemann I deleted the folder unit/java_bytecode/generate_concrete_generic_type which contained unit tests for checking whether a new symbol was created in the symbol table for specialized generic classes with correct types. Now we do not create such a symbol, the specialization is now done on-the-fly. I also removed some utility functions used in those tests only.

thk123

Got to commit Adding and updating unit tests so appologies if comments are addressed in later commits

thk123 · 2018-02-23T11:27:09Z

src/java_bytecode/java_object_factory.cpp

@@ -68,6 +68,17 @@ class java_object_factoryt
  /// this set AND the tree depth becomes >= than the maximum value above.
  std::unordered_set<irep_idt, irep_id_hash> recursion_set;

+  /// Every time the non-det generator visits a type and the type is generic
+  /// (either a struct or a pointer), all its generic parameters must have
+  /// a concrete type at this point (otherwise an object cannot be created).


This comment doesn't seem quite correct (it isn't the case that they must since the function might be generic)

thk123 · 2018-02-23T13:43:36Z

src/java_bytecode/java_object_factory.cpp

+      (*generic_recursion_map.find(key)).second.pop();
+      if((*generic_recursion_map.find(key)).second.empty())
+      {
+        generic_recursion_map.erase(key);


Does it not need to restore the old value?

We pop from the stack once (three lines above), so the old value is now the top value. We only remove the whole entry for the key if the stack is empty.

thk123 · 2018-02-23T15:04:46Z

src/java_bytecode/java_types.h

+/// \param type Source type
+/// \return The vector of implicitly generic and generic type parameters of
+/// the given type.
+inline const std::vector<java_generic_parametert> get_all_generic_parameters


Why are these methods marked as inline?

The functions are reasonably small (at least the first one) and may end up being called quite often, I thought. Would you remove the inline?

In C++ inline no longer means inline this function. It is, at best, a hint to the compiler that this might be a good candidate to inline.

Modern compilers will ignore this as they (almost) always know better and will inline according to their own criteria (including functions that are not marked inline). Instead, it is mainly for AFAIK allowing more than one definition.

I see, thanks for the link. I will remove the inline then.

Seems that to keep the functions in the header (which I think makes sense, since similar functions for java types are in the header too) I have to keep the inline. Otherwise I get errors about multiple definitions.

Since non-trivial I would favour in the cpp file, but just preference

Since I only used this function while updating the generic map and I pulled that map into a separate file, I moved the function to that file and it's not inlined anymore.

thk123 · 2018-02-23T15:06:13Z

src/java_bytecode/java_types.h

+/// \param type The type to check
+/// \return True if the given type is a generic class type or an implicitly
+/// generic class type, false otherwise
+inline const bool is_java_any_generic_class_type(const typet &type)


I'm not sure this method improves readability - I wouldn't know what "any generic class" means so would have to look it up, probably would prefer to just use the condition. Or better yet if we can come up with a better name (I'll have a think)

is_class_with_generic_parameter?

One option would be to have java_explicitly_generic_class_type and java_implicitly_generic_class_type that would both extend java_generic_class_type (there is already a class like this but it's meaning now is only explicitly generic, not implicitly). Then we could use the word generic everywhere in the code with the expected meaning, only the lower level code would distinguish between the two.

That sounds reasonable - is it a big change? If so, would it be reasonable to do a separate PR?

I think it would make a good sized PR and the issue is independent of this ticket. I can create a Jira ticket for it.

https://diffblue.atlassian.net/browse/TG-2639

I think in the mean time (since we don't know when we're going to get to this TD) I'd rename this function (or eliminate it if you prefer) according to above suggestions

I will remove it for now.

thk123 · 2018-02-23T15:08:46Z

src/java_bytecode/ci_lazy_methods.cpp

+  // current context at this point (we are not initializing objects, just
+  // loading necessary classes). All the types that we need to load for
+  // future specialization must anyway appear on left-hand-side somewhere.
+  const pointer_typet &subbed_pointer_type =


Note to check there is a test verifying this assumption

I'm not sure how to check that the assumption is always true.. any idea what the test should have in it? I was trying to think of an example, something like this:

class A<T> { public T a; } class B extends A<Integer> { } public class base_test { public B f; public A g = new A<Boolean>(); public Integer test() { if(f.a==null && g.a) { return 0; } else if(f.a!=null) { return f.a; } else { return 1; } } }

But this does not compile with an error:

error: bad operand types for binary operator '&&' if(f.a==null && g.a)

Which supports the assumption.

I guess I was just thinking:

public class base_test { public static String test(A<Integer> input) { if(input != null) return input.toString(); else return ""; }

Then this should lazy load Integer.toString()

(even better if it includes another test which is the same except the input type is B .

I tested it, with A<Integer> input it loads the correct method, but not with B input. Will come up with a solution...

I'm happy for this to be spun out into a separate ticket (with appropriate notes for QA) as this is still a big step forward, unless it seems super simple. (Though of course adding a test demonstrating the problem would be appreciated)

It turns out it's not super simple :) I pulled the issue out into a separate ticket https://diffblue.atlassian.net/browse/TG-2664. The ticket contains the example from above.

thk123 · 2018-02-23T15:16:03Z

src/java_bytecode/select_pointer_type.cpp

+    return find_concrete_type(type, generic_recursion_map);
+  }
+  else if(is_java_generic_type(type))
+  {


I don't follow this block - going to come back to it when I've reviewed the test

So if I've understood correctly: this is required because if we have:

class Gen<T> { T field; } class Gen2 { Gen genField; } Gen2<Integer> param;

We need to make sure we map Gen::T -> Gen2::U. Gen2::U is mapped Integer in the generic_recursion_map.

What I don't understand is why can't this first relation be in the map also?

Long term thoughts: when we deal with generic functions, we might have for example that Gen2::U is one of {Object, Integer, String}, then here we'd need duplicate however we handle having multiple types.

Let's discuss this offline tomorrow

This is the tree of calls that happen for your example in the code (hope it's not more confusing than helping):
call gen_nondet_init on pointer to Gen2<Integer> (this adds Gen2::U -> Integer to the map)

call gen_nondet_pointer_init on Gen2<Integer>

call specialize_generics on Gen2<Integer> (this is java generic type - else if branch)

call specialize_generics on Integer (this is not parameter, not generic type - else branch)

call gen_nondet_init on class Gen2

call gen_nondet_struct_init on Gen2

call gen_nondet_init on pointer to Gen as a field of Gen2 (this adds Gen::T -> Gen2::U to the map)

call gen_nondet_pointer_init on Gen

call specialize_generics on Gen (this is java generic type - else if branch)

call specialize_generics on U (this is parameter - if branch) which returns Integer

call gen_nondet_init on class Gen

call gen_nondet_struct_init on Gen

call gen_nondet_init on pointer to T as field of Gen

call gen_nondet_pointer_init on T

call specialize_generics on T (this is parameter - if branch) which returns Integer

So you do have all you need in the map. In specialize_generics, you do not manipulate the map, just recursively go over the generic type (might have multiple and/or nested generic types and parameters in it such as Gen<GenTwo<U, Integer>>).

That is helpful, but I don't see how the result is used anywhere? Seems like the first call adds Get2::U -> Integer to the map, so we don't care when we read it on

- call specialize_generics on U (this is parameter - if branch) which returns Integer

After an offline discussion, I believe this indeed can be reduced to only specialize generics if the type at hand is a generic parameter.

thk123 · 2018-02-23T15:16:41Z

src/java_bytecode/select_pointer_type.h

@@ -21,7 +22,22 @@ class select_pointer_typet
 public:
  virtual ~select_pointer_typet()=default;
  virtual pointer_typet convert_pointer_type(
-    const pointer_typet &pointer_type, const namespacet &ns) const;
+    const pointer_typet &pointer_type,
+    const std::unordered_map<irep_idt,


Probably worth typedefing this type

thk123 · 2018-02-23T15:17:42Z

src/java_bytecode/generate_java_generic_type.cpp

-/// Small auxiliary function, to print a single generic argument name.
-/// \param argument argument type
-/// \return printed name of the argument
-static std::string argument_name_printer(const reference_typet &argument)


Probably worth taking a note of this commit somewhere, as some of the utilities seem like they will be useful?

I agree, I made a note about this function in my notes. I also added a comment in TG-1278 and TG-1871 which seem to be the most relevant open tickets for pretty printing generic types.

thk123 · 2018-02-23T15:21:09Z

unit/testing-utils/require_goto_statements.cpp

+              to_member_expr(superclass_compound);
+
+            if(
+              superclass_member_expr.get_component_name() ==


This condition is hard to follow (partly down to line breaks) consider breaking out the two conditions into intermediate variables

thk123 · 2018-02-23T15:29:38Z

unit/testing-utils/require_goto_statements.cpp

-        if(
-          symbol.get_identifier() == structure_name &&
-          member_expr.get_component_name() == component_name)
+        if(superclass_name.has_value())


I found this a bit hard to follow - might it be simpler to construct the expected expr tree and then check if they are equal?

I only pass irep_ids to this function and to construct the expr, I would need to full types. As mentioned in a comment above, I tried to make things more readable here, let me know if you find it sufficient.

thk123

Nothing blocking on the unit tests, just some suggestions for reducing duplication

thk123 · 2018-02-26T16:52:26Z

unit/goto-programs/goto_program_generics/generic_bases_test.cpp

+
+    WHEN("The entry point function is generated")
+    {
+      const auto &entry_point_function =


In the interest of getting these tests to be as short as possible, I wonder if you could pull out (into this file) hyper specific utilities to:

get the code_blockt for the entry function

get the this pointer assignment (with the checks that there is precisely 1 non-null assignment)

And maybe even getting the rhs of that assignment since that is all we care about

thk123 · 2018-02-26T17:39:36Z

unit/goto-programs/goto_program_generics/generic_parameters_test.cpp

+
+      THEN(
+        "Object 'this' has field 'field_input' of type "
+          "SimpleWrapper<IWrapper>")


Comment needs updating (just of type SimpleWrapper)

And elsewhere in this file I guess

thk123 · 2018-02-26T17:49:46Z

unit/testing-utils/require_goto_statements.cpp

          if(
            member_expr.get_component_name() == component_name &&
-            superclass_compound.id() == ID_member)
+            member_expr.op0().id() == ID_member)


compound() rather than op0

thk123 · 2018-02-26T17:51:30Z

unit/testing-utils/require_goto_statements.cpp

-              superclass_member_expr.symbol().get_identifier() ==
-                structure_name)
+              superclass_expr.get_component_name() == supercomponent_name &&
+              superclass_expr.symbol().get_identifier() == structure_name)


Would still rather if we could de-duplicate this if block with the existing one (i.e. if super class check the super class component then have one bit of code that checks the final component), but it is now much clearer so non-blocking.

thk123 · 2018-02-26T18:02:15Z

src/java_bytecode/select_pointer_type.cpp

+    return find_concrete_type(type, generic_recursion_map);
+  }
+  else if(is_java_generic_type(type))
+  {


So if I've understood correctly: this is required because if we have:

class Gen<T> { T field; } class Gen2 { Gen genField; } Gen2<Integer> param;

We need to make sure we map Gen::T -> Gen2::U. Gen2::U is mapped Integer in the generic_recursion_map.

What I don't understand is why can't this first relation be in the map also?

Long term thoughts: when we deal with generic functions, we might have for example that Gen2::U is one of {Object, Integer, String}, then here we'd need duplicate however we handle having multiple types.

Let's discuss this offline tomorrow

thk123 · 2018-02-26T18:06:21Z

src/java_bytecode/ci_lazy_methods.cpp

+  // current context at this point (we are not initializing objects, just
+  // loading necessary classes). All the types that we need to load for
+  // future specialization must anyway appear on left-hand-side somewhere.
+  const pointer_typet &subbed_pointer_type =


I guess I was just thinking:

public class base_test { public static String test(A<Integer> input) { if(input != null) return input.toString(); else return ""; }

Then this should lazy load Integer.toString()

(even better if it includes another test which is the same except the input type is B .

thk123 · 2018-02-28T15:44:56Z

unit/testing-utils/require_goto_statements.cpp

+  // Retrieve __CPROVER_start
+  const symbolt *entry_point_function =
+    symbol_table.lookup(goto_functionst::entry_point());
+


To avoid crashing probably worth putting a REQUIRE(entry_point_function != nullptr) in here

thk123 · 2018-02-28T15:49:08Z

src/java_bytecode/ci_lazy_methods.cpp

+  // current context at this point (we are not initializing objects, just
+  // loading necessary classes). All the types that we need to load for
+  // future specialization must anyway appear on left-hand-side somewhere.
+  const pointer_typet &subbed_pointer_type =


I'm happy for this to be spun out into a separate ticket (with appropriate notes for QA) as this is still a big step forward, unless it seems super simple. (Though of course adding a test demonstrating the problem would be appreciated)

thk123

Nothing blocking - some final suggestions (all review comments from previous reviews either addressed or re-mentioned in this review)

thk123 · 2018-02-28T15:51:34Z

src/java_bytecode/java_object_factory.cpp

+    const std::vector<reference_typet> &types)
+  {
+    INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
+    PRECONDITION(!parameters.empty() && (parameters.size() == types.size()));


Missed this earlier, but maybe a std::vector<std::pair<java_generic_parametert, reference_typet>> (or even std::mapr<java_generic_parametert, reference_typet>) would encode this precondition at compile time.

And would simplify the below for loop as you could just use a range based for loop over the pairs

Though I see this makes calling this more complicated - up to you what you do here

Yes, I would have to construct the vector of pairs before calling the function and this precondition would have to appear there somewhere anyway. I can create a separate function for the construction and call it at the beginning of this function.

thk123 · 2018-02-28T15:54:43Z

src/java_bytecode/java_object_factory.cpp

+    {
+      const irep_idt &key = parameters.at(i).get_name();
+      const reference_typet &value = types.at(i);
+      // Only add the pair if the type is not the parameter itself. This can


Consider adding an example to this comment as I'm struggling to figure out what it means

This is mapping A::T -> A::T right?

thk123 · 2018-02-28T15:56:18Z

src/java_bytecode/java_object_factory.cpp

+        !(is_java_generic_parameter(value) &&
+          to_java_generic_parameter(value).get_name() == key))
+      {
+        if(!generic_recursion_map.count(key))


Implict conversion from int to bool, replace with == 0

thk123 · 2018-02-28T16:51:04Z

src/java_bytecode/java_object_factory.cpp

+        (*generic_recursion_map.find(key)).second.push(value);
+
+        // We added something, so pop it when this is destroyed:
+        erase_keys.push_back(parameters.at(i).get_name());


parameters.at(i).get_name() = key no?

thk123 · 2018-02-28T16:53:44Z

src/java_bytecode/java_object_factory.cpp

+  {
+    for(const auto key : erase_keys)
+    {
+      PRECONDITION(generic_recursion_map.count(key));


Implicit conversion from int to bool

thk123 · 2018-02-28T16:55:56Z

src/java_bytecode/java_types.h

+/// \param type The type to check
+/// \return True if the given type is a generic class type or an implicitly
+/// generic class type, false otherwise
+inline const bool is_java_any_generic_class_type(const typet &type)


I think in the mean time (since we don't know when we're going to get to this TD) I'd rename this function (or eliminate it if you prefer) according to above suggestions

thk123 · 2018-02-28T16:57:03Z

src/java_bytecode/java_types.h

+/// \param type Source type
+/// \return The vector of implicitly generic and generic type parameters of
+/// the given type.
+inline const std::vector<java_generic_parametert> get_all_generic_parameters


Since non-trivial I would favour in the cpp file, but just preference

thk123 · 2018-02-28T16:58:25Z

src/java_bytecode/java_types.h

+  /// Replace every occurrence of a generic type argument with a given type.
+  /// \param argument generic type argument that should be replaced
+  /// \param type new type that the argument should be replaced with
+  void replace(const typet &argument, const typet &type)


Outstanding without reply:

Ah I know what confused me - method body inside the class definition, would prefer since not completely trivial to move into the source file.

Preference/non-blocking

thk123 · 2018-02-28T17:02:53Z

src/java_bytecode/select_pointer_type.cpp

+    return find_concrete_type(type, generic_recursion_map);
+  }
+  else if(is_java_generic_type(type))
+  {


That is helpful, but I don't see how the result is used anywhere? Seems like the first call adds Get2::U -> Integer to the map, so we don't care when we read it on

- call specialize_generics on U (this is parameter - if branch) which returns Integer

thk123

All previous comments have been addressed, commits look reasonable. This needs for sure the TG pointer bump updating. I also think it is worth reconsidering the name of the generic_recursion_map as I'm not really sure what the recursive element is.

thk123 · 2018-03-02T11:09:51Z

src/java_bytecode/generic_recursion_map_keys.cpp

+/// \return The vector of implicitly generic and (explicitly) generic type
+/// parameters of the given type.
+const std::vector<java_generic_parametert> get_all_generic_parameters
+  (const typet &type)


This formatting looks suspect?

thk123 · 2018-03-02T11:15:33Z

src/java_bytecode/generic_recursion_map_keys.cpp

+  const std::vector<java_generic_parametert> &parameters,
+  const std::vector<reference_typet> &types)
+{
+  PRECONDITION(!parameters.empty() && (parameters.size() == types.size()));


While I agree parameters being empty seems odd, not really a pre-req for this function (in can pair up two empty lists into an empty list of pairs) might not be useful now but in some circumstances might make using this utility more complicated.

You might consider pulling this into a totally templated function in util to pair arbitary vectors in to a vector of pairs,
but no need to do this as part of this PR.

thk123 · 2018-03-02T11:18:43Z

src/java_bytecode/generic_recursion_map_keys.cpp

+{
+  PRECONDITION(!parameters.empty() && (parameters.size() == types.size()));
+  std::vector<std::pair<java_generic_parametert, reference_typet>> vector;
+  for(size_t i = 0; i < parameters.size(); i++)


This SO answer has a way of doing it using std::transform, though I'm not sure it is better.

For consistency, prefer ++i in a for loop (or use iterators)

thk123 · 2018-03-02T11:19:48Z

src/java_bytecode/generic_recursion_map_keys.cpp

+  const std::vector<reference_typet> &types)
+{
+  INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
+  const std::vector<std::pair<java_generic_parametert, reference_typet>>


I'd probably typedef std::vector<std::pair<java_generic_parametert, reference_typet>> somewhere

I removed the function pair_up and the construction is done within insert_pairs so this type is explicitly used only once now.

thk123 · 2018-03-02T11:25:48Z

src/java_bytecode/generic_recursion_map_keys.h

+    const std::vector<java_generic_parametert> &parameters,
+    const std::vector<reference_typet> &types);
+
+public:


Nit: I think it is helpful to keep the public interface at the top of the class

thk123 · 2018-03-02T11:26:06Z

src/java_bytecode/generic_recursion_map_keys.h

+class generic_recursion_map_keyst
+{
+  /// Recursion map to modify
+  generic_recursion_mapt &generic_recursion_map;


Nit: prefer keeping private members at the bottom so easy to see the interface

thk123 · 2018-03-02T11:28:15Z

src/java_bytecode/generic_recursion_map_keys.cpp

+  }
+}
+
+///


Either document or don't 😛

thk123 · 2018-03-02T11:31:57Z

src/java_bytecode/generic_recursion_map_keys.cpp

+}
+
+///
+/// \param pointer_type


docs missing

thk123 · 2018-03-02T11:36:22Z

src/java_bytecode/java_object_factory.cpp

+  /// from the map when the scope changes. Note that in different depths
+  /// of the scope the parameters can be specialized with different types
+  /// so we keep a stack of types for each parameter.
+  generic_recursion_mapt generic_recursion_map;


Is recursion actually the right name? Sorry should have spotted earlier, but it is more of a generic_type_specialisation_map no?

thk123 · 2018-03-02T11:38:26Z

src/java_bytecode/java_types.cpp

+/// with a given type.
+/// \param argument generic type argument that should be replaced
+/// \param type new type that the argument should be replaced with
+void java_generic_typet::replace(const typet &argument, const typet &type)


This method is no longer used I think?

mgudemann

LGTM, two small comments but not blocking of course

mgudemann · 2018-03-02T11:34:20Z

src/java_bytecode/java_types.h

  const std::string get_parameter_class_name() const
  {
-    const std::string &parameter_name =
-      type_variable().get_identifier().c_str();
+    const std::string &parameter_name = get_name().c_str();


why not id2string instead of c_str here?

This function is actually not used anymore (was part of the old implementation for specialization) so will remove.

This still seems to be here? Perhaps removed in a later commit

mgudemann · 2018-03-02T11:35:54Z

unit/goto-programs/goto_program_generics/GenericFields.java

@@ -0,0 +1,99 @@
+// THIS FILE HAS A COPY IN test-gen/unit/test-java-gen


does git allow for symbolic links? we don't have to support Windows in TG

I removed this because the tests in test-gen will be changed to not be just a copy.

thk123

Some suggestions for comments but no need for re-review

thk123 · 2018-03-06T09:23:06Z

src/java_bytecode/generic_parameter_specialization_map_keys.h

+    const typet &symbol_struct);
+
+private:
+  /// Recursion map to modify


Generic parameter map to modify

thk123 · 2018-03-06T09:24:33Z

src/java_bytecode/generic_parameter_specialization_map_keys.cpp

+  }
+}
+
+/// Add pairs of parameters and their types for a generic symbol type to the


Perhaps improve this comment by explaining that the pairs are for each generic parameter and why you would use this overload of the method vs. the above one (e.g. something about being used for the base class?)

thk123 · 2018-03-06T09:24:47Z

src/java_bytecode/generic_parameter_specialization_map_keys.cpp

+  }
+}
+
+/// Add pairs of parameters and their types for a generic pointer type to the


Perhaps improve this comment by explaining that the pairs are for each generic parameter

thk123 · 2018-03-06T14:08:42Z

@marek-trtik This is the PR you will be interested in when it is merged (tagging you so you'll get a notification when merged)

marek-trtik · 2018-03-06T16:15:03Z

@thk123 Thanks a lot!

majakusber · 2018-03-06T17:11:01Z

@thk123 Can you please have one last look? I made some changes to the commit 'Use the map..' so that a replacement pointer type is now created for array types that use generic parameters.

thk123

Will have a detailed look tomorrow - most important question, do you have a test that now passes that previously would have failed?

thk123 · 2018-03-06T17:35:54Z

src/java_bytecode/java_object_factory.cpp

+    (is_reference(replacement_pointer_type) && is_reference(pointer_type) &&
+     to_reference_type(replacement_pointer_type)
+       .
+       operator!=(to_reference_type(pointer_type))))


Don't use .operator!=, just use !=?
Also I'm not sure how this works. Perhaps for readability it could be broken into two local booleans. None the less, I can't see how r == p but casting it using to_reference_type and then checking again can produce a different result?

I replaced the operator with a function called equal_java_types and put it in java_types.cpp

thk123

A unit test with an interface in a package and a unit test with an inner class interface would be good - lets talk tomorrow if this is a sensible thing to spin out or whether should be tacked on.

thk123 · 2018-03-07T17:52:54Z

src/java_bytecode/java_types.h

  const std::string get_parameter_class_name() const
  {
-    const std::string &parameter_name =
-      type_variable().get_identifier().c_str();
+    const std::string &parameter_name = get_name().c_str();


This still seems to be here? Perhaps removed in a later commit

thk123 · 2018-03-07T17:59:08Z

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -151,7 +151,16 @@ static optionalt<std::string> extract_generic_interface_reference(
    start =
      find_closing_semi_colon_for_reference_type(signature.value(), start) + 1;

-    start = signature.value().find("L" + interface_name + "<", start);
+    // if the interface name includes package name, convert dots to slashes
+    std::string interface_name_slash_to_dot = interface_name;


When doing this kind of string manipulation, it is probably worth also checking that inner classes work (since the whole $/. fiasco)

For example (though I guess with some generics in there as well).

class Outer { public interface InnerInterface { } } class TestClass implements Outer.InnerInterface {}

I tried the example, this is not causing a problem since both in class signatures and in our representation we use $ as separator for inner classes.

The map of generic parameters and a stack of their concrete types in the various depths of the current scope.

We now specialize generics on-the-fly using a context-sensitive map of parameter-type pairs

207b801 Merge branch 'develop' into merge_2018-03-26 301cd46 Merge pull request diffblue#1969 from smowton/smowton/cleanup/document_sccs_guarantee 9c04abd Document grapht::SCCs 18478e9 Merge pull request diffblue#1947 from romainbrenguier/dependency-graph/stop-adding-unecessary-constraints#TG-2608 be66b35 Merge pull request diffblue#1961 from danpoe/slice-global-inits-fix 60bfbd0 Reduce string-max-length on String.equals test 50cfe34 Clear constraints at each call to dec_solve 367ca13 Ensure all atomic strings in arguments have node 0bb2fad Define a for_each_atomic_string helper function 805f45f Correct add_constraints in string_dependencies 61b3910 Add length_constraint method to builtin functions 8684e6d Helper functions for length constraints on strings 8a98246 Adapt unit tests for the new interface c3aed85 Define two helper functions for for_each_successor a45c64f Add tests for the use of string dependencies e3da98c Deactivating invariant 2655a9b Rewrite axioms for insert be5f194 Add double quotes to output_dot 4b342f7 Only add constraints on test function dependencies 3c61cf2 Add a hash function for nodes 23f8cd4 Correct name of builtin function with no eval c487c4b Generic get_reachable function 46d2507 Add move constructors to builtin_function_nodet 6609247 Add a maybe_testing_function to builtin functions 97ee2d6 Store builtin function pointer inside builtin node 41c0294 Add constraints from the string dependencies 8a7d194 add_constraints method in string_dependencies b8df2b3 Initialize return_code for all builtin_functions 82f552c Add and add_constraint method to builtin functions 2e7057a Remove use of unknown_dependency 408adbe never return nullptr in to_string_builtin_function c26b83d Constructor for builtin function with no eval 54a4d7d Add class for builtin function with no eval 8e0f974 Merge pull request diffblue#1970 from tautschnig/java-bytecode-fixes edb8eeb Merge pull request diffblue#1905 from smowton/smowton/cleanup/broken-regression-tests c188986 Merge pull request diffblue#1957 from smowton/smowton/cleanup/show-goto-functions-documentation df1c7e3 Builds require javac as of f66288b 1782e8f Include missing map header 55656ff Include missing invariant header 0b17511 Merge pull request diffblue#1955 from svorenova/bugfix_tg2842 eb1ac7b Merge pull request diffblue#1964 from peterschrammel/documentation/online-docs-link 356a96c Merge pull request diffblue#1953 from smowton/smowton/cleanup/document-java-synthetic-methods 19e5bba Document synthetic methods generated by the Java frontend 706ffa7 Make test lambda1 compatible with symex-driven loading 0759129 Clarify slightly that show-symbol-table et al are restricted to loaded symbols d7efdd1 Improve docs TOC structure 4043681 Add online documentation to README 076aa5a Improving warnings for unsupported signatures for generics cont. c63c05b Add unit tests for mocked/unsupported generics cont. 067eeff Refactoring and adding utility functions in require_type 11e9a77 Ignore generic arguments for mocked and unsupported generic classes cont. 3a45ee9 Improving warnings for unsupported signatures for generics f3cdd97 Add unit tests for mocked/unsupported generics 51a5845 Pull out common generic classes/interfaces for unit tests fc83526 Ignore generic arguments for mocked and unsupported generic classes 3b00bdc Fix tests with missing EXIT or SIGNAL tests 7b56203 Merge pull request diffblue#1965 from smowton/smowton/fix/reachability-slicer-incompatible-with-symex-driven-loading 5903b62 Merge pull request diffblue#1952 from diffblue/more-builtins e25a7ac Mark the new reachability-slicer incompatible with symex-driven loading c5b4e19 Merge pull request diffblue#1963 from tautschnig/dimacs-output 4f3fb8b Merge pull request diffblue#1958 from romainbrenguier/bugfix/insert-offset cd184f1 Merge pull request diffblue#1780 from Charliemowood/documentation/review-cbmc-docs 1ee0dd9 Merge pull request diffblue#1943 from forejtv/forejtv/reachability-slicer 9aa70a7 Add doc README.md files to each directory 1b7f57d Use doxygen layout file c22e2e9 Add make doc to Makefile c50f40d Remove old doxygen module directives from header files c1f9e34 Move SATABS references to separate from user manual 42f9f36 Improve docs content layout and front page 0afcf90 dimacs: make sure printing a dimacs is fast a403fdd Fix a bug in slice global inits where guard expressions were disregarded 7e00a30 Merge pull request diffblue#1759 from smowton/smowton/feature/symex-driven-program-loading 22e9b32 Merge pull request diffblue#1960 from smowton/smowton/admin/remove-reuk f10c697 Remove reuk as a code-owner c5aa507 Document builtin function constructors 953e2df Enable show-properties with symex-driven lazy loading 6c79494 Fix broken static_init_order test descriptions ccb2cf3 Fix broken test descriptions 8aa38e7 Add tests for symex-driven lazy loading 7b5d73b JBMC: use symex-driven lazy loading 978ca5b Add callback after symex to bmct 8df9350 Java frontend: rename externally driven loading 98741f9 Java frontend: note availability of synthetic methods 890b8b1 Remove exceptions: add per-function entry point 3ef9ec8 Correct for_each_successor method aebadee Correct offset in eval for insert 71983b3 Remove mention of size in eval_string 4cca831 Move string_builtin_function class to a new file 6120c17 Changes to the reachability slicer f6219d4 Merge pull request diffblue#1940 from smowton/smowton/cleanup/remove-virtual-functions 34b2b02 Merge pull request diffblue#1939 from romainbrenguier/bugfix/builtin-string-insert-eval 9d9fafa Merge pull request diffblue#1941 from diffblue/rotate 84186ff Tests for CProverString.append with start/end args 882bbb1 Fix eval of concatenation builtin functions ad9b86c Fix add_axioms_for_concat_substr b43bbff Tests for CProverString.substring 4be7532 Test for CProverString.insert 5f96226 Fix string constraints for substring 9ff1e82 Fix eval of insert to match string constraints f3694af added support for rotation operators 126e90a Remove virtual functions: fix no-fallback-function mode 442f315 Merge pull request diffblue#1951 from zemanlx/support/public-cprover-documentation 8c501cc Use abstract_goto_modelt instead of goto_functionst in bmc reporting phase 760d1ca Lazy goto model: implement abstract_goto_modelt a4f5d77 goto_modelt: implement abstract_goto_modelt 311ca9c Add abstract_goto_modelt 2fe999c Add gcloud integration to Travis a5c26a8 Add script for uploading documentation 566539e Add encrypted GCloud key for Travis 07bafd2 move CPROVER built-in functions into the factory 7f3ba30 Merge pull request diffblue#1814 from NlightNFotis/flush-json-stream 7161f17 Merge pull request diffblue#1879 from diffblue/smt2-frontend ab68848 tests for smt2_solver 246472f an SMT2 solver using boolbv and satcheckt a75ee3f Add missing langapi dependency to util d83fa17 Merge pull request diffblue#1932 from romainbrenguier/stop-adding-counter-examples b5f12ff Correct initial index set computation c905c2c Remove "Adding counter-examples" message 7085f9c Correct find_index function for `if`-expressions 123be20 Fix goto-diff tests that got broken by streaming json 2ab3b9c Activate JSON streaming when printing goto-traces 54bae24 Refactor huge convert function into multiple ones a68125c Base JSON UI message handler upon json_streamt 35ac459 Introduce class for streaming JSON to the output a2a3140 Correct bounds in instantiate method 0910010 Fix string constraints 7586f76 Only add counter examples when index set exhausted 5268c44 a translator from SMT2 into expressions 6dde6b1 add support for let_exprt 37f69b2 added to_mathematical_function_type 7b670cd fix line number counting in SMT2 tokenizer f3cb5bb Merge pull request diffblue#1938 from romainbrenguier/fix-cmake 213cb57 Fix cmake build 9e11b41 Replace java_int_type by tyep deduced from array fc67510 Get rid of java_bytecode includes in string solver 461b3a5 Merge pull request diffblue#1922 from romainbrenguier/dependency-graph/get-model#TG-2607 1a874b3 Add name method to builtin functions 8d4a057 Decompose if_expr when adding dependencies cb72bb7 Correct insert builtin function construction d0a8868 Constructor and destructor of builtin functions 7bb5aff Make node point to builtin func they result from a89ceb0 Tests for string solver get with new dependencies 0b3796e Declare a nodet class in string_dependencies fb676d5 Add a cache for eval in string dependences 095d57b Add concat_char builtin function for strings 44693e8 Use eval of builtin function in get when available 56cb571 Activate dependency computation in string solver 69f31c1 Add eval function to string_dependenciest 357cb44 Add const node_at function in string dependencies e308bad Rename class to string_dependenciest 06dc6b2 Add an evaluation method to builtin functions f6a153e Check type before adding dependencies 0139424 Fix linting problem in string_constraint 5108a72 Fix string constraints printing a2fab10 Linting corrections in string_refinement 05a3426 Merge pull request diffblue#1925 from hannes-steffenhagen-diffblue/testpl_use_env_testpl 8869dd8 Merge pull request diffblue#1920 from diffblue/bugfix/continue_bootstrapmethods_parsing_after_unsupported_entry d404a55 Merge pull request diffblue#1931 from owen-jones-diffblue/owen-jones-diffblue/fix-release-build-compilation c6102f7 Merge pull request diffblue#1918 from thk123/tests/tg-2485/lambda-lazy-loading 008de5d Use environment variable for jobs in test.pl ea6f00f Fixing linter error 0b20a81 Added explanation to the test 1974010 Adjusted the if check to aid readability 42065ec Adjust the interface of the bootstrap methods map dcd680f Correcting formating on java file d8edf4f Adjusted test to pass c0f054a Removing redundant method from test f494674 Use function that actually contains the lambdas 8615500 Added to readme that the file is compiled using the eclipse compiler a604b26 !fixup Removed impossible condition (9fc5bfd) 12f049e Added extra information to the warnings to differentaite the different cases 1db68a5 Moved the first condition to after the explanation of our assumptions c1aa16c Renamed parameter variables 4bb98f0 Removed impossible condition 9749d5a Refactored error reporting method into a seperate function 6400294 Replace nested else ifs with a continue on error conditions 067ccbf Rename j to boostrap_method_index d7a4e50 Add regression test compiled with ecj e11163c Continue parsing after unsupported BootstrapMethods entry e1961d8 Adding unit tests for verifying the behaviour of lazy methods on lambdas 28c6477 Adding utility for getting symbols out of the symbol table 06ab440 Merge pull request diffblue#1930 from owen-jones-diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods-v1 6eab160 Speed up resolution of virtual callsites in lazy loading v1 c470bdf Replace assert(false) by UNREACHABLE 3af5509 Merge pull request diffblue#1923 from romainbrenguier/author-refinement-util 802b819 Merge pull request diffblue#1926 from tautschnig/fix-json 08ad919 Merge pull request diffblue#1913 from thk123/refactor/lazy-load-java-class-unit-tests 1abbaff Merge pull request diffblue#1927 from peterschrammel/json-xml-timestamps 3864e6c Updating comment with relevant JIRA ticket 72fc31e Add lazy version of load_java_class 5912a04 Refactored java_load_class to allow specifying different cmd line args 9374a1f Remove trailing whitespace from timestamp string 2ae5310 Add timestamp to JSON and XML messages 22b1628 goto-analyzer (un)reachable-functions: build valid json output 1e7f2bc Merge pull request diffblue#1907 from chrisr-diffblue/travis-test-speedups ee2cf14 Correct author entry 2e7f785 Merge pull request diffblue#1895 from romainbrenguier/dependency-graph#TG-2582 86b3e87 Merge pull request diffblue#1919 from mgudemann/enhancement/fix_diffblue_author 123541f Correct string-max-input-length tests 411e654 Unit tests for dependency graph c4ba7b4 Separate pointer/function substitutions in solver a599003 Define function for array_pointer_association a556d3d Pull out a get_function_name function 859d74c Class for string builtin functions and dependences bd8ee51 Define function template for output_dot 0b58e31 Move utility functions to string_refinement_util 68ecd9e Make interface of equation_symbol_mappingt clearer 3e688e0 Create string_refinement_util for utility function e72eacf Pull array_pool class out of constraint generator 42971da Remove default axiom in associate array to pointer f5adb47 Pull symbol generation out of constraint generator e2ca928 DiffBlue -> Diffblue d430ddc Replace copyright notice with author entry 631acab Fix Diffblue author entries e6e5134 Merge pull request diffblue#1911 from thk123/bugfix/TG-2434/static-constructor-calling-opaque-constructor 1a89e97 Remove lambda in favour of direct construction bf86af4 Correcting review comments 44153b7 Adding unit tests verifying initalizsers are correctly labelled 80a439d Apply clang-format 6edaaa0 Remove the uncasted member_type so all references use the correct version e8cbf90 Adding wrappers around whether a code_type is a constructor e5ff31f Replace checks for <init> with a call to is_constructor b25301e Remove redundant method and constructor setter c84cf21 Made member_type_lazy return type match what the method returns 6505e8c Merge pull request diffblue#1875 from peterschrammel/remove-cout-solvers 26ef31c Use invariant instead of abort() fe40b19 Use invariant instead of printing error message to cerr 066ba51 Merge pull request diffblue#1778 from peterschrammel/java-array-is-object 3548d99 Merge pull request diffblue#1917 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-do-not-create-stubs-when-resolving-virtual-calls e7a6769 Merge pull request diffblue#1877 from svorenova/specialized_generics_tg1419 b87661e Do not create stubs when resolving virtual methods 0ac57ba Rename `needed_methods` to `callable_methods` 9fef129 Rename `needed_classes` to `instantiated_classes` 0d524ee Merge pull request diffblue#1893 from diffblue/expression-printer 48024c7 Replace function applications: don't break irep sharing 86bf547 replace_expr: avoid breaking irep sharing 69bef76 Typo in function header c53cb29 Adding and updating unit tests a1e9d00 Updating and extending utility functions 2964910 Fix a bug in function for extracting generic interface reference 5c00440 Remove the old way of specializing generics 624cc91 Use the map of parameter-type pairs to specialize generics 3111255 Introduce a map of parameter-type pairs aaf9477 Use ranged for and const 7018ab4 Clean up commented out code 2529211 Clang-format f7afe1f Replace assert by invariant fc44d99 Use invariant instead if printing error message to cout a15b75f Merge pull request diffblue#1910 from diffblue/builtin-factory 5de436b usage of format() instead of from_expr for debugging b38ecc3 added format() for exprt and typet 2c8ae92 Makefile: use a variable for all those generated .inc files 17d9897 switch to C++ version of find_pattern 80ee0b1 pass type definitions to the C++ front-end 15ec42f use the builtins factory in the C frontend 1711345 added a factory for builtin function declarations 4a5b952 export all gcc bultin headers 691816b Improve job scheduling when running regression tests with -jN 87526e0 Enable a coarse-grained prallelism when running regression test jobs via Makefiles 76b93e8 Factoring out a private code from module 'remove_virtual_functions.cpp'. 15d7b71 Merge pull request diffblue#1908 from mgudemann/bugfix/fix_bootstrapmethods_empty_optional 0fd6482 Add regression test 5fa3a1a Refactor: improve variable naming ae276ef Activate two instanceof regression tests 8995fce Java arrays are instanceof Object 881b127 Refactor: use class_typet instead of struct_typet for java class fdba57c Merge pull request diffblue#1901 from romainbrenguier/fix/quantifier_exprt 782df52 Merge pull request diffblue#1909 from chrisr-diffblue/travis-make-options-cleanup 1edf0e8 Cleanup Travis Makefile build commands 1457849 Merge pull request diffblue#1894 from thomasspriggs/lambdas_compiliers_test 0ed21ca Treat empty optional case separately 3e298ef Formmatting fixes/updates for `java_bytecode_parse_lambda_method_handle` test update. f1ee826 Update `java_bytecode_parse_lambda_method_handle` tests to run for each java compiler. fe34bf6 AWS Codebuild: 4th attempt to speed up install 58b4196 AWS Codebuild: 3nd attempt to speed up install 71ab5cd AWS Codebuild: 2nd attempt to speed up install b95383a Merge branch 'develop' of github.com:diffblue/cbmc into develop e7bb127 AWS Codebuild: avoid one round of apt-get update f20e8d7 Merge pull request diffblue#1891 from diffblue/deprecated-exprt-methods 20fc8d1 Merge pull request diffblue#1363 from diffblue/undeclared-return-conflict 92b4873 Merge pull request diffblue#1791 from thk123/feature/make-irep-ids-modifiable-by-all 2fef8fd Merge pull request diffblue#1772 from tautschnig/fix-1771 f6890b3 modernisation of sum_expr and mul_expr 4d87ba1 remove exprt::negate, sum, mul, subtract (deprecated since 2011) 0d0dca4 Merge pull request diffblue#1839 from thomasspriggs/tidy_up1 1b24851 Merge pull request diffblue#1903 from chrisr-diffblue/travis-speedups b19b4a2 codebuild: enable the tests 44aa443 AWS codebuild: enable ccache 8549ecb AWS codebuild: enable cache a7cc2a0 Merge pull request diffblue#1885 from tautschnig/use-std-expr 6ef804c Merge pull request diffblue#1888 from tautschnig/linker-script-fixes d04312f Use std_{code,expr,type} constructors 00ec070 Slightly increase the number of parallel build jobs f0fc345 Increase ccache size for debug builds 423cd49 Ensure all compile jobs declare their compiler type 7b6f849 Avoid double invoking ccache a75c4f0 attempt 6 to use AWS Codebuild d3ebda0 attempt 5 to use AWS Codebuild a185ae0 fourth attempt to use AWS Codebuild 2948a43 third attempt to use AWS Codebuild 097de57 second attempt to use AWS Codebuild 4331120 first attempt to use AWS Codebuild 5c18ccc Type conflicts on the return value of implicitly declared functions are errors d074537 test for signature conflict with undeclared function 37a11f9 Merge pull request diffblue#1808 from LAJW/lajw/floating-point-to-java-string b3f2320 Add unit test for floating_point_to_java_string 7ac4fda Refactor and expose floating point to java conversion in expr2java.h 1a88479 Merge pull request diffblue#1896 from NathanJPhillips/bugfix/erroneous-reference f5330c9 Correct can_cast_expr for quantifier_exprt 00cc4b1 Merge pull request diffblue#1897 from diffblue/quantifier_exprt 8897709 Merge pull request diffblue#1800 from tautschnig/fix-process_array_expr fd513a6 added a base class for forall_exprt and exists_exprt c3ee2a1 Merge pull request diffblue#1010 from danpoe/no-body-inlining 8d8c2e0 Fix bug causing crash on Windows 4dd0f29 Merge pull request diffblue#1892 from diffblue/remove-OPERANDS_IN_GETSUB b519b41 remove OPERANDS_IN_GETSUB define, which is now simply the only option 80060ea goto-diff is missing dependencies on goto-instrument and goto-symex 7a71c80 Merge pull request diffblue#1884 from mgudemann/enhancement/update_copyright_2018 bb47a84 Merge pull request diffblue#1883 from tautschnig/implement-popcount 90beed4 Merge pull request diffblue#1845 from tautschnig/fix-1837 5cdfa94 Merge pull request diffblue#1804 from mgudemann/feature/parse_bootstrapmethods_attribute ea7975f Remove unused goto_functions parameters 76d4014 Adding tests for inner classes that capture outer class variables 9b8a73e Adding tests for lambdas as member variables db1f3b5 Adding tests for local lambdas ba8b958 Adding tests for static lambdas ebdcfb1 Adding utiltiy functions required for unit tests f79e895 Fix format and account for reviewer's comments 51bb367 Merge pull request diffblue#1886 from smowton/smowton/fix/static-inititialisers-doxygen e0ccb12 Refactor BootstrapMethods attribute reading into function 463ffe1 Refactor parse_method_handle to just deal with the lambda special case ca5dae4 Fixup Use the strcutured classes to simplify and make more explict the code b56e42e Fix missing swap for classt e3ff312 Use the strcutured classes to simplify and make more explict the code 3ac7d09 Introduce classes representing relevant constant pool entries 0e40081 Adding validation on the type of descriptor found 6d44836 Use optionalt<lambda_method_handlet> as return value f765a0d Rename, some more comments 01dcda5 status()->debug() 603aced Add regression test for lambda functions e79a655 Initial support for reading BootstrapMethods attribute b371e28 Linker-scripts: support linker symbols with struct type e999552 Linker-script processing: mind temporaries 1612f74 Do not modify object_files list while processing it 60487f7 Distribute ls_parse.py with goto-cc 631ea60 Make linker-script processing failures non-fatal 1f753d8 fixup! goto-gcc removes CPROVER macros for native gcc 716103e Implement popcount in SAT back-end ddde9dc Introduce popcount_exprt 3e793f5 Merge pull request diffblue#1887 from diffblue/string-constant-to-util 683d821 move ansi-c/string_constant.h to util/ 3188f10 Merge pull request diffblue#1795 from thk123/bugfix/TG-1358/local-variables 0cfd14b Add missing Doxygen parameter 81d2ea4 Update copyright in help output for {CJ}BM and goto-analyzer 06483f3 Merge pull request diffblue#1881 from tautschnig/fix-runtime-report 3c17453 Merge pull request diffblue#1882 from tautschnig/address_bits ce600d9 Update copyright in .cpp/.h files 004626c Adding invariant to check instruction is normal wide 60af165 Adding handmade class file exhibiting the same problem 5bdaa64 Adding test demonstrating the too many variables problem e976d6f Correctly handle wide iload commands f59092c address_bits need not return an arbitrary-sized integer 3bcb3a5 Fix decision procedure runtime computation 4d33a91 Add missing brackets to multiline if statements. 357bbe4 Fix formatting in assert replacements. f8c2b09 Replace asserts with new equivalents. ecbbc73 Remove unused `forall_symbols` macro. f1670b2 Refactor `forall_symbols` usage into c++11 loop. a8319a3 Remove unused macro `forall_symbol_module_map` 96bf623 Merge pull request diffblue#1856 from thk123/refactor/fieldref_expr 3819295 Merge pull request diffblue#1797 from thk123/bugfix/TG-1358/long-jumps 7e5922a remove functions without a body bc2c0cd Inliner fixes 0003d8a Merge pull request diffblue#1864 from owen-jones-diffblue/owen-jones-diffblue/consistent-casts-in-remove-virtual-function d2e10af Remove the "fieldref" id 2ba794d Introduce fieldref_exprt to represent a field reference c9f3ea4 Test casts in remove_virtual_function() 9df769a Byte offset to array index translation must use array type f4fb099 Fix process_array_expr to take into account pointer offset 379705f Process array_equal the same way as array_{replace,copy} c62b957 Merge pull request diffblue#1551 from tautschnig/perf-test-improvements 1dfb5cd Merge pull request diffblue#1871 from mgudemann/bugfix/superclass_references_for_implicit_generic 71b32f4 Merge pull request diffblue#1777 from romainbrenguier/refactor/java-bytecode-instrument-TG-2331 25eb1a3 Add unit test for implicitly generic super class 590fc2d Make USE_DSTRING conditional and disable it in Ubuntu/Clang/DEBUG Travis job 52290b0 Include string when not using dstringt as irep_idt representation 25ffad4 Do not use dstringt-specific APIs with irep_idt 534f4d2 Include list in expr.h d87d6e4 Include unordered_map where using a std::unordered_map a72f52a [TG-2585] Support implicitly generic superclasses 83d9272 Merge pull request diffblue#1870 from diffblue/chrono-precision 2dc9fcd do not round reported durations to seconds 28c3c9f Merge pull request diffblue#853 from owen-jones-diffblue/feature/pointer-function-parameters ab1b267 Merge pull request diffblue#1832 from diffblue/smt2-backend 11f3699 Merge pull request diffblue#1853 from danpoe/is-threaded-fixes 3e7e840 Merge pull request diffblue#1829 from romainbrenguier/refactor/substitute_array_access#TG-2138 830d519 Merge pull request diffblue#1830 from romainbrenguier/feature/cover-basic-block-java#TG-1404 3a112af Merge pull request diffblue#1846 from hannes-steffenhagen-diffblue/develop-fix_appveyor 9d1e625 Merge pull request diffblue#1641 from karkhaz/kk-big-6-6 7e176f7 Make argument of instrument_code be of type codet b0df38d Make return type of expr_instrumentation an optional 9c838a1 Documentation improvements in bytecode instrument ea3ba42 Remove unused includes f6488d7 Using constant string vector instead of irep_idt d67fa60 [path explore 7/7] Path exploration documentation 53df567 [path explore 6/7] cpplint & clang-fmt agree on : e8eec2c [path explore 5/7] Support path-based exploratio2 c88a3ab [path explore 4/7] Factor out common BMC code d7a70e1 [path explore 3/7] Logical ops for resultt c53d630 [path explore 2/7] Ignore jbmc binary 6d657a0 Merge pull request diffblue#1779 from diffblue/smt2-integers 63beb71 Update coverage goals in goto-diff test 654418a Unit tests for sparse_arrayt d65bf9f Class for sparse arrays representations 773721b Refactoring of substitute array access dc5ffc9 Documentation improvements in string solver 5f54049 Add unit tests for java block instrumentation 105c7e3 Adapt coverage test for new instrumentation c1045aa Use [] instead of `at` on vector 6811238 cover_block implementation using bytecode location acf9fe4 Refer to interface rather than cover_basic_blockst 3cd2f0b Put interface to cover_blocks in virtual class 8e7f129 Correct types from unsigned to std::size_t 0fc9c5e Merge pull request diffblue#1866 from romainbrenguier/feature/code-location-in-preprocessing f270e92 Merge pull request diffblue#1835 from diffblue/remove-goto-templates d82c586 missing header for std::time_t fdc5b1e Add source location to code added by preprocessing 0208218 Merge pull request diffblue#1861 from peterschrammel/goto-diff-properties 8192246 Make remove_virtual_function() consistent 9c12abb make linter happy ba8bbe2 expand goto_programt and goto_functionst templates b36a90a Merge pull request diffblue#1851 from tautschnig/remove-expr-listt 897e29e Fix CMakeLists to correctly pass test exclusion flags 07e0d58 Merge pull request diffblue#1841 from NathanJPhillips/cleanup/remove-unused-params 4d3ab7a Merge pull request diffblue#1838 from mgudemann/bugfix/catch_unsupported_generics_exception a8bdb09 Merge pull request diffblue#1817 from allredj/string-primitives-for-exceptions 1ebec11 get values for nondet symbols a827c77 fix: add missing integer casts and operations bf9b2c1 Merge pull request diffblue#1862 from diffblue/cbmc-test-results-quantifiers 2b92cd3 Update regression tests to use string primitives dd5a674 Add jbmc string primitives to CProverString 8f6431c Introduce more string primitives in JBMC a39fff8 remove iteration count from test result daab304 remove spurious spaces 482ec4a edit a space df9aab5 Test for goto-diff show properties a4d3dc3 Show properties in goto-diff d3eb1f3 Use CPROVER exit codes a0e5063 Enable goto check and cover options in goto-diff a0c45f4 Factor out show properties command line def and docs 937b5f9 Expose conversion of properties of a goto-program into a JSON array f4a8b0c Replace cout in show_properties c480d28 Merge pull request diffblue#1842 from NathanJPhillips/feature/depth_iterator_get_mutable 416bbe0 Allow non-const depth_iteratort to be created from a const root ac37f0b Removed unused parameter/private field 7070296 Add unit test to Makefile f42eeb2 Add unit test for generic superclass with unsupported signature e760d6b Catch unsupported generics exception in superclass ref extraction b0eb45e Merge pull request diffblue#1840 from NathanJPhillips/bugfix/test-name 6f622d1 Fixes for is_threadedt, --is-threaded 13b77d8 Include list where using a std::list and drop forall_expr_list macro 2ccc41b Remove destination directory before trying to move to it in AppVeyor a094990 Fixed test name a0bfd42 smt2irep now uses smt2_tokenizert 3587184 added an SMT-LIB2 tokenizer dea2592 treat real and integer as 'numeric' in C front-end 57ecf15 + is multi-ary in SMT-LIB2 12ae728 fixes for integers in SMT2 698ccdd use a ranged for bc0ebd3 Bounds checks in fgets, read dda54c7 Adding test includes a jump to address 2^16 3f202fa Add support for reading nop operations 7a205f0 Correct handling of two byte offsets cb2c7a8 Adding the irep_ids file to frequently modified low risk files 03095d4 Use svcomp18 as base f659577 perf-test: build configuration using glucose 98b9ae6 SV-COMP now requires zip files 1c0cf32 Support custom CodeBuild templates 6eeb672 Permit selecting a regular-expression-defined set of tasks d3b29d2 Update cprover-sv-comp, benchexec to latest version 3269da7 Utility to generate HTML reports from perf-test experiments cf4eeb2 Move code into code block instead of copying it 7f4a79e Tidy up C symbol factory code REVERT: f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 git-subtree-dir: cbmc git-subtree-split: 207b801

majakusber requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners February 22, 2018 18:02

mgudemann suggested changes Feb 23, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch from 150c878 to 1fb7ac0 Compare February 23, 2018 14:38

thk123 reviewed Feb 23, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch from 1fb7ac0 to 9a78cb5 Compare February 23, 2018 17:08

thk123 reviewed Feb 26, 2018

View reviewed changes

thk123 reviewed Feb 28, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch 2 times, most recently from 82e1c91 to fb5f99f Compare March 2, 2018 10:28

thk123 reviewed Mar 2, 2018

View reviewed changes

mgudemann approved these changes Mar 2, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch 10 times, most recently from 1ab0ce9 to 2e373db Compare March 5, 2018 14:32

thk123 approved these changes Mar 6, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch from 2e373db to aa06299 Compare March 6, 2018 10:23

thk123 added the do not merge label Mar 6, 2018

majakusber force-pushed the specialized_generics_tg1419 branch from aa06299 to a50973c Compare March 6, 2018 16:53

majakusber requested review from kroening and tautschnig as code owners March 6, 2018 16:53

thk123 reviewed Mar 6, 2018

View reviewed changes

majakusber force-pushed the specialized_generics_tg1419 branch 4 times, most recently from fdf60cd to 7d67e28 Compare March 7, 2018 17:13

thk123 reviewed Mar 7, 2018

View reviewed changes

svorenova added 6 commits March 8, 2018 09:47

Introduce a map of parameter-type pairs

3111255

The map of generic parameters and a stack of their concrete types in the various depths of the current scope.

Use the map of parameter-type pairs to specialize generics

624cc91

Remove the old way of specializing generics

5c00440

We now specialize generics on-the-fly using a context-sensitive map of parameter-type pairs

Fix a bug in function for extracting generic interface reference

2964910

Updating and extending utility functions

a1e9d00

Adding and updating unit tests

c53cb29

majakusber force-pushed the specialized_generics_tg1419 branch from 7d67e28 to c53cb29 Compare March 8, 2018 09:48

thk123 removed the do not merge label Mar 8, 2018

thk123 merged commit e7a6769 into diffblue:develop Mar 8, 2018

majakusber deleted the specialized_generics_tg1419 branch March 8, 2018 16:54

+                }
+              }
+              ///

		@@ -0,0 +1,99 @@
		// THIS FILE HAS A COPY IN test-gen/unit/test-java-gen

[TG-1419] Specialization of generics #1877

[TG-1419] Specialization of generics #1877

Conversation

majakusber commented Feb 22, 2018

mgudemann 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

majakusber commented Feb 23, 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

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 Feb 26, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 Feb 28, 2018 • 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

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

thk123 Feb 28, 2018 • edited Loading

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

majakusber Feb 26, 2018 •

edited

Loading

thk123 Feb 28, 2018 •

edited

Loading

thk123 Feb 28, 2018 •

edited

Loading