Configure bits_per_byte in byte_extract/byte_update expression

Semantically evaluating a byte_extract/byte_update expression requires
knowledge of the number of bits that a byte is composed of. This,
however, is a configuration parameter known to the front-end that
created the expression in the first place. The back-end should not need
to consult configuration information to evaluate the expression.

Author: tautschnig

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -33,9 +33,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
     index_exprt(valid_symbol_expr, valid_constant);
   const index_exprt index_plain = index_exprt(exprt(), exprt());
   const byte_extract_exprt byte_little_endian = byte_extract_exprt(
-    ID_byte_extract_little_endian, exprt(), exprt(), typet());
-  const byte_extract_exprt byte_big_endian =
-    byte_extract_exprt(ID_byte_extract_big_endian, exprt(), exprt(), typet());
+    ID_byte_extract_little_endian, exprt(), exprt(), 8, typet());
+  const byte_extract_exprt byte_big_endian = byte_extract_exprt(
+    ID_byte_extract_big_endian, exprt(), exprt(), 8, typet());
   const address_of_exprt valid_address = address_of_exprt(valid_symbol_expr);
   const address_of_exprt invalid_address = address_of_exprt(exprt());
   const struct_exprt struct_plain =

scripts/expected_doxygen_warnings.txt

@@ -23,7 +23,7 @@ warning: Included by graph for 'goto_functions.h' not generated, too many nodes
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (143), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (85), 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 (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/goto_rw.cpp

@@ -157,7 +157,7 @@ void rw_range_sett::get_objects_byte_extract(
     get_objects_rec(mode, be.op(), -1, size);
   else
   {
-    *index *= 8;
+    *index *= be.get_bits_per_byte();
     if(*index >= *pointer_offset_bits(be.op().type(), ns))
       return;
 

src/ansi-c/c_typecheck_initializer.cpp

@@ -542,8 +542,11 @@ 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{byte_update_id(),
+                                        *dest,
+                                        from_integer(0, index_type()),
+                                        *zero,
+                                        config.ansi_c.char_width};
           byte_update.add_source_location() = value.source_location();
           *dest = std::move(byte_update);
           dest = &(to_byte_update_expr(*dest).op2());

src/goto-programs/rewrite_union.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
@@ -84,7 +85,8 @@ 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());
+      byte_extract_exprt tmp(
+        byte_extract_id(), op, offset, config.ansi_c.char_width, expr.type());
       expr=tmp;
     }
   }
@@ -94,7 +96,11 @@ void rewrite_union(exprt &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());
+      byte_update_id(),
+      nondet,
+      offset,
+      union_expr.op(),
+      config.ansi_c.char_width);
     expr=tmp;
   }
 }

src/goto-symex/symex_assign.cpp

@@ -11,13 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "symex_assign.h"
 
-#include "expr_skeleton.h"
-#include "goto_symex.h"
-#include "goto_symex_state.h"
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
 
+#include "expr_skeleton.h"
+#include "goto_symex.h"
+#include "goto_symex_state.h"
+
 // We can either use with_exprt or update_exprt when building expressions that
 // modify components of an array or a struct. Set USE_UPDATE to use
 // update_exprt.
@@ -377,7 +378,8 @@ void symex_assignt::assign_byte_extract(
   else
     UNREACHABLE;
 
-  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
+  const byte_update_exprt new_rhs{
+    byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
   const expr_skeletont new_skeleton =
     full_lhs.compose(expr_skeletont::remove_op0(lhs));
   assign_rec(lhs.op(), new_skeleton, new_rhs, guard);

src/goto-symex/symex_clean_expr.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/expr_iterator.h>
 #include <util/nodiscard.h>
 #include <util/pointer_offset_size.h>
@@ -46,6 +47,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
         byte_extract_id(),
         if_expr.false_case(),
         from_integer(0, index_type()),
+        config.ansi_c.char_width,
         if_expr.true_case().type());
 
       if_expr.false_case().swap(be);
@@ -95,6 +97,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
           byte_extract_id(),
           expr,
           from_integer(0, index_type()),
+          config.ansi_c.char_width,
           array_typet(char_type(), array_size.value()));
       }
 
@@ -123,12 +126,12 @@ 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 = byte_extract_exprt(
+        byte_extract_id(),
+        expr,
+        ode.offset(),
+        config.ansi_c.char_width,
+        new_array_type);
     }
   }
 }

src/goto-symex/symex_dereference.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
@@ -93,7 +94,11 @@ exprt goto_symext::address_arithmetic(
     ode.build(expr, ns);
 
     const byte_extract_exprt be(
-      byte_extract_id(), ode.root_object(), ode.offset(), expr.type());
+      byte_extract_id(),
+      ode.root_object(),
+      ode.offset(),
+      config.ansi_c.char_width,
+      expr.type());
 
     // recursive call
     result = address_arithmetic(be, state, keep_array);
@@ -152,6 +157,7 @@ exprt goto_symext::address_arithmetic(
         byte_extract_id(),
         to_ssa_expr(expr).get_l1_object(),
         from_integer(offset, index_type()),
+        config.ansi_c.char_width,
         expr.type());
 
       result = address_arithmetic(be, state, keep_array);

src/goto-symex/symex_function_call.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -112,7 +113,7 @@ void goto_symext::parameter_assignments(
             byte_extract_exprt(
               byte_extract_id(),
               rhs,
-              from_integer(0, index_type()),
+              from_integer(0, index_type()), config.ansi_c.char_width,
               parameter_type);
         }
         // clang-format on

src/goto-symex/symex_other.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/pointer_offset_size.h>
 
 void goto_symext::havoc_rec(
@@ -148,6 +149,7 @@ void goto_symext::symex_other(
           byte_extract_id(),
           src_array,
           from_integer(0, index_type()),
+          config.ansi_c.char_width,
           dest_array.type());
         src_array.swap(be);
         do_simplify(src_array);
@@ -159,6 +161,7 @@ void goto_symext::symex_other(
           byte_extract_id(),
           dest_array,
           from_integer(0, index_type()),
+          config.ansi_c.char_width,
           src_array.type());
         dest_array.swap(be);
         do_simplify(dest_array);
@@ -200,6 +203,7 @@ void goto_symext::symex_other(
         byte_extract_id(),
         array_expr,
         from_integer(0, index_type()),
+        config.ansi_c.char_width,
         array_typet(char_type(), array_size.value()));
     }