Pull more functions out of abstract_environmentt::do_assume

Trim do_assume right down.

assume_* function take expr by const ref now. Mark all assume_* as
static.

Author: jezhiggins

scripts/expected_doxygen_warnings.txt

@@ -26,7 +26,7 @@ warning: Included by graph for 'c_types.h' not generated, too many nodes (144),
 warning: Included by graph for 'config.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'expr_util.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'expr_util.h' not generated, too many nodes (63), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (186), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (118), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -26,17 +26,28 @@
 #endif
 
 typedef exprt (
-  *assume_function)(abstract_environmentt &, exprt, const namespacet &);
-
-exprt assume_eq(abstract_environmentt &env, exprt expr, const namespacet &ns);
-exprt assume_noteq(
+  *assume_function)(abstract_environmentt &, const exprt &, const namespacet &);
+
+static exprt
+assume_not(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
+static exprt
+assume_or(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
+static exprt
+assume_and(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
+static exprt
+assume_eq(abstract_environmentt &env, const exprt &expr, const namespacet &ns);
+static exprt assume_noteq(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns);
+static exprt assume_less_than(
   abstract_environmentt &env,
-  exprt expr,
+  const exprt &expr,
+  const namespacet &ns);
+static exprt assume_greater_than(
+  abstract_environmentt &env,
+  const exprt &expr,
   const namespacet &ns);
-exprt assume_le(abstract_environmentt &env, exprt expr, const namespacet &ns);
-exprt assume_lt(abstract_environmentt &env, exprt expr, const namespacet &ns);
-exprt assume_ge(abstract_environmentt &env, exprt expr, const namespacet &ns);
-exprt assume_gt(abstract_environmentt &env, exprt expr, const namespacet &ns);
 
 abstract_value_pointert as_value(const abstract_object_pointert &obj);
 bool is_value(const abstract_object_pointert &obj);
@@ -258,51 +269,20 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
 }
 
 static auto assume_functions =
-  std::map<dstringt, assume_function>{{ID_equal, assume_eq},
+  std::map<dstringt, assume_function>{{ID_not, assume_not},
+                                      {ID_and, assume_and},
+                                      {ID_or, assume_or},
+                                      {ID_equal, assume_eq},
                                       {ID_notequal, assume_noteq},
-                                      {ID_le, assume_le},
-                                      {ID_lt, assume_lt},
-                                      {ID_ge, assume_ge},
-                                      {ID_gt, assume_gt}};
+                                      {ID_le, assume_less_than},
+                                      {ID_lt, assume_less_than},
+                                      {ID_ge, assume_greater_than},
+                                      {ID_gt, assume_greater_than}};
 
-exprt abstract_environmentt::do_assume(exprt expr, const namespacet &ns)
+exprt abstract_environmentt::do_assume(const exprt &expr, const namespacet &ns)
 {
   auto expr_id = expr.id();
 
-  if(expr_id == ID_not)
-  {
-    auto not_expr = to_not_expr(expr);
-    auto result = do_assume(not_expr.op(), ns);
-    if(result.is_boolean())
-      result = result.is_true() ? exprt(false_exprt()) : true_exprt();
-    return result;
-  }
-  if(expr_id == ID_and)
-  {
-    auto and_expr = to_and_expr(expr);
-    for(auto const &operand : and_expr.operands())
-    {
-      auto result = do_assume(operand, ns);
-      if(result.is_nil() || result.is_false())
-        return result;
-    }
-    return true_exprt();
-  }
-  if(expr_id == ID_or)
-  {
-    exprt or_result = false_exprt();
-    auto or_expr = to_or_expr(expr);
-    for(auto const &operand : or_expr.operands())
-    {
-      auto result = do_assume(operand, ns);
-      if(result.is_nil())
-        return result;
-      if(result.is_true())
-        or_result = true_exprt();
-    }
-    return or_result;
-  }
-
   auto fn = assume_functions[expr_id];
 
   if(fn)
@@ -557,9 +537,57 @@ bool is_value(const abstract_object_pointert &obj)
   return as_value(obj) != nullptr;
 }
 
-exprt assume_eq(abstract_environmentt &env, exprt expr, const namespacet &ns)
+exprt assume_not(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
+{
+  auto not_expr = to_not_expr(expr);
+  auto result = env.do_assume(not_expr.op(), ns);
+  if(result.is_boolean())
+    result = result.is_true() ? exprt(false_exprt()) : true_exprt();
+  return result;
+}
+
+exprt assume_and(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
+{
+  auto and_expr = to_and_expr(expr);
+  for(auto const &operand : and_expr.operands())
+  {
+    auto result = env.do_assume(operand, ns);
+    if(result.is_nil() || result.is_false())
+      return result;
+  }
+  return true_exprt();
+}
+
+exprt assume_or(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
+{
+  exprt or_result = false_exprt();
+  auto or_expr = to_or_expr(expr);
+  for(auto const &operand : or_expr.operands())
+  {
+    auto result = env.do_assume(operand, ns);
+    if(result.is_nil())
+      return result;
+    if(result.is_true())
+      or_result = true_exprt();
+  }
+  return or_result;
+}
+
+exprt assume_eq(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
 {
-  auto equal_expr = to_binary_expr(expr);
+  auto const &equal_expr = to_binary_expr(expr);
 
   auto left = env.eval(equal_expr.lhs(), ns);
   auto right = env.eval(equal_expr.rhs(), ns);
@@ -581,9 +609,12 @@ exprt assume_eq(abstract_environmentt &env, exprt expr, const namespacet &ns)
   return true_exprt();
 }
 
-exprt assume_noteq(abstract_environmentt &env, exprt expr, const namespacet &ns)
+exprt assume_noteq(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
 {
-  auto notequal_expr = to_binary_expr(expr);
+  auto const &notequal_expr = to_binary_expr(expr);
 
   auto left = env.eval(notequal_expr.lhs(), ns);
   auto right = env.eval(notequal_expr.rhs(), ns);
@@ -601,7 +632,7 @@ exprt assume_noteq(abstract_environmentt &env, exprt expr, const namespacet &ns)
   return false_exprt();
 }
 
-struct left_and_right_values
+struct left_and_right_valuest
 {
   abstract_value_pointert left;
   abstract_value_pointert right;
@@ -621,12 +652,12 @@ struct left_and_right_values
   }
 };
 
-left_and_right_values eval_operands_as_values(
+left_and_right_valuest eval_operands_as_values(
   abstract_environmentt &env,
-  exprt expr,
+  const exprt &expr,
   const namespacet &ns)
 {
-  auto relationship_expr = to_binary_expr(expr);
+  auto const &relationship_expr = to_binary_expr(expr);
 
   auto left = env.eval(relationship_expr.lhs(), ns);
   auto right = env.eval(relationship_expr.rhs(), ns);
@@ -637,7 +668,10 @@ left_and_right_values eval_operands_as_values(
   return {as_value(left), as_value(right)};
 }
 
-exprt assume_le(abstract_environmentt &env, exprt expr, const namespacet &ns)
+exprt assume_less_than(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
 {
   auto operands = eval_operands_as_values(env, expr, ns);
   if(!operands.are_good())
@@ -646,24 +680,15 @@ exprt assume_le(abstract_environmentt &env, exprt expr, const namespacet &ns)
   auto left_lower = operands.left_interval().get_lower();
   auto right_upper = operands.right_interval().get_upper();
 
-  auto reduced_le_expr = binary_relation_exprt(left_lower, ID_le, right_upper);
+  auto reduced_le_expr =
+    binary_relation_exprt(left_lower, expr.id(), right_upper);
   return env.eval(reduced_le_expr, ns)->to_constant();
 }
 
-exprt assume_lt(abstract_environmentt &env, exprt expr, const namespacet &ns)
-{
-  auto operands = eval_operands_as_values(env, expr, ns);
-  if(!operands.are_good())
-    return nil_exprt();
-
-  auto left_lower = operands.left_interval().get_lower();
-  auto right_upper = operands.right_interval().get_upper();
-
-  auto reduced_lt_expr = binary_relation_exprt(left_lower, ID_lt, right_upper);
-  return env.eval(reduced_lt_expr, ns)->to_constant();
-}
-
-exprt assume_ge(abstract_environmentt &env, exprt expr, const namespacet &ns)
+exprt assume_greater_than(
+  abstract_environmentt &env,
+  const exprt &expr,
+  const namespacet &ns)
 {
   auto operands = eval_operands_as_values(env, expr, ns);
   if(!operands.are_good())
@@ -672,19 +697,7 @@ exprt assume_ge(abstract_environmentt &env, exprt expr, const namespacet &ns)
   auto left_upper = operands.left_interval().get_upper();
   auto right_lower = operands.right_interval().get_lower();
 
-  auto reduced_ge_expr = binary_relation_exprt(left_upper, ID_ge, right_lower);
+  auto reduced_ge_expr =
+    binary_relation_exprt(left_upper, expr.id(), right_lower);
   return env.eval(reduced_ge_expr, ns)->to_constant();
 }
-
-exprt assume_gt(abstract_environmentt &env, exprt expr, const namespacet &ns)
-{
-  auto operands = eval_operands_as_values(env, expr, ns);
-  if(!operands.are_good())
-    return nil_exprt();
-
-  auto left_upper = operands.left_interval().get_upper();
-  auto right_lower = operands.right_interval().get_lower();
-
-  auto reduced_gt_expr = binary_relation_exprt(left_upper, ID_gt, right_lower);
-  return env.eval(reduced_gt_expr, ns)->to_constant();
-}

src/analyses/variable-sensitivity/abstract_environment.h

@@ -103,7 +103,7 @@ class abstract_environmentt
   /// The better the implementation the more precise the results
   /// will be.
   virtual bool assume(const exprt &expr, const namespacet &ns);
-  exprt do_assume(exprt e, const namespacet &ns);
+  exprt do_assume(const exprt &e, const namespacet &ns);
 
   /// Used within assign to do the actual dispatch
   ///

unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp

@@ -43,7 +43,7 @@ std::vector<std::string>
 split(std::string const &s, std::string const &delimiter);
 std::vector<exprt> numbersToExprs(std::vector<std::string> const &numbers);
 
-class assume_tester
+class assume_testert
 {
 public:
   void operator()(bool is_true, std::vector<std::string> const &tests)
@@ -95,7 +95,7 @@ class assume_tester
     }
   }
 
-  assume_tester(abstract_environmentt &env, namespacet &n)
+  assume_testert(abstract_environmentt &env, namespacet &n)
     : environment(env), ns(n)
   {
   }
@@ -163,7 +163,7 @@ SCENARIO(
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
-  assume_tester assumeTester(environment, ns);
+  assume_testert assumeTester(environment, ns);
 
   GIVEN("true or false")
   {
@@ -189,7 +189,7 @@ SCENARIO(
     auto val2 = from_integer(2, type);
     auto val3 = from_integer(3, type);
     auto val4 = from_integer(4, type);
-    auto val5 = from_integer(4, type);
+    auto val5 = from_integer(5, type);
     auto constant1 = make_constant(val1, environment, ns);
     auto constant3 = make_constant(val3, environment, ns);
     auto interval12 = make_interval(val1, val2, environment, ns);