-
Notifications
You must be signed in to change notification settings - Fork 273
Move definition of can-be-constant-propagated to a central location #2221
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
Conversation
} | ||
else if(expr.id()==ID_with) | ||
{ | ||
// this is bad |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is probably not your code, but it would be good to give an idea of 'what didn't work here' in place of a commented piece of code.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed, let me try to dig this up.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(But it might take a while to do so.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Throughout the back-end there are hints that the array theory used to do Strange Things. At one point I (tried to) patch a rewrite that converted with to ITE.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#3095 for further discussion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A really good review strategy is to find simple refactorings or moving the code around and ask for complex semantic changes!
Happy with this as a refactor but think some of the questions are worth discussing.
{ | ||
if(expr.id()==ID_mult) | ||
{ | ||
// propagate stuff with sizeof in it |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this only the case for multiply?
(Again, I realise that this is not new code.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#3095 for further discussion.
} | ||
else if(expr.id()==ID_with) | ||
{ | ||
// this is bad |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Throughout the back-end there are hints that the array theory used to do Strange Things. At one point I (tried to) patch a rewrite that converted with to ITE.
return is_constant(expr.op0()); | ||
} | ||
else if( | ||
expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array || |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What about divide, floating-point ops, etc. Do we have any exprt's that cannot be constant folded if all arguments are constant? If we do; should we?
I realise that constant folding and expression forwarding in symex is more involved than just "is it constant" but...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#3095 for further discussion.
75a9a24
to
fd339a7
Compare
@kroening Would you be able to respond to some of the questions above? |
fd339a7
to
8d24d2f
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: 8d24d2f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86785268
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I suggest to turn the questions into issues instead of delaying this further.
This is re-usable, for example for the constant-propagation data-flow analysis.
8d24d2f
to
be11b36
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Passed Diffblue compatibility checks (cbmc commit: be11b36).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86839351
This is re-usable, for example for the constant-propagation data-flow analysis.
This is factored out from #2132.