Merge branch 'slhv_encoding' of github.com:SpencerL-Y/esbmc into slhv…

…_encoding

src/goto-symex/slice.cpp

@@ -11,12 +11,16 @@ template <bool Add>
 bool symex_slicet::get_symbols(const expr2tc &expr)
 {
   bool res = false;
-  // Recursively look if any of the operands has a inner symbol
-  expr->foreach_operand([this, &res](const expr2tc &e) {
-    if (!is_nil_expr(e))
-      res |= get_symbols<Add>(e);
-    return res;
-  });
+  if (is_slhv_expr(expr)) {
+    res |= get_slhv_symbols<Add>(expr);
+  } else {
+    // Recursively look if any of the operands has a inner symbol
+    expr->foreach_operand([this, &res](const expr2tc &e) {
+      if (!is_nil_expr(e))
+        res |= get_symbols<Add>(e);
+      return res;
+    });
+  }
 
   if (!is_symbol2t(expr))
     return res;
@@ -29,6 +33,38 @@ bool symex_slicet::get_symbols(const expr2tc &expr)
   return res;
 }
 
+template <bool Add>
+bool symex_slicet::get_slhv_symbols(const expr2tc& expr)
+{
+  switch (expr->expr_id) {
+    case expr2t::constant_intheap_id:
+    case expr2t::constant_intloc_id:
+      return false; // TODO: right?
+    case expr2t::points_to_id:
+    case expr2t::uplus_id:
+    case expr2t::locadd_id:
+    case expr2t::heap_contains_id:
+    case expr2t::heap_load_id:
+    case expr2t::heap_append_id:
+    case expr2t::heap_update_id: {
+      bool res = false;
+      expr->foreach_operand([this, &res](const expr2tc &e) {
+        if (!is_nil_expr(e))
+          res |= get_symbols<Add>(e);
+        return res;
+      });
+      return res;
+    }
+    case expr2t::pointer_with_region_id: {
+      const pointer_with_region2t& pwr = to_pointer_with_region2t(expr);
+      return get_symbols<Add>(pwr.loc_ptr);
+    }
+    default:
+      log_error("Wrong SLHV expr");
+      abort();
+  }
+}
+
 void symex_slicet::run_on_assert(symex_target_equationt::SSA_stept &SSA_step)
 {
   get_symbols<true>(SSA_step.guard);
@@ -238,4 +274,4 @@ expr2tc symex_slicet::get_nondet_symbol(const expr2tc &expr)
   default:
     return expr2tc();
   }
-}
+}

src/goto-symex/slice.h

@@ -157,6 +157,17 @@ class symex_slicet : public slicer
   template <bool Add>
   bool get_symbols(const expr2tc &expr);
 
+  /**
+   * Recursively explores the operands of an SLHV expression.
+   * If a symbol is found, then it is added into the #depends
+   * member if `Add` is true, otherwise returns true.
+   *
+   * @param expr expression to extract every symbol
+   * @return true if at least one symbol was found
+   */
+  template <bool Add>
+  bool get_slhv_symbols(const expr2tc& expr);
+
   /**
    * Remove unneeded assumes from the formula
    *

src/irep2/irep2_utils.h

@@ -239,6 +239,20 @@ inline bool is_false(const expr2tc &expr)
   return false;
 }
 
+inline bool is_slhv_expr(const expr2tc& expr)
+{
+  return expr->expr_id == expr2t::constant_intheap_id ||
+         expr->expr_id == expr2t::constant_intloc_id ||
+         expr->expr_id == expr2t::pointer_with_region_id ||
+         expr->expr_id == expr2t::points_to_id ||
+         expr->expr_id == expr2t::uplus_id ||
+         expr->expr_id == expr2t::locadd_id ||
+         expr->expr_id == expr2t::heap_contains_id ||
+         expr->expr_id == expr2t::heap_load_id ||
+         expr->expr_id == expr2t::heap_update_id ||
+         expr->expr_id == expr2t::heap_append_id;
+}
+
 inline expr2tc gen_true_expr()
 {
   static expr2tc c = constant_bool2tc(true);

src/solvers/smt/smt_conv.cpp

@@ -340,7 +340,8 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
   case expr2t::locadd_id:
   case expr2t::heap_update_id:
   case expr2t::heap_load_id:
-  case expr2t::heap_contains_id: {
+  case expr2t::heap_contains_id:
+  case expr2t::heap_append_id: {
     a = convert_slhv_opts(expr, args); 
     break;
   }

src/solvers/z3-slhv/z3_slhv_conv.cpp

@@ -202,6 +202,16 @@ z3_slhv_convt::convert_slhv_opts(
       assert(args.size() == 2);
       return mk_locadd(args[0], args[1]);
     }
+    case expr2t::heap_append_id: {
+      const heap_append2t& heap_app = to_heap_append2t(expr);
+      // TODO : fix width
+      assert(heap_app.byte_len == 4);
+      smt_astt h = args[0];
+      smt_astt adr = args[1];
+      smt_astt val = args[2];
+      // new heap state
+      return mk_uplus(h, mk_pt(adr, val));
+    }
     case expr2t::heap_update_id: {
       const heap_update2t& heap_upd = to_heap_update2t(expr);
       // TODO : fix width

src/util/migrate.cpp

@@ -2646,6 +2646,17 @@ exprt migrate_expr_back(const expr2tc &ref)
     heap_load.set("byte_len", irep_idt(std::to_string(ref2.byte_len)));
     return heap_load;
   }
+  case expr2t::heap_append_id:
+  {
+    const heap_append2t &ref2 = to_heap_append2t(ref);
+    typet thetype = migrate_type_back(ref->type);
+    exprt heap_append("heap_append", thetype);
+    heap_append.copy_to_operands(migrate_expr_back(ref2.src_heap));
+    heap_append.copy_to_operands(migrate_expr_back(ref2.start_addr));
+    heap_append.copy_to_operands(migrate_expr_back(ref2.create_val));
+    heap_append.set("byte_len", irep_idt(std::to_string(ref2.byte_len)));
+    return heap_append;
+  }
   case expr2t::heap_update_id:
   {
     const heap_update2t &ref2 = to_heap_update2t(ref);