28 std::string trace_files,
31 std::cout <<
"Slicing by trace...\n";
37 std::vector<exprt> trace_conditions;
39 size_t length=trace_files.length();
40 for(
size_t idx=0; idx < length; idx++)
43 std::string filename=trace_files.substr(idx, next - idx);
50 trace_conditions.push_back(t_copy);
52 if(next==std::string::npos)
57 exprt trace_condition;
59 if(trace_conditions.size()==1)
61 trace_condition=trace_conditions[0];
66 trace_condition.
operands().reserve(trace_conditions.size());
67 for(std::vector<exprt>::iterator i=trace_conditions.begin();
68 i!=trace_conditions.end(); i++)
83 if(g_copy.
id()==ID_symbol || g_copy.
id() == ID_not)
87 implications.insert(g_copy);
89 else if(g_copy.
id()==ID_and)
94 implications.insert(copy_last);
96 else if(!(g_copy.
id()==ID_constant))
98 throw "guards should only be and, symbol, constant, or `not'";
114 SSA_step.
source=empty_source;
118 std::cout <<
"Finished slicing by trace...\n";
123 std::cout <<
"Reading trace from file " << filename <<
'\n';
124 std::ifstream
file(filename);
126 throw "failed to read from trace file";
134 std::string read_line;
139 while(!done && !file.eof())
141 std::getline(file, read_line);
142 if(begin && (read_line==
"!"))
150 std::getline(file, read_line);
154 for(
size_t i=0; i <
sigma.size(); i++)
168 if((read_line==
":") || (read_line ==
":exact") ||
169 (read_line==
":suffix") || (read_line ==
":exact-suffix") ||
170 (read_line==
":prefix"))
177 std::cout <<
"Alphabet: ";
180 std::cout << read_line <<
'\n';
190 bool parity=strstr(read_line.c_str(),
"!")==
nullptr;
191 bool universe=strstr(read_line.c_str(),
"?")!=
nullptr;
192 bool has_values=strstr(read_line.c_str(),
" ")!=
nullptr;
193 std::cout <<
"Trace: " << read_line <<
'\n';
194 std::vector<irep_idt> value_v;
198 std::string values=(read_line.substr(sloc, read_line.size()-1));
199 size_t length=values.length();
200 for(
size_t idx=0; idx < length; idx++)
203 std::string value=values.substr(idx, next - idx);
204 value_v.push_back(value);
205 if(next==std::string::npos)
209 read_line=read_line.substr(0, sloc);
215 read_line=read_line.substr(1, read_line.size()-1);
216 std::set<irep_idt> eis;
217 size_t vlength=read_line.length();
218 for(
size_t vidx=0; vidx < vlength; vidx++)
221 std::string
event=read_line.substr(vidx, vnext - vidx);
225 throw "trace uses symbol not in alphabet: "+event;
226 if(vnext==std::string::npos)
237 size_t merge_count=0;
239 for(symex_target_equationt::SSA_stepst::reverse_iterator
245 !i->io_args.empty() &&
246 i->io_args.front().id()==
"trace_event")
248 irep_idt event=i->io_args.front().get(
"event");
252 bool present=(
alphabet.count(event)!=0);
257 exprt guard=i->guard;
260 std::cout <<
"EVENT: " <<
event <<
'\n';
261 std::cout <<
"GUARD: " <<
from_expr(
ns,
"", guard) <<
'\n';
262 for(
size_t j=0; j <
t.size(); j++)
264 std::cout <<
"t[" << j <<
"]=" <<
from_expr(
ns,
"",
t[j]) <<
270 std::vector<exprt> merge;
272 for(
size_t j=0; j <
t.size(); j++)
274 if((
t[j].is_true()) || (
t[j].is_false()))
276 merge.push_back(
t[j]);
284 std::set<exprt> empty_impls;
286 (std::pair<
bool, std::set<exprt> >(
false, empty_impls));
287 merge.push_back(merge_sym);
291 for(
size_t j=0; j <
t.size(); j++)
300 std::list<exprt> eq_conds;
301 std::list<exprt>::iterator pvi=i->io_args.begin();
302 for(std::vector<irep_idt>::iterator k=
sigma_vals[j].begin();
309 exprt constant_value=
312 eq_conds.push_back(equal_cond);
316 val_merge.
operands().reserve(eq_conds.size()+1);
318 for(std::list<exprt>::iterator k=eq_conds.begin();
319 k!= eq_conds.end(); k++)
351 u_rhs.
swap(merge[j]);
368 exprt guard_copy(guard);
383 std::set<exprt> implications)
387 size_t sliced_SSA_steps=0;
388 size_t potential_SSA_steps=0;
389 size_t sliced_conds=0;
390 size_t trace_SSA_steps=0;
391 size_t location_SSA_steps=0;
392 size_t trace_loc_sliced=0;
394 for(symex_target_equationt::SSA_stepst::iterator
401 if(it->is_location())
402 location_SSA_steps++;
403 bool sliced_SSA_step=
false;
404 exprt guard=it->guard;
409 potential_SSA_steps++;
413 if((guard.
id()==ID_symbol) || (guard.
id() == ID_not))
418 if(implications.count(guard)!=0)
424 if(it->is_output() || it->is_location())
426 sliced_SSA_step=
true;
429 else if(guard.
id()==ID_and)
437 if(implications.count(neg_expr)!=0)
443 if(it->is_output() || it->is_location())
445 sliced_SSA_step=
true;
449 else if(guard.
id()==ID_or)
451 std::cout <<
"Guarded by an OR.\n";
455 if(!sliced_SSA_step && it->is_assignment())
457 if(it->ssa_rhs.id()==ID_if)
460 exprt cond_copy(it->ssa_rhs.op0());
463 if(implications.count(cond_copy)!=0)
466 exprt t_copy1(it->ssa_rhs.op1());
467 exprt t_copy2(it->ssa_rhs.op1());
469 it->cond_expr.
op1().
swap(t_copy2);
473 cond_copy.make_not();
475 if(implications.count(cond_copy)!=0)
478 exprt f_copy1(it->ssa_rhs.op2());
479 exprt f_copy2(it->ssa_rhs.op2());
481 it->cond_expr.
op1().
swap(f_copy2);
488 std::cout <<
"Trace slicing effectively removed " 489 << (sliced_SSA_steps + sliced_conds) <<
" out of " 490 << equation.
SSA_steps.size() <<
" SSA_steps.\n";
492 << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
494 << (equation.
SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
495 <<
" non-trace, non-location SSA_steps)\n";
502 bool present=s.first.count(event)!=0;
503 return ((s.second && present) || (!s.second && !present));
510 for(std::vector<exprt>::reverse_iterator i=
merge_map_back.rbegin();
520 exprt merge_copy(*i);
532 SSA_step.
source=empty_source;
540 if(e.
id()==ID_symbol)
544 if(merge_loc==std::string::npos)
567 else if(e.
id()==ID_not)
574 else if(e.
id()==ID_and)
579 for(std::set<exprt>::iterator i=r.begin();
587 else if(e.
id()==ID_or)
589 std::vector<std::set<exprt> > rs;
594 for(std::set<exprt>::iterator i=rs.front().begin();
595 i!=rs.front().end();)
597 for(std::vector<std::set<exprt> >::iterator j=rs.begin();
602 std::set<exprt>::iterator k=i;
622 for(std::set<exprt>::iterator
629 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)
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)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, 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 irep_idt & get(const irep_namet &name) const
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)