[TG-375] Fotis/generics support #1406

NlightNFotis · 2017-09-19T16:15:07Z

Added support for concretising a generic after enough information has been found in class fields, and consequently adding it to the symbol table.

chrisr-diffblue · 2017-09-26T14:43:58Z

@NlightNFotis I've checked out the code from this PR and I'm seeing Matthias unit tests failing with a SIGABRT triggered by the unit test parse_generic_class.cpp:92 - does the unit test need updating to match your changes?

NlightNFotis · 2017-09-26T15:07:44Z

@chrisr-diffblue I'm not entirely sure to be honest. I remember @thk123 saying that he was "ironing" Matthias' tests IIRC, but we have to ask him for more information. I don't think my changes have anything to do with Matthias' unit tests breaking, as they should depend on the interface he made, and I think I've made no changes to it - especially for a unit test called parse_generic_class

NlightNFotis · 2017-09-26T15:09:24Z

@chrisr-diffblue Oooohh, I just remembered: The issue we were debugging with @thk123 yesterday had something to do with SIGABRT that was getting triggered by java_type_from_string. If I recall correctly, it was fixed by Thomas yesterday. You should ask him for more information.

thk123

You should add some more tests:

two variables of the same type (e.g. two different bound_element<Integer> variables)
two references of same generic type but with different instantiated type
A test with two generic parameters (e.g. KeyValuePair<K, V> - I suspect this won't work as it doesn't appear to work with Matthias's code, but the tests could be marked as KNOWNBUG so we remember to turn them on when the other part works.
A test with a non-instantiated generic reference:

class G<T>
{
  element<T> ref;
}

The test shouldn't create a new symbol Element<T> and it shouldn't crash.

These may be easier to test using unit tests - see Matthias's tests for how you can load a .class file in a unit test.

thk123 · 2017-09-27T09:08:18Z

src/java_bytecode/generate_java_generic_type.cpp

+    message_handler(message_handler)
+{}
+
+symbolt generate_java_generic_typet::operator()(


Comment required here

thk123 · 2017-09-27T09:12:17Z

src/java_bytecode/generate_java_generic_type.cpp

+    pointer_subtype.id()==ID_struct, "Only pointers to classes in java");
+
+  const java_class_typet &java_class=to_java_class_type(pointer_subtype);
+  java_class_typet replacement_type=java_class;


I seem to have used two different ways of copying the class - first we copy the existing one and modify the components, then we generate a new stub and use the components. I think you should do only one. I think the generate_class_stub is probably better, so you should just build a componentst here rather than a whole type.

thk123 · 2017-09-27T09:12:56Z

src/java_bytecode/generate_java_generic_type.cpp

+#include <sstream>
+
+generate_java_generic_typet::generate_java_generic_typet(
+  symbol_tablet &symbol_table,


As suggested - since the symbol table is mutable, please add as a parameter to the operator() allowing it to become const.

thk123 · 2017-09-27T09:13:09Z

src/java_bytecode/generate_java_generic_type.cpp

+  return symbol_table.lookup("java::"+id2string(new_tag));
+}
+
+irep_idt generate_java_generic_typet::build_generic_tag(


thk123 · 2017-09-27T09:13:46Z

src/java_bytecode/java_bytecode_language.cpp

@@ -198,6 +199,8 @@ bool java_bytecode_languaget::parse(
  return false;
 }

+#include <map>


Includes go at the top of a file

thk123 · 2017-09-27T09:23:28Z

src/java_bytecode/java_utils.cpp

+  {
+    components.insert(components.begin(), component);
+  }
+}


Missing new line

thk123 · 2017-09-27T09:25:17Z

src/java_bytecode/java_utils.cpp

+void java_add_components_to_class(
+  symbolt &class_symbol,
+  const struct_union_typet::componentst &components_to_add)
+{


Add PRECONDITIONs on what is required of the class symbol (e.g. it is a type symbol, the type is a struct)

thk123 · 2017-09-27T09:25:52Z

src/java_bytecode/java_utils.cpp

+
+  for(const struct_union_typet::componentt &component : components_to_add)
+  {
+    components.insert(components.begin(), component);


Why not just push_back? Seems surprising to insert them back to front?

This was actually me copying the implementation of java_root_class. I didn't understand why insert was used instead of push_back, but I assumed there must be a reason that the original author did that, so I thought I would roll with that. I can change it very easily, and I thought about it, but does it actually impact anything?

I can't speak for java_root_class but following the principle of least surprise I think it makes sense to insert the components in order. I agree it shouldn't make any difference

thk123 · 2017-09-27T09:26:07Z

unit/java_bytecode/generate_java_generic_type.cpp

+    REQUIRE(new_symbol.base_name=="UserClass<java.lang.Integer>");
+    REQUIRE(new_symbol.type.id()==ID_pointer);
+  }
+}


Nit: new line

thk123 · 2017-09-27T09:27:29Z

unit/java_bytecode/generate_java_generic_type.cpp

+  "generate_java_generic_type",
+  "[CORE][java_bytecode][generate_java_generic_type")
+{
+  GIVEN("A generic java type and a concrete substitution")


Add more unit tests for classes with multiple fields, multiple generic parameters, nested generic parameters.

thk123 · 2017-09-28T09:32:34Z

src/java_bytecode/generate_java_generic_type.cpp

-  replacement_type.components().clear();
-
-  const irep_idt new_tag=build_generic_tag(existing_generic_type, java_class);
+  java_class_typet &replacement_type=to_java_class_type(const_cast<typet &>(pointer_subtype));


What is going on here? It appears you are casting away const-ness(?!) which means you'd actually end up modifying the components on the original type? I don't think you need to create a java_class_typet here since you create one in generate_class_stub, it should be sufficent to make a new componentst that is a copy of the pointer_subtype.components(). Suggest you extend your tests to check that the original struct is still present with the original type for the components.

thk123 · 2017-09-28T09:52:01Z

src/java_bytecode/java_bytecode_language.cpp

-
-  generate_java_generic_typet new_symbol_generator(symbol_table, get_message_handler());
+  bool res=java_bytecode_typecheck(symbol_table, get_message_handler(), string_refinement_enabled);
+//  if (!res)


I think this just need to be toggled (that is java_bytecode_typecheck returns false when everything went well)

NlightNFotis · 2017-09-28T10:21:28Z

src/java_bytecode/generate_java_generic_type.cpp

+    {
+      if(is_java_generic_parameter(component.type()))
+      {
+        INVARIANT(


@thk123 This becomes way more readable if I remove the invariant from here. I wanted to ask if that makes sense (it's guarding against a case that's always guaranteed to be true in this case).

Invariants are always meant to be guarding against cases that are guaranteed to be true?

I'm also not sure that is true in this case, if it is, why is generic_type_variables a vector data structure vs. just a single element? I think I put this in to remind me to deal with when we have generic classes with multiple generic parameters.

there can be more type variables than just one here, I think
Maybe add some documentation what the function does to clarify

mgudemann · 2017-10-02T11:16:40Z

src/java_bytecode/generate_java_generic_type.cpp

+#include <java_bytecode/java_types.h>
+#include <java_bytecode/java_utils.h>
+
+#include <iostream>


maybe put this into a #DEBUG

There are no debug statements left in, so I eliminated the include, instead of just enclosing it in an ifdef.

mgudemann · 2017-10-02T11:27:38Z

src/java_bytecode/generate_java_generic_type.cpp

+  const java_generic_typet &existing_generic_type,
+  symbol_tablet &symbol_table) const
+{
+  PRECONDITION(existing_generic_type.id()==ID_pointer);


the java_generic_typet inherits from reference_typet so this is not necessary

mgudemann · 2017-10-02T11:42:49Z

src/java_bytecode/generate_java_generic_type.cpp

+    {
+      if(is_java_generic_parameter(component.type()))
+      {
+        INVARIANT(


there can be more type variables than just one here, I think
Maybe add some documentation what the function does to clarify

mgudemann · 2017-10-02T11:55:40Z

src/java_bytecode/generate_java_generic_type.cpp

+
+  INVARIANT(
+    pre_modification_size==after_modification_size,
+    "All components in the original class should be in the new class");


wouldn't it make more sense to check that all has been replaced with a concrete type ? replace_type_for_generic_field is called exactly once for each element

mgudemann · 2017-10-02T12:03:00Z

src/java_bytecode/generate_java_generic_type.cpp

+  return symbol_table.lookup("java::"+id2string(new_tag));
+}
+
+/// Build a unique tag for the generic to be instantiated.


please give an example of how the tag will look like. Also it seems that you concat using , , I am not too fond of using spaces here

This comment doesn't seem to have been addressed?

mgudemann · 2017-10-02T12:08:21Z

src/java_bytecode/java_bytecode_language.cpp

+  if (res)
+  {
+    // there is no point in continuing to concretise the generic types if typechecking failed.
+    return res;


maybe return literal true here

mgudemann · 2017-10-02T12:15:32Z

src/java_bytecode/java_utils.cpp

@@ -182,3 +184,21 @@ dereference_exprt checked_dereference(const exprt &expr, const typet &type)
  result.set(ID_java_member_access, true);
  return result;
 }
+
+/// Add the components in compomnents_to_add to the class denoted by class symbol.


compomnents -> components

mgudemann · 2017-10-02T12:16:09Z

src/java_bytecode/java_utils.h

@@ -66,4 +67,11 @@ irep_idt resolve_friendly_method_name(
 /// \param type: expected result type (typically expr.type().subtype())
 dereference_exprt checked_dereference(const exprt &expr, const typet &type);

+/// Add the components in compomnents_to_add to the class denoted by class symbol.


mgudemann · 2017-10-02T12:19:11Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+    generate_java_generic_typet type_generator(message_handler);
+
+    auto boxed_type_reference = symbol_typet("java.lang.Integer");


also name should have java:: prefix for consistency

mgudemann · 2017-10-02T12:21:23Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+    auto boxed_type_reference = symbol_typet("java.lang.Integer");
+    auto boxed_parameter = java_generic_inst_parametert(boxed_type_reference);
+    auto list_type_reference = java_type_from_string("Ljava/util/List;", "List");


the second parameter makes not much sense here, its idea is to serve as a prefix when a type variable is generated, to make those unique, as for example T could be used as type paramter name in different generic classes

thk123

I think you are still missing the two references of same generic type but with different instantiated type test.

Also I think one of the tests is testing the exact opposite condition (a generic reference that is not instantiated).

thk123 · 2017-10-02T14:50:04Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+  GIVEN("A generic java type with two generic fields and a concrete "
+          "substitution")
+  {
+    java_lang->parse(java_code_stream, "generic_two_fields.class");


Nit: you can use the load_java_class that now exists in develop (save doing this until rebased after #1434 is merged in)

This please :)

thk123 · 2017-10-02T14:55:01Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+      class_typet class_type=to_class_type(symbol_type);
+      REQUIRE(class_type.is_class());
+
+      REQUIRE(class_type.subtypes().size()==2);


What does this mean? How come the subtypes must be of size two (consider a comment)

thk123 · 2017-10-02T14:55:18Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+    java_lang->final(new_symbol_table);
+
+    new_symbol_table.show(


Debug code should be removed from PR

thk123 · 2017-10-02T14:55:38Z

unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java

+  }
+
+  class element<T> {
+    T haha;


Nit: professional names please :)

thk123 · 2017-10-03T08:58:43Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+  std::unique_ptr<languaget> java_lang(new_java_bytecode_language());
+
+  // Configure the path loading
+  cmdlinet command_line;


I don't think this is required any more as you are not loading the class file

thk123 · 2017-10-03T09:09:42Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+      class_typet class_type=to_class_type(symbol_type);
+      REQUIRE(class_type.is_class());
+
+      auto generic_components_counter=0;


I think this would be better to explicitly get the components:

REQUIRE(`class_type.has_component("first")); const auto &first_component=class_type.get_component("first"); REQUIRE(is_java_generic_parameter(first_component.type())); REQUIRE(`class_type.has_component("second")); const auto &second_component=class_type.get_component("second"); REQUIRE(is_java_generic_parameter(second_component.type()));

Or even pull it out into a function that verifies that the relevant component exists without duplication.

This for loop can just be deleted right?

thk123 · 2017-10-03T09:12:19Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+        "java::generic_two_parameters$KeyValuePair");
+      const typet &symbol_type=class_symbol.type;
+
+      REQUIRE(symbol_type.id()==ID_struct);


Could I also request it isn't an incomplete class:

REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));

thk123 · 2017-10-03T09:13:26Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+    java_lang->final(new_symbol_table);
+
+    REQUIRE(new_symbol_table.has_symbol
+      ("java::generic_unknown_field$element<T>"));


I think this is the opposite of what we should have? Specifically we shouldn't create a new type representing element<T> (we already have the symbol element to represent this).

mgudemann

looks better now, linter still complains though

thk123

Nearly there - mostly just removing what appears to be unused code 👍 Only major thing is since this code now supports types with multiple generic params, you should validate that your test covers this.

Make sure when you've done the rebase you remember to:

validate the linter output
use the utility function for loading the class type
do a test-gen submodule bump before merging.

thk123 · 2017-10-04T09:56:50Z

src/java_bytecode/generate_java_generic_type.cpp

+            to_java_generic_parameter(component.type()).type_variable()
+              .get_identifier());
+
+        if(results)


I think this should be an invariant

thk123 · 2017-10-04T09:57:11Z

src/java_bytecode/generate_java_generic_type.cpp

+    {
+      if(is_java_generic_parameter(component.type()))
+      {
+        optionalt<size_t> results=


Nit: consider pulling out some of these parameter into local variables

thk123 · 2017-10-04T10:01:23Z

src/java_bytecode/generate_java_generic_type.cpp

+    "All components in the original class should be in the new class");
+
+  generate_class_stub(new_tag, symbol_table, message_handler, replacement_components);
+  INVARIANT(symbol_table.has_symbol("java::"+id2string(new_tag)), "New class not created");


Nit: only do the "java::"+id2string(new_tag) once

thk123 · 2017-10-04T14:13:40Z

src/java_bytecode/generate_java_generic_type.cpp

+  return symbol_table.lookup("java::"+id2string(new_tag));
+}
+
+/// Build a unique tag for the generic to be instantiated.


This comment doesn't seem to have been addressed?

thk123 · 2017-10-04T14:15:12Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+  // Configure the language
+  null_message_handlert message_handler;
+  java_lang->set_message_handler(message_handler);


I don't think java_lang and java_code_stream are used anywhere in this test.

thk123 · 2017-10-04T14:15:59Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+      class_typet class_type=to_class_type(symbol_type);
+      REQUIRE(class_type.is_class());
+
+      auto generic_components_counter=0;


This for loop can just be deleted right?

thk123 · 2017-10-04T14:16:42Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+    java_lang->final(new_symbol_table);
+
+//    REQUIRE(new_symbol_table.has_symbol(


Nit: Comment out using #if 0 though actually with your latest changes - won't this now work?

thk123

A bunch of tidy up changes then this looks good to go. Please check the linter as I spotted a bunch of errors that I didn't bother to mark.

thk123 · 2017-10-11T17:25:45Z

src/java_bytecode/generate_java_generic_type.cpp

+
+        if(results)
+        {
+          component.type()=existing_generic_type.generic_type_variables()


Nit: break after the =

thk123 · 2017-10-11T17:26:23Z

src/java_bytecode/generate_java_generic_type.cpp

+  const auto expected_symbol="java::"+id2string(new_tag);
+
+  generate_class_stub(new_tag, symbol_table, message_handler, replacement_components);
+  auto sym = symbol_table.lookup(expected_symbol);


Nit: symbol rather than sym also linter (spaces around =)

thk123 · 2017-10-11T17:27:01Z

src/java_bytecode/java_bytecode_language.cpp

+      }
+    }
+  }
+}


Missing empty last line

thk123 · 2017-10-11T17:27:28Z

src/java_bytecode/java_bytecode_language.cpp

+/// \param message_handler
+/// \param symbol_table The symbol table so far.
+void
+java_bytecode_languaget::handle_generics(


I think my preference would be to put this method in generate_java_generic_type.h and probably call it something more descriptive (since handle_generics is both vague (handle how?) and wrong (doesn't solve all generic problems 😛 ))

My thought process for this was for it to be locus of control for all handling of generics in the java_bytecode_languaget class, containing the whole sequence of steps (not just mine) that are required for handling generics, and then just hook this self contained unit into whatever step of the pipeline of the conversion we want, be it after type-checking, or after conversion, or whatever.
Therefore, I do not think it's appropriate for it to go into generate_java_generic_type.h, unless its semantics change to the point where it only does the adding to the symbol table and nothing else.

To put it in fewer words, it's just a re-organisation of the original logic that I had, for it to be more modular.

thk123 · 2017-10-11T17:29:35Z

src/java_bytecode/java_bytecode_language.cpp

+  // have a a generic type in.
+  for(const auto &symbol : symbol_table.symbols)
+  {
+    if(symbol.second.type.id()==ID_struct)


I suspect we want to include not just component members but also parameters to functions - but let us leave that for now

thk123 · 2017-10-11T17:32:51Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+      REQUIRE(class_type.has_component("key"));
+      const auto &first_component=class_type.get_component("key");
+      REQUIRE(is_java_generic_inst_parameter(first_component.type()));


Tighten bound to check is a pointer to a java.lang.String for key

thk123 · 2017-10-11T17:34:57Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+
+    java_lang->final(new_symbol_table);
+
+    REQUIRE_FALSE(new_symbol_table.has_symbol


Nit: Consider adding a comment explaining why this symbol should not be found

thk123 · 2017-10-11T17:35:23Z

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

+    REQUIRE(new_symbol_table.has_symbol
+      ("java::generic_two_instances$element<java::java.lang.Boolean>"));
+    REQUIRE(new_symbol_table.has_symbol
+      ("java::generic_two_instances$element<java::java.lang.Integer>"));


Please tighten as with the above tests to check that the components of the created class are of the correct type

thk123 · 2017-10-11T17:35:50Z

unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java

+  bound_element<Integer> belem;
+
+  Integer f(int n) {
+    bound_element<Integer> e=new bound_element<Integer>();


To avoid making this test unnecesarily confusing, please remove irrelevant code (e.g. maybe this entire function?)

thk123 · 2017-10-11T17:36:06Z

unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java

+  element<Integer> int_element;
+
+  public void func() {
+    bool_element = new element<Boolean>();


Ditto: I don't think this function is required

thk123

Couple of formatting things that have flitted through the formatter if you wouldn't mind fixing them

thk123 · 2017-10-12T15:00:35Z

src/java_bytecode/generate_java_generic_type.h

+  message_handlert &message_handler;
+};
+
+void instantiate_generics(message_handlert &message_handler,


Nit: dunno why linter didn't pick up on this but should be:

void instantiate_generics( message_handlert &message_handler, symbol_tablet &symbol_table);

table.

thk123 · 2017-10-12T16:15:12Z

Forgot to request a submodule bump, have created: diffblue/test-gen#1099

@smowton

64d81f1 Merge remote-tracking branch 'upstream/develop' into pull-support-20171019 9e05177 Merge pull request diffblue#1474 from diffblue/jbmc e847137 Merge pull request diffblue#1493 from reuk/reuk/output-instruction-const-ref e74e1d8 Merge pull request diffblue#1489 from svorenova/tg-865 09431fd Adding unit tests for the signature/descripture mismatch 9a59fb9 Renamed DiffBlue -> Diffblue 185206c cbmc cleanup d542f7e cbmc: clean out java 320eeaf use jbmc in regression tests 4286b86 added jbmc executable b61cb56 Resolving signature/descriptor mismatch for methods 62675bb Merge pull request diffblue#1494 from thk123/tests/adding-generic-unit-tests 69d67ab Modified unit test to compile 9e68466 Replace loop_id parameter with const instructiont& dbff05b Replace iterator with const value_type& in output_instruction signature 5191170 Merge pull request diffblue#1485 from diffblue/std_expr_typing 210a2f4 Merge pull request diffblue#1491 from andreast271/cbmc_parse_options_fix fbc54ad guard against spurious pointers in taint analysis 5d6ebfd Revert "test isn't ready yet" de668e6 upgrade uses of deprecated member_exprt constructor 9da3f4f elaborate typing of std_expr expression classes 36ac8c9 Merge pull request diffblue#1482 from reuk/reuk/more-cmake-errors 47c2a51 Merge pull request diffblue#1447 from NathanJPhillips/bugfix/calculate_max_string_length-unit-test b2b4ca5 Align options string with help function and options parser dfb11c2 Merge pull request diffblue#1480 from diffblue/java-types-cleanup 11c8aba Fixed calculate_max_string_length unit test to work in CLion 8f4f2ec Merge pull request diffblue#1473 from reuk/reuk/simplify-expr-fixup 1ad89a0 Merge pull request diffblue#1475 from martin-cs/goto-analyzer-6-part1 3c5df61 Merge pull request diffblue#1486 from diffblue/revert-1413-smowton/feature/prepare_vsa_for_subclasses 24f9867 Simplify a broader range of java primitive types a18d7ec Revert "Value-set analysis: templatise and virtualise to facilitate customisation" 88acdfd Merge pull request diffblue#1355 from diffblue/cleanout-config-dependency 7df77e8 Add the overrides that clang wants. e96e09b Regression test for constant propagator merge bug ba55a2f constant propagator fix 350aa96 Addressing constant domain review comments by Daniel Poetzl. 5e9b2f4 Fail CMake build if make-generated files are found 32dcad8 test approx-const-fp-array-variable-invalid-cast-const-fp now more generous 12d45c6 Remove config dependency from CVC and DPLIB solvers 00d25a2 Pointers now come with a width f4bc0ec cleanup of java_types.h 08b2332 disable two-way propagation for now 76abe8a Fix constant propagator. c0ce9de Merge pull request diffblue#1413 from smowton/smowton/feature/prepare_vsa_for_subclasses 0bf2ce8 Merge pull request diffblue#1478 from smowton/smowton/fix/doxygen_fixes 0e0b501 Merge pull request diffblue#1463 from diffblue/mem-safety-check 04aff7c Remove residual doc template fc02354 Fix docstyle in dump_c.cpp a99b254 Indirect value_set_domaint -> value_sett operations via non-member functions f94807d Merge pull request diffblue#1428 from romainbrenguier/refactor/find_index 433fdbf Merge pull request diffblue#1472 from reuk/reuk/label-tests df6a0b3 Merge pull request diffblue#1406 from NlightNFotis/fotis/generics_support 123162b Merge pull request diffblue#1476 from diffblue/remove_ID_reference e669c12 Add unit tests for value-set-analysis customisation 9465771 Value-set analysis: ignore DEAD statements a2c1685 Templatize and virtualize value-set analysis 8ea9dcb Use std::find_if instead of expr visitor 5e1eede Merge pull request diffblue#1454 from martin-cs/feature/string-solver-performance c73b758 Merge pull request diffblue#1452 from diffblue/call-seq-fix d735cc5 Added support for concretising a generic and adding it into the symbol table. f131b34 Remove ID_reference as front-ends use ID_pointer+ID_C_reference d67bc87 Merge pull request diffblue#1471 from reuk/reuk/more-expr-cast-updates 5777062 check that memory for memcpy, memset and memmove is accessible 808a6ad Created basic class for creating new java instantiations of classes 57c2c1f Label tests with CBMC bf4a103 Make a few changes suggested by @smowton b63eb99 Merge pull request diffblue#1418 from diffblue/address_of_unions e82701a Merge pull request diffblue#1456 from diffblue/preserve-hidden 3ff8448 Merge pull request diffblue#1468 from smowton/smowton/fix/unit_test_makefile_dependencies 1a81b3f Merge pull request diffblue#1341 from reuk/reuk/big-int-fixes 1d9eace Merge pull request diffblue#1465 from mgudemann/feature/string-solver-performance 987d384 Switch (!a | b) for (a => b) to clarrify the intent of the code. 40ff71b Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs. d8b25f3 Merge pull request diffblue#1470 from reuk/reuk/fix-null-dereferences 5fa7b9a Merge pull request diffblue#1466 from reuk/reuk/return-ptr-from-expr-cast 0832454 Fix a couple of places where a null pointer may be dereferenced 47e426f Merge pull request diffblue#1442 from andreast271/compilation-NDEBUG-enable 869043a Merge pull request diffblue#1464 from smowton/smowton/fix/messaget_copy_and_assign_operators 9f53e90 Return pointer from expr_try_dynamic_cast 838c8a1 Fix testing-utils Makefile dependency 691e9fb Merge pull request diffblue#1449 from diffblue/havoc_object 78cd286 Fix messaget's copy-constructor and operator= 1614c2c Merge pull request diffblue#1462 from reuk/reuk/symbol-table-pointer a9ba0f9 Modify/add symbol table lookup and get_writeable d19e737 Merge pull request diffblue#1461 from thk123/bugfix/correcting-includes-in-new-unit-tests 3b69fe1 Missing source file from Makefile d70a08a Util files were moved into a util library 0681219 Merge branch 'develop' of github.com:diffblue/cbmc into develop 8891466 test isn't ready yet (cmake variant) b8057d3 Merge pull request diffblue#1448 from diffblue/goto-analalyzer-taint-test beac327 added __CPROVER_havoc(...) 8118efa test isn't ready yet 19858f9 Fix zeroing of arrays in value set analysis 12fd5fe Fix identifying arrays in value set analysis e618169 Merge pull request diffblue#1434 from svorenova/generics_support 68e4d6b Merge pull request diffblue#1457 from reuk/reuk/testing-utils 7c545c8 Switch (!a | b) for (a => b) to clarrify the intent of the code. 438ba8d Avoid generating redundant constraints by iterating over n^2/2 rather than n^2 pairs. aacd436 Add new testing-utils library b7aaad0 Removing signature parsing for local variables 8d54be1 Adding exception and tests for missing closing delimiter 608c6b6 Disabling part of the unit test for generic classes e140bb7 Updating the calls of lookup method to reflect the new return type cfb5212 Resolving name shadowing 97e1b9a Adding a warning and a commentary for unsupported generics, cleaning 4f305de Handling wild card generics with exception 8f527f8 Cleaning java files 3a1962f Turning back on regression tests a9dc64d Disabling part of the unit test for generic classes 04e55be Reverting method descriptor loading 2f7925d Adding unit test for recursive generic class 764c651 Enable compilation with NDEBUG defined e8c75ac Adding unit test for generic array de5c040 Adding tests for generic functions 85c1574 Applied use of utility function for loading a class file 8c7f4e4 Adding unit test for java class that inherits from a generic class 1dd221d Correct handling of the java generic class signature 33afe48 Adding unit tests for parsing wild card functions a2344f8 Extending the tests for the generic class 35cd160 Deal with generic methods 7320c46 Correcting a typo 2f7f695 Adding some useful debug info 79f743b Adding conversions for wild cards a60ead4 Correctly handle nested generic types b59c659 When dealing with generic arrays we should treat them like ref arrays too 1bd95c0 Classes that aren't generic but inherit from a generic type have a signature b2f57e8 Fixing handling the case of * 31faaa6 Revert "Revert "TG-374 Feature/java support generics"" 89341da Merge pull request diffblue#227 from diffblue/feature/adding_goto_statistics_to_goto-instrument 99eb662 Merge pull request diffblue#1450 from reuk/reuk/join-strings 9cf47a2 Updates requested in the PR. 4c4a267 Adding computation and save of goto program statistics. 7fcfd30 Merge pull request diffblue#1453 from diffblue/integer-addressees 639d1aa Merge pull request diffblue#1451 from diffblue/time-stopping 7e42fd2 preserve hidden flag for functions 0346f87 Add a join function for strings 2b17564 integer dereferences are now re-written to a custom expression 202b509 fix for call-sequences and call-graph f159bd5 more time stopping functionality ba96dde Merge pull request diffblue#1441 from reuk/reuk/expr-cast-for-code-types 086d6da moved taint-related tests for goto-analyzer into separate subdirectory c25e56f Respond to @NathanJPhillips' review feedback 3a4d364 Add checked_cast signatures 47a13c7 Remove unnecessary explicit typelists bc3d79b Use decay instead of remove_const(remove_reference) f9c1c70 Reorder and hide functions in expr_cast 800adbe Allow dynamic expr cast with code types 3ce8f11 Fix comparison in expr_cast.h 48b154a Bugfix: Exclude functions without bodies from GOTO statistics. 22a68fe Merge pull request diffblue#1444 from smowton/upstream/restrict-symbol-table d577d40 Merge pull request diffblue#1445 from smowton/smowton/feature/test-pl-interrupt b01ff65 Test.pl: exit if a test is interrupted 6794191 Improve symbol table documentation d320187 Linter fixes 53e1ca2 Made move constructor strong exception safe 9f4e933 Changed interface to symbol_tablet::insert e35f2fc Misc review requests a9d802b Made lookup return optional d1d502f Restricted interface of current symbol_tablet 478dc8a Merge pull request diffblue#1371 from NathanJPhillips/feature/unhide-error b790095 Merge pull request diffblue#1443 from tautschnig/fix-library-check ab2f3c3 Merge pull request diffblue#1438 from reuk/reuk/simplify-expr-improvement e865729 Updated comment 1def64c Added INVARIANT to symbol_tablet::remove 7798daa Add move insert to symbol_table b14a495 Tidy up symbol_tablet::move 6be5fd5 Merge pull request diffblue#1394 from smowton/smowton/feature/split_frontend_final_stage 14eecf6 library_check: use the build-system configured C compiler 3197045 library_check: rename _mm_*fence functions 6bc86e1 Merge pull request diffblue#222 from diffblue/feature/lexicographical_ordered_dump_of_functions_and_symbols a73ee46 Merge pull request diffblue#224 from diffblue/feature/file_utils_add_parsing_of_file_extension 421f4eb Merge pull request diffblue#226 from diffblue/feature/goto_statistics 1d87928 Add unit test for new behavior 9ea7414 Set up config in unit tests 0e2b13f Remove tautological typecasts 901d745 Switch to C++11 for-loops in language_file.cpp c7c8022 Add tests for mixed GOTO and C input 05f2f3c Split the entry-point-generation phase into two parts 268d196 Display error in catch(...) 6888dd2 Merge pull request diffblue#1436 from smowton/smowton/initialize-goto-model-opaque-stub-generation 6d9f029 Updates requested in the PR. 6f8ebe4 Updates requested in the PR. d4a04ac Added support of Windows platform to parsing file extension. 1884d67 Merge pull request diffblue#221 from diffblue/bugfix/INVARIANT_while(0)_to_while(false) 39a774f Introducing GOTO program statistics. 821ba1c Updates requested in the PR. 9266de0 Add parsing of file extension from file path-name. a9fa893 Merge pull request diffblue#1437 from smowton/smowton/fix-object-factory-globals 632ae4b Updates to recording_symbol_tablet 7545fc5 Merge pull request diffblue#1409 from thk123/bugfix/lang-args-missing 7fb835c Merge pull request diffblue#1433 from thk123/bugfix/doxy-script-documentation 56b0b26 Added lexicographical order to textual dump of functions and symbols. 58ef65b Object factory: initialise global symbols in place c41acce Set opaque stub generation in initialize-goto-model ef76441 Corrected error in the run_diff script 897aaf6 Merge pull request diffblue#1431 from thk123/feature/java-load-class-utility 79324b3 INVARIANT: while(0) -> while(false) 774bfdb Correcting type in the extendor class 46cbec6 Created utility function for loading a class file 8151e91 Merge pull request diffblue#1429 from janmroczkowski/janmroczkowski/unified_difft-remove-unused-identifier 3ceb89b Merge pull request diffblue#1390 from diffblue/fix_pointer_type 733f7b2 Added is_success and is_error helpers 5e7f3f7 Added implicit constructors to main_function_resultt to make code in get_main_symbol even briefer 3317a3a Tidied up code in get_main_symbol 47fe36f Changed main_function_resultt to use an enum instead of a collection of bools 8bb39ca Merge pull request diffblue#1427 from LAJW/feature/string-replace-single-character-strings a084a6a Reverting indentation in order to make the compiler silent. f948c2f Readability improvement fc7c615 Remove unused function identifier c063d01 Merge pull request diffblue#1259 from romainbrenguier/cleaning/factor-assign-java-string c24e6c9 Update regression test that can randomly fail df88b49 Rename operand_to_process into expr_to_process e0441cb Add example where the solver potentially runing out of memory 52a08d8 Setting string-max-length on strings test 02e42da Adding unit test for convert exprt to string exprt 870814e Make code_assign_java_string_to_string_expr append to a code argument e8491a6 Factoring assign_java_string_to_string_expr with process_operands 00af153 Add comment on implementation status of String.replace f2fab1a String.replace for single-character strings fade69f Move expr_cast to a separate file e4b5e12 Merge pull request diffblue#218 from diffblue/cleanup/typo 5fecceb Added recording_symbol_tablet 4d65951 Split storage for symbol_tablet into a concrete derived type 7b254e2 Made move constructor strong exception safe d66c0bc Changed interface to symbol_tablet::insert 6dc1213 Typo in reachable 51e493e Merge pull request diffblue#1422 from reuk/reuk/library-check-dep 27e1f2a Merge pull request diffblue#1423 from janmroczkowski/janmroczkowski/fresh_symbol-reset_temporary_counter 15af645 Merge pull request diffblue#1426 from reuk/reuk/download-project db9a0a7 Updates requested in the PR. d00c03d Introducing "enable_ccache" switch (default on) into our build system. 88c2f9c Use DownloadProject method for integrating sat libraries bc593c5 Add DownloadProject cmake script 0cc696b introduced ID_frontend_pointer cc63551 revert bits of a9806c0; the width of these pointers is done during the conversion phase 8fdb06f preserve location of pointer types de493ae Merge pull request diffblue#1412 from diffblue/java-object-factory-bug 7c3239b Merge pull request diffblue#1417 from diffblue/builtin_memset 368bb27 Merge pull request diffblue#1421 from jasigal/refactor/string-refinement-decision-procedure#TG-672 f079156 Merge pull request diffblue#205 from diffblue/feature/restrict-symbol-table 2462077 Misc review requests 98d0082 Made lookup return optional db69023 Restricted interface of current symbol_tablet ea74c6d Updated comment 909b557 Added INVARIANT to symbol_tablet::remove bd3ee6e Add move insert to symbol_table e67f326 TG-672 Added universal constraint counter-examples, assumed fix-point with no not contains constraints is equi-SAT 72a537a TG-672 Remove some unused concretizing code 95efc6f TG-672 Grouped string axioms together a65407e TG-672 Grouped index sets together 503c49d TG-672 Removed unneeded code (current index set display, extra invariant check) 45af45d TG-672 Uniformity in algorithm for treatement of universal and not contains constraints dd03003 TG-672 Fixed correctness issue in main loop of algorithm and added first UNSAT return dfa3ffd TG-672 Replaced `push_back` with `emplace_back` ac1b620 TG-672 Fixed `expr_cast` to be unambiguous and added `const` and `const` references throughout eb5726e Add reset_temporary_counter to fresh_symbol b5fe7e3 TG-672 Initial refactoring (renaming, code removal) 438d9f0 Merge pull request diffblue#1401 from janmroczkowski/janmroczkowski/java_bytecode_convert_classt-add_array_types-fix 18aacc0 Add full JSON-structured output for value-set analysis 0cdd9c6 Improve structure of JSON static-analysis dump 7df9f15 Add LVSA summary dump-to-JSON 83ee7d4 Only re-run library-check when ansi-c changes 2adc013 symex: fix address_of unions cd8d494 added __builtin_memset fcd470a only attempt to translate nondet sideeffects for Java code b9dfda9 Fix to java_bytecode_convert_classt.add_array_types 61c6489 Verify that language options have been initialized e3ad6c0 Update Big-Int with copy, move, swap git-subtree-dir: cbmc git-subtree-split: 64d81f1

peterschrammel added the do not merge label Sep 19, 2017

thk123 suggested changes Sep 27, 2017

View reviewed changes

thk123 reviewed Sep 28, 2017

View reviewed changes

NlightNFotis commented Sep 28, 2017

View reviewed changes

thk123 changed the title ~~Fotis/generics support~~ [TG-375] Fotis/generics support Oct 2, 2017

thk123 requested a review from mgudemann October 2, 2017 09:16

mgudemann suggested changes Oct 2, 2017

View reviewed changes

thk123 suggested changes Oct 3, 2017

View reviewed changes

mgudemann approved these changes Oct 4, 2017

View reviewed changes

thk123 suggested changes Oct 4, 2017

View reviewed changes

NlightNFotis force-pushed the fotis/generics_support branch 4 times, most recently from 1a3a2dd to 6d2f0bf Compare October 11, 2017 15:47

thk123 suggested changes Oct 11, 2017

View reviewed changes

NlightNFotis force-pushed the fotis/generics_support branch from 0c076d3 to 26daeb9 Compare October 12, 2017 10:59

Created basic class for creating new java instantiations of classes

808a6ad

NlightNFotis force-pushed the fotis/generics_support branch 2 times, most recently from 67ea955 to ad1c819 Compare October 12, 2017 14:07

thk123 approved these changes Oct 12, 2017

View reviewed changes

Added support for concretising a generic and adding it into the symbol

d735cc5

table.

NlightNFotis force-pushed the fotis/generics_support branch from ad1c819 to d735cc5 Compare October 12, 2017 15:04

thk123 merged commit df6a0b3 into diffblue:develop Oct 13, 2017

thk123 removed the do not merge label Oct 13, 2017

NlightNFotis deleted the fotis/generics_support branch February 19, 2021 11:16


		generate_java_generic_typet type_generator(message_handler);

		auto boxed_type_reference = symbol_typet("java.lang.Integer");


		java_lang->final(new_symbol_table);

		// REQUIRE(new_symbol_table.has_symbol(


		java_lang->final(new_symbol_table);

		REQUIRE_FALSE(new_symbol_table.has_symbol

[TG-375] Fotis/generics support #1406

[TG-375] Fotis/generics support #1406

Conversation

NlightNFotis commented Sep 19, 2017 • edited Loading

chrisr-diffblue commented Sep 26, 2017

NlightNFotis commented Sep 26, 2017

NlightNFotis commented Sep 26, 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

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

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

mgudemann left a 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

thk123 left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

thk123 commented Oct 12, 2017

NlightNFotis commented Sep 19, 2017 •

edited

Loading

thk123 left a comment •

edited

Loading