From e7d82097590385ad860833ecfd75ab23644a2310 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 23 Apr 2021 20:43:51 +0000
Subject: [PATCH] make_byte_{extract,update} to build byte_{extract,update}
 expressions

Remove byte_{extract,update}_id from the API (marking them static) and
instead add factory functions make_byte_{extract,update} to construct
the full expression. These functions will ensure that both endianness
and byte width are consistently configured.
---
 src/ansi-c/c_typecheck_initializer.cpp        |  4 ++--
 src/goto-programs/rewrite_union.cpp           |  7 ++-----
 src/goto-symex/symex_clean_expr.cpp           | 13 +++---------
 src/goto-symex/symex_dereference.cpp          |  7 +++----
 src/goto-symex/symex_function_call.cpp        | 10 +++------
 src/goto-symex/symex_other.cpp                | 19 +++++------------
 .../value_set_dereference.cpp                 | 14 ++++++-------
 src/solvers/flattening/boolbv_index.cpp       |  4 ++--
 src/solvers/flattening/pointer_logic.cpp      |  6 +++++-
 src/util/byte_operators.cpp                   | 16 ++++++++++++--
 src/util/byte_operators.h                     | 13 +++++++++---
 src/util/pointer_offset_size.cpp              |  7 ++-----
 src/util/simplify_expr.cpp                    | 21 +++++++++++++------
 unit/util/pointer_offset_size.cpp             | 14 +++++--------
 unit/util/simplify_expr.cpp                   |  4 ++--
 15 files changed, 80 insertions(+), 79 deletions(-)

diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 5e04a751b3e..73beab374ac 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -542,8 +542,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
         if(current_symbol.is_static_lifetime)
         {
-          byte_update_exprt byte_update{
-            byte_update_id(), *dest, from_integer(0, index_type()), *zero};
+          byte_update_exprt byte_update =
+            make_byte_update(*dest, from_integer(0, index_type()), *zero);
           byte_update.add_source_location() = value.source_location();
           *dest = std::move(byte_update);
           dest = &(to_byte_update_expr(*dest).op2());
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index d68d999681d..8df56a41a9b 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -84,8 +84,7 @@ void rewrite_union(exprt &expr)
     if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
       exprt offset=from_integer(0, index_type());
-      byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());
-      expr=tmp;
+      expr = make_byte_extract(op, offset, expr.type());
     }
   }
   else if(expr.id()==ID_union)
@@ -93,9 +92,7 @@ void rewrite_union(exprt &expr)
     const union_exprt &union_expr=to_union_expr(expr);
     exprt offset=from_integer(0, index_type());
     side_effect_expr_nondett nondet(expr.type(), expr.source_location());
-    byte_update_exprt tmp(
-      byte_update_id(), nondet, offset, union_expr.op());
-    expr=tmp;
+    expr = make_byte_update(nondet, offset, union_expr.op());
   }
 }
 
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 057e7e31f86..2ae12cd473c 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -42,8 +42,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 
     if(if_expr.true_case() != if_expr.false_case())
     {
-      byte_extract_exprt be(
-        byte_extract_id(),
+      byte_extract_exprt be = make_byte_extract(
         if_expr.false_case(),
         from_integer(0, index_type()),
         if_expr.true_case().type());
@@ -91,8 +90,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
         CHECK_RETURN(array_size.has_value());
         if(do_simplify)
           simplify(array_size.value(), ns);
-        expr = byte_extract_exprt(
-          byte_extract_id(),
+        expr = make_byte_extract(
           expr,
           from_integer(0, index_type()),
           array_typet(char_type(), array_size.value()));
@@ -123,12 +121,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
 
       array_typet new_array_type(subtype, new_size);
 
-      expr =
-        byte_extract_exprt(
-          byte_extract_id(),
-          expr,
-          ode.offset(),
-          new_array_type);
+      expr = make_byte_extract(expr, ode.offset(), new_array_type);
     }
   }
 }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index a88321abd48..b1b1d1665c3 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -95,8 +95,8 @@ exprt goto_symext::address_arithmetic(
     object_descriptor_exprt ode;
     ode.build(expr, ns);
 
-    const byte_extract_exprt be(
-      byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
+    const byte_extract_exprt be =
+      make_byte_extract(ode.root_object(), ode.offset(), expr.type());
 
     // recursive call
     result = address_arithmetic(be, state, keep_array);
@@ -151,8 +151,7 @@ exprt goto_symext::address_arithmetic(
 
     if(offset>0)
     {
-      const byte_extract_exprt be(
-        byte_extract_id(),
+      const byte_extract_exprt be = make_byte_extract(
         to_ssa_expr(expr).get_l1_object(),
         from_integer(offset, index_type()),
         expr.type());
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index 2470249ace1..918c40ba090 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -107,15 +107,11 @@ void goto_symext::parameter_assignments(
            rhs_type.id() == ID_pointer ||
            rhs_type.id() == ID_union ||
            rhs_type.id() == ID_union_tag))
+        // clang-format on
         {
-          rhs=
-            byte_extract_exprt(
-              byte_extract_id(),
-              rhs,
-              from_integer(0, index_type()),
-              parameter_type);
+          rhs = make_byte_extract(
+            rhs, from_integer(0, index_type()), parameter_type);
         }
-        // clang-format on
         else
         {
           std::ostringstream error;
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 0e00d311fa4..c26f3621971 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -144,23 +144,15 @@ void goto_symext::symex_other(
     {
       if(statement==ID_array_copy)
       {
-        byte_extract_exprt be(
-          byte_extract_id(),
-          src_array,
-          from_integer(0, index_type()),
-          dest_array.type());
-        src_array.swap(be);
+        src_array = make_byte_extract(
+          src_array, from_integer(0, index_type()), dest_array.type());
         do_simplify(src_array);
       }
       else
       {
         // ID_array_replace
-        byte_extract_exprt be(
-          byte_extract_id(),
-          dest_array,
-          from_integer(0, index_type()),
-          src_array.type());
-        dest_array.swap(be);
+        dest_array = make_byte_extract(
+          dest_array, from_integer(0, index_type()), src_array.type());
         do_simplify(dest_array);
       }
     }
@@ -196,8 +188,7 @@ void goto_symext::symex_other(
       auto array_size = size_of_expr(array_expr.type(), ns);
       CHECK_RETURN(array_size.has_value());
       do_simplify(array_size.value());
-      array_expr = byte_extract_exprt(
-        byte_extract_id(),
+      array_expr = make_byte_extract(
         array_expr,
         from_integer(0, index_type()),
         array_typet(char_type(), array_size.value()));
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 0e994f8ba4d..3d2d4e65aed 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -530,11 +530,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       }
       else
       {
-        result.value = byte_extract_exprt(
-          byte_extract_id(),
-          symbol_expr,
-          pointer_offset(pointer_expr),
-          dereference_type);
+        result.value = make_byte_extract(
+          symbol_expr, pointer_offset(pointer_expr), dereference_type);
         result.pointer = address_of_exprt{result.value};
       }
     }
@@ -627,7 +624,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         root_object_subexpression, o.offset(), dereference_type, ns);
       if(subexpr.has_value())
         simplify(subexpr.value(), ns);
-      if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())
+      if(
+        subexpr.has_value() &&
+        subexpr.value().id() != ID_byte_extract_little_endian &&
+        subexpr.value().id() != ID_byte_extract_big_endian)
       {
         // Successfully found a member, array index, or combination thereof
         // that matches the desired type and offset:
@@ -768,7 +768,7 @@ bool value_set_dereferencet::memory_model_bytes(
   else
   {
     // no, use 'byte_extract'
-    result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
+    result = make_byte_extract(value, offset, to_type);
   }
 
   value=result;
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 0b2cec1dba2..a267bd2af3f 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -338,8 +338,8 @@ bvt boolbvt::convert_index(
         o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
       ns);
 
-    byte_extract_exprt be(
-      byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
+    byte_extract_exprt be =
+      make_byte_extract(o.root_object(), new_offset, array_type.subtype());
 
     return convert_bv(be);
   }
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index f96921d3a48..91f59a7c0ab 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -118,9 +118,13 @@ exprt pointer_logict::pointer_expr(
   CHECK_RETURN(deep_object_opt.has_value());
   exprt deep_object = deep_object_opt.value();
   simplify(deep_object, ns);
-  if(deep_object.id() != byte_extract_id())
+  if(
+    deep_object.id() != ID_byte_extract_little_endian &&
+    deep_object.id() != ID_byte_extract_big_endian)
+  {
     return typecast_exprt::conditional_cast(
       address_of_exprt(deep_object), type);
+  }
 
   const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
   const address_of_exprt base(be.op());
diff --git a/src/util/byte_operators.cpp b/src/util/byte_operators.cpp
index 25895e872e6..a5d14030835 100644
--- a/src/util/byte_operators.cpp
+++ b/src/util/byte_operators.cpp
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "config.h"
 
-irep_idt byte_extract_id()
+static irep_idt byte_extract_id()
 {
   switch(config.ansi_c.endianness)
   {
@@ -27,7 +27,7 @@ irep_idt byte_extract_id()
   UNREACHABLE;
 }
 
-irep_idt byte_update_id()
+static irep_idt byte_update_id()
 {
   switch(config.ansi_c.endianness)
   {
@@ -43,3 +43,15 @@ irep_idt byte_update_id()
 
   UNREACHABLE;
 }
+
+byte_extract_exprt
+make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
+{
+  return byte_extract_exprt{byte_extract_id(), _op, _offset, _type};
+}
+
+byte_update_exprt
+make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
+{
+  return byte_update_exprt{byte_update_id(), _op, _offset, _value};
+}
diff --git a/src/util/byte_operators.h b/src/util/byte_operators.h
index 9700c6b4471..e7e99c89818 100644
--- a/src/util/byte_operators.h
+++ b/src/util/byte_operators.h
@@ -71,9 +71,6 @@ inline void validate_expr(const byte_extract_exprt &value)
   validate_operands(value, 2, "Byte extract must have two operands");
 }
 
-irep_idt byte_extract_id();
-irep_idt byte_update_id();
-
 /// Expression corresponding to \c op() where the bytes starting at
 /// position \c offset (given in number of bytes) have been updated with
 /// \c value.
@@ -129,4 +126,14 @@ inline byte_update_exprt &to_byte_update_expr(exprt &expr)
   return static_cast<byte_update_exprt &>(expr);
 }
 
+/// Construct a byte_extract_exprt with endianness and byte width matching the
+/// current configuration.
+byte_extract_exprt
+make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
+
+/// Construct a byte_update_exprt with endianness and byte width matching the
+/// current configuration.
+byte_update_exprt
+make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
+
 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index ab5877de5bf..0ca699855cc 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -682,11 +682,8 @@ optionalt<exprt> get_subexpression_at_offset(
     }
   }
 
-  return byte_extract_exprt(
-    byte_extract_id(),
-    expr,
-    from_integer(offset_bytes, index_type()),
-    target_type_raw);
+  return make_byte_extract(
+    expr, from_integer(offset_bytes, index_type()), target_type_raw);
 }
 
 optionalt<exprt> get_subexpression_at_offset(
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index a23dde76f80..edf07cf7189 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -152,7 +152,9 @@ simplify_exprt::resultt<>
 simplify_exprt::simplify_clz(const count_leading_zeros_exprt &expr)
 {
   const auto const_bits_opt = expr2bits(
-    expr.op(), byte_extract_id() == ID_byte_extract_little_endian, ns);
+    expr.op(),
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
+    ns);
 
   if(!const_bits_opt.has_value())
     return unchanged(expr);
@@ -1634,7 +1636,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
   // don't do any of the following if endianness doesn't match, as
   // bytes need to be swapped
-  if(*offset == 0 && byte_extract_id() == expr.id())
+  if(
+    *offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
+                      config.ansi_c.endianness ==
+                        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
+                     (expr.id() == ID_byte_extract_big_endian &&
+                      config.ansi_c.endianness ==
+                        configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
   {
     // byte extract of full object is object
     if(expr.type() == expr.op().type())
@@ -1658,7 +1666,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   {
     const auto const_bits_opt = expr2bits(
       to_array_of_expr(expr.op()).op(),
-      byte_extract_id() == ID_byte_extract_little_endian,
+      config.ansi_c.endianness ==
+        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN,
       ns);
 
     if(!const_bits_opt.has_value())
@@ -2023,11 +2032,11 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           bytes_req = (*val_size) / 8 - val_offset;
 
         byte_extract_exprt new_val(
-          byte_extract_id(),
+          ID_byte_extract_little_endian,
           value,
           from_integer(val_offset, offset.type()),
-          array_typet(unsignedbv_typet(8),
-                      from_integer(bytes_req, offset.type())));
+          array_typet(
+            unsignedbv_typet(8), from_integer(bytes_req, offset.type())));
 
         *it = byte_update_exprt(
           expr.id(),
diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp
index 64ba0afcb55..3a1a5f8edd4 100644
--- a/unit/util/pointer_offset_size.cpp
+++ b/unit/util/pointer_offset_size.cpp
@@ -59,8 +59,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
     const signedbv_typet small_t(8);
     const auto result = get_subexpression_at_offset(a, 1, small_t, ns);
     REQUIRE(
-      result.value() == byte_extract_exprt(
-                          byte_extract_id(),
+      result.value() == make_byte_extract(
                           index_exprt(a, from_integer(0, index_type())),
                           from_integer(1, index_type()),
                           small_t));
@@ -74,8 +73,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
     // index_exprt.
     REQUIRE(
       result.value() ==
-      byte_extract_exprt(
-        byte_extract_id(), a, from_integer(3, index_type()), int16_t));
+      make_byte_extract(a, from_integer(3, index_type()), int16_t));
   }
 }
 
@@ -121,10 +119,8 @@ TEST_CASE("Build subexpression to access element at offset into struct")
     const signedbv_typet small_t(8);
     const auto result = get_subexpression_at_offset(s, 1, small_t, ns);
     REQUIRE(
-      result.value() == byte_extract_exprt(
-                          byte_extract_id(),
-                          member_exprt(s, "foo", t),
-                          from_integer(1, index_type()),
-                          small_t));
+      result.value() ==
+      make_byte_extract(
+        member_exprt(s, "foo", t), from_integer(1, index_type()), small_t));
   }
 }
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 50058792484..a7f1e19a62b 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -78,8 +78,8 @@ TEST_CASE("Simplify byte extract", "[core][util]")
   // byte-extracting type T at offset 0 from an object of type T yields the
   // object
   symbol_exprt s("foo", size_type());
-  byte_extract_exprt be(
-    byte_extract_id(), s, from_integer(0, index_type()), size_type());
+  byte_extract_exprt be =
+    make_byte_extract(s, from_integer(0, index_type()), size_type());
 
   exprt simp = simplify_expr(be, ns);