Move has_byte_operator to util

There is nothing solvers-specific to this function. Cleanup in
preparation of moving all byte-operator lowering to util.

Author: tautschnig

src/solvers/flattening/boolbv_equality.cpp

@@ -6,13 +6,14 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
-#include <util/std_expr.h>
+#include <util/byte_operators.h>
 #include <util/invariant.h>
+#include <util/std_expr.h>
 
 #include <solvers/lowering/expr_lowering.h>
 
+#include "boolbv.h"
+
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
   const bool equality_types_match = expr.lhs().type() == expr.rhs().type();

src/solvers/lowering/byte_operators.cpp

@@ -2483,21 +2483,6 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
   return result;
 }
 
-bool has_byte_operator(const exprt &src)
-{
-  if(src.id()==ID_byte_update_little_endian ||
-     src.id()==ID_byte_update_big_endian ||
-     src.id()==ID_byte_extract_little_endian ||
-     src.id()==ID_byte_extract_big_endian)
-    return true;
-
-  forall_operands(it, src)
-    if(has_byte_operator(*it))
-      return true;
-
-  return false;
-}
-
 exprt lower_byte_operators(const exprt &src, const namespacet &ns)
 {
   exprt tmp=src;

src/solvers/lowering/expr_lowering.h

@@ -41,6 +41,4 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
 ///   byte_extract_exprt or \ref byte_update_exprt.
 exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
-bool has_byte_operator(const exprt &src);
-
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/util/byte_operators.cpp

@@ -57,3 +57,23 @@ make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
   return byte_update_exprt{
     byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};
 }
+
+bool has_byte_operator(const exprt &src)
+{
+  if(
+    src.id() == ID_byte_update_little_endian ||
+    src.id() == ID_byte_update_big_endian ||
+    src.id() == ID_byte_extract_little_endian ||
+    src.id() == ID_byte_extract_big_endian)
+  {
+    return true;
+  }
+
+  for(const auto &op : src.operands())
+  {
+    if(has_byte_operator(op))
+      return true;
+  }
+
+  return false;
+}

src/util/byte_operators.h

@@ -162,4 +162,8 @@ make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
 byte_update_exprt
 make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
 
+/// Return true iff \p src or one of its operands contain a byte extract or byte
+/// update expression.
+bool has_byte_operator(const exprt &src);
+
 #endif // CPROVER_UTIL_BYTE_OPERATORS_H