Skip to content

Symex trace fix #1373

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 7 commits into from
Sep 12, 2017
Merged

Symex trace fix #1373

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8fc714d
use __CPROVER_assert
Sep 11, 2017
3896110
output statements
Sep 11, 2017
211355d
comments on test
Sep 11, 2017
746bff5
remove_returns missing in symex
Sep 11, 2017
430218f
option is now --trace
Sep 11, 2017
5195d24
avoid confusion between SSA lhs and full lhs during assignment
Sep 11, 2017
5d2d07b
enable symex regression testing
Sep 12, 2017
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
1 change: 1 addition & 0 deletions regression/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ DIRS = ansi-c \
invariants \
strings \
strings-smoke-tests \
symex \
test-script \
# Empty last line

Expand Down
8 changes: 4 additions & 4 deletions regression/symex/show-trace1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,12 @@ int main()
{
int i, j, k;

i=input();
j=input();
k=input();
i=input(); // expect 2
j=input(); // expect 3
k=input(); // expect 6

if(i==2)
if(j==i+1)
if(k==i*j)
assert(0);
__CPROVER_assert(0, "");
}
2 changes: 1 addition & 1 deletion regression/symex/show-trace1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
--show-trace
--trace
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
49 changes: 27 additions & 22 deletions src/path-symex/path_symex.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ void path_symext::assign(

// start recursion on lhs
exprt::operandst _guard; // start with empty guard
assign_rec(state, _guard, ssa_lhs, ssa_rhs);
assign_rec(state, _guard, lhs, ssa_lhs, ssa_rhs);
}

inline static typet c_sizeof_type_rec(const exprt &expr)
Expand Down Expand Up @@ -347,6 +347,7 @@ void path_symext::symex_va_arg_next(
void path_symext::assign_rec(
path_symex_statet &state,
exprt::operandst &guard,
const exprt &full_lhs,
const exprt &ssa_lhs,
const exprt &ssa_rhs)
{
Expand Down Expand Up @@ -376,17 +377,17 @@ void path_symext::assign_rec(

// increase the SSA counter and produce new SSA symbol expression
var_info.increment_ssa_counter();
symbol_exprt new_lhs=var_info.ssa_symbol();
symbol_exprt new_ssa_lhs=var_info.ssa_symbol();

#ifdef DEBUG
std::cout << "new_lhs: " << new_lhs.get_identifier() << '\n';
std::cout << "new_ssa_lhs: " << new_ssa_lhs.get_identifier() << '\n';
#endif

// record new state of lhs
{
// reference is not stable
path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
var_state.ssa_symbol=new_lhs;
var_state.ssa_symbol=new_ssa_lhs;
}

// rhs nil means non-det assignment
Expand All @@ -398,11 +399,11 @@ void path_symext::assign_rec(
else
{
// consistency check
if(!base_type_eq(ssa_rhs.type(), new_lhs.type(), state.var_map.ns))
if(!base_type_eq(ssa_rhs.type(), new_ssa_lhs.type(), state.var_map.ns))
{
#ifdef DEBUG
std::cout << "ssa_rhs: " << ssa_rhs.pretty() << '\n';
std::cout << "new_lhs: " << new_lhs.pretty() << '\n';
std::cout << "new_ssa_lhs: " << new_ssa_lhs.pretty() << '\n';
#endif
throw "assign_rec got different types";
}
Expand All @@ -413,8 +414,8 @@ void path_symext::assign_rec(

if(!guard.empty())
step.guard=conjunction(guard);
step.full_lhs=ssa_lhs;
step.ssa_lhs=new_lhs;
step.full_lhs=full_lhs;
step.ssa_lhs=new_ssa_lhs;
step.ssa_rhs=ssa_rhs;

// propagate the rhs?
Expand All @@ -425,10 +426,10 @@ void path_symext::assign_rec(
else if(ssa_lhs.id()==ID_typecast)
{
// dereferencing might yield a typecast
const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
const exprt &new_ssa_lhs=to_typecast_expr(ssa_lhs).op();
typecast_exprt new_rhs(ssa_rhs, new_ssa_lhs.type());

assign_rec(state, guard, new_lhs, new_rhs);
assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);
}
else if(ssa_lhs.id()==ID_member)
{
Expand All @@ -454,17 +455,17 @@ void path_symext::assign_rec(

with_exprt new_rhs(struct_op, member_name, ssa_rhs);

assign_rec(state, guard, struct_op, new_rhs);
assign_rec(state, guard, full_lhs, struct_op, new_rhs);
}
else if(compound_type.id()==ID_union)
{
// rewrite into byte_extract, and do again
exprt offset=from_integer(0, index_type());

byte_extract_exprt
new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());
new_ssa_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());

assign_rec(state, guard, new_lhs, ssa_rhs);
assign_rec(state, guard, full_lhs, new_ssa_lhs, ssa_rhs);
}
else
throw "assign_rec: member expects struct or union type";
Expand Down Expand Up @@ -496,12 +497,12 @@ void path_symext::assign_rec(

// true
guard.push_back(cond);
assign_rec(state, guard, lhs_if_expr.true_case(), ssa_rhs);
assign_rec(state, guard, full_lhs, lhs_if_expr.true_case(), ssa_rhs);
guard.pop_back();

// false
guard.push_back(not_exprt(cond));
assign_rec(state, guard, lhs_if_expr.false_case(), ssa_rhs);
assign_rec(state, guard, full_lhs, lhs_if_expr.false_case(), ssa_rhs);
guard.pop_back();
}
else if(ssa_lhs.id()==ID_byte_extract_little_endian ||
Expand Down Expand Up @@ -533,9 +534,9 @@ void path_symext::assign_rec(
new_rhs.offset()=byte_extract_expr.offset();
new_rhs.value()=ssa_rhs;

const exprt new_lhs=byte_extract_expr.op();
const exprt new_ssa_lhs=byte_extract_expr.op();

assign_rec(state, guard, new_lhs, new_rhs);
assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);
}
else if(ssa_lhs.id()==ID_struct)
{
Expand All @@ -555,7 +556,7 @@ void path_symext::assign_rec(
exprt::operandst::const_iterator lhs_it=operands.begin();
forall_operands(it, ssa_rhs)
{
assign_rec(state, guard, *lhs_it, *it);
assign_rec(state, guard, full_lhs, *lhs_it, *it);
++lhs_it;
}
}
Expand All @@ -571,7 +572,7 @@ void path_symext::assign_rec(
components[i].get_name(),
components[i].type()),
state.var_map.ns);
assign_rec(state, guard, operands[i], new_rhs);
assign_rec(state, guard, full_lhs, operands[i], new_rhs);
}
}
}
Expand All @@ -594,7 +595,7 @@ void path_symext::assign_rec(
exprt::operandst::const_iterator lhs_it=operands.begin();
forall_operands(it, ssa_rhs)
{
assign_rec(state, guard, *lhs_it, *it);
assign_rec(state, guard, full_lhs, *lhs_it, *it);
++lhs_it;
}
}
Expand All @@ -610,7 +611,7 @@ void path_symext::assign_rec(
from_integer(i, index_type()),
array_type.subtype()),
state.var_map.ns);
assign_rec(state, guard, operands[i], new_rhs);
assign_rec(state, guard, full_lhs, operands[i], new_rhs);
}
}
}
Expand Down Expand Up @@ -1090,6 +1091,10 @@ void path_symext::operator()(
{
// just needs to be recorded
}
else if(statement==ID_output)
{
// just needs to be recorded
}
else
throw "unexpected OTHER statement: "+id2string(statement);
}
Expand Down
1 change: 1 addition & 0 deletions src/path-symex/path_symex_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ class path_symext
void assign_rec(
path_symex_statet &state,
exprt::operandst &guard, // instantiated
const exprt &full_lhs, // not instantiated, no recursion
const exprt &ssa_lhs, // instantiated, recursion here
const exprt &ssa_rhs); // instantiated

Expand Down
22 changes: 12 additions & 10 deletions src/symex/symex_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,23 +26,24 @@ Author: Daniel Kroening, [email protected]
#include <cpp/cpp_language.h>
#include <java_bytecode/java_bytecode_language.h>

#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/show_properties.h>
#include <goto-programs/set_properties.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/loop_ids.h>
#include <goto-programs/link_to_library.h>
#include <goto-programs/goto_inline.h>
#include <goto-programs/xml_goto_trace.h>
#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/link_to_library.h>
#include <goto-programs/loop_ids.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/remove_complex.h>
#include <goto-programs/remove_exceptions.h>
#include <goto-programs/remove_function_pointers.h>
#include <goto-programs/remove_instanceof.h>
#include <goto-programs/remove_returns.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/remove_unused_functions.h>
#include <goto-programs/remove_vector.h>
#include <goto-programs/remove_virtual_functions.h>
#include <goto-programs/remove_exceptions.h>
#include <goto-programs/remove_instanceof.h>
#include <goto-programs/remove_unused_functions.h>
#include <goto-programs/set_properties.h>
#include <goto-programs/show_properties.h>
#include <goto-programs/xml_goto_trace.h>

#include <goto-symex/rewrite_union.h>
#include <goto-symex/adjust_float_expressions.h>
Expand Down Expand Up @@ -304,6 +305,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
goto_check(options, goto_model);

// remove stuff
remove_returns(goto_model);
remove_complex(goto_model);
remove_vector(goto_model);
// remove function pointers
Expand Down