Skip to content

Commit

Permalink
turn all form of pointer arithmetic to locadd
Browse files Browse the repository at this point in the history
  • Loading branch information
@zhuyutian57
zhuyutian57 committed Aug 19, 2024
1 parent a02f264 commit fbd6603
Show file tree
Hide file tree
Showing 15 changed files with 172 additions and 247 deletions.
34 changes: 4 additions & 30 deletions benchmark/case_0.c
View file
Original file line number Diff line number Diff line change
@@ -1,41 +1,15 @@
#include <stdlib.h>


// typedef struct {
// int data;
// int* next;
// } node_t;
typedef struct {
void* lo;
void* hi;
} TData;
int main(){
// node_t node;
// node.data = 10;
// node.next = malloc(sizeof(int));
// node_t* t = (node_t*)malloc(sizeof(node_t));
// t->data = 10;
// int whatever;
// int * data = malloc(sizeof(int));
// int * data2 = malloc(2*sizeof(int));
// free(data);
// int i = *(data);
int * data = malloc(sizeof(int));
int * data2 = malloc(2*sizeof(int));
free(data2);
int i = *(data + 1);
// int* j = NULL;
// int* i = j;
// // *(data + 1) = whatever;
// int n = *(data+1);
// if(i > 0) {
// free(data);
// }
TData *p1 = malloc(sizeof(TData));
p1->lo = malloc(12);
p1->hi = malloc(12);
void *p2;
int x;
if(x) {
p2 = p1->hi;
} else {
p2 = p1->lo;
}
free(p2);
}
54 changes: 26 additions & 28 deletions src/goto-symex/builtin_functions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -284,64 +284,62 @@ expr2tc goto_symext::symex_mem(

symbol.type.dynamic(true);
symbol.mode = "C";
log_status("new_context.add(symbol);");
new_context.add(symbol);

expr2tc lhs_flag;
if (is_symbol2t(lhs))
lhs_flag = lhs;
else if (is_heap_load2t(lhs))
lhs_flag = to_heap_load2t(lhs).flag;
else
{
log_error("Do not support this expr");
abort();
}

expr2tc rhs_heap = symbol2tc(get_intheap_type(), symbol.id);
guardt rhs_guard = cur_state->guard;

std::string rhs_base_id = to_symbol2t(lhs_flag).get_symbol_name();
expr2tc rhs_base_addr = symbol2tc(get_intloc_type(), rhs_base_id);
// set a location for new heap region
symbolt heap_region_loc;
heap_region_loc.name = "heap_region_loc_"+ i2string(dynamic_counter);

heap_region_loc.id = std::string("symex_dynamic::") + id2string(heap_region_loc.name);
heap_region_loc.lvalue = true;

heap_region_loc.type = typet(typet::t_intheap);

heap_region_loc.mode = "C";
new_context.add(heap_region_loc);

expr2tc rhs_base_loc = symbol2tc(get_intloc_type(), heap_region_loc.id);
cur_state->rename(rhs_base_loc);

expr2tc rhs_heap_region_flag = symbol2tc(get_intheap_type(), symbol.id);
expr2tc rhs_region =
heap_region2tc(
rhs_heap_region_flag,
rhs_base_addr,
rhs_heap,
rhs_base_loc,
region_pt_bytes,
region_size,
size != 1
);

log_status("symex assign in symex_mem: allocated_heap = heaplet");
symex_assign(code_assign2tc(rhs_heap, rhs_region));

log_status("create valueset base addr symbol and assign");
cur_state->rename(rhs_base_addr);
expr2tc pwr = pointer_with_region2tc(rhs_base_addr, rhs_heap);
symex_assign(code_assign2tc(lhs_flag, pwr));

// TODO: modify the pointer object here, maybe to wrap the intloc symbol directly
expr2tc ptr_obj =
pointer_object2tc(get_intloc_type(), to_pointer_with_region2t(pwr).loc_ptr);
// link pointer variable and heap variable
expr2tc pwr = pointer_with_region2tc(rhs_base_loc, rhs_heap);
track_new_pointer(
ptr_obj,
rhs_base_loc,
get_intheap_type(),
gen_ulong(total_bytes));
cur_state->rename(rhs_heap);

dynamic_memory.emplace_back(
rhs_heap,
rhs_guard,
!is_malloc,
symbol.name.as_string()
);

log_status("create valueset base loc symbol and assign");
if (is_heap_load2t(lhs))
{
guardt g;
symex_assign_heap_load(lhs, lhs, pwr, pwr, g, false);
}
else
{
symex_assign(code_assign2tc(lhs, pwr));
}
return expr2tc();
}
}
Expand Down
6 changes: 6 additions & 0 deletions src/goto-symex/goto_symex.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -806,6 +806,12 @@ class goto_symext
*/
void replace_null(expr2tc &expr);

/**
* Replace member, indexof ... by locadd
* @param expr Expr to a location.
*/
void replace_by_locadd(expr2tc &expr);

/**
* Fetch reference to global dynamic object counter.
* @return Reference to global dynamic object counter.
Expand Down
7 changes: 0 additions & 7 deletions src/goto-symex/goto_symex_state.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,13 +288,6 @@ void goto_symex_statet::rename(expr2tc &expr)
if (is_pointer_with_region2t(hr.start_loc))
hr.start_loc = to_pointer_with_region2t(hr.start_loc).loc_ptr;
}

if (is_heap_load2t(expr))
{
heap_load2t &hl = to_heap_load2t(expr);
if (is_pointer_with_region2t(hl.flag))
hl.flag = to_pointer_with_region2t(hl.flag).loc_ptr;
}
}

void goto_symex_statet::rename_address(expr2tc &expr)
Expand Down
68 changes: 64 additions & 4 deletions src/goto-symex/symex_assign.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -186,8 +186,13 @@ void goto_symext::symex_assign(
expr2tc rhs = code.source;
if (options.get_bool_option("z3-slhv"))
{
// Use SLHV empty pointer and empty heap
replace_null(lhs);
replace_null(rhs);

// Turn every form of pointer arithmetic to locadd
replace_by_locadd(lhs);
replace_by_locadd(rhs);
}

log_status("symex assign lhs : ------------- ");
Expand Down Expand Up @@ -902,15 +907,12 @@ void goto_symext::symex_assign_heap_load(
assert(is_scalar_type(rhs));

const heap_load2t& heap_load = to_heap_load2t(lhs);
// assert(heap_load.byte_len * 8 == rhs->type->get_width());

symex_assign_rec(heap_load.flag, heap_load.flag, rhs, full_rhs, guard, hidden);

expr2tc updated_heap =
heap_update2tc(
heap_load.heap,
heap_load.start_loc,
heap_load.flag,
rhs,
heap_load.byte_len);

symex_assign_rec(heap_load.heap, heap_load.heap, updated_heap, updated_heap, guard, hidden);
Expand Down Expand Up @@ -949,4 +951,62 @@ void goto_symext::replace_null(expr2tc &expr)
replace_null(e);
});
}
}

void goto_symext::replace_by_locadd(expr2tc &expr)
{
if (is_nil_expr(expr) || is_symbol2t(expr)) return;
if (is_member2t(expr))
{
member2t& member = to_member2t(expr);

type2tc deref_type = member.type;
expr2tc deref_loc;

if (is_dereference2t(member.source_value))
{
dereference2t& deref = to_dereference2t(member.source_value);
expr2tc loc_ptr = deref.value;
replace_by_locadd(loc_ptr);

struct_type2t& ty = to_struct_type(deref.type);
unsigned int index = ty.get_component_number(member.member);

if (index != 0)
deref_loc = locadd2tc(loc_ptr, gen_ulong(index));
else
deref_loc = loc_ptr;
}
else
{
// TODO
log_error("Do not support this member expr");
abort();
}

expr = dereference2tc(deref_type, deref_loc);
}
else 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;

replace_by_locadd(side_1);
replace_by_locadd(side_2);

if (is_pointer_type(side_2) || is_intloc_type(side_2))
std::swap(side_1, side_2);

if (is_sub2t(expr))
side_2 = neg2tc(side_2->type, side_2);

expr = locadd2tc(side_1, side_2);
}
else
{
expr->Foreach_operand([this](expr2tc &e) {
if (!is_nil_expr(e))
replace_by_locadd(e);
});
}
}
125 changes: 0 additions & 125 deletions src/goto-symex/symex_target_equation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,21 +147,6 @@ void symex_target_equationt::convert(smt_convt &smt_conv)
log_status("final convert result ============= ");
}

// void symex_target_equationt::convert2slhv(z3_slhv_convt& slhv_convt) {
// smt_convt::ast_vec assertions;
// smt_astt assumpt_ast = slhv_convt.convert_ast_slhv(gen_true_expr());
// for (auto &SSA_step : SSA_steps)
// convert_internal_step_slhv(slhv_convt, assumpt_ast, assertions, SSA_step);

// if (!assertions.empty())
// slhv_convt.assert_ast(slhv_convt.make_n_ary_or(assertions));
// log_status("final convert result ============= ");

// slhv_convt.dump_smt();
// log_status("================================== ");

// }

void symex_target_equationt::convert_internal_step(
smt_convt &smt_conv,
smt_astt &assumpt_ast,
Expand Down Expand Up @@ -271,116 +256,6 @@ void symex_target_equationt::convert_internal_step(
log_status("-------------- over -----------------");
}


// void symex_target_equationt::convert_internal_step_slhv(
// z3_slhv_convt& slhv_convt,
// smt_astt& assumpt_ast,
// smt_convt::ast_vec& assertions,
// SSA_stept &step
// ) {

// log_status("------ convert internal step slhv ------ ");
// static unsigned output_count = 0; // Temporary hack; should become scoped.
// smt_astt true_val = slhv_convt.convert_ast_slhv(gen_true_expr());
// smt_astt false_val = slhv_convt.convert_ast_slhv(gen_false_expr());

// if (step.ignore)
// {
// // std::ostringstream oss;
// // step.output(ns, oss);
// // log_status("{}", oss.str());
// // log_status("convert internal step ignored ------ ");

// // log_status("-------------- over -----------------");
// step.cond_ast = true_val;
// step.guard_ast = false_val;
// return;
// }

// log_status(" ------------------ dump step ------------------- ");
// step.dump();

// if (ssa_trace)
// {
// log_status("-------------- ssa trace -----------------");
// std::ostringstream oss;
// step.output(ns, oss);
// log_status("{}", oss.str());
// log_status("-------------- ssa trace end-----------------");
// }
// log_status("------------- convert step guard ast: ");
// step.guard_ast = slhv_convt.convert_ast_slhv(step.guard);

// if (step.is_assume() || step.is_assert())
// {
// log_status("----- step is_assume || step is_assert");
// expr2tc tmp(step.cond);
// step.cond_ast = slhv_convt.convert_ast_slhv(tmp);
// if (ssa_smt_trace)
// {
// step.cond_ast->dump();
// }
// }
// else if (step.is_assignment())
// {
// log_status(" ----- step is_assignment");
// smt_astt assign = slhv_convt.convert_assign_slhv(step.cond);
// if (ssa_smt_trace)
// {
// assign->dump();
// }

// log_status("-------------- assignment over -----------------");
// }
// else if (step.is_output())
// {
// log_status(" ----- step is_output");
// // for (std::list<expr2tc>::const_iterator o_it = step.output_args.begin();
// // o_it != step.output_args.end();
// // o_it++)
// // {
// // const expr2tc &tmp = *o_it;
// // if (is_constant_expr(tmp) || is_constant_string2t(tmp))
// // step.converted_output_args.push_back(tmp);
// // else
// // {
// // expr2tc sym =
// // symbol2tc(tmp->type, "symex::output::" + i2string(output_count++));
// // expr2tc eq = equality2tc(sym, tmp);
// // smt_astt assign = smt_conv.convert_assign(eq);
// // if (ssa_smt_trace)
// // assign->dump();
// // step.converted_output_args.push_back(sym);
// // }
// // }
// }
// else if (step.is_renumber())
// {
// log_status(" ----- step is_renumber");
// // smt_conv.renumber_symbol_address(step.guard, step.lhs, step.rhs);
// }
// else if (!step.is_skip())
// {
// assert(0 && "Unexpected SSA step type in conversion");
// }

// if (step.is_assert())
// {
// log_status(" ----- step is_assert");
// step.cond_ast = slhv_convt.imply_ast(assumpt_ast, step.cond_ast);
// assertions.push_back(slhv_convt.invert_ast(step.cond_ast));
// slhv_convt.invert_ast(step.cond_ast)->dump();
// }
// else if (step.is_assume())
// {
// log_status(" ----- step is_assume");
// assumpt_ast = slhv_convt.mk_and(assumpt_ast, step.cond_ast);
// step.cond_ast->dump();
// }

// log_status("-------------- over -----------------");
// }

void symex_target_equationt::output(std::ostream &out) const
{
for (const auto &SSA_step : SSA_steps)
Expand Down
Loading

0 comments on commit fbd6603

Please sign in to comment.