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 <chrono>
16 
17 #include <util/std_expr.h>
18 
21 
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  const auto convert_SSA_start = std::chrono::steady_clock::now();
350 
351  convert_without_assertions(decision_procedure);
352  convert_assertions(decision_procedure);
353 
354  const auto convert_SSA_stop = std::chrono::steady_clock::now();
355  std::chrono::duration<double> convert_SSA_runtime =
356  std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
357  log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
358  << messaget::eom;
359 }
360 
362  decision_proceduret &decision_procedure)
363 {
364  std::size_t step_index = 0;
365  for(auto &step : SSA_steps)
366  {
367  if(step.is_assignment() && !step.ignore && !step.converted)
368  {
369  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
370  step.output(mstream);
371  mstream << messaget::eom;
372  });
373 
374  decision_procedure.set_to_true(step.cond_expr);
375  step.converted = true;
377  decision_procedure, hardness_register_ssa(step_index, step));
378  }
379  ++step_index;
380  }
381 }
382 
384  decision_proceduret &decision_procedure)
385 {
386  std::size_t step_index = 0;
387  for(auto &step : SSA_steps)
388  {
389  if(step.is_decl() && !step.ignore && !step.converted)
390  {
391  // The result is not used, these have no impact on
392  // the satisfiability of the formula.
393  decision_procedure.handle(step.cond_expr);
394  step.converted = true;
396  decision_procedure, hardness_register_ssa(step_index, step));
397  }
398  ++step_index;
399  }
400 }
401 
403  decision_proceduret &decision_procedure)
404 {
405  std::size_t step_index = 0;
406  for(auto &step : SSA_steps)
407  {
408  if(step.ignore)
409  step.guard_handle = false_exprt();
410  else
411  {
412  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
413  step.output(mstream);
414  mstream << messaget::eom;
415  });
416 
417  step.guard_handle = decision_procedure.handle(step.guard);
419  decision_procedure, hardness_register_ssa(step_index, step));
420  }
421  ++step_index;
422  }
423 }
424 
426  decision_proceduret &decision_procedure)
427 {
428  std::size_t step_index = 0;
429  for(auto &step : SSA_steps)
430  {
431  if(step.is_assume())
432  {
433  if(step.ignore)
434  step.cond_handle = true_exprt();
435  else
436  {
438  log.debug(), [&step](messaget::mstreamt &mstream) {
439  step.output(mstream);
440  mstream << messaget::eom;
441  });
442 
443  step.cond_handle = decision_procedure.handle(step.cond_expr);
444 
446  decision_procedure, hardness_register_ssa(step_index, step));
447  }
448  }
449  ++step_index;
450  }
451 }
452 
454  decision_proceduret &decision_procedure)
455 {
456  std::size_t step_index = 0;
457  for(auto &step : SSA_steps)
458  {
459  if(step.is_goto())
460  {
461  if(step.ignore)
462  step.cond_handle = true_exprt();
463  else
464  {
466  log.debug(), [&step](messaget::mstreamt &mstream) {
467  step.output(mstream);
468  mstream << messaget::eom;
469  });
470 
471  step.cond_handle = decision_procedure.handle(step.cond_expr);
473  decision_procedure, hardness_register_ssa(step_index, step));
474  }
475  }
476  ++step_index;
477  }
478 }
479 
481  decision_proceduret &decision_procedure)
482 {
483  std::size_t step_index = 0;
484  for(auto &step : SSA_steps)
485  {
486  if(step.is_constraint() && !step.ignore && !step.converted)
487  {
488  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
489  step.output(mstream);
490  mstream << messaget::eom;
491  });
492 
493  decision_procedure.set_to_true(step.cond_expr);
494  step.converted = true;
495 
497  decision_procedure, hardness_register_ssa(step_index, step));
498  }
499  ++step_index;
500  }
501 }
502 
504  decision_proceduret &decision_procedure,
505  bool optimized_for_single_assertions)
506 {
507  // we find out if there is only _one_ assertion,
508  // which allows for a simpler formula
509 
510  std::size_t number_of_assertions=count_assertions();
511 
512  if(number_of_assertions==0)
513  return;
514 
515  if(number_of_assertions == 1 && optimized_for_single_assertions)
516  {
517  std::size_t step_index = 0;
518  for(auto &step : SSA_steps)
519  {
520  // hide already converted assertions in the error trace
521  if(step.is_assert() && step.converted)
522  step.hidden = true;
523 
524  if(step.is_assert() && !step.ignore && !step.converted)
525  {
526  step.converted = true;
527  decision_procedure.set_to_false(step.cond_expr);
528  step.cond_handle = false_exprt();
529 
531  decision_procedure, hardness_register_ssa(step_index, step));
532  return; // prevent further assumptions!
533  }
534  else if(step.is_assume())
535  {
536  decision_procedure.set_to_true(step.cond_expr);
537 
539  decision_procedure, hardness_register_ssa(step_index, step));
540  }
541  ++step_index;
542  }
543 
544  UNREACHABLE; // unreachable
545  }
546 
547  // We do (NOT a1) OR (NOT a2) ...
548  // where the a's are the assertions
549  or_exprt::operandst disjuncts;
550  disjuncts.reserve(number_of_assertions);
551 
553 
554  std::vector<goto_programt::const_targett> involved_steps;
555 
556  for(auto &step : SSA_steps)
557  {
558  // hide already converted assertions in the error trace
559  if(step.is_assert() && step.converted)
560  step.hidden = true;
561 
562  if(step.is_assert() && !step.ignore && !step.converted)
563  {
564  step.converted = true;
565 
566  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
567  step.output(mstream);
568  mstream << messaget::eom;
569  });
570 
571  implies_exprt implication(
572  assumption,
573  step.cond_expr);
574 
575  // do the conversion
576  step.cond_handle = decision_procedure.handle(implication);
577 
579  decision_procedure,
580  [&involved_steps, &step](solver_hardnesst &hardness) {
581  involved_steps.push_back(step.source.pc);
582  });
583 
584  // store disjunct
585  disjuncts.push_back(not_exprt(step.cond_handle));
586  }
587  else if(step.is_assume())
588  {
589  // the assumptions have been converted before
590  // avoid deep nesting of ID_and expressions
591  if(assumption.id()==ID_and)
592  assumption.copy_to_operands(step.cond_handle);
593  else
594  assumption = and_exprt(assumption, step.cond_handle);
595 
597  decision_procedure,
598  [&involved_steps, &step](solver_hardnesst &hardness) {
599  involved_steps.push_back(step.source.pc);
600  });
601  }
602  }
603 
604  const auto assertion_disjunction = disjunction(disjuncts);
605  // the below is 'true' if there are no assertions
606  decision_procedure.set_to_true(assertion_disjunction);
607 
609  decision_procedure,
610  [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
611  hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
612  });
613 }
614 
616  decision_proceduret &decision_procedure)
617 {
618  std::size_t step_index = 0;
619  for(auto &step : SSA_steps)
620  {
621  if(!step.ignore)
622  {
623  and_exprt::operandst conjuncts;
624  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
625 
626  for(const auto &arg : step.ssa_function_arguments)
627  {
628  if(arg.is_constant() ||
629  arg.id()==ID_string_constant)
630  step.converted_function_arguments.push_back(arg);
631  else
632  {
633  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
634  symbol_exprt symbol(identifier, arg.type());
635 
636  equal_exprt eq(arg, symbol);
637  merge_irep(eq);
638 
639  decision_procedure.set_to(eq, true);
640  conjuncts.push_back(eq);
641  step.converted_function_arguments.push_back(symbol);
642  }
643  }
645  decision_procedure,
646  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
647  hardness.register_ssa(
648  step_index, conjunction(conjuncts), step.source.pc);
649  });
650  }
651  ++step_index;
652  }
653 }
654 
656 {
657  std::size_t step_index = 0;
658  for(auto &step : SSA_steps)
659  {
660  if(!step.ignore)
661  {
662  and_exprt::operandst conjuncts;
663  for(const auto &arg : step.io_args)
664  {
665  if(arg.is_constant() ||
666  arg.id()==ID_string_constant)
667  step.converted_io_args.push_back(arg);
668  else
669  {
670  const irep_idt identifier =
671  "symex::io::" + std::to_string(io_count++);
672  symbol_exprt symbol(identifier, arg.type());
673 
674  equal_exprt eq(arg, symbol);
675  merge_irep(eq);
676 
677  decision_procedure.set_to(eq, true);
678  conjuncts.push_back(eq);
679  step.converted_io_args.push_back(symbol);
680  }
681  }
683  decision_procedure,
684  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
685  hardness.register_ssa(
686  step_index, conjunction(conjuncts), step.source.pc);
687  });
688  }
689  ++step_index;
690  }
691 }
692 
697 {
698  merge_irep(SSA_step.guard);
699 
700  merge_irep(SSA_step.ssa_lhs);
701  merge_irep(SSA_step.ssa_full_lhs);
702  merge_irep(SSA_step.original_full_lhs);
703  merge_irep(SSA_step.ssa_rhs);
704 
705  merge_irep(SSA_step.cond_expr);
706 
707  for(auto &step : SSA_step.io_args)
708  merge_irep(step);
709 
710  for(auto &arg : SSA_step.ssa_function_arguments)
711  merge_irep(arg);
712 
713  // converted_io_args is merged in convert_io
714 }
715 
716 void symex_target_equationt::output(std::ostream &out) const
717 {
718  for(const auto &step : SSA_steps)
719  {
720  step.output(out);
721  out << "--------------\n";
722  }
723 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:69
symex_target_equation.h
Generate Equation using Symbolic Execution.
solver_hardnesst::register_ssa_size
void register_ssa_size(std::size_t size)
Definition: solver_hardness.cpp:64
goto_trace_stept::typet::LOCATION
@ 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:34
goto_trace_stept::typet::ASSUME
@ ASSUME
SSA_stept::comment
std::string comment
Definition: ssa_step.h:151
hardness_collector.h
Capability to collect the statistics of the complexity of individual solver queries.
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:171
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:47
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:42
messaget::status
mstreamt & status() const
Definition: message.h:414
hardness_collectort::handlert
std::function< void(solver_hardnesst &)> handlert
Definition: hardness_collector.h:25
decision_proceduret
Definition: decision_procedure.h:21
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:453
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:288
and_exprt
Boolean AND.
Definition: std_expr.h:1920
exprt
Base class for all expressions.
Definition: expr.h:54
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:295
SSA_stept::formatted
bool formatted
Definition: ssa_step.h:160
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
SSA_stept::guard
exprt guard
Definition: ssa_step.h:139
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:49
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
SSA_stept::called_function
irep_idt called_function
Definition: ssa_step.h:165
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:383
equal_exprt
Equality.
Definition: std_expr.h:1225
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:40
SSA_stept::ssa_function_arguments
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:168
ssa_step.h
decision_procedure.h
Decision Procedure Interface.
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
@ STATE
SSA_stept::io_args
std::list< exprt > io_args
Definition: ssa_step.h:161
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:361
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:17
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:233
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
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:22
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
SSA_stept::io_id
irep_idt io_id
Definition: ssa_step.h:159
SSA_assignment_stept
Definition: ssa_step.h:206
goto_trace_stept::typet::DECL
@ DECL
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
goto_trace_stept::typet::ASSERT
@ ASSERT
SSA_stept::ssa_full_lhs
exprt ssa_full_lhs
Definition: ssa_step.h:144
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:149
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:655
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
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:480
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ 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:292
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:43
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:73
SSA_stept::hidden
bool hidden
Definition: ssa_step.h:137
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:402
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
@ 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:696
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ 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:503
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
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
@ 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:144
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:42
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:615
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:250
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:145
goto_trace_stept::typet::ATOMIC_BEGIN
@ 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:139
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:159
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:224
implies_exprt
Boolean implication.
Definition: std_expr.h:1983
goto_trace_stept::typet::SHARED_READ
@ 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:425
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
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
API to expression classes.
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:33
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
@ 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:285
not_exprt
Boolean negation.
Definition: std_expr.h:2127
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