heap update encoding

src/esbmc/bmc.cpp

@@ -657,7 +657,7 @@ smt_convt::resultt bmct::run_thread(std::shared_ptr<symex_target_equationt> &eq)
         std::unique_ptr<smt_convt>(create_solver("", ns, options));
       log_status("smt_convt created");
       if (options.get_bool_option("z3-slhv")) {
-        // show_vcc(*eq);
+        show_vcc(*eq);
         generate_smt_from_equation(*runtime_solver, *eq);
         return smt_convt::P_SMTLIB;
       }

src/solvers/smt/smt_casts.cpp

@@ -403,7 +403,7 @@ smt_astt smt_convt::convert_typecast_to_ptr(const typecast2t &cast)
 {
   // First, sanity check -- typecast from one kind of a pointer to another kind
   // is a simple operation. Check for that first.
-  if (is_pointer_type(cast.from))
+  if (is_pointer_type(cast.from) || is_intloc_type(cast.from))
     return convert_ast(cast.from);
 
   // Unpleasentness; we don't know what pointer this integer is going to

src/solvers/smt/smt_conv.cpp

@@ -232,6 +232,11 @@ 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;
 }
 
@@ -315,6 +320,12 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
     unsigned int i = 0;
     expr->foreach_operand(
       [this, &args, &i](const expr2tc &e) { args[i++] = convert_ast(e); });
+    log_status(" -------------- convert args finished ------------ ");
+    for (int i = 0; i < expr->get_num_sub_exprs(); i++) {
+      args[i]->dump();
+    }
+    log_status(" -------------- convert args finished ------------ ");
+
   }
   }
 
@@ -339,6 +350,29 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
     a = mk_locadd(args[0], args[1]);
     break;
   }
+  case expr2t::heap_update_id: {
+    log_status("heap update");
+    const heap_update2t& heap_upd = to_heap_update2t(expr);
+    smt_astt h = args[0];
+    smt_astt h1 = mk_fresh(mk_intheap_sort(), mk_fresh_name("tmp_heap"));
+    smt_astt adr = args[1];
+    smt_astt val = args[2];
+    smt_astt v1 = mk_fresh(val->sort, mk_fresh_name("tmp_val"));
+    // old heap state
+    smt_astt o_state = mk_eq(h, mk_uplus(mk_pt(adr, v1), h1));
+    assert_ast(o_state);
+    // new heap state
+    a = mk_uplus(mk_pt(adr, val), h1);
+    break;
+  }
+  case expr2t::heap_load_id: {
+    log_status("TODO: heap load");
+    abort();
+  }
+  case expr2t::heap_contains_id: {
+    log_status("TODO: heap contains");
+    abort();
+  }
 
   case expr2t::constant_intheap_id:
   case expr2t::constant_intloc_id:
@@ -721,9 +755,12 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
   }
   case expr2t::same_object_id:
   {
+    const same_object2t& so = to_same_object2t(expr);
     // Two projects, then comparison.
-    args[0] = args[0]->project(this, 0);
-    args[1] = args[1]->project(this, 0);
+    if (this->solver_text() != "Z3-slhv") {
+      args[0] = args[0]->project(this, 0);
+      args[1] = args[1]->project(this, 0);
+    }
     a = mk_eq(args[0], args[1]);
     break;
   }
@@ -748,7 +785,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
       ptr = &to_typecast2t(*ptr).from;
 
     args[0] = convert_ast(*ptr);
-    a = args[0]->project(this, 0);
+    a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0);
     break;
   }
   case expr2t::pointer_capability_id:

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -3,8 +3,7 @@
 #include <solvers/smt/smt_conv.h>
 #include <z3_slhv_conv.h>
 
-
-#define new_ast new_solver_ast<z3_slhv_smt_ast>
+#define new_ast new_solver_ast<z3_smt_ast>
 
 smt_convt *create_new_z3_slhv_solver(
   const optionst &options,
@@ -43,22 +42,22 @@ smt_convt *create_new_z3_slhv_solver(
   return conv;
 }
 
-smt_astt z3_slhv_smt_ast::update(smt_convt *ctx,
-  smt_astt value,
-  unsigned int idx,
-  expr2tc idx_expr)
-  const {
-    log_status("slhv_smt does not support update");
-    return nullptr;
-  }
-smt_astt z3_slhv_smt_ast::project(smt_convt *ctx, unsigned int elem)const  {
-  log_status("slhv_smt does not support project");
-  return nullptr;
-}
-void z3_slhv_smt_ast::dump() const  {
-  std::string print_str = a.to_string();
-  log_status("{}\n sort is {}", print_str, a.get_sort().to_string());
-}
+// smt_astt z3_slhv_smt_ast::update(smt_convt *ctx,
+//   smt_astt value,
+//   unsigned int idx,
+//   expr2tc idx_expr)
+//   const {
+//     log_status("slhv_smt does not support update");
+//     return nullptr;
+//   }
+// smt_astt z3_slhv_smt_ast::project(smt_convt *ctx, unsigned int elem) const  {
+//   log_status("slhv_smt does not support project");
+//   return nullptr;
+// }
+// void z3_slhv_smt_ast::dump() const  {
+//   std::string print_str = a.to_string();
+//   log_status("{}\n sort is {}", print_str, a.get_sort().to_string());
+// }
 
 z3_slhv_convt::z3_slhv_convt(const namespacet &_ns, const optionst& _options) : z3_convt(_ns, _options) {
     // initialize the z3 based slhv converter here
@@ -192,15 +191,15 @@ const std::string z3_slhv_convt::solver_text() {
 // heap terms
 smt_astt z3_slhv_convt::mk_pt(smt_astt a, smt_astt b) {
   z3::expr pt = z3::points_to(
-    to_solver_smt_ast<z3_slhv_smt_ast>(a)->a,
-    to_solver_smt_ast<z3_slhv_smt_ast>(b)->a
+    to_solver_smt_ast<z3_smt_ast>(a)->a,
+    to_solver_smt_ast<z3_smt_ast>(b)->a
   );
   return new_ast(pt, this->mk_intheap_sort());
 }
 smt_astt z3_slhv_convt::mk_uplus(smt_astt a, smt_astt b){
   z3::expr h = z3::uplus(
-    to_solver_smt_ast<z3_slhv_smt_ast>(a)->a,
-    to_solver_smt_ast<z3_slhv_smt_ast>(b)->a
+    to_solver_smt_ast<z3_smt_ast>(a)->a,
+    to_solver_smt_ast<z3_smt_ast>(b)->a
   );
   return new_ast(h, this->mk_intheap_sort());
 }

src/solvers/z3-slhv/z3_slhv_conv.h

@@ -7,22 +7,22 @@
 #include <solvers/z3/z3_conv.h>
 #include <z3++.h>
 
-class z3_slhv_smt_ast : public solver_smt_ast<z3::expr>
-{
-public:
-  using solver_smt_ast<z3::expr>::solver_smt_ast;
-  ~z3_slhv_smt_ast() override = default;
-
-  smt_astt update(smt_convt *ctx,
-    smt_astt value,
-    unsigned int idx,
-    expr2tc idx_expr)
-    const override;
-
-  smt_astt project(smt_convt *ctx, unsigned int elem) const override;
-
-  void dump() const override;
-};
+// class z3_slhv_smt_ast : public solver_smt_ast<z3::expr>
+// {
+// public:
+//   using solver_smt_ast<z3::expr>::solver_smt_ast;
+//   ~z3_slhv_smt_ast() override = default;
+
+//   smt_astt update(smt_convt *ctx,
+//     smt_astt value,
+//     unsigned int idx,
+//     expr2tc idx_expr)
+//     const override;
+
+//   smt_astt project(smt_convt *ctx, unsigned int elem) const override;
+
+//   void dump() const override;
+// };
 
 class z3_slhv_convt : public z3_convt {
 public: