Skip to content

TG-1877: Include array pointer types in needed classes #1660

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

Conversation

smowton
Copy link
Contributor

@smowton smowton commented Dec 7, 2017

Lazy methods attempts a pointer graph walk starting from the main function's
parameters to determine what classes may exist before the main function is
entered; for example, starting at f(A a) implies that an A instance may exist,
and if A itself has a B field that too might exist, and so on. However, until
now this failed to account for array-typed parameters and fields. This commit
amends gather_field_types to account for this special case.

Corresponding PR: https://github.com/diffblue/test-gen/pull/1289

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think the test is a good one since test.g being the entry point, doesn't this already imply test needs to be loaded?

Extra tests:

  • class that contains an array

@@ -477,17 +477,28 @@ void ci_lazy_methodst::gather_field_types(
ci_lazy_methods_neededt &needed_lazy_methods)
{
const auto &underlying_type=to_struct_type(ns.follow(class_type));
for(const auto &field : underlying_type.components())
const typet &element_type=
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Prefer java_types.h java_array_element_type (with probably a check that is is an array).

else if(field.type().id()==ID_pointer)
{
// Skip array primitive pointers, for example:
if(field.type().subtype().id()!=ID_symbol)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I realise this isn't from this PR - but is there a better way to skip array primitive pointers as this feels like a fairly loose check.

@smowton
Copy link
Contributor Author

smowton commented Dec 8, 2017

No, the entry point actually does not imply test being available, as it's a static method (thus no instance of class test is implied)

@thk123
Copy link
Contributor

thk123 commented Dec 8, 2017

@smowton OK - in which case, I think the addition of the test where the array is loaded transitively and this should be OK (though I think using java_array_element_type would be good).

@antlechner
Copy link
Contributor

I tested it on some examples and it does not work with generic arrays.
Comparing

public class IntegerArray {

    Integer[] array;

    public static boolean testLess(IntegerArray intArr) {
        int first = intArr.array[0];
        int second = intArr.array[1];
        if (first < second)
            return true;
        else
            return false;
    }

}

and

public class GenericArray<E> {

    E[] array;

    public static boolean testLess(GenericArray<Integer> intArr) {
        int first = intArr.array[0];
        int second = intArr.array[1];
        if (first < second)
            return true;
        else
            return false;
    }

}

IntegerArray.testLess generates a correct test (it previously didn't) while GenericArray.testLess still puts zeros everywhere.

@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch 2 times, most recently from ee3b84c to 1b6c07a Compare December 9, 2017 17:16
@smowton
Copy link
Contributor Author

smowton commented Dec 9, 2017

@thk123 changes applied.
@antlechner The generic array case indeed doesn't work yet. At the moment I'm not confident I understand how generics have been done well enough to fix it, but a generics team person should be able to improve on this in short order. Will describe the situation in better detail in a moment.

@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch from 1b6c07a to df9a34a Compare December 9, 2017 17:19
@smowton
Copy link
Contributor Author

smowton commented Dec 9, 2017

@thk123 here are the problems I ran into briefly to address the generic-array case raised by @antlechner:

  1. The generic specialisation is attached to the pointer, like:
pointer
  * width: 64
  * #reference: 1
  * #java_generic_type: 1
  * #type_variables: 
    0: pointer
        * width: 64
        * #reference: 1
        0: symbol
            * identifier: java::test
            * #base_name: test
  0: symbol
      * identifier: java::container
      * #base_name: container

Would it be better to annotate the symbol, as is done for arrays, since it's the object at the end of the pointer that is specialised, not the pointer itself? As it stands functions like this that walk over the type graph have to retrieve generic information at the pointer stage and pass it into the function that handles structs.

  1. This specifies that some type variable has been instantiated with test, but what variable has been instantiated is implied by context. Can I always assume that *ptr is the specialised thing (as in, is the pattern always pointer(#type_variables -> [ actual list ], subtype -> symbol (specialised_classname))? Would it be more robust to specialise a name = variable pair, like (pseudocode) lhs: java::container::T, rhs: pointer(java::test)?

  2. The actual type I need to specialise is given:

pointer
  * width: 64
  * #reference: 1
  * #java_generic_parameter: 1
  * #type_variables: 
    0: symbol
        * identifier: java::container::T
  0: symbol
      * identifier: java::java.lang.Object
      * #base_name: java.lang.Object

This is the member type of an array T[]. type_variables, plural, suggests that T has been used somehow, but doesn't seem to specify that it replaces Object? What are the rules for using the implied environment to generate a specialised type here? Is there a function that will take my knowledge implied by context that T == test and give me a concrete type back? Longer term, how about we show T in situe, like #generic_type: pointer: symbol: T, such that substituting T for its actual value is sufficient?

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the extra tests. @mgudemann might have something to say on the generics being attached to a pointer -let's discuss tomorrow when I'm in the office. The only reason I can see to prefer on the pointer is technically it is associated with the pointer since I can do:

gen g = new gen();
gen<Integer> gi = g;
gen<Float> gf = g;

But I don't know if that is relevant.

@@ -0,0 +1,7 @@
KNOWNBUG
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you create and link to to a jira ticket to avoid this test getting lost and then duplicated.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could either link to https://diffblue.atlassian.net/browse/TG-1877 and mention in the ticket that the generics case doesn't work yet, or move TG-1877 to "Ready for QA" and create a new ticket for the generics case.

Copy link
Contributor

@antlechner antlechner left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the delay. I've tested these changes with the example in TG-1877 and all examples in TG-1712. All of them work except for the arrays of Floats and Doubles, but that seems to be an unrelated problem. So for non-generic arrays, this PR looks good!


if(args == null || args.length != 1 || args[0] == null)
return;
asserthere.doassert(args[0].f() == 1);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the reason behind using a separate class here rather than just calling assert(args[0].f() == 1); directly?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Turns out lazy loading always marks classes that make assertions as needed! I'm not sure why, I certainly didn't write that code, but I didn't want to meddle with it for now...

@@ -0,0 +1,7 @@
KNOWNBUG
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could either link to https://diffblue.atlassian.net/browse/TG-1877 and mention in the ticket that the generics case doesn't work yet, or move TG-1877 to "Ready for QA" and create a new ticket for the generics case.

@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch from df9a34a to 4001a1b Compare December 14, 2017 15:45
@smowton
Copy link
Contributor Author

smowton commented Dec 14, 2017

@antlechner added comments in both cases. Will merge this once CI passes.

@antlechner
Copy link
Contributor

@smowton I just talked to @thk123 and he asked for a new ticket to be created for the generics case, as that would make it clearer. So I'll make a new ticket in a bit. Sorry for the confusion. If you don't want to update the comment again, we could always link TG-1877 and the new ticket...

@mgudemann
Copy link
Contributor

@thk123 yes, the idea was to implement this as closely as possible as it is in the JVM bytecode
@smowton yes, one could have used the symbol also for annotation of the generic type, but the original goal was to keep it as close as possible to the JVM internals

@smowton for 3 the java_generic_parameter states that is a generic type variable that has not been instantiated with a real type. The Object entry is because any type variable is bound by an object type, with Object being the most permissive, of couse. (I am also not sure whether we actually do support tighter bounds or still have everything as Object @svorenova ?)

@majakusber
Copy link

Yes, as far as I know, all bounds are set to Object currently, the task to parse bounds is TG-1286.

@smowton
Copy link
Contributor Author

smowton commented Dec 14, 2017

@mgudemann @svorenova it looks like the information is actually already there? Look at the #type_variables with child test, isn't that indicating the concrete type container<test>?

@mgudemann
Copy link
Contributor

@smowton was referring to point 3) where this is not the case. In 1) yes, it is the instantiation of the pointed to type, there is no java_generic_parameter, but a reference type which represented the concrete object type. So in 1) you have a container<test> . In 3) this is the type variable only which is replaced by a reference type when doing the specialisation.

Please correct me if I am wrong @svorenova

@antlechner
Copy link
Contributor

Created a new ticket for the generics case, in case a new PR is needed for that:
https://diffblue.atlassian.net/browse/TG-1938

@majakusber
Copy link

@mgudemann Yes, you are correct. I just talked to @smowton and hopefully have pointed him towards the right direction. The problem is, if I understood correctly from the discussion, how to quickly find, given a generic type with concrete types, the corresponding specialized java generic class. There is a function called build_generic_name that does almost exactly what is needed.

@smowton
Copy link
Contributor Author

smowton commented Dec 15, 2017

@thk123 @antlechner @mgudemann @svorenova this has been updated to support generic type arguments, with a few extra tests too. One fails due to inadequate generic support, but lazy loading appears to do the right thing at least.

@thk123
Copy link
Contributor

thk123 commented Dec 20, 2017

I've created a diffblue/test-gen#1317 to check this works, assuming it does I will merge unless anyone has any objections

Copy link
Contributor

@thk123 thk123 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unfortunately this creates quite a few failures in the TG repo - so until someone has a had a chance to investigate and fix these can I request this doesn't go in.

@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch from ed5cea9 to 794e8c3 Compare December 20, 2017 18:06
@smowton
Copy link
Contributor Author

smowton commented Dec 20, 2017

I've updated this to work around the vast majority of failures -- the problem was that the string library version of String contains a uint16_t*, which is usually impossible in Java. However it has exposed a generics bug in the unit tests, and broken a few string tests for reasons I don't understand yet. Nontheless the failure count in test-gen is down from hundreds to ~5.

@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch from 794e8c3 to 0f8ae92 Compare December 29, 2017 14:50
@smowton
Copy link
Contributor Author

smowton commented Dec 29, 2017

@thk123 fixed the remaining problem, which was an incidentally perturbed string test (see commit message at https://github.com/diffblue/test-gen/pull/1317 for more detail). Now waiting for test-gen CI (and a re-check here).

@smowton
Copy link
Contributor Author

smowton commented Dec 29, 2017

Passes, ready to merge I think

@thk123
Copy link
Contributor

thk123 commented Jan 4, 2018

It'd be good if you could rebase the test-gen PR before merging, but looks fine.

@smowton
Copy link
Contributor Author

smowton commented Jan 5, 2018

@thk123 I'll rebase both once https://github.com/diffblue/test-gen/pull/1063 lands, thus bringing latest cbmc and latest test-gen back into line.

@smowton
Copy link
Contributor Author

smowton commented Jan 5, 2018

This is currently blocked because #1419 was merged, but doesn't currently work with test-gen. @peterschrammel is currently debugging that, after which we'll be able to advance the tg pointer and get this in.

Lazy methods attempts a pointer graph walk starting from the main function's
parameters to determine what classes may exist before the main function is
entered; for example, starting at f(A a) implies that an A instance may exist,
and if A itself has a B field that too might exist, and so on. However, until
now this failed to account for array-typed parameters and fields. This commit
amends gather_field_types to account for this special case.

This also adds a test for the generic parameter case, which is not solved yet.
This extends the previous commit to assume that generic parameter types are needed, which
overapproximates what is requried, but seems likely to suffice in most cases.
@smowton smowton force-pushed the smowton/fix/lazy_methods_array_parameters branch from 0f8ae92 to ae89c94 Compare January 8, 2018 12:07
@smowton
Copy link
Contributor Author

smowton commented Jan 8, 2018

Rebased, and rebased @thk123's bump PR; will merge if CI passes both.

@smowton smowton merged commit 1c227b7 into diffblue:develop Jan 8, 2018
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
d190fd8 Merge remote-tracking branch 'upstream/develop' into pull-support-20180112
5bd5962 Merge pull request diffblue#1667 from romainbrenguier/feature/type_cast
8ecb55a Merge pull request diffblue#1717 from smowton/smowton/feature/remove_virtual_functions_per_function
0d7310a Merge pull request diffblue#1691 from romainbrenguier/bugfix/getClass#TG-1245
2064849 Use type_checked_cast in boolbv_width
c5fc351 Validate data in pointer_typet in to_pointer_typet
35905c6 Add can_cast_type, validate_type for pointer_typet
b72bacf Define type_try_dynamic_cast and type_checked_cast
23c3561 Unit test for string symbol resolution
c13e602 Adding only needed equations in symbol resolution
ae4deff Debug information for string equations
912828d JBMC: Run remove-virtual-functions as each function is converted
a711c64 Introduce mechanism for renumbering an individual GOTO program
e308a32 Merge pull request diffblue#1679 from NlightNFotis/nondet_extra_test
e6ceb91 Merge pull request diffblue#1724 from tautschnig/fix-visitor
ea74bed Add extra test for nondet-static flag and arrays
4f74896 Use irept API, not implementation-level API
c55b4a5 Merge pull request diffblue#1682 from martin-cs/fix/dependence-graph-namespace-lifespan
1a2c14b Merge pull request diffblue#1722 from diffblue/unsafe_type_constructors
957a568 Merge pull request diffblue#1677 from NlightNFotis/pb4_develop
9c5add4 remove deprecated constructors for three bitvector types
c96e02a no longer use deprecated constructors for some bitvector types
954060e Add unit test for has_subtype
3dd3877 Refactor has_char_pointer_subtype with has_subtype
4699c13 Extend symbol resolution to string_typet
74144fc Handle if_exprt in add_axioms_for_string_literal
c6c1b3f Add an optional guard to add_axioms_for_constant
933d635 Merge pull request diffblue#1716 from mgudemann/fix/null_check_for_java_instanceof
1659314 Merge pull request diffblue#1715 from smowton/smowton/cleanup/jbmc_unused_passes
9c457b7 Add regression test for null instanceof.
2080cd3 Complete instanceof for Java.
d4300d0 Merge pull request diffblue#1697 from diffblue/nondet_symbol_exprt
1c68dd4 Merge pull request diffblue#1714 from tautschnig/c-library-strcat
44b5bae Merge pull request diffblue#1698 from thomasspriggs/tg1633
c4304ba JBMC: Remove C-only passes
bb8cfaa C library: Check upper bounds in memset, memcpy, memmove
7d4984f C library: Implement strcat, strncat
2a5cea2 This introduces nondet_symbol_exprt, which is generated by symbolic execution in response to side_effect_expr_nondett
85193a0 Merge pull request diffblue#1694 from NathanJPhillips/feature/add-raw-lhs-to-trace
d9122dc Merge pull request diffblue#1710 from NathanJPhillips/feature/remove_instanceof_per_function
092df69 Switch from custom file / path routines to Boost-filesystem
c8821b2 Allow to remove instanceof when remove exceptions
94b7658 Don't pass iterators into function calls
a9c4e4f Added regression tests
76318ce Protect extended trace behind a command line option
69b0ff1 Added base_name in comments for all symbols
e86080a Add raw LHS irep field to trace output
ddd1b7a Add remove_instanceof overload to remove from a particular instruction
1c227b7 Merge pull request diffblue#1660 from smowton/smowton/fix/lazy_methods_array_parameters
ae89c94 Lazy loading: assume concrete generic parameter types are needed
80eb6a6 TG-1877: Include array pointer types in needed classes
1053e5f Fix for [TG-1633] Inner generic types have incorrect type identifier
e2cda1a Merge pull request diffblue#1704 from tautschnig/fix-copy-paste
ef4a65e Fix op1/op0 copy&paste typo
21ea31f Merge pull request diffblue#1702 from peterschrammel/goto-diff-java
c4bc953 Merge pull request diffblue#1701 from peterschrammel/allow-instrument-jdk
2811363 Java regression test for goto-diff
43d2e09 Also reset fresh temporary symbol counter
9ef28f4 Compare relative goto target offsets
eaf3a7d Get source location from symbol table
ab59659 Allow instrumentation of java.* and org.cprover.*
6fbd59c Merge pull request diffblue#1631 from tautschnig/fix-pointer-minus
7c04b5c Merge pull request diffblue#1699 from NathanJPhillips/feature/reset-main-in-tests
5e0f186 Pointer difference over void* is difference over char*
faf8f00 Merge commit 'a83b52cddbed22304372c276512c63701eb3aedb' into pull-support-20180104
8236db4 Merge pull request diffblue#1419 from peterschrammel/refactor/cover-instrument
a580e27 Merge pull request diffblue#1689 from smowton/smowton/feature/get_this
591511a Allow callers of load_java_class to pass the name of the main function
1b86b27 Merge pull request diffblue#1687 from smowton/smowton/feature/class-hierarchy-dot
fd2bf6a Merge pull request diffblue#1688 from smowton/smowton/feature/parameter_indices
f570ce5 Merge pull request diffblue#1696 from smowton/smowton/fix/identical_struct_equality
61b0d6d Merge pull request diffblue#1666 from mgudemann/bugfix/removed_required_virtual_calls
3365054 Add regression test
2b6dc8b Resolve concrete function call if no implementation is found
3f1fd64 Add code_typet::get_parameter_indices
42cf61a Fix testing for empty line in test desc file
2090000 Fix missing newline at end of desc file
e448d5f Fix unsatisfiable test line
f7f033d String smoke tests: ensure no type mismatches are seen
b627c3d Replace unsound struct-cast simplification
8fa42b3 Class hierarchy: add DOT output, unit tests
04f2faf Mark GOTO instructions with unresolved virtual calls
aac181f Pass command line options via optionst
b6fa3e8 Factorize source location initialization
8da5395 Document cover functions
a7f0c3d Introduce cover instrumenter
873627a Split cover into several files
0fc08f3 Replace cover-function-only by cover-include-pattern
1f2102c Add code_typet::get_this
2801f0f Avoid crashing when --dependence-graph is used by correcting namespace scoping.
acac776 Add a test for the same-named static functions crashing dependence graph in the goto-analyser
05f46a9 Fix the problem where two static functions with the same name would cause the dependency graph to fail.

git-subtree-dir: cbmc
git-subtree-split: d190fd8
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants