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  std::set<exprt> implications)
378 {
379  // Some statistics for our benefit.
380  size_t conds_seen=0;
381  size_t sliced_SSA_steps=0;
382  size_t potential_SSA_steps=0;
383  size_t sliced_conds=0;
384  size_t trace_SSA_steps=0;
385  size_t location_SSA_steps=0;
386  size_t trace_loc_sliced=0;
387 
388  for(symex_target_equationt::SSA_stepst::iterator
389  it=equation.SSA_steps.begin();
390  it!=equation.SSA_steps.end();
391  it++)
392  {
393  if(it->is_output())
394  trace_SSA_steps++;
395  if(it->is_location())
396  location_SSA_steps++;
397  bool sliced_SSA_step=false;
398  exprt guard=it->guard;
399 
400  simplify(guard, ns);
401 
402  if(!guard.is_true())
403  potential_SSA_steps++;
404  // it->output(ns,std::cout);
405  // std::cout << "-----------------\n";
406 
407  if((guard.id()==ID_symbol) || (guard.id() == ID_not))
408  {
409  guard.make_not();
410  simplify(guard, ns);
411 
412  if(implications.count(guard)!=0)
413  {
414  it->cond_expr=true_exprt();
415  it->ssa_rhs=true_exprt();
416  it->guard=false_exprt();
417  sliced_SSA_steps++;
418  if(it->is_output() || it->is_location())
419  trace_loc_sliced++;
420  sliced_SSA_step=true;
421  }
422  }
423  else if(guard.id()==ID_and)
424  {
425  Forall_operands(git, guard)
426  {
427  exprt neg_expr=*git;
428  neg_expr.make_not();
429  simplify(neg_expr, ns);
430 
431  if(implications.count(neg_expr)!=0)
432  {
433  it->cond_expr=true_exprt();
434  it->ssa_rhs=true_exprt();
435  it->guard=false_exprt();
436  sliced_SSA_steps++;
437  if(it->is_output() || it->is_location())
438  trace_loc_sliced++;
439  sliced_SSA_step=true;
440  break; // Sliced, so no need to consider the rest
441  }
442  }
443  else if(guard.id()==ID_or)
444  {
445  std::cout << "Guarded by an OR.\n";
446  }
447  }
448 
449  if(!sliced_SSA_step && it->is_assignment())
450  {
451  if(it->ssa_rhs.id()==ID_if)
452  {
453  conds_seen++;
454  exprt cond_copy(it->ssa_rhs.op0());
455  simplify(cond_copy, ns);
456 
457  if(implications.count(cond_copy)!=0)
458  {
459  sliced_conds++;
460  exprt t_copy1(it->ssa_rhs.op1());
461  exprt t_copy2(it->ssa_rhs.op1());
462  it->ssa_rhs=t_copy1;
463  it->cond_expr.op1().swap(t_copy2);
464  }
465  else
466  {
467  cond_copy.make_not();
468  simplify(cond_copy, ns);
469  if(implications.count(cond_copy)!=0)
470  {
471  sliced_conds++;
472  exprt f_copy1(it->ssa_rhs.op2());
473  exprt f_copy2(it->ssa_rhs.op2());
474  it->ssa_rhs=f_copy1;
475  it->cond_expr.op1().swap(f_copy2);
476  }
477  }
478  }
479  }
480  }
481 
482  std::cout << "Trace slicing effectively removed "
483  << (sliced_SSA_steps + sliced_conds) << " out of "
484  << equation.SSA_steps.size() << " SSA_steps.\n";
485  std::cout << " ("
486  << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
487  << " out of "
488  << (equation.SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
489  << " non-trace, non-location SSA_steps)\n";
490 }
491 
493  event_sett s,
494  irep_idt event)
495 {
496  bool present=s.first.count(event)!=0;
497  return ((s.second && present) || (!s.second && !present));
498 }
499 
501  symex_target_equationt &equation)
502 {
503  size_t merge_count=(merge_map_back.size()) - 1;
504  for(std::vector<exprt>::reverse_iterator i=merge_map_back.rbegin();
505  i!=merge_map_back.rend(); i++)
506  {
507  ssa_exprt merge_sym(merge_symbol);
508  merge_sym.set_level_2(merge_count);
509  merge_count--;
510  guardt t_guard;
511  t_guard.make_true();
512  symex_targett::sourcet empty_source;
513 
514  exprt merge_copy(*i);
515 
516  equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
517  symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
518 
519  SSA_step.guard=t_guard.as_expr();
520  SSA_step.ssa_lhs=merge_sym;
521  SSA_step.ssa_rhs.swap(merge_copy);
523 
524  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
526  SSA_step.source=empty_source;
527  }
528 }
529 
531 {
532  std::set<exprt> s;
533 
534  if(e.id()==ID_symbol)
535  { // Guard or merge
536  const std::string &id_string =
537  id2string(to_symbol_expr(e).get_identifier());
538 
539  std::string::size_type merge_loc=id_string.find("merge#");
540 
541  if(merge_loc==std::string::npos)
542  {
543  exprt e_copy(e);
544  simplify(e_copy, ns);
545  s.insert(e_copy);
546  return s;
547  }
548  else
549  {
550  const std::size_t i = unsafe_string2size_t(id_string.substr(merge_loc+6));
551  if(merge_impl_cache_back[i].first)
552  {
553  return merge_impl_cache_back[i].second;
554  }
555  else
556  {
557  merge_impl_cache_back[i].first=true;
558  exprt merge_copy(merge_map_back[i]);
559  merge_impl_cache_back[i].second=implied_guards(merge_copy);
560  return merge_impl_cache_back[i].second;
561  }
562  }
563  }
564  else if(e.id()==ID_not)
565  { // Definitely a guard
566  exprt e_copy(e);
567  simplify(e_copy, ns);
568  s.insert(e_copy);
569  return s;
570  }
571  else if(e.id()==ID_and)
572  { // Descend into and
573  Forall_operands(it, e)
574  {
575  std::set<exprt> r=implied_guards(*it);
576  for(std::set<exprt>::iterator i=r.begin();
577  i!=r.end(); i++)
578  {
579  s.insert(*i);
580  }
581  }
582  return s;
583  }
584  else if(e.id()==ID_or)
585  { // Descend into or
586  std::vector<std::set<exprt> > rs;
587  Forall_operands(it, e)
588  {
589  rs.push_back(implied_guards(*it));
590  }
591  for(std::set<exprt>::iterator i=rs.front().begin();
592  i!=rs.front().end();)
593  {
594  for(std::vector<std::set<exprt> >::iterator j=rs.begin();
595  j!=rs.end(); j++)
596  {
597  if(j==rs.begin())
598  j++;
599  std::set<exprt>::iterator k=i;
600  i++;
601  if(j->count(*k)==0)
602  {
603  rs.front().erase(k);
604  break;
605  }
606  }
607  }
608  s=rs.front();
609  return s;
610  }
611 
612  return s;
613 }
614 
616 {
617  std::set<exprt> imps=implied_guards(e);
618 
619  for(std::set<exprt>::iterator
620  i=imps.begin();
621  i!=imps.end(); i++)
622  {
623  exprt i_copy(*i);
624  i_copy.make_not();
625  simplify(i_copy, ns);
626  if(imps.count(i_copy)!=0)
627  return true;
628  }
629 
630  return false;
631 }
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:44
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:259
std::set< exprt > sliced_guards
symbol_exprt merge_symbol
The boolean constant true.
Definition: std_expr.h:4486
trace_conditionst t
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:74
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::pair< std::set< irep_idt >, bool > event_sett
The boolean constant false.
Definition: std_expr.h:4497
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:315
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
void swap(irept &irep)
Definition: irep.h:303
#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