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, [email protected]
 #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, [email protected]
 
 #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, [email protected]
 #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, [email protected]
 #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, [email protected]
 #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, [email protected]
 #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()));
     }
 

src/pointer-analysis/value_set_dereference.cpp

@@ -534,6 +534,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
           byte_extract_id(),
           symbol_expr,
           pointer_offset(pointer_expr),
+          config.ansi_c.char_width,
           dereference_type);
         result.pointer = address_of_exprt{result.value};
       }
@@ -768,7 +769,8 @@ bool value_set_dereferencet::memory_model_bytes(
   else
   {
     // no, use 'byte_extract'
-    result = byte_extract_exprt(byte_extract_id(), value, offset, to_type);
+    result = byte_extract_exprt(
+      byte_extract_id(), value, offset, config.ansi_c.char_width, to_type);
   }
 
   value=result;

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -49,11 +49,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   #if 0
   if(expr.id()==ID_byte_extract_big_endian &&
      expr.type().id()==ID_c_bit_field &&
-     (width%8)!=0)
+     (width%expr.get_bits_per_byte())!=0)
   {
     byte_extract_exprt tmp=expr;
     // round up
-    to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
+    to_c_bit_field_type(tmp.type()).set_width(
+      width+expr.get_bits_per_byte()-width%expr.get_bits_per_byte());
     convert_byte_extract(tmp, bv);
     bv.resize(width); // chop down
     return;
@@ -87,6 +88,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       expr.id(),
       o.root_object(),
       plus_exprt(o.offset(), expr.offset()),
+      expr.get_bits_per_byte(),
       expr.type());
 
     return convert_bv(be);
@@ -108,11 +110,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   bv.resize(width);
 
   // see if the byte number is constant
-  unsigned byte_width=8;
-
   if(index.has_value())
   {
-    const mp_integer offset = *index * byte_width;
+    const mp_integer offset = *index * expr.get_bits_per_byte();
 
     for(std::size_t i=0; i<width; i++)
       // out of bounds?
@@ -123,7 +123,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
   else
   {
-    std::size_t bytes=op_bv.size()/byte_width;
+    std::size_t bytes = op_bv.size() / expr.get_bits_per_byte();
 
     if(prop.has_set_to())
     {
@@ -141,7 +141,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
           if(offset+j<op_bv.size())
@@ -164,7 +164,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
         literalt e =
           convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
 
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
         {

src/solvers/flattening/boolbv_byte_update.cpp

@@ -39,7 +39,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
   const bvt &value_bv=convert_bv(value);
   std::size_t update_width=value_bv.size();
-  std::size_t byte_width=8;
+  std::size_t byte_width = expr.get_bits_per_byte();
 
   if(update_width>bv.size())
     update_width=bv.size();
@@ -50,7 +50,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   if(index.has_value())
   {
     // yes!
-    const mp_integer offset = *index * 8;
+    const mp_integer offset = *index * byte_width;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {

src/solvers/flattening/boolbv_index.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -347,7 +348,11 @@ bvt boolbvt::convert_index(
       ns);
 
     byte_extract_exprt be(
-      byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
+      byte_extract_id(),
+      o.root_object(),
+      new_offset,
+      config.ansi_c.char_width,
+      array_type.subtype());
 
     return convert_bv(be);
   }