remove padded field and record its width

src/goto-symex/builtin_functions.cpp

@@ -1819,6 +1819,9 @@ type2tc goto_symext::create_heap_region_type(
   unsigned int bytes,
   const expr2tc &loc)
 {
+  log_debug("SLHV", "Create heap region with type : ");
+  if (messaget::state.modules.count("SLHV") > 0) type->dump();
+
   type2tc heap_type = get_intheap_type();
   intheap_type2t &_heap_type = to_intheap_type(heap_type);
   _heap_type.location = loc;
@@ -1831,8 +1834,22 @@ type2tc goto_symext::create_heap_region_type(
     _heap_type.total_bytes = bytes;
     const struct_type2t &_type = to_struct_type(type);
     _heap_type.field_types.clear();
-    for (auto const &it : _type.members)
-      _heap_type.field_types.push_back(it);
+    const std::vector<type2tc> &inner_types = _type.get_structure_members();
+    const std::vector<irep_idt> &inner_field_names = _type.get_structure_member_names();
+    _heap_type.field_types.push_back(inner_types[0]);
+    for (unsigned int i = 1; i < inner_field_names.size(); i++)
+    {
+      const std::string &field_name = inner_field_names[i].as_string();
+      if (has_prefix(inner_field_names[i], "anon"))
+        _heap_type.pads.push_back(inner_types[i]->get_width());
+      else
+      {  
+        _heap_type.field_types.push_back(inner_types[i]);
+        _heap_type.pads.push_back(0);
+      }
+    }
+    if (!has_prefix(inner_field_names.back(), "anon"))
+      _heap_type.pads.push_back(0);
   }
   else
     _heap_type.field_types.push_back(empty_type2tc());

src/goto-symex/symex_assign.cpp

@@ -994,8 +994,13 @@ void goto_symext::replace_pointer_airth(expr2tc &expr)
 
     const struct_type2t &struct_type = to_struct_type(member.source_value->type);
 
-    expr2tc field = gen_ulong(struct_type.get_component_number(member.member));
-
+    unsigned int idx = struct_type.get_component_number(member.member);
+    unsigned int count_pad = 0;
+    for (unsigned int i = 0; i < idx; i++)
+      count_pad += has_prefix(struct_type.member_names[i], "anon");
+    idx -= count_pad;
+
+    expr2tc field = gen_ulong(idx);
     expr = field_of2tc(member.type, member.source_value, field);
   }
 }

src/irep2/irep2_type.cpp

@@ -192,7 +192,7 @@ unsigned int intheap_type2t::get_width() const
 bool intheap_type2t::do_alignment(const type2tc &type)
 {
   if (is_aligned) return false;
-  unsigned int access_sz = type->get_width();
+  int access_sz = type->get_width();
   if (access_sz % 8 != 0) access_sz = -1;
   else access_sz /= 8;
   if (access_sz == -1 || total_bytes % access_sz != 0)
@@ -203,7 +203,10 @@ bool intheap_type2t::do_alignment(const type2tc &type)
   unsigned int num_of_fields = total_bytes / access_sz;
   if (!field_types.empty()) field_types.clear();
   for (unsigned int i = 0; i < num_of_fields; i++)
+  {
     field_types.push_back(type);
+    pads.push_back(0);
+  }
   is_aligned = true;
   return true;
 }

src/irep2/irep2_type.h

@@ -226,6 +226,9 @@ class intheap_data : public type2t
   bool is_region;
   bool is_aligned;
   bool is_alloced;
+
+  // Hide
+  std::vector<unsigned int> pads;
 
   // Type mangling:
   typedef esbmct::field_traits<expr2tc, intheap_data, &intheap_data::location>

src/pointer-analysis/dereference.cpp

@@ -682,6 +682,8 @@ expr2tc dereferencet::build_reference_to(
     what->dump();
     log_debug("SLHV", "with type : ");
     type->dump();
+    log_debug("SLHV", "offset - {}", !is_nil_expr(lexical_offset));
+    if (!is_nil_expr(lexical_offset)) lexical_offset->dump();
     log_debug("SLHV", "|------------------------------------|");
   }
 
@@ -838,10 +840,6 @@ expr2tc dereferencet::build_reference_to(
   } else {
     value = object;
 
-    if (messaget::state.modules.count("SLHV") > 0 &&
-        !is_nil_expr(lexical_offset))
-      lexical_offset->dump();
-
     guardt tmp_guard(guard);
     if (!is_intheap_type(value) &&
         !is_pointer_type(value) &&
@@ -2564,7 +2562,7 @@ void dereferencet::check_heap_region_access(
       unsigned int _offset_bits = 0;
       // Get the highest bit
       for (unsigned int i = 0; i <= _field; i++)
-        _offset_bits += _type.field_types[i]->get_width();
+        _offset_bits += _type.field_types[i]->get_width() + _type.pads[i];
 
       expr2tc total_bits = gen_ulong(_type.total_bytes * 8);
       expr2tc offset_bits = gen_ulong(_offset_bits);
@@ -2725,8 +2723,24 @@ void dereferencet::set_intheap_type(expr2tc &heap_region, const type2tc &ty)
     const struct_type2t &_ty = to_struct_type(ty);
 
     _type.field_types.clear();
-    for (auto const &it : _ty.members)
-      _type.field_types.push_back(it);
+    const std::vector<type2tc> &inner_types = 
+      _ty.get_structure_members();
+    const std::vector<irep_idt> &inner_field_names =
+      _ty.get_structure_member_names();
+    _type.field_types.push_back(inner_types[0]);
+    for (unsigned int i = 1; i < inner_field_names.size(); i++)
+    {
+      const std::string &field_name = inner_field_names[i].as_string();
+      if (has_prefix(inner_field_names[i], "anon"))
+        _type.pads.push_back(inner_types[i]->get_width());
+      else
+      {  
+        _type.field_types.push_back(inner_types[i]);
+        _type.pads.push_back(0);
+      }
+    }
+    if (!has_prefix(inner_field_names.back(), "anon"))
+      _type.pads.push_back(0);
     _type.is_aligned = true;
     dereference_callback.update_heap_type(_type);
     return;

src/solvers/smt/smt_casts.cpp

@@ -650,10 +650,6 @@ smt_astt smt_convt::convert_typecast(const expr2tc &expr)
 {
   const typecast2t &cast = to_typecast2t(expr);
 
-  if (is_intloc_type(cast.from->type) && is_pointer_type(cast.type) ||
-      is_pointer_type(cast.from->type) && is_intloc_type(cast.type))
-    return convert_ast(cast.from);
-
   if (
     int_encoding && is_floatbv_type(cast.from->type) &&
     is_floatbv_type(cast.type))

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -163,6 +163,15 @@ smt_astt z3_slhv_convt::mk_locadd(smt_astt l, smt_astt o)
   );
 }
 
+smt_astt z3_slhv_convt::mk_loc2int(smt_astt l)
+{
+  assert(l->sort->id == SMT_SORT_INTLOC);
+//   return new_ast(
+//     z3::loc2int(to_solver_smt_ast<z3_smt_ast>(l)->a),
+//     this->mk_intloc_sort()
+//   );
+}
+
 BigInt z3_slhv_convt::get_bv(smt_astt a, bool is_signed)
 {
   log_error("SLHV does not support bv");
@@ -287,7 +296,7 @@ smt_astt z3_slhv_convt::convert_ast(const expr2tc &expr)
     }
     case expr2t::typecast_id:
     {
-      a = convert_typecast(expr);
+      a = convert_slhv_typecast(expr);
       break;
     }
     case expr2t::if_id:
@@ -633,6 +642,29 @@ z3_slhv_convt::convert_slhv_opts(
   }
 }
 
+smt_astt z3_slhv_convt::convert_slhv_typecast(const expr2tc &expr)
+{
+  if (!is_typecast2t(expr))
+  {
+    log_error("Wrong typecast expr");
+    expr->dump();
+    abort();
+  }
+
+  const typecast2t &cast = to_typecast2t(expr);
+
+  return convert_ast(cast.from);
+
+  smt_astt a = convert_ast(cast.from);
+
+  // TODO: add support loc2int
+  if ((is_pointer_type(cast.from->type) || is_intloc_type(cast.from->type)) &&
+      (is_signedbv_type(cast.type) || is_unsignedbv_type(cast.type)))
+    return mk_loc2int(a);
+
+  return a;
+}
+
 smt_astt z3_slhv_convt::project(const expr2tc &expr)
 {
   if (is_constant_intloc2t(expr))

src/solvers/z3-slhv/z3_slhv_conv.h

@@ -31,8 +31,9 @@ class z3_slhv_convt : public z3_convt {
     smt_astt mk_uplus(smt_astt ht1, smt_astt ht2);
     smt_astt mk_uplus(std::vector<smt_astt> hts);
     smt_astt mk_subh(smt_astt ht1, smt_astt ht2);
-    smt_astt mk_disjh(smt_astt ht1, smt_astt );
+    smt_astt mk_disjh(smt_astt ht1, smt_astt ht2);
     smt_astt mk_locadd(smt_astt l, smt_astt o);
+    smt_astt mk_loc2int(smt_astt l);
 
     // value obtaining from solver, not supported here
     BigInt get_bv(smt_astt a, bool is_signed) override;
@@ -55,6 +56,8 @@ class z3_slhv_convt : public z3_convt {
     void print_smt_formulae(std::ostream& dest);
 
     std::vector<smt_astt> assertions;
+
+    smt_astt convert_slhv_typecast(const expr2tc &expr);
 };
 
 #endif