fix offset for object field_of

benchmark/case_2.c

@@ -1,7 +1,7 @@
 #include <stdlib.h>
 typedef struct {
     void *lo;
-    int hi;
+    void *hi;
 } TData;
 
 int main(){
@@ -12,7 +12,7 @@ int main(){
     pdata->lo = malloc(16);
     pdata->hi = malloc(24);
     void *lo = pdata->lo;
-    int hi = pdata->hi;
+    void *hi = pdata->hi;
     if(lo == hi){
         free(lo);
         free(hi);

src/goto-symex/symex_assign.cpp

@@ -213,11 +213,6 @@ void goto_symext::symex_assign(
   replace_nondet(lhs);
   replace_nondet(rhs);
 
-  log_status("symex assign lhs : ------------- ");
-  lhs->dump();
-  log_status("symex assign rhs : ------------- ");
-  rhs->dump();
-
   intrinsic_races_check_dereference(lhs);
   log_status("dereference lhs write");
   dereference(lhs, dereferencet::WRITE);
@@ -229,7 +224,7 @@ void goto_symext::symex_assign(
   replace_dynamic_allocation(rhs);
   log_status("replace done");
 
-  log_status("after deref and replace : =-====");
+  log_status("after deref and replace -------------");
   lhs->dump();
   rhs->dump();
 
@@ -289,10 +284,6 @@ void goto_symext::symex_assign(
     }
   }
 
-  log_status("before symex assign rec : =-====");
-  lhs->dump();
-  rhs->dump();
-
   guardt g(guard); // NOT the state guard!
   symex_assign_rec(lhs, original_lhs, rhs, expr2tc(), g, hidden_ssa);
   log_status("xxxxxxxxxxxx symex assign: done for this step");
@@ -1104,10 +1095,16 @@ 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 inner_type : _type.get_structure_members())
+    const std::vector<type2tc> &inner_types = _type.get_structure_members();
+    const std::vector<irep_idt> &inner_field_names = _type.get_structure_member_names();
+    for (unsigned int i = 0; i < inner_field_names.size(); i++)
+    {
+      const std::string &field_name = inner_field_names[i].as_string();
+      if (field_name.find("anon_pad") != std::string::npos) continue;
       _heap_type.field_types.push_back(
-        is_pointer_type(inner_type) ? get_intloc_type() : get_int64_type()
+        is_pointer_type(inner_types[i]) ? get_intloc_type() : get_int64_type()
       );
+    }
   }
 
   return heap_type;
@@ -1141,8 +1138,6 @@ expr2tc goto_symext::create_heap_region(const sideeffect2t &effect, expr2tc &fla
   {
     expr2tc op = effect.operand;
     cur_state->rename(op);
-    log_status("malloc size:");
-    op->dump();
     do_simplify(op);
     if (!is_constant_int2t(op))
     {
@@ -1152,12 +1147,13 @@ expr2tc goto_symext::create_heap_region(const sideeffect2t &effect, expr2tc &fla
     bytes = to_constant_int2t(op).value.to_uint64();
   }
 
+  log_status("malloc size : {}", bytes);
+
   type2tc heap_type = create_heap_region_type(type, bytes, base_loc);
   flag->type = heap_type;
 
   log_status(" ======= create a heap region ========== ");
-
-  return heap_region2tc(heap_type, flag, base_loc);
+  return heap_region2tc(heap_type, base_loc);
 }
 
 void goto_symext::symex_nondet(const expr2tc &lhs, const expr2tc &effect)

src/goto-symex/symex_dereference.cpp

@@ -204,12 +204,6 @@ void symex_dereference_statet::update_heap_type_rec(
     if (to_symbol2t(_type.location).get_symbol_name() ==
         to_symbol2t(type.location).get_symbol_name())
       expr->type = intheap_type2tc(type);
-
-    if (is_heap_region2t(expr))
-    {
-      heap_region2t &heap_region = to_heap_region2t(expr);
-      update_heap_type_rec(heap_region.flag, type);
-    }
   }
   else
   {

src/irep2/irep2_expr.h

@@ -987,22 +987,18 @@ class heap_region_data : public expr2t
   heap_region_data(
     const type2tc &t,
     datatype_ops::expr_ids id,
-    const expr2tc &f,
-    const expr2tc &sl)
-    : expr2t(t, id), flag(f), source_location(sl)
+    const expr2tc &l)
+    : expr2t(t, id), source_location(l)
   {
   }
   heap_region_data(const heap_region_data& ref) = default;
 
-  expr2tc flag;
   expr2tc source_location;
 
   // Type mangling:
-  typedef esbmct::field_traits<expr2tc, heap_region_data, &heap_region_data::flag>
-    flag_field;
   typedef esbmct::field_traits<expr2tc, heap_region_data, &heap_region_data::source_location>
     source_location_field;
-  typedef esbmct::expr2t_traits<flag_field, source_location_field> traits;
+  typedef esbmct::expr2t_traits<source_location_field> traits;
 };
 
 class heap_ops : public expr2t
@@ -3220,9 +3216,8 @@ class heap_region2t : public heap_region_expr_methods
 public:
   heap_region2t(
     const type2tc &type,
-    const expr2tc &flag,
     const expr2tc &source_location)
-    : heap_region_expr_methods(type, heap_region_id, flag, source_location)
+    : heap_region_expr_methods(type, heap_region_id, source_location)
   {
   }
   heap_region2t(const heap_region2t &ref) = default;

src/irep2/templates/irep2_templates.cpp

@@ -169,7 +169,7 @@ std::string uplus2t::field_names[esbmct::num_type_fields] =
 std::string locadd2t::field_names[esbmct::num_type_fields] = 
   {"location", "offset", "", "", ""};
 std::string heap_region2t::field_names[esbmct::num_type_fields] = 
-  {"flag", "source_location", "", "", ""};
+  {"source_location", "", "", "", ""};
 std::string location_of2t::field_names[esbmct::num_type_fields] =
   {"source_region", "", "", "", ""};
 std::string field_of2t::field_names[esbmct::num_type_fields] =

src/irep2/templates/irep2_templates_expr_data.cpp

@@ -60,4 +60,4 @@ expr_typedefs3(extract, extract_data);
 expr_typedefs2(points_to, points_to_data);
 expr_typedefs1(uplus, uplus_data);
 expr_typedefs2(locadd, locadd_data);
-expr_typedefs3(heap_region, heap_region_data);
+expr_typedefs2(heap_region, heap_region_data);

src/pointer-analysis/dereference.cpp

@@ -141,8 +141,6 @@ const expr2tc &dereferencet::get_symbol(const expr2tc &expr)
 
 void dereferencet::dereference_expr(expr2tc &expr, guardt &guard, modet mode)
 {
-  log_status("deref expr:");
-  expr->dump();
   if (!has_dereference(expr))
     return;
 
@@ -158,8 +156,6 @@ void dereferencet::dereference_expr(expr2tc &expr, guardt &guard, modet mode)
     break;
   case expr2t::dereference_id:
   {
-    log_status("dereference expr: dereference id");
-    expr->dump();
     /* Interpret an actual dereference expression. First dereferences the
      * pointer expression, then dereferences the pointer itself, and stores the
      * result in 'expr'. */
@@ -363,8 +359,6 @@ expr2tc dereferencet::dereference_expr_nonscalar(
   modet mode,
   const expr2tc &base)
 {
-  log_status("deref expr nonscalar");
-  expr->dump();
   if (is_dereference2t(expr))
   {
     /* The first expression we're called with is index2t, member2t or non-scalar
@@ -487,16 +481,13 @@ expr2tc dereferencet::dereference(
     src = typecast2tc(pointer_type2tc(get_empty_type()), src);
 
   type2tc type = ns.follow(to_type);
-  log_status("dereference type:");
-  type->dump();
 
   // collect objects dest may point to
   value_setst::valuest points_to_set;
 
   log_status("---- value set for ");
   src->dump();
   dereference_callback.get_value_set(src, points_to_set);
-  log_status("---- value set: {} items", points_to_set.size());
   log_status("get value set done --------------------");
 
   /* If the value-set contains unknown or invalid, we cannot be sure it contains
@@ -806,10 +797,6 @@ expr2tc dereferencet::build_reference_to(
   } else {
     value = object;
 
-    log_status("before building pointer guard");
-    value->dump();
-    deref_expr->dump();
-    type->dump();
     if (!is_nil_expr(lexical_offset))
       lexical_offset->dump();
 
@@ -840,15 +827,10 @@ expr2tc dereferencet::build_reference_to(
     pointer_guard = same_object2tc(deref_expr, location_of2tc(value));
     tmp_guard.add(pointer_guard);
 
-    log_status("generated pointer guard:");
-    pointer_guard->dump();
-
     // Check that the object we're accessing is actually alive and valid for this
     // mode.
     valid_check(value, tmp_guard, mode);
 
-    log_status("finish checking");
-
     // Don't do anything further if we're freeing things
     if (is_free(mode))
       return expr2tc();
@@ -863,13 +845,9 @@ expr2tc dereferencet::build_reference_to(
     {
       if (is_locadd2t(deref_expr))
       {
-        log_status("get offset from locadd by renaming");
         expr2tc locadd = deref_expr;
         dereference_callback.rename(locadd);
         expr2tc off = to_locadd2t(locadd).get_offset();
-        off->dump();
-        log_status("after renaming");
-        off->dump();
         final_offset = to_locadd2t(off).get_offset();
       }
       else
@@ -886,9 +864,6 @@ expr2tc dereferencet::build_reference_to(
       final_offset = add2tc(final_offset->type, final_offset, lexical_offset);
     simplify(final_offset);
 
-    log_status("final offset : ");
-    final_offset->dump();
-
     if (!is_constant_int2t(final_offset) &&
         !is_symbol2t(final_offset))
     {
@@ -2281,9 +2256,6 @@ void dereferencet::valid_check(
   const guardt &guard,
   modet mode)
 {
-  log_status("entering valid check");
-  object->dump();
-
   const expr2tc &symbol = get_symbol(object);
 
   if (is_constant_string2t(symbol))
@@ -2303,11 +2275,7 @@ void dereferencet::valid_check(
   }
   else if(is_intheap_type(symbol))
   {
-    log_status("guard : ");
-    guard.dump();
     expr2tc not_valid_heap_region = not2tc(valid_object2tc(symbol));
-    log_status("not valid print:");
-    not_valid_heap_region->dump();
     guardt tmp_guard(guard);
     tmp_guard.add(not_valid_heap_region);
     std::string foo = is_free(mode) ?  "invalid free pointer"

src/pointer-analysis/value_set.cpp

@@ -626,10 +626,18 @@ void value_sett::get_value_set_rec(
   if (is_location_of2t(expr))
   {
     // TODO : maybe we should introduce reference
-    const location_of2t &loc_of = to_location_of2t(expr);
-    expr2tc new_obj = loc_of.source_heap;
-
-    insert(dest, new_obj, BigInt(0));
+    const location_of2t &locof = to_location_of2t(expr);
+    expr2tc new_obj = locof.source_heap;
+    BigInt off(0);
+
+    if (is_field_of2t(locof.source_heap))
+    {
+      const field_of2t &fieldof = to_field_of2t(locof.source_heap);
+      new_obj = fieldof.source_heap;
+      off = to_constant_int2t(fieldof.operand).value;
+    }
+
+    insert(dest, new_obj, off);
     return;
   }
 

src/solvers/smt/smt_casts.cpp

@@ -650,6 +650,10 @@ 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/smt/smt_conv.cpp

@@ -232,11 +232,6 @@ smt_astt smt_convt::convert_assign(const expr2tc &expr)
   smt_cache_entryt e = {eq.side_1, side2, ctx_level};
   smt_cache.insert(e);
 
-  log_status(" ----------------- assignment result ----------------- ");
-  side1->dump();
-  side2->dump();
-  log_status(" ----------------- assignment result ----------------- ");
-
   return side2;
 }
 
@@ -318,6 +313,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
   case expr2t::pointer_object_id:
   case expr2t::pointer_capability_id:
 
+  case expr2t::location_of_id:
   case expr2t::field_of_id:
   case expr2t::heap_region_id:
   case expr2t::heap_update_id:

src/solvers/smt/smt_conv.h

@@ -187,7 +187,7 @@ class smt_convt
    *
    *  @param expr The expression to convert into the SMT solver
    *  @return The resulting handle to the SMT value. */
-  smt_astt convert_ast(const expr2tc &expr);
+  virtual smt_astt convert_ast(const expr2tc &expr);
 
   /** Interface to specifig SMT conversion.
    *  Takes one expression, and converts it into the underlying SMT solver,
@@ -204,7 +204,7 @@ class smt_convt
     smt_astt const *args,
     struct expr_op_convert ops);
 
-  smt_astt convert_assign(const expr2tc &expr);
+  virtual smt_astt convert_assign(const expr2tc &expr);
 
   smt_astt make_n_ary_and(const ast_vec &v);
   smt_astt make_n_ary_or(const ast_vec &v);