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 
19 #include "solver_hardness.h"
20 #include "ssa_step.h"
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 std::string &msg,
286  const sourcet &source)
287 {
288  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
289  SSA_stept &SSA_step=SSA_steps.back();
290 
291  SSA_step.guard=guard;
292  SSA_step.cond_expr=cond;
293  SSA_step.comment=msg;
294 
295  merge_ireps(SSA_step);
296 }
297 
299  const exprt &guard,
300  const renamedt<exprt, L2> &cond,
301  const sourcet &source)
302 {
303  SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
304  SSA_stept &SSA_step=SSA_steps.back();
305 
306  SSA_step.guard=guard;
307  SSA_step.cond_expr = cond.get();
308 
309  merge_ireps(SSA_step);
310 }
311 
313  const exprt &cond,
314  const std::string &msg,
315  const sourcet &source)
316 {
317  // like assumption, but with global effect
318  SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
319  SSA_stept &SSA_step=SSA_steps.back();
320 
321  SSA_step.guard=true_exprt();
322  SSA_step.cond_expr=cond;
323  SSA_step.comment=msg;
324 
325  merge_ireps(SSA_step);
326 }
327 
329  decision_proceduret &decision_procedure)
330 {
331  with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
332  hardness.register_ssa_size(SSA_steps.size());
333  });
334 
335  convert_guards(decision_procedure);
336  convert_assignments(decision_procedure);
337  convert_decls(decision_procedure);
338  convert_assumptions(decision_procedure);
339  convert_goto_instructions(decision_procedure);
340  convert_function_calls(decision_procedure);
341  convert_io(decision_procedure);
342  convert_constraints(decision_procedure);
343 }
344 
346 {
347  const auto convert_SSA_start = std::chrono::steady_clock::now();
348 
349  convert_without_assertions(decision_procedure);
350  convert_assertions(decision_procedure);
351 
352  const auto convert_SSA_stop = std::chrono::steady_clock::now();
353  std::chrono::duration<double> convert_SSA_runtime =
354  std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
355  log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
356  << messaget::eom;
357 }
358 
360  decision_proceduret &decision_procedure)
361 {
362  std::size_t step_index = 0;
363  for(auto &step : SSA_steps)
364  {
365  if(step.is_assignment() && !step.ignore && !step.converted)
366  {
367  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
368  step.output(mstream);
369  mstream << messaget::eom;
370  });
371 
372  decision_procedure.set_to_true(step.cond_expr);
373  step.converted = true;
375  decision_procedure, hardness_register_ssa(step_index, step));
376  }
377  ++step_index;
378  }
379 }
380 
382  decision_proceduret &decision_procedure)
383 {
384  std::size_t step_index = 0;
385  for(auto &step : SSA_steps)
386  {
387  if(step.is_decl() && !step.ignore && !step.converted)
388  {
389  // The result is not used, these have no impact on
390  // the satisfiability of the formula.
391  decision_procedure.handle(step.cond_expr);
392  step.converted = true;
394  decision_procedure, hardness_register_ssa(step_index, step));
395  }
396  ++step_index;
397  }
398 }
399 
401  decision_proceduret &decision_procedure)
402 {
403  std::size_t step_index = 0;
404  for(auto &step : SSA_steps)
405  {
406  if(step.ignore)
407  step.guard_handle = false_exprt();
408  else
409  {
410  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
411  step.output(mstream);
412  mstream << messaget::eom;
413  });
414 
415  step.guard_handle = decision_procedure.handle(step.guard);
417  decision_procedure, hardness_register_ssa(step_index, step));
418  }
419  ++step_index;
420  }
421 }
422 
424  decision_proceduret &decision_procedure)
425 {
426  std::size_t step_index = 0;
427  for(auto &step : SSA_steps)
428  {
429  if(step.is_assume())
430  {
431  if(step.ignore)
432  step.cond_handle = true_exprt();
433  else
434  {
436  log.debug(), [&step](messaget::mstreamt &mstream) {
437  step.output(mstream);
438  mstream << messaget::eom;
439  });
440 
441  step.cond_handle = decision_procedure.handle(step.cond_expr);
442 
444  decision_procedure, hardness_register_ssa(step_index, step));
445  }
446  }
447  ++step_index;
448  }
449 }
450 
452  decision_proceduret &decision_procedure)
453 {
454  std::size_t step_index = 0;
455  for(auto &step : SSA_steps)
456  {
457  if(step.is_goto())
458  {
459  if(step.ignore)
460  step.cond_handle = true_exprt();
461  else
462  {
464  log.debug(), [&step](messaget::mstreamt &mstream) {
465  step.output(mstream);
466  mstream << messaget::eom;
467  });
468 
469  step.cond_handle = decision_procedure.handle(step.cond_expr);
471  decision_procedure, hardness_register_ssa(step_index, step));
472  }
473  }
474  ++step_index;
475  }
476 }
477 
479  decision_proceduret &decision_procedure)
480 {
481  std::size_t step_index = 0;
482  for(auto &step : SSA_steps)
483  {
484  if(step.is_constraint() && !step.ignore && !step.converted)
485  {
486  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
487  step.output(mstream);
488  mstream << messaget::eom;
489  });
490 
491  decision_procedure.set_to_true(step.cond_expr);
492  step.converted = true;
493 
495  decision_procedure, hardness_register_ssa(step_index, step));
496  }
497  ++step_index;
498  }
499 }
500 
502  decision_proceduret &decision_procedure,
503  bool optimized_for_single_assertions)
504 {
505  // we find out if there is only _one_ assertion,
506  // which allows for a simpler formula
507 
508  std::size_t number_of_assertions=count_assertions();
509 
510  if(number_of_assertions==0)
511  return;
512 
513  if(number_of_assertions == 1 && optimized_for_single_assertions)
514  {
515  std::size_t step_index = 0;
516  for(auto &step : SSA_steps)
517  {
518  // hide already converted assertions in the error trace
519  if(step.is_assert() && step.converted)
520  step.hidden = true;
521 
522  if(step.is_assert() && !step.ignore && !step.converted)
523  {
524  step.converted = true;
525  decision_procedure.set_to_false(step.cond_expr);
526  step.cond_handle = false_exprt();
527 
529  decision_procedure, hardness_register_ssa(step_index, step));
530  return; // prevent further assumptions!
531  }
532  else if(step.is_assume())
533  {
534  decision_procedure.set_to_true(step.cond_expr);
535 
537  decision_procedure, hardness_register_ssa(step_index, step));
538  }
539  ++step_index;
540  }
541 
542  UNREACHABLE; // unreachable
543  }
544 
545  // We do (NOT a1) OR (NOT a2) ...
546  // where the a's are the assertions
547  or_exprt::operandst disjuncts;
548  disjuncts.reserve(number_of_assertions);
549 
551 
552  std::vector<goto_programt::const_targett> involved_steps;
553 
554  for(auto &step : SSA_steps)
555  {
556  // hide already converted assertions in the error trace
557  if(step.is_assert() && step.converted)
558  step.hidden = true;
559 
560  if(step.is_assert() && !step.ignore && !step.converted)
561  {
562  step.converted = true;
563 
564  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
565  step.output(mstream);
566  mstream << messaget::eom;
567  });
568 
570  assumption,
571  step.cond_expr);
572 
573  // do the conversion
574  step.cond_handle = decision_procedure.handle(implication);
575 
577  decision_procedure,
578  [&involved_steps, &step](solver_hardnesst &hardness) {
579  involved_steps.push_back(step.source.pc);
580  });
581 
582  // store disjunct
583  disjuncts.push_back(not_exprt(step.cond_handle));
584  }
585  else if(step.is_assume())
586  {
587  // the assumptions have been converted before
588  // avoid deep nesting of ID_and expressions
589  if(assumption.id()==ID_and)
590  assumption.copy_to_operands(step.cond_handle);
591  else
592  assumption = and_exprt(assumption, step.cond_handle);
593 
595  decision_procedure,
596  [&involved_steps, &step](solver_hardnesst &hardness) {
597  involved_steps.push_back(step.source.pc);
598  });
599  }
600  }
601 
602  const auto assertion_disjunction = disjunction(disjuncts);
603  // the below is 'true' if there are no assertions
604  decision_procedure.set_to_true(assertion_disjunction);
605 
607  decision_procedure,
608  [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
609  hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
610  });
611 }
612 
614  decision_proceduret &decision_procedure)
615 {
616  std::size_t step_index = 0;
617  for(auto &step : SSA_steps)
618  {
619  if(!step.ignore)
620  {
621  and_exprt::operandst conjuncts;
622  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
623 
624  for(const auto &arg : step.ssa_function_arguments)
625  {
626  if(arg.is_constant() ||
627  arg.id()==ID_string_constant)
628  step.converted_function_arguments.push_back(arg);
629  else
630  {
631  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
632  symbol_exprt symbol(identifier, arg.type());
633 
634  equal_exprt eq(arg, symbol);
635  merge_irep(eq);
636 
637  decision_procedure.set_to(eq, true);
638  conjuncts.push_back(eq);
639  step.converted_function_arguments.push_back(symbol);
640  }
641  }
643  decision_procedure,
644  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
645  hardness.register_ssa(
646  step_index, conjunction(conjuncts), step.source.pc);
647  });
648  }
649  ++step_index;
650  }
651 }
652 
654 {
655  std::size_t step_index = 0;
656  for(auto &step : SSA_steps)
657  {
658  if(!step.ignore)
659  {
660  and_exprt::operandst conjuncts;
661  for(const auto &arg : step.io_args)
662  {
663  if(arg.is_constant() ||
664  arg.id()==ID_string_constant)
665  step.converted_io_args.push_back(arg);
666  else
667  {
668  const irep_idt identifier =
669  "symex::io::" + std::to_string(io_count++);
670  symbol_exprt symbol(identifier, arg.type());
671 
672  equal_exprt eq(arg, symbol);
673  merge_irep(eq);
674 
675  decision_procedure.set_to(eq, true);
676  conjuncts.push_back(eq);
677  step.converted_io_args.push_back(symbol);
678  }
679  }
681  decision_procedure,
682  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
683  hardness.register_ssa(
684  step_index, conjunction(conjuncts), step.source.pc);
685  });
686  }
687  ++step_index;
688  }
689 }
690 
695 {
696  merge_irep(SSA_step.guard);
697 
698  merge_irep(SSA_step.ssa_lhs);
699  merge_irep(SSA_step.ssa_full_lhs);
700  merge_irep(SSA_step.original_full_lhs);
701  merge_irep(SSA_step.ssa_rhs);
702 
703  merge_irep(SSA_step.cond_expr);
704 
705  for(auto &step : SSA_step.io_args)
706  merge_irep(step);
707 
708  for(auto &arg : SSA_step.ssa_function_arguments)
709  merge_irep(arg);
710 
711  // converted_io_args is merged in convert_io
712 }
713 
714 void symex_target_equationt::output(std::ostream &out) const
715 {
716  for(const auto &step : SSA_steps)
717  {
718  step.output(out);
719  out << "--------------\n";
720  }
721 }
Single SSA step in the equation.
Definition: ssa_step.h:47
irep_idt io_id
Definition: ssa_step.h:159
irep_idt called_function
Definition: ssa_step.h:165
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:168
exprt cond_expr
Definition: ssa_step.h:149
unsigned atomic_section_id
Definition: ssa_step.h:171
irep_idt format_string
Definition: ssa_step.h:159
bool formatted
Definition: ssa_step.h:160
exprt ssa_full_lhs
Definition: ssa_step.h:144
bool hidden
Definition: ssa_step.h:137
exprt guard
Definition: ssa_step.h:139
exprt ssa_rhs
Definition: ssa_step.h:145
std::string comment
Definition: ssa_step.h:151
symex_targett::sourcet source
Definition: ssa_step.h:49
exprt original_full_lhs
Definition: ssa_step.h:144
std::list< exprt > io_args
Definition: ssa_step.h:161
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
Boolean AND.
Definition: std_expr.h:1974
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...
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
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'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
The Boolean constant false.
Definition: std_expr.h:2865
Boolean implication.
Definition: std_expr.h:2037
bool is_not_nil() const
Definition: irep.h:380
mstreamt & status() const
Definition: message.h:414
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:429
static eomt eom
Definition: message.h:297
Boolean negation.
Definition: std_expr.h:2181
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:80
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 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.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
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:2856
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:503
#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:34
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
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.