[TG-3067] Support generic type parameters that create recursion loops in instantiation stack #2239

mgudemann · 2018-05-25T21:02:33Z

No description provided.

romainbrenguier · 2018-05-29T08:25:15Z

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -33,7 +33,7 @@ class generic_parameter_specialization_map_keyst
    for(const auto key : erase_keys)
    {
      PRECONDITION(generic_parameter_specialization_map.count(key) != 0);
-      (*generic_parameter_specialization_map.find(key)).second.pop();
+      (*generic_parameter_specialization_map.find(key)).second.pop_back();


generic_parameter_specialization_map.find(parameter_name)->second

romainbrenguier · 2018-05-29T08:26:19Z

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

@@ -33,7 +33,7 @@ class generic_parameter_specialization_map_keyst
    for(const auto key : erase_keys)
    {
      PRECONDITION(generic_parameter_specialization_map.count(key) != 0);
-      (*generic_parameter_specialization_map.find(key)).second.pop();
+      (*generic_parameter_specialization_map.find(key)).second.pop_back();
      if((*generic_parameter_specialization_map.find(key)).second.empty())


there are three successive lookups for the same key in the map, this could be reduced to one.

romainbrenguier · 2018-05-29T08:27:45Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+    // information from further recursion, only cause a segmentation fault.
+    if(visited_nodes.find(parameter_name) != visited_nodes.end())
+    {
+      throw "no infinite recursion";


avoid throwing strings

romainbrenguier · 2018-05-29T08:29:14Z

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -80,12 +82,21 @@ pointer_typet select_pointer_typet::specialize_generics(
    const pointer_typet &type =
      generic_parameter_specialization_map.find(parameter_name)->second.back();

+    // if we have already seen this before, we will not learn any additional
+    // information from further recursion, only cause a segmentation fault.


I find the comment a bit long, could just be avoid infinite recursion

romainbrenguier · 2018-05-29T08:31:50Z

jbmc/src/java_bytecode/select_pointer_type.cpp

    // generic parameters can be adopted from outer classes or superclasses so
    // we may need to search for the concrete type recursively
    return is_java_generic_parameter(type)
             ? specialize_generics(
                 to_java_generic_parameter(type),
-                 generic_parameter_specialization_map)
+                 generic_parameter_specialization_map, visited_nodes)


I think the parameter should be on a new line

romainbrenguier · 2018-05-29T08:42:17Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+        {
+          return type;
+        }
+        else


unnecessary else

romainbrenguier · 2018-05-29T08:42:49Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+    {
+      const size_t index = (replacements.size() - depth) - 1;
+      const auto &type = replacements[index];
+      {


unnecessary new block

romainbrenguier · 2018-05-29T08:43:56Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+  else
+  {
+    UNREACHABLE;
+  }


The condition in the corresponding if should probably be made a precondition instead of having UNREACHABLE here

romainbrenguier · 2018-05-29T08:45:55Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+    {
+      if(is_java_generic_parameter(*retval))
+      {
+        UNREACHABLE;


could use CHECK_RETURN instead

romainbrenguier · 2018-05-29T08:46:36Z

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -179,16 +204,14 @@ optionalt<pointer_typet> select_pointer_typet::get_instantiated_type(
    const auto &replacements =
      generic_parameter_specialization_map.find(parameter_name)->second;

-    // max depth reached and nothing found
+    // max depth reached and nothing found, TODO return bound


put the TODO on a new line

majakusber · 2018-05-29T13:17:23Z

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

+{
+  const symbol_tablet &symbol_table = load_java_class(
+    "MutuallyRecursiveGenerics",
+    "./java_bytecode/goto_programs_generics",


I think your CI is failing due to a typo here, it should be goto_program_generics, not goto_programs_generics

mgudemann · 2018-05-29T14:02:24Z

@romainbrenguier adressed most of your comments
@svorenova all green now

majakusber

I have some design questions/suggestions. I'm not quite sure if this would work in all cases, so adding additional test cases would be great - something where the cycles in the specialization map are bigger (say 3 or 4 parameters), having different specialization for certain parameters in the same scope but different scope depth etc.

majakusber · 2018-05-29T13:43:45Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+      else
+      {
+        // return pointer type of generic parameter bound
+        return java_reference_type(parameter.subtype());


In the previous if block, for generic parameter which is not in the map, we return the parameter itself - the parameter is basically a pointer to its upper bound anyway. So for consistency, I suggest to do the same here.

majakusber · 2018-05-29T13:45:42Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+/// \param parameter_name The name of the generic parameter type we want to have
+///   instantiated
+/// \param generic_specialization_map Map of type names to specialization stack
+/// \param depth start depth for instantiation search


There is no depth argument in this function

majakusber · 2018-05-29T13:47:03Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+///   instantiated
+/// \param generic_specialization_map Map of type names to specialization stack
+/// \param depth start depth for instantiation search
+/// \return the first instantiated type for the generic type or nothing if no


Sometimes you use uppercase first letter in documentation of arguments and sometimes not, please make it consistent.

majakusber · 2018-05-29T13:59:05Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+/// recursion to prevent, visiting the same depth again and specify which stack
+/// depth is analyzed.
+/// \param visited tracks the visited parameter names
+/// \param depth stack depth to analyze


Uppercase first letter?

majakusber · 2018-05-29T14:02:52Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+  auto val = generic_parameter_specialization_map.find(parameter_name);
+  INVARIANT(
+    val != generic_parameter_specialization_map.end(),
+    "generic parameter must be a key in map");


Is this really an invariant? Not all parameters need to be specialized, for example if the method under test is generic. See similar case in specialize_generics.

else we would not have found the loop and the intention of this function is to break the recursion loop

I clarified that the function should only be called in the case of a recursion loop in specialize_generics

majakusber · 2018-05-29T14:06:21Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+    // avoid infinite recursion
+    if(visited_nodes.find(parameter_name) != visited_nodes.end())
+    {
+      optionalt<pointer_typet> result = get_instantiated_type(


I'm curious, specialize_generics is itself recursive, isn't this redundant in some way? Or does this new function solely serves the purpose of breaking cycles? If so, it would be helpful if you could change the name to something that reflects it, e.g., resolve_specialization_cycle or something like that.

I renamed them to get_recursively_instantiated_type

majakusber · 2018-05-29T14:07:11Z

jbmc/src/java_bytecode/select_pointer_type.cpp

@@ -109,3 +135,95 @@ pointer_typet select_pointer_typet::specialize_generics(
  }
  return pointer_type;
 }
+
+/// Return the first concrete type instantiation if any such exists.


If this function is meant to only be used to break cycles in specialization, please make it clear in documentation and an example would be very helpful here too.

I added

/// Return the first concrete type instantiation if any such exists. This method /// is only to be called when the `specialize_generics` cannot find an /// instantiation due to a loop in its recursion.

mgudemann · 2018-05-29T18:00:49Z

@svorenova I added a specialization with a cycle length of 3 as unit test

mgudemann · 2018-05-29T18:03:00Z

@svorenova when different specializations are used or on different levels, we will not hit the recursive definition. Or do you have a specific exmaple in mind for this ?

mgudemann · 2018-05-31T08:18:17Z

@svorenova @romainbrenguier please have another look

majakusber

Few more things, but the logic of it is now more clear to me, thanks for the updates. I couldn't come up with an example as I mentioned before, it doesn't seem to make sense :) But could you please add a test with a nested type like a class Gen<T,U> with a field Gen<Gen<U,U>,T> or some other variations of it? I can't quite see how it would behave in this case.

majakusber · 2018-05-31T08:23:30Z

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

+        }
+      }
+    }
+    THEN("The Object has a field `example3` of type `Outer<Boolean, Byte>`")


This should be Outer<Boolean, Byte, Short>, and fields for inner are also not quite right - the type of o has also three parameters and test for u is missing.

I'm not quite sure how this test is passing actually :)

why is it wrong? K and V are instantiated with Boolean and Byte, U is Short. U isn't directly used in Outer, only to instantiate Inner (I added the test to check Inner.u). Inner then contains a field of Type Outer<V, K, U> i.e., Boolean and Byte are reversed in that field

In THEN, the type should be Outer<Boolean, Byte, Short>, that's the full type of example3. This is the only thing that is wrong, so now I see how this is passing, the test for inner is indeed correct. What got me confused is that the correct instantiation is tested via checking the types of fields, not the expression type (java_generic_typet with the expected list of generic variables). I guess that would be a completely different test though, in a later stage than goto I guess? In any case, the only thing that doesn't match is the comment in THEN.

majakusber · 2018-05-31T08:32:29Z

jbmc/src/java_bytecode/select_pointer_type.cpp

-      generic_parameter_specialization_map.find(parameter_name)->second.top();
+      generic_parameter_specialization_map.find(parameter_name)->second.back();
+
+    // avoid infinite recursion


Can you please move this block that handles recursion to the beginning of this if block? The logic of the subsequent steps would be more clear - if you're specializing a parameter, first check if you've seen it already (i.e., there's recursion), if not try to find it in the map.

majakusber · 2018-05-31T08:33:03Z

jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h

-      if((*generic_parameter_specialization_map.find(key)).second.empty())
+      auto &val = generic_parameter_specialization_map.find(key)->second;
+      val.pop_back();
+      if(val.empty())
      {


Curly braces can be removed here

majakusber · 2018-05-31T08:42:43Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+        ->second.back();
+    const java_generic_parametert &gen_param = to_java_generic_parameter(entry);
+    const auto &type_var = gen_param.type_variable();
+    current_parameter = type_var.get_identifier();


The above three lines can be replaced with current_parameter = to_java_generic_parameter(entry).get_name();.

majakusber · 2018-05-31T08:43:23Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+}
+
+/// See get_recursively instantiated_type, the additional parameters just track
+/// the recursion to prevent, visiting the same depth again and specify which


Typo - no comma needed here

majakusber · 2018-05-31T08:44:43Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+  //   instantiation
+  // - if nothing can be found at the given depth, an empty optional is returned
+
+  auto val = generic_parameter_specialization_map.find(parameter_name);


Do you actually need to assign it to a variable? In the invariant, you can perhaps use count and then only assign replacements as generic_parameter_specialization_map.find(parameter_name)->second.

not doing two lookups was the other reviewers comment here

majakusber · 2018-05-31T08:48:57Z

jbmc/src/java_bytecode/select_pointer_type.h

@@ -34,7 +45,8 @@ class select_pointer_typet
  pointer_typet specialize_generics(
    const pointer_typet &pointer_type,
    const generic_parameter_specialization_mapt
-      &generic_parameter_specialization_map) const;
+      &generic_parameter_specialization_map,
+    generic_parameter_recursion_trackingt &) const;


Since all the other arguments are named, I would call it visited.

majakusber · 2018-05-31T08:52:07Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+    return {};
+  }
+
+  const size_t index = (replacements.size() - depth) - 1;


Nit - (replacements.size() - 1) - depth is more understandable to me, as replacements.size() - 1 is the last element index and you go through them from the back. But it's just a minor thing so keep whatever makes more sense to you.

majakusber · 2018-05-31T08:54:21Z

jbmc/src/java_bytecode/select_pointer_type.cpp

+  visited.insert(parameter_name);
+  const auto &gen_type = to_java_generic_parameter(type).type_variable();
+  const auto inst_val = get_recursively_instantiated_type(
+    gen_type.get_identifier(),


You can use to_java_generic_parameter(type).get_name() to get the parameter name directly, no need for an extra variable.

mgudemann · 2018-06-05T13:06:43Z

new ticket is TG-3828

majakusber

Looks good but there are some doxygen/linter failures and the tests in CI did not run for some reason? For the new ticket - when you'll have time, please fill in more information (including the nested example) and fix the formatting. Thank you!

majakusber · 2018-06-05T13:24:22Z

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

+              "java::java.lang.Integer",
+              "java::java.lang.Byte",
+              "java::java.lang.Character");
+          }


Please add a TODO here with the new ticket number to test example3.

mgudemann · 2018-06-05T15:11:33Z

@svorenova looks better now, waiting for appveyor, added todo as suggested

This makes the generics type tracking information traversable, allows for push_back / pop_back and provides constant time access to any element.

thk123

Please add the regression test from the original ticket.
Please add a test for arrays
Please add a test for inheritance

thk123 · 2018-06-07T13:16:14Z

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

+        require_goto_statements::require_struct_component_assignment(
+          tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code);
+
+      const auto has_x_u_e_fields = [&](


has_x_e_u_fields

thk123 · 2018-06-07T13:21:49Z

jbmc/src/java_bytecode/select_pointer_type.cpp

 {
  if(is_java_generic_parameter(pointer_type))
  {
    const java_generic_parametert &parameter =
      to_java_generic_parameter(pointer_type);
    const irep_idt &parameter_name = parameter.get_name();
+
+    // avoid infinite recursion


Please expand this comment with how we avoid infinite recursion:

// avoid infinite recursion by looking at each generic arguments previous assignemnt

?

thk123

Agreed extra tests would be added as part of the spun out ticket.

9441a92 Merge pull request diffblue#2317 from tautschnig/c++-attributes-lists cad7b3a Merge pull request diffblue#2297 from romainbrenguier/bugfix/starts-with 7a6277d Reformat documentation without latex 0c56151 Add test for StartsWith d599dfc Allow duplicate instantiations of the same constant string 6763669 Correct starts_with for offset out of bound case 71f80e1 Deprecates add_axioms_for_is_suffix 8ee1c16 Merge pull request diffblue#2340 from tautschnig/c++-cassert 39a5631 Enabled failed-tests output in cbmc-cpp fafe4d9 C++ front-end: support =delete method declarations e3de3f6 Re-enable access control checks df85911 Fix access in test b092a13 char16_t and char32_t are typedefs in Visual Studio 1e00fcf Default to C++14 as language standard accepted by the C++ front-end on Windows 61ec7fc Merge pull request diffblue#2331 from diffblue/arch_flags_tests 8b2fc41 mark gcc tests as 'gcc-only' to prevent execution by goto-cl on Windows ebf7c7e fix return values of __builtin_classify_type 57ed2bc fix gcc_attributes10 2796025 Merge pull request diffblue#2329 from diffblue/msvc_packed_union 37c0b83 Merge pull request diffblue#2309 from qaphla/regression be6f3c9 Merge pull request diffblue#2346 from peterschrammel/fix-class-models-nondet d49ea09 Added an initial set of tests for contracts, which (expectedly) either fail or will need to be redone once the new flags are added in. d17c990 Merge pull request diffblue#2321 from tautschnig/vs-temporary-filet 43d008a Merge pull request diffblue#2347 from diffblue/smt2-bounds-checks dfff111 Merge pull request diffblue#2348 from tautschnig/c++-block-pointer 1d93fa1 Visual Studio packs bit-fields differently bffb1ca smt2_parser: avoid access to vector without prior size check e6d76e5 Merge pull request diffblue#2349 from tautschnig/document-gcc-req 7d0195a Fix allow-null initialization logic for class models 5a50203 Merge pull request diffblue#2308 from smowton/smowton/feature/must-not-throw-annotation bd74d87 Merge pull request diffblue#2343 from tautschnig/c++-auto d08a75a Document the required GCC/G++ version as >= 5.0 612fc38 C++ front-end: Type check Apple block pointers 278e506 Merge pull request diffblue#2345 from tautschnig/c++-array-ini af83568 C++11 auto type specifier 24ba2a0 Tests for proper pre-C++11 handling of "auto" 830c1d8 Revert "parse C++11 auto declarations" f3a3e79 Merge pull request diffblue#2344 from tautschnig/c++-vs-enum ce4884e C++ front-end: maintain #array_ini flag 19cfa50 Visual Studio supports C11 _Alignof e0d56da Support Visual Studio's forward enum declarations ab60852 Add org.cprover.MustNotThrow method attribute 5b8897e Merge pull request diffblue#2342 from tautschnig/constructor 12e8f46 Merge pull request diffblue#2341 from tautschnig/c++-qualified bc568b7 Only parameter-free constructors can be static initializer functions 57a14b0 C++ front-end: qualified template specialisation can just be accepted bcf8e61 Use temporary_filet for automatic resource management 1d95ab4 Permit compound literals in place of PODs e229b4c Typecheck initializer lists 999ad15 Swap order of subtypes in construction of merged_type nodes 4a47de6 Mark already-typechecked types as such d5183fb Permit GCC attributes after struct/class in class declaration d82f554 Permit asm post-declarator mixed in any order with other qualifiers fde09ca C++ front-end: parse GCC attributes 1f9deb3 Merge pull request diffblue#2333 from tautschnig/reduce-test-memory-footprint 04a8c35 Merge pull request diffblue#2334 from tautschnig/c++-virtual 0216dbd Merge pull request diffblue#2336 from tautschnig/c++-pointer-to-member 73d688d Merge pull request diffblue#2270 from peterschrammel/fix-stub-identifiers 13a1afc Merge pull request diffblue#2338 from tautschnig/c++-enum-operator 4ff6d5c Merge pull request diffblue#2337 from tautschnig/c++-enum-class 21bbecc Reduce memory cost of test by using a scalar variable instead of an array 439d6d3 Merge pull request diffblue#2332 from diffblue/goto-cc-warning-syntax a8f9fd9 C++ front-end: support pointer to non-method members 2f34833 C++ operator overload over enum tag types 4637f87 Fix virtual table construction f3550ea Cleanup: is_virtual is trivally true in this context a172c34 C++ virtual tables: fix inconsistent string suffixes ec5425e Code cleanup a7502c9 C++: support enum class 9e9f251 Prefix identifiers in stubs with function name 774060b Merge pull request diffblue#1768 from peterschrammel/fix-java-main-harness 3cb8bcf Deduplicate string tests 9b19015 Fix tests with incorrect main methods b047091 Simplify main method detection for Java b726dd1 Add regression tests for initialization of Java main args 7348c74 Elements of String array argument to Java main cannot be null 751c040 Simplify check whether String model is present 7a3a07f fix test result for goto-cl 8f2a82e Generalize allow_null to max_nonnull_tree_depth bbe8cca Java main method must be public 86b143b Merge pull request diffblue#2316 from tautschnig/ssa-perf-fix a6d32eb Merge pull request diffblue#2323 from tautschnig/vs-float 86687f7 Fix typos in doxygen f2ec10e Merge pull request diffblue#2320 from tautschnig/vs-return-type 0f2cc3a Merge pull request diffblue#2330 from diffblue/msvc-utf8 bdd5bbb ask CL preprocessor for UTF-8 output 1df3b9d Merge pull request diffblue#2325 from tautschnig/vs-empty-files ecee38d Remove useless cpp files ae1d039 Merge pull request diffblue#2322 from tautschnig/vs-cstring aeafc49 Merge pull request diffblue#2311 from diffblue/aws-codebuild-windows d4cd32d AWS codebuild buildspec for Windows 2c21295 missing dependency in Makefile 3fcdae1 Merge pull request diffblue#2319 from tautschnig/vs-linker-warning 6c22191 Merge pull request diffblue#2312 from diffblue/missing-iterator-headers 6a16f85 Merge pull request diffblue#2324 from tautschnig/vs-big-int-copyright d9a2339 Merge pull request diffblue#2327 from mre/patch-1 363291a Fix typo 8d6335a big-int copyright line c15f47f Mark floating-point constants as float 7e03746 Avoid using C string functions 3e8eff4 Fix the return type to match the class member types 1cb3d4d Avoid Visual Studio linker warning 33787ed missing <iterator> header 223d872 Revert undocumented change of 27153d1 63acc5b Merge pull request diffblue#2303 from smowton/smowton/fix/initialize-before-class-literal-init f927ae9 Merge pull request diffblue#2313 from smowton/smowton/admin/coverity-travis 6982f86 Improve coverity Travis build 894a20f Merge pull request diffblue#2294 from tautschnig/c++-built-ins 4edecbc Rename add_cprover_X_library to cprover_X_library_factory 1201ffe C++ front-end: Use C factory for compiler builtins 0451f1e C++ front-end now has its own library ed05d3e Refactor add_cprover_library to make parts re-usable by the C++ front-end 0ea6143 Make link_to_library independent of the C front-end c8702ab CPROVER library linking: move status message to front-end c471f72 jdiff: remove C library d597d90 Remove unused include 6877b21 Merge pull request diffblue#2305 from tautschnig/c++-operator da5ce90 Fix operator parsing 0d04f37 Merge pull request diffblue#2239 from mgudemann/bugfix/generics/fix_infinite_recursion 2e83ec9 Zero-initialize Class literals before calling initializer function b7725b8 Merge pull request diffblue#2306 from tautschnig/c++-qualifiers 0612749 Merge pull request diffblue#2304 from tautschnig/appveyor-warnings e54bba2 Merge pull request diffblue#2293 from tautschnig/c++-decltype-bit-field d196cf7 Add regression test for recursive generic-parameters 934c555 Do not lose method qualifiers d7b1572 Doxygen update 2d9970c Clarify and correct 04565b4 Un-deprecate to_integer(constant_exprt) feb59ab Use not-as-deprecated version of to_integer e23a1bb Avoid deprecated code_typet() constructor aef48c2 Avoid implicit cast int -> bool c5de7ba Merge pull request diffblue#2296 from smowton/smowton/fix/restore-float128 8c08946 decltype(bit field type) is the underlying subtype 9160e99 Merge pull request diffblue#2292 from tautschnig/c++-windows 7b61482 Extend cbmc ts18661 test 4180e65 Add test for gcc-5 b46e4bf Improve gcc-4 and -7 tests b0d1f9e Restore _Float128 support by default 22b9182 Merge pull request diffblue#2165 from tautschnig/interpreter-member-offset 5fd18a9 Enable C++ regression tests on AppVeyor 8d86e44 Prevent regression failures of cpp tests on windows 9adf5f1 Configure C++ language standard in goto-cl 10a4685 Merge pull request diffblue#2219 from tautschnig/nondet-initializer e12cb04 Merge pull request diffblue#2298 from tautschnig/move-printf_formatter 71c1227 Merge pull request diffblue#2299 from tautschnig/no-c_qualifier 339fcbd Merge pull request diffblue#2300 from tautschnig/no-c_typecast 0a77ce0 Do not use c_qualifiers on goto-program expressions d089ddd Do not use c_typecast in pointer-analysis 60ab7ec Array/vector sizes can be size_t 4031eac Non-negative array/vector sizes are invariants cf41a88 nondet_initializer to build deep non-deterministic expressions 626fb98 Rename zero_initializer to expr_initializer in preparation of generalisation bc15b1b Move zero_initializer to util 7716f3f Remove unused include cc23b20 Move printf_formatter to goto-programs 2ed63f5 Merge pull request diffblue#2156 from tautschnig/gcc-8-fixes 260156f Merge pull request diffblue#2288 from peterschrammel/code-type-const 2bea6fc Merge pull request diffblue#2274 from peterschrammel/travis-new-doxygen c6cfb02 Merge pull request diffblue#2291 from tautschnig/c++-fixes-1 80112d8 Make CMake regression test set match the Makefile one 63c5a32 Install doxygen 1.8.14 on travis 1bd942f Remove redundant invariants 11005ec Remove duplicate save_scope fc670b5 Do not lint .h files in regression/ 763d4d1 Style improvements 204c60f Failing regression test from diffblue#933 1132562 Failing regression test from diffblue#661 fe8ef6d Whitespace cleanup, comment type fixed 5bb13db Initial set of mini-system-c tests 3564324 Line break 402b29b Fix broken comment frame 8480d96 Fix command-line option syntax a3a4696 Fix syntax errors in C++ regression tests f2c60cf Do not use assert without prior declaration 7c053bf Merge pull request diffblue#2290 from diffblue/flt_rounds 4a7a389 Merge pull request diffblue#2262 from karkhaz/kk-rm-noop-depth-lookup 43b41a4 Simplify return f6586ed Rename functions to `get_recursively_instantiated_type` b0fde14 Doxygen update, clarification 8b4920e Return input pointer_type in case of no instantiation 05ff12d Clarifications and corrections 2c5e0b8 Return bound if no concrete instantiation is found 26e5433 Add unit test for mutually recursive generic parameters 6ff2993 Choose mapped-to type when doing higher depth search 31004f5 Search through stack for instantiation 3264023 Fix Typo 258e3ae Track recursion for generic type parameter definition 7360696 Use `std::vector` instead of `std::stack` 8f094e2 added model for FreeBSD __flt_rounds 98379b3 Interpreter: simplify code by not using member_offset_iterator 64cd733 Make code_typet declarations const 6d5e446 Merge pull request diffblue#2240 from diffblue/get-gcc-version b618d94 Merge pull request diffblue#2269 from peterschrammel/parameters-code-type 2a72bf2 Merge pull request diffblue#2268 from allredj/trigger-testgen 78794e2 undo parts of diffblue#2185 e040723 _FloatX support based on gcc version cd6ecec goto-cc now reports version of installed gcc fd910a7 added gcc_versiont 09a4e6c run() can now redirect stderr 32fd0c2 Return original type instead of nil in original_return_type 29bf299 Test for incomplete code_typet construction 05a5efb Use the two-param code_typet constructor 103c7b7 Add missing module definitions 724a36c Add two-param code_typet constructors and deprecate the default one 63a5131 Make sure code_typet is fully constructed 61b9647 Revert 0b3170d: Stabilize clinit wrapper function type parameters da34ceb Merge pull request diffblue#2283 from tautschnig/appveyor-fix 4d70915 Merge pull request diffblue#2279 from diffblue/void-star-arithmetic d668583 Merge pull request diffblue#2282 from diffblue/unused-lambda-capture 2a2907e Unstall AppVeyor by checking for the correct file path 7bad913 the 'this' capture is not used d24f773 Merge pull request diffblue#2233 from thomasspriggs/global_null_message_handler 690613d Merge pull request diffblue#2275 from tautschnig/gcc-case-range e8ff243 Merge pull request diffblue#2225 from cesaro/extended-java-models 5242dc9 Merge pull request diffblue#2265 from smowton/smowton/fix/dont-advertise-ignored-methods 6eab2f9 document why sizeof(void) works 690d10b Merge pull request diffblue#1956 from romainbrenguier/refactor/prop_conv_straightforward2 fc33598 Implement GCC's switch-case ranges e8d26ae Merge pull request diffblue#2267 from LAJW/lajw/always-load-cprover-nondet-initialize c6d2dba JBMC: Added java-models-library dependency e5f3c41 Use a reference with exception types that use vtables 7211280 Silence spurious GCC 8 warning 0c00835 Do not use parentheses around the declared symbol 4f3c102 Silence Minisat's use of realloc on non-POD and fix and use its xrealloc 3082d9d Merge pull request diffblue#2029 from tautschnig/remove-asm c14677b Java frontend: don't advertise ignored methods f8df76a Merge pull request diffblue#2276 from tautschnig/c-string-zero bb1bae9 Merge pull request diffblue#2184 from tautschnig/human-readable-output d35c2ac Refactoring in boolbvt::convert_byte_extract 523f8ae Zero-length C string operations should not yield pointer checks a673e5d Add test verifying that the cproverNondetInitialize method is always loaded 4d67ed5 goto-instrument: Remove inline asm before doing various operations 6f51513 Print (at debug level) the current SSA step being converted b0fce60 Print (at debug level) the size of assignments during symex e515f26 List all candidate functions for a function pointer at debug verbosity 9717af2 messaget helper to encapsulate if(debug-verbosity) { complex output } e698be9 Cleanup: use most suitable symbol_exprt constructor 07ef32d remove_const_function_pointerst::functionst only holds symbol expressions 75f021c Print current depth in BMC progress debug logging 65f0ec0 Provide a source location when analysis finds constness is lost 6f72d9b Split binary string in plain-text output of goto trace in groups of 8 0ff1384 Remove unused local variable e05dad5 Clang format include order. 8e20ac6 Use global `null_message_handlert` instead of duplicates. dab421c Add global instance of `null_message_handlert` 1a4fc92 Merge pull request diffblue#2089 from tautschnig/remove-skip-cleanup 971a34b Always load cprover-nondet-initialize d58eeb4 Add webhook to invoke a Diffblue-specific function 1b43ee9 Refactoring in boolbvt::convert_bitwise adc2d5d Make convert_abs take an abs_exprt parameter b837b8a Remove useless throws in boolbvt::convert_index 52d0fe4 Make build_offset_map return an offset_mapt 2dc7bee Replacing throws by invariants in boolbv convert 15ce938 Enable remove_skip to soundly remove skips with labels 3f34c1a Explicitly invoke goto_program.update() where remove_skip is not used 6bac80e Run remove_skip in passes that may introduce skips 533775c Remove redundant calls to compute_{location,loop}_numbers e9cdffd remove_skip includes goto_{program,functions}.update(), avoid redundant calls cfb733a Make remove_skip call goto_program.update() 91d47c2 remove_skip implementation restricted to a range of instructions 41d38bc Remove unused includes of remove_skip.h c9ead2c Avoid redundant calls to remove_skip 6298c18 Fix wrong function description 9e355e9 Use make_skip to turn an instruction into a SKIP b055179 Relax test: there need not be any code at the end of the block to cover f1a5d6a Make functions non-empty so that the test remains stable under skip cleanup 1bd4f04 JBMC: Minor fix, removing superfluous padding from converter b5ebe6b Remove string lookups from goto_symext main loop e77cabc Remove optionst member from goto_symext git-subtree-dir: cbmc git-subtree-split: 9441a92

mgudemann self-assigned this May 25, 2018

mgudemann requested review from cesaro, peterschrammel, smowton and thk123 as code owners May 25, 2018 21:02

mgudemann requested a review from majakusber May 25, 2018 21:03

mgudemann added do not merge work in progress labels May 25, 2018

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch 2 times, most recently from bc80f5a to 595fca7 Compare May 26, 2018 08:34

romainbrenguier reviewed May 29, 2018

View reviewed changes

mgudemann requested review from kroening and tautschnig as code owners May 29, 2018 10:59

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch from 70524c3 to 93970f2 Compare May 29, 2018 12:08

majakusber reviewed May 29, 2018

View reviewed changes

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch from f8125b6 to 341f53c Compare May 29, 2018 13:18

mgudemann removed do not merge work in progress labels May 29, 2018

majakusber reviewed May 29, 2018

View reviewed changes

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch 6 times, most recently from c001f6a to 0422748 Compare May 30, 2018 07:15

majakusber reviewed May 31, 2018

View reviewed changes

romainbrenguier approved these changes Jun 5, 2018

View reviewed changes

majakusber approved these changes Jun 5, 2018

View reviewed changes

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch 3 times, most recently from bd8f646 to 2b9953f Compare June 5, 2018 14:33

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch from 2b9953f to 97bb047 Compare June 6, 2018 07:32

Matthias Güdemann added 12 commits June 6, 2018 15:16

Use std::vector instead of std::stack

7360696

This makes the generics type tracking information traversable, allows for push_back / pop_back and provides constant time access to any element.

Track recursion for generic type parameter definition

258e3ae

Fix Typo

3264023

Search through stack for instantiation

31004f5

Choose mapped-to type when doing higher depth search

6ff2993

Add unit test for mutually recursive generic parameters

26e5433

Return bound if no concrete instantiation is found

2c5e0b8

Clarifications and corrections

05ff12d

Return input pointer_type in case of no instantiation

8b4920e

Doxygen update, clarification

b0fde14

Rename functions to get_recursively_instantiated_type

f6586ed

Simplify return

43b41a4

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch from 97bb047 to c5cef40 Compare June 6, 2018 13:18

thk123 reviewed Jun 7, 2018

View reviewed changes

Matthias Güdemann added 3 commits June 7, 2018 15:58

Clarify and correct

2d9970c

Doxygen update

d7b1572

Add regression test for recursive generic-parameters

d196cf7

mgudemann force-pushed the bugfix/generics/fix_infinite_recursion branch from c5cef40 to d196cf7 Compare June 7, 2018 14:23

thk123 approved these changes Jun 7, 2018

View reviewed changes

mgudemann merged commit 0d04f37 into diffblue:develop Jun 7, 2018

mgudemann deleted the bugfix/generics/fix_infinite_recursion branch June 7, 2018 18:08

[TG-3067] Support generic type parameters that create recursion loops in instantiation stack #2239

[TG-3067] Support generic type parameters that create recursion loops in instantiation stack #2239

Uh oh!

Conversation

mgudemann commented May 25, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mgudemann commented May 29, 2018

Uh oh!

majakusber left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mgudemann commented May 29, 2018

Uh oh!

mgudemann commented May 29, 2018

Uh oh!

mgudemann commented May 31, 2018

Uh oh!

majakusber left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber May 31, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber May 31, 2018 •

edited

Loading