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/format_expr.h>
18 #include <util/std_expr.h>
19 
22 
23 #include "goto_symex_state.h"
24 #include "ssa_step.h"
25 
27 hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
28 {
29  return [step_index, &step](solver_hardnesst &hardness) {
30  hardness.register_ssa(step_index, step.cond_expr, step.source.pc);
31  };
32 }
33 
35  const exprt &guard,
36  const ssa_exprt &ssa_object,
37  unsigned atomic_section_id,
38  const sourcet &source)
39 {
40  SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
41  SSA_stept &SSA_step=SSA_steps.back();
42 
43  SSA_step.guard=guard;
44  SSA_step.ssa_lhs=ssa_object;
45  SSA_step.atomic_section_id=atomic_section_id;
46 
47  merge_ireps(SSA_step);
48 }
49 
51  const exprt &guard,
52  const ssa_exprt &ssa_object,
53  unsigned atomic_section_id,
54  const sourcet &source)
55 {
57  SSA_stept &SSA_step=SSA_steps.back();
58 
59  SSA_step.guard=guard;
60  SSA_step.ssa_lhs=ssa_object;
61  SSA_step.atomic_section_id=atomic_section_id;
62 
63  merge_ireps(SSA_step);
64 }
65 
68  const exprt &guard,
69  const sourcet &source)
70 {
71  SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
72  SSA_stept &SSA_step=SSA_steps.back();
73  SSA_step.guard=guard;
74 
75  merge_ireps(SSA_step);
76 }
77 
79  const exprt &guard,
80  const sourcet &source)
81 {
83  SSA_stept &SSA_step=SSA_steps.back();
84  SSA_step.guard=guard;
85 
86  merge_ireps(SSA_step);
87 }
88 
91  const exprt &guard,
92  unsigned atomic_section_id,
93  const sourcet &source)
94 {
96  SSA_stept &SSA_step=SSA_steps.back();
97  SSA_step.guard=guard;
98  SSA_step.atomic_section_id=atomic_section_id;
99 
100  merge_ireps(SSA_step);
101 }
102 
105  const exprt &guard,
106  unsigned atomic_section_id,
107  const sourcet &source)
108 {
109  SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
110  SSA_stept &SSA_step=SSA_steps.back();
111  SSA_step.guard=guard;
112  SSA_step.atomic_section_id=atomic_section_id;
113 
114  merge_ireps(SSA_step);
115 }
116 
118  const exprt &guard,
119  const ssa_exprt &ssa_lhs,
120  const exprt &ssa_full_lhs,
121  const exprt &original_full_lhs,
122  const exprt &ssa_rhs,
123  const sourcet &source,
124  assignment_typet assignment_type)
125 {
126  PRECONDITION(ssa_lhs.is_not_nil());
127 
128  SSA_steps.emplace_back(SSA_assignment_stept{source,
129  guard,
130  ssa_lhs,
131  ssa_full_lhs,
132  original_full_lhs,
133  ssa_rhs,
134  assignment_type});
135 
136  merge_ireps(SSA_steps.back());
137 }
138 
140  const exprt &guard,
141  const ssa_exprt &ssa_lhs,
142  const exprt &initializer,
143  const sourcet &source,
144  assignment_typet assignment_type)
145 {
146  PRECONDITION(ssa_lhs.is_not_nil());
147 
148  SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
149  SSA_stept &SSA_step=SSA_steps.back();
150 
151  SSA_step.guard=guard;
152  SSA_step.ssa_lhs=ssa_lhs;
153  SSA_step.ssa_full_lhs = initializer;
154  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
155  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
156 
157  // the condition is trivially true, and only
158  // there so we see the symbols
159  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
160 
161  merge_ireps(SSA_step);
162 }
163 
166  const exprt &,
167  const ssa_exprt &,
168  const sourcet &)
169 {
170  // we currently don't record these
171 }
172 
174  const exprt &guard,
175  const sourcet &source)
176 {
177  SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
178  SSA_stept &SSA_step=SSA_steps.back();
179 
180  SSA_step.guard=guard;
181 
182  merge_ireps(SSA_step);
183 }
184 
186  const exprt &guard,
187  const irep_idt &function_id,
188  const std::vector<renamedt<exprt, L2>> &function_arguments,
189  const sourcet &source,
190  const bool hidden)
191 {
193  SSA_stept &SSA_step=SSA_steps.back();
194 
195  SSA_step.guard = guard;
196  SSA_step.called_function = function_id;
197  for(const auto &arg : function_arguments)
198  SSA_step.ssa_function_arguments.emplace_back(arg.get());
199  SSA_step.hidden = hidden;
200 
201  merge_ireps(SSA_step);
202 }
203 
205  const exprt &guard,
206  const irep_idt &function_id,
207  const sourcet &source,
208  const bool hidden)
209 {
211  SSA_stept &SSA_step=SSA_steps.back();
212 
213  SSA_step.guard = guard;
214  SSA_step.called_function = function_id;
215  SSA_step.hidden = hidden;
216 
217  merge_ireps(SSA_step);
218 }
219 
221  const exprt &guard,
222  const sourcet &source,
223  const irep_idt &output_id,
224  const std::list<renamedt<exprt, L2>> &args)
225 {
226  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
227  SSA_stept &SSA_step=SSA_steps.back();
228 
229  SSA_step.guard=guard;
230  for(const auto &arg : args)
231  SSA_step.io_args.emplace_back(arg.get());
232  SSA_step.io_id=output_id;
233 
234  merge_ireps(SSA_step);
235 }
236 
238  const exprt &guard,
239  const sourcet &source,
240  const irep_idt &output_id,
241  const irep_idt &fmt,
242  const std::list<exprt> &args)
243 {
244  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
245  SSA_stept &SSA_step=SSA_steps.back();
246 
247  SSA_step.guard=guard;
248  SSA_step.io_args=args;
249  SSA_step.io_id=output_id;
250  SSA_step.formatted=true;
251  SSA_step.format_string=fmt;
252 
253  merge_ireps(SSA_step);
254 }
255 
257  const exprt &guard,
258  const sourcet &source,
259  const irep_idt &input_id,
260  const std::list<exprt> &args)
261 {
262  SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
263  SSA_stept &SSA_step=SSA_steps.back();
264 
265  SSA_step.guard=guard;
266  SSA_step.io_args=args;
267  SSA_step.io_id=input_id;
268 
269  merge_ireps(SSA_step);
270 }
271 
273  const exprt &guard,
274  const exprt &cond,
275  const sourcet &source)
276 {
277  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
278  SSA_stept &SSA_step=SSA_steps.back();
279 
280  SSA_step.guard=guard;
281  SSA_step.cond_expr=cond;
282 
283  merge_ireps(SSA_step);
284 }
285 
287  const exprt &guard,
288  const exprt &cond,
289  const std::string &msg,
290  const sourcet &source)
291 {
292  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
293  SSA_stept &SSA_step=SSA_steps.back();
294 
295  SSA_step.guard=guard;
296  SSA_step.cond_expr=cond;
297  SSA_step.comment=msg;
298 
299  merge_ireps(SSA_step);
300 }
301 
303  const exprt &guard,
304  const renamedt<exprt, L2> &cond,
305  const sourcet &source)
306 {
307  SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
308  SSA_stept &SSA_step=SSA_steps.back();
309 
310  SSA_step.guard=guard;
311  SSA_step.cond_expr = cond.get();
312 
313  merge_ireps(SSA_step);
314 }
315 
317  const exprt &cond,
318  const std::string &msg,
319  const sourcet &source)
320 {
321  // like assumption, but with global effect
322  SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
323  SSA_stept &SSA_step=SSA_steps.back();
324 
325  SSA_step.guard=true_exprt();
326  SSA_step.cond_expr=cond;
327  SSA_step.comment=msg;
328 
329  merge_ireps(SSA_step);
330 }
331 
333  decision_proceduret &decision_procedure)
334 {
335  with_solver_hardness(decision_procedure, [&](solver_hardnesst &hardness) {
336  hardness.register_ssa_size(SSA_steps.size());
337  });
338 
339  convert_guards(decision_procedure);
340  convert_assignments(decision_procedure);
341  convert_decls(decision_procedure);
342  convert_assumptions(decision_procedure);
343  convert_goto_instructions(decision_procedure);
344  convert_function_calls(decision_procedure);
345  convert_io(decision_procedure);
346  convert_constraints(decision_procedure);
347 }
348 
350 {
351  const auto convert_SSA_start = std::chrono::steady_clock::now();
352 
353  convert_without_assertions(decision_procedure);
354  convert_assertions(decision_procedure);
355 
356  const auto convert_SSA_stop = std::chrono::steady_clock::now();
357  std::chrono::duration<double> convert_SSA_runtime =
358  std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
359  log.status() << "Runtime Convert SSA: " << convert_SSA_runtime.count() << "s"
360  << messaget::eom;
361 }
362 
364  decision_proceduret &decision_procedure)
365 {
366  std::size_t step_index = 0;
367  for(auto &step : SSA_steps)
368  {
369  if(step.is_assignment() && !step.ignore && !step.converted)
370  {
371  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
372  step.output(mstream);
373  mstream << messaget::eom;
374  });
375 
376  decision_procedure.set_to_true(step.cond_expr);
377  step.converted = true;
379  decision_procedure, hardness_register_ssa(step_index, step));
380  }
381  ++step_index;
382  }
383 }
384 
386  decision_proceduret &decision_procedure)
387 {
388  std::size_t step_index = 0;
389  for(auto &step : SSA_steps)
390  {
391  if(step.is_decl() && !step.ignore && !step.converted)
392  {
393  // The result is not used, these have no impact on
394  // the satisfiability of the formula.
395  decision_procedure.handle(step.cond_expr);
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, hardness_register_ssa(step_index, step));
422  }
423  ++step_index;
424  }
425 }
426 
428  decision_proceduret &decision_procedure)
429 {
430  std::size_t step_index = 0;
431  for(auto &step : SSA_steps)
432  {
433  if(step.is_assume())
434  {
435  if(step.ignore)
436  step.cond_handle = true_exprt();
437  else
438  {
440  log.debug(), [&step](messaget::mstreamt &mstream) {
441  step.output(mstream);
442  mstream << messaget::eom;
443  });
444 
445  step.cond_handle = decision_procedure.handle(step.cond_expr);
446 
448  decision_procedure, hardness_register_ssa(step_index, step));
449  }
450  }
451  ++step_index;
452  }
453 }
454 
456  decision_proceduret &decision_procedure)
457 {
458  std::size_t step_index = 0;
459  for(auto &step : SSA_steps)
460  {
461  if(step.is_goto())
462  {
463  if(step.ignore)
464  step.cond_handle = true_exprt();
465  else
466  {
468  log.debug(), [&step](messaget::mstreamt &mstream) {
469  step.output(mstream);
470  mstream << messaget::eom;
471  });
472 
473  step.cond_handle = decision_procedure.handle(step.cond_expr);
475  decision_procedure, hardness_register_ssa(step_index, step));
476  }
477  }
478  ++step_index;
479  }
480 }
481 
483  decision_proceduret &decision_procedure)
484 {
485  std::size_t step_index = 0;
486  for(auto &step : SSA_steps)
487  {
488  if(step.is_constraint() && !step.ignore && !step.converted)
489  {
490  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
491  step.output(mstream);
492  mstream << messaget::eom;
493  });
494 
495  decision_procedure.set_to_true(step.cond_expr);
496  step.converted = true;
497 
499  decision_procedure, hardness_register_ssa(step_index, step));
500  }
501  ++step_index;
502  }
503 }
504 
506  decision_proceduret &decision_procedure,
507  bool optimized_for_single_assertions)
508 {
509  // we find out if there is only _one_ assertion,
510  // which allows for a simpler formula
511 
512  std::size_t number_of_assertions=count_assertions();
513 
514  if(number_of_assertions==0)
515  return;
516 
517  if(number_of_assertions == 1 && optimized_for_single_assertions)
518  {
519  std::size_t step_index = 0;
520  for(auto &step : SSA_steps)
521  {
522  // hide already converted assertions in the error trace
523  if(step.is_assert() && step.converted)
524  step.hidden = true;
525 
526  if(step.is_assert() && !step.ignore && !step.converted)
527  {
528  step.converted = true;
529  decision_procedure.set_to_false(step.cond_expr);
530  step.cond_handle = false_exprt();
531 
533  decision_procedure, hardness_register_ssa(step_index, step));
534  return; // prevent further assumptions!
535  }
536  else if(step.is_assume())
537  {
538  decision_procedure.set_to_true(step.cond_expr);
539 
541  decision_procedure, hardness_register_ssa(step_index, step));
542  }
543  ++step_index;
544  }
545 
546  UNREACHABLE; // unreachable
547  }
548 
549  // We do (NOT a1) OR (NOT a2) ...
550  // where the a's are the assertions
551  or_exprt::operandst disjuncts;
552  disjuncts.reserve(number_of_assertions);
553 
555 
556  std::vector<goto_programt::const_targett> involved_steps;
557 
558  for(auto &step : SSA_steps)
559  {
560  // hide already converted assertions in the error trace
561  if(step.is_assert() && step.converted)
562  step.hidden = true;
563 
564  if(step.is_assert() && !step.ignore && !step.converted)
565  {
566  step.converted = true;
567 
568  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
569  step.output(mstream);
570  mstream << messaget::eom;
571  });
572 
573  implies_exprt implication(
574  assumption,
575  step.cond_expr);
576 
577  // do the conversion
578  step.cond_handle = decision_procedure.handle(implication);
579 
581  decision_procedure,
582  [&involved_steps, &step](solver_hardnesst &hardness) {
583  involved_steps.push_back(step.source.pc);
584  });
585 
586  // store disjunct
587  disjuncts.push_back(not_exprt(step.cond_handle));
588  }
589  else if(step.is_assume())
590  {
591  // the assumptions have been converted before
592  // avoid deep nesting of ID_and expressions
593  if(assumption.id()==ID_and)
594  assumption.copy_to_operands(step.cond_handle);
595  else
596  assumption = and_exprt(assumption, step.cond_handle);
597 
599  decision_procedure,
600  [&involved_steps, &step](solver_hardnesst &hardness) {
601  involved_steps.push_back(step.source.pc);
602  });
603  }
604  }
605 
606  const auto assertion_disjunction = disjunction(disjuncts);
607  // the below is 'true' if there are no assertions
608  decision_procedure.set_to_true(assertion_disjunction);
609 
611  decision_procedure,
612  [&assertion_disjunction, &involved_steps](solver_hardnesst &hardness) {
613  hardness.register_assertion_ssas(assertion_disjunction, involved_steps);
614  });
615 }
616 
618  decision_proceduret &decision_procedure)
619 {
620  std::size_t step_index = 0;
621  for(auto &step : SSA_steps)
622  {
623  if(!step.ignore)
624  {
625  and_exprt::operandst conjuncts;
626  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
627 
628  for(const auto &arg : step.ssa_function_arguments)
629  {
630  if(arg.is_constant() ||
631  arg.id()==ID_string_constant)
632  step.converted_function_arguments.push_back(arg);
633  else
634  {
635  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
636  symbol_exprt symbol(identifier, arg.type());
637 
638  equal_exprt eq(arg, symbol);
639  merge_irep(eq);
640 
641  decision_procedure.set_to(eq, true);
642  conjuncts.push_back(eq);
643  step.converted_function_arguments.push_back(symbol);
644  }
645  }
647  decision_procedure,
648  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
649  hardness.register_ssa(
650  step_index, conjunction(conjuncts), step.source.pc);
651  });
652  }
653  ++step_index;
654  }
655 }
656 
658 {
659  std::size_t step_index = 0;
660  for(auto &step : SSA_steps)
661  {
662  if(!step.ignore)
663  {
664  and_exprt::operandst conjuncts;
665  for(const auto &arg : step.io_args)
666  {
667  if(arg.is_constant() ||
668  arg.id()==ID_string_constant)
669  step.converted_io_args.push_back(arg);
670  else
671  {
672  const irep_idt identifier =
673  "symex::io::" + std::to_string(io_count++);
674  symbol_exprt symbol(identifier, arg.type());
675 
676  equal_exprt eq(arg, symbol);
677  merge_irep(eq);
678 
679  decision_procedure.set_to(eq, true);
680  conjuncts.push_back(eq);
681  step.converted_io_args.push_back(symbol);
682  }
683  }
685  decision_procedure,
686  [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
687  hardness.register_ssa(
688  step_index, conjunction(conjuncts), step.source.pc);
689  });
690  }
691  ++step_index;
692  }
693 }
694 
699 {
700  merge_irep(SSA_step.guard);
701 
702  merge_irep(SSA_step.ssa_lhs);
703  merge_irep(SSA_step.ssa_full_lhs);
704  merge_irep(SSA_step.original_full_lhs);
705  merge_irep(SSA_step.ssa_rhs);
706 
707  merge_irep(SSA_step.cond_expr);
708 
709  for(auto &step : SSA_step.io_args)
710  merge_irep(step);
711 
712  for(auto &arg : SSA_step.ssa_function_arguments)
713  merge_irep(arg);
714 
715  // converted_io_args is merged in convert_io
716 }
717 
718 void symex_target_equationt::output(std::ostream &out) const
719 {
720  for(const auto &step : SSA_steps)
721  {
722  step.output(out);
723  out << "--------------\n";
724  }
725 }
Single SSA step in the equation.
Definition: ssa_step.h:45
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:147
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:142
bool hidden
Definition: ssa_step.h:135
exprt guard
Definition: ssa_step.h:137
exprt ssa_rhs
Definition: ssa_step.h:143
std::string comment
Definition: ssa_step.h:149
symex_targett::sourcet source
Definition: ssa_step.h:47
exprt original_full_lhs
Definition: ssa_step.h:142
std::list< exprt > io_args
Definition: ssa_step.h:159
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
Boolean AND.
Definition: std_expr.h:1835
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:1140
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:2726
std::function< void(solver_hardnesst &)> handlert
Boolean implication.
Definition: std_expr.h:1898
bool is_not_nil() const
Definition: irep.h:391
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:138
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
Boolean negation.
Definition: std_expr.h:2042
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
const underlyingt & get() const
Definition: renamed.h:34
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:81
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:2717
Decision Procedure Interface.
Symbolic Execution.
Capability to collect the statistics of the complexity of individual solver queries.
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:41
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
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:38
goto_programt::const_targett pc
Definition: symex_target.h:43
static hardness_collectort::handlert hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
Generate Equation using Symbolic Execution.