29 std::string trace_files,
32 std::cout <<
"Slicing by trace...\n";
38 std::vector<exprt> trace_conditions;
40 size_t length=trace_files.length();
41 for(
size_t idx=0; idx < length; idx++)
44 std::string filename=trace_files.substr(idx, next - idx);
51 trace_conditions.push_back(t_copy);
53 if(next==std::string::npos)
58 exprt trace_condition;
60 if(trace_conditions.size()==1)
62 trace_condition=trace_conditions[0];
67 trace_condition.
operands().reserve(trace_conditions.size());
68 for(std::vector<exprt>::iterator i=trace_conditions.begin();
69 i!=trace_conditions.end(); i++)
85 g_copy.
id() == ID_symbol || g_copy.
id() == ID_not ||
86 g_copy.
id() == ID_and || g_copy.
id() == ID_constant,
87 "guards should only be and, symbol, constant, or `not'");
89 if(g_copy.
id()==ID_symbol || g_copy.
id() == ID_not)
92 implications.insert(g_copy);
94 else if(g_copy.
id()==ID_and)
98 implications.insert(copy_last);
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);
126 "invalid file to read trace from: " + filename,
"");
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);
226 "trace uses symbol not in alphabet: " + event);
227 if(vnext==std::string::npos)
238 size_t merge_count=0;
240 for(symex_target_equationt::SSA_stepst::reverse_iterator
246 !i->io_args.empty() &&
247 i->io_args.front().id()==
"trace_event")
249 irep_idt event = i->io_args.front().get(ID_event);
253 bool present=(
alphabet.count(event)!=0);
258 exprt guard=i->guard;
261 std::cout <<
"EVENT: " <<
event <<
'\n';
262 std::cout <<
"GUARD: " <<
format(guard) <<
'\n';
263 for(
size_t j=0; j <
t.size(); j++)
265 std::cout <<
"t[" << j <<
"]=" <<
format(
t[j]) <<
271 std::vector<exprt>
merge;
273 for(
size_t j=0; j <
t.size(); j++)
275 if((
t[j].
is_true()) || (
t[j].is_false()))
285 std::set<exprt> empty_impls;
287 (std::pair<
bool, std::set<exprt> >(
false, empty_impls));
288 merge.push_back(merge_sym);
292 for(
size_t j=0; j <
t.size(); j++)
301 std::list<exprt> eq_conds;
302 std::list<exprt>::iterator pvi=i->io_args.begin();
303 for(std::vector<irep_idt>::iterator k=
sigma_vals[j].begin();
310 exprt constant_value=
313 eq_conds.push_back(equal_cond);
317 val_merge.
operands().reserve(eq_conds.size()+1);
319 for(std::list<exprt>::iterator k=eq_conds.begin();
320 k!= eq_conds.end(); k++)
366 exprt guard_copy(guard);
376 std::set<exprt> implications)
380 size_t sliced_SSA_steps=0;
381 size_t potential_SSA_steps=0;
382 size_t sliced_conds=0;
383 size_t trace_SSA_steps=0;
384 size_t location_SSA_steps=0;
385 size_t trace_loc_sliced=0;
387 for(symex_target_equationt::SSA_stepst::iterator
394 if(it->is_location())
395 location_SSA_steps++;
396 bool sliced_SSA_step=
false;
397 exprt guard=it->guard;
402 potential_SSA_steps++;
406 if((guard.
id()==ID_symbol) || (guard.
id() == ID_not))
410 if(implications.count(guard)!=0)
416 if(it->is_output() || it->is_location())
418 sliced_SSA_step=
true;
421 else if(guard.
id()==ID_and)
428 if(implications.count(neg_expr)!=0)
434 if(it->is_output() || it->is_location())
436 sliced_SSA_step=
true;
440 else if(guard.
id()==ID_or)
442 std::cout <<
"Guarded by an OR.\n";
446 if(!sliced_SSA_step && it->is_assignment())
448 if(it->ssa_rhs.id()==ID_if)
454 if(implications.count(cond_copy)!=0)
460 it->cond_expr.
op1().
swap(t_copy2);
465 if(implications.count(cond_copy)!=0)
471 it->cond_expr.
op1().
swap(f_copy2);
478 std::cout <<
"Trace slicing effectively removed " 479 << (sliced_SSA_steps + sliced_conds) <<
" out of " 480 << equation.
SSA_steps.size() <<
" SSA_steps.\n";
482 << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
484 << (equation.
SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
485 <<
" non-trace, non-location SSA_steps)\n";
492 bool present=s.first.count(event)!=0;
493 return ((s.second && present) || (!s.second && !present));
500 for(std::vector<exprt>::reverse_iterator i=
merge_map_back.rbegin();
509 exprt merge_copy(*i);
521 SSA_step.
source=empty_source;
529 if(e.
id()==ID_symbol)
536 if(merge_loc==std::string::npos)
559 else if(e.
id()==ID_not)
566 else if(e.
id()==ID_and)
571 for(std::set<exprt>::iterator i=
r.begin();
579 else if(e.
id()==ID_or)
581 std::vector<std::set<exprt> > rs;
586 for(std::set<exprt>::iterator i=rs.front().begin();
587 i!=rs.front().end();)
589 for(std::vector<std::set<exprt> >::iterator j=rs.begin();
594 std::set<exprt>::iterator k=i;
614 for(std::set<exprt>::iterator
620 if(imps.count(i_copy)!=0)
std::vector< exprt > merge_map_back
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const irept & get_nil_irep()
The type of an expression, extends irept.
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)
exprt simplify_expr(const exprt &src, const namespacet &ns)
Deprecated expression utility functions.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Slicer for matching with trace files.
bool is_false() const
Return whether the expression is a constant representing false.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
bool is_true() const
Return whether the expression is a constant representing true.
unsignedbv_typet size_type()
assignment_typet assignment_type
void set_level_2(unsigned i)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
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
Identifies source in the context of symbolic execution.
std::size_t unsafe_string2size_t(const std::string &str, int base)
API to expression classes.
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
std::set< exprt > implied_guards(exprt e)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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)
Single SSA step in the 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)
#define Forall_operands(it, expr)
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Expression providing an SSA-renamed symbol of expressions.
const irept & find(const irep_namet &name) const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
bool parse_alphabet(std::string read_line)
bool simplify(exprt &expr, const namespacet &ns)