cprover
slice_by_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicer for symex traces
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "slice_by_trace.h"
13 
14 #include <cstring>
15 #include <set>
16 #include <fstream>
17 #include <iostream>
18 
19 #include <util/string2int.h>
20 #include <util/simplify_expr.h>
21 #include <util/arith_tools.h>
22 #include <util/std_expr.h>
23 #include <util/guard.h>
24 
25 #include <langapi/language_util.h>
26 
28  std::string trace_files,
29  symex_target_equationt &equation)
30 {
31  std::cout << "Slicing by trace...\n";
32 
33  merge_identifier="goto_symex::\\merge";
36 
37  std::vector<exprt> trace_conditions;
38 
39  size_t length=trace_files.length();
40  for(size_t idx=0; idx < length; idx++)
41  {
42  const std::string::size_type next=trace_files.find(",", idx);
43  std::string filename=trace_files.substr(idx, next - idx);
44 
45  read_trace(filename);
46 
47  compute_ts_back(equation);
48 
49  exprt t_copy(t[0]);
50  trace_conditions.push_back(t_copy);
51 
52  if(next==std::string::npos)
53  break;
54  idx=next;
55  }
56 
57  exprt trace_condition;
58 
59  if(trace_conditions.size()==1)
60  {
61  trace_condition=trace_conditions[0];
62  }
63  else
64  {
65  trace_condition=exprt(ID_and, typet(ID_bool));
66  trace_condition.operands().reserve(trace_conditions.size());
67  for(std::vector<exprt>::iterator i=trace_conditions.begin();
68  i!=trace_conditions.end(); i++)
69  {
70  trace_condition.move_to_operands(*i);
71  }
72  }
73 
74  simplify(trace_condition, ns);
75 
76  std::set<exprt> implications=implied_guards(trace_condition);
77 
78  for(std::set<exprt>::iterator i=sliced_guards.begin(); i !=
79  sliced_guards.end(); i++)
80  {
81  exprt g_copy(*i);
82 
83  if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
84  {
85  g_copy.make_not();
86  simplify(g_copy, ns);
87  implications.insert(g_copy);
88  }
89  else if(g_copy.id()==ID_and)
90  {
91  exprt copy_last(g_copy.operands().back());
92  copy_last.make_not();
93  simplify(copy_last, ns);
94  implications.insert(copy_last);
95  }
96  else if(!(g_copy.id()==ID_constant))
97  {
98  throw "guards should only be and, symbol, constant, or `not'";
99  }
100  }
101 
102  slice_SSA_steps(equation, implications); // Slice based on implications
103 
104  guardt t_guard;
105  t_guard.make_true();
106  symex_targett::sourcet empty_source;
107  equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
108  symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
109 
110  SSA_step.guard=t_guard.as_expr();
111  SSA_step.ssa_lhs.make_nil();
112  SSA_step.cond_expr.swap(trace_condition);
114  SSA_step.source=empty_source;
115 
116  assign_merges(equation); // Now add the merge variable assignments to eqn
117 
118  std::cout << "Finished slicing by trace...\n";
119 }
120 
121 void symex_slice_by_tracet::read_trace(std::string filename)
122 {
123  std::cout << "Reading trace from file " << filename << '\n';
124  std::ifstream file(filename);
125  if(file.fail())
126  throw "failed to read from trace file";
127 
128  // In case not the first trace read
129  alphabet.clear();
130  sigma.clear();
131  sigma_vals.clear();
132  t.clear();
133 
134  std::string read_line;
135  bool done=false;
136  bool begin=true;
137  alphabet_parity=true;
138 
139  while(!done && !file.eof())
140  {
141  std::getline(file, read_line);
142  if(begin && (read_line=="!"))
143  alphabet_parity=false;
144  else
145  done=parse_alphabet(read_line);
146  }
147 
148  while(!file.eof())
149  {
150  std::getline(file, read_line);
151  parse_events(read_line);
152  }
153 
154  for(size_t i=0; i < sigma.size(); i++)
155  {
156  exprt f_e=static_cast<const exprt &>(get_nil_irep());
157  f_e=false_exprt();
158  t.push_back(f_e);
159  }
160 
161  exprt t_e=static_cast<const exprt &>(get_nil_irep());
162  t_e=true_exprt();
163  t.push_back(t_e);
164 }
165 
166 bool symex_slice_by_tracet::parse_alphabet(std::string read_line)
167 {
168  if((read_line==":") || (read_line == ":exact") ||
169  (read_line==":suffix") || (read_line == ":exact-suffix") ||
170  (read_line==":prefix"))
171  {
172  semantics=read_line;
173  return true;
174  }
175  else
176  {
177  std::cout << "Alphabet: ";
178  if(!alphabet_parity)
179  std::cout << "!";
180  std::cout << read_line << '\n';
181  alphabet.insert(read_line);
182  }
183  return false;
184 }
185 
186 void symex_slice_by_tracet::parse_events(std::string read_line)
187 {
188  if(read_line=="")
189  return;
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;
195  if(has_values)
196  {
197  std::string::size_type sloc=read_line.find(" ", 0);
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++)
201  {
202  const std::string::size_type next=values.find(",", idx);
203  std::string value=values.substr(idx, next - idx);
204  value_v.push_back(value);
205  if(next==std::string::npos)
206  break;
207  idx=next;
208  }
209  read_line=read_line.substr(0, sloc);
210  }
211  sigma_vals.push_back(value_v);
212  if(universe)
213  parity=false;
214  if(!parity)
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++)
219  {
220  const std::string::size_type vnext=read_line.find(",", vidx);
221  std::string event=read_line.substr(vidx, vnext - vidx);
222  eis.insert(event);
223  if((!alphabet.empty()) &&
224  ((alphabet.count(event)!=0)!=alphabet_parity))
225  throw "trace uses symbol not in alphabet: "+event;
226  if(vnext==std::string::npos)
227  break;
228  vidx=vnext;
229  }
230  event_sett es=event_sett(eis, parity);
231  sigma.push_back(es);
232 }
233 
235  symex_target_equationt &equation)
236 {
237  size_t merge_count=0;
238 
239  for(symex_target_equationt::SSA_stepst::reverse_iterator
240  i=equation.SSA_steps.rbegin();
241  i!=equation.SSA_steps.rend();
242  i++)
243  {
244  if(i->is_output() &&
245  !i->io_args.empty() &&
246  i->io_args.front().id()=="trace_event")
247  {
248  irep_idt event=i->io_args.front().get("event");
249 
250  if(!alphabet.empty())
251  {
252  bool present=(alphabet.count(event)!=0);
253  if(alphabet_parity!=present)
254  continue;
255  }
256 
257  exprt guard=i->guard;
258 
259 #if 0
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++)
263  {
264  std::cout << "t[" << j << "]=" << from_expr(ns, "", t[j]) <<
265  '\n';
266  }
267 #endif
268 
269  bool slice_this=(semantics!=":prefix");
270  std::vector<exprt> merge;
271 
272  for(size_t j=0; j < t.size(); j++)
273  {
274  if((t[j].is_true()) || (t[j].is_false()))
275  {
276  merge.push_back(t[j]);
277  }
278  else
279  {
280  ssa_exprt merge_sym(merge_symbol);
281  merge_sym.set_level_2(merge_count++);
282  exprt t_copy(t[j]);
283  merge_map_back.push_back(t_copy);
284  std::set<exprt> empty_impls;
285  merge_impl_cache_back.push_back
286  (std::pair<bool, std::set<exprt> >(false, empty_impls));
287  merge.push_back(merge_sym);
288  }
289  }
290 
291  for(size_t j=0; j < t.size(); j++)
292  {
293  exprt u_lhs=exprt(ID_and, typet(ID_bool));
294  if((j < sigma.size()) && (matches(sigma[j], event)))
295  {
296  u_lhs.operands().reserve(2);
297  u_lhs.copy_to_operands(guard);
298  if(!sigma_vals[j].empty())
299  {
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();
303  k!=sigma_vals[j].end(); k++)
304  {
305  exprt equal_cond=exprt(ID_equal, bool_typet());
306  equal_cond.operands().reserve(2);
307  equal_cond.copy_to_operands(*pvi);
308  // Should eventually change to handle non-bv types!
309  exprt constant_value=
310  from_integer(unsafe_string2int(id2string(*k)), (*pvi).type());
311  equal_cond.move_to_operands(constant_value);
312  eq_conds.push_back(equal_cond);
313  pvi++;
314  }
315  exprt val_merge=exprt(ID_and, typet(ID_bool));
316  val_merge.operands().reserve(eq_conds.size()+1);
317  val_merge.copy_to_operands(merge[j+1]);
318  for(std::list<exprt>::iterator k=eq_conds.begin();
319  k!= eq_conds.end(); k++)
320  {
321  val_merge.copy_to_operands(*k);
322  }
323  u_lhs.move_to_operands(val_merge);
324  }
325  else
326  {
327  u_lhs.copy_to_operands(merge[j+1]);
328  }
329 
330  simplify(u_lhs, ns);
331 
332  if((!u_lhs.is_false()) && implies_false(u_lhs))
333  u_lhs=false_exprt();
334  if(!u_lhs.is_false())
335  slice_this=false;
336  }
337  else
338  {
339  u_lhs=false_exprt();
340  }
341  exprt u_rhs=exprt(ID_and, typet(ID_bool));
342  if((semantics!=":suffix") || (j != 0))
343  {
344  u_rhs.operands().reserve(2);
345  u_rhs.copy_to_operands(guard);
346  u_rhs.copy_to_operands(merge[j]);
347  u_rhs.op0().make_not();
348  }
349  else
350  {
351  u_rhs.swap(merge[j]);
352  }
353  exprt u_j=exprt(ID_or, typet(ID_bool));
354  u_j.operands().reserve(2);
355  u_j.copy_to_operands(u_lhs);
356  u_j.copy_to_operands(u_rhs);
357 
358  simplify(u_j, ns);
359 
360  t[j]=u_j;
361  }
362 
363  if(semantics==":prefix")
364  t[t.size()-1]=true_exprt();
365 
366  if(slice_this)
367  {
368  exprt guard_copy(guard);
369 
370  sliced_guards.insert(guard_copy);
371  }
372  }
373  }
374 }
375 
377  symex_target_equationt &equation)
378 {
379 }
380 
382  symex_target_equationt &equation,
383  std::set<exprt> implications)
384 {
385  // Some statistics for our benefit.
386  size_t conds_seen=0;
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;
393 
394  for(symex_target_equationt::SSA_stepst::iterator
395  it=equation.SSA_steps.begin();
396  it!=equation.SSA_steps.end();
397  it++)
398  {
399  if(it->is_output())
400  trace_SSA_steps++;
401  if(it->is_location())
402  location_SSA_steps++;
403  bool sliced_SSA_step=false;
404  exprt guard=it->guard;
405 
406  simplify(guard, ns);
407 
408  if(!guard.is_true())
409  potential_SSA_steps++;
410  // it->output(ns,std::cout);
411  // std::cout << "-----------------\n";
412 
413  if((guard.id()==ID_symbol) || (guard.id() == ID_not))
414  {
415  guard.make_not();
416  simplify(guard, ns);
417 
418  if(implications.count(guard)!=0)
419  {
420  it->cond_expr=true_exprt();
421  it->ssa_rhs=true_exprt();
422  it->guard=false_exprt();
423  sliced_SSA_steps++;
424  if(it->is_output() || it->is_location())
425  trace_loc_sliced++;
426  sliced_SSA_step=true;
427  }
428  }
429  else if(guard.id()==ID_and)
430  {
431  Forall_operands(git, guard)
432  {
433  exprt neg_expr=*git;
434  neg_expr.make_not();
435  simplify(neg_expr, ns);
436 
437  if(implications.count(neg_expr)!=0)
438  {
439  it->cond_expr=true_exprt();
440  it->ssa_rhs=true_exprt();
441  it->guard=false_exprt();
442  sliced_SSA_steps++;
443  if(it->is_output() || it->is_location())
444  trace_loc_sliced++;
445  sliced_SSA_step=true;
446  break; // Sliced, so no need to consider the rest
447  }
448  }
449  else if(guard.id()==ID_or)
450  {
451  std::cout << "Guarded by an OR.\n";
452  }
453  }
454 
455  if(!sliced_SSA_step && it->is_assignment())
456  {
457  if(it->ssa_rhs.id()==ID_if)
458  {
459  conds_seen++;
460  exprt cond_copy(it->ssa_rhs.op0());
461  simplify(cond_copy, ns);
462 
463  if(implications.count(cond_copy)!=0)
464  {
465  sliced_conds++;
466  exprt t_copy1(it->ssa_rhs.op1());
467  exprt t_copy2(it->ssa_rhs.op1());
468  it->ssa_rhs=t_copy1;
469  it->cond_expr.op1().swap(t_copy2);
470  }
471  else
472  {
473  cond_copy.make_not();
474  simplify(cond_copy, ns);
475  if(implications.count(cond_copy)!=0)
476  {
477  sliced_conds++;
478  exprt f_copy1(it->ssa_rhs.op2());
479  exprt f_copy2(it->ssa_rhs.op2());
480  it->ssa_rhs=f_copy1;
481  it->cond_expr.op1().swap(f_copy2);
482  }
483  }
484  }
485  }
486  }
487 
488  std::cout << "Trace slicing effectively removed "
489  << (sliced_SSA_steps + sliced_conds) << " out of "
490  << equation.SSA_steps.size() << " SSA_steps.\n";
491  std::cout << " ("
492  << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
493  << " out of "
494  << (equation.SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
495  << " non-trace, non-location SSA_steps)\n";
496 }
497 
499  event_sett s,
500  irep_idt event)
501 {
502  bool present=s.first.count(event)!=0;
503  return ((s.second && present) || (!s.second && !present));
504 }
505 
507  symex_target_equationt &equation)
508 {
509  size_t merge_count=(merge_map_back.size()) - 1;
510  for(std::vector<exprt>::reverse_iterator i=merge_map_back.rbegin();
511  i!=merge_map_back.rend(); i++)
512  {
513  ssa_exprt merge_sym(merge_symbol);
514  merge_sym.set_level_2(merge_count);
515  merge_count--;
516  guardt t_guard;
517  t_guard.make_true();
518  symex_targett::sourcet empty_source;
519 
520  exprt merge_copy(*i);
521 
522  equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
523  symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
524 
525  SSA_step.guard=t_guard.as_expr();
526  SSA_step.ssa_lhs=merge_sym;
527  SSA_step.ssa_rhs.swap(merge_copy);
529 
530  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
532  SSA_step.source=empty_source;
533  }
534 }
535 
537 {
538  std::set<exprt> s;
539 
540  if(e.id()==ID_symbol)
541  { // Guard or merge
542  const std::string &id_string=id2string(e.get(ID_identifier));
543  std::string::size_type merge_loc=id_string.find("merge#");
544  if(merge_loc==std::string::npos)
545  {
546  exprt e_copy(e);
547  simplify(e_copy, ns);
548  s.insert(e_copy);
549  return s;
550  }
551  else
552  {
553  int i=unsafe_string2int(id_string.substr(merge_loc+6));
554  if(merge_impl_cache_back[i].first)
555  {
556  return merge_impl_cache_back[i].second;
557  }
558  else
559  {
560  merge_impl_cache_back[i].first=true;
561  exprt merge_copy(merge_map_back[i]);
562  merge_impl_cache_back[i].second=implied_guards(merge_copy);
563  return merge_impl_cache_back[i].second;
564  }
565  }
566  }
567  else if(e.id()==ID_not)
568  { // Definitely a guard
569  exprt e_copy(e);
570  simplify(e_copy, ns);
571  s.insert(e_copy);
572  return s;
573  }
574  else if(e.id()==ID_and)
575  { // Descend into and
576  Forall_operands(it, e)
577  {
578  std::set<exprt> r=implied_guards(*it);
579  for(std::set<exprt>::iterator i=r.begin();
580  i!=r.end(); i++)
581  {
582  s.insert(*i);
583  }
584  }
585  return s;
586  }
587  else if(e.id()==ID_or)
588  { // Descend into or
589  std::vector<std::set<exprt> > rs;
590  Forall_operands(it, e)
591  {
592  rs.push_back(implied_guards(*it));
593  }
594  for(std::set<exprt>::iterator i=rs.front().begin();
595  i!=rs.front().end();)
596  {
597  for(std::vector<std::set<exprt> >::iterator j=rs.begin();
598  j!=rs.end(); j++)
599  {
600  if(j==rs.begin())
601  j++;
602  std::set<exprt>::iterator k=i;
603  i++;
604  if(j->count(*k)==0)
605  {
606  rs.front().erase(k);
607  break;
608  }
609  }
610  }
611  s=rs.front();
612  return s;
613  }
614 
615  return s;
616 }
617 
619 {
620  std::set<exprt> imps=implied_guards(e);
621 
622  for(std::set<exprt>::iterator
623  i=imps.begin();
624  i!=imps.end(); i++)
625  {
626  exprt i_copy(*i);
627  i_copy.make_not();
628  simplify(i_copy, ns);
629  if(imps.count(i_copy)!=0)
630  return true;
631  }
632 
633  return false;
634 }
std::vector< exprt > merge_map_back
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
exprt as_expr() const
Definition: guard.h:43
bool implies_false(exprt e)
static int8_t r
Definition: irep_hash.h:59
value_tracet sigma_vals
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
exprt & op0()
Definition: expr.h:84
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
Slicer for matching with trace files.
bool is_false() const
Definition: expr.cpp:140
bool is_true() const
Definition: expr.cpp:133
Definition: guard.h:19
unsignedbv_typet size_type()
Definition: c_types.cpp:57
The proper Booleans.
Definition: std_types.h:33
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
equality
Definition: std_expr.h:1082
void make_true()
Definition: expr.cpp:153
const irep_idt & id() const
Definition: irep.h:189
std::set< exprt > sliced_guards
symbol_exprt merge_symbol
The boolean constant true.
Definition: std_expr.h:3742
trace_conditionst t
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Guard Data Structure.
std::set< exprt > implied_guards(exprt e)
std::pair< std::set< irep_idt >, bool > event_sett
The boolean constant false.
Definition: std_expr.h:3753
void read_trace(std::string filename)
void make_not()
Definition: expr.cpp:100
bool matches(event_sett s, irep_idt event)
void assign_merges(symex_target_equationt &equation)
const namespacet & ns
Base class for all expressions.
Definition: expr.h:46
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
void make_nil()
Definition: irep.h:243
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
void compute_ts_fd(symex_target_equationt &equation)
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void parse_events(std::string read_line)
void compute_ts_back(symex_target_equationt &equation)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool parse_alphabet(std::string read_line)
bool simplify(exprt &expr, const namespacet &ns)
Definition: kdev_t.h:19