cprover
symex_target_equation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
12 
13 #include "symex_target_equation.h"
14 
15 #include <util/format_expr.h>
16 #include <util/std_expr.h>
17 
19 
20 #include "goto_symex_state.h"
21 #include "ssa_step.h"
22 
24  const exprt &guard,
25  const ssa_exprt &ssa_object,
26  unsigned atomic_section_id,
27  const sourcet &source)
28 {
29  SSA_steps.emplace_back(source, goto_trace_stept::typet::SHARED_READ);
30  SSA_stept &SSA_step=SSA_steps.back();
31 
32  SSA_step.guard=guard;
33  SSA_step.ssa_lhs=ssa_object;
34  SSA_step.atomic_section_id=atomic_section_id;
35 
36  merge_ireps(SSA_step);
37 }
38 
40  const exprt &guard,
41  const ssa_exprt &ssa_object,
42  unsigned atomic_section_id,
43  const sourcet &source)
44 {
46  SSA_stept &SSA_step=SSA_steps.back();
47 
48  SSA_step.guard=guard;
49  SSA_step.ssa_lhs=ssa_object;
50  SSA_step.atomic_section_id=atomic_section_id;
51 
52  merge_ireps(SSA_step);
53 }
54 
57  const exprt &guard,
58  const sourcet &source)
59 {
60  SSA_steps.emplace_back(source, goto_trace_stept::typet::SPAWN);
61  SSA_stept &SSA_step=SSA_steps.back();
62  SSA_step.guard=guard;
63 
64  merge_ireps(SSA_step);
65 }
66 
68  const exprt &guard,
69  const sourcet &source)
70 {
72  SSA_stept &SSA_step=SSA_steps.back();
73  SSA_step.guard=guard;
74 
75  merge_ireps(SSA_step);
76 }
77 
80  const exprt &guard,
81  unsigned atomic_section_id,
82  const sourcet &source)
83 {
85  SSA_stept &SSA_step=SSA_steps.back();
86  SSA_step.guard=guard;
87  SSA_step.atomic_section_id=atomic_section_id;
88 
89  merge_ireps(SSA_step);
90 }
91 
94  const exprt &guard,
95  unsigned atomic_section_id,
96  const sourcet &source)
97 {
98  SSA_steps.emplace_back(source, goto_trace_stept::typet::ATOMIC_END);
99  SSA_stept &SSA_step=SSA_steps.back();
100  SSA_step.guard=guard;
101  SSA_step.atomic_section_id=atomic_section_id;
102 
103  merge_ireps(SSA_step);
104 }
105 
107  const exprt &guard,
108  const ssa_exprt &ssa_lhs,
109  const exprt &ssa_full_lhs,
110  const exprt &original_full_lhs,
111  const exprt &ssa_rhs,
112  const sourcet &source,
113  assignment_typet assignment_type)
114 {
115  PRECONDITION(ssa_lhs.is_not_nil());
116 
117  SSA_steps.emplace_back(SSA_assignment_stept{source,
118  guard,
119  ssa_lhs,
120  ssa_full_lhs,
121  original_full_lhs,
122  ssa_rhs,
123  assignment_type});
124 
125  merge_ireps(SSA_steps.back());
126 }
127 
129  const exprt &guard,
130  const ssa_exprt &ssa_lhs,
131  const exprt &initializer,
132  const sourcet &source,
133  assignment_typet assignment_type)
134 {
135  PRECONDITION(ssa_lhs.is_not_nil());
136 
137  SSA_steps.emplace_back(source, goto_trace_stept::typet::DECL);
138  SSA_stept &SSA_step=SSA_steps.back();
139 
140  SSA_step.guard=guard;
141  SSA_step.ssa_lhs=ssa_lhs;
142  SSA_step.ssa_full_lhs = initializer;
143  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
144  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
145 
146  // the condition is trivially true, and only
147  // there so we see the symbols
148  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
149 
150  merge_ireps(SSA_step);
151 }
152 
155  const exprt &,
156  const ssa_exprt &,
157  const sourcet &)
158 {
159  // we currently don't record these
160 }
161 
163  const exprt &guard,
164  const sourcet &source)
165 {
166  SSA_steps.emplace_back(source, goto_trace_stept::typet::LOCATION);
167  SSA_stept &SSA_step=SSA_steps.back();
168 
169  SSA_step.guard=guard;
170 
171  merge_ireps(SSA_step);
172 }
173 
175  const exprt &guard,
176  const irep_idt &function_id,
177  const std::vector<renamedt<exprt, L2>> &function_arguments,
178  const sourcet &source,
179  const bool hidden)
180 {
182  SSA_stept &SSA_step=SSA_steps.back();
183 
184  SSA_step.guard = guard;
185  SSA_step.called_function = function_id;
186  for(const auto &arg : function_arguments)
187  SSA_step.ssa_function_arguments.emplace_back(arg.get());
188  SSA_step.hidden = hidden;
189 
190  merge_ireps(SSA_step);
191 }
192 
194  const exprt &guard,
195  const irep_idt &function_id,
196  const sourcet &source,
197  const bool hidden)
198 {
200  SSA_stept &SSA_step=SSA_steps.back();
201 
202  SSA_step.guard = guard;
203  SSA_step.called_function = function_id;
204  SSA_step.hidden = hidden;
205 
206  merge_ireps(SSA_step);
207 }
208 
210  const exprt &guard,
211  const sourcet &source,
212  const irep_idt &output_id,
213  const std::list<renamedt<exprt, L2>> &args)
214 {
215  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
216  SSA_stept &SSA_step=SSA_steps.back();
217 
218  SSA_step.guard=guard;
219  for(const auto &arg : args)
220  SSA_step.io_args.emplace_back(arg.get());
221  SSA_step.io_id=output_id;
222 
223  merge_ireps(SSA_step);
224 }
225 
227  const exprt &guard,
228  const sourcet &source,
229  const irep_idt &output_id,
230  const irep_idt &fmt,
231  const std::list<exprt> &args)
232 {
233  SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
234  SSA_stept &SSA_step=SSA_steps.back();
235 
236  SSA_step.guard=guard;
237  SSA_step.io_args=args;
238  SSA_step.io_id=output_id;
239  SSA_step.formatted=true;
240  SSA_step.format_string=fmt;
241 
242  merge_ireps(SSA_step);
243 }
244 
246  const exprt &guard,
247  const sourcet &source,
248  const irep_idt &input_id,
249  const std::list<exprt> &args)
250 {
251  SSA_steps.emplace_back(source, goto_trace_stept::typet::INPUT);
252  SSA_stept &SSA_step=SSA_steps.back();
253 
254  SSA_step.guard=guard;
255  SSA_step.io_args=args;
256  SSA_step.io_id=input_id;
257 
258  merge_ireps(SSA_step);
259 }
260 
262  const exprt &guard,
263  const exprt &cond,
264  const sourcet &source)
265 {
266  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSUME);
267  SSA_stept &SSA_step=SSA_steps.back();
268 
269  SSA_step.guard=guard;
270  SSA_step.cond_expr=cond;
271 
272  merge_ireps(SSA_step);
273 }
274 
276  const exprt &guard,
277  const exprt &cond,
278  const std::string &msg,
279  const sourcet &source)
280 {
281  SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSERT);
282  SSA_stept &SSA_step=SSA_steps.back();
283 
284  SSA_step.guard=guard;
285  SSA_step.cond_expr=cond;
286  SSA_step.comment=msg;
287 
288  merge_ireps(SSA_step);
289 }
290 
292  const exprt &guard,
293  const renamedt<exprt, L2> &cond,
294  const sourcet &source)
295 {
296  SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
297  SSA_stept &SSA_step=SSA_steps.back();
298 
299  SSA_step.guard=guard;
300  SSA_step.cond_expr = cond.get();
301 
302  merge_ireps(SSA_step);
303 }
304 
306  const exprt &cond,
307  const std::string &msg,
308  const sourcet &source)
309 {
310  // like assumption, but with global effect
311  SSA_steps.emplace_back(source, goto_trace_stept::typet::CONSTRAINT);
312  SSA_stept &SSA_step=SSA_steps.back();
313 
314  SSA_step.guard=true_exprt();
315  SSA_step.cond_expr=cond;
316  SSA_step.comment=msg;
317 
318  merge_ireps(SSA_step);
319 }
320 
322  decision_proceduret &decision_procedure)
323 {
324  convert_guards(decision_procedure);
325  convert_assignments(decision_procedure);
326  convert_decls(decision_procedure);
327  convert_assumptions(decision_procedure);
328  convert_goto_instructions(decision_procedure);
329  convert_function_calls(decision_procedure);
330  convert_io(decision_procedure);
331  convert_constraints(decision_procedure);
332 }
333 
335 {
336  convert_without_assertions(decision_procedure);
337  convert_assertions(decision_procedure);
338 }
339 
341  decision_proceduret &decision_procedure)
342 {
343  for(auto &step : SSA_steps)
344  {
345  if(step.is_assignment() && !step.ignore && !step.converted)
346  {
347  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
348  step.output(mstream);
349  mstream << messaget::eom;
350  });
351 
352  decision_procedure.set_to_true(step.cond_expr);
353  step.converted = true;
354  }
355  }
356 }
357 
359  decision_proceduret &decision_procedure)
360 {
361  for(auto &step : SSA_steps)
362  {
363  if(step.is_decl() && !step.ignore && !step.converted)
364  {
365  // The result is not used, these have no impact on
366  // the satisfiability of the formula.
367  decision_procedure.handle(step.cond_expr);
368  step.converted = true;
369  }
370  }
371 }
372 
374  decision_proceduret &decision_procedure)
375 {
376  for(auto &step : SSA_steps)
377  {
378  if(step.ignore)
379  step.guard_handle = false_exprt();
380  else
381  {
382  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
383  step.output(mstream);
384  mstream << messaget::eom;
385  });
386 
387  step.guard_handle = decision_procedure.handle(step.guard);
388  }
389  }
390 }
391 
393  decision_proceduret &decision_procedure)
394 {
395  for(auto &step : SSA_steps)
396  {
397  if(step.is_assume())
398  {
399  if(step.ignore)
400  step.cond_handle = true_exprt();
401  else
402  {
404  log.debug(), [&step](messaget::mstreamt &mstream) {
405  step.output(mstream);
406  mstream << messaget::eom;
407  });
408 
409  step.cond_handle = decision_procedure.handle(step.cond_expr);
410  }
411  }
412  }
413 }
414 
416  decision_proceduret &decision_procedure)
417 {
418  for(auto &step : SSA_steps)
419  {
420  if(step.is_goto())
421  {
422  if(step.ignore)
423  step.cond_handle = true_exprt();
424  else
425  {
427  log.debug(), [&step](messaget::mstreamt &mstream) {
428  step.output(mstream);
429  mstream << messaget::eom;
430  });
431 
432  step.cond_handle = decision_procedure.handle(step.cond_expr);
433  }
434  }
435  }
436 }
437 
439  decision_proceduret &decision_procedure)
440 {
441  for(auto &step : SSA_steps)
442  {
443  if(step.is_constraint() && !step.ignore && !step.converted)
444  {
445  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
446  step.output(mstream);
447  mstream << messaget::eom;
448  });
449 
450  decision_procedure.set_to_true(step.cond_expr);
451  step.converted = true;
452  }
453  }
454 }
455 
457  decision_proceduret &decision_procedure,
458  bool optimized_for_single_assertions)
459 {
460  // we find out if there is only _one_ assertion,
461  // which allows for a simpler formula
462 
463  std::size_t number_of_assertions=count_assertions();
464 
465  if(number_of_assertions==0)
466  return;
467 
468  if(number_of_assertions == 1 && optimized_for_single_assertions)
469  {
470  for(auto &step : SSA_steps)
471  {
472  // hide already converted assertions in the error trace
473  if(step.is_assert() && step.converted)
474  step.hidden = true;
475 
476  if(step.is_assert() && !step.ignore && !step.converted)
477  {
478  step.converted = true;
479  decision_procedure.set_to_false(step.cond_expr);
480  step.cond_handle = false_exprt();
481  return; // prevent further assumptions!
482  }
483  else if(step.is_assume())
484  decision_procedure.set_to_true(step.cond_expr);
485  }
486 
487  UNREACHABLE; // unreachable
488  }
489 
490  // We do (NOT a1) OR (NOT a2) ...
491  // where the a's are the assertions
492  or_exprt::operandst disjuncts;
493  disjuncts.reserve(number_of_assertions);
494 
496 
497  for(auto &step : SSA_steps)
498  {
499  // hide already converted assertions in the error trace
500  if(step.is_assert() && step.converted)
501  step.hidden = true;
502 
503  if(step.is_assert() && !step.ignore && !step.converted)
504  {
505  step.converted = true;
506 
507  log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
508  step.output(mstream);
509  mstream << messaget::eom;
510  });
511 
512  implies_exprt implication(
513  assumption,
514  step.cond_expr);
515 
516  // do the conversion
517  step.cond_handle = decision_procedure.handle(implication);
518 
519  // store disjunct
520  disjuncts.push_back(not_exprt(step.cond_handle));
521  }
522  else if(step.is_assume())
523  {
524  // the assumptions have been converted before
525  // avoid deep nesting of ID_and expressions
526  if(assumption.id()==ID_and)
527  assumption.copy_to_operands(step.cond_handle);
528  else
529  assumption = and_exprt(assumption, step.cond_handle);
530  }
531  }
532 
533  // the below is 'true' if there are no assertions
534  decision_procedure.set_to_true(disjunction(disjuncts));
535 }
536 
538  decision_proceduret &dec_proc)
539 {
540  for(auto &step : SSA_steps)
541  if(!step.ignore)
542  {
543  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
544 
545  for(const auto &arg : step.ssa_function_arguments)
546  {
547  if(arg.is_constant() ||
548  arg.id()==ID_string_constant)
549  step.converted_function_arguments.push_back(arg);
550  else
551  {
552  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
553  symbol_exprt symbol(identifier, arg.type());
554 
555  equal_exprt eq(arg, symbol);
556  merge_irep(eq);
557 
558  dec_proc.set_to(eq, true);
559  step.converted_function_arguments.push_back(symbol);
560  }
561  }
562  }
563 }
564 
566  decision_proceduret &dec_proc)
567 {
568  for(auto &step : SSA_steps)
569  if(!step.ignore)
570  {
571  for(const auto &arg : step.io_args)
572  {
573  if(arg.is_constant() ||
574  arg.id()==ID_string_constant)
575  step.converted_io_args.push_back(arg);
576  else
577  {
578  const irep_idt identifier =
579  "symex::io::" + std::to_string(io_count++);
580  symbol_exprt symbol(identifier, arg.type());
581 
582  equal_exprt eq(arg, symbol);
583  merge_irep(eq);
584 
585  dec_proc.set_to(eq, true);
586  step.converted_io_args.push_back(symbol);
587  }
588  }
589  }
590 }
591 
596 {
597  merge_irep(SSA_step.guard);
598 
599  merge_irep(SSA_step.ssa_lhs);
600  merge_irep(SSA_step.ssa_full_lhs);
601  merge_irep(SSA_step.original_full_lhs);
602  merge_irep(SSA_step.ssa_rhs);
603 
604  merge_irep(SSA_step.cond_expr);
605 
606  for(auto &step : SSA_step.io_args)
607  merge_irep(step);
608 
609  for(auto &arg : SSA_step.ssa_function_arguments)
610  merge_irep(arg);
611 
612  // converted_io_args is merged in convert_io
613 }
614 
615 void symex_target_equationt::output(std::ostream &out) const
616 {
617  for(const auto &step : SSA_steps)
618  {
619  step.output(out);
620  out << "--------------\n";
621  }
622 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
symex_target_equation.h
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::typet::ASSUME
@ ASSUME
SSA_stept::comment
std::string comment
Definition: ssa_step.h:149
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:261
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:193
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:67
SSA_stept::atomic_section_id
unsigned atomic_section_id
Definition: ssa_step.h:164
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
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:415
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:293
and_exprt
Boolean AND.
Definition: std_expr.h:2166
exprt
Base class for all expressions.
Definition: expr.h:53
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:300
SSA_stept::formatted
bool formatted
Definition: ssa_step.h:153
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
SSA_stept::guard
exprt guard
Definition: ssa_step.h:137
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
SSA_stept::called_function
irep_idt called_function
Definition: ssa_step.h:158
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:358
equal_exprt
Equality.
Definition: std_expr.h:1196
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
renamedt::get
const underlyingt & get() const
Definition: renamed.h:34
SSA_stept::ssa_function_arguments
std::vector< exprt > ssa_function_arguments
Definition: ssa_step.h:161
ssa_step.h
decision_procedure.h
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
Definition: decision_procedure.cpp:28
symex_targett::assignment_typet::STATE
@ STATE
SSA_stept::io_args
std::list< exprt > io_args
Definition: ssa_step.h:154
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:162
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:340
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:93
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:238
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
SSA_stept::io_id
irep_idt io_id
Definition: ssa_step.h:152
SSA_assignment_stept
Definition: ssa_step.h:199
goto_trace_stept::typet::DECL
@ DECL
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
goto_trace_stept::typet::ASSERT
@ ASSERT
SSA_stept::ssa_full_lhs
exprt ssa_full_lhs
Definition: ssa_step.h:142
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:147
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symex_target_equationt::dead
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
Definition: symex_target_equation.cpp:154
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:565
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
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:438
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:297
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:56
SSA_stept::hidden
bool hidden
Definition: ssa_step.h:135
symex_target_equationt::convert_guards
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
Definition: symex_target_equation.cpp:373
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:39
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:595
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:79
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:456
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:275
format_expr.h
symex_target_equationt::output_fmt
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
Definition: symex_target_equation.cpp:226
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:291
SSA_stept::original_full_lhs
exprt original_full_lhs
Definition: ssa_step.h:142
goto_symex_state.h
symex_target_equationt::function_call
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Definition: symex_target_equation.cpp:174
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:537
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:255
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
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:133
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:334
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:23
SSA_stept::format_string
irep_idt format_string
Definition: ssa_step.h:152
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:321
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:305
messaget::mstreamt
Definition: message.h:221
implies_exprt
Boolean implication.
Definition: std_expr.h:2229
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
messaget::debug
mstreamt & debug() const
Definition: message.h:415
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:392
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
true_exprt
The Boolean constant true.
Definition: std_expr.h:3984
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:128
std_expr.h
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
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:245
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:209
symex_target_equationt::log
messaget log
Definition: symex_target_equation.h:290
not_exprt
Boolean negation.
Definition: std_expr.h:2872
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:106