make_byte_{extract,update} to build byte_{extract,update} expressions

tautschnig · tautschnig · commit e98ee3bd6a49 · 2021-04-23T20:57:47.000Z
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.
diff --git 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
@@ -84,18 +84,15 @@ 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)
   {
     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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,17 @@ 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, config.ansi_c.char_width, _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, config.ansi_c.char_width};
+}
diff --git 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
@@ -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
@@ -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())
@@ -2022,8 +2031,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         if(val_offset + bytes_req > (*val_size) / 8)
           bytes_req = (*val_size) / 8 - val_offset;
 
-        byte_extract_exprt new_val(
-          byte_extract_id(),
+        byte_extract_exprt new_val = make_byte_extract(
+          ID_byte_extract_little_endian,
           value,
           from_integer(val_offset, offset.type()),
           array_typet(unsignedbv_typet(8),
diff --git 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
@@ -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);
 

Original file line number	Diff line number	Diff line change
`@@ -84,18 +84,15 @@ void rewrite_union(exprt &expr)`
`84`	`84`	`if(op.type().id() == ID_union_tag \|\| op.type().id() == ID_union)`
`85`	`85`	`{`
`86`	`86`	`exprt offset=from_integer(0, index_type());`
`87`		`- byte_extract_exprt tmp(byte_extract_id(), op, offset, expr.type());`
`88`		`- expr=tmp;`
	`87`	`+ expr = make_byte_extract(op, offset, expr.type());`
`89`	`88`	`}`
`90`	`89`	`}`
`91`	`90`	`else if(expr.id()==ID_union)`
`92`	`91`	`{`
`93`	`92`	`const union_exprt &union_expr=to_union_expr(expr);`
`94`	`93`	`exprt offset=from_integer(0, index_type());`
`95`	`94`	`side_effect_expr_nondett nondet(expr.type(), expr.source_location());`
`96`		`- byte_update_exprt tmp(`
`97`		`- byte_update_id(), nondet, offset, union_expr.op());`
`98`		`- expr=tmp;`
	`95`	`+ expr = make_byte_update(nondet, offset, union_expr.op());`
`99`	`96`	`}`
`100`	`97`	`}`
`101`	`98`
Original file line number	Diff line number	Diff line change
`@@ -107,15 +107,11 @@ void goto_symext::parameter_assignments(`
`107`	`107`	`rhs_type.id() == ID_pointer \|\|`
`108`	`108`	`rhs_type.id() == ID_union \|\|`
`109`	`109`	`rhs_type.id() == ID_union_tag))`
	`110`	`+ // clang-format on`
`110`	`111`	`{`
`111`		`- rhs=`
`112`		`- byte_extract_exprt(`
`113`		`- byte_extract_id(),`
`114`		`- rhs,`
`115`		`- from_integer(0, index_type()),`
`116`		`- parameter_type);`
	`112`	`+ rhs = make_byte_extract(`
	`113`	`+ rhs, from_integer(0, index_type()), parameter_type);`
`117`	`114`	`}`
`118`		`- // clang-format on`
`119`	`115`	`else`
`120`	`116`	`{`
`121`	`117`	`std::ostringstream error;`
Original file line number	Diff line number	Diff line change
`@@ -530,11 +530,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(`
`530`	`530`	`}`
`531`	`531`	`else`
`532`	`532`	`{`
`533`		`- result.value = byte_extract_exprt(`
`534`		`- byte_extract_id(),`
`535`		`- symbol_expr,`
`536`		`- pointer_offset(pointer_expr),`
`537`		`- dereference_type);`
	`533`	`+ result.value = make_byte_extract(`
	`534`	`+ symbol_expr, pointer_offset(pointer_expr), dereference_type);`
`538`	`535`	`result.pointer = address_of_exprt{result.value};`
`539`	`536`	`}`
`540`	`537`	`}`
`@@ -627,7 +624,10 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(`
`627`	`624`	`root_object_subexpression, o.offset(), dereference_type, ns);`
`628`	`625`	`if(subexpr.has_value())`
`629`	`626`	`simplify(subexpr.value(), ns);`
`630`		`- if(subexpr.has_value() && subexpr.value().id() != byte_extract_id())`
	`627`	`+ if(`
	`628`	`+ subexpr.has_value() &&`
	`629`	`+ subexpr.value().id() != ID_byte_extract_little_endian &&`
	`630`	`+ subexpr.value().id() != ID_byte_extract_big_endian)`
`631`	`631`	`{`
`632`	`632`	`// Successfully found a member, array index, or combination thereof`
`633`	`633`	`// that matches the desired type and offset:`
`@@ -768,7 +768,7 @@ bool value_set_dereferencet::memory_model_bytes(`
`768`	`768`	`else`
`769`	`769`	`{`
`770`	`770`	`// no, use 'byte_extract'`
`771`		`- result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);`
	`771`	`+ result = make_byte_extract(value, offset, to_type);`
`772`	`772`	`}`
`773`	`773`
`774`	`774`	`value=result;`
Original file line number	Diff line number	Diff line change
`@@ -338,8 +338,8 @@ bvt boolbvt::convert_index(`
`338`	`338`	`o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),`
`339`	`339`	`ns);`
`340`	`340`
`341`		`- byte_extract_exprt be(`
`342`		`- byte_extract_id(), o.root_object(), new_offset, array_type.subtype());`
	`341`	`+ byte_extract_exprt be =`
	`342`	`+ make_byte_extract(o.root_object(), new_offset, array_type.subtype());`
`343`	`343`
`344`	`344`	`return convert_bv(be);`
`345`	`345`	`}`
Original file line number	Diff line number	Diff line change
`@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]`
`10`	`10`
`11`	`11`	`#include "config.h"`
`12`	`12`
`13`		`-irep_idt byte_extract_id()`
	`13`	`+static irep_idt byte_extract_id()`
`14`	`14`	`{`
`15`	`15`	`switch(config.ansi_c.endianness)`
`16`	`16`	`{`
`@@ -27,7 +27,7 @@ irep_idt byte_extract_id()`
`27`	`27`	`UNREACHABLE;`
`28`	`28`	`}`
`29`	`29`
`30`		`-irep_idt byte_update_id()`
	`30`	`+static irep_idt byte_update_id()`
`31`	`31`	`{`
`32`	`32`	`switch(config.ansi_c.endianness)`
`33`	`33`	`{`
`@@ -43,3 +43,17 @@ irep_idt byte_update_id()`
`43`	`43`
`44`	`44`	`UNREACHABLE;`
`45`	`45`	`}`
	`46`	`+`
	`47`	`+byte_extract_exprt`
	`48`	`+make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)`
	`49`	`+{`
	`50`	`+ return byte_extract_exprt{`
	`51`	`+ byte_extract_id(), _op, _offset, config.ansi_c.char_width, _type};`
	`52`	`+}`
	`53`	`+`
	`54`	`+byte_update_exprt`
	`55`	`+make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)`
	`56`	`+{`
	`57`	`+ return byte_update_exprt{`
	`58`	`+ byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};`
	`59`	`+}`