Add support for inheritence of Java static fields. Fixes TG-2457 #1826

smowton · 2018-02-12T18:48:38Z

Up until now, the Java frontend ignored that a static field reference (e.g. A.x) in Java bytecode may refer to a static field belonging to any parent class or interface. This had gone un-noticed for a while, but recently came to a head because we had been creating a stub (nondet) symbol for the apparently-dangling reference to A.x, and my recent PR #1781, which moved stub static field initialisation into clinit routines, included an invariant that the class a stub field was attached to must itself be a stub (unavailable). In this case if the class A is concrete the invariant failed, exposing the latent bug that we had never been resolving static fields correctly.

This PR addresses the underlying bug by adapting our existing find-inherited-method machinery to handle finding inherited fields, and uses it both during stub global creation and when translating getstatic and putstatic bytecodes to find the correct static field symbol. When a static field cannot be resolved a stub is created, attached to an arbitrary stub class that is a parent of the type referred to. I believe in general we can't do better than that, as even if two types A and B are related somehow, and we see references to A.z and B.z somewhere in the code, we cannot determine whether those are inherited, or two different private/protected/default access static fields.

I recommend reviewing commit-by-commit, as the series starts with a couple of moves to share some existing code, which account for most of the diff.

smowton · 2018-02-12T18:56:14Z

Test-gen bump: https://github.com/diffblue/test-gen/pull/1489

mgudemann · 2018-02-13T14:11:27Z

regression/cbmc-java/inherited_static_field5/test.desc

+--
+--
+This is the same as inherited_static_field2, except that parent is opaque. It must pass because
+the field 'x' should be found on interface_with_static, and so not created as a stub on 'parent'.


if it must pass, then why is the match no success or fail?

mgudemann · 2018-02-13T14:23:06Z

src/java_bytecode/java_bytecode_convert_method.cpp


  java_bytecode_convert_method(class_symbol, method);
 }

 /// Returns true iff method \p methodid from class \p classname is
 /// a method inherited from a class (and not an interface!) from which
 /// \p classname inherits, either directly or indirectly.
+/// \param classname: class whose method is referenced
+/// \param methodid: method basename
+/// \param class_hierarchy: global class hierarchy


this parameter does not exist here

mgudemann · 2018-02-13T14:25:15Z

src/java_bytecode/java_bytecode_language.cpp

@@ -405,13 +410,14 @@ static void create_stub_global_symbol(
  new_symbol.base_name = symbol_basename;
  new_symbol.type = symbol_type;
  new_symbol.type.set(ID_C_class, class_id);
+  new_symbol.type.set(ID_C_access, ID_public); // Guessed.


What does guessed mean here? Please add some comment of why it's public rather than default for example.

mgudemann · 2018-02-13T14:28:23Z

src/java_bytecode/java_bytecode_language.cpp

+
+            log.warning() << "Stub static field " << component << " found for "
+                          << "non-stub type " << class_id << ". In future this "
+                          << "will be a fatal error." << messaget::eom;


is there an issue for this already? if not, would it make sense to add an easier to find TODO here?

I described the problem to @antlechner who I think was going to submit a fix in the near future. I'm not sure where such an issue should go; @antlechner would you mind making one?

PR is here: https://github.com/diffblue/models-library/pull/361
Once it's merged (and updated in test-gen) you should be able to replace the warning with an error. I added tests in my PR that showed the warning before the change in the model, and do not show it any more after the change.

mgudemann · 2018-02-13T14:35:44Z

src/java_bytecode/java_utils.cpp

+///   ancestors including interfaces, rather than just parents.
+/// \return the concrete component referred to if any is found, or an invalid
+///   resolve_inherited_componentt::inherited_componentt otherwise.
+resolve_inherited_componentt::inherited_componentt get_inherited_component(


it might make sense to return an optional inherited_componentt here instead of resolve_inherited_componentt::inherited_componentt(); in the case of access-protected fields.

Nah, that type already has a distinguished not-valid value.

peterschrammel · 2018-02-13T14:20:28Z

src/java_bytecode/java_utils.cpp

+    const auto &access=component_symbol.type.get(ID_access);
+    if(access==ID_public || access==ID_protected)
+    {
+      // since the component is public, it is inherited


public or protected

peterschrammel · 2018-02-13T14:22:53Z

src/java_bytecode/java_utils.cpp

+
+    if(access==ID_private)
+    {
+      // We return false because the component found by the component_resolver


"Return false" doesn't quite match the code below.

peterschrammel · 2018-02-13T14:25:43Z

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -385,6 +385,16 @@ void java_bytecode_convert_classt::convert(
      "."+id2string(f.name);
    new_symbol.mode=ID_java;
    new_symbol.is_type=false;
+
+    if(f.is_public)
+      new_symbol.type.set(ID_C_access, ID_public);


Why is ID_C_access used here, whereas for classes and methods we use ID_access?

Added comment -- it's so we don't get type clashes against constants, local variables, and anything else that might be assigned to a static field but doesn't itself carry a visibility modifier.

peterschrammel · 2018-02-13T14:32:46Z

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2025,6 +2027,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
      }
      results[0]=java_bytecode_promotion(symbol_expr);

+      // Note this initialiser call deliberately inits the class used to make


initializer

peterschrammel · 2018-02-13T14:33:22Z

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2067,6 +2073,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
      code_blockt block;
      block.add_source_location()=i_it->source_location;

+      // Note this initialiser call deliberately inits the class used to make


initializer

peterschrammel · 2018-02-13T14:37:09Z

src/java_bytecode/java_bytecode_language.cpp

@@ -390,12 +390,17 @@ static void generate_constant_global_variables(
 /// \param symbol_basename: new symbol basename
 /// \param symbol_type: new symbol type
 /// \param class_id: class id that directly encloses this static field
+/// \param force_nondet_init: if true, always leave the symbol's value nil so it
+///   gets nondet initialised during __CPROVER_initialize. Otherwise, pointer-


nitpick: initialized (in several places)

thk123

Some suggestions. Main critical problem is regex is wrong in the tests. Also in general, these tests aren't very precise and would be better being unit tests so that we can verify that the structure is as expected (particularly given the presence of tests where we don't even check if verification is successful or not).

I'm also concerned about whether it is "correct" to pick arbitrarily which class the static stub is put on? Normally that would be shunted to the solver no?

It would be good to see some tests for:

field hiding ✅
A extends Opaque extends C sort of test ✅
A extends B extends Opaque ✅
some sort of test that checks the last commit (i.e. replicating the unusual setup found in models) ✅
some tests (maybe already exist?) for private fields not be selected in children. ✅

thk123 · 2018-02-13T13:40:45Z

src/java_bytecode/java_utils.cpp

+      if(component_package == class_package)
+        return resolved_component;
+      else
+        return resolve_inherited_componentt::inherited_componentt();


Might be preferable to make this method use an optionalt

Nah, that type already has a distinguished not-valid value.

thk123 · 2018-02-13T13:41:20Z

src/java_bytecode/java_utils.cpp

+      return resolve_inherited_componentt::inherited_componentt();
+    }
+
+    INVARIANT(false, "Unexpected access modifier.");


UNREACHABLE; // Unexpected access modifier I think is preferred to INVARIANT(false, ...)

thk123 · 2018-02-13T13:47:41Z

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -385,6 +385,16 @@ void java_bytecode_convert_classt::convert(
      "."+id2string(f.name);
    new_symbol.mode=ID_java;
    new_symbol.is_type=false;
+
+    if(f.is_public)


Surely this is already done since we do things like:

component.get_access() == ID_public

how come this change is needed?

Those are class fields, which are given their visibility attributes at java_bytecode_convert_class.cpp:431 onwards. These are static fields, which were until now not given a visibility.

thk123 · 2018-02-13T13:59:16Z

src/java_bytecode/java_bytecode_language.cpp

@@ -523,6 +526,10 @@ bool java_bytecode_languaget::typecheck(
      return true;
  }

+  // Now that all classes have been created in the symbol table we can populate
+  // the class hierarchy:
+  class_hierarchy(symbol_table);


In this commit I can't see any removal of construction of the class_hierachy only the creation of an additional one, will see if it is in a later commit.

thk123 · 2018-02-13T14:04:22Z

src/java_bytecode/java_bytecode_language.cpp

@@ -457,7 +457,8 @@ static void create_stub_global_symbols(
            component,
            "java::" + id2string(parse_tree.parsed_class.name),
            symbol_table,
-            class_hierarchy);
+            class_hierarchy,
+            true);


This is worth a comment here (include interfaces as interfaces can define fields) (of course in Java9, interfaces can define methods so I suppose we'll need to come back to this anyway...)

Apparently default methods are actually in Java 8, but I guess this won't be the only problem with them!

thk123 · 2018-02-13T14:28:09Z

regression/cbmc-java/inherited_static_field4/test.desc

+CORE
+test.class
+
+^VERIFICATION (SUCCESSFUL)|(FAILED)$


This regex seems wrong, accordding to debuggex matches VERIFICATION SUCCESSFUL or FAILED, I think it should be:

^VERIFICATION (SUCCESSFUL|FAILED)$

thk123 · 2018-02-13T14:29:26Z

regression/cbmc-java/inherited_static_field5/test.desc

+CORE
+test.class
+
+^VERIFICATION (SUCCESSFUL)|(FAILED)$


If it must pass (as comment below suggests) how come we allow failed here? (Again the regex is wrong)

thk123 · 2018-02-13T14:33:11Z

regression/cbmc-java/inherited_static_field6/test.desc

+CORE
+test.class
+
+^VERIFICATION (SUCCESSFUL)|(FAILED)$


Regex wrong

thk123 · 2018-02-13T14:45:33Z

regression/cbmc-java/inherited_static_field6/test.desc

+^VERIFICATION (SUCCESSFUL)|(FAILED)$
+--
+--
+This test can either pass or fail as the first 'x' reference may legitimately be guessed to belong to


Is it not incorrect for this to be non-deterministic. Surely if x could below to both parent and interface_without_static it should be allowing cbmc the possibility that they belong to either or both or them?

Will address the correctness question in the top level thread

thk123 · 2018-02-13T14:47:06Z

src/java_bytecode/java_bytecode_language.cpp

@@ -449,7 +454,7 @@ static irep_idt get_any_incomplete_ancestor(
      classes_to_check.end(), parents.begin(), parents.end());
  }

-  INVARIANT(false, "input class id should have some incomplete ancestor");
+  return irep_idt();


Can we add a TODO here so that we come back and fix it.

Done at the callsite

smowton · 2018-02-14T08:58:32Z

@thk123 regarding the correctness question, any choice is possibly incorrect, as if we don't have the class file for A but we see a reference to B.x, where B inherits from A and does not define x, we cannot know whether B is referring to A.x, some parent of A, or some also-opaque interface that either A or B inherits. We can only guess.

This patch-set (almost) eliminates the definitely wrong case where we guess that the field belongs to B, which it certainly does not as we do have the bytecode for B and know it doesn't make such a definition. Similarly we would have previously got wrong the case where we have the bytecode for all classes involved, and A.x is sometimes referred to by A.x and sometimes by B.x.

The one remaining case where we introduce a field we know doesn't exist is when we see a reference to System.out, and we have a class file for System and all its ancestors, and so know there is no field "out" ever defined. That would normally be a fatal error, but the models library presently does this. Once its authors are convinced it doesn't behave this way any longer we should revert commit "Tolerate stub static fields defined on non-stub types".

Regarding the possibility of giving the solver the choice about which opaque static fields alias and which don't, this would be similar to letting it make a nondet choice about what invisible class hierarchy exists -- for example, if user code calls SomeOpaqueType.get(int), perhaps that is inherited from LinkedList.get(int)? I recommend if we want to go down this road it should be a separate block of work.

This actually doesn't have any logic specific to function calls, and can be used to resolve inherited fields too.

This can now resolve fields too, and is moved into java_utils so it can be used more widely.

This mirrors the annotation already present on methods, and is needed to resolve indirect reference to an inherited static field, similar to virtual call resolution. The access attribute is set as a comment so that in an assignment some_static_field = some_constant we don't need to attach spurious access tags to the constant, or scrub them from the field, for their types to be considered matching.

Bytecode can refer to a static field via a child class; for example, referring to B.f when the actual referee field is A.f, where B extends A. By missing this case we could previously accidentally create a stub global for (in this example) B.f.

This avoids constructing a fresh class_hierarchyt with a consequent sweep of the complete symbol table every time inheritence is queried.

Previously if a reference to static field A.x did not resolve, then A.x would be created as a stub, but this is inappropriate if A is a complete (non-stub) class. Instead, create the field on A's first ancestor that is incomplete.

Previously we assumed that static fields, like regular fields, could only be inherited from ordinary classes, but in fact they can also come from interfaces. We therefore augment resolve-inherited-component to optionally search in all ancestors including interfaces, and use that facility when searching for inherited static fields.

Previously they were always created on either the class that was referred to, or on some parent or grandparent; however, this was inappropriate if all those classes were concrete (non-stub) types but some interface *was* a stub. In that case an interface will be arbitrarily picked and given a stub field.

Previously it assumed that static field references were resolved in the bytecode (e.g. that a reference to A.somefield meant that A defines somefield). However in fact they can be inherited, and especially now that stub fields can be created on parent classes they are likely to appear there. As such the "get/putstatic" instructions now search the class hierarchy for the field they actually refer to.

Any choice here is wrong (we can't know the global's actual visibility because we don't have the bytecode). I guess at public visibility on the hunch that actually- shared globals are somewhat more common than private ones with the same name and type.

Normally this situation (a reference to static field A.x, when neither A nor any of its ancestors either define a field x or are opaque stubs) would be an error, probably indicating a class version mismatch, but at present some of our library models intentionally exploit this behaviour to obtain a nondet- initialised field. Therefore for the time being we tolerate the situation, initialising such fields in __CPROVER_initialize, as we cannot attach a synthetic clinit method to a non-stub type.

No functional changes.

smowton · 2018-02-14T14:11:16Z

@mgudemann @thk123 @peterschrammel changes applied, except as noted. Largest change: lots of new tests added, both regression and unit, which exercise all the cases @thk123 mentioned above and a few more.

thk123

Thanks for the diligence on these extra tests - they look really great!

thk123 · 2018-02-14T14:52:00Z

src/java_bytecode/java_bytecode_language.cpp

 static void create_stub_global_symbols(
  const java_bytecode_parse_treet &parse_tree,
  symbol_table_baset &symbol_table,
-  const class_hierarchyt &class_hierarchy)
+  const class_hierarchyt &class_hierarchy,
+  messaget &log)


Nit: isn't this normally called message_handler rather than log

That's not the handler, but the messaget itself. We don't usually pass those around, but I don't see any reason why not?

thk123 · 2018-02-14T15:00:54Z

regression/cbmc-java/inherited_static_field10/Test.java

@@ -0,0 +1,10 @@
+public class Test extends Parent {
+
+  public static void main(int nondet) {


I did not know it is valid Java to have a static main method that doesn't take String[] - awesome.

It isn't in Java, but it is in jbmc :) The JVM would say "that's not a proper main()", but jbmc only cares about the name, not the arg types.

Not blocking - but I'd suggest this isn't a great thing to therefore rely on in tests...

With #1768, you'll have to provide a --function to make this test run.

thk123 · 2018-02-14T15:12:02Z

unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp

+
+#include <util/expr_iterator.h>
+
+static bool contains_symbol_reference(const exprt &expr, const irep_idt &id)


A comment would be great here:

/// Check the full tree of expr for any symbol_exprts that have an identifier id /// \return true if a suitable symbol_exprt is found

thk123 · 2018-02-14T15:16:45Z

unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp

+    symbol_tablet symbol_table=
+      load_java_class("Test3", "./java_bytecode/inherited_static_fields");
+    THEN("A static field 'OpaqueParent3.x' should exist")
+    {


If someone updates Test3.java and recompiles it, the file will come back into existance, could you add a REQUIRE that the symbol for all the opaque classes is correctly marked as an ID_incomplete_class?

thk123 · 2018-02-14T15:18:02Z

unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp

+      load_java_class("Test5", "./java_bytecode/inherited_static_fields");
+    THEN("One or other parent (not both) should gain a static field 'x'")
+    {
+      REQUIRE(


These cover various permutations of static fields defined on parents, on interfaces, and those parents and/or interfaces being opaque (stubs). They check both that jbmc doesn't outright crash, and in some cases that jbmc correctly determines that two static fields must be the same one, and therefore cannot differ.

smowton · 2018-02-14T15:41:58Z

@thk123 changes applied

peterschrammel

Apart from the remaining open comment, LGTM.

smowton · 2018-02-14T22:28:36Z

In the interests of not blocking the test-gen fix I'll tweak the function names separately

f7602af Merge commit 'bb88574aaa4043f0ebf0ad6881ccaaeb1f0413ff' into merge-develop-20180327 906aeb3 Merge pull request diffblue#349 from diffblue/owen-jones-diffblue/fix-compilation-for-release 3d8423c Merge pull request diffblue#350 from diffblue/owen-jones-diffblue/skip-duplicate-callsites-in-lazy-methods 73fb488 bugfix from upstream repo for generic crash fd76555 Speed up resolution of virtual callsites in lazy loading 3fd28f3 Replace assert(X) by UNREACHABLE/INVARIANT(X) 557158e Merge pull request diffblue#334 from diffblue/pull-support-20180216 1e48132 Merge from master, 20180216 ad7b28e Updates requsted in the PR: mostly rename 'size -> length'. e3fcb9b Introducing MAX_FILE_NAME_SIZE constant. bb88574 Merge pull request diffblue#1806 from thk123/refactor/address-review-comments-from-1796 db9c214 Merge pull request diffblue#1850 from tautschnig/include-cleanup 78fbf08 Merge pull request diffblue#1844 from smowton/smowton/feature/prepare-symex-for-lazy-loading 4098ed5 Merge pull request diffblue#1849 from smowton/smowton/cleanup/java-main-function-types 06f3e83 Use C++ headers instead of their C variants e918a91 Goto-symex: add support for general function accessor 9e31303 Symex: switch to incrementally populating address-taken locals ac5af68 Address-taken locals analysis: support incremental analysis fe775f3 Merge pull request diffblue#1843 from peterschrammel/instructions-function a6fd729 Cleanup tests with anomalous main functions 5df3fca Clean up get_function_id hacks 552b100 Set function member of each goto instruction in goto program passes 38e6e4a Merge pull request diffblue#1813 from smowton/smowton/fix/cleanup-unused-clinits 278e4e6 Merge pull request diffblue#1826 from smowton/smowton/fix/java-inherited-static-fields a2ebb33 Merge pull request diffblue#1713 from karkhaz/kk-debug-timestamps 7b5dd17 Merge pull request diffblue#1834 from diffblue/library-preconditions 1da5be1 Add tests for inherited static fields 19d622b Add tests to verify that synthetic method removal is performed adc9fd4 Java frontend: clean up unused clinit symbols f15c312 Exclude j.l.O from possible static field hosts. afa443c US spelling of initialize d4d4a9a Tolerate stub static fields defined on non-stub types 873e1f6 Guess public access for stub globals d6783d8 Java method converter: look for inherited static fields 32cc538 Insert stub static globals onto any incomplete ancestor class b2d3d61 Search static fields inherited from interfaces 045ac05 Create stub globals on the first parent incomplete class 5b3cde5 Use a common instance of class_hierarchyt in get_inherited_component e73e756 Create stub globals: check for inherited globals bea6371 Annotate static fields with accessibility 168c2a8 Generalise get_inherited_method f3160e1 resolve_concrete_function_callt -> resolve_inherited_componentt 82549de Emit timestamps on each line of output 3f6965b Replace util/timer* with std::chrono ef08ae2 Merge pull request diffblue#1820 from smowton/smowton/fix/remove-string-solver-iteration-limit 0f20482 Merge pull request diffblue#1836 from karkhaz/kk-remove-unused-lambda-capture e8105bd Merge pull request diffblue#1833 from diffblue/symex_class_cleanup f6f45fc turn some assertions in the stdlib.h models into preconditions 9ea0cc6 pre-conditions for strings fbd54df Remove unused lambda capture 9620802 Merge pull request diffblue#1815 from smowton/smowton/feature/replace-clinit-unwinder 9b59631 Merge pull request diffblue#1828 from smowton/smowton/cleanup/remove-recreate-initialize 1ac9abe Remove string refinement iteration limit c94548c preconditions for delete and delete[] 9ba7fe2 cleanup of some noise (mostly obvious declarators) in the goto_symext class bb64ea6 clean up symex_assign vs. symex_assign_rec 932a38f Merge pull request diffblue#1827 from karkhaz/kk-symex-operator-tidy 968d97e Remove __CPROVER_initialize recreation 06a220a Reimplement remove-static-init-loops to avoid need to inspect GOTO program 2bb98d9 Merge pull request diffblue#1819 from romainbrenguier/refactor/coverage-instrumentation 6492b3a Rearrange cover_basic_blocks header a9549e7 Define constants as const fa35ccd Pull continuation_of_block function out 560d712 Declare constants as const 35422f3 Make update_covered_lines a static function b4cadf8 [path explore 1/8] Tidy up symext top-level funs 0f3ae1a Make representative_inst an optional dc696a4 Make format_number_range function instead of class 678218a Merge pull request diffblue#1825 from thk123/refactor/corrected-path-of-language-file ba76a8f Merge pull request diffblue#1751 from tautschnig/fix-1748 b665269 Correcting path to a file d0889a8 Merge pull request diffblue#1822 from diffblue/legacy-language 441f706 Merge pull request diffblue#1823 from diffblue/cleanup 11714b2 use constant_exprt version of to_integer 733f3b8 remove old-style constructor for member_exprt 63f09ac remove unused function make_next_state 77c8b9c remove translation for certain boolean program constructs 1bac484 cleanout decision_proceduret::in_core d8967f5 moving language.h and language_file.h to langapi folder f9b9599 Merge pull request diffblue#1761 from diffblue/function_typet dd040e5 Added function_typet. bcd88a0 Merge pull request diffblue#1821 from smowton/smowton/feature/test-pl-tags 45f0939 test.pl: add support for tagging test-cases 40b8c03 Updates requested in PR - mainly rename of functions. 7f868e2 Reused private code in 'remove_virtual_functions.cpp' by making it public. ae6775a Merge pull request diffblue#1790 from martin-cs/fix/correct-domain-interface d7bb937 Catch the case when a GOTO instruction is effectively a SKIP. b2fba97 Correct domain transformers so that they meet the preconditions. d447c26 Document the invariants on iterators arguments to transform and merge. e3db794 Whitespace changes to keep clang-format happy. 1990994 Revert "Add edge type parameter to ai transform method" 3ca91bc Revert "Fix iterator comparison bug in reaching_definitions.cpp" ac036fd Revert "Fix iterator equality check bug in dependence_graph.cpp" 86cadcd Revert "Fix iterator equality check bug in custom_bitvector_analysis.cpp" db925de Revert "Fix iterator equality check bug in constant_propagator.cpp" 2c69364 Merge pull request diffblue#1811 from cesaro/iterator-fix 807268e Fixes the symbol_base_tablet iterator 0df054c Merge pull request diffblue#1781 from smowton/smowton/feature/java-create-stub-globals-earlier e163ab6 Java frontend: create synthetic static initialisers for stub globals fbcb423 Merge pull request diffblue#1802 from NathanJPhillips/feature/symbol_iterator e106cf8 Merge pull request diffblue#1793 from smowton/smowton/cleanup/remove-java-new-lowering-pass 52dfc36 Merge pull request diffblue#1731 from diffblue/bugfix/all_resolved_calls f123ae9 Adding comment referencing where the invariant comes from f7c89e1 Add iterator for symbol_table_baset 150f826 Merge pull request diffblue#1801 from hannes-steffenhagen-diffblue/add-idea-gitignore 745afbc Merge pull request diffblue#1796 from thk123/refactor/bytecode-parsing-tidy 6362295 Add .idea (CLion) directory to .gitignore 31da890 Revert "Do lowering of java_new as a function-level pass" 6f6fda7 Merge pull request diffblue#1794 from smowton/smowton/fix/goto-diff-test-escapes 4a538d2 Adding comments on the non-standard patternt 9bfe177 Adding an early guard for correctly parsed exception table 6fe1808 Improved error reporting on invalid constant pool index 93dab4c Escape curly braces in regexes 814cfcc Adapt failing unit test for value set analysis 3ff90bc Add unit test e67a96e Add regression test 3df5348 Adapt regression tests for virtual functions. 09efc90 Re-Resolve function calls if only java.lang.Object was found. a619e48 Merge pull request diffblue#1763 from jeannielynnmoulton/base_class_info_tg1287 0b8dd57 Merge pull request diffblue#1785 from smowton/smowton/fix/core-models-cmake-script 50dcec8 Adding unit tests for extracting generic bases' info 54df3a1 Correcting generic parameters in bases for implicitly generic classes 6d691d7 Parsing generic bases' information into the class symbol 7d041f0 Defining a new type for generic bases f10eb71 Fix Java core-models build script 8d66028 Merge pull request diffblue#1774 from smowton/smowton/feature/java-create-clinit-state-earlier 679d9b8 Java frontend: create static initialiser globals ahead of time 4a93a29 Merge pull request diffblue#1788 from smowton/smowton/fix/java_tcmp_nan 6ad8ffd Fix Java ternary-compare against NaN 1e0ac30 Turn get_may, set_may, etc into irep_ids b0cb1ee Merge pull request diffblue#1766 from smowton/smowton/feature/java-frontend-create-literal-globals-early a2e3af5 Merge pull request diffblue#1744 from smowton/smowton/feature/instrument_cover_per_function 22ae7aa Merge pull request diffblue#1637 from tautschnig/bswap a1a972f Merge pull request diffblue#1776 from smowton/smowton/feature/class-hierarchy-grapht ef3c598 Merge pull request diffblue#1775 from diffblue/refactor/set_classpath 45dd840 Merge pull request diffblue#1728 from romainbrenguier/refactor/split-axiom-vectors 8a27950 Java frontend: create String an Class literals earlier d95cb12 Move string literal initialisation into separate file 515ebdd CI lazy methods: scan global initialisers for global references cab7b52 C front-end: fix promotion order for types ranking lower than int c450328 Support for --16 on Visual Studio, no _WIN64 in 32-bit mode b2c4188 Do not use non-trivial system headers with --32 80b972b Use split_string in set_classpath fdb2ebc Merge pull request diffblue#1773 from smowton/smowton/feature/string-solver-ensure-class-graph-consistency a6eed7c Add class-hierarchy variant based on grapht 311af6d Coverage: fully support instrumenting one function at a time ceafd85 Java string solver: ensure base types are loaded 1e17db6 Merge pull request diffblue#1735 from cesaro/core-models 6844760 Merge pull request diffblue#1769 from smowton/smowton/fix/nondet-initialize-after-initialize a8e659c Fixed CMake linker ODR violations caused by a regression-test f66288b Internalize core models of the Java Class Library 34216f5 Refactor jar loading ed008f9 Add constructors for having memory-loaded jar files This allows the jar_file class to load from a buffer (c array) as opposed to a file 86a34c9 Merge pull request diffblue#1765 from smowton/smowton/fix/ci-lazy-methods-array-element-types 1e11f6d Add test for multiple array types in single method 5009cbb CI lazy methods: re-explore array types with different element types 857fcf9 Cleanup unused fields in string refinement 51d86f5 Adapt unit tests for splitted axiom vectors 1843e44 Split string generator axioms into separate vectors 5669d9b Java: run nondet-initialize method *after* initialization 0b5a5c3 Rename test case 3440018 Provide function name in goto_model_functiont f17e2c8 Merge pull request diffblue#1741 from smowton/smowton/feature/add_failed_symbols_per_function f65f0fd Merge pull request diffblue#1764 from smowton/smowton/feature/java-infer-opaque-type-fields-earlier dbc00a7 Add doxygen to add-failed-symbols 3788467 JBMC: add failed symbols on a per-function basis e934867 Provide a journalling symbol table to process-goto-function e86e2a0 Java: infer opaque type fields before method conversion f0f50e3 Journalling symbol table: enable nesting 58d5980 Merge pull request diffblue#1740 from smowton/smowton/feature/adjust_float_expressions_per_function c91ff69 JBMC: adjust float expressions per function eed983a JBMC: add property checks on a per-function basis db3bc99 JBMC: run convert-nondet on a per-function basis 99ea8fe JBMC: run replace-Java-nondet on function-by-function basis bfd4f50 Merge pull request diffblue#1730 from smowton/smowton/feature/remove_returns_per_function 96569c3 JBMC: remove return values on a per-function basis a7595c1 Remove returns: support running per-function fd6e195 Merge pull request diffblue#1718 from cesaro/concurrency-team-small-fixes e6fe617 Merge pull request diffblue#1705 from jgwilson42/goto-diff-tests 22afc5c Fixes wrong invocation order for static initializers 5c3997d Refectors how CBMC interprets a codet thread-block 001c1a2 ireps of type "ID_atomic_begin" and "ID_atomic_end" will now be properly displayed when the "show-symbol-table" flag is specified. d978ef9 Folder build/ ignored. bc145fd Merge pull request diffblue#1756 from romainbrenguier/tests/index-of-corrections#TG-2246 47b4ee9 Merge pull request diffblue#1725 from cesaro/exception-handlig-fixes d397d6a Merge pull request diffblue#1726 from diffblue/multi_ary_expr2c bd95317 Merge pull request diffblue#1753 from diffblue/xor_exprt 1d4af6d Merge pull request diffblue#1747 from NathanJPhillips/feature/upstream-cleanup 9c7debb Merge pull request diffblue#1750 from pkesseli/feature/sat-interrupt f11c995 Merge pull request diffblue#1749 from pkesseli/ci/remove-unapproved 981c8e0 Merge pull request diffblue#1743 from tautschnig/dump-c-fix bcb076b Correct tests for String.indexOf ef5c6f0 Merge pull request diffblue#1742 from owen-jones-diffblue/owen-jones-diffblue/small-shared-ptr 6c9f05e Fixes to exception handling behaviour 80dd48a added multi-ary xor_exprt 703e4a3 Remove unapproved C++11 header warning. bf7ed1a Merge pull request diffblue#313 from diffblue/owen-jones-diffblue/add-structured-lhs-to-value-set cc9398d Expose MiniSAT's `interrupt()` 8360233 Merge pull request diffblue#1646 from peterschrammel/list-goto-functions e4a2763 Tests for scope changes for variables and functions 8ee1956 goto-diff tests for package name changes ce3a5e9 Basic tests for java goto-diff 3bf9987 Compare access qualifiers in goto-diff f71cc7f Attach class name to method symbol 1f06d35 Merge pull request diffblue#312 from diffblue/pull-support-20180112 fda9daa Cleanup of create-and-swap to emplace e42e97a Merge commit '23666e3af35673c734c9816ffc131b6b9a379e86' into pull-support-20180112 53f1a41 Populate structured_lhs in all `entryt`s d7121f2 dump-c: fix support of use-system-headers eb5ec24 Merge pull request diffblue#1736 from hannes-steffenhagen-diffblue/develop_fix-bitfield-pretty-printing 7a0de46 Add comment suggested by @owen-jones-diffblue b741d4b Use small intrusive pointer in irep 434cc99 Merge pull request diffblue#1732 from peterschrammel/catch-sat-memout 8ae53bb Merge pull request diffblue#1733 from peterschrammel/mem-limit 574101c Add `structured_lhs` field to entryt 4f1a67a Uses alternatives to get_string in type2name when possible b46149d Merge pull request diffblue#1719 from smowton/smowton/cleanup/remove_exceptions_single_global 82a7ec6 Adds regression test for bitfield naming bug 651d8d1 Fixes use of wrong identifier when pretty printing bitfield types 638937a Merge pull request diffblue#1709 from romainbrenguier/doc/string-solver-intro 1d1be4c Move non-string-specific part of doc to solvers 549eb57 Delete trailing whitespaces db3e044 Add introduction to string solver documentation 74be7fb Merge pull request diffblue#1729 from romainbrenguier/refactor/unused-nonempty-option d101b22 Set memory limit utility ef45a1d Replace assertions by invariants 84e04a7 Catch Glucose::OutOfMemoryException 89fc48d Replace assertions by invariants 5e85701 Catch Minisat::OutOfMemoryException b8cee29 Enable list-goto-functions in clobber d902ec8 Replace cout by message stream in show-goto-functions d970673 Move show-loops in the right place in goto-diff e1227ef Enable list-goto-functions in goto diff 7e1110c Enable list-goto-functions in goto-instrument 0fb4868 Enable list-goto-functions in goto-analyzer e67abfa Remove exceptions: switch to single inflight exception global 2fabbd4 Enable list-goto-functions in JBMC 9e1705f Enable list-goto-functions in CBMC ebd8248 Add list-goto-functions command line option 2fe43a9 Add parameter to list goto functions without printing bodies 3d492fe Add documentation of return values 5a8eea5 Remove the string-non-empty option 9810f92 Drop string_non_empty field for string refinement fec16d7 expr2c now distinguishes binary and multi-ary expressions d16a918 C library: network byteorder functions 05bc9ed Implement bswap in SAT back-end 4f37035 Introduce bswap_exprt git-subtree-dir: cbmc git-subtree-split: f7602af

smowton requested review from cesaro, kroening, mgudemann, peterschrammel, tautschnig and thk123 as code owners February 12, 2018 18:48

smowton force-pushed the smowton/fix/java-inherited-static-fields branch 3 times, most recently from 5082af5 to d83a034 Compare February 13, 2018 10:48

mgudemann reviewed Feb 13, 2018

View reviewed changes

peterschrammel reviewed Feb 13, 2018

View reviewed changes

thk123 suggested changes Feb 13, 2018

View reviewed changes

smowton added 13 commits February 14, 2018 14:06

resolve_concrete_function_callt -> resolve_inherited_componentt

f3160e1

This actually doesn't have any logic specific to function calls, and can be used to resolve inherited fields too.

Generalise get_inherited_method

168c2a8

This can now resolve fields too, and is moved into java_utils so it can be used more widely.

Use a common instance of class_hierarchyt in get_inherited_component

5b3cde5

This avoids constructing a fresh class_hierarchyt with a consequent sweep of the complete symbol table every time inheritence is queried.

US spelling of initialize

afa443c

No functional changes.

Exclude j.l.O from possible static field hosts.

f15c312

smowton force-pushed the smowton/fix/java-inherited-static-fields branch 2 times, most recently from 6f7f07c to 80e1648 Compare February 14, 2018 14:09

mgudemann approved these changes Feb 14, 2018

View reviewed changes

thk123 approved these changes Feb 14, 2018

View reviewed changes

smowton force-pushed the smowton/fix/java-inherited-static-fields branch from 80e1648 to 1da5be1 Compare February 14, 2018 15:41

peterschrammel approved these changes Feb 14, 2018

View reviewed changes

smowton merged commit 278e4e6 into diffblue:develop Feb 14, 2018

		@@ -0,0 +1,10 @@
		public class Test extends Parent {

		public static void main(int nondet) {


		#include <util/expr_iterator.h>

		static bool contains_symbol_reference(const exprt &expr, const irep_idt &id)

Add support for inheritence of Java static fields. Fixes TG-2457 #1826

Add support for inheritence of Java static fields. Fixes TG-2457 #1826

Conversation

smowton commented Feb 12, 2018 • edited Loading

smowton commented Feb 12, 2018

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 • 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton commented Feb 14, 2018

smowton commented Feb 14, 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

smowton commented Feb 14, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

smowton commented Feb 14, 2018

smowton commented Feb 12, 2018 •

edited

Loading

thk123 left a comment •

edited

Loading