Merge pull request #6290 from jezhiggins/vsd-eval-within-our-lifetime

VSD - constant expression evaluation speedup

Author: martin-cs

regression/goto-analyzer-simplify/simplify-deeply-nested-expression/main.c

@@ -0,0 +1,42 @@
+int nondet_int(void);
+
+struct MH
+{
+  int s;
+  int t;
+  int to;
+  int su;
+};
+
+int main(void)
+{
+  int l = nondet_int();
+  int s = nondet_int();
+  int n = nondet_int();
+  int o = nondet_int();
+  int nt = nondet_int();
+  int ns = nondet_int();
+
+  struct MH mh;
+  mh.s = nondet_int();
+  mh.t = nondet_int();
+  mh.to = nondet_int();
+  mh.su = nondet_int();
+
+  int result =
+    ((l >= mh.s ? 1 : 0) &
+     (((mh.s >= s ? 1 : 0) &
+       (((n >= mh.t ? 1 : 0) &
+         (((mh.t >= o ? 1 : 0) & ((((int)mh.to == (int)nt ? 0 : 1) &
+                                   ((int)mh.su == (int)ns ? 0 : 1)) == 0
+                                    ? 0
+                                    : 1)) == 0
+            ? 0
+            : 1)) == 0
+          ? 0
+          : 1)) == 0
+        ? 0
+        : 1)) == 0;
+
+  assert(result = 0);
+}

regression/goto-analyzer-simplify/simplify-deeply-nested-expression/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--vsd
+^SIGNAL=0$
+^EXIT=0$
+--
+--
+This expression is derived from a real system under test. Due to inadvertent reevaluation of expression operands, all expression evaluations had geometric complexity (even more so in the presence of TOP values). This particular expression took nearly two hours to evaluate. Reworking to prevent repeated reevaluation brings this down to a few tenths.
+See https://github.com/diffblue/cbmc/pull/6290
+If this test appears to hang, the constant_evaluator is probably your first port of call.

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -225,9 +225,10 @@ class constants_evaluator
 public:
   constants_evaluator(
     const exprt &e,
+    const std::vector<abstract_object_pointert> &ops,
     const abstract_environmentt &env,
     const namespacet &n)
-    : expression(e), environment(env), ns(n)
+    : expression(e), operands(ops), environment(env), ns(n)
   {
   }
 
@@ -244,28 +245,26 @@ class constants_evaluator
 private:
   abstract_object_pointert transform() const
   {
-    exprt expr = adjust_expression_for_rounding_mode();
-    auto operands = expr.operands();
-    expr.operands().clear();
+    auto expr = adjust_expression_for_rounding_mode();
 
-    // Two passes over the expression - one for simplification,
-    // another to check if there are any top subexpressions left
-    for(const exprt &op : operands)
+    auto operand_is_top = false;
+    for(size_t i = 0; i != operands.size(); ++i)
     {
-      auto lhs_value = eval_constant(op);
+      auto lhs_value = operands[i]->to_constant();
 
       // do not give up if a sub-expression is not a constant,
       // because the whole expression may still be simplified in some cases
-      expr.operands().push_back(lhs_value.is_nil() ? op : lhs_value);
+      // (eg multiplication by zero)
+      if(lhs_value.is_not_nil())
+        expr.operands()[i] = lhs_value;
+      else
+        operand_is_top = true;
     }
 
-    exprt simplified = simplify_expr(expr, ns);
-    for(const exprt &op : simplified.operands())
-    {
-      auto lhs_value = eval_constant(op);
-      if(lhs_value.is_nil())
-        return top(simplified.type());
-    }
+    auto simplified = simplify_expr(expr, ns);
+
+    if(simplified.has_operands() && operand_is_top)
+      return top(simplified.type());
 
     // the expression is fully simplified
     return std::make_shared<constant_abstract_valuet>(
@@ -274,22 +273,31 @@ class constants_evaluator
 
   abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
   {
-    std::vector<abstract_object_pointert> possible_results;
+    abstract_object_pointert last_result;
+
+    auto results_differ = [](
+                            const abstract_object_pointert &prev,
+                            const abstract_object_pointert &cur) {
+      if(prev == nullptr)
+        return false;
+      return prev->to_constant() != cur->to_constant();
+    };
+
     for(auto rounding_mode : all_rounding_modes)
     {
       auto child_env(environment_with_rounding_mode(rounding_mode));
-      possible_results.push_back(
-        constants_evaluator(expression, child_env, ns)());
-    }
+      auto child_operands =
+        reeval_operands(expression.operands(), child_env, ns);
 
-    auto first = possible_results.front()->to_constant();
-    for(auto const &possible_result : possible_results)
-    {
-      auto current = possible_result->to_constant();
-      if(current.is_nil() || current != first)
+      auto result =
+        constants_evaluator(expression, child_operands, child_env, ns)();
+
+      if(result->is_top() || results_differ(last_result, result))
         return top(expression.type());
+      last_result = result;
     }
-    return possible_results.front();
+
+    return last_result;
   }
 
   abstract_environmentt
@@ -311,12 +319,25 @@ class constants_evaluator
   {
     exprt adjusted_expr = expression;
     adjust_float_expressions(adjusted_expr, ns);
+
+    if(adjusted_expr != expression)
+      operands = reeval_operands(adjusted_expr.operands(), environment, ns);
+
     return adjusted_expr;
   }
 
-  exprt eval_constant(const exprt &op) const
+  static std::vector<abstract_object_pointert> reeval_operands(
+    const exprt::operandst &ops,
+    const abstract_environmentt &env,
+    const namespacet &ns)
   {
-    return environment.eval(op, ns)->to_constant();
+    auto reevaled_operands = std::vector<abstract_object_pointert>{};
+    std::transform(
+      ops.cbegin(),
+      ops.end(),
+      std::back_inserter(reevaled_operands),
+      [&env, &ns](const exprt &op) { return env.eval(op, ns); });
+    return reevaled_operands;
   }
 
   abstract_object_pointert top(const typet &type) const
@@ -326,11 +347,13 @@ class constants_evaluator
 
   bool rounding_mode_is_not_set() const
   {
-    auto rounding_mode = eval_constant(rounding_mode_symbol);
+    auto rounding_mode =
+      environment.eval(rounding_mode_symbol, ns)->to_constant();
     return rounding_mode.is_nil();
   }
 
   const exprt &expression;
+  mutable std::vector<abstract_object_pointert> operands;
   const abstract_environmentt &environment;
   const namespacet &ns;
 
@@ -355,7 +378,7 @@ abstract_object_pointert constants_expression_transform(
   const abstract_environmentt &environment,
   const namespacet &ns)
 {
-  auto evaluator = constants_evaluator(expr, environment, ns);
+  auto evaluator = constants_evaluator(expr, operands, environment, ns);
   return evaluator();
 }