Skip to content

Commit

Permalink
fix build deref for a whole region and fix project for field_of
Browse files Browse the repository at this point in the history
  • Loading branch information
@zhuyutian57
zhuyutian57 committed Sep 5, 2024
1 parent 5a12ee7 commit cc9210b
Show file tree
Hide file tree
Showing 6 changed files with 58 additions and 72 deletions.
8 changes: 4 additions & 4 deletions benchmark/case_3.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@


int main(){
int num = 5;
int *j = (int*)malloc(num*sizeof(int));
*(j+6) = num + (-1);
free(j);
int **p = malloc(sizeof(int*));
*p = malloc(sizeof(int));
free(*p);
free(p);
}
7 changes: 4 additions & 3 deletions src/goto-symex/symex_target_equation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,9 +169,10 @@ void symex_target_equationt::convert_internal_step(
step.dump();
log_status(" ============================== step ======================== ");

log_status("convert step guard ast: ");
step.guard_ast = smt_conv.convert_ast(step.guard);
step.guard_ast->dump();
// log_status("convert step guard ast: ");
// guard_ast is used for generating witness
// not used now
// step.guard_ast = smt_conv.convert_ast(step.guard);

if (step.is_assume() || step.is_assert())
{
Expand Down
18 changes: 10 additions & 8 deletions src/pointer-analysis/dereference.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -532,12 +532,12 @@ expr2tc dereferencet::dereference(

if (is_nil_expr(new_value))
continue;

log_status("after building reference to : not nill");
new_value->dump();

assert(!is_nil_expr(pointer_guard));

new_value->dump();
type->dump();

if (!dereference_type_compare(new_value, type))
{
guardt new_guard(guard);
Expand Down Expand Up @@ -915,6 +915,7 @@ expr2tc dereferencet::build_reference_to(
// to have a reference built at all.
if (is_internal(mode))
{
log_status("collect objects for doing free");
dereference_callbackt::internal_item internal;
internal.object = value;
internal.offset = final_offset; // offset for SLHV
Expand Down Expand Up @@ -1274,10 +1275,8 @@ void dereferencet::build_deref_slhv(
log_error("heap region must be aligned");
abort();
}

// heap region as a value
if (field == 0 && access_sz == _type.total_bytes) return;

bool is_field = true;
if (field >= _type.field_types.size() ||
access_sz != _type.total_bytes / _type.field_types.size())
{
Expand All @@ -1286,15 +1285,18 @@ void dereferencet::build_deref_slhv(
type,
dereference_callback.get_nondet_id("undefined_behavior_var"));
value = sym;
return;
is_field = false;
}
else
value = field_of2tc(type, value, gen_ulong(field));

// update field type
if (_type.set_field_type(field, type))
if (is_field && _type.set_field_type(field, type))
dereference_callback.update_heap_type(_type);

log_status("return dereference --->");
value->dump();

log_status(" ----------------- build deref slhv ----------------- ");
}

Expand Down
19 changes: 11 additions & 8 deletions src/solvers/smt/smt_conv.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,6 +252,8 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
return (cache_result->ast);
}

bool use_old_encoding = !options.get_bool_option("z3-slhv");

/* Vectors!
*
* Here we need special attention for Vectors, because of the way
Expand All @@ -262,7 +264,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
* for some reason we would like to run ESBMC without simplifications
* then we need to apply it here.
*/
if (!options.get_bool_option("z3-slhv") && is_vector_type(expr))
if (use_old_encoding && is_vector_type(expr))
{
if (is_neg2t(expr))
{
Expand Down Expand Up @@ -317,12 +319,15 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
case expr2t::pointer_capability_id:

case expr2t::field_of_id:
case expr2t::heap_region_id:
case expr2t::heap_update_id:
case expr2t::heap_delete_id:
break; // Don't convert their operands

default:
{
if (is_same_object2t(expr) && !use_old_encoding) break;

// Convert all the arguments and store them in 'args'.
unsigned int i = 0;
expr->foreach_operand(
Expand Down Expand Up @@ -365,8 +370,6 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
case expr2t::symbol_id:
{
a = convert_terminal(expr);
log_status("convert_terminal result: ");
a->dump();
break;
}
case expr2t::constant_string_id:
Expand Down Expand Up @@ -455,7 +458,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
is_pointer_type(expr->type) || is_pointer_type(add.side_1) ||
is_pointer_type(add.side_2))
{
a = this->solver_text() == "Z3-slhv" ?
a = !use_old_encoding ?
convert_slhv_opts(expr, args) :
convert_pointer_arith(expr, expr->type);
}
Expand All @@ -476,7 +479,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
is_pointer_type(expr->type) || is_pointer_type(sub.side_1) ||
is_pointer_type(sub.side_2))
{
a = this->solver_text() == "Z3-slhv" ?
a = !use_old_encoding ?
convert_slhv_opts(expr, args) :
convert_pointer_arith(expr, expr->type);
}
Expand Down Expand Up @@ -742,7 +745,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
{
const same_object2t& so = to_same_object2t(expr);
// Two projects, then comparison.
if (this->solver_text() != "Z3-slhv") {
if (use_old_encoding) {
args[0] = args[0]->project(this, 0);
args[1] = args[1]->project(this, 0);
a = mk_eq(args[0], args[1]);
Expand All @@ -760,7 +763,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
ptr = &to_typecast2t(*ptr).from;

args[0] = convert_ast(*ptr);
a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0);
a = !use_old_encoding ? args[0] : args[0]->project(this, 0);
break;
}
case expr2t::pointer_object_id:
Expand All @@ -772,7 +775,7 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
ptr = &to_typecast2t(*ptr).from;

args[0] = convert_ast(*ptr);
a = this->solver_text() == "Z3-slhv" ? args[0] : args[0]->project(this, 0);
a = !use_old_encoding ? args[0] : args[0]->project(this, 0);
break;
}
case expr2t::pointer_capability_id:
Expand Down
74 changes: 29 additions & 45 deletions src/solvers/z3-slhv/z3_slhv_conv.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,13 +206,15 @@ z3_slhv_convt::convert_slhv_opts(
case expr2t::heap_region_id:
{
const intheap_type2t &_type = to_intheap_type(expr->type);

smt_astt base_loc = convert_ast(_type.location);

std::vector<smt_astt> pt_vec;
if (_type.is_aligned)
{
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_astt loc = i == 0 ? base_loc : mk_locadd(base_loc, mk_smt_int(BigInt(i)));
smt_sortt sort =
is_intloc_type(_type.field_types[i]) ?
mk_intloc_sort() : mk_int_sort();
Expand All @@ -229,7 +231,7 @@ z3_slhv_convt::convert_slhv_opts(
// Default sort is intloc
pt_vec.push_back(
mk_pt(
args[1],
base_loc,
mk_fresh(mk_intloc_sort(), mk_fresh_name("tmp_loc::")
)
)
Expand Down Expand Up @@ -289,43 +291,12 @@ z3_slhv_convt::convert_slhv_opts(
}
return mk_subh(args[1], args[0]);
}
case expr2t::field_of_id:
case expr2t::heap_update_id:
case expr2t::heap_delete_id:
{
z3_slhv_convt::smt_ast_pair sap = convert_opt_without_assert(expr);
assert_ast(sap.first);
return sap.second;
}
case expr2t::same_object_id:
{
// Do project for SLHV
const same_object2t& same = to_same_object2t(expr);
smt_astt p1 = this->project(same.side_1);
smt_astt p2 = this->project(same.side_2);
smt_astt eq = mk_eq(p1, p2);
return eq;
}
default: {
log_status("Invalid SLHV operations!!!");
abort();
}
}
}

z3_slhv_convt::smt_ast_pair
z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)
{
switch (expr->expr_id)
{
case expr2t::field_of_id:
{
const field_of2t &field_of = to_field_of2t(expr);

if (is_constant_intheap2t(field_of.source_heap))
return std::make_pair(
mk_smt_bool(true),
mk_fresh(convert_sort(field_of.type), mk_fresh_name("invalid_loc_")));
return mk_fresh(convert_sort(field_of.type), mk_fresh_name("invalid_fieldof_"));

if (!is_constant_int2t(field_of.operand))
{
Expand Down Expand Up @@ -357,8 +328,8 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)
}
smt_astt v1 = mk_fresh(s1, name);

smt_astt assert_expr = mk_subh(mk_pt(loc, v1), convert_ast(heap_region));
return std::make_pair(assert_expr, v1);
assert_ast(mk_subh(mk_pt(loc, v1), convert_ast(heap_region)));
return v1;
}
case expr2t::heap_update_id:
{
Expand Down Expand Up @@ -387,13 +358,11 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)

// current heap state
smt_astt old_state = mk_uplus(h1, mk_pt(loc, v1));
smt_astt assert_expr = mk_eq(h, old_state);
assert_ast(mk_eq(h, old_state));

// new heap state
smt_astt new_state = mk_uplus(h1, mk_pt(loc, val));

// new heap state
return std::make_pair(assert_expr, new_state);
return new_state;
}
case expr2t::heap_delete_id:
{
Expand All @@ -404,12 +373,22 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)

smt_astt h1 = mk_fresh(mk_intheap_sort(), mk_fresh_name("tmp_heap::"));
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, h1);
assert_ast(mk_eq(h, mk_uplus(h1, mk_pt(l, v1))));
return h1;
}
case expr2t::same_object_id:
{
// Do project for SLHV
const same_object2t& same = to_same_object2t(expr);
smt_astt p1 = this->project(same.side_1);
smt_astt p2 = this->project(same.side_2);
smt_astt eq = mk_eq(p1, p2);
return eq;
}
default: {
return std::make_pair(mk_smt_bool(true), convert_ast(expr));
log_status("Invalid SLHV operations!!!");
abort();
}
}
}
Expand All @@ -423,12 +402,17 @@ smt_astt z3_slhv_convt::project(const expr2tc &expr)
const intheap_type2t &_type = to_intheap_type(expr->type);
return this->project(_type.location);
}
return convert_opt_without_assert(expr).second;

if (is_intloc_type(expr) || is_pointer_type(expr))
return convert_ast(expr);

log_error("Wrong symbol for projection");
expr->dump();
}
else if (is_location_of2t(expr))
return this->project(to_location_of2t(expr).source_heap);
else if (is_field_of2t(expr))
return convert_opt_without_assert(expr).second;
return convert_ast(expr);
else if (is_typecast2t(expr))
return this->project(to_typecast2t(expr).from);
else if (is_locadd2t(expr))
Expand Down
4 changes: 0 additions & 4 deletions src/solvers/z3-slhv/z3_slhv_conv.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,10 +42,6 @@ class z3_slhv_convt : public z3_convt {
smt_astt
convert_slhv_opts(const expr2tc &expr, const std::vector<smt_astt>& args) override;

typedef std::pair<smt_astt, smt_astt> smt_ast_pair;

smt_ast_pair convert_opt_without_assert(const expr2tc &expr);

smt_astt project(const expr2tc &expr);

void dump_smt() override;
Expand Down

0 comments on commit cc9210b

Please sign in to comment.