Merge pull request #2221 from tautschnig/is-constantt

Move definition of can-be-constant-propagated to a central location

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/base_exceptions.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
@@ -79,122 +80,6 @@ void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
   ssa_expr.set_level_1(it->second.second);
 }
 
-/// This function determines what expressions are to be propagated as
-/// "constants"
-bool goto_symex_statet::constant_propagation(const exprt &expr) const
-{
-  if(expr.is_constant())
-    return true;
-
-  if(expr.id()==ID_address_of)
-  {
-    const address_of_exprt &address_of_expr=to_address_of_expr(expr);
-
-    return constant_propagation_reference(address_of_expr.object());
-  }
-  else if(expr.id()==ID_typecast)
-  {
-    const typecast_exprt &typecast_expr=to_typecast_expr(expr);
-
-    return constant_propagation(typecast_expr.op());
-  }
-  else if(expr.id()==ID_plus)
-  {
-    forall_operands(it, expr)
-      if(!constant_propagation(*it))
-        return false;
-
-    return true;
-  }
-  else if(expr.id()==ID_mult)
-  {
-    // propagate stuff with sizeof in it
-    forall_operands(it, expr)
-    {
-      if(it->find(ID_C_c_sizeof_type).is_not_nil())
-        return true;
-      else if(!constant_propagation(*it))
-        return false;
-    }
-
-    return true;
-  }
-  else if(expr.id()==ID_array)
-  {
-    forall_operands(it, expr)
-      if(!constant_propagation(*it))
-        return false;
-
-    return true;
-  }
-  else if(expr.id()==ID_array_of)
-  {
-    return constant_propagation(expr.op0());
-  }
-  else if(expr.id()==ID_with)
-  {
-    // this is bad
-    /*
-    forall_operands(it, expr)
-      if(!constant_propagation(expr.op0()))
-        return false;
-
-    return true;
-    */
-    return false;
-  }
-  else if(expr.id()==ID_struct)
-  {
-    forall_operands(it, expr)
-      if(!constant_propagation(*it))
-        return false;
-
-    return true;
-  }
-  else if(expr.id()==ID_union)
-  {
-    forall_operands(it, expr)
-      if(!constant_propagation(*it))
-        return false;
-
-    return true;
-  }
-  // byte_update works, byte_extract may be out-of-bounds
-  else if(expr.id()==ID_byte_update_big_endian ||
-          expr.id()==ID_byte_update_little_endian)
-  {
-    forall_operands(it, expr)
-      if(!constant_propagation(*it))
-        return false;
-
-    return true;
-  }
-
-  return false;
-}
-
-/// this function determines which reference-typed expressions are constant
-bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
-{
-  if(expr.id()==ID_symbol)
-    return true;
-  else if(expr.id()==ID_index)
-  {
-    const index_exprt &index_expr=to_index_expr(expr);
-
-    return constant_propagation_reference(index_expr.array()) &&
-           constant_propagation(index_expr.index());
-  }
-  else if(expr.id()==ID_member)
-  {
-    return constant_propagation_reference(to_member_expr(expr).compound());
-  }
-  else if(expr.id()==ID_string_constant)
-    return true;
-
-  return false;
-}
-
 /// write to a variable
 static bool check_renaming(const exprt &expr);
 
@@ -297,6 +182,41 @@ static void assert_l2_renaming(const exprt &expr)
   #endif
 }
 
+class goto_symex_is_constantt : public is_constantt
+{
+protected:
+  bool is_constant(const exprt &expr) const override
+  {
+    if(expr.id() == ID_mult)
+    {
+      // propagate stuff with sizeof in it
+      forall_operands(it, expr)
+      {
+        if(it->find(ID_C_c_sizeof_type).is_not_nil())
+          return true;
+        else if(!is_constant(*it))
+          return false;
+      }
+
+      return true;
+    }
+    else if(expr.id() == ID_with)
+    {
+      // this is bad
+      /*
+      forall_operands(it, expr)
+      if(!is_constant(expr.op0()))
+      return false;
+
+      return true;
+      */
+      return false;
+    }
+
+    return is_constantt::is_constant(expr);
+  }
+};
+
 void goto_symex_statet::assignment(
   ssa_exprt &lhs, // L0/L1
   const exprt &rhs,  // L2
@@ -341,7 +261,7 @@ void goto_symex_statet::assignment(
 
   // for value propagation -- the RHS is L2
 
-  if(!is_shared && record_value && constant_propagation(rhs))
+  if(!is_shared && record_value && goto_symex_is_constantt()(rhs))
     propagation.values[l1_identifier]=rhs;
   else
     propagation.remove(l1_identifier);

src/goto-symex/goto_symex_state.h

@@ -179,10 +179,6 @@ class goto_symex_statet final
     bool record_value,
     bool allow_pointer_unsoundness=false);
 
-  // what to propagate
-  bool constant_propagation(const exprt &expr) const;
-  bool constant_propagation_reference(const exprt &expr) const;
-
   // undoes all levels of renaming
   void get_original_name(exprt &expr) const;
   void get_original_name(typet &type) const;

src/util/expr_util.cpp

@@ -6,10 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "expr_util.h"
 
+#include <algorithm>
 #include <unordered_set>
+
 #include "expr.h"
 #include "expr_iterator.h"
 #include "fixedbv.h"
@@ -222,3 +223,55 @@ const exprt &skip_typecast(const exprt &expr)
 
   return skip_typecast(to_typecast_expr(expr).op());
 }
+
+/// This function determines what expressions are to be propagated as
+/// "constants"
+bool is_constantt::is_constant(const exprt &expr) const
+{
+  if(expr.is_constant())
+    return true;
+
+  if(expr.id() == ID_address_of)
+  {
+    return is_constant_address_of(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_typecast || expr.id() == ID_array_of ||
+    expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
+    expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
+    // byte_update works, byte_extract may be out-of-bounds
+    expr.id() == ID_byte_update_big_endian ||
+    expr.id() == ID_byte_update_little_endian)
+  {
+    return std::all_of(
+      expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
+        return is_constant(e);
+      });
+  }
+
+  return false;
+}
+
+/// this function determines which reference-typed expressions are constant
+bool is_constantt::is_constant_address_of(const exprt &expr) const
+{
+  if(expr.id() == ID_symbol)
+  {
+    return true;
+  }
+  else if(expr.id() == ID_index)
+  {
+    const index_exprt &index_expr = to_index_expr(expr);
+
+    return is_constant_address_of(index_expr.array()) &&
+           is_constant(index_expr.index());
+  }
+  else if(expr.id() == ID_member)
+  {
+    return is_constant_address_of(to_member_expr(expr).compound());
+  }
+  else if(expr.id() == ID_string_constant)
+    return true;
+
+  return false;
+}

src/util/expr_util.h

@@ -78,4 +78,23 @@ if_exprt lift_if(const exprt &, std::size_t operand_number);
 /// find the expression nested inside typecasts, if any
 const exprt &skip_typecast(const exprt &expr);
 
+/// Determine whether an expression is constant.  A literal constant is
+/// constant, but so are, e.g., sums over constants or addresses of objects.
+/// An implementation derive from this class to refine what it considers
+/// constant in a particular context by overriding is_constant and/or
+/// is_constant_address_of.
+class is_constantt
+{
+public:
+  /// returns true iff the expression can be considered constant
+  bool operator()(const exprt &e) const
+  {
+    return is_constant(e);
+  }
+
+protected:
+  virtual bool is_constant(const exprt &) const;
+  virtual bool is_constant_address_of(const exprt &) const;
+};
+
 #endif // CPROVER_UTIL_EXPR_UTIL_H