cprover
symex_target_equation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
12 
13 #include "symex_target_equation.h"
14 
15 #include <util/format_expr.h>
16 #include <util/std_expr.h>
17 
20 
21 #include "goto_symex_state.h"
22 #include "ssa_step.h"
23 
25 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
26 {
27  return [step_index, &step](solver_hardnesst &hardness) {
28  hardness.register_ssa(step_index, step.cond_expr, step.source.pc);
29  };
30 }
31 
33  const exprt &guard,
34  const ssa_exprt &ssa_object,
35  unsigned atomic_section_id,
36  const sourcet &source)
37 {
38  SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
39  SSA_stept &SSA_step=SSA_steps.back();
40 
41  SSA_step.guard=guard;
42  SSA_step.ssa_lhs=ssa_object;
43  SSA_step.atomic_section_id=atomic_section_id;
44 
45  merge_ireps(SSA_step);
46 }
47 
49  const exprt &guard,
50  const ssa_exprt &ssa_object,
51  unsigned atomic_section_id,
52  const sourcet &source)
53 {
55  SSA_stept &SSA_step=SSA_steps.back();
56 
57  SSA_step.guard=guard;
58  SSA_step.ssa_lhs=ssa_object;
59  SSA_step.atomic_section_id=atomic_section_id;
60 
61  merge_ireps(SSA_step);
62 }
63 
66  const exprt &guard,
67  const sourcet &source)
68 {
69  SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
70  SSA_stept &SSA_step=SSA_steps.back();
71  SSA_step.guard=guard;
72 
73  merge_ireps(SSA_step);
74 }
75 
77  const exprt &guard,
78  const sourcet &source)
79 {
81  SSA_stept &SSA_step=SSA_steps.back();
82  SSA_step.guard=guard;
83 
84  merge_ireps(SSA_step);
85 }
86 
89  const exprt &guard,
90  unsigned atomic_section_id,
91  const sourcet &source)
92 {
94  SSA_stept &SSA_step=SSA_steps.back();
95  SSA_step.guard=guard;
96  SSA_step.atomic_section_id=atomic_section_id;
97 
98  merge_ireps(SSA_step);
99 }
100 
103  const exprt &guard,
104  unsigned atomic_section_id,
105  const sourcet &source)
106 {
107  SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
108  SSA_stept &SSA_step=SSA_steps.back();
109  SSA_step.guard=guard;
110  SSA_step.atomic_section_id=atomic_section_id;
111 
112  merge_ireps(SSA_step);
113 }
114 
116  const exprt &guard,
117  const ssa_exprt &ssa_lhs,
118  const exprt &ssa_full_lhs,
119  const exprt &original_full_lhs,
120  const exprt &ssa_rhs,
121  const sourcet &source,
122  assignment_typet assignment_type)
123 {
124  PRECONDITION(ssa_lhs.is_not_nil());
125 
126  SSA_steps.emplace_back(SSA_assignment_stept{source,
127  guard,
128  ssa_lhs,
129  ssa_full_lhs,
130  original_full_lhs,
131  ssa_rhs,
132  assignment_type});
133 
134  merge_ireps(SSA_steps.back());
135 }
136 
138  const exprt &guard,
139  const ssa_exprt &ssa_lhs,
140  const exprt &initializer,
141  const sourcet &source,
142  assignment_typet assignment_type)
143 {
144  PRECONDITION(ssa_lhs.is_not_nil());
145 
146  SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
147  SSA_stept &SSA_step=SSA_steps.back();
148 
149  SSA_step.guard=guard;
150  SSA_step.ssa_lhs=ssa_lhs;
151  SSA_step.ssa_full_lhs = initializer;
152  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
153  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
154 
155  // the condition is trivially true, and only
156  // there so we see the symbols
157  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
158 
159  merge_ireps(SSA_step);
160 }
161 
164  const exprt &,
165  const ssa_exprt &,
166  const sourcet &)
167 {
168  // we currently don't record these
169 }
170 
172  const exprt &guard,
173  const sourcet &source)
174 {
175  SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
176  SSA_stept &SSA_step=SSA_steps.back();
177 
178  SSA_step.guard=guard;
179 
180  merge_ireps(SSA_step);
181 }
182 
184  const exprt &guard,
185  const irep_idt &function_id,
186  const std::vector<renamedt<exprt, L2>> &function_arguments,
187  const sourcet &source,
188  const bool hidden)
189 {
191  SSA_stept &SSA_step=SSA_steps.back();
192 
193  SSA_step.guard = guard;
194  SSA_step.called_function = function_id;
195  for(const auto &arg : function_arguments)
196  SSA_step.ssa_function_arguments.emplace_back(arg.get());
197  SSA_step.hidden = hidden;
198 
199  merge_ireps(SSA_step);
200 }
201 
203  const exprt &guard,
204  const irep_idt &function_id,
205  const sourcet &source,
206  const bool hidden)
207 {
209  SSA_stept &SSA_step=SSA_steps.back();
210 
211  SSA_step.guard = guard;
212  SSA_step.called_function = function_id;
213  SSA_step.hidden = hidden;
214 
215  merge_ireps(SSA_step);
216 }
217 
219  const exprt &guard,
220  const sourcet &source,
221  const irep_idt &output_id,
222  const std::list<renamedt<exprt, L2>> &args)
223 {
224  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
225  SSA_stept &SSA_step=SSA_steps.back();
226 
227  SSA_step.guard=guard;
228  for(const auto &arg : args)
229  SSA_step.io_args.emplace_back(arg.get());
230  SSA_step.io_id=output_id;
231 
232  merge_ireps(SSA_step);
233 }
234 
236  const exprt &guard,
237  const sourcet &source,
238  const irep_idt &output_id,
239  const irep_idt &fmt,
240  const std::list<exprt> &args)
241 {
242  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
243  SSA_stept &SSA_step=SSA_steps.back();
244 
245  SSA_step.guard=guard;
246  SSA_step.io_args=args;
247  SSA_step.io_id=output_id;
248  SSA_step.formatted=true;
249  SSA_step.format_string=fmt;
250 
251  merge_ireps(SSA_step);
252 }
253 
255  const exprt &guard,
256  const sourcet &source,
257  const irep_idt &input_id,
258  const std::list<exprt> &args)
259 {
260  SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
261  SSA_stept &SSA_step=SSA_steps.back();
262 
263  SSA_step.guard=guard;
264  SSA_step.io_args=args;
265  SSA_step.io_id=input_id;
266 
267  merge_ireps(SSA_step);
268 }
269 
271  const exprt &guard,
272  const exprt &cond,
273  const sourcet &source)
274 {
275  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
276  SSA_stept &SSA_step=SSA_steps.back();
277 
278  SSA_step.guard=guard;
279  SSA_step.cond_expr=cond;
280 
281  merge_ireps(SSA_step);
282 }
283 
285  const exprt &guard,
286  const exprt &cond,
287  const std::string &msg,
288  const sourcet &source)
289 {
290  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
291  SSA_stept &SSA_step=SSA_steps.back();
292 
293  SSA_step.guard=guard;
294  SSA_step.cond_expr=cond;
295  SSA_step.comment=msg;
296 
297  merge_ireps(SSA_step);
298 }
299 
301  const exprt &guard,
302  const renamedt<exprt, L2> &cond,
303  const sourcet &source)
304 {
305  SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
306  SSA_stept &SSA_step=SSA_steps.back();
307 
308  SSA_step.guard=guard;
309  SSA_step.cond_expr = cond.get();
310 
311  merge_ireps(SSA_step);
312 }
313 
315  const exprt &cond,
316  const std::string &msg,
317  const sourcet &source)
318 {
319  // like assumption, but with global effect
320  SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
321  SSA_stept &SSA_step=SSA_steps.back();
322 
323  SSA_step.guard=true_exprt();
324  SSA_step.cond_expr=cond;
325  SSA_step.comment=msg;
326 
327  merge_ireps(SSA_step);
328 }
329 
331  decision_proceduret &decision_procedure)
332 {
333  with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
334  hardness.register_ssa_size(SSA_steps.size());
335  });
336 
337  convert_guards(decision_procedure);
338  convert_assignments(decision_procedure);
339  convert_decls(decision_procedure);
340  convert_assumptions(decision_procedure);
341  convert_goto_instructions(decision_procedure);
342  convert_function_calls(decision_procedure);
343  convert_io(decision_procedure);
344  convert_constraints(decision_procedure);
345 }
346 
348 {
349  convert_without_assertions(decision_procedure);
350  convert_assertions(decision_procedure);
351 }
352 
354  decision_proceduret &decision_procedure)
355 {
356  std::size_t step_index = 0;
357  for(auto &step : SSA_steps)
358  {
359  if(step.is_assignment() && !step.ignore && !step.converted)
360  {
361  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
362  step.output(mstream);
363  mstream << messaget::eom;
364  });
365 
366  decision_procedure.set_to_true(step.cond_expr);
367  step.converted = true;
369  decision_procedure, hardness_register_ssa(step_index, step));
370  }
371  ++step_index;
372  }
373 }
374 
376  decision_proceduret &decision_procedure)
377 {
378  std::size_t step_index = 0;
379  for(auto &step : SSA_steps)
380  {
381  if(step.is_decl() && !step.ignore && !step.converted)
382  {
383  // The result is not used, these have no impact on
384  // the satisfiability of the formula.
385  decision_procedure.handle(step.cond_expr);
386  step.converted = true;
388  decision_procedure, hardness_register_ssa(step_index, step));
389  }
390  ++step_index;
391  }
392 }
393 
395  decision_proceduret &decision_procedure)
396 {
397  std::size_t step_index = 0;
398  for(auto &step : SSA_steps)
399  {
400  if(step.ignore)
401  step.guard_handle = false_exprt();
402  else
403  {
404  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
405  step.output(mstream);
406  mstream << messaget::eom;
407  });
408 
409  step.guard_handle = decision_procedure.handle(step.guard);
411  decision_procedure, hardness_register_ssa(step_index, step));
412  }
413  ++step_index;
414  }
415 }
416 
418  decision_proceduret &decision_procedure)
419 {
420  std::size_t step_index = 0;
421  for(auto &step : SSA_steps)
422  {
423  if(step.is_assume())
424  {
425  if(step.ignore)
426  step.cond_handle = true_exprt();
427  else
428  {
430  log.debug(), [&step](messaget::mstreamt &mstream) {
431  step.output(mstream);
432  mstream << messaget::eom;
433  });
434 
435  step.cond_handle = decision_procedure.handle(step.cond_expr);
436 
438  decision_procedure, hardness_register_ssa(step_index, step));
439  }
440  }
441  ++step_index;
442  }
443 }
444 
446  decision_proceduret &decision_procedure)
447 {
448  std::size_t step_index = 0;
449  for(auto &step : SSA_steps)
450  {
451  if(step.is_goto())
452  {
453  if(step.ignore)
454  step.cond_handle = true_exprt();
455  else
456  {
458  log.debug(), [&step](messaget::mstreamt &mstream) {
459  step.output(mstream);
460  mstream << messaget::eom;
461  });
462 
463  step.cond_handle = decision_procedure.handle(step.cond_expr);
465  decision_procedure, hardness_register_ssa(step_index, step));
466  }
467  }
468  ++step_index;
469  }
470 }
471 
473  decision_proceduret &decision_procedure)
474 {
475  std::size_t step_index = 0;
476  for(auto &step : SSA_steps)
477  {
478  if(step.is_constraint() && !step.ignore && !step.converted)
479  {
480  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
481  step.output(mstream);
482  mstream << messaget::eom;
483  });
484 
485  decision_procedure.set_to_true(step.cond_expr);
486  step.converted = true;
487 
489  decision_procedure, hardness_register_ssa(step_index, step));
490  }
491  ++step_index;
492  }
493 }
494 
496  decision_proceduret &decision_procedure,
497  bool optimized_for_single_assertions)
498 {
499  // we find out if there is only _one_ assertion,
500  // which allows for a simpler formula
501 
502  std::size_t number_of_assertions=count_assertions();
503 
504  if(number_of_assertions==0)
505  return;
506 
507  if(number_of_assertions == 1 && optimized_for_single_assertions)
508  {
509  std::size_t step_index = 0;
510  for(auto &step : SSA_steps)
511  {
512  // hide already converted assertions in the error trace
513  if(step.is_assert() && step.converted)
514  step.hidden = true;
515 
516  if(step.is_assert() && !step.ignore && !step.converted)
517  {
518  step.converted = true;
519  decision_procedure.set_to_false(step.cond_expr);
520  step.cond_handle = false_exprt();
521 
523  decision_procedure, hardness_register_ssa(step_index, step));
524  return; // prevent further assumptions!
525  }
526  else if(step.is_assume())
527  {
528  decision_procedure.set_to_true(step.cond_expr);
529 
531  decision_procedure, hardness_register_ssa(step_index, step));
532  }
533  ++step_index;
534  }
535 
536  UNREACHABLE; // unreachable
537  }
538 
539  // We do (NOT a1) OR (NOT a2) ...
540  // where the a's are the assertions
541  or_exprt::operandst disjuncts;
542  disjuncts.reserve(number_of_assertions);
543 
545 
546  std::vector<goto_programt::const_targett> involved_steps;
547 
548  for(auto &step : SSA_steps)
549  {
550  // hide already converted assertions in the error trace
551  if(step.is_assert() && step.converted)
552  step.hidden = true;
553 
554  if(step.is_assert() && !step.ignore && !step.converted)
555  {
556  step.converted = true;
557 
558  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
559  step.output(mstream);
560  mstream << messaget::eom;
561  });
562 
563  implies_exprt implication(
564  assumption,
565  step.cond_expr);
566 
567  // do the conversion
568  step.cond_handle = decision_procedure.handle(implication);
569 
571  decision_procedure,
572  [&involved_steps, &step](solver_hardnesst &hardness) {
573  involved_steps.push_back(step.source.pc);
574  });
575 
576  // store disjunct
577  disjuncts.push_back(not_exprt(step.cond_handle));
578  }
579  else if(step.is_assume())
580  {
581  // the assumptions have been converted before
582  // avoid deep nesting of ID_and expressions
583  if(assumption.id()==ID_and)
584  assumption.copy_to_operands(step.cond_handle);
585  else
586  assumption = and_exprt(assumption, step.cond_handle);
587 
589  decision_procedure,
590  [&involved_steps, &step](solver_hardnesst &hardness) {
591  involved_steps.push_back(step.source.pc);
592  });
593  }
594  }
595 
596  const auto assertion_disjunction = disjunction(disjuncts);
597  // the below is 'true' if there are no assertions
598  decision_procedure.set_to_true(assertion_disjunction);
599 
601  decision_procedure,
602  [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
603  hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
604  });
605 }
606 
608  decision_proceduret &decision_procedure)
609 {
610  std::size_t step_index = 0;
611  for(auto &step : SSA_steps)
612  {
613  if(!step.ignore)
614  {
615  and_exprt::operandst conjuncts;
616  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
617 
618  for(const auto &arg : step.ssa_function_arguments)
619  {
620  if(arg.is_constant() ||
621  arg.id()==ID_string_constant)
622  step.converted_function_arguments.push_back(arg);
623  else
624  {
625  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
626  symbol_exprt symbol(identifier, arg.type());
627 
628  equal_exprt eq(arg, symbol);
629  merge_irep(eq);
630 
631  decision_procedure.set_to(eq, true);
632  conjuncts.push_back(eq);
633  step.converted_function_arguments.push_back(symbol);
634  }
635  }
637  decision_procedure,
638  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
639  hardness.register_ssa(
640  step_index, conjunction(conjuncts), step.source.pc);
641  });
642  }
643  ++step_index;
644  }
645 }
646 
648 {
649  std::size_t step_index = 0;
650  for(auto &step : SSA_steps)
651  {
652  if(!step.ignore)
653  {
654  and_exprt::operandst conjuncts;
655  for(const auto &arg : step.io_args)
656  {
657  if(arg.is_constant() ||
658  arg.id()==ID_string_constant)
659  step.converted_io_args.push_back(arg);
660  else
661  {
662  const irep_idt identifier =
663  "symex::io::" + std::to_string(io_count++);
664  symbol_exprt symbol(identifier, arg.type());
665 
666  equal_exprt eq(arg, symbol);
667  merge_irep(eq);
668 
669  decision_procedure.set_to(eq, true);
670  conjuncts.push_back(eq);
671  step.converted_io_args.push_back(symbol);
672  }
673  }
675  decision_procedure,
676  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
677  hardness.register_ssa(
678  step_index, conjunction(conjuncts), step.source.pc);
679  });
680  }
681  ++step_index;
682  }
683 }
684 
689 {
690  merge_irep(SSA_step.guard);
691 
692  merge_irep(SSA_step.ssa_lhs);
693  merge_irep(SSA_step.ssa_full_lhs);
694  merge_irep(SSA_step.original_full_lhs);
695  merge_irep(SSA_step.ssa_rhs);
696 
697  merge_irep(SSA_step.cond_expr);
698 
699  for(auto &step : SSA_step.io_args)
700  merge_irep(step);
701 
702  for(auto &arg : SSA_step.ssa_function_arguments)
703  merge_irep(arg);
704 
705  // converted_io_args is merged in convert_io
706 }
707 
708 void symex_target_equationt::output(std::ostream &out) const
709 {
710  for(const auto &step : SSA_steps)
711  {
712  step.output(out);
713  out << "--------------\n";
714  }
715 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:69
symex_target_equation.h
solver_hardnesst::register_ssa_size
void register_ssa_size(std::size_t size)
Definition: solver_hardness.cpp:67
goto_trace_stept::typet::LOCATION
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
goto_trace_stept::typet::ASSUME
SSA_stept::comment
std::string comment
Definition: ssa_step.h:149
hardness_collector.h
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:270
symex_target_equationt::function_return
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
Definition: symex_target_equation.cpp:202
symex_target_equationt::memory_barrier
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
Definition: symex_target_equation.cpp:76
SSA_stept::atomic_section_id
unsigned atomic_section_id
Definition: ssa_step.h:169
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:44
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
hardness_collectort::handlert
std::function< void(solver_hardnesst &)> handlert
Definition: hardness_collector.h:25
decision_proceduret
Definition: decision_procedure.h:20
symex_target_equationt::convert_goto_instructions
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
Definition: symex_target_equation.cpp:445
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:295
and_exprt
Boolean AND.
Definition: std_expr.h:2136
exprt
Base class for all expressions.
Definition: expr.h:52
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
Definition: decision_procedure.cpp:23
symex_target_equationt::argument_count
std::size_t argument_count
Definition: symex_target_equation.h:302
SSA_stept::formatted
bool formatted
Definition: ssa_step.h:158
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:47
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
SSA_stept::called_function
irep_idt called_function
Definition: ssa_step.h:163
symex_target_equationt::convert_decls
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
Definition: symex_target_equation.cpp:375
equal_exprt
Equality.
Definition: std_expr.h:1189
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
renamedt::get
const underlyingt & get() const
Definition: renamed.h:34
SSA_stept::ssa_function_arguments
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:166
ssa_step.h
decision_procedure.h
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
Definition: decision_procedure.cpp:28
symex_targett::assignment_typet::STATE
SSA_stept::io_args
std::list< exprt > io_args
Definition: ssa_step.h:159
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:171
symex_target_equationt::convert_assignments
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
Definition: symex_target_equation.cpp:353
hardness_register_ssa
static hardness_collectort::handlert hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
Definition: symex_target_equation.cpp:25
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
decision_proceduret::set_to
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
symex_target_equationt::atomic_end
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
Definition: symex_target_equation.cpp:102
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:240
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
goto_trace_stept::typet::OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
SSA_stept::io_id
irep_idt io_id
Definition: ssa_step.h:157
SSA_assignment_stept
Definition: ssa_step.h:203
goto_trace_stept::typet::DECL
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
goto_trace_stept::typet::ASSERT
SSA_stept::ssa_full_lhs
exprt ssa_full_lhs
Definition: ssa_step.h:142
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:147
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symex_target_equationt::dead
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
Definition: symex_target_equation.cpp:163
symex_target_equationt::convert_io
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
Definition: symex_target_equation.cpp:647
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3963
symex_target_equationt::convert_constraints
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
Definition: symex_target_equation.cpp:472
goto_trace_stept::typet::INPUT
goto_trace_stept::typet::ATOMIC_END
decision_proceduret::handle
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
symex_target_equationt::io_count
std::size_t io_count
Definition: symex_target_equation.h:299
solver_hardnesst::register_ssa
void register_ssa(std::size_t ssa_index, const exprt ssa_expression, goto_programt::const_targett pc)
Called from the symtex_target_equationt::convert_*, this function associates an SSA step to all the s...
Definition: solver_hardness.cpp:46
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:65
solver_hardnesst::register_assertion_ssas
void register_assertion_ssas(const exprt ssa_expression, const std::vector< goto_programt::const_targett > &pcs)
Called from the symtex_target_equationt::convert_assertions, this function associates the disjunction...
Definition: solver_hardness.cpp:76
SSA_stept::hidden
bool hidden
Definition: ssa_step.h:135
symex_target_equationt::convert_guards
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
Definition: symex_target_equation.cpp:394
symex_target_equationt::shared_write
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
Definition: symex_target_equation.cpp:48
goto_trace_stept::typet::SPAWN
symex_target_equationt::merge_ireps
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
Definition: symex_target_equation.cpp:688
goto_trace_stept::typet::MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
symex_target_equationt::atomic_begin
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
Definition: symex_target_equation.cpp:88
symex_target_equationt::convert_assertions
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
Definition: symex_target_equation.cpp:495
symex_target_equationt::assertion
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
Definition: symex_target_equation.cpp:284
format_expr.h
symex_target_equationt::output_fmt
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
Definition: symex_target_equation.cpp:235
goto_trace_stept::typet::GOTO
symex_target_equationt::goto_instruction
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
Definition: symex_target_equation.cpp:300
SSA_stept::original_full_lhs
exprt original_full_lhs
Definition: ssa_step.h:142
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:44
goto_symex_state.h
symex_target_equationt::function_call
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Definition: symex_target_equation.cpp:183
symex_target_equationt::convert_function_calls
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
Definition: symex_target_equation.cpp:607
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
goto_trace_stept::typet::ATOMIC_BEGIN
messaget::conditional_output
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:138
symex_target_equationt::convert
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:347
symex_target_equationt::shared_read
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
Definition: symex_target_equation.cpp:32
SSA_stept::format_string
irep_idt format_string
Definition: ssa_step.h:157
symex_target_equationt::convert_without_assertions
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:330
symex_target_equationt::constraint
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
Definition: symex_target_equation.cpp:314
messaget::mstreamt
Definition: message.h:223
implies_exprt
Boolean implication.
Definition: std_expr.h:2199
goto_trace_stept::typet::SHARED_READ
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
messaget::debug
mstreamt & debug() const
Definition: message.h:429
symex_target_equationt::convert_assumptions
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
Definition: symex_target_equation.cpp:417
goto_trace_stept::typet::FUNCTION_CALL
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
symex_target_equationt::decl
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Definition: symex_target_equation.cpp:137
std_expr.h
with_solver_hardness
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
Definition: hardness_collector.h:32
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
symex_target_equationt::input
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
Definition: symex_target_equation.cpp:254
goto_trace_stept::typet::CONSTRAINT
symex_target_equationt::output
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
Definition: symex_target_equation.cpp:218
symex_target_equationt::log
messaget log
Definition: symex_target_equation.h:292
not_exprt
Boolean negation.
Definition: std_expr.h:2842
symex_target_equationt::assignment
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
Definition: symex_target_equation.cpp:115