Merge 9530cd3 into 308cc0a

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -82,9 +82,9 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (180), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), 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 'config.h' not generated, too many nodes (84), 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/solvers/flattening/boolbv.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/config.h>
 #include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
@@ -31,6 +32,13 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/floatbv/float_utils.h>
 #include <solvers/lowering/expr_lowering.h>
 
+endianness_mapt boolbvt::endianness_map(const typet &type) const
+{
+  const bool little_endian =
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
+  return endianness_map(type, little_endian);
+}
+
 /// Convert expression to vector of literalts, using an internal
 /// cache to speed up conversion if available. Also assert the resultant
 /// vector is of a specific size, and freeze any elements if appropriate.

src/solvers/flattening/boolbv.h

@@ -104,6 +104,8 @@ class boolbvt:public arrayst
     return endianness_mapt{type, little_endian, ns};
   }
 
+  virtual endianness_mapt endianness_map(const typet &type) const;
+
 protected:
   boolbv_widtht bv_width;
   bv_utilst bv_utils;

src/solvers/flattening/boolbv_byte_update.cpp

@@ -58,31 +58,23 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
     }
     else
     {
-      if(little_endian)
-      {
-        for(std::size_t i=0; i<update_width; i++)
-          bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
-      }
-      else
-      {
-        endianness_mapt map_op = endianness_map(op.type(), false);
-        endianness_mapt map_value = endianness_map(value.type(), false);
+      endianness_mapt map_op = endianness_map(op.type(), little_endian);
+      endianness_mapt map_value = endianness_map(value.type(), little_endian);
 
-        const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
+      const std::size_t offset_i = numeric_cast_v<std::size_t>(offset);
 
-        for(std::size_t i=0; i<update_width; i++)
-        {
-          size_t index_op=map_op.map_bit(offset_i+i);
-          size_t index_value=map_value.map_bit(i);
+      for(std::size_t i = 0; i < update_width; i++)
+      {
+        size_t index_op = map_op.map_bit(offset_i + i);
+        size_t index_value = map_value.map_bit(i);
 
-          INVARIANT(
-            index_op < bv.size(), "bit vector index shall be within bounds");
-          INVARIANT(
-            index_value < value_bv.size(),
-            "bit vector index shall be within bounds");
+        INVARIANT(
+          index_op < bv.size(), "bit vector index shall be within bounds");
+        INVARIANT(
+          index_value < value_bv.size(),
+          "bit vector index shall be within bounds");
 
-          bv[index_op]=value_bv[index_value];
-        }
+        bv[index_op] = value_bv[index_value];
       }
     }
 

src/solvers/flattening/boolbv_member.cpp

@@ -8,16 +8,18 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-bvt boolbvt::convert_member(const member_exprt &expr)
+static bvt convert_member_struct(
+  const member_exprt &expr,
+  const bvt &struct_bv,
+  const std::function<std::size_t(const typet &)> boolbv_width,
+  const namespacet &ns)
 {
   const exprt &struct_op=expr.struct_op();
   const typet &struct_op_type=ns.follow(struct_op.type());
 
-  const bvt &struct_bv=convert_bv(struct_op);
-
   const irep_idt &component_name = expr.get_component_name();
-  const struct_union_typet::componentst &components =
-    to_struct_union_type(struct_op_type).components();
+  const struct_typet::componentst &components =
+    to_struct_type(struct_op_type).components();
 
   std::size_t offset = 0;
 
@@ -42,8 +44,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
         struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
     }
 
-    if(struct_op_type.id() != ID_union)
-      offset += sub_width;
+    offset += sub_width;
   }
 
   INVARIANT_WITH_DIAGNOSTICS(
@@ -52,3 +53,52 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     expr.find_source_location(),
     id2string(component_name));
 }
+
+static bvt convert_member_union(
+  const member_exprt &expr,
+  const bvt &union_bv,
+  const boolbvt &boolbv,
+  const namespacet &ns)
+{
+  const exprt &union_op = expr.compound();
+  const union_typet &union_op_type =
+    ns.follow_tag(to_union_tag_type(union_op.type()));
+
+  const irep_idt &component_name = expr.get_component_name();
+  const union_typet::componentt &component =
+    union_op_type.get_component(component_name);
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    component.is_not_nil(),
+    "union type shall contain component accessed by member expression",
+    expr.find_source_location(),
+    id2string(component_name));
+
+  const typet &subtype = component.type();
+  const std::size_t sub_width = boolbv.boolbv_width(subtype);
+
+  endianness_mapt map_u = boolbv.endianness_map(union_op_type);
+  endianness_mapt map_component = boolbv.endianness_map(subtype);
+
+  bvt result(sub_width, literalt{});
+  for(std::size_t i = 0; i < sub_width; ++i)
+    result[map_u.map_bit(i)] = union_bv[map_component.map_bit(i)];
+
+  return result;
+}
+
+bvt boolbvt::convert_member(const member_exprt &expr)
+{
+  const bvt &compound_bv = convert_bv(expr.compound());
+
+  if(expr.compound().type().id() == ID_struct_tag)
+    return convert_member_struct(
+      expr,
+      compound_bv,
+      [this](const typet &t) { return boolbv_width(t); },
+      ns);
+  else
+  {
+    PRECONDITION(expr.compound().type().id() == ID_union_tag);
+    return convert_member_union(expr, compound_bv, *this, ns);
+  }
+}

src/solvers/flattening/boolbv_union.cpp

@@ -8,9 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <util/arith_tools.h>
-#include <util/config.h>
-
 bvt boolbvt::convert_union(const union_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
@@ -28,31 +25,15 @@ bvt boolbvt::convert_union(const union_exprt &expr)
   bvt bv;
   bv.resize(width);
 
-  if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
-  {
-    for(std::size_t i=0; i<op_bv.size(); i++)
-      bv[i]=op_bv[i];
-
-    // pad with nondets
-    for(std::size_t i=op_bv.size(); i<bv.size(); i++)
-      bv[i]=prop.new_variable();
-  }
-  else
-  {
-    INVARIANT(
-      config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_BIG_ENDIAN,
-      "endianness should be set to either little endian or big endian");
-
-    endianness_mapt map_u = endianness_map(expr.type(), false);
-    endianness_mapt map_op = endianness_map(expr.op().type(), false);
-
-    for(std::size_t i=0; i<op_bv.size(); i++)
-      bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];
-
-    // pad with nondets
-    for(std::size_t i=op_bv.size(); i<bv.size(); i++)
-      bv[map_u.map_bit(i)]=prop.new_variable();
-  }
+  endianness_mapt map_u = endianness_map(expr.type());
+  endianness_mapt map_op = endianness_map(expr.op().type());
+
+  for(std::size_t i = 0; i < op_bv.size(); i++)
+    bv[map_u.map_bit(i)] = op_bv[map_op.map_bit(i)];
+
+  // pad with nondets
+  for(std::size_t i = op_bv.size(); i < bv.size(); i++)
+    bv[map_u.map_bit(i)] = prop.new_variable();
 
   return bv;
 }

src/solvers/flattening/boolbv_with.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
-#include <util/config.h>
 
 bvt boolbvt::convert_with(const with_exprt &expr)
 {
@@ -236,20 +235,9 @@ void boolbvt::convert_with_union(
     "convert_with_union: unexpected operand op2 width",
     irep_pretty_diagnosticst{type});
 
-  if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
-  {
-    for(std::size_t i=0; i<op2_bv.size(); i++)
-      next_bv[i]=op2_bv[i];
-  }
-  else
-  {
-    assert(
-      config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN);
+  endianness_mapt map_u = endianness_map(type);
+  endianness_mapt map_op2 = endianness_map(op2.type());
 
-    endianness_mapt map_u = endianness_map(type, false);
-    endianness_mapt map_op2 = endianness_map(op2.type(), false);
-
-    for(std::size_t i=0; i<op2_bv.size(); i++)
-      next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
-  }
+  for(std::size_t i = 0; i < op2_bv.size(); i++)
+    next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
 }