[TG-3173] Assign Strings at malloc site in java object factory

[romainbrenguier]

This appears to be much more efficient than assigning to the object in the case the
object is an element of an array.

[tautschnig]

My apologies for being (too) late to the party, but I take issue with this PR. Here's why:

1. The commit message says "much more efficient" - that's weasel words, how much more? The second commit says "15 times", but what are the absolute numbers? Going from 0.15ms to 0.1ms is measurement inaccuracy, going from 15h to 1h is a clearly noticeable difference.
2. The regression test is not immediately useful as such: this seems to have worked before, so maybe we could regress back into a worse state without noticing? A regression test must actually check for something. From the commit messages I'd guess that one would notice a regression because running the regression test suite would take much longer? How much longer? I use many different systems, some of which are pretty slow, would I notice that regression or would I just blame it on my computer being slow?
3. I have tried to figure out what the difference in the generated programs is. I may be doing this very wrong due to my poor knowledge of the Java frontend, but here's what I got by running jbmc --show-goto-functions --refine-strings --function Test.check --string-max-input-length 1000 Test.class (please tell me if that isn't telling the full story):

--- before.txt	2018-04-11 10:06:23.289256817 +0000
+++ after.txt	2018-04-11 10:26:05.663043314 +0000
@@ -985,7 +985,7 @@
         // 438 file Test.java line 5 function java::Test.check:([Ljava/lang/String;)Ljava/lang/String;
         return_array$34 = cprover_associate_length_to_array_func(*string_data_pointer$31, tmp_object_factory$30);
         // 439 no location
-        *array_data_init$27[array_init_iter$28] = { [email protected]={ .@class_identifier="java::java.lang.String",
+        *malloc_site$29 = { [email protected]={ .@class_identifier="java::java.lang.String",
     .@lock=false },
     .length=tmp_object_factory$30, .data=*string_data_pointer$31 };
         // 440 no location

Ok, so that seems to fit the code changes and the commit messages: rather than relying on the alias analysis (array_data_init$27[array_init_iter$28] is earlier set to malloc_site$29), which may over-approximate and thus generate assignments to some invalid_object array, just one level of indirection is used. It seems reasonable that this would improve performance. Is that a correct analysis of why this improves performance?
4. Looking at the resulting goto program, array_data_init$27 only ever appears on the left-hand side, and none of these involve dereferencing. Thus (but again I may not have used jbmc correctly) it just seems to be adding overhead and should be removed completely? But then also malloc_site$29 never appears on the right-hand side, so it seems to be equally useless? Is that just because it's such a limited regression test?

[romainbrenguier]

@tautschnig

1. The commit message says "much more efficient" - that's weasel words, how much more? The second commit says "15 times", but what are the absolute numbers? Going from 0.15ms to 0.1ms is measurement inaccuracy, going from 15h to 1h is a clearly noticeable difference.

On my computer this was 7s against 0.4s.

2. The regression test is not immediately useful as such: this seems to have worked before, so maybe we could regress back into a worse state without noticing? A regression test must actually check for something. From the commit messages I'd guess that one would notice a regression because running the regression test suite would take much longer? How much longer? I use many different systems, some of which are pretty slow, would I notice that regression or would I just blame it on my computer being slow?

Yes, I know this is not ideal, but couldn't find a good solution for checking that performances do not degrade. The test at least checks that we haven't broken things. Do you have suggestions for a better check?

Ok, so that seems to fit the code changes and the commit messages: rather than relying on the alias analysis (array_data_init$27[array_init_iter$28] is earlier set to malloc_site$29), which may over-approximate and thus generate assignments to some invalid_object array, just one level of indirection is used. It seems reasonable that this would improve performance. Is that a correct analysis of why this improves performance?

Yes that's a possible explanation. What I observed is that with the 'before' version some unecessary equations where generated:

 {-96} dynamic_object9#1 == (dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object9 ? { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 } : dynamic_object9#0)
{-97} dynamic_object7#2 == (dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object7 && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object9) ? { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 } : dynamic_object7#1)
{-98} dynamic_object5#3 == (dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object5 && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object7) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object9) ? { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 } : dynamic_object5#2)
{-99} dynamic_object3#4 == (dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object3 && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object5) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object7) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object9) ? { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 } : dynamic_object3#3)
{-100} invalid_object3#1 == (!(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object3) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object5) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object7) && !(dynamic_2_array#11[(24l + POINTER_OFFSET(array_data_init$27!0#2)) / 8l] == &dynamic_object9) ? { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 } : invalid_object3#0)

instead of just

dynamic_object9#1 == { [email protected]={ .@class_identifier="java::java.lang.String", .@lock=FALSE }, .length=tmp_object_factory$30!0#11,
    .data=dynamic_object10 }

which makes the rest of the analysis more complicated

4. Looking at the resulting goto program, array_data_init$27 only ever appears on the left-hand side, and none of these involve dereferencing. Thus (but again I may not have used jbmc correctly) it just seems to be adding overhead and should be removed completely? But then also malloc_site$29 never appears on the right-hand side, so it seems to be equally useless? Is that just because it's such a limited regression test?

The first assignment of array_data_init$27 is array_data_init$27 = (struct java.lang.String **)arg0a->data; so the modifications we do afterwards affect arg0a which is the input of our function.

[tautschnig]

Thanks a lot for all the input!

Yes, I know this is not ideal, but couldn't find a good solution for checking that performances do not degrade. The test at least checks that we haven't broken things. Do you have suggestions for a better check?

How about you add another x.desc file that includes --show-goto-functions and then checks for the absence of \*array_data_init\$ (that is, no dereferencing on array_data_init? Alternatively you could do --show-vcc and check for absence of the lines you raised, but I think that's harder to do without ambiguity.

The first assignment of [...]

My apologies for missing that, makes of course sense and does the dereferencing (via indexed access) that I wrongly claimed was not happening.