update

src/goto-symex/dynamic_allocation.cpp

@@ -18,15 +18,31 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
   {
     /* alloc */
     // replace with CPROVER_alloc[POINTER_OBJECT(...)]
-    const valid_object2t &obj = to_valid_object2t(expr);
+    bool use_old_encoding = !options.get_bool_option("z3-slhv");
+    if(use_old_encoding) {
+      const valid_object2t &obj = to_valid_object2t(expr);
 
-    expr2tc obj_expr = pointer_object2tc(pointer_type2(), obj.value);
+      expr2tc obj_expr = pointer_object2tc(pointer_type2(), obj.value);
 
-    expr2tc alloc_arr_2;
-    migrate_expr(symbol_expr(*ns.lookup(valid_ptr_arr_name)), alloc_arr_2);
+      expr2tc alloc_arr_2;
+      migrate_expr(symbol_expr(*ns.lookup(valid_ptr_arr_name)), alloc_arr_2);
 
-    expr2tc index_expr = index2tc(get_bool_type(), alloc_arr_2, obj_expr);
-    expr = index_expr;
+      expr2tc index_expr = index2tc(get_bool_type(), alloc_arr_2, obj_expr);
+      expr = index_expr;
+
+    } else {
+      log_status("replace valid_object");
+      const valid_object2t &obj = to_valid_object2t(expr);
+      assert(is_pointer_with_region2t(obj.value));
+      const pointer_with_region2t& valid_inner = to_pointer_with_region2t(obj.value);
+      expr2tc alloc_size_heap_2;
+      log_status("before migrate");
+      migrate_expr(symbol_expr(*ns.lookup(alloc_size_heap_name)), alloc_size_heap_2);
+      log_status("migrate over");
+      expr2tc heap_contains = heap_contains2tc(get_bool_type(), alloc_size_heap_2, valid_inner.loc_ptr, 1);
+      expr = heap_contains;
+
+    }
   }
   else if (is_invalid_pointer2t(expr))
   {

src/goto-symex/symex_assign.cpp

@@ -111,6 +111,7 @@ goto_symext &goto_symext::operator=(const goto_symext &sym)
   valid_ptr_arr_name = sym.valid_ptr_arr_name;
   alloc_size_arr_name = sym.alloc_size_arr_name;
   dyn_info_arr_name = sym.dyn_info_arr_name;
+  alloc_size_heap_name = sym.alloc_size_heap_name;
 
   dynamic_memory = sym.dynamic_memory;
 
@@ -138,6 +139,33 @@ void goto_symext::symex_assign(
   log_status("xxxxxxxxxxxx symex assign: ");
 
   const code_assign2t &code = to_code_assign2t(code_assign);
+  expr2tc assign_target = code.target;
+  expr2tc assign_source = code.source;
+  bool use_old_encoding = !options.get_bool_option("z3-slhv");
+  if(!use_old_encoding) {
+    if(is_symbol2t(assign_target) &&
+       is_array_type(assign_target->type) && 
+       (to_symbol2t(assign_target).get_symbol_name().compare(valid_ptr_arr_name.as_string()) == 0 ||
+        to_symbol2t(assign_target).get_symbol_name().compare(dyn_info_arr_name.as_string()) == 0 ||
+        to_symbol2t(assign_target).get_symbol_name().compare(alloc_size_arr_name.as_string()) == 0)) {
+          if(
+              (to_symbol2t(assign_target).get_symbol_name().compare(alloc_size_arr_name.as_string()) == 0) && 
+              is_constant_array_of2t(assign_source)) {
+            // construct the initialization code of allocsize heap in slhv
+            // and do the symbolic execution for it
+            symbolt allocsize_heap;
+            allocsize_heap.name = alloc_size_heap_name;
+            allocsize_heap.id = alloc_size_heap_name;
+            allocsize_heap.lvalue = true;
+            allocsize_heap.type = typet(typet::t_intheap);
+            new_context.add(allocsize_heap);
+            expr2tc new_lhs = symbol2tc(get_intheap_type(),   allocsize_heap.id);
+            expr2tc new_rhs = constant_intheap2tc(get_intheap_type(), true);
+            symex_assign(code_assign2tc(new_lhs, new_rhs));
+          } 
+          return;
+        }
+  }
   code.dump();
   // Sanity check: if the target has zero size, then we've ended up assigning
   // to/from either a C++ POD class with no fields or an empty C struct or

src/goto-symex/symex_valid_object.cpp

@@ -25,8 +25,7 @@ void goto_symext::replace_dynamic_allocation(expr2tc &expr)
   if (is_nil_expr(expr))
     return;
 
-  log_status("replace dynamic allocation for: ");
-  expr->dump();
+  log_status("replace dynamic allocation");
   expr->Foreach_operand([this](expr2tc &e) { replace_dynamic_allocation(e); });
 
   if (is_valid_object2t(expr) || is_deallocated_obj2t(expr))

src/irep2/templates/irep2_templates_expr_data.cpp

@@ -2,6 +2,7 @@
 
 expr_typedefs1(constant_int, constant_int_data);
 expr_typedefs1(constant_intloc, constant_intloc_data);
+expr_typedefs2(constant_intheap, constant_intheap_data);
 expr_typedefs1(constant_fixedbv, constant_fixedbv_data);
 expr_typedefs1(constant_floatbv, constant_floatbv_data);
 expr_typedefs1(constant_struct, constant_datatype_data);

src/util/migrate.cpp

@@ -2031,6 +2031,25 @@ exprt migrate_expr_back(const expr2tc &ref)
     theexpr.set_value(integer2binary(ref2.value, width));
     return theexpr;
   }
+  case expr2t::constant_intloc_id:
+  {
+    const constant_intloc2t &ref2 = to_constant_intloc2t(ref);
+    typet thetype = migrate_type_back(ref->type);
+    constant_exprt theexpr(thetype);
+    unsigned int width = 8;
+    theexpr.set_value(integer2binary(ref2.value, width));
+    return theexpr;
+  }
+  case expr2t::constant_intheap_id:
+  {
+
+    const constant_intheap2t &ref2 = to_constant_intheap2t(ref);
+    typet thetype = migrate_type_back(ref->type);
+    constant_exprt theexpr(thetype);
+    bool is_emp = ref2.is_emp;
+    theexpr.set("is_emp", is_emp ? irep_idt("true") : irep_idt("false"));
+    return theexpr;
+  }
   case expr2t::constant_fixedbv_id:
   {
     return to_constant_fixedbv2t(ref).value.to_expr();

src/util/namespace.cpp

@@ -17,7 +17,8 @@ unsigned namespacet::get_max(const std::string &prefix) const
 
 const symbolt *namespacet::lookup(const irep_idt &name) const
 {
-  return context->find_symbol(name);
+  auto result = context->find_symbol(name);
+  return result;
 }
 
 void namespacet::follow_symbol(irept &irep) const