Conversation
4efea63 to
17c27c1
Compare
17c27c1 to
2b19b59
Compare
2b19b59 to
e3767ec
Compare
e3767ec to
d268552
Compare
d268552 to
a82ffaa
Compare
a82ffaa to
c00ea94
Compare
c00ea94 to
440d1e4
Compare
|
@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. |
|
@tautschnig, needs rebasing... |
440d1e4 to
f86fb0b
Compare
|
@peterschrammel Rebasing done. |
f86fb0b to
5d208a6
Compare
|
@tautschnig can you please rebase to see if all tests pass? |
5d208a6 to
3090a26
Compare
|
Rebased, all checks passing. There is another question about performance, however. |
|
@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance? |
|
Would the performance concern be addressed by only doing this for compound/array types? |
|
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... |
4242805 to
2262960
Compare
80f79a4 to
2775f9e
Compare
|
CI passes here, TG bump would be appreciated. I am meanwhile working on eliminating/clarifying |
2775f9e to
15c7af1
Compare
|
I have now added two additional commits that clean up the code a fair bit, most notably is the |
|
Updated. |
|
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? |
|
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 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. |
| state.top().hidden_function || | ||
| state.source.pc->source_location.get_hide(); | ||
|
|
||
| target.decl( |
There was a problem hiding this comment.
Surprised the target doesn't get told of the declaration anymore?
There was a problem hiding this comment.
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?!
| argc_symbol.type=op0.type(); | ||
| argc_symbol.is_static_lifetime=true; | ||
| argc_symbol.is_lvalue=true; | ||
| argc_symbol.value = side_effect_expr_nondett(op0.type()); |
There was a problem hiding this comment.
This is surprising -- the convention elsewhere seems to be that a nil value implies nondet init (for example, Java globals)
There was a problem hiding this comment.
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...
src/goto-symex/goto_symex_state.cpp
Outdated
| bool goto_symex_statet::constant_propagation(const exprt &expr) const | ||
| { | ||
| if(expr.is_constant()) | ||
| if(expr.is_constant() || expr.id() == ID_nondet_symbol) |
There was a problem hiding this comment.
This commit ( cb6f737 ) seems to be breaking our string tests...
There was a problem hiding this comment.
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"
}
}
There was a problem hiding this comment.
Thank you for bisecting! I'll take a look and will try to figure out what is going on.
Constant propagation now yields different right-hand sides in a test.
15c7af1 to
efc5608
Compare
|
Closing as field sensitivity already covers possible benefits of this change. |
Instead of leaving the right-hand side empty, explicitly assign non-deterministic values when creating objects. This enables constant propagation for non-POD types.