@@ -225,9 +225,10 @@ class constants_evaluator
225225public:
226226 constants_evaluator (
227227 const exprt &e,
228+ const std::vector<abstract_object_pointert> &ops,
228229 const abstract_environmentt &env,
229230 const namespacet &n)
230- : expression(e), environment(env), ns(n)
231+ : expression(e), operands(ops), environment(env), ns(n)
231232 {
232233 }
233234
@@ -244,31 +245,28 @@ class constants_evaluator
244245private:
245246 abstract_object_pointert transform () const
246247 {
247- exprt expr = adjust_expression_for_rounding_mode ();
248- auto operands = expr.operands ();
249- expr.operands ().clear ();
248+ auto expr = adjust_expression_for_rounding_mode ();
250249
251- // Two passes over the expression - one for simplification,
252- // another to check if there are any top subexpressions left
253- for (const exprt &op : operands)
250+ auto operand_is_top = false ;
251+ for (size_t i = 0 ; i != operands.size (); ++i)
254252 {
255- auto lhs_value = eval_constant (op );
253+ auto lhs_value = operands[i]-> to_constant ( );
256254
257255 // do not give up if a sub-expression is not a constant,
258- if (lhs_value.is_nil ())
259- {
260- exprt simplified_op = simplify_expr (op, ns);
261- if (simplified_op.is_not_nil ())
262- lhs_value = eval_constant (simplified_op);
263- if (lhs_value.is_nil ())
264- return top (expr.type ());
265- }
266-
267- expr.operands ().push_back (lhs_value);
256+ // because the whole expression may still be simplified in some cases
257+ // (eg multiplication by zero)
258+ if (lhs_value.is_not_nil ())
259+ expr.operands ()[i] = lhs_value;
260+ else
261+ operand_is_top = true ;
268262 }
269263
264+ auto simplified = simplify_expr (expr, ns);
265+
266+ if (simplified.has_operands () && operand_is_top)
267+ return top (simplified.type ());
268+
270269 // the expression is fully simplified
271- exprt simplified = simplify_expr (expr, ns);
272270 return std::make_shared<constant_abstract_valuet>(
273271 simplified, environment, ns);
274272 }
@@ -279,8 +277,11 @@ class constants_evaluator
279277 for (auto rounding_mode : all_rounding_modes)
280278 {
281279 auto child_env (environment_with_rounding_mode (rounding_mode));
280+ auto child_operands =
281+ reeval_operands (expression.operands (), child_env, ns);
282+
282283 possible_results.push_back (
283- constants_evaluator (expression, child_env, ns)());
284+ constants_evaluator (expression, child_operands, child_env, ns)());
284285 }
285286
286287 auto first = possible_results.front ()->to_constant ();
@@ -312,12 +313,25 @@ class constants_evaluator
312313 {
313314 exprt adjusted_expr = expression;
314315 adjust_float_expressions (adjusted_expr, ns);
316+
317+ if (adjusted_expr != expression)
318+ operands = reeval_operands (adjusted_expr.operands (), environment, ns);
319+
315320 return adjusted_expr;
316321 }
317322
318- exprt eval_constant (const exprt &op) const
323+ static std::vector<abstract_object_pointert> reeval_operands (
324+ const exprt::operandst &ops,
325+ const abstract_environmentt &env,
326+ const namespacet &ns)
319327 {
320- return environment.eval (op, ns)->to_constant ();
328+ auto reevaled_operands = std::vector<abstract_object_pointert>{};
329+ std::transform (
330+ ops.cbegin (),
331+ ops.end (),
332+ std::back_inserter (reevaled_operands),
333+ [&env, &ns](const exprt &op) { return env.eval (op, ns); });
334+ return reevaled_operands;
321335 }
322336
323337 abstract_object_pointert top (const typet &type) const
@@ -327,11 +341,13 @@ class constants_evaluator
327341
328342 bool rounding_mode_is_not_set () const
329343 {
330- auto rounding_mode = eval_constant (rounding_mode_symbol);
344+ auto rounding_mode =
345+ environment.eval (rounding_mode_symbol, ns)->to_constant ();
331346 return rounding_mode.is_nil ();
332347 }
333348
334349 const exprt &expression;
350+ mutable std::vector<abstract_object_pointert> operands;
335351 const abstract_environmentt &environment;
336352 const namespacet &ns;
337353
@@ -356,7 +372,7 @@ abstract_object_pointert constants_expression_transform(
356372 const abstract_environmentt &environment,
357373 const namespacet &ns)
358374{
359- auto evaluator = constants_evaluator (expr, environment, ns);
375+ auto evaluator = constants_evaluator (expr, operands, environment, ns);
360376 return evaluator ();
361377}
362378
0 commit comments