replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

use ssa_exprt 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6381 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2016-02-17 17:10:28 +00:00
parent 6e71d5c978
commit a5bc493713
35 changed files with 754 additions and 698 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
regression/cbmc/Malloc18/test.desc
View File

@ -1,4 +1,4 @@
KNOWNBUG
CORE
main.c
^EXIT=0$

2
regression/cbmc/Malloc21/test.desc
View File

@ -1,4 +1,4 @@
KNOWNBUG
CORE
main.c
^EXIT=0$

2
src/analyses/goto_check.cpp
View File

@ -1540,6 +1540,8 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
goto_programt::targett t=new_code.add_instruction(ASSIGN);
exprt address_of_expr=address_of_exprt(variable);
exprt lhs=ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
address_of_expr.make_typecast(lhs.type());
exprt rhs=if_exprt(
side_effect_expr_nondett(bool_typet()), address_of_expr, lhs, lhs.type());
t->source_location=i.source_location;

2
src/cbmc/counterexample_beautification.cpp
View File

@ -45,7 +45,7 @@ void counterexample_beautificationt::get_minimization_list(
{
if(!prop_conv.l_get(it->guard_literal).is_false())
{
const typet &type=it->original_lhs_object.type();
const typet &type=it->ssa_lhs.type();
if(type!=bool_typet())
{

8
src/goto-programs/goto_trace.cpp
View File

@ -112,8 +112,8 @@ void goto_trace_stept::output(
if(pc->is_other() || pc->is_assign())
{
irep_idt identifier=lhs_object.get_identifier();
out << " " << identifier
irep_idt identifier=lhs_object.get_object_name();
out << " " << from_expr(ns, identifier, lhs_object.get_original_expr())
<< " = " << from_expr(ns, identifier, lhs_object_value)
<< "\n";
}
@ -221,11 +221,11 @@ Function: trace_value
void trace_value(
std::ostream &out,
const namespacet &ns,
const symbol_exprt &lhs_object,
const ssa_exprt &lhs_object,
const exprt &full_lhs,
const exprt &value)
{
const irep_idt &identifier=lhs_object.get_identifier();
const irep_idt &identifier=lhs_object.get_object_name();
std::string value_string;
if(value.is_nil())

6
src/goto-programs/goto_trace.h
View File

@ -21,7 +21,7 @@ Date: July 2005
#include <iosfwd>
#include <vector>
#include <util/std_expr.h>
#include <util/ssa_expr.h>
#include <goto-programs/goto_program.h>
@ -80,7 +80,7 @@ public:
std::string comment;
// the object being assigned
symbol_exprt lhs_object;
ssa_exprt lhs_object;
// the full, original lhs expression
exprt full_lhs;
@ -173,7 +173,7 @@ void show_goto_trace(
void trace_value(
std::ostream &out,
const namespacet &ns,
const symbol_exprt &lhs_object,
const ssa_exprt &lhs_object,
const exprt &full_lhs,
const exprt &value);

28
src/goto-symex/auto_objects.cpp
View File

@ -101,7 +101,7 @@ void goto_symext::initialize_auto_object(
address_of_expr);
code_assignt assignment(expr, rhs);
symex_assign(state, assignment); /* TODO: needs clean */
symex_assign_rec(state, assignment);
}
}
}
@ -122,21 +122,25 @@ void goto_symext::trigger_auto_object(
const exprt &expr,
statet &state)
{
if(expr.id()==ID_symbol)
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
const symbol_exprt &symbol_expr=to_symbol_expr(expr);
const irep_idt &identifier=symbol_expr.get_identifier();
const ssa_exprt &ssa_expr=to_ssa_expr(expr);
const irep_idt &obj_identifier=ssa_expr.get_object_name();
const symbolt &symbol=
ns.lookup(state.get_original_name(identifier));
if(has_prefix(id2string(symbol.base_name), "auto_object"))
if(obj_identifier!="goto_symex::\\guard")
{
// done already?
if(state.level2.current_names.find(identifier)==
state.level2.current_names.end())
const symbolt &symbol=
ns.lookup(obj_identifier);
if(has_prefix(id2string(symbol.base_name), "auto_object"))
{
initialize_auto_object(expr, state);
// done already?
if(state.level2.current_names.find(ssa_expr.get_identifier())==
state.level2.current_names.end())
{
initialize_auto_object(expr, state);
}
}
}
}

5
src/goto-symex/build_goto_trace.cpp
View File

@ -226,7 +226,10 @@ void build_goto_trace(
goto_trace_step.thread_nr=SSA_step.source.thread_nr;
goto_trace_step.pc=SSA_step.source.pc;
goto_trace_step.comment=SSA_step.comment;
goto_trace_step.lhs_object=SSA_step.original_lhs_object;
if(SSA_step.ssa_lhs.is_not_nil())
goto_trace_step.lhs_object=ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
else
goto_trace_step.lhs_object.make_nil();
goto_trace_step.type=SSA_step.type;
goto_trace_step.hidden=SSA_step.hidden;
goto_trace_step.format_string=SSA_step.format_string;

4
src/goto-symex/goto_symex.h
View File

@ -153,6 +153,7 @@ protected:
virtual void symex_atomic_begin(statet &state);
virtual void symex_atomic_end(statet &state);
virtual void symex_decl(statet &state);
virtual void symex_decl(statet &state, const symbol_exprt &expr);
virtual void symex_dead(statet &state);
virtual void symex_other(
@ -239,12 +240,13 @@ protected:
virtual void do_simplify(exprt &expr);
//virtual void symex_block(statet &state, const codet &code);
void symex_assign_rec(statet &state, const code_assignt &code);
virtual void symex_assign(statet &state, const code_assignt &code);
typedef symex_targett::assignment_typet assignment_typet;
void symex_assign_rec(statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
void symex_assign_symbol(statet &state, const symbol_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);
void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type);

578
src/goto-symex/goto_symex_state.cpp
View File

@ -76,49 +76,41 @@ Function: goto_symex_statet::level0t::operator()
\*******************************************************************/
irep_idt goto_symex_statet::level0t::operator()(
const irep_idt &identifier,
void goto_symex_statet::level0t::operator()(
ssa_exprt &ssa_expr,
const namespacet &ns,
unsigned thread_nr)
{
// already renamed?
if(original_identifiers.find(identifier)!=original_identifiers.end())
return identifier;
if(!ssa_expr.get_level_0().empty())
return;
const irep_idt &obj_identifier=ssa_expr.get_object_name();
// guards are not L0-renamed
if(identifier=="goto_symex::\\guard")
{
original_identifiers[identifier]=identifier;
return identifier;
}
if(obj_identifier=="goto_symex::\\guard")
return;
const symbolt *s;
if(ns.lookup(identifier, s))
if(ns.lookup(obj_identifier, s))
{
std::cerr << "level0: failed to find " << identifier << std::endl;
std::cerr << "level0: failed to find " << obj_identifier << std::endl;
abort();
}
// don't rename shared variables or functions
if(s->type.id()==ID_code ||
s->is_shared())
{
original_identifiers[identifier]=identifier;
return identifier;
}
return;
// rename!
irep_idt new_identifier=name(identifier, thread_nr);
// remember that
original_identifiers[new_identifier]=identifier;
return new_identifier;
ssa_expr.set_level_0(thread_nr);
}
/*******************************************************************\
Function: goto_symex_statet::renaming_levelt::current_count
Function: goto_symex_statet::level1t::operator()
Inputs:
@ -128,11 +120,19 @@ Function: goto_symex_statet::renaming_levelt::current_count
\*******************************************************************/
unsigned goto_symex_statet::renaming_levelt::current_count(
const irep_idt &identifier) const
void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
{
current_namest::const_iterator it=current_names.find(identifier);
return it==current_names.end()?0:it->second;
// already renamed?
if(!ssa_expr.get_level_1().empty())
return;
const irep_idt l0_name=ssa_expr.get_l1_object_identifier();
current_namest::const_iterator it=current_names.find(l0_name);
if(it==current_names.end()) return;
// rename!
ssa_expr.set_level_1(it->second.second);
}
/*******************************************************************\
@ -285,22 +285,118 @@ Function: goto_symex_statet::assignment
\*******************************************************************/
static bool check_renaming(const exprt &expr);
static bool check_renaming(const typet &type)
{
if(type.id()==ID_array)
return check_renaming(to_array_type(type).size());
else if(type.id()==ID_struct ||
type.id()==ID_union ||
type.id()==ID_class)
{
const struct_union_typet &s_u_type=to_struct_union_type(type);
const struct_union_typet::componentst &components=s_u_type.components();
for(struct_union_typet::componentst::const_iterator
it=components.begin();
it!=components.end();
++it)
if(check_renaming(it->type()))
return true;
}
else if(type.has_subtype())
return check_renaming(type.subtype());
return false;
}
static bool check_renaming_l1(const exprt &expr)
{
if(check_renaming(expr.type())) return true;
if(expr.id()==ID_symbol)
{
if(!expr.get_bool(ID_C_SSA_symbol)) return expr.type().id()!=ID_code;
if(!to_ssa_expr(expr).get_level_2().empty()) return true;
if(to_ssa_expr(expr).get_original_expr().type()!=expr.type()) return true;
}
else
{
forall_operands(it, expr)
if(check_renaming_l1(*it)) return true;
}
return false;
}
static bool check_renaming(const exprt &expr)
{
if(check_renaming(expr.type())) return true;
if(expr.id()==ID_address_of &&
expr.op0().id()==ID_symbol)
return check_renaming_l1(expr.op0());
else if(expr.id()==ID_address_of &&
expr.op0().id()==ID_index)
return check_renaming_l1(expr.op0().op0()) ||
check_renaming(expr.op0().op1());
else if(expr.id()==ID_symbol)
{
if(!expr.get_bool(ID_C_SSA_symbol)) return expr.type().id()!=ID_code;
if(to_ssa_expr(expr).get_level_2().empty()) return true;
if(to_ssa_expr(expr).get_original_expr().type()!=expr.type()) return true;
}
else
{
forall_operands(it, expr)
if(check_renaming(*it)) return true;
}
return false;
}
static void assert_l1_renaming(const exprt &expr)
{
#if 1
if(check_renaming_l1(expr))
{
std::cerr << expr.pretty() << std::endl;
assert(false);
}
#else
(void)expr;
#endif
}
static void assert_l2_renaming(const exprt &expr)
{
#if 1
if(check_renaming(expr))
{
std::cerr << expr.pretty() << std::endl;
assert(false);
}
#else
(void)expr;
#endif
}
void goto_symex_statet::assignment(
symbol_exprt &lhs, // L0/L1
ssa_exprt &lhs, // L0/L1
const exprt &rhs, // L2
const namespacet &ns,
bool rhs_is_simplified,
bool record_value)
{
assert(lhs.id()==ID_symbol);
// identifier should be l0 or l1, make sure it's l1
rename(lhs, ns, L1);
irep_idt l1_identifier=lhs.get_identifier();
// the type might need renaming
rename(lhs.type(), ns);
irep_idt identifier=lhs.get_identifier();
// identifier should be l0 or l1, make sure it's l1
irep_idt l1_identifier=level1(identifier);
rename(lhs.type(), l1_identifier, ns);
lhs.update_type();
assert_l1_renaming(lhs);
#if 0
assert(l1_identifier != get_original_name(l1_identifier)
@ -310,13 +406,18 @@ void goto_symex_statet::assignment(
|| has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
#endif
// do the l2 renaming
irep_idt new_l2_name=level2.increase_counter(l1_identifier);
lhs.set_identifier(new_l2_name);
// do the l2 renaming
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
level2.current_names[l1_identifier]=std::make_pair(lhs, 0);
level2.increase_counter(l1_identifier);
set_ssa_indices(lhs, ns, L2);
// in case we happen to be multi-threaded, record the memory access
bool is_shared=l2_thread_write_encoding(lhs, ns);
assert_l2_renaming(lhs);
assert_l2_renaming(rhs);
// for value propagation -- the RHS is L2
if(!is_shared && record_value && constant_propagation(rhs))
@ -328,16 +429,19 @@ void goto_symex_statet::assignment(
// update value sets
value_sett::expr_sett rhs_value_set;
exprt l1_rhs(rhs);
level2.get_original_name(l1_rhs);
get_l1_name(l1_rhs);
symbol_exprt l1_lhs(l1_identifier, lhs.type());
level2.get_original_name(l1_lhs.type());
ssa_exprt l1_lhs(lhs);
get_l1_name(l1_lhs);
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
assert_l1_renaming(l1_lhs);
assert_l1_renaming(l1_rhs);
value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
}
#if 0
std::cout << "Assigning " << identifier << std::endl;
std::cout << "Assigning " << l1_identifier << std::endl;
value_set.output(ns, std::cout);
std::cout << "**********************" << std::endl;
#endif
@ -360,7 +464,7 @@ void goto_symex_statet::propagationt::operator()(exprt &expr)
if(expr.id()==ID_symbol)
{
valuest::const_iterator it=
values.find(to_symbol_expr(expr).get_identifier());
values.find(expr.get(ID_identifier));
if(it!=values.end())
expr=it->second;
}
@ -378,7 +482,7 @@ void goto_symex_statet::propagationt::operator()(exprt &expr)
/*******************************************************************\
Function: goto_symex_statet::rename_identifier
Function: goto_symex_statet::set_ssa_indices
Inputs:
@ -388,31 +492,30 @@ Function: goto_symex_statet::rename_identifier
\*******************************************************************/
irep_idt goto_symex_statet::rename_identifier(
const irep_idt &identifier,
void goto_symex_statet::set_ssa_indices(
ssa_exprt &ssa_expr,
const namespacet &ns,
levelt level)
{
switch(level)
{
case L0:
return level0(identifier, ns, source.thread_nr);
level0(ssa_expr, ns, source.thread_nr);
break;
case L1:
{
if(level2.is_renamed(identifier)) return identifier;
if(level1.is_renamed(identifier)) return identifier;
irep_idt l0_identifier=level0(identifier, ns, source.thread_nr);
return level1(l0_identifier);
}
if(!ssa_expr.get_level_2().empty()) return;
if(!ssa_expr.get_level_1().empty()) return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
break;
case L2:
{
if(level2.is_renamed(identifier)) return identifier;
irep_idt l0_identifier=level0(identifier, ns, source.thread_nr);
irep_idt l1_identifier=level1(l0_identifier);
return level2(l1_identifier); // L2
}
if(!ssa_expr.get_level_2().empty()) return;
level0(ssa_expr, ns, source.thread_nr);
level1(ssa_expr);
ssa_expr.set_level_2(level2.current_count(ssa_expr.get_identifier()));
break;
default:
assert(false);
@ -437,62 +540,87 @@ void goto_symex_statet::rename(
levelt level)
{
// rename all the symbols with their last known value
rename(expr.type(), ns, level);
if(expr.id()==ID_symbol)
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
// we never rename function symbols
if(ns.follow(expr.type()).id()==ID_code)
return;
const irep_idt identifier=to_symbol_expr(expr).get_identifier();
ssa_exprt &ssa=to_ssa_expr(expr);
if(level==L0 || level==L1)
{
const irep_idt new_name=rename_identifier(identifier, ns, level);
to_symbol_expr(expr).set_identifier(new_name);
}
set_ssa_indices(ssa, ns, level);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
}
else if(level==L2)
{
if(l2_thread_read_encoding(to_symbol_expr(expr), ns))
set_ssa_indices(ssa, ns, L1);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
if(l2_thread_read_encoding(ssa, ns))
{
// renaming taken care of by l2_thread_encoding
}
else if(level2.is_renamed(identifier))
else if(!ssa.get_level_2().empty())
{
// already at L2
}
else
{
irep_idt l1_identifier=rename_identifier(identifier, ns, L1);
// We also consider propagation if we go up to L2.
// L1 identifiers are used for propagation!
propagationt::valuest::const_iterator p_it=
propagation.values.find(l1_identifier);
propagation.values.find(ssa.get_identifier());
if(p_it!=propagation.values.end())
expr=p_it->second; // already L2
else
{
irep_idt new_name=level2(l1_identifier); // L2
to_symbol_expr(expr).set_identifier(new_name);
}
set_ssa_indices(ssa, ns, L2);
}
}
}
else if(expr.id()==ID_symbol)
{
// we never rename function symbols
if(ns.follow(expr.type()).id()==ID_code)
{
rename(
expr.type(),
to_symbol_expr(expr).get_identifier(),
ns,
level);
return;
}
expr=ssa_exprt(expr);
rename(expr, ns, level);
}
else if(expr.id()==ID_address_of)
{
assert(expr.operands().size()==1);
rename_address(expr.op0(), ns, level);
assert(expr.type().id()==ID_pointer);
expr.type().subtype()=expr.op0().type();
}
else
{
// this could go wrong, but we would have to re-typecheck ...
rename(expr.type(), irep_idt(), ns, level);
// do this recursively
Forall_operands(it, expr)
rename(*it, ns, level);
// some fixes
if(expr.id()==ID_with)
expr.type()=to_with_expr(expr).old().type();
else if(expr.id()==ID_if)
{
assert(to_if_expr(expr).true_case().type()==to_if_expr(expr).false_case().type());
expr.type()=to_if_expr(expr).true_case().type();
}
}
}
@ -509,7 +637,7 @@ Function: goto_symex_statet::l2_thread_read_encoding
\*******************************************************************/
bool goto_symex_statet::l2_thread_read_encoding(
symbol_exprt &expr,
ssa_exprt &expr,
const namespacet &ns)
{
if(!record_events)
@ -519,17 +647,15 @@ bool goto_symex_statet::l2_thread_read_encoding(
if(threads.size()<=1)
return false;
const irep_idt &identifier=expr.get_identifier();
const irep_idt &orig_identifier=get_original_name(identifier);
// is it a shared object?
if(orig_identifier=="goto_symex::\\guard" ||
!ns.lookup(orig_identifier).is_shared())
const irep_idt &obj_identifier=expr.get_object_name();
if(obj_identifier=="goto_symex::\\guard" ||
!ns.lookup(obj_identifier).is_shared())
return false;
const irep_idt l1_identifier=rename_identifier(orig_identifier, ns, L1);
symbol_exprt ssa_l1=expr;
ssa_l1.set_identifier(l1_identifier);
ssa_exprt ssa_l1=expr;
ssa_l1.remove_level_2();
const irep_idt &l1_identifier=ssa_l1.get_identifier();
// see whether we are within an atomic section
if(atomic_section_id!=0)
@ -586,16 +712,17 @@ bool goto_symex_statet::l2_thread_read_encoding(
cond=or_exprt(no_write.op(), cond);
if_exprt tmp(cond, ssa_l1, ssa_l1);
level2(to_symbol_expr(tmp.true_case()));
set_ssa_indices(to_ssa_expr(tmp.true_case()), ns, L2);
if(a_s_read.second.empty())
{
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
level2.increase_counter(l1_identifier);
a_s_read.first=level2.current_count(l1_identifier);
}
to_symbol_expr(tmp.false_case()).set_identifier(
level2.name(l1_identifier, a_s_read.first));
to_ssa_expr(tmp.false_case()).set_level_2(a_s_read.first);
if(cond.is_false())
{
@ -605,17 +732,21 @@ bool goto_symex_statet::l2_thread_read_encoding(
const bool record_events_bak=record_events;
record_events=false;
assignment(expr, tmp, ns, true, true);
assignment(ssa_l1, tmp, ns, true, true);
record_events=record_events_bak;
symbol_exprt lhs=ns.lookup(orig_identifier).symbol_expr();
symex_target->assignment(
guard.as_expr(),
expr, lhs, expr, lhs,
ssa_l1,
ssa_l1,
ssa_l1.get_original_expr(),
tmp,
source,
symex_targett::PHI);
set_ssa_indices(ssa_l1, ns, L2);
expr=ssa_l1;
a_s_read.second.push_back(guard);
if(!no_write.op().is_false())
a_s_read.second.back().add(no_write);
@ -624,16 +755,17 @@ bool goto_symex_statet::l2_thread_read_encoding(
}
// produce a fresh L2 name
irep_idt new_l2_name=level2.increase_counter(l1_identifier);
expr.set_identifier(new_l2_name);
if(level2.current_names.find(l1_identifier)==level2.current_names.end())
level2.current_names[l1_identifier]=std::make_pair(ssa_l1, 0);
level2.increase_counter(l1_identifier);
set_ssa_indices(ssa_l1, ns, L2);
expr=ssa_l1;
// and record that
assert(symex_target!=NULL);
symbol_exprt original_symbol(orig_identifier, expr.type());
symex_target->shared_read(
guard.as_expr(),
expr,
original_symbol,
atomic_section_id,
source);
@ -653,38 +785,32 @@ Function: goto_symex_statet::l2_thread_write_encoding
\*******************************************************************/
bool goto_symex_statet::l2_thread_write_encoding(
const symbol_exprt &expr,
const ssa_exprt &expr,
const namespacet &ns)
{
if(!record_events)
return false;
const irep_idt &identifier=expr.get_identifier();
const irep_idt &orig_identifier=get_original_name(identifier);
// is it a shared object?
if(orig_identifier=="goto_symex::\\guard" ||
!ns.lookup(orig_identifier).is_shared())
const irep_idt &obj_identifier=expr.get_object_name();
if(obj_identifier=="goto_symex::\\guard" ||
!ns.lookup(obj_identifier).is_shared())
return false; // not shared
// see whether we are within an atomic section
if(atomic_section_id!=0)
{
const irep_idt l1_identifier=rename_identifier(orig_identifier, ns, L1);
symbol_exprt ssa_l1=expr;
ssa_l1.set_identifier(l1_identifier);
ssa_exprt ssa_l1=expr;
ssa_l1.remove_level_2();
written_in_atomic_section[ssa_l1].push_back(guard);
return false;
}
// record a shared write
symbol_exprt original_symbol(orig_identifier, expr.type());
symex_target->shared_write(
guard.as_expr(),
expr,
original_symbol,
atomic_section_id,
source);
@ -709,24 +835,34 @@ void goto_symex_statet::rename_address(
const namespacet &ns,
levelt level)
{
rename(expr.type(), ns, level);
if(expr.id()==ID_symbol)
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
ssa_exprt &ssa=to_ssa_expr(expr);
// only do L1!
irep_idt identifier=to_symbol_expr(expr).get_identifier();
identifier=rename_identifier(identifier, ns, L1);
to_symbol_expr(expr).set_identifier(identifier);
set_ssa_indices(ssa, ns, L1);
rename(expr.type(), ssa.get_identifier(), ns, level);
ssa.update_type();
}
else if(expr.id()==ID_symbol)
{
expr=ssa_exprt(expr);
rename_address(expr, ns, level);
}
else
{
if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);
rename_address(expr.op0(), ns, level);
index_exprt &index_expr=to_index_expr(expr);
rename_address(index_expr.array(), ns, level);
assert(index_expr.array().type().id()==ID_array);
expr.type()=index_expr.array().type().subtype();
// the index is not an address
rename(expr.op1(), ns, level);
rename(index_expr.index(), ns, level);
}
else if(expr.id()==ID_if)
{
@ -735,13 +871,34 @@ void goto_symex_statet::rename_address(
rename(if_expr.cond(), ns, level);
rename_address(if_expr.true_case(), ns, level);
rename_address(if_expr.false_case(), ns, level);
if_expr.type()=if_expr.true_case().type();
}
else if(expr.id()==ID_member)
{
rename_address(to_member_expr(expr).struct_op(), ns, level);
member_exprt &member_expr=to_member_expr(expr);
rename_address(member_expr.struct_op(), ns, level);
// type might not have been renamed in case of nesting of
// structs and pointers/arrays
if(member_expr.struct_op().type().id()!=ID_symbol)
{
const struct_union_typet &su_type=
to_struct_union_type(member_expr.struct_op().type());
const struct_union_typet::componentt &comp=
su_type.get_component(member_expr.get_component_name());
assert(comp.is_not_nil());
expr.type()=comp.type();
}
else
rename(expr.type(), irep_idt(), ns, level);
}
else
{
// this could go wrong, but we would have to re-typecheck ...
rename(expr.type(), irep_idt(), ns, level);
// do this recursively; we assume here
// that all the operands are addresses
Forall_operands(it, expr)
@ -764,57 +921,63 @@ Function: goto_symex_statet::rename
void goto_symex_statet::rename(
typet &type,
const irep_idt &l1_identifier,
const namespacet &ns,
levelt level)
{
// rename all the symbols with their last known value
// to the given level
std::pair<l1_typest::iterator, bool> l1_type_entry;
if(level==L2 &&
!l1_identifier.empty())
{
l1_type_entry=l1_types.insert(std::make_pair(l1_identifier, type));
if(!l1_type_entry.second)
{
type=l1_type_entry.first->second;
return;
}
}
if(type.id()==ID_array)
{
rename(type.subtype(), ns, level);
rename(type.subtype(), irep_idt(), ns, level);
rename(to_array_type(type).size(), ns, level);
}
else if(type.id()==ID_struct ||
type.id()==ID_union ||
type.id()==ID_class)
{
// TODO
struct_union_typet &s_u_type=to_struct_union_type(type);
struct_union_typet::componentst &components=s_u_type.components();
for(struct_union_typet::componentst::iterator
it=components.begin();
it!=components.end();
++it)
// be careful, or it might get cyclic
if(it->type().id()==ID_array)
rename(to_array_type(it->type()).size(), ns, level);
else if(it->type().id()!=ID_pointer)
rename(it->type(), irep_idt(), ns, level);
}
else if(type.id()==ID_pointer)
{
// rename(type.subtype(), ns);
// don't do this, or it might get cyclic
rename(type.subtype(), irep_idt(), ns, level);
}
else if(type.id()==ID_symbol)
{
const symbolt &symbol=
ns.lookup(to_symbol_type(type).get_identifier());
type=symbol.type;
rename(type, ns, level);
rename(type, l1_identifier, ns, level);
}
}
/*******************************************************************\
Function: goto_symex_statet::renaming_levelt::print
Inputs:
Outputs:
Purpose:
\*******************************************************************/
void goto_symex_statet::renaming_levelt::print(std::ostream &out) const
{
for(current_namest::const_iterator
it=current_names.begin();
it!=current_names.end();
it++)
out << it->first << " --> "
<< name(it->first, it->second) << std::endl;
if(level==L2 &&
!l1_identifier.empty())
l1_type_entry.first->second=type;
}
/*******************************************************************\
@ -833,68 +996,15 @@ void goto_symex_statet::get_original_name(exprt &expr) const
{
get_original_name(expr.type());
Forall_operands(it, expr)
get_original_name(*it);
if(expr.id()==ID_symbol)
{
level2.get_original_name(expr);
level1.get_original_name(expr);
level0.get_original_name(expr);
}
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
expr=to_ssa_expr(expr).get_original_expr();
else
Forall_operands(it, expr)
get_original_name(*it);
}
/*******************************************************************\
Function: goto_symex_statet::renaming_levelt::get_original_name
Inputs:
Outputs:
Purpose:
\*******************************************************************/
void goto_symex_statet::renaming_levelt::get_original_name(exprt &expr) const
{
get_original_name(expr.type());
Forall_operands(it, expr)
get_original_name(*it);
if(expr.id()==ID_symbol)
{
original_identifierst::const_iterator it=
original_identifiers.find(expr.get(ID_identifier));
if(it==original_identifiers.end()) return;
assert(it->second!="");
expr.set(ID_identifier, it->second);
}
}
/*******************************************************************\
Function: goto_symex_statet::renaming_levelt::get_original_name
Inputs:
Outputs:
Purpose:
\*******************************************************************/
const irep_idt &goto_symex_statet::renaming_levelt::get_original_name(
const irep_idt &identifier) const
{
original_identifierst::const_iterator it=
original_identifiers.find(identifier);
if(it==original_identifiers.end()) return identifier;
return it->second;
}
/*******************************************************************\
Function: goto_symex_statet::get_original_name
@ -919,7 +1029,14 @@ void goto_symex_statet::get_original_name(typet &type) const
type.id()==ID_union ||
type.id()==ID_class)
{
// TODO
struct_union_typet &s_u_type=to_struct_union_type(type);
struct_union_typet::componentst &components=s_u_type.components();
for(struct_union_typet::componentst::iterator
it=components.begin();
it!=components.end();
++it)
get_original_name(it->type());
}
else if(type.id()==ID_pointer)
{
@ -929,7 +1046,7 @@ void goto_symex_statet::get_original_name(typet &type) const
/*******************************************************************\
Function: goto_symex_statet::renaming_levelt::get_original_name
Function: goto_symex_statet::get_l1_name
Inputs:
@ -939,45 +1056,16 @@ Function: goto_symex_statet::renaming_levelt::get_original_name
\*******************************************************************/
void goto_symex_statet::renaming_levelt::get_original_name(typet &type) const
void goto_symex_statet::get_l1_name(exprt &expr) const
{
// rename all the symbols back to their original name
// do not reset the type !
if(type.id()==ID_array)
{
get_original_name(type.subtype());
get_original_name(to_array_type(type).size());
}
else if(type.id()==ID_struct ||
type.id()==ID_union ||
type.id()==ID_class)
{
// TODO
}
else if(type.id()==ID_pointer)
{
get_original_name(type.subtype());
}
}
/*******************************************************************\
Function: goto_symex_statet::get_original_name
Inputs:
Outputs:
Purpose:
\*******************************************************************/
const irep_idt &goto_symex_statet::get_original_name(
const irep_idt &identifier) const
{
return level0.get_original_name(
level1.get_original_name(
level2.get_original_name(identifier)));
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
to_ssa_expr(expr).remove_level_2();
else
Forall_operands(it, expr)
get_l1_name(*it);
}
/*******************************************************************\

184
src/goto-symex/goto_symex_state.h
View File

@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/guard.h>
#include <util/std_expr.h>
#include <util/i2string.h>
#include <util/ssa_expr.h>
#include <pointer-analysis/value_set.h>
#include <goto-programs/goto_functions.h>
@ -45,97 +46,39 @@ public:
struct renaming_levelt
{
public:
virtual irep_idt current_name(const irep_idt &identifier) const=0;
virtual irep_idt name(const irep_idt &identifier, unsigned count) const=0;
virtual ~renaming_levelt() { }
typedef std::map<irep_idt, unsigned> current_namest;
typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned> > current_namest;
current_namest current_names;
void remove(const irep_idt &identifier) { current_names.erase(identifier); }
const irep_idt &get_original_name(const irep_idt &identifier) const;
void get_original_name(exprt &expr) const;
void get_original_name(typet &type) const;
void print(std::ostream &out) const;
unsigned current_count(const irep_idt &identifier) const;
irep_idt operator()(const irep_idt &identifier)
unsigned current_count(const irep_idt &identifier) const
{
// see if it's already renamed
if(is_renamed(identifier)) return identifier;
// record
irep_idt i=current_name(identifier);
original_identifiers[i]=identifier;
return i;
current_namest::const_iterator it=
current_names.find(identifier);
return it==current_names.end()?0:it->second.second;
}
inline void operator()(symbol_exprt &expr)
void increase_counter(const irep_idt &identifier)
{
expr.set_identifier(operator()(expr.get_identifier()));
}
irep_idt rename_identifier(const irep_idt &identifier, unsigned count)
{
current_names[identifier]=count;
irep_idt new_name=name(identifier, count);
original_identifiers[new_name]=identifier;
return new_name;
}
irep_idt increase_counter(const irep_idt &identifier)
{
return rename_identifier(identifier, current_names[identifier]+1);
}
inline bool is_renamed(const irep_idt &identifier) const
{
return original_identifiers.find(identifier)!=original_identifiers.end();
}
void restore_from(const current_namest &other)
{
for(current_namest::const_iterator
it=other.begin();
it!=other.end();
it++)
{
// could be done faster exploing ordering
current_names[it->first]=it->second;
}
assert(current_names.find(identifier)!=current_names.end());
++current_names[identifier].second;
}
void get_variables(std::set<irep_idt> &vars) const
void get_variables(hash_set_cont<ssa_exprt, irep_hash> &vars) const
{
for(current_namest::const_iterator it=current_names.begin();
it!=current_names.end();
it++)
vars.insert(it->first);
vars.insert(it->second.first);
}
protected:
original_identifierst original_identifiers;
};
// level 0 -- threads!
// renaming built for one particular interleaving
struct level0t:public renaming_levelt
{
public:
virtual irep_idt name(const irep_idt &identifier, unsigned thread_nr) const
{
return id2string(identifier)+"!"+i2string(thread_nr);
}
virtual irep_idt current_name(const irep_idt &identifier) const
{ // never called
assert(false);
return irep_idt();
}
irep_idt operator()(
const irep_idt &identifier,
void operator()(
ssa_exprt &ssa_expr,
const namespacet &ns,
unsigned thread_nr);
@ -148,26 +91,27 @@ public:
struct level1t:public renaming_levelt
{
public:
virtual irep_idt name(const irep_idt &identifier, unsigned frame) const
{
return id2string(identifier)+"@"+i2string(frame);
}
virtual irep_idt current_name(const irep_idt &identifier) const
{
// see if it's already renamed
if(is_renamed(identifier))
return identifier;
void operator()(ssa_exprt &ssa_expr);
// rename only if needed
const current_namest::const_iterator it=
current_names.find(identifier);
if(it==current_names.end())
return identifier;
else
return name(identifier, it->second);
void restore_from(const current_namest &other)
{
current_namest::iterator it=current_names.begin();
for(current_namest::const_iterator
ito=other.begin();
ito!=other.end();
++ito)
{
while(it!=current_names.end() && it->first<ito->first)
++it;
if(it==current_names.end() || ito->first<it->first)
current_names.insert(it, *ito);
else if(it!=current_names.end())
{
assert(it->first==ito->first);
it->second=ito->second;
++it;
}
}
}
level1t() { }
@ -178,22 +122,6 @@ public:
struct level2t:public renaming_levelt
{
public:
virtual irep_idt name(const irep_idt &identifier, unsigned count) const
{
return id2string(identifier)+"#"+i2string(count);
}
virtual irep_idt current_name(const irep_idt &identifier) const
{
// see if it's already renamed
if(is_renamed(identifier))
return identifier;
// _always_ rename
return name(identifier, current_count(identifier));
}
level2t() { }
virtual ~level2t() { }
} level2;
@ -216,14 +144,15 @@ public:
typedef enum { L0=0, L1=1, L2=2 } levelt;
// performs renaming _up to_ the given level
irep_idt rename_identifier(const irep_idt &identifier, const namespacet &ns, levelt level=L2);
void rename(exprt &expr, const namespacet &ns, levelt level=L2);
void rename(typet &type, const namespacet &ns, levelt level=L2);
void rename_address(exprt &expr, const namespacet &ns, levelt level);
void rename(
typet &type,
const irep_idt &l1_identifier,
const namespacet &ns,
levelt level=L2);
void assignment(
symbol_exprt &lhs, // L0/L1
ssa_exprt &lhs, // L0/L1
const exprt &rhs, // L2
const namespacet &ns,
bool rhs_is_simplified,
@ -234,10 +163,20 @@ public:
bool constant_propagation_reference(const exprt &expr) const;
// undoes all levels of renaming
const irep_idt &get_original_name(const irep_idt &identifier) const;
void get_original_name(exprt &expr) const;
void get_original_name(typet &type) const;
protected:
void rename_address(exprt &expr, const namespacet &ns, levelt level);
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2);
// only required for value_set.assign
void get_l1_name(exprt &expr) const;
// this maps L1 names to (L2) types
typedef hash_map_cont<irep_idt, typet, irep_id_hash> l1_typest;
l1_typest l1_types;
public:
// uses level 1 names, and is used to
// do dereferencing
value_sett value_set;
@ -263,25 +202,20 @@ public:
}
// the below replicate levelt2 member functions
void level2_get_variables(std::set<irep_idt> &vars) const
void level2_get_variables(hash_set_cont<ssa_exprt, irep_hash> &vars) const
{
for(level2t::current_namest::const_iterator
it=level2_current_names.begin();
it!=level2_current_names.end();
it++)
vars.insert(it->first);
vars.insert(it->second.first);
}
unsigned level2_current_count(const irep_idt &identifier) const
{
level2t::current_namest::const_iterator it=
level2_current_names.find(identifier);
return it==level2_current_names.end()?0:it->second;
}
irep_idt level2_current_name(const irep_idt &identifier) const
{
return id2string(identifier)+"#"+i2string(level2_current_count(identifier));
return it==level2_current_names.end()?0:it->second.second;
}
};
@ -305,8 +239,8 @@ public:
renaming_levelt::current_namest old_level1;
typedef std::set<irep_idt> local_variablest;
local_variablest local_variables;
typedef std::set<irep_idt> local_objectst;
local_objectst local_objects;
framet():
return_value(nil_exprt()),
@ -368,9 +302,9 @@ public:
// threads
unsigned atomic_section_id;
typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
typedef hash_map_cont<symbol_exprt, a_s_r_entryt, irep_hash> read_in_atomic_sectiont;
typedef hash_map_cont<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_sectiont;
typedef std::list<guardt> a_s_w_entryt;
typedef hash_map_cont<symbol_exprt, a_s_w_entryt, irep_hash> written_in_atomic_sectiont;
typedef hash_map_cont<ssa_exprt, a_s_w_entryt, irep_hash> written_in_atomic_sectiont;
read_in_atomic_sectiont read_in_atomic_section;
written_in_atomic_sectiont written_in_atomic_section;
@ -392,8 +326,8 @@ public:
typedef std::vector<threadt> threadst;
threadst threads;
bool l2_thread_read_encoding(symbol_exprt &expr, const namespacet &ns);
bool l2_thread_write_encoding(const symbol_exprt &expr, const namespacet &ns);
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
void switch_to_thread(unsigned t);
bool record_events;

20
src/goto-symex/partial_order_concurrency.cpp
View File

@ -93,9 +93,9 @@ void partial_order_concurrencyt::add_init_writes(
symex_target_equationt::SSA_stept &SSA_step=init_steps.back();
SSA_step.guard=true_exprt();
// no SSA index, thus nondet value
SSA_step.ssa_lhs=e_it->original_lhs_object;
SSA_step.original_lhs_object=e_it->original_lhs_object;
// no SSA L2 index, thus nondet value
SSA_step.ssa_lhs=e_it->ssa_lhs;
SSA_step.ssa_lhs.remove_level_2();
SSA_step.type=goto_trace_stept::SHARED_WRITE;
SSA_step.atomic_section_id=0;
SSA_step.source=e_it->source;
@ -238,9 +238,10 @@ Function: partial_order_concurrencyt::is_shared_write
bool partial_order_concurrencyt::is_shared_write(event_it event) const
{
if(!event->is_shared_write()) return false;
const irep_idt identifier=event->original_lhs_object.get_identifier();
if(identifier=="goto_symex::\\guard") return false;
const symbolt &symbol=ns.lookup(identifier);
const irep_idt obj_identifier=event->ssa_lhs.get_object_name();
if(obj_identifier=="goto_symex::\\guard") return false;
const symbolt &symbol=ns.lookup(obj_identifier);
return !symbol.is_thread_local;
}
@ -259,9 +260,10 @@ Function: partial_order_concurrencyt::is_shared_read
bool partial_order_concurrencyt::is_shared_read(event_it event) const
{
if(!event->is_shared_read()) return false;
const irep_idt identifier=event->original_lhs_object.get_identifier();
if(identifier=="goto_symex::\\guard") return false;
const symbolt &symbol=ns.lookup(identifier);
const irep_idt obj_identifier=event->ssa_lhs.get_object_name();
if(obj_identifier=="goto_symex::\\guard") return false;
const symbolt &symbol=ns.lookup(obj_identifier);
return !symbol.is_thread_local;
}

4
src/goto-symex/partial_order_concurrency.h
View File

@ -65,7 +65,9 @@ protected:
// produces an address ID for an event
inline irep_idt address(event_it event) const
{
return event->original_lhs_object.get_identifier();
ssa_exprt tmp=event->ssa_lhs;
tmp.remove_level_2();
return tmp.get_identifier();
}
// produce a clock symbol for some event

13
src/goto-symex/postcondition.cpp
View File

@ -175,8 +175,7 @@ void postconditiont::weaken(exprt &dest)
// we are lazy:
// if lhs is mentioned in dest, we use "true".
const irep_idt &lhs_identifier=
s.get_original_name(SSA_step.ssa_lhs.get_identifier());
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
if(is_used(dest, lhs_identifier))
dest=true_exprt();
@ -198,8 +197,7 @@ Function: postconditiont::strengthen
void postconditiont::strengthen(exprt &dest)
{
const irep_idt &lhs_identifier=
s.get_original_name(SSA_step.ssa_lhs.get_identifier());
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
if(!is_used(SSA_step.ssa_rhs, lhs_identifier))
{
@ -240,9 +238,14 @@ bool postconditiont::is_used(
assert(expr.operands().size()==1);
return is_used_address_of(expr.op0(), identifier);
}
else if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
return to_ssa_expr(expr).get_object_name()==identifier;
}
else if(expr.id()==ID_symbol)
{
return s.get_original_name(expr.get(ID_identifier))==identifier;
return expr.get(ID_identifier)==identifier;
}
else if(expr.id()==ID_dereference)
{

17
src/goto-symex/precondition.cpp
View File

@ -161,21 +161,11 @@ void preconditiont::compute_rec(exprt &dest)
assert(dest.operands().size()==1);
compute_address_of(dest.op0());
}
else if(dest.id()==ID_symbol)
{
if(dest.get(ID_identifier)==
s.get_original_name(SSA_step.ssa_lhs.get_identifier()))
{
dest=SSA_step.ssa_rhs;
s.get_original_name(dest);
}
}
else if(dest.id()==ID_dereference)
{
assert(dest.operands().size()==1);
const irep_idt &lhs_identifier=
s.get_original_name(SSA_step.ssa_lhs.get_identifier());
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
// aliasing may happen here
@ -204,6 +194,11 @@ void preconditiont::compute_rec(exprt &dest)
compute_rec(dest.op0());
}
}
else if(dest==SSA_step.ssa_lhs.get_original_expr())
{
dest=SSA_step.ssa_rhs;
s.get_original_name(dest);
}
else
Forall_operands(it, dest)
compute_rec(*it);

39
src/goto-symex/renaming_ns.h
View File

@ -1,39 +0,0 @@
/*******************************************************************\
Module:
Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
#ifndef CPROVER_GOTO_SYMEX_RENAMING_NS_H
#define CPROVER_GOTO_SYMEX_RENAMING_NS_H
#include <util/namespace.h>
class renaming_nst:public namespacet
{
public:
renaming_nst(
const namespacet &_ns,
class goto_symex_statet &_state):
namespacet(_ns),
state(_state)
{
}
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
{
return namespacet::lookup(state.get_original_name(name), symbol);
}
const symbolt &lookup(const irep_idt &name) const
{
return namespacet::lookup(state.get_original_name(name));
}
protected:
class goto_symex_statet &state;
};
#endif

10
src/goto-symex/slice_by_trace.cpp
View File

@ -309,9 +309,8 @@ void symex_slice_by_tracet::compute_ts_back(
if ((t[j].is_true()) || (t[j].is_false())) {
merge.push_back(t[j]);
} else {
exprt merge_sym =exprt(ID_symbol, typet(ID_bool));
merge_sym.set(ID_identifier, id2string(merge_identifier)+"#"+
i2string(merge_count++));
ssa_exprt merge_sym(merge_symbol);
merge_sym.set_level_2(merge_count++);
exprt t_copy (t[j]);
merge_map_back.push_back(t_copy);
std::set<exprt> empty_impls;
@ -571,8 +570,8 @@ void symex_slice_by_tracet::assign_merges(
size_t merge_count = (merge_map_back.size()) - 1;
for (std::vector<exprt>::reverse_iterator i = merge_map_back.rbegin();
i != merge_map_back.rend(); i++) {
symbol_exprt merge_sym(typet(ID_bool));
merge_sym.set_identifier(id2string(merge_identifier)+"#"+i2string(merge_count));
ssa_exprt merge_sym(merge_symbol);
merge_sym.set_level_2(merge_count);
merge_count--;
guardt t_guard;
t_guard.make_true();
@ -585,7 +584,6 @@ void symex_slice_by_tracet::assign_merges(
SSA_step.guard=t_guard.as_expr();
SSA_step.ssa_lhs=merge_sym;
SSA_step.original_lhs_object=merge_symbol;
SSA_step.ssa_rhs.swap(merge_copy);
SSA_step.assignment_type=symex_targett::HIDDEN;

47
src/goto-symex/symex_assign.cpp
View File

@ -19,6 +19,30 @@ Author: Daniel Kroening, kroening@kroening.com
/*******************************************************************\
Function: goto_symext::symex_assign_rec
Inputs:
Outputs:
Purpose:
\*******************************************************************/
void goto_symext::symex_assign_rec(
statet &state,
const code_assignt &code)
{
code_assignt deref_code=code;
clean_expr(deref_code.lhs(), state, true);
clean_expr(deref_code.rhs(), state, false);
symex_assign(state, deref_code);
}
/*******************************************************************\
Function: goto_symext::symex_assign
Inputs:
@ -153,8 +177,9 @@ void goto_symext::symex_assign_rec(
guardt &guard,
assignment_typet assignment_type)
{
if(lhs.id()==ID_symbol)
symex_assign_symbol(state, to_symbol_expr(lhs), full_lhs, rhs, guard, assignment_type);
if(lhs.id()==ID_symbol &&
lhs.get_bool(ID_C_SSA_symbol))
symex_assign_symbol(state, to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
else if(lhs.id()==ID_index)
symex_assign_array(state, to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
else if(lhs.id()==ID_member)
@ -228,7 +253,7 @@ Function: goto_symext::symex_assign_symbol
void goto_symext::symex_assign_symbol(
statet &state,
const symbol_exprt &lhs,
const ssa_exprt &lhs, // L1
const exprt &full_lhs,
const exprt &rhs,
guardt &guard,
@ -247,17 +272,10 @@ void goto_symext::symex_assign_symbol(
tmp_ssa_rhs.swap(ssa_rhs);
}
symbol_exprt original_lhs=lhs;
state.get_original_name(original_lhs);
const symbolt &symbol=ns.lookup(original_lhs);
if(symbol.is_auxiliary) assignment_type=symex_targett::HIDDEN;
state.rename(ssa_rhs, ns);
do_simplify(ssa_rhs);
symbol_exprt ssa_lhs=lhs;
state.rename(ssa_lhs, ns, goto_symex_statet::L1);
ssa_exprt ssa_lhs=lhs;
state.assignment(ssa_lhs, ssa_rhs, ns, options.get_bool_option("simplify"), constant_propagation);
exprt ssa_full_lhs=full_lhs;
@ -271,10 +289,13 @@ void goto_symext::symex_assign_symbol(
tmp_guard.append(guard);
// do the assignment
const symbolt &symbol=ns.lookup(ssa_lhs.get_original_expr());
if(symbol.is_auxiliary) assignment_type=symex_targett::HIDDEN;
target.assignment(
tmp_guard.as_expr(),
ssa_lhs, original_lhs,
ssa_full_lhs, add_to_lhs(full_lhs, original_lhs),
ssa_lhs,
ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
ssa_rhs,
state.source,
assignment_type);

15
src/goto-symex/symex_atomic_section.cpp
View File

@ -66,9 +66,8 @@ void goto_symext::symex_atomic_end(statet &state)
r_it!=state.read_in_atomic_section.end();
++r_it)
{
symbol_exprt r=r_it->first;
r.set_identifier(
state.level2.name(r.get_identifier(), r_it->second.first));
ssa_exprt r=r_it->first;
r.set_level_2(r_it->second.first);
// guard is the disjunction over reads
assert(!r_it->second.second.empty());
@ -81,12 +80,9 @@ void goto_symext::symex_atomic_end(statet &state)
exprt read_guard_expr=read_guard.as_expr();
do_simplify(read_guard_expr);
symbol_exprt original_symbol=r_it->first;
state.get_original_name(original_symbol);
target.shared_read(
read_guard_expr,
r,
original_symbol,
atomic_section_id,
state.source);
}
@ -96,8 +92,8 @@ void goto_symext::symex_atomic_end(statet &state)
w_it!=state.written_in_atomic_section.end();
++w_it)
{
symbol_exprt w=w_it->first;
state.level2(w);
ssa_exprt w=w_it->first;
w.set_level_2(state.level2.current_count(w.get_identifier()));
// guard is the disjunction over writes
assert(!w_it->second.empty());
@ -110,12 +106,9 @@ void goto_symext::symex_atomic_end(statet &state)
exprt write_guard_expr=write_guard.as_expr();
do_simplify(write_guard_expr);
symbol_exprt original_symbol=w_it->first;
state.get_original_name(original_symbol);
target.shared_write(
write_guard_expr,
w,
original_symbol,
atomic_section_id,
state.source);
}

28
src/goto-symex/symex_builtin_functions.cpp
View File

@ -133,12 +133,10 @@ void goto_symext::symex_malloc(
new_symbol_table.add(size_symbol);
guardt guard;
symex_assign_rec(
state, size_symbol.symbol_expr(), nil_exprt(), size, guard,
symex_targett::HIDDEN);
code_assignt assignment(size_symbol.symbol_expr(), size);
size=assignment.lhs();
size=size_symbol.symbol_expr();
symex_assign_rec(state, assignment);
}
}
@ -173,10 +171,7 @@ void goto_symext::symex_malloc(
if(rhs.type()!=lhs.type())
rhs.make_typecast(lhs.type());
state.rename(rhs, ns);
guardt guard;
symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
symex_assign_rec(state, code_assignt(lhs, rhs));
}
/*******************************************************************\
@ -198,8 +193,9 @@ irep_idt get_symbol(const exprt &src)
else if(src.id()==ID_address_of)
{
exprt op=to_address_of_expr(src).object();
if(op.id()==ID_symbol)
return to_symbol_expr(op).get_identifier();
if(op.id()==ID_symbol &&
op.get_bool(ID_C_SSA_symbol))
return to_ssa_expr(op).get_object_name();
else
return irep_idt();
}
@ -226,8 +222,6 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
if(id!=irep_idt())
{
id=state.get_original_name(id);
// strip last name off id to get function name
std::size_t pos=id2string(id).rfind("::");
if(pos!=std::string::npos)
@ -252,8 +246,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next(
}
}
guardt guard;
symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, symex_targett::STATE);
symex_assign_rec(state, code_assignt(lhs, rhs));
}
/*******************************************************************\
@ -488,10 +481,7 @@ void goto_symext::symex_cpp_new(
else
rhs.copy_to_operands(symbol.symbol_expr());
state.rename(rhs, ns);
guardt guard;
symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, symex_targett::STATE);
symex_assign_rec(state, code_assignt(lhs, rhs));
}
/*******************************************************************\

18
src/goto-symex/symex_clean_expr.cpp
View File

@ -60,6 +60,15 @@ void goto_symext::process_array_expr_rec(
expr.swap(tmp);
process_array_expr_rec(expr, type);
}
else if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol) &&
to_ssa_expr(expr).get_original_expr().id()==ID_index)
{
const ssa_exprt &ssa=to_ssa_expr(expr);
const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
exprt tmp=index_expr.array();
expr.swap(tmp);
}
else
Forall_operands(it, expr)
process_array_expr_rec(*it, it->type());
@ -122,6 +131,15 @@ void goto_symext::process_array_expr(exprt &expr)
expr.swap(tmp);
process_array_expr(expr);
}
else if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol) &&
to_ssa_expr(expr).get_original_expr().id()==ID_index)
{
const ssa_exprt &ssa=to_ssa_expr(expr);
const index_exprt &index_expr=to_index_expr(ssa.get_original_expr());
exprt tmp=index_expr.array();
expr.swap(tmp);
}
else
Forall_operands(it, expr)
process_array_expr(*it);

30
src/goto-symex/symex_dead.cpp
View File

@ -43,19 +43,9 @@ void goto_symext::symex_dead(statet &state)
// We increase the L2 renaming to make these non-deterministic.
// We also prevent propagation of old values.
const irep_idt &identifier=
to_symbol_expr(code.op0()).get_identifier();
const irep_idt l1_identifier=
state.rename_identifier(identifier, ns, goto_symex_statet::L1);
// prevent propagation
state.propagation.remove(l1_identifier);
ssa_exprt ssa(to_symbol_expr(code.op0()));
state.rename(ssa, ns, goto_symex_statet::L1);
// L2 renaming
unsigned new_count=state.level2.current_count(l1_identifier)+1;
state.level2.rename_identifier(l1_identifier, new_count);
// in case of pointers, put something into the value set
if(ns.follow(code.op0().type()).id()==ID_pointer)
{
@ -74,10 +64,18 @@ void goto_symext::symex_dead(statet &state)
else
rhs=exprt(ID_invalid);
symbol_exprt l1_lhs;
l1_lhs.type()=code.op0().type();
l1_lhs.set_identifier(l1_identifier);
state.rename(rhs, ns, goto_symex_statet::L1);
state.value_set.assign(l1_lhs, rhs, ns, true, false);
state.value_set.assign(ssa, rhs, ns, true, false);
}
ssa_exprt ssa_lhs=to_ssa_expr(ssa);
const irep_idt &l1_identifier=ssa_lhs.get_identifier();
// prevent propagation
state.propagation.remove(l1_identifier);
// L2 renaming
if(state.level2.current_names.find(l1_identifier)!=
state.level2.current_names.end())
state.level2.increase_counter(l1_identifier);
}

66
src/goto-symex/symex_decl.cpp
View File

@ -43,27 +43,39 @@ void goto_symext::symex_decl(statet &state)
if(code.op0().id()!=ID_symbol)
throw "decl expects symbol as first operand";
symex_decl(state, to_symbol_expr(code.op0()));
}
/*******************************************************************\
Function: goto_symext::symex_decl
Inputs:
Outputs:
Purpose:
\*******************************************************************/
void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
{
// We increase the L2 renaming to make these non-deterministic.
// We also prevent propagation of old values.
const irep_idt &identifier=
to_symbol_expr(code.op0()).get_identifier();
const irep_idt l1_identifier=
state.rename_identifier(identifier, ns, goto_symex_statet::L1);
// prevent propagation
state.propagation.remove(l1_identifier);
ssa_exprt ssa(expr);
state.rename(ssa, ns, goto_symex_statet::L1);
const irep_idt &l1_identifier=ssa.get_identifier();
// rename type to L2
state.rename(ssa.type(), l1_identifier, ns);
ssa.update_type();
// L2 renaming
unsigned new_count=state.level2.current_count(l1_identifier)+1;
state.level2.rename_identifier(l1_identifier, new_count);
// in case of pointers, put something into the value set
if(ns.follow(code.op0().type()).id()==ID_pointer)
if(ns.follow(expr.type()).id()==ID_pointer)
{
exprt failed=
get_failed_symbol(to_symbol_expr(code.op0()), ns);
get_failed_symbol(expr, ns);
exprt rhs;
@ -71,34 +83,38 @@ void goto_symext::symex_decl(statet &state)
{
address_of_exprt address_of_expr;
address_of_expr.object()=failed;
address_of_expr.type()=code.op0().type();
address_of_expr.type()=expr.type();
rhs=address_of_expr;
}
else
rhs=exprt(ID_invalid);
symbol_exprt l1_lhs;
l1_lhs.type()=code.op0().type();
l1_lhs.set_identifier(l1_identifier);
state.rename(rhs, ns, goto_symex_statet::L1);
state.value_set.assign(l1_lhs, rhs, ns, true, false);
state.value_set.assign(ssa, rhs, ns, true, false);
}
// record the declaration
symbol_exprt original_lhs=to_symbol_expr(code.op0());
symbol_exprt ssa_lhs=original_lhs;
state.rename(ssa_lhs, ns);
// prevent propagation
state.propagation.remove(l1_identifier);
// L2 renaming
// inlining may yield multiple declarations of the same identifier
// within the same L1 context
if(state.level2.current_names.find(l1_identifier)==
state.level2.current_names.end())
state.level2.current_names[l1_identifier]=std::make_pair(ssa, 0);
state.level2.increase_counter(l1_identifier);
state.rename(ssa, ns);
// we hide the declaration of auxiliary variables
// and if the statement itself is hidden
bool hidden=
ns.lookup(original_lhs.get_identifier()).is_auxiliary ||
ns.lookup(expr.get_identifier()).is_auxiliary ||
state.top().hidden_function ||
state.source.pc->source_location.get_hide();
target.decl(
state.guard.as_expr(),
ssa_lhs, original_lhs,
ssa,
state.source,
hidden?symex_targett::HIDDEN:symex_targett::STATE);
}

31
src/goto-symex/symex_dereference.cpp
View File

@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include <ansi-c/c_types.h>
#include "goto_symex.h"
#include "renaming_ns.h"
#include "symex_dereference_state.h"
/*******************************************************************\
@ -227,8 +226,28 @@ exprt goto_symext::address_arithmetic(
if(ns.follow(result.type()).id()==ID_array && !keep_array)
result=index_exprt(result, gen_zero(index_type()));
// TODO: consider pointer offset for ID_SSA_symbol
result=address_of_exprt(result);
// handle field-sensitive SSA symbol
mp_integer offset=0;
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
offset=compute_pointer_offset(expr, ns);
assert(offset>=0);
}
if(offset>0)
{
byte_extract_exprt be(byte_extract_id());
be.type()=expr.type();
be.op()=to_ssa_expr(expr).get_l1_object();
be.offset()=from_integer(offset, index_type());
result=address_arithmetic(be, state, guard, keep_array);
do_simplify(result);
}
else
result=address_of_exprt(result);
}
else
throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
@ -271,10 +290,9 @@ void goto_symext::dereference_rec(
// we need to set up some elaborate call-backs
symex_dereference_statet symex_dereference_state(*this, state);
renaming_nst renaming_ns(ns, state);
value_set_dereferencet dereference(
renaming_ns,
ns,
new_symbol_table,
options,
symex_dereference_state);
@ -386,4 +404,7 @@ void goto_symext::dereference(
// start the recursion!
guardt guard;
dereference_rec(expr, state, guard, write);
// dereferencing may introduce new symbol_exprt
// (like __CPROVER_memory)
state.rename(expr, ns, goto_symex_statet::L1);
}

43
src/goto-symex/symex_dereference_state.cpp
View File

@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
#include <util/symbol_table.h>
#include "symex_dereference_state.h"
#include "renaming_ns.h"
/*******************************************************************\
@ -46,22 +45,50 @@ bool symex_dereference_statet::has_failed_symbol(
const exprt &expr,
const symbolt *&symbol)
{
renaming_nst renaming_ns(goto_symex.ns, state);
const namespacet &ns=goto_symex.ns;
if(expr.id()==ID_symbol)
if(expr.id()==ID_symbol &&
expr.get_bool(ID_C_SSA_symbol))
{
const ssa_exprt &ssa_expr=to_ssa_expr(expr);
if(ssa_expr.get_original_expr().id()!=ID_symbol)
return false;
const symbolt &ptr_symbol=
ns.lookup(to_ssa_expr(expr).get_object_name());
const irep_idt &failed_symbol=
ptr_symbol.type.get("#failed_symbol");
if(failed_symbol!="" &&
!ns.lookup(failed_symbol, symbol))
{
symbolt sym=*symbol;
symbolt *sym_ptr=0;
symbol_exprt sym_expr=sym.symbol_expr();
state.rename(sym_expr, ns, goto_symex_statet::L1);
sym.name=to_ssa_expr(sym_expr).get_identifier();
goto_symex.new_symbol_table.move(sym, sym_ptr);
symbol=sym_ptr;
return true;
}
}
else if(expr.id()==ID_symbol)
{
const symbolt &ptr_symbol=
renaming_ns.lookup(to_symbol_expr(expr).get_identifier());
ns.lookup(to_symbol_expr(expr).get_identifier());
const irep_idt &failed_symbol=
ptr_symbol.type.get("#failed_symbol");
if(failed_symbol!="" &&
!renaming_ns.lookup(failed_symbol, symbol))
!ns.lookup(failed_symbol, symbol))
{
symbolt sym=*symbol;
symbolt *sym_ptr=0;
sym.name=state.rename_identifier(sym.name, renaming_ns, goto_symex_statet::L1);
symbol_exprt sym_expr=sym.symbol_expr();
state.rename(sym_expr, ns, goto_symex_statet::L1);
sym.name=to_ssa_expr(sym_expr).get_identifier();
goto_symex.new_symbol_table.move(sym, sym_ptr);
symbol=sym_ptr;
return true;
@ -87,9 +114,7 @@ void symex_dereference_statet::get_value_set(
const exprt &expr,
value_setst::valuest &value_set)
{
renaming_nst renaming_ns(goto_symex.ns, state);
state.value_set.get_value_set(expr, value_set, renaming_ns);
state.value_set.get_value_set(expr, value_set, goto_symex.ns);
#if 0
std::cout << "**************************\n";

71
src/goto-symex/symex_function_call.cpp
View File

@ -136,15 +136,7 @@ void goto_symext::parameter_assignments(
}
}
guardt guard;
state.rename(lhs, ns, goto_symex_statet::L1);
symex_targett::assignment_typet assignment_type=
goto_function.is_hidden()?
symex_targett::HIDDEN_ACTUAL_PARAMETER:
symex_targett::VISIBLE_ACTUAL_PARAMETER;
symex_assign_symbol(state, lhs, nil_exprt(), rhs, guard, assignment_type);
symex_assign_rec(state, code_assignt(lhs, rhs));
}
it1++;
@ -173,15 +165,7 @@ void goto_symext::parameter_assignments(
symbol_exprt lhs=symbol_exprt(id, it1->type());
guardt guard;
state.rename(lhs, ns, goto_symex_statet::L1);
symex_targett::assignment_typet assignment_type=
goto_function.is_hidden()?
symex_targett::HIDDEN_ACTUAL_PARAMETER:
symex_targett::VISIBLE_ACTUAL_PARAMETER;
symex_assign_symbol(state, lhs, nil_exprt(), *it1, guard, assignment_type);
symex_assign_rec(state, code_assignt(lhs, *it1));
}
}
else if(it1!=arguments.end())
@ -328,9 +312,8 @@ void goto_symext::symex_function_call_code(
{
side_effect_expr_nondett rhs(call.lhs().type());
rhs.add_source_location()=call.source_location();
state.rename(rhs, ns, goto_symex_statet::L1);
code_assignt code(call.lhs(), rhs);
symex_assign(state, to_code_assign(code)); /* TODO: clean_expr? */
symex_assign_rec(state, code);
}
state.source.pc++;
@ -400,11 +383,23 @@ void goto_symext::pop_frame(statet &state)
state.level1.restore_from(frame.old_level1);
// clear function-locals from L2 renaming
for(statet::framet::local_variablest::const_iterator
it=frame.local_variables.begin();
it!=frame.local_variables.end();
it++)
state.level2.remove(*it);
for(goto_symex_statet::renaming_levelt::current_namest::iterator
c_it=state.level2.current_names.begin();
c_it!=state.level2.current_names.end();
) // no ++c_it
{
const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
// could use iteration over local_objects as l1_o_id is prefix
if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
{
++c_it;
continue;
}
goto_symex_statet::renaming_levelt::current_namest::iterator
cur=c_it;
++c_it;
state.level2.current_names.erase(cur);
}
}
state.pop_frame();
@ -467,7 +462,9 @@ void goto_symext::locality(
it++)
{
// get L0 name
irep_idt l0_name=state.rename_identifier(*it, ns, goto_symex_statet::L0);
ssa_exprt ssa(ns.lookup(*it).symbol_expr());
state.rename(ssa, ns, goto_symex_statet::L0);
const irep_idt l0_name=ssa.get_identifier();
// save old L1 name for popping the frame
statet::level1t::current_namest::const_iterator c_it=
@ -480,19 +477,23 @@ void goto_symext::locality(
// identifiers may be shared among functions
// (e.g., due to inlining or other code restructuring)
irep_idt l1_name;
state.level1.current_names[l0_name]=
std::make_pair(ssa, frame_nr);
state.rename(ssa, ns, goto_symex_statet::L1);
irep_idt l1_name=ssa.get_identifier();
unsigned offset=0;
do
while(state.l1_history.find(l1_name)!=state.l1_history.end())
{
state.level1.rename_identifier(l0_name, frame_nr+offset);
l1_name=state.level1(l0_name);
offset++;
state.level1.increase_counter(l0_name);
ssa.set_level_1(frame_nr+offset);
l1_name=ssa.get_identifier();
++offset;
}
while(state.l1_history.find(l1_name)!=state.l1_history.end());
// now unique -- store
frame.local_variables.insert(l1_name);
frame.local_objects.insert(l1_name);
state.l1_history.insert(l1_name);
}
}
@ -522,8 +523,6 @@ void goto_symext::return_assignment(statet &state)
if(code.operands().size()==1)
{
exprt value=code.op0();
clean_expr(value, state, false);
if(frame.return_value.is_not_nil())
{
@ -536,7 +535,7 @@ void goto_symext::return_assignment(statet &state)
"assignment.lhs().type():\n"+assignment.lhs().type().pretty()+"\n"+
"assignment.rhs().type():\n"+assignment.rhs().type().pretty();
symex_assign(state, assignment);
symex_assign_rec(state, assignment);
}
}
else

35
src/goto-symex/symex_goto.cpp
View File

@ -141,7 +141,7 @@ void goto_symext::symex_goto(statet &state)
exprt new_rhs=new_guard;
new_rhs.make_not();
symbol_exprt new_lhs=guard_symbol_expr;
ssa_exprt new_lhs(guard_symbol_expr);
state.rename(new_lhs, ns, goto_symex_statet::L1);
state.assignment(new_lhs, new_rhs, ns, true, false);
@ -149,7 +149,7 @@ void goto_symext::symex_goto(statet &state)
target.assignment(
guard.as_expr(),
new_lhs, guard_symbol_expr, new_lhs, guard_symbol_expr,
new_lhs, new_lhs, guard_symbol_expr,
new_rhs,
original_source,
symex_targett::GUARD);
@ -297,19 +297,20 @@ void goto_symext::phi_function(
statet &dest_state)
{
// go over all variables to see what changed
std::set<irep_idt> variables;
hash_set_cont<ssa_exprt, irep_hash> variables;
goto_state.level2_get_variables(variables);
dest_state.level2.get_variables(variables);
for(std::set<irep_idt>::const_iterator
for(hash_set_cont<ssa_exprt, irep_hash>::const_iterator
it=variables.begin();
it!=variables.end();
it++)
{
const irep_idt l1_identifier=*it;
const irep_idt l1_identifier=it->get_identifier();
const irep_idt &obj_identifier=it->get_object_name();
if(l1_identifier==guard_identifier)
if(obj_identifier==guard_identifier)
continue; // just a guard, don't bother
if(goto_state.level2_current_count(l1_identifier)==
@ -318,12 +319,9 @@ void goto_symext::phi_function(
// changed!
irep_idt original_identifier=
dest_state.get_original_name(l1_identifier);
// shared variables are renamed on every access anyway, we don't need to
// merge anything
const symbolt &symbol=ns.lookup(original_identifier);
const symbolt &symbol=ns.lookup(obj_identifier);
// shared?
if(dest_state.atomic_section_id==0 &&
@ -340,11 +338,7 @@ void goto_symext::phi_function(
continue;
#endif
// get type (may need renaming)
typet type=symbol.type;
dest_state.rename(type, ns);
exprt goto_state_rhs, dest_state_rhs;
exprt goto_state_rhs=*it, dest_state_rhs=*it;
{
goto_symex_statet::propagationt::valuest::const_iterator p_it=
@ -353,7 +347,7 @@ void goto_symext::phi_function(
if(p_it!=goto_state.propagation.values.end())
goto_state_rhs=p_it->second;
else
goto_state_rhs=symbol_exprt(goto_state.level2_current_name(l1_identifier), type);
to_ssa_expr(goto_state_rhs).set_level_2(goto_state.level2_current_count(l1_identifier));
}
{
@ -363,7 +357,7 @@ void goto_symext::phi_function(
if(p_it!=dest_state.propagation.values.end())
dest_state_rhs=p_it->second;
else
dest_state_rhs=symbol_exprt(dest_state.level2.current_name(l1_identifier), type);
to_ssa_expr(dest_state_rhs).set_level_2(dest_state.level2.current_count(l1_identifier));
}
exprt rhs;
@ -379,12 +373,11 @@ void goto_symext::phi_function(
// this gets the diff between the guards
tmp_guard-=dest_state.guard;
rhs=if_exprt(tmp_guard.as_expr(), goto_state_rhs, dest_state_rhs, type);
rhs=if_exprt(tmp_guard.as_expr(), goto_state_rhs, dest_state_rhs);
do_simplify(rhs);
}
symbol_exprt lhs=symbol.symbol_expr();
symbol_exprt new_lhs=symbol_exprt(l1_identifier, type);
ssa_exprt new_lhs=*it;
const bool record_events=dest_state.record_events;
dest_state.record_events=false;
dest_state.assignment(new_lhs, rhs, ns, true, true);
@ -392,7 +385,7 @@ void goto_symext::phi_function(
target.assignment(
true_exprt(),
new_lhs, lhs, new_lhs, lhs,
new_lhs, new_lhs, new_lhs.get_original_expr(),
rhs,
dest_state.source,
symex_targett::PHI);

14
src/goto-symex/symex_main.cpp
View File

@ -131,8 +131,9 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
// we keep the quantified variable unique by means of L2 renaming
assert(expr.operands().size()==2);
assert(expr.op0().id()==ID_symbol);
irep_idt identifier=to_symbol_expr(expr.op0()).get_identifier();
state.level2.increase_counter(state.level1(identifier));
symbol_exprt tmp0=
to_symbol_expr(to_ssa_expr(expr.op0()).get_original_expr());
symex_decl(state, tmp0);
exprt tmp=expr.op1();
expr.swap(tmp);
}
@ -324,14 +325,7 @@ void goto_symext::symex_step(
case ASSIGN:
if(!state.guard.is_false())
{
code_assignt deref_code=to_code_assign(instruction.code);
clean_expr(deref_code.lhs(), state, true);
clean_expr(deref_code.rhs(), state, false);
symex_assign(state, deref_code);
}
symex_assign_rec(state, to_code_assign(instruction.code));
state.source.pc++;
break;

9
src/goto-symex/symex_other.cpp
View File

@ -101,10 +101,13 @@ void goto_symext::symex_other(
clean_code.op0()=d0;
clean_code.op1()=d1;
clean_expr(clean_code, state, false);
clean_expr(clean_code.op0(), state, true);
clean_expr(clean_code.op1(), state, false);
process_array_expr(clean_code.op0());
clean_expr(clean_code.op0(), state, true);
process_array_expr(clean_code.op1());
clean_expr(clean_code.op1(), state, false);
if(!base_type_eq(clean_code.op0().type(),
@ -136,9 +139,11 @@ void goto_symext::symex_other(
clean_code.op0()=d0;
clean_expr(clean_code, state, false);
clean_expr(clean_code.op0(), state, true);
clean_expr(clean_code.op1(), state, false);
process_array_expr(clean_code.op0());
clean_expr(clean_code.op0(), state, true);
const typet &op0_type=ns.follow(clean_code.op0().type());

56
src/goto-symex/symex_start_thread.cpp
View File

@ -52,7 +52,7 @@ void goto_symext::symex_start_thread(statet &state)
new_thread.pc=thread_target;
new_thread.guard=state.guard;
new_thread.call_stack.push_back(state.top());
new_thread.call_stack.back().local_variables.clear();
new_thread.call_stack.back().local_objects.clear();
new_thread.call_stack.back().goto_state_map.clear();
#if 0
new_thread.abstract_events=&(target.new_thread(cur_thread.abstract_events));
@ -61,29 +61,36 @@ void goto_symext::symex_start_thread(statet &state)
// create a copy of the local variables for the new thread
statet::framet &frame=state.top();
for(std::set<irep_idt>::const_iterator
it=frame.local_variables.begin();
it!=frame.local_variables.end();
it++)
for(goto_symex_statet::renaming_levelt::current_namest::const_iterator
c_it=state.level2.current_names.begin();
c_it!=state.level2.current_names.end();
++c_it)
{
// get original name
irep_idt original_name=state.get_original_name(*it);
// get L0 name for current thread
irep_idt l0_name=state.level0.rename_identifier(original_name, t);
// setup L1 name
state.level1.rename_identifier(l0_name, 0);
irep_idt l1_name=state.level1.current_name(l0_name);
state.l1_history.insert(l1_name);
const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
// could use iteration over local_objects as l1_o_id is prefix
if(frame.local_objects.find(l1_o_id)==frame.local_objects.end())
continue;
// get original name
ssa_exprt lhs(c_it->second.first.get_original_expr());
// get L0 name for current thread
lhs.set_level_0(t);
// setup L1 name
if(!state.level1.current_names.insert(
std::make_pair(lhs.get_l1_object_identifier(),
std::make_pair(lhs, 0))).second)
assert(false);
state.rename(lhs, ns, goto_symex_statet::L1);
const irep_idt l1_name=lhs.get_l1_object_identifier();
// store it
state.l1_history.insert(l1_name);
new_thread.call_stack.back().local_objects.insert(l1_name);
// make sure the L2 name with current index exists for future renaming
state.level2(l1_name);
// make copy
typet type=ns.lookup(original_name).type;
symbol_exprt lhs(l1_name, type);
symbol_exprt rhs(*it, type);
ssa_exprt rhs=c_it->second.first;
state.rename(rhs, ns);
guardt guard;
symex_assign_symbol(state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
@ -102,13 +109,10 @@ void goto_symext::symex_start_thread(statet &state)
continue;
// get original name
irep_idt original_name=symbol.name;
ssa_exprt lhs(symbol.symbol_expr());
// get L0 name for current thread
irep_idt l0_name=state.level0.rename_identifier(original_name, t);
symbol_exprt lhs=symbol.symbol_expr();
lhs.set_identifier(l0_name);
lhs.set_level_0(t);
exprt rhs=symbol.value;
if(rhs.is_nil())

16
src/goto-symex/symex_target.h
View File

@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
#include <goto-programs/goto_program.h>
class ssa_exprt;
class symbol_exprt;
class symex_targett
@ -57,24 +58,21 @@ public:
// read event
virtual void shared_read(
const exprt &guard,
const symbol_exprt &ssa_rhs,
const symbol_exprt &original_rhs,
const ssa_exprt &ssa_rhs,
unsigned atomic_section_id,
const sourcet &source)=0;
// write event
virtual void shared_write(
const exprt &guard,
const symbol_exprt &ssa_rhs,
const symbol_exprt &original_rhs,
const ssa_exprt &ssa_rhs,
unsigned atomic_section_id,
const sourcet &source)=0;
// write event - lhs must be symbol
virtual void assignment(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const exprt &ssa_full_lhs,
const exprt &original_full_lhs,
const exprt &ssa_rhs,
@ -84,16 +82,14 @@ public:
// declare fresh variable - lhs must be symbol
virtual void decl(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source,
assignment_typet assignment_type)=0;
// note the death of a variable - lhs must be symbol
virtual void dead(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source)=0;
// record a function call

22
src/goto-symex/symex_target_equation.cpp
View File

@ -67,8 +67,7 @@ Function: symex_target_equationt::shared_read
void symex_target_equationt::shared_read(
const exprt &guard,
const symbol_exprt &ssa_object,
const symbol_exprt &original_object,
const ssa_exprt &ssa_object,
unsigned atomic_section_id,
const sourcet &source)
{
@ -77,7 +76,6 @@ void symex_target_equationt::shared_read(
SSA_step.guard=guard;
SSA_step.ssa_lhs=ssa_object;
SSA_step.original_lhs_object=original_object;
SSA_step.type=goto_trace_stept::SHARED_READ;
SSA_step.atomic_section_id=atomic_section_id;
SSA_step.source=source;
@ -99,8 +97,7 @@ Function: symex_target_equationt::shared_write
void symex_target_equationt::shared_write(
const exprt &guard,
const symbol_exprt &ssa_object,
const symbol_exprt &original_object,
const ssa_exprt &ssa_object,
unsigned atomic_section_id,
const sourcet &source)
{
@ -109,7 +106,6 @@ void symex_target_equationt::shared_write(
SSA_step.guard=guard;
SSA_step.ssa_lhs=ssa_object;
SSA_step.original_lhs_object=original_object;
SSA_step.type=goto_trace_stept::SHARED_WRITE;
SSA_step.atomic_section_id=atomic_section_id;
SSA_step.source=source;
@ -235,8 +231,7 @@ Function: symex_target_equationt::assignment
void symex_target_equationt::assignment(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const exprt &ssa_full_lhs,
const exprt &original_full_lhs,
const exprt &ssa_rhs,
@ -250,7 +245,6 @@ void symex_target_equationt::assignment(
SSA_step.guard=guard;
SSA_step.ssa_lhs=ssa_lhs;
SSA_step.original_lhs_object=original_lhs_object;
SSA_step.ssa_full_lhs=ssa_full_lhs;
SSA_step.original_full_lhs=original_full_lhs;
SSA_step.ssa_rhs=ssa_rhs;
@ -279,8 +273,7 @@ Function: symex_target_equationt::decl
void symex_target_equationt::decl(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source,
assignment_typet assignment_type)
{
@ -292,8 +285,7 @@ void symex_target_equationt::decl(
SSA_step.guard=guard;
SSA_step.ssa_lhs=ssa_lhs;
SSA_step.ssa_full_lhs=ssa_lhs;
SSA_step.original_lhs_object=original_lhs_object;
SSA_step.original_full_lhs=original_lhs_object;
SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
SSA_step.type=goto_trace_stept::DECL;
SSA_step.source=source;
SSA_step.hidden=(assignment_type!=STATE);
@ -319,8 +311,7 @@ Function: symex_target_equationt::dead
void symex_target_equationt::dead(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source)
{
// we currently don't record these
@ -946,7 +937,6 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
merge_irep(SSA_step.guard);
merge_irep(SSA_step.ssa_lhs);
merge_irep(SSA_step.original_lhs_object);
merge_irep(SSA_step.ssa_full_lhs);
merge_irep(SSA_step.original_full_lhs);
merge_irep(SSA_step.ssa_rhs);

20
src/goto-symex/symex_target_equation.h
View File

@ -34,24 +34,21 @@ public:
// read event
virtual void shared_read(
const exprt &guard,
const symbol_exprt &ssa_object,
const symbol_exprt &original_object,
const ssa_exprt &ssa_object,
unsigned atomic_section_id,
const sourcet &source);
// write event
virtual void shared_write(
const exprt &guard,
const symbol_exprt &ssa_object,
const symbol_exprt &original_object,
const ssa_exprt &ssa_object,
unsigned atomic_section_id,
const sourcet &source);
// assignment to a variable - lhs must be symbol
virtual void assignment(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs,
const ssa_exprt &ssa_lhs,
const exprt &ssa_full_lhs,
const exprt &original_full_lhs,
const exprt &ssa_rhs,
@ -61,16 +58,14 @@ public:
// declare fresh variable - lhs must be symbol
virtual void decl(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source,
assignment_typet assignment_type);
// note the death of a variable - lhs must be symbol
virtual void dead(
const exprt &guard,
const symbol_exprt &ssa_lhs,
const symbol_exprt &original_lhs_object,
const ssa_exprt &ssa_lhs,
const sourcet &source);
// record a function call
@ -199,7 +194,7 @@ public:
literalt guard_literal;
// for ASSIGNMENT and DECL
symbol_exprt ssa_lhs, original_lhs_object;
ssa_exprt ssa_lhs;
exprt ssa_full_lhs, original_full_lhs;
exprt ssa_rhs;
assignment_typet assignment_type;
@ -228,8 +223,7 @@ public:
type(goto_trace_stept::NONE),
hidden(false),
guard(static_cast<const exprt &>(get_nil_irep())),
ssa_lhs(static_cast<const symbol_exprt &>(get_nil_irep())),
original_lhs_object(static_cast<const symbol_exprt &>(get_nil_irep())),
ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
ssa_rhs(static_cast<const exprt &>(get_nil_irep())),

2
src/path-symex/build_goto_trace.cpp
View File

@ -57,7 +57,7 @@ void build_goto_trace(
case DECL:
trace_step.type=goto_trace_stept::DECL;
trace_step.full_lhs=step.full_lhs;
trace_step.lhs_object=to_symbol_expr(step.full_lhs);
trace_step.lhs_object=ssa_exprt(step.full_lhs);
trace_step.full_lhs_value=decision_procedure.get(step.ssa_lhs);
break;

5
src/util/ssa_expr.h
View File

@ -32,6 +32,11 @@ public:
update_identifier();
}
inline void update_type()
{
static_cast<exprt &>(add(ID_expression)).type()=type();
}
inline const exprt &get_original_expr() const
{
return static_cast<const exprt &>(find(ID_expression));