Skip to content

Assignment typet strong typing and UB fix #864

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

Closed
wants to merge 2 commits into from
Closed

Assignment typet strong typing and UB fix #864

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7d7147a
Make assignment_typet into an enum class
reuk Apr 24, 2017
1043242
Initialise variables in symex_target_equation.h
reuk Apr 24, 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
4 changes: 2 additions & 2 deletions src/cbmc/counterexample_beautification.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ void counterexample_beautificationt::get_minimization_list(
it!=equation.SSA_steps.end(); it++)
{
if(it->is_assignment() &&
it->assignment_type==symex_targett::STATE)
it->assignment_type==symex_targett::assignment_typet::STATE)
{
if(!prop_conv.l_get(it->guard_literal).is_false())
{
Expand Down Expand Up @@ -136,7 +136,7 @@ void counterexample_beautificationt::operator()(
it!=equation.SSA_steps.end(); it++)
{
if(it->is_assignment() &&
it->assignment_type!=symex_targett::HIDDEN)
it->assignment_type!=symex_targett::assignment_typet::HIDDEN)
{
if(!it->guard_literal.is_constant())
guard_count[it->guard_literal]++;
Expand Down
2 changes: 1 addition & 1 deletion src/cbmc/fault_localization.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ void fault_localizationt::collect_guards(lpointst &lpoints)
it!=bmc.equation.SSA_steps.end(); it++)
{
if(it->is_assignment() &&
it->assignment_type==symex_targett::STATE &&
it->assignment_type==symex_targett::assignment_typet::STATE &&
!it->ignore)
{
if(!it->guard_literal.is_constant())
Expand Down
14 changes: 10 additions & 4 deletions src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -300,9 +300,13 @@ void build_goto_trace(

// drop PHI and GUARD assignments altogether
if(it->is_assignment() &&
(SSA_step.assignment_type==symex_target_equationt::PHI ||
SSA_step.assignment_type==symex_target_equationt::GUARD))
(SSA_step.assignment_type==
symex_target_equationt::assignment_typet::PHI ||
SSA_step.assignment_type==
symex_target_equationt::assignment_typet::GUARD))
{
continue;
}

goto_tracet::stepst &steps=time_map[current_time];
steps.push_back(goto_trace_stept());
Expand Down Expand Up @@ -330,8 +334,10 @@ void build_goto_trace(

goto_trace_step.assignment_type=
(it->is_assignment()&&
(SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER ||
SSA_step.assignment_type==symex_targett::HIDDEN_ACTUAL_PARAMETER))?
(SSA_step.assignment_type==
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER ||
SSA_step.assignment_type==
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER))?
goto_trace_stept::ACTUAL_PARAMETER:
goto_trace_stept::STATE;

Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/goto_symex_state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -759,7 +759,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
ssa_l1.get_original_expr(),
tmp,
source,
symex_targett::PHI);
symex_targett::assignment_typet::PHI);

set_ssa_indices(ssa_l1, ns, L2);
expr=ssa_l1;
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/slice_by_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -630,7 +630,7 @@ void symex_slice_by_tracet::assign_merges(
SSA_step.guard=t_guard.as_expr();
SSA_step.ssa_lhs=merge_sym;
SSA_step.ssa_rhs.swap(merge_copy);
SSA_step.assignment_type=symex_targett::HIDDEN;
SSA_step.assignment_type=symex_targett::assignment_typet::HIDDEN;

SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
SSA_step.type=goto_trace_stept::ASSIGNMENT;
Expand Down
10 changes: 5 additions & 5 deletions src/goto-symex/symex_assign.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,21 +93,21 @@ void goto_symext::symex_assign(
}
else
{
assignment_typet assignment_type=symex_targett::STATE;
assignment_typet assignment_type=symex_targett::assignment_typet::STATE;

// Let's hide return value assignments.
if(lhs.id()==ID_symbol &&
id2string(to_symbol_expr(lhs).get_identifier()).find(
"#return_value!")!=std::string::npos)
assignment_type=symex_targett::HIDDEN;
assignment_type=symex_targett::assignment_typet::HIDDEN;

// We hide if we are in a hidden function.
if(state.top().hidden_function)
assignment_type=symex_targett::HIDDEN;
assignment_type=symex_targett::assignment_typet::HIDDEN;

// We hide if we are executing a hidden instruction.
if(state.source.pc->source_location.get_hide())
assignment_type=symex_targett::HIDDEN;
assignment_type=symex_targett::assignment_typet::HIDDEN;

guardt guard; // NOT the state guard!
symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
Expand Down Expand Up @@ -303,7 +303,7 @@ void goto_symext::symex_assign_symbol(
// do the assignment
const symbolt &symbol=ns.lookup(ssa_lhs.get_original_expr());
if(symbol.is_auxiliary)
assignment_type=symex_targett::HIDDEN;
assignment_type=symex_targett::assignment_typet::HIDDEN;

target.assignment(
tmp_guard.as_expr(),
Expand Down
4 changes: 3 additions & 1 deletion src/goto-symex/symex_decl.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
state.guard.as_expr(),
ssa,
state.source,
hidden?symex_targett::HIDDEN:symex_targett::STATE);
hidden ?
symex_targett::assignment_typet::HIDDEN :
symex_targett::assignment_typet::STATE);

assert(state.dirty);
if((*state.dirty)(ssa.get_object_name()) &&
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/symex_goto.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,7 +184,7 @@ void goto_symext::symex_goto(statet &state)
new_lhs, new_lhs, guard_symbol_expr,
new_rhs,
original_source,
symex_targett::GUARD);
symex_targett::assignment_typet::GUARD);

guard_expr=guard_symbol_expr;
guard_expr.make_not();
Expand Down Expand Up @@ -437,7 +437,7 @@ void goto_symext::phi_function(
new_lhs, new_lhs, new_lhs.get_original_expr(),
rhs,
dest_state.source,
symex_targett::PHI);
symex_targett::assignment_typet::PHI);
}
}

Expand Down
14 changes: 12 additions & 2 deletions src/goto-symex/symex_start_thread.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,12 @@ void goto_symext::symex_start_thread(statet &state)
const bool record_events=state.record_events;
state.record_events=false;
symex_assign_symbol(
state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
state,
lhs,
nil_exprt(),
rhs,
guard,
symex_targett::assignment_typet::HIDDEN);
state.record_events=record_events;
}

Expand Down Expand Up @@ -122,6 +127,11 @@ void goto_symext::symex_start_thread(statet &state)

guardt guard;
symex_assign_symbol(
state, lhs, nil_exprt(), rhs, guard, symex_targett::HIDDEN);
state,
lhs,
nil_exprt(),
rhs,
guard,
symex_targett::assignment_typet::HIDDEN);
}
}
11 changes: 8 additions & 3 deletions src/goto-symex/symex_target.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,10 +51,15 @@ class symex_targett
}
};

typedef enum
enum class assignment_typet
{
STATE, HIDDEN, VISIBLE_ACTUAL_PARAMETER, HIDDEN_ACTUAL_PARAMETER, PHI, GUARD
} assignment_typet;
STATE,
HIDDEN,
VISIBLE_ACTUAL_PARAMETER,
HIDDEN_ACTUAL_PARAMETER,
PHI,
GUARD,
};

// read event
virtual void shared_read(
Expand Down
30 changes: 21 additions & 9 deletions src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -250,8 +250,8 @@ void symex_target_equationt::assignment(

SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
SSA_step.type=goto_trace_stept::ASSIGNMENT;
SSA_step.hidden=(assignment_type!=STATE &&
assignment_type!=VISIBLE_ACTUAL_PARAMETER);
SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
assignment_type!=assignment_typet::VISIBLE_ACTUAL_PARAMETER);
SSA_step.source=source;

merge_ireps(SSA_step);
Expand Down Expand Up @@ -286,7 +286,7 @@ void symex_target_equationt::decl(
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);
SSA_step.hidden=(assignment_type!=assignment_typet::STATE);

// the condition is trivially true, and only
// there so we see the symbols
Expand Down Expand Up @@ -1001,12 +1001,24 @@ void symex_target_equationt::SSA_stept::output(
out << "ASSIGNMENT (";
switch(assignment_type)
{
case HIDDEN: out << "HIDDEN"; break;
case STATE: out << "STATE"; break;
case VISIBLE_ACTUAL_PARAMETER: out << "VISIBLE_ACTUAL_PARAMETER"; break;
case HIDDEN_ACTUAL_PARAMETER: out << "HIDDEN_ACTUAL_PARAMETER"; break;
case PHI: out << "PHI"; break;
case GUARD: out << "GUARD"; break;
case assignment_typet::HIDDEN:
out << "HIDDEN";
break;
case assignment_typet::STATE:
out << "STATE";
break;
case assignment_typet::VISIBLE_ACTUAL_PARAMETER:
out << "VISIBLE_ACTUAL_PARAMETER";
break;
case assignment_typet::HIDDEN_ACTUAL_PARAMETER:
out << "HIDDEN_ACTUAL_PARAMETER";
break;
case assignment_typet::PHI:
out << "PHI";
break;
case assignment_typet::GUARD:
out << "GUARD";
break;
default:
{
}
Expand Down
10 changes: 5 additions & 5 deletions src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -197,7 +197,7 @@ class symex_target_equationt:public symex_targett
bool is_atomic_end() const { return type==goto_trace_stept::ATOMIC_END; }

// we may choose to hide
bool hidden;
bool hidden=false;

exprt guard;
literalt guard_literal;
Expand All @@ -206,7 +206,7 @@ class symex_target_equationt:public symex_targett
ssa_exprt ssa_lhs;
exprt ssa_full_lhs, original_full_lhs;
exprt ssa_rhs;
assignment_typet assignment_type;
assignment_typet assignment_type=assignment_typet::STATE;

// for ASSUME/ASSERT/GOTO/CONSTRAINT
exprt cond_expr;
Expand All @@ -215,18 +215,18 @@ class symex_target_equationt:public symex_targett

// for INPUT/OUTPUT
irep_idt format_string, io_id;
bool formatted;
bool formatted=false;
std::list<exprt> io_args;
std::list<exprt> converted_io_args;

// for function call/return
irep_idt identifier;

// for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
unsigned atomic_section_id;
unsigned atomic_section_id=0;

// for slicing
bool ignore;
bool ignore=false;

SSA_stept():
type(goto_trace_stept::NONE),
Expand Down