Explicit nondet initialisation

[tautschnig]

Instead of leaving the right-hand side empty, explicitly assign non-deterministic values when creating objects. This enables constant propagation for non-POD types.

[tautschnig]

@martin-cs If you have any spare cycles to evaluate the performance impact of this pull request I'd be grateful. It should enable a lot more constant propagation for any code using structs or fixed-size arrays.

[peterschrammel]

@tautschnig, needs rebasing...

[tautschnig]

@peterschrammel Rebasing done.

[forejtv]

@tautschnig can you please rebase to see if all tests pass?

[tautschnig]

Rebased, all checks passing. There is another question about performance, however.

[forejtv]

@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance?

[kroening]

Would the performance concern be addressed by only doing this for compound/array types?

[tautschnig]

I don't necessarily think there is a performance problem - it just needs to be evaluated to make sure there is no such problem. The lack of evaluation infrastructure for doing this evaluation is a problem...

[tautschnig]

CI passes here, TG bump would be appreciated. I am meanwhile working on eliminating/clarifying init_l1 and then some performance evaluation.

[smowton]

https://github.com/diffblue/test-gen/pull/1811

[tautschnig]

I have now added two additional commits that clean up the code a fair bit, most notably is the init_l1 gone (and all the special-casing at the beginning of symex_assign_symbol). Could the TG run please be updated (if that's necessary)?

[smowton]

Updated.

[smowton]

Test-gen bump fails; it appears to break lots of tests, but they all have strings in common, so I suspect the string solver is being perturbed somehow. @romainbrenguier@allredj could either of you have a look here please?

[tautschnig]

If there's any info that can be shared (such as a failing assertion) then I'm happy to take a look. It is entirely possible that there are more places in the code that handle ID_symbol but don't yet handle ID_nondet_symbol.

Edit: I am meanwhile working on the performance analysis. There are some cases that show improvement, while others have considerable higher memory consumption, which I need to investigate.

[smowton]

Surprised the target doesn't get told of the declaration anymore?

[tautschnig]

That's a point worth considering, but really symex_targett::decl just bloats the formula. I might rather go one step further and remove it completely?!

[smowton]

This is surprising -- the convention elsewhere seems to be that a nil value implies nondet init (for example, Java globals)

[tautschnig]

Is that maybe only the case in Java? The one place that takes care of initialising globals is static_lifetime_init, which will zero-initialise all symbols that don't have a value (unless they are marked extern). Now of course the Java front-end had to do this in its very own way...

[romainbrenguier]

This commit ( cb6f737 ) seems to be breaking our string tests...

[romainbrenguier]

We can see the difference on this example:

public class test
{
public static int check(String s)
{
if(s.length()==2)
return 2;
if(s.length()==4)
return 4;
return s.length()+1;
}
}

running with options: jbmc test.class --refine-strings --function test.check --trace --string-max-length 100 --cover location --trace --json-ui
current develop as some assignment in the trace of the form

{
"assignmentType": "variable",
"hidden": false,
"internal": true,
"lhs": "dynamic_object2",
"mode": "java",
"stepType": "assignment",
"thread": 0,
"value": {
"elements": [
{
"index": 0,
"value": {
"binary": "0000000000111111",
"data": "(char)'?'",
"name": "integer",
"type": "char",
"width": 16
}
},
{
"index": 1,
"value": {
"binary": "0000000000111111",
"data": "(char)'?'",
"name": "integer",
"type": "char",
"width": 16
}
}
],
"name": "array"
}
}

but with this commit, this is just replaced by

{
"assignmentType": "variable",
"hidden": false,
"internal": true,
"lhs": "dynamic_object2",
"mode": "java",
"stepType": "assignment",
"thread": 0,
"value": {
"name": "unknown"
}
}

[tautschnig]

Thank you for bisecting! I'll take a look and will try to figure out what is going on.

[tautschnig]

Closing as field sensitivity already covers possible benefits of this change.