Skip to content

Do not misuse symex dereferencing code for finding array objects [blocks: #3725] #3953

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 30, 2019
Merged

Do not misuse symex dereferencing code for finding array objects [blocks: #3725] #3953

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/goto-symex/goto_symex.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ class goto_symext

void trigger_auto_object(const exprt &, statet &);
void initialize_auto_object(const exprt &, statet &);
void process_array_expr(exprt &);
void process_array_expr(statet &, exprt &, bool);
exprt make_auto_object(const typet &, statet &);
virtual void dereference(exprt &, statet &, bool write);

Expand Down
41 changes: 33 additions & 8 deletions src/goto-symex/symex_clean_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,26 @@ Author: Daniel Kroening, [email protected]
#include <util/byte_operators.h>
#include <util/c_types.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>

#include "symex_dereference_state.h"

#include <pointer-analysis/value_set_dereference.h>

/// Given an expression, find the root object and the offset into it.
///
/// The extra complication to be considered here is that the expression may
/// have any number of ternary expressions mixed with type casts.
void goto_symext::process_array_expr(exprt &expr)
static void
process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
{
// This may change the type of the expression!

if(expr.id()==ID_if)
{
if_exprt &if_expr=to_if_expr(expr);
process_array_expr(if_expr.true_case());
process_array_expr(if_expr.false_case());
process_array_expr(if_expr.true_case(), do_simplify, ns);
process_array_expr(if_expr.false_case(), do_simplify, ns);

if(!base_type_eq(if_expr.true_case(), if_expr.false_case(), ns))
{
Expand All @@ -49,7 +55,7 @@ void goto_symext::process_array_expr(exprt &expr)
// strip
exprt tmp = to_address_of_expr(expr).object();
expr.swap(tmp);
process_array_expr(expr);
process_array_expr(expr, do_simplify, ns);
}
else if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol) &&
Expand All @@ -60,13 +66,14 @@ void goto_symext::process_array_expr(exprt &expr)
exprt tmp=index_expr.array();
expr.swap(tmp);

process_array_expr(expr);
process_array_expr(expr, do_simplify, ns);
}
else if(expr.id() != ID_symbol)
{
object_descriptor_exprt ode;
ode.build(expr, ns);
do_simplify(ode.offset());
if(do_simplify)
simplify(ode.offset(), ns);

expr = ode.root_object();

Expand All @@ -75,7 +82,8 @@ void goto_symext::process_array_expr(exprt &expr)
if(expr.type().id() != ID_array)
{
exprt array_size = size_of_expr(expr.type(), ns);
do_simplify(array_size);
if(do_simplify)
simplify(array_size, ns);
expr =
byte_extract_exprt(
byte_extract_id(),
Expand All @@ -99,7 +107,8 @@ void goto_symext::process_array_expr(exprt &expr)
subtype_size.make_typecast(array_size_type);
new_offset = div_exprt(new_offset, subtype_size);
minus_exprt new_size(prev_array_type.size(), new_offset);
do_simplify(new_size);
if(do_simplify)
simplify(new_size, ns);

array_typet new_array_type(subtype, new_size);

Expand All @@ -113,6 +122,22 @@ void goto_symext::process_array_expr(exprt &expr)
}
}

void goto_symext::process_array_expr(statet &state, exprt &expr, bool is_lhs)
{
symex_dereference_statet symex_dereference_state(*this, state);

value_set_dereferencet dereference(
ns, state.symbol_table, symex_dereference_state, language_mode, false);

expr = dereference.dereference(
expr,
guardt{true_exprt()},
is_lhs ? value_set_dereferencet::modet::WRITE
: value_set_dereferencet::modet::READ);

::process_array_expr(expr, symex_config.simplify_opt, ns);
}

/// Rewrite index/member expressions in byte_extract to offset
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
{
Expand Down
36 changes: 18 additions & 18 deletions src/goto-symex/symex_other.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ void goto_symext::symex_other(
statement==ID_array_replace)
{
// array_copy and array_replace take two pointers (to arrays); we need to:
// 1. dereference the pointers (via clean_expr)
// 1. remove any dereference expressions (via clean_expr)
// 2. find the actual array objects/candidates for objects (via
// process_array_expr)
// 3. build an assignment where the type on lhs and rhs is:
Expand All @@ -139,14 +139,14 @@ void goto_symext::symex_other(
"expected array_copy/array_replace statement to have two operands");

// we need to add dereferencing for both operands
dereference_exprt dest_array(code.op0());
clean_expr(dest_array, state, true);
dereference_exprt src_array(code.op1());
exprt dest_array(code.op0());
clean_expr(dest_array, state, false);
exprt src_array(code.op1());
clean_expr(src_array, state, false);

// obtain the actual arrays
process_array_expr(dest_array);
process_array_expr(src_array);
process_array_expr(state, dest_array, true);
process_array_expr(state, src_array, false);

// check for size (or type) mismatch and adjust
if(!base_type_eq(dest_array.type(), src_array.type(), ns))
Expand Down Expand Up @@ -181,7 +181,7 @@ void goto_symext::symex_other(
{
// array_set takes a pointer (to an array) and a value that each element
// should be set to; we need to:
// 1. dereference the pointer (via clean_expr)
// 1. remove any dereference expressions (via clean_expr)
// 2. find the actual array object/candidates for objects (via
// process_array_expr)
// 3. use the type of the resulting array to construct an array_of
Expand All @@ -191,11 +191,11 @@ void goto_symext::symex_other(
"expected array_set statement to have two operands");

// we need to add dereferencing for the first operand
exprt array_expr = dereference_exprt(code.op0());
clean_expr(array_expr, state, true);
exprt array_expr(code.op0());
clean_expr(array_expr, state, false);

// obtain the actual array(s)
process_array_expr(array_expr);
process_array_expr(state, array_expr, true);

// prepare to build the array_of
exprt value = code.op1();
Expand Down Expand Up @@ -227,7 +227,7 @@ void goto_symext::symex_other(
{
// array_equal takes two pointers (to arrays) and the symbol that the result
// should get assigned to; we need to:
// 1. dereference the pointers (via clean_expr)
// 1. remove any dereference expressions (via clean_expr)
// 2. find the actual array objects/candidates for objects (via
// process_array_expr)
// 3. build an assignment where the lhs is the previous third argument, and
Expand All @@ -238,14 +238,14 @@ void goto_symext::symex_other(
"expected array_equal statement to have three operands");

// we need to add dereferencing for the first two
dereference_exprt array1(code.op0());
exprt array1(code.op0());
clean_expr(array1, state, false);
dereference_exprt array2(code.op1());
exprt array2(code.op1());
clean_expr(array2, state, false);

// obtain the actual arrays
process_array_expr(array1);
process_array_expr(array2);
process_array_expr(state, array1, false);
process_array_expr(state, array2, false);

code_assignt assignment(code.op2(), equal_exprt(array1, array2));

Expand All @@ -271,10 +271,10 @@ void goto_symext::symex_other(
code.operands().size() == 1,
"expected havoc_object statement to have one operand");

// we need to add dereferencing for the first operand
dereference_exprt object(code.op0(), empty_typet());
clean_expr(object, state, true);
exprt object(code.op0());
clean_expr(object, state, false);

process_array_expr(state, object, true);
havoc_rec(state, guardt(true_exprt()), object);
}
else
Expand Down