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