turn pointer arithmetic to locadd

src/esbmc/show_vcc.cpp

@@ -61,7 +61,7 @@ void bmct::show_vcc(const symex_target_equationt &eq)
   }
   else
   {
-    std::ofstream out(filename.c_str());
+    std::ofstream out(filename.c_str(), std::ios_base::app);
     if (!out)
       log_error("failed to open {}", filename);
     else

src/goto-symex/builtin_functions.cpp

@@ -268,8 +268,7 @@ expr2tc goto_symext::symex_mem(
     else
     {
       expr2tc bytes = size;
-      if (!is_constant_int2t(bytes)) 
-        bytes = bytes->simplify();
+      do_simplify(bytes);
       if (is_constant_int2t(bytes))
       {
         heap_type = get_intheap_type(to_constant_int2t(bytes).value.to_uint64());

src/goto-symex/symex_assign.cpp

@@ -137,6 +137,7 @@ void goto_symext::symex_assign(
   const guardt &guard)
 {
   log_status("xxxxxxxxxxxx symex assign: ");
+  code_assign->dump();
 
   const code_assign2t &code = to_code_assign2t(code_assign);
   expr2tc assign_target = code.target;
@@ -188,6 +189,13 @@ void goto_symext::symex_assign(
   {
     replace_null(lhs);
     replace_null(rhs);
+
+    log_status("here");
+
+    replace_by_locadd(lhs);
+    log_status("here");
+    replace_by_locadd(rhs);
+    log_status("here");
   }
 
   log_status("symex assign lhs : ------------- ");
@@ -948,4 +956,35 @@ void goto_symext::replace_null(expr2tc &expr)
         replace_null(e);
     });
   }
+}
+
+void goto_symext::replace_by_locadd(expr2tc &expr)
+{
+  if (is_nil_expr(expr)) return;
+
+  expr->Foreach_operand([this](expr2tc &e) { replace_by_locadd(e); });
+
+  if (is_add2t(expr) || is_sub2t(expr))
+  {
+    expr2tc side_1 = is_add2t(expr) ? to_add2t(expr).side_1 : to_sub2t(expr).side_1;
+    expr2tc side_2 = is_add2t(expr) ? to_add2t(expr).side_2 : to_sub2t(expr).side_2;
+
+    if (is_pointer_type(side_2) || is_intloc_type(side_2))
+      std::swap(side_1, side_2);
+
+    if (is_pointer_type(side_2) || is_intloc_type(side_2))
+    {
+      log_error("Wrong pointer arithmetic");
+      abort();
+    }
+
+    if (is_sub2t(expr)) side_2 = neg2tc(side_2->type, side_2);
+
+    expr2tc locadd = locadd2tc(side_1, side_2);
+    do_simplify(locadd);
+
+    locadd->dump();
+
+    expr = locadd;
+  }
 }

src/irep2/irep2_expr.cpp

@@ -439,60 +439,6 @@ void with2t::assert_consistency() const
   assert(type == source_value->type);
 }
 
-// bool heap_region2t::update(uint byte_len)
-// {
-//   uint old_bytes = to_constant_int2t(field_bytes).value.to_uint64();
-//   uint old_size = to_constant_int2t(size).value.to_uint64();
-
-//   assert(old_bytes * old_size % byte_len == 0);
-//   // TODO: allow to split only one time
-//   if (is_aligned) {
-//     assert(byte_len == old_bytes);
-//     return false;
-//   }
-
-//   uint new_bytes = byte_len;
-//   uint new_size;
-//   if (byte_len != old_bytes)
-//   {
-//     new_size = old_bytes * old_size / byte_len;
-//     is_aligned = true;
-//     field_bytes = constant_int2tc(get_uint64_type(), BigInt(new_bytes));
-//     size = constant_int2tc(get_uint64_type(), BigInt(new_size));
-//     return true;
-//   }
-//   return false;
-// }
-
-// std::string locadd2t::offset_as_string() const
-// {
-//   if (is_symbol2t(offset))
-//     return to_symbol2t(offset).get_symbol_name();
-//   else if (is_neg2t(offset))
-//   {
-//     neg2t off = to_neg2t(offset);
-//     expr2tc val = off.value.simplify();
-//     if (!is_constant_int2t(val))
-//     {
-//       log_error("Doe no support for offset_as_string of neg");
-//       abort();
-//     }
-//     return std::string("-")
-//       + std::to_string(to_constant_int2t(val).value.to_int64());
-//   }
-//   else
-//   {
-//     expr2tc off = offset;
-//     if (!is_constant_int2t(off)) off = off.simplify();
-//     if (!is_constant_int2t(off))
-//     {
-//       log_error("Doe no support for offset_as_string");
-//       abort();
-//     }
-//     return std::to_string(to_constant_int2t(off).value.to_int64());
-//   }
-// }
-
 const expr2tc &object_descriptor2t::get_root_object() const
 {
   const expr2tc *tmp = &object;
@@ -540,3 +486,18 @@ arith_2ops::arith_2ops(
   // TODO: Add consistency checks for vectors
 #endif
 }
+
+expr2tc locadd2t::get_base_location() const
+{
+  if (is_locadd2t(location))
+    return to_locadd2t(location).get_base_location();
+  return location;
+}
+
+expr2tc locadd2t::get_offset() const
+{
+  expr2tc off = offset;
+  if (is_locadd2t(location))
+    off = add2tc(off->type, off, to_locadd2t(location).get_offset());
+  return off;
+}

src/irep2/irep2_expr.h

@@ -3277,6 +3277,11 @@ class locadd2t : public locadd_expr_methods
   }
   locadd2t(const locadd2t &ref) = default;
 
+  expr2tc do_simplify() const override;
+
+  expr2tc get_base_location() const;
+  expr2tc get_offset() const;
+
   static std::string field_names[esbmct::num_type_fields];
 };
 
@@ -3292,8 +3297,6 @@ class heap_region2t : public heap_region_expr_methods
   }
   heap_region2t(const heap_region2t &ref) = default;
 
-  // bool update(uint byte_len);
-
   static std::string field_names[esbmct::num_type_fields];
 };
 

src/irep2/irep2_type.h

@@ -400,6 +400,8 @@ class intheap_type2t : public intheap_type_methods
     bool is_aligned)
     : intheap_type_methods(intheap_id, field_types, total_bytes, is_region, is_aligned)
   {
+    if (is_region && this->field_types.empty())
+      this->field_types.push_back(empty_type2tc());
   }
   intheap_type2t(const intheap_type2t &ref) = default;
   unsigned int get_width() const override;

src/pointer-analysis/dereference.cpp

@@ -500,13 +500,30 @@ expr2tc dereferencet::dereference(
   expr2tc value;
   if (!known_exhaustive)
     value = make_failed_symbol(type);
+
+  // TODO : fix
+  // Extract base location ad offset from locadd
+  expr2tc new_src = src;
+  expr2tc offset = lexical_offset;
+  if (is_locadd2t(src))
+  {
+    new_src = to_locadd2t(src).get_base_location();
+    expr2tc off_from_src = to_locadd2t(src).get_offset();
+    if (is_nil_expr(offset))
+      offset = off_from_src;
+    else
+      offset = add2tc(offset->type, offset, off_from_src);
+    expr2tc simp = offset->simplify();
+    if (!is_nil_expr(simp))
+      offset = simp;
+  }
 
   for (const expr2tc &target : points_to_set)
   {
     expr2tc new_value, pointer_guard;
 
     new_value = build_reference_to(
-      target, mode, src, type, guard, lexical_offset, pointer_guard);
+      target, mode, new_src, type, guard, offset, pointer_guard);
 
     if (is_nil_expr(new_value))
       continue;
@@ -809,6 +826,8 @@ expr2tc dereferencet::build_reference_to(
     value->dump();
     deref_expr->dump();
     type->dump();
+    if (!is_nil_expr(lexical_offset))
+      lexical_offset->dump();
 
     guardt tmp_guard(guard);
     if (is_heap_region2t(value))
@@ -898,11 +917,15 @@ expr2tc dereferencet::build_reference_to(
     }
     else
     {
+      log_status("set final offset");
+      final_offset->dump();
       if (!is_nil_expr(lexical_offset))
         final_offset = add2tc(final_offset->type, final_offset, lexical_offset);
 
-      if (!is_constant_int2t(final_offset))
-        final_offset = final_offset.simplify();
+      expr2tc simp = final_offset->simplify();
+      if (!is_nil_expr(simp)) final_offset = simp;
+
+      final_offset->dump();
     }
 
     // If we're in internal mode, collect all of our data into one struct, insert
@@ -1274,6 +1297,7 @@ void dereferencet::build_reference_slhv(
   if(is_scalar_type(type)) {
     if (!is_constant_int2t(offset))
     {
+      // TODO : support
       log_error("Do not support non-constant offset");
       abort();
     }
@@ -1282,7 +1306,15 @@ void dereferencet::build_reference_slhv(
     heap_region2t& heap_region = to_heap_region2t(value);
 
     intheap_type2t &_type = to_intheap_type(heap_region.type);
-    if (_type.set_field_type(field, type))
+    if (field >= _type.field_types.size())
+    {
+      expr2tc sym = symbol2tc(
+        type, 
+        dereference_callback.get_nondet_id("undefined_behavior_var"));
+      value = sym;
+      return;
+    }
+    else if (_type.set_field_type(field, type))
     {
       heap_region.flag->type = heap_region.type;
       dereference_callback.update_heap_type(heap_region.flag);

src/pointer-analysis/value_set.cpp

@@ -581,10 +581,23 @@ void value_sett::get_value_set_rec(
 
   if (is_locadd2t(expr))
   {
-    const locadd2t& locadd = to_locadd2t(expr);
-    assert(is_intloc_type(locadd.location));
-    abort();
-    // TODO
+    expr2tc simp = expr;
+
+    if (!is_symbol2t(to_locadd2t(simp).location) ||
+        !is_constant_int2t(to_locadd2t(simp).offset))
+      simp = simp->simplify();
+
+    if (!is_symbol2t(to_locadd2t(simp).location) ||
+        !is_constant_int2t(to_locadd2t(simp).offset))
+    {
+      log_error("Do not support dynamic pointer arithmetic");
+      abort();
+    }
+
+    const locadd2t &locadd = to_locadd2t(simp);
+
+    get_value_set_rec(locadd.location, dest, suffix, original_type);
+    return;
   }
 
   if (is_locationof2t(expr))

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -201,19 +201,20 @@ z3_slhv_convt::convert_slhv_opts(
       return mk_nil();
     case expr2t::heap_region_id:
     {
-      const intheap_type2t &type = to_intheap_type(expr->type);
+      const intheap_type2t &_type = to_intheap_type(expr->type);
 
       std::vector<smt_astt> pt_vec;
-      if (type.is_aligned)
+      if (_type.is_aligned)
       {
-        for (unsigned i = 0; i < type.field_types.size(); i++) {
+        for (unsigned i = 0; i < _type.field_types.size(); i++)
+        {
           smt_astt loc = i == 0 ? args[1] : mk_locadd(args[1], mk_smt_int(BigInt(i)));
           smt_sortt sort =
-            is_intloc_type(type.field_types[i]) ?
+            is_intloc_type(_type.field_types[i]) ?
               mk_intloc_sort() : mk_int_sort();
           std::string name =
             mk_fresh_name(
-              is_intloc_type(type.field_types[i]) ?
+              is_intloc_type(_type.field_types[i]) ?
                 "tmp_loc::" : "tmp_val::");
           smt_astt v = mk_fresh(sort, name);
           pt_vec.push_back(mk_pt(loc, v));
@@ -399,7 +400,7 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)
       smt_astt v1 = mk_fresh(mk_int_sort(), mk_fresh_name("tmp_val::"));
       smt_astt assert_expr = mk_eq(h, mk_uplus(h1, mk_pt(l, v1)));
 
-      return std::make_pair(assert_expr, v1);
+      return std::make_pair(assert_expr, h1);
     }
     default: {
       return std::make_pair(mk_smt_bool(true), convert_ast(expr));

src/util/simplify_expr2.cpp

@@ -1060,6 +1060,27 @@ expr2tc index2t::do_simplify() const
   return expr2tc();
 }
 
+expr2tc locadd2t::do_simplify() const
+{
+  expr2tc src_loc = location;
+  expr2tc off = offset;
+
+  while(is_locadd2t(src_loc))
+  {
+    off = add2tc(off->type, off, to_locadd2t(src_loc).offset);
+    src_loc = to_locadd2t(src_loc).location;
+  }
+
+  if (!is_constant_int2t(off))
+    off = off->simplify();
+
+  if (src_loc != location &&
+      off != offset && !is_nil_expr(off))
+    return locadd2tc(src_loc, off);
+
+  return expr2tc();
+}
+
 expr2tc not2t::do_simplify() const
 {
   expr2tc simp = try_simplification(value);