Use adjust_float_expression in simplify #2076
Conversation
hannes-steffenhagen-diffblue
requested review from
cesaro,
kroening,
mgudemann,
peterschrammel,
smowton and
tautschnig
as code owners
|
@martin-cs This has the floating point changes we were talking about last week. Can you please check if this is in line with what you were thinking? This doesn't have any goto-analyzer specific things in it (like trying to use different rounding modes), but I believe this is an independent step we can use as a starting point. |
This necessitates moving the code from symex to util.
hannes-steffenhagen-diffblue
force-pushed
the
floating_point_simplificiation
branch
from
8da4c69 to
651d41f
Compare
hannes-steffenhagen-diffblue
requested a review
from chrisr-diffblue
as a code owner
| } | ||
|
|
||
| void adjust_float_expressions( | ||
| goto_functionst::goto_functiont &goto_function, |
There was a problem hiding this comment.
This file will need to be split up, those functions can't live in util/ as they have dependencies on goto-programs.
| else if(expr.id()==ID_mod) | ||
| result=simplify_mod(expr) && result; | ||
| if(expr.type().id() == ID_floatbv) |
There was a problem hiding this comment.
Please add braces here.
| @@ -2284,11 +2303,35 @@ bool simplify_exprt::simplify_node(exprt &expr) | |||
| else if(expr.id()==ID_power) | |||
| result=simplify_power(expr) && result; | |||
| else if(expr.id()==ID_plus) | |||
| result=simplify_plus(expr) && result; | |||
| if(expr.type().id() == ID_floatbv) | |||
| else if(expr.id()==ID_minus) | ||
| result=simplify_minus(expr) && result; | ||
| if(expr.type().id() == ID_floatbv) |
| else if(expr.id()==ID_mult) | ||
| result=simplify_mult(expr) && result; | ||
| if(expr.type().id() == ID_floatbv) |
| if(expr.type().id() == ID_floatbv) | ||
| { | ||
| adjust_float_expressions(expr, ns); | ||
| result = simplify_rec(expr); |
There was a problem hiding this comment.
Missing && result (the same in all the other edits below)
| } | ||
| else | ||
| { | ||
| result = simplify_div(expr) && result; |
There was a problem hiding this comment.
Why not move the if(expr.type().id() == ID_floatbv) inside simplify_div etc?
| to_symbol_expr(attached_rounding_mode).get_identifier(), | ||
| p_rounding_sym)) | ||
| { | ||
| attached_rounding_mode = p_rounding_sym->value; |
There was a problem hiding this comment.
How is using the initial value justified? It may, after all, change during program execution?
There was a problem hiding this comment.
That was just me misunderstanding how namespacet is used, this indeed seems to be the wrong thing to do here.
I was thinking I could somehow do symbol evaluation in simplify_expr, but it seems that this will have to be done outside of it.
|
Closing for now as per @tautschnig comments this seems like the wrong approach to take. I'll try moving |
This lets the simplifier rewrite generic arithmetic operations to their floating point equivalents, which can simplify floating point expressions respecting rounding mode.