27 std::string trace_files,
30 std::cout <<
"Slicing by trace...\n";
36 std::vector<exprt> trace_conditions;
38 size_t length=trace_files.length();
39 for(
size_t idx=0; idx < length; idx++)
42 std::string filename=trace_files.substr(idx, next - idx);
49 trace_conditions.push_back(t_copy);
51 if(next==std::string::npos)
56 exprt trace_condition;
58 if(trace_conditions.size()==1)
60 trace_condition=trace_conditions[0];
65 trace_condition.
operands().reserve(trace_conditions.size());
66 for(std::vector<exprt>::iterator i=trace_conditions.begin();
67 i!=trace_conditions.end(); i++)
82 if(g_copy.
id()==ID_symbol || g_copy.
id() == ID_not)
86 implications.insert(g_copy);
88 else if(g_copy.
id()==ID_and)
93 implications.insert(copy_last);
95 else if(!(g_copy.
id()==ID_constant))
97 throw "guards should only be and, symbol, constant, or `not'";
113 SSA_step.
source=empty_source;
117 std::cout <<
"Finished slicing by trace...\n";
122 std::cout <<
"Reading trace from file " << filename <<
'\n';
123 std::ifstream
file(filename);
125 throw "failed to read from trace file";
133 std::string read_line;
138 while(!done && !
file.eof())
140 std::getline(
file, read_line);
141 if(begin && (read_line==
"!"))
149 std::getline(
file, read_line);
153 for(
size_t i=0; i <
sigma.size(); i++)
167 if((read_line==
":") || (read_line ==
":exact") ||
168 (read_line==
":suffix") || (read_line ==
":exact-suffix") ||
169 (read_line==
":prefix"))
176 std::cout <<
"Alphabet: ";
179 std::cout << read_line <<
'\n';
189 bool parity=strstr(read_line.c_str(),
"!")==
nullptr;
190 bool universe=strstr(read_line.c_str(),
"?")!=
nullptr;
191 bool has_values=strstr(read_line.c_str(),
" ")!=
nullptr;
192 std::cout <<
"Trace: " << read_line <<
'\n';
193 std::vector<irep_idt> value_v;
197 std::string values=(read_line.substr(sloc, read_line.size()-1));
198 size_t length=values.length();
199 for(
size_t idx=0; idx < length; idx++)
202 std::string value=values.substr(idx, next - idx);
203 value_v.push_back(value);
204 if(next==std::string::npos)
208 read_line=read_line.substr(0, sloc);
214 read_line=read_line.substr(1, read_line.size()-1);
215 std::set<irep_idt> eis;
216 size_t vlength=read_line.length();
217 for(
size_t vidx=0; vidx < vlength; vidx++)
220 std::string
event=read_line.substr(vidx, vnext - vidx);
224 throw "trace uses symbol not in alphabet: "+event;
225 if(vnext==std::string::npos)
236 size_t merge_count=0;
238 for(symex_target_equationt::SSA_stepst::reverse_iterator
244 !i->io_args.empty() &&
245 i->io_args.front().id()==
"trace_event")
247 irep_idt event = i->io_args.front().get(ID_event);
251 bool present=(
alphabet.count(event)!=0);
256 exprt guard=i->guard;
259 std::cout <<
"EVENT: " <<
event <<
'\n';
260 std::cout <<
"GUARD: " <<
format(guard) <<
'\n';
261 for(
size_t j=0; j <
t.size(); j++)
263 std::cout <<
"t[" << j <<
"]=" <<
format(
t[j]) <<
269 std::vector<exprt> merge;
271 for(
size_t j=0; j <
t.size(); j++)
273 if((
t[j].
is_true()) || (
t[j].is_false()))
275 merge.push_back(
t[j]);
283 std::set<exprt> empty_impls;
285 (std::pair<
bool, std::set<exprt> >(
false, empty_impls));
286 merge.push_back(merge_sym);
290 for(
size_t j=0; j <
t.size(); j++)
299 std::list<exprt> eq_conds;
300 std::list<exprt>::iterator pvi=i->io_args.begin();
301 for(std::vector<irep_idt>::iterator k=
sigma_vals[j].begin();
308 exprt constant_value=
311 eq_conds.push_back(equal_cond);
315 val_merge.
operands().reserve(eq_conds.size()+1);
317 for(std::list<exprt>::iterator k=eq_conds.begin();
318 k!= eq_conds.end(); k++)
350 u_rhs.
swap(merge[j]);
367 exprt guard_copy(guard);
382 std::set<exprt> implications)
386 size_t sliced_SSA_steps=0;
387 size_t potential_SSA_steps=0;
388 size_t sliced_conds=0;
389 size_t trace_SSA_steps=0;
390 size_t location_SSA_steps=0;
391 size_t trace_loc_sliced=0;
393 for(symex_target_equationt::SSA_stepst::iterator
400 if(it->is_location())
401 location_SSA_steps++;
402 bool sliced_SSA_step=
false;
403 exprt guard=it->guard;
408 potential_SSA_steps++;
412 if((guard.
id()==ID_symbol) || (guard.
id() == ID_not))
417 if(implications.count(guard)!=0)
423 if(it->is_output() || it->is_location())
425 sliced_SSA_step=
true;
428 else if(guard.
id()==ID_and)
436 if(implications.count(neg_expr)!=0)
442 if(it->is_output() || it->is_location())
444 sliced_SSA_step=
true;
448 else if(guard.
id()==ID_or)
450 std::cout <<
"Guarded by an OR.\n";
454 if(!sliced_SSA_step && it->is_assignment())
456 if(it->ssa_rhs.id()==ID_if)
459 exprt cond_copy(it->ssa_rhs.op0());
462 if(implications.count(cond_copy)!=0)
465 exprt t_copy1(it->ssa_rhs.op1());
466 exprt t_copy2(it->ssa_rhs.op1());
468 it->cond_expr.
op1().
swap(t_copy2);
472 cond_copy.make_not();
474 if(implications.count(cond_copy)!=0)
477 exprt f_copy1(it->ssa_rhs.op2());
478 exprt f_copy2(it->ssa_rhs.op2());
480 it->cond_expr.
op1().
swap(f_copy2);
487 std::cout <<
"Trace slicing effectively removed " 488 << (sliced_SSA_steps + sliced_conds) <<
" out of " 489 << equation.
SSA_steps.size() <<
" SSA_steps.\n";
491 << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
493 << (equation.
SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
494 <<
" non-trace, non-location SSA_steps)\n";
501 bool present=s.first.count(event)!=0;
502 return ((s.second && present) || (!s.second && !present));
509 for(std::vector<exprt>::reverse_iterator i=
merge_map_back.rbegin();
519 exprt merge_copy(*i);
531 SSA_step.
source=empty_source;
539 if(e.
id()==ID_symbol)
546 if(merge_loc==std::string::npos)
569 else if(e.
id()==ID_not)
576 else if(e.
id()==ID_and)
581 for(std::set<exprt>::iterator i=
r.begin();
589 else if(e.
id()==ID_or)
591 std::vector<std::set<exprt> > rs;
596 for(std::set<exprt>::iterator i=rs.front().begin();
597 i!=rs.front().end();)
599 for(std::vector<std::set<exprt> >::iterator j=rs.begin();
604 std::set<exprt>::iterator k=i;
624 for(std::set<exprt>::iterator
631 if(imps.count(i_copy)!=0)
std::vector< exprt > merge_map_back
const irept & get_nil_irep()
The type of an expression.
bool implies_false(exprt e)
bool is_true(const literalt &l)
const std::string & id2string(const irep_idt &d)
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
void copy_to_operands(const exprt &expr)
void move_to_operands(exprt &expr)
Slicer for matching with trace files.
unsignedbv_typet size_type()
assignment_typet assignment_type
void set_level_2(unsigned i)
const irep_idt & id() const
std::set< exprt > sliced_guards
symbol_exprt merge_symbol
The boolean constant true.
irep_idt merge_identifier
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
std::set< exprt > implied_guards(exprt e)
std::pair< std::set< irep_idt >, bool > event_sett
The boolean constant false.
void read_trace(std::string filename)
bool matches(event_sett s, irep_idt event)
void assign_merges(symex_target_equationt &equation)
Base class for all expressions.
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
void set_identifier(const irep_idt &identifier)
void compute_ts_fd(symex_target_equationt &equation)
#define Forall_operands(it, expr)
Expression to hold a symbol (variable)
void parse_events(std::string read_line)
void compute_ts_back(symex_target_equationt &equation)
goto_trace_stept::typet type
int unsafe_string2int(const std::string &str, int base)
Expression providing an SSA-renamed symbol of expressions.
const irept & find(const irep_namet &name) const
bool parse_alphabet(std::string read_line)
bool simplify(exprt &expr, const namespacet &ns)