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/arith_tools.h>
20 #include <util/exception_utils.h>
21 #include <util/expr_util.h>
22 #include <util/format_expr.h>
23 #include <util/guard.h>
24 #include <util/simplify_expr.h>
25 #include <util/std_expr.h>
26 #include <util/string2int.h>
27 
29  std::string trace_files,
30  symex_target_equationt &equation)
31 {
32  std::cout << "Slicing by trace...\n";
33 
34  merge_identifier="goto_symex::\\merge";
37 
38  std::vector<exprt> trace_conditions;
39 
40  size_t length=trace_files.length();
41  for(size_t idx=0; idx < length; idx++)
42  {
43  const std::string::size_type next=trace_files.find(",", idx);
44  std::string filename=trace_files.substr(idx, next - idx);
45 
46  read_trace(filename);
47 
48  compute_ts_back(equation);
49 
50  exprt t_copy(t[0]);
51  trace_conditions.push_back(t_copy);
52 
53  if(next==std::string::npos)
54  break;
55  idx=next;
56  }
57 
58  exprt trace_condition;
59 
60  if(trace_conditions.size()==1)
61  {
62  trace_condition=trace_conditions[0];
63  }
64  else
65  {
66  trace_condition=exprt(ID_and, typet(ID_bool));
67  trace_condition.operands().reserve(trace_conditions.size());
68  for(std::vector<exprt>::iterator i=trace_conditions.begin();
69  i!=trace_conditions.end(); i++)
70  {
71  trace_condition.move_to_operands(*i);
72  }
73  }
74 
75  simplify(trace_condition, ns);
76 
77  std::set<exprt> implications=implied_guards(trace_condition);
78 
79  for(std::set<exprt>::iterator i=sliced_guards.begin(); i !=
80  sliced_guards.end(); i++)
81  {
82  exprt g_copy(*i);
83 
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'");
88 
89  if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
90  {
91  g_copy = simplify_expr(boolean_negate(g_copy), ns);
92  implications.insert(g_copy);
93  }
94  else if(g_copy.id()==ID_and)
95  {
96  exprt copy_last = boolean_negate(g_copy.operands().back());
97  simplify(copy_last, ns);
98  implications.insert(copy_last);
99  }
100  }
101 
102  slice_SSA_steps(equation, implications); // Slice based on implications
103 
104  guardt t_guard;
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())
126  "invalid file to read trace from: " + filename, "");
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  PRECONDITION(!alphabet.empty());
224  INVARIANT(
225  (alphabet.count(event) != 0) == alphabet_parity,
226  "trace uses symbol not in alphabet: " + event);
227  if(vnext==std::string::npos)
228  break;
229  vidx=vnext;
230  }
231  event_sett es=event_sett(eis, parity);
232  sigma.push_back(es);
233 }
234 
236  symex_target_equationt &equation)
237 {
238  size_t merge_count=0;
239 
240  for(symex_target_equationt::SSA_stepst::reverse_iterator
241  i=equation.SSA_steps.rbegin();
242  i!=equation.SSA_steps.rend();
243  i++)
244  {
245  if(i->is_output() &&
246  !i->io_args.empty() &&
247  i->io_args.front().id()=="trace_event")
248  {
249  irep_idt event = i->io_args.front().get(ID_event);
250 
251  if(!alphabet.empty())
252  {
253  bool present=(alphabet.count(event)!=0);
254  if(alphabet_parity!=present)
255  continue;
256  }
257 
258  exprt guard=i->guard;
259 
260 #if 0
261  std::cout << "EVENT: " << event << '\n';
262  std::cout << "GUARD: " << format(guard) << '\n';
263  for(size_t j=0; j < t.size(); j++)
264  {
265  std::cout << "t[" << j << "]=" << format(t[j]) <<
266  '\n';
267  }
268 #endif
269 
270  bool slice_this=(semantics!=":prefix");
271  std::vector<exprt> merge;
272 
273  for(size_t j=0; j < t.size(); j++)
274  {
275  if((t[j].is_true()) || (t[j].is_false()))
276  {
277  merge.push_back(t[j]);
278  }
279  else
280  {
281  ssa_exprt merge_sym(merge_symbol);
282  merge_sym.set_level_2(merge_count++);
283  exprt t_copy(t[j]);
284  merge_map_back.push_back(t_copy);
285  std::set<exprt> empty_impls;
286  merge_impl_cache_back.push_back
287  (std::pair<bool, std::set<exprt> >(false, empty_impls));
288  merge.push_back(merge_sym);
289  }
290  }
291 
292  for(size_t j=0; j < t.size(); j++)
293  {
294  exprt u_lhs=exprt(ID_and, typet(ID_bool));
295  if((j < sigma.size()) && (matches(sigma[j], event)))
296  {
297  u_lhs.operands().reserve(2);
298  u_lhs.copy_to_operands(guard);
299  if(!sigma_vals[j].empty())
300  {
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();
304  k!=sigma_vals[j].end(); k++)
305  {
306  exprt equal_cond=exprt(ID_equal, bool_typet());
307  equal_cond.operands().reserve(2);
308  equal_cond.copy_to_operands(*pvi);
309  // Should eventually change to handle non-bv types!
310  exprt constant_value=
311  from_integer(unsafe_string2int(id2string(*k)), (*pvi).type());
312  equal_cond.move_to_operands(constant_value);
313  eq_conds.push_back(equal_cond);
314  pvi++;
315  }
316  exprt val_merge=exprt(ID_and, typet(ID_bool));
317  val_merge.operands().reserve(eq_conds.size()+1);
318  val_merge.copy_to_operands(merge[j+1]);
319  for(std::list<exprt>::iterator k=eq_conds.begin();
320  k!= eq_conds.end(); k++)
321  {
322  val_merge.copy_to_operands(*k);
323  }
324  u_lhs.move_to_operands(val_merge);
325  }
326  else
327  {
328  u_lhs.copy_to_operands(merge[j+1]);
329  }
330 
331  simplify(u_lhs, ns);
332 
333  if((!u_lhs.is_false()) && implies_false(u_lhs))
334  u_lhs=false_exprt();
335  if(!u_lhs.is_false())
336  slice_this=false;
337  }
338  else
339  {
340  u_lhs=false_exprt();
341  }
342  exprt u_rhs=exprt(ID_and, typet(ID_bool));
343  if((semantics!=":suffix") || (j != 0))
344  {
345  u_rhs.add_to_operands(boolean_negate(guard), merge[j]);
346  }
347  else
348  {
349  u_rhs.swap(merge[j]);
350  }
351  exprt u_j=exprt(ID_or, typet(ID_bool));
352  u_j.operands().reserve(2);
353  u_j.copy_to_operands(u_lhs);
354  u_j.copy_to_operands(u_rhs);
355 
356  simplify(u_j, ns);
357 
358  t[j]=u_j;
359  }
360 
361  if(semantics==":prefix")
362  t[t.size()-1]=true_exprt();
363 
364  if(slice_this)
365  {
366  exprt guard_copy(guard);
367 
368  sliced_guards.insert(guard_copy);
369  }
370  }
371  }
372 }
373 
375  symex_target_equationt &equation,
376  std::set<exprt> implications)
377 {
378  // Some statistics for our benefit.
379  size_t conds_seen=0;
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;
386 
387  for(symex_target_equationt::SSA_stepst::iterator
388  it=equation.SSA_steps.begin();
389  it!=equation.SSA_steps.end();
390  it++)
391  {
392  if(it->is_output())
393  trace_SSA_steps++;
394  if(it->is_location())
395  location_SSA_steps++;
396  bool sliced_SSA_step=false;
397  exprt guard=it->guard;
398 
399  simplify(guard, ns);
400 
401  if(!guard.is_true())
402  potential_SSA_steps++;
403  // it->output(ns,std::cout);
404  // std::cout << "-----------------\n";
405 
406  if((guard.id()==ID_symbol) || (guard.id() == ID_not))
407  {
408  guard = simplify_expr(boolean_negate(guard), ns);
409 
410  if(implications.count(guard)!=0)
411  {
412  it->cond_expr=true_exprt();
413  it->ssa_rhs=true_exprt();
414  it->guard=false_exprt();
415  sliced_SSA_steps++;
416  if(it->is_output() || it->is_location())
417  trace_loc_sliced++;
418  sliced_SSA_step=true;
419  }
420  }
421  else if(guard.id()==ID_and)
422  {
423  Forall_operands(git, guard)
424  {
425  exprt neg_expr = boolean_negate(*git);
426  simplify(neg_expr, ns);
427 
428  if(implications.count(neg_expr)!=0)
429  {
430  it->cond_expr=true_exprt();
431  it->ssa_rhs=true_exprt();
432  it->guard=false_exprt();
433  sliced_SSA_steps++;
434  if(it->is_output() || it->is_location())
435  trace_loc_sliced++;
436  sliced_SSA_step=true;
437  break; // Sliced, so no need to consider the rest
438  }
439  }
440  else if(guard.id()==ID_or)
441  {
442  std::cout << "Guarded by an OR.\n";
443  }
444  }
445 
446  if(!sliced_SSA_step && it->is_assignment())
447  {
448  if(it->ssa_rhs.id()==ID_if)
449  {
450  conds_seen++;
451  exprt cond_copy(to_if_expr(it->ssa_rhs).cond());
452  simplify(cond_copy, ns);
453 
454  if(implications.count(cond_copy)!=0)
455  {
456  sliced_conds++;
457  exprt t_copy1(to_if_expr(it->ssa_rhs).true_case());
458  exprt t_copy2(to_if_expr(it->ssa_rhs).true_case());
459  it->ssa_rhs=t_copy1;
460  it->cond_expr.op1().swap(t_copy2);
461  }
462  else
463  {
464  cond_copy = simplify_expr(boolean_negate(cond_copy), ns);
465  if(implications.count(cond_copy)!=0)
466  {
467  sliced_conds++;
468  exprt f_copy1(to_if_expr(it->ssa_rhs).false_case());
469  exprt f_copy2(to_if_expr(it->ssa_rhs).false_case());
470  it->ssa_rhs=f_copy1;
471  it->cond_expr.op1().swap(f_copy2);
472  }
473  }
474  }
475  }
476  }
477 
478  std::cout << "Trace slicing effectively removed "
479  << (sliced_SSA_steps + sliced_conds) << " out of "
480  << equation.SSA_steps.size() << " SSA_steps.\n";
481  std::cout << " ("
482  << ((sliced_SSA_steps + sliced_conds) - trace_loc_sliced)
483  << " out of "
484  << (equation.SSA_steps.size()-trace_SSA_steps-location_SSA_steps)
485  << " non-trace, non-location SSA_steps)\n";
486 }
487 
489  event_sett s,
490  irep_idt event)
491 {
492  bool present=s.first.count(event)!=0;
493  return ((s.second && present) || (!s.second && !present));
494 }
495 
497  symex_target_equationt &equation)
498 {
499  size_t merge_count=(merge_map_back.size()) - 1;
500  for(std::vector<exprt>::reverse_iterator i=merge_map_back.rbegin();
501  i!=merge_map_back.rend(); i++)
502  {
503  ssa_exprt merge_sym(merge_symbol);
504  merge_sym.set_level_2(merge_count);
505  merge_count--;
506  guardt t_guard;
507  symex_targett::sourcet empty_source;
508 
509  exprt merge_copy(*i);
510 
511  equation.SSA_steps.push_front(symex_target_equationt::SSA_stept());
512  symex_target_equationt::SSA_stept &SSA_step=equation.SSA_steps.front();
513 
514  SSA_step.guard=t_guard.as_expr();
515  SSA_step.ssa_lhs=merge_sym;
516  SSA_step.ssa_rhs.swap(merge_copy);
518 
519  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
521  SSA_step.source=empty_source;
522  }
523 }
524 
526 {
527  std::set<exprt> s;
528 
529  if(e.id()==ID_symbol)
530  { // Guard or merge
531  const std::string &id_string =
532  id2string(to_symbol_expr(e).get_identifier());
533 
534  std::string::size_type merge_loc=id_string.find("merge#");
535 
536  if(merge_loc==std::string::npos)
537  {
538  exprt e_copy(e);
539  simplify(e_copy, ns);
540  s.insert(e_copy);
541  return s;
542  }
543  else
544  {
545  const std::size_t i = unsafe_string2size_t(id_string.substr(merge_loc+6));
546  if(merge_impl_cache_back[i].first)
547  {
548  return merge_impl_cache_back[i].second;
549  }
550  else
551  {
552  merge_impl_cache_back[i].first=true;
553  exprt merge_copy(merge_map_back[i]);
554  merge_impl_cache_back[i].second=implied_guards(merge_copy);
555  return merge_impl_cache_back[i].second;
556  }
557  }
558  }
559  else if(e.id()==ID_not)
560  { // Definitely a guard
561  exprt e_copy(e);
562  simplify(e_copy, ns);
563  s.insert(e_copy);
564  return s;
565  }
566  else if(e.id()==ID_and)
567  { // Descend into and
568  Forall_operands(it, e)
569  {
570  std::set<exprt> r=implied_guards(*it);
571  for(std::set<exprt>::iterator i=r.begin();
572  i!=r.end(); i++)
573  {
574  s.insert(*i);
575  }
576  }
577  return s;
578  }
579  else if(e.id()==ID_or)
580  { // Descend into or
581  std::vector<std::set<exprt> > rs;
582  Forall_operands(it, e)
583  {
584  rs.push_back(implied_guards(*it));
585  }
586  for(std::set<exprt>::iterator i=rs.front().begin();
587  i!=rs.front().end();)
588  {
589  for(std::vector<std::set<exprt> >::iterator j=rs.begin();
590  j!=rs.end(); j++)
591  {
592  if(j==rs.begin())
593  j++;
594  std::set<exprt>::iterator k=i;
595  i++;
596  if(j->count(*k)==0)
597  {
598  rs.front().erase(k);
599  break;
600  }
601  }
602  }
603  s=rs.front();
604  return s;
605  }
606 
607  return s;
608 }
609 
611 {
612  std::set<exprt> imps=implied_guards(e);
613 
614  for(std::set<exprt>::iterator
615  i=imps.begin();
616  i!=imps.end(); i++)
617  {
618  exprt i_copy = boolean_negate(*i);
619  simplify(i_copy, ns);
620  if(imps.count(i_copy)!=0)
621  return true;
622  }
623 
624  return false;
625 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
symex_slice_by_tracet::t
trace_conditionst t
Definition: slice_by_trace.h:48
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
slice_by_trace.h
symex_target_equationt::SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: symex_target_equation.h:291
format
static format_containert< T > format(const T &o)
Definition: format.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
symex_target_equationt::SSA_stept::guard
exprt guard
Definition: symex_target_equation.h:285
symex_slice_by_tracet::compute_ts_back
void compute_ts_back(symex_target_equationt &equation)
Definition: slice_by_trace.cpp:235
goto_trace_stept::typet::ASSUME
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
symex_target_equationt::SSA_stept::assignment_type
assignment_typet assignment_type
Definition: symex_target_equation.h:292
arith_tools.h
symex_slice_by_tracet::alphabet
alphabett alphabet
Definition: slice_by_trace.h:33
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
irept::make_nil
void make_nil()
Definition: irep.h:315
typet
The type of an expression, extends irept.
Definition: type.h:27
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
symex_slice_by_tracet::parse_alphabet
bool parse_alphabet(std::string read_line)
Definition: slice_by_trace.cpp:166
symex_target_equationt::SSA_stept::type
goto_trace_stept::typet type
Definition: symex_target_equation.h:247
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
file
Definition: kdev_t.h:19
exprt
Base class for all expressions.
Definition: expr.h:54
bool_typet
The Boolean type.
Definition: std_types.h:28
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
symex_slice_by_tracet::sigma_vals
value_tracet sigma_vals
Definition: slice_by_trace.h:44
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
equal_exprt
Equality.
Definition: std_expr.h:1484
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:225
symex_target_equationt::SSA_stept::source
sourcet source
Definition: symex_target_equation.h:246
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
guard.h
string2int.h
symex_slice_by_tracet::alphabet_parity
bool alphabet_parity
Definition: slice_by_trace.h:34
guardt
Definition: guard.h:19
symex_slice_by_tracet::merge_symbol
symbol_exprt merge_symbol
Definition: slice_by_trace.h:58
symex_slice_by_tracet::merge_impl_cache_back
std::vector< std::pair< bool, std::set< exprt > > > merge_impl_cache_back
Definition: slice_by_trace.h:54
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symex_slice_by_tracet::event_sett
std::pair< std::set< irep_idt >, bool > event_sett
Definition: slice_by_trace.h:37
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
symex_slice_by_tracet::assign_merges
void assign_merges(symex_target_equationt &equation)
Definition: slice_by_trace.cpp:496
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
exprt::op1
exprt & op1()
Definition: expr.h:87
symex_slice_by_tracet::ns
const namespacet & ns
Definition: slice_by_trace.h:31
goto_trace_stept::typet::ASSIGNMENT
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
symex_slice_by_tracet::implied_guards
std::set< exprt > implied_guards(exprt e)
Definition: slice_by_trace.cpp:525
symex_slice_by_tracet::read_trace
void read_trace(std::string filename)
Definition: slice_by_trace.cpp:120
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
simplify_expr.h
expr_util.h
Deprecated expression utility functions.
symex_slice_by_tracet::slice_by_trace
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Definition: slice_by_trace.cpp:28
format_expr.h
symex_slice_by_tracet::matches
bool matches(event_sett s, irep_idt event)
Definition: slice_by_trace.cpp:488
symex_slice_by_tracet::semantics
std::string semantics
Definition: slice_by_trace.h:35
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
symex_slice_by_tracet::implies_false
bool implies_false(exprt e)
Definition: slice_by_trace.cpp:610
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
symex_slice_by_tracet::parse_events
void parse_events(std::string read_line)
Definition: slice_by_trace.cpp:186
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
symex_slice_by_tracet::sliced_guards
std::set< exprt > sliced_guards
Definition: slice_by_trace.h:50
ssa_exprt::set_level_2
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:130
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
unsafe_string2size_t
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:74
symex_slice_by_tracet::merge_identifier
irep_idt merge_identifier
Definition: slice_by_trace.h:56
symex_target_equationt::SSA_stept::cond_expr
exprt cond_expr
Definition: symex_target_equation.h:295
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
exprt::operands
operandst & operands()
Definition: expr.h:78
r
static int8_t r
Definition: irep_hash.h:59
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
symex_targett::assignment_typet::HIDDEN
symex_slice_by_tracet::sigma
event_tracet sigma
Definition: slice_by_trace.h:40
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symex_target_equationt::SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: symex_target_equation.h:289
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
is_true
bool is_true(const literalt &l)
Definition: literal.h:197
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:37
std_expr.h
symex_slice_by_tracet::slice_SSA_steps
void slice_SSA_steps(symex_target_equationt &equation, std::set< exprt > implications)
Definition: slice_by_trace.cpp:374
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
symex_slice_by_tracet::merge_map_back
std::vector< exprt > merge_map_back
Definition: slice_by_trace.h:52
unsafe_string2int
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
validation_modet::INVARIANT