CBMC
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/std_expr.h>
16 
17 #include "solver_hardness.h"
18 #include "ssa_step.h"
19 
20 #include <chrono> // IWYU pragma: keep
21 
22 static std::function<void(solver_hardnesst &)>
23 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
24 {
25  return [step_index, &step](solver_hardnesst &hardness) {
26  hardness.register_ssa(step_index, step.cond_expr, step.source.pc);
27  };
28 }
29 
31  const exprt &guard,
32  const ssa_exprt &ssa_object,
33  unsigned atomic_section_id,
34  const sourcet &source)
35 {
36  SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
37  SSA_stept &SSA_step=SSA_steps.back();
38 
39  SSA_step.guard=guard;
40  SSA_step.ssa_lhs=ssa_object;
41  SSA_step.atomic_section_id=atomic_section_id;
42 
43  merge_ireps(SSA_step);
44 }
45 
47  const exprt &guard,
48  const ssa_exprt &ssa_object,
49  unsigned atomic_section_id,
50  const sourcet &source)
51 {
53  SSA_stept &SSA_step=SSA_steps.back();
54 
55  SSA_step.guard=guard;
56  SSA_step.ssa_lhs=ssa_object;
57  SSA_step.atomic_section_id=atomic_section_id;
58 
59  merge_ireps(SSA_step);
60 }
61 
64  const exprt &guard,
65  const sourcet &source)
66 {
67  SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
68  SSA_stept &SSA_step=SSA_steps.back();
69  SSA_step.guard=guard;
70 
71  merge_ireps(SSA_step);
72 }
73 
75  const exprt &guard,
76  const sourcet &source)
77 {
79  SSA_stept &SSA_step=SSA_steps.back();
80  SSA_step.guard=guard;
81 
82  merge_ireps(SSA_step);
83 }
84 
87  const exprt &guard,
88  unsigned atomic_section_id,
89  const sourcet &source)
90 {
92  SSA_stept &SSA_step=SSA_steps.back();
93  SSA_step.guard=guard;
94  SSA_step.atomic_section_id=atomic_section_id;
95 
96  merge_ireps(SSA_step);
97 }
98 
101  const exprt &guard,
102  unsigned atomic_section_id,
103  const sourcet &source)
104 {
105  SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
106  SSA_stept &SSA_step=SSA_steps.back();
107  SSA_step.guard=guard;
108  SSA_step.atomic_section_id=atomic_section_id;
109 
110  merge_ireps(SSA_step);
111 }
112 
114  const exprt &guard,
115  const ssa_exprt &ssa_lhs,
116  const exprt &ssa_full_lhs,
117  const exprt &original_full_lhs,
118  const exprt &ssa_rhs,
119  const sourcet &source,
120  assignment_typet assignment_type)
121 {
122  PRECONDITION(ssa_lhs.is_not_nil());
123 
124  SSA_steps.emplace_back(SSA_assignment_stept{source,
125  guard,
126  ssa_lhs,
127  ssa_full_lhs,
128  original_full_lhs,
129  ssa_rhs,
130  assignment_type});
131 
132  merge_ireps(SSA_steps.back());
133 }
134 
136  const exprt &guard,
137  const ssa_exprt &ssa_lhs,
138  const exprt &initializer,
139  const sourcet &source,
140  assignment_typet assignment_type)
141 {
142  PRECONDITION(ssa_lhs.is_not_nil());
143 
144  SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
145  SSA_stept &SSA_step=SSA_steps.back();
146 
147  SSA_step.guard=guard;
148  SSA_step.ssa_lhs=ssa_lhs;
149  SSA_step.ssa_full_lhs = initializer;
150  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
151  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
152 
153  // the condition is trivially true, and only
154  // there so we see the symbols
155  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
156 
157  merge_ireps(SSA_step);
158 }
159 
162  const exprt &,
163  const ssa_exprt &,
164  const sourcet &)
165 {
166  // we currently don't record these
167 }
168 
170  const exprt &guard,
171  const sourcet &source)
172 {
173  SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
174  SSA_stept &SSA_step=SSA_steps.back();
175 
176  SSA_step.guard=guard;
177 
178  merge_ireps(SSA_step);
179 }
180 
182  const exprt &guard,
183  const irep_idt &function_id,
184  const std::vector<renamedt<exprt, L2>> &function_arguments,
185  const sourcet &source,
186  const bool hidden)
187 {
189  SSA_stept &SSA_step=SSA_steps.back();
190 
191  SSA_step.guard = guard;
192  SSA_step.called_function = function_id;
193  for(const auto &arg : function_arguments)
194  SSA_step.ssa_function_arguments.emplace_back(arg.get());
195  SSA_step.hidden = hidden;
196 
197  merge_ireps(SSA_step);
198 }
199 
201  const exprt &guard,
202  const irep_idt &function_id,
203  const sourcet &source,
204  const bool hidden)
205 {
207  SSA_stept &SSA_step=SSA_steps.back();
208 
209  SSA_step.guard = guard;
210  SSA_step.called_function = function_id;
211  SSA_step.hidden = hidden;
212 
213  merge_ireps(SSA_step);
214 }
215 
217  const exprt &guard,
218  const sourcet &source,
219  const irep_idt &output_id,
220  const std::list<renamedt<exprt, L2>> &args)
221 {
222  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
223  SSA_stept &SSA_step=SSA_steps.back();
224 
225  SSA_step.guard=guard;
226  for(const auto &arg : args)
227  SSA_step.io_args.emplace_back(arg.get());
228  SSA_step.io_id=output_id;
229 
230  merge_ireps(SSA_step);
231 }
232 
234  const exprt &guard,
235  const sourcet &source,
236  const irep_idt &output_id,
237  const irep_idt &fmt,
238  const std::list<exprt> &args)
239 {
240  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
241  SSA_stept &SSA_step=SSA_steps.back();
242 
243  SSA_step.guard=guard;
244  SSA_step.io_args=args;
245  SSA_step.io_id=output_id;
246  SSA_step.formatted=true;
247  SSA_step.format_string=fmt;
248 
249  merge_ireps(SSA_step);
250 }
251 
253  const exprt &guard,
254  const sourcet &source,
255  const irep_idt &input_id,
256  const std::list<exprt> &args)
257 {
258  SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
259  SSA_stept &SSA_step=SSA_steps.back();
260 
261  SSA_step.guard=guard;
262  SSA_step.io_args=args;
263  SSA_step.io_id=input_id;
264 
265  merge_ireps(SSA_step);
266 }
267 
269  const exprt &guard,
270  const exprt &cond,
271  const sourcet &source)
272 {
273  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
274  SSA_stept &SSA_step=SSA_steps.back();
275 
276  SSA_step.guard=guard;
277  SSA_step.cond_expr=cond;
278 
279  merge_ireps(SSA_step);
280 }
281 
283  const exprt &guard,
284  const exprt &cond,
285  const irep_idt &property_id,
286  const std::string &msg,
287  const sourcet &source)
288 {
289  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
290  SSA_stept &SSA_step=SSA_steps.back();
291 
292  SSA_step.guard=guard;
293  SSA_step.cond_expr=cond;
294  SSA_step.comment=msg;
295  SSA_step.property_id = property_id;
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.statistics() << "Runtime Convert SSA: " << convert_SSA_runtime.count()
358  << "s" << 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  decision_procedure.handle(
395  equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs});
396  step.converted = true;
398  decision_procedure, hardness_register_ssa(step_index, step));
399  }
400  ++step_index;
401  }
402 }
403 
405  decision_proceduret &decision_procedure)
406 {
407  std::size_t step_index = 0;
408  for(auto &step : SSA_steps)
409  {
410  if(step.ignore)
411  step.guard_handle = false_exprt();
412  else
413  {
414  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
415  step.output(mstream);
416  mstream << messaget::eom;
417  });
418 
419  step.guard_handle = decision_procedure.handle(step.guard);
421  decision_procedure, [step_index, &step](solver_hardnesst &hardness) {
422  hardness.register_ssa(step_index, step.guard, step.source.pc);
423  });
424  }
425  ++step_index;
426  }
427 }
428 
430  decision_proceduret &decision_procedure)
431 {
432  std::size_t step_index = 0;
433  for(auto &step : SSA_steps)
434  {
435  if(step.is_assume())
436  {
437  if(step.ignore)
438  step.cond_handle = true_exprt();
439  else
440  {
442  log.debug(), [&step](messaget::mstreamt &mstream) {
443  step.output(mstream);
444  mstream << messaget::eom;
445  });
446 
447  step.cond_handle = decision_procedure.handle(step.cond_expr);
448 
450  decision_procedure, hardness_register_ssa(step_index, step));
451  }
452  }
453  ++step_index;
454  }
455 }
456 
458  decision_proceduret &decision_procedure)
459 {
460  std::size_t step_index = 0;
461  for(auto &step : SSA_steps)
462  {
463  if(step.is_goto())
464  {
465  if(step.ignore)
466  step.cond_handle = true_exprt();
467  else
468  {
470  log.debug(), [&step](messaget::mstreamt &mstream) {
471  step.output(mstream);
472  mstream << messaget::eom;
473  });
474 
475  step.cond_handle = decision_procedure.handle(step.cond_expr);
477  decision_procedure, hardness_register_ssa(step_index, step));
478  }
479  }
480  ++step_index;
481  }
482 }
483 
485  decision_proceduret &decision_procedure)
486 {
487  std::size_t step_index = 0;
488  for(auto &step : SSA_steps)
489  {
490  if(step.is_constraint() && !step.ignore && !step.converted)
491  {
492  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
493  step.output(mstream);
494  mstream << messaget::eom;
495  });
496 
497  decision_procedure.set_to_true(step.cond_expr);
498  step.converted = true;
499 
501  decision_procedure, hardness_register_ssa(step_index, step));
502  }
503  ++step_index;
504  }
505 }
506 
508  decision_proceduret &decision_procedure,
509  bool optimized_for_single_assertions)
510 {
511  // we find out if there is only _one_ assertion,
512  // which allows for a simpler formula
513 
514  std::size_t number_of_assertions=count_assertions();
515 
516  if(number_of_assertions==0)
517  return;
518 
519  if(number_of_assertions == 1 && optimized_for_single_assertions)
520  {
521  std::size_t step_index = 0;
522  for(auto &step : SSA_steps)
523  {
524  // hide already converted assertions in the error trace
525  if(step.is_assert() && step.converted)
526  step.hidden = true;
527 
528  if(step.is_assert() && !step.ignore && !step.converted)
529  {
530  step.converted = true;
531  decision_procedure.set_to_false(step.cond_expr);
532  step.cond_handle = false_exprt();
533 
535  decision_procedure, hardness_register_ssa(step_index, step));
536  return; // prevent further assumptions!
537  }
538  else if(step.is_assume())
539  {
540  decision_procedure.set_to_true(step.cond_expr);
541 
543  decision_procedure, hardness_register_ssa(step_index, step));
544  }
545  ++step_index;
546  }
547 
548  UNREACHABLE; // unreachable
549  }
550 
551  // We do (NOT a1) OR (NOT a2) ...
552  // where the a's are the assertions
553  or_exprt::operandst disjuncts;
554  disjuncts.reserve(number_of_assertions);
555 
557 
558  std::vector<goto_programt::const_targett> involved_steps;
559 
560  for(auto &step : SSA_steps)
561  {
562  // hide already converted assertions in the error trace
563  if(step.is_assert() && step.converted)
564  step.hidden = true;
565 
566  if(step.is_assert() && !step.ignore && !step.converted)
567  {
568  step.converted = true;
569 
570  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
571  step.output(mstream);
572  mstream << messaget::eom;
573  });
574 
576  assumption,
577  step.cond_expr);
578 
579  // do the conversion
580  step.cond_handle = decision_procedure.handle(implication);
581 
583  decision_procedure,
584  [&involved_steps, &step](solver_hardnesst &hardness) {
585  involved_steps.push_back(step.source.pc);
586  });
587 
588  // store disjunct
589  disjuncts.push_back(not_exprt(step.cond_handle));
590  }
591  else if(step.is_assume())
592  {
593  // the assumptions have been converted before
594  // avoid deep nesting of ID_and expressions
595  if(assumption.id()==ID_and)
596  assumption.copy_to_operands(step.cond_handle);
597  else
598  assumption = and_exprt(assumption, step.cond_handle);
599 
601  decision_procedure,
602  [&involved_steps, &step](solver_hardnesst &hardness) {
603  involved_steps.push_back(step.source.pc);
604  });
605  }
606  }
607 
608  const auto assertion_disjunction = disjunction(disjuncts);
609  // the below is 'true' if there are no assertions
610  decision_procedure.set_to_true(assertion_disjunction);
611 
613  decision_procedure,
614  [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
615  hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
616  });
617 }
618 
620  decision_proceduret &decision_procedure)
621 {
622  std::size_t step_index = 0;
623  for(auto &step : SSA_steps)
624  {
625  if(!step.ignore)
626  {
627  and_exprt::operandst conjuncts;
628  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
629 
630  for(const auto &arg : step.ssa_function_arguments)
631  {
632  if(arg.is_constant() ||
633  arg.id()==ID_string_constant)
634  step.converted_function_arguments.push_back(arg);
635  else
636  {
637  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
638  symbol_exprt symbol(identifier, arg.type());
639 
640  equal_exprt eq(arg, symbol);
641  merge_irep(eq);
642 
643  decision_procedure.set_to(eq, true);
644  conjuncts.push_back(eq);
645  step.converted_function_arguments.push_back(symbol);
646  }
647  }
649  decision_procedure,
650  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
651  hardness.register_ssa(
652  step_index, conjunction(conjuncts), step.source.pc);
653  });
654  }
655  ++step_index;
656  }
657 }
658 
660 {
661  std::size_t step_index = 0;
662  for(auto &step : SSA_steps)
663  {
664  if(!step.ignore)
665  {
666  and_exprt::operandst conjuncts;
667  for(const auto &arg : step.io_args)
668  {
669  if(arg.is_constant() ||
670  arg.id()==ID_string_constant)
671  step.converted_io_args.push_back(arg);
672  else
673  {
674  const irep_idt identifier =
675  "symex::io::" + std::to_string(io_count++);
676  symbol_exprt symbol(identifier, arg.type());
677 
678  equal_exprt eq(arg, symbol);
679  merge_irep(eq);
680 
681  decision_procedure.set_to(eq, true);
682  conjuncts.push_back(eq);
683  step.converted_io_args.push_back(symbol);
684  }
685  }
687  decision_procedure,
688  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
689  hardness.register_ssa(
690  step_index, conjunction(conjuncts), step.source.pc);
691  });
692  }
693  ++step_index;
694  }
695 }
696 
701 {
702  merge_irep(SSA_step.guard);
703 
704  merge_irep(SSA_step.ssa_lhs);
705  merge_irep(SSA_step.ssa_full_lhs);
706  merge_irep(SSA_step.original_full_lhs);
707  merge_irep(SSA_step.ssa_rhs);
708 
709  merge_irep(SSA_step.cond_expr);
710 
711  for(auto &step : SSA_step.io_args)
712  merge_irep(step);
713 
714  for(auto &arg : SSA_step.ssa_function_arguments)
715  merge_irep(arg);
716 
717  // converted_io_args is merged in convert_io
718 }
719 
720 void symex_target_equationt::output(std::ostream &out) const
721 {
722  for(const auto &step : SSA_steps)
723  {
724  step.output(out);
725  out << "--------------\n";
726  }
727 }
static exprt guard(const exprt::operandst &guards, exprt cond)
Single SSA step in the equation.
Definition: ssa_step.h:47
irep_idt io_id
Definition: ssa_step.h:157
irep_idt called_function
Definition: ssa_step.h:163
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:166
exprt cond_expr
Definition: ssa_step.h:145
unsigned atomic_section_id
Definition: ssa_step.h:169
irep_idt format_string
Definition: ssa_step.h:157
bool formatted
Definition: ssa_step.h:158
exprt ssa_full_lhs
Definition: ssa_step.h:140
bool hidden
Definition: ssa_step.h:133
exprt guard
Definition: ssa_step.h:135
exprt ssa_rhs
Definition: ssa_step.h:141
std::string comment
Definition: ssa_step.h:147
symex_targett::sourcet source
Definition: ssa_step.h:49
exprt original_full_lhs
Definition: ssa_step.h:140
irep_idt property_id
Definition: ssa_step.h:149
std::list< exprt > io_args
Definition: ssa_step.h:159
ssa_exprt ssa_lhs
Definition: ssa_step.h:139
Boolean AND.
Definition: std_expr.h:2120
An interface for a decision procedure for satisfiability problems.
void set_to_false(const exprt &)
For a Boolean expression expr, add the constraint 'not expr'.
virtual exprt handle(const exprt &)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
The Boolean constant false.
Definition: std_expr.h:3072
Boolean implication.
Definition: std_expr.h:2183
bool is_not_nil() const
Definition: irep.h:372
mstreamt & statistics() const
Definition: message.h:411
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
mstreamt & debug() const
Definition: message.h:421
static eomt eom
Definition: message.h:289
Boolean negation.
Definition: std_expr.h:2327
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
const underlyingt & get() const
Definition: renamed.h:40
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
Expression to hold a symbol (variable)
Definition: std_expr.h:131
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
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...
virtual void assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
std::size_t count_assertions() const
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
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...
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.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
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.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
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.
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.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
The Boolean constant true.
Definition: std_expr.h:3063
static exprt implication(exprt lhs, exprt rhs)
static void with_solver_hardness(decision_proceduret &maybe_hardness_collector, std::function< void(solver_hardnesst &hardness)> handler)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:83
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:71
API to expression classes.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
A structure that facilitates collecting the complexity statistics from a decision procedure.
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...
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...
void register_ssa_size(std::size_t size)
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
goto_programt::const_targett pc
Definition: symex_target.h:42
static std::function< void(solver_hardnesst &)> hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
Generate Equation using Symbolic Execution.