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 
11 
12 #include "symex_target_equation.h"
13 
14 #include <util/format_expr.h>
15 #include <util/std_expr.h>
16 #include <util/throw_with_nested.h>
18 
19 // Can be removed once deprecated SSA_stept::output is removed
20 #include <langapi/language_util.h>
21 
24 #include <solvers/prop/prop.h>
25 #include <solvers/prop/prop_conv.h>
26 
28 #include "goto_symex_state.h"
29 
32  const exprt &guard,
33  const ssa_exprt &ssa_object,
34  unsigned atomic_section_id,
35  const sourcet &source)
36 {
37  SSA_steps.push_back(SSA_stept());
38  SSA_stept &SSA_step=SSA_steps.back();
39 
40  SSA_step.guard=guard;
41  SSA_step.ssa_lhs=ssa_object;
43  SSA_step.atomic_section_id=atomic_section_id;
44  SSA_step.source=source;
45 
46  merge_ireps(SSA_step);
47 }
48 
51  const exprt &guard,
52  const ssa_exprt &ssa_object,
53  unsigned atomic_section_id,
54  const sourcet &source)
55 {
56  SSA_steps.push_back(SSA_stept());
57  SSA_stept &SSA_step=SSA_steps.back();
58 
59  SSA_step.guard=guard;
60  SSA_step.ssa_lhs=ssa_object;
62  SSA_step.atomic_section_id=atomic_section_id;
63  SSA_step.source=source;
64 
65  merge_ireps(SSA_step);
66 }
67 
70  const exprt &guard,
71  const sourcet &source)
72 {
73  SSA_steps.push_back(SSA_stept());
74  SSA_stept &SSA_step=SSA_steps.back();
75  SSA_step.guard=guard;
77  SSA_step.source=source;
78 
79  merge_ireps(SSA_step);
80 }
81 
83  const exprt &guard,
84  const sourcet &source)
85 {
86  SSA_steps.push_back(SSA_stept());
87  SSA_stept &SSA_step=SSA_steps.back();
88  SSA_step.guard=guard;
90  SSA_step.source=source;
91 
92  merge_ireps(SSA_step);
93 }
94 
97  const exprt &guard,
98  unsigned atomic_section_id,
99  const sourcet &source)
100 {
101  SSA_steps.push_back(SSA_stept());
102  SSA_stept &SSA_step=SSA_steps.back();
103  SSA_step.guard=guard;
105  SSA_step.atomic_section_id=atomic_section_id;
106  SSA_step.source=source;
107 
108  merge_ireps(SSA_step);
109 }
110 
113  const exprt &guard,
114  unsigned atomic_section_id,
115  const sourcet &source)
116 {
117  SSA_steps.push_back(SSA_stept());
118  SSA_stept &SSA_step=SSA_steps.back();
119  SSA_step.guard=guard;
121  SSA_step.atomic_section_id=atomic_section_id;
122  SSA_step.source=source;
123 
124  merge_ireps(SSA_step);
125 }
126 
129  const exprt &guard,
130  const ssa_exprt &ssa_lhs,
131  const exprt &ssa_full_lhs,
132  const exprt &original_full_lhs,
133  const exprt &ssa_rhs,
134  const sourcet &source,
135  assignment_typet assignment_type)
136 {
137  PRECONDITION(ssa_lhs.is_not_nil());
138 
139  SSA_steps.push_back(SSA_stept());
140  SSA_stept &SSA_step=SSA_steps.back();
141 
142  SSA_step.guard=guard;
143  SSA_step.ssa_lhs=ssa_lhs;
144  SSA_step.ssa_full_lhs=ssa_full_lhs;
145  SSA_step.original_full_lhs=original_full_lhs;
146  SSA_step.ssa_rhs=ssa_rhs;
147  SSA_step.assignment_type=assignment_type;
148 
149  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
151  SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
153  SSA_step.source=source;
154 
155  merge_ireps(SSA_step);
156 }
157 
160  const exprt &guard,
161  const ssa_exprt &ssa_lhs,
162  const sourcet &source,
163  assignment_typet assignment_type)
164 {
165  PRECONDITION(ssa_lhs.is_not_nil());
166 
167  SSA_steps.push_back(SSA_stept());
168  SSA_stept &SSA_step=SSA_steps.back();
169 
170  SSA_step.guard=guard;
171  SSA_step.ssa_lhs=ssa_lhs;
172  SSA_step.ssa_full_lhs=ssa_lhs;
173  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
175  SSA_step.source=source;
176  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
177 
178  // the condition is trivially true, and only
179  // there so we see the symbols
180  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
181 
182  merge_ireps(SSA_step);
183 }
184 
187  const exprt &,
188  const ssa_exprt &,
189  const sourcet &)
190 {
191  // we currently don't record these
192 }
193 
196  const exprt &guard,
197  const sourcet &source)
198 {
199  SSA_steps.push_back(SSA_stept());
200  SSA_stept &SSA_step=SSA_steps.back();
201 
202  SSA_step.guard=guard;
204  SSA_step.source=source;
205 
206  merge_ireps(SSA_step);
207 }
208 
211  const exprt &guard,
212  const irep_idt &identifier,
213  const sourcet &source)
214 {
215  SSA_steps.push_back(SSA_stept());
216  SSA_stept &SSA_step=SSA_steps.back();
217 
218  SSA_step.guard=guard;
220  SSA_step.source=source;
221  SSA_step.identifier=identifier;
222 
223  merge_ireps(SSA_step);
224 }
225 
228  const exprt &guard,
229  const irep_idt &identifier,
230  const sourcet &source)
231 {
232  SSA_steps.push_back(SSA_stept());
233  SSA_stept &SSA_step=SSA_steps.back();
234 
235  SSA_step.guard=guard;
237  SSA_step.source=source;
238  SSA_step.identifier=identifier;
239 
240  merge_ireps(SSA_step);
241 }
242 
245  const exprt &guard,
246  const sourcet &source,
247  const irep_idt &output_id,
248  const std::list<exprt> &args)
249 {
250  SSA_steps.push_back(SSA_stept());
251  SSA_stept &SSA_step=SSA_steps.back();
252 
253  SSA_step.guard=guard;
255  SSA_step.source=source;
256  SSA_step.io_args=args;
257  SSA_step.io_id=output_id;
258 
259  merge_ireps(SSA_step);
260 }
261 
264  const exprt &guard,
265  const sourcet &source,
266  const irep_idt &output_id,
267  const irep_idt &fmt,
268  const std::list<exprt> &args)
269 {
270  SSA_steps.push_back(SSA_stept());
271  SSA_stept &SSA_step=SSA_steps.back();
272 
273  SSA_step.guard=guard;
275  SSA_step.source=source;
276  SSA_step.io_args=args;
277  SSA_step.io_id=output_id;
278  SSA_step.formatted=true;
279  SSA_step.format_string=fmt;
280 
281  merge_ireps(SSA_step);
282 }
283 
286  const exprt &guard,
287  const sourcet &source,
288  const irep_idt &input_id,
289  const std::list<exprt> &args)
290 {
291  SSA_steps.push_back(SSA_stept());
292  SSA_stept &SSA_step=SSA_steps.back();
293 
294  SSA_step.guard=guard;
296  SSA_step.source=source;
297  SSA_step.io_args=args;
298  SSA_step.io_id=input_id;
299 
300  merge_ireps(SSA_step);
301 }
302 
305  const exprt &guard,
306  const exprt &cond,
307  const sourcet &source)
308 {
309  SSA_steps.push_back(SSA_stept());
310  SSA_stept &SSA_step=SSA_steps.back();
311 
312  SSA_step.guard=guard;
313  SSA_step.cond_expr=cond;
315  SSA_step.source=source;
316 
317  merge_ireps(SSA_step);
318 }
319 
322  const exprt &guard,
323  const exprt &cond,
324  const std::string &msg,
325  const sourcet &source)
326 {
327  SSA_steps.push_back(SSA_stept());
328  SSA_stept &SSA_step=SSA_steps.back();
329 
330  SSA_step.guard=guard;
331  SSA_step.cond_expr=cond;
333  SSA_step.source=source;
334  SSA_step.comment=msg;
335 
336  merge_ireps(SSA_step);
337 }
338 
341  const exprt &guard,
342  const exprt &cond,
343  const sourcet &source)
344 {
345  SSA_steps.push_back(SSA_stept());
346  SSA_stept &SSA_step=SSA_steps.back();
347 
348  SSA_step.guard=guard;
349  SSA_step.cond_expr=cond;
351  SSA_step.source=source;
352 
353  merge_ireps(SSA_step);
354 }
355 
358  const exprt &cond,
359  const std::string &msg,
360  const sourcet &source)
361 {
362  // like assumption, but with global effect
363  SSA_steps.push_back(SSA_stept());
364  SSA_stept &SSA_step=SSA_steps.back();
365 
366  SSA_step.guard=true_exprt();
367  SSA_step.cond_expr=cond;
369  SSA_step.source=source;
370  SSA_step.comment=msg;
371 
372  merge_ireps(SSA_step);
373 }
374 
376  prop_convt &prop_conv)
377 {
378  try
379  {
380  convert_guards(prop_conv);
381  convert_assignments(prop_conv);
382  convert_decls(prop_conv);
383  convert_assumptions(prop_conv);
384  convert_assertions(prop_conv);
385  convert_goto_instructions(prop_conv);
386  convert_io(prop_conv);
387  convert_constraints(prop_conv);
388  }
389  catch(const equation_conversion_exceptiont &conversion_exception)
390  {
391  // unwrap the except and throw like normal
392  const std::string full_error = unwrap_exception(conversion_exception);
393  throw full_error;
394  }
395 }
396 
401  decision_proceduret &decision_procedure) const
402 {
403  for(const auto &step : SSA_steps)
404  {
405  if(step.is_assignment() && !step.ignore)
406  {
407  decision_procedure.conditional_output(
408  decision_procedure.debug(),
409  [&step](messaget::mstreamt &mstream) {
410  std::ostringstream oss;
411  step.output(oss);
412  mstream << oss.str() << messaget::eom;
413  });
414 
415  decision_procedure.set_to_true(step.cond_expr);
416  }
417  }
418 }
419 
423  prop_convt &prop_conv) const
424 {
425  for(const auto &step : SSA_steps)
426  {
427  if(step.is_decl() && !step.ignore)
428  {
429  // The result is not used, these have no impact on
430  // the satisfiability of the formula.
431  try
432  {
433  prop_conv.convert(step.cond_expr);
434  }
435  catch(const bitvector_conversion_exceptiont &)
436  {
439  "Error converting decls for step", step));
440  }
441  }
442  }
443 }
444 
448  prop_convt &prop_conv)
449 {
450  for(auto &step : SSA_steps)
451  {
452  if(step.ignore)
453  step.guard_literal=const_literal(false);
454  else
455  {
456  prop_conv.conditional_output(
457  prop_conv.debug(),
458  [&step](messaget::mstreamt &mstream) {
459  std::ostringstream oss;
460  step.output(oss);
461  mstream << oss.str() << messaget::eom;
462  });
463 
464  try
465  {
466  step.guard_literal = prop_conv.convert(step.guard);
467  }
468  catch(const bitvector_conversion_exceptiont &)
469  {
472  "Error converting guard for step", step));
473  }
474  }
475  }
476 }
477 
481  prop_convt &prop_conv)
482 {
483  for(auto &step : SSA_steps)
484  {
485  if(step.is_assume())
486  {
487  if(step.ignore)
488  step.cond_literal=const_literal(true);
489  else
490  {
491  prop_conv.conditional_output(
492  prop_conv.debug(),
493  [&step](messaget::mstreamt &mstream) {
494  std::ostringstream oss;
495  step.output(oss);
496  mstream << oss.str() << messaget::eom;
497  });
498 
499  try
500  {
501  step.cond_literal = prop_conv.convert(step.cond_expr);
502  }
503  catch(const bitvector_conversion_exceptiont &)
504  {
507  "Error converting assumptions for step", step));
508  }
509  }
510  }
511  }
512 }
513 
517  prop_convt &prop_conv)
518 {
519  for(auto &step : SSA_steps)
520  {
521  if(step.is_goto())
522  {
523  if(step.ignore)
524  step.cond_literal=const_literal(true);
525  else
526  {
527  prop_conv.conditional_output(
528  prop_conv.debug(),
529  [&step](messaget::mstreamt &mstream) {
530  std::ostringstream oss;
531  step.output(oss);
532  mstream << oss.str() << messaget::eom;
533  });
534 
535  try
536  {
537  step.cond_literal = prop_conv.convert(step.cond_expr);
538  }
539  catch(const bitvector_conversion_exceptiont &)
540  {
543  "Error converting goto instructions for step", step));
544  }
545  }
546  }
547  }
548 }
549 
554  decision_proceduret &decision_procedure) const
555 {
556  for(const auto &step : SSA_steps)
557  {
558  if(step.is_constraint())
559  {
560  if(!step.ignore)
561  {
562  decision_procedure.conditional_output(
563  decision_procedure.debug(),
564  [&step](messaget::mstreamt &mstream) {
565  std::ostringstream oss;
566  step.output(oss);
567  mstream << oss.str() << messaget::eom;
568  });
569 
570  try
571  {
572  decision_procedure.set_to_true(step.cond_expr);
573  }
574  catch(const bitvector_conversion_exceptiont &)
575  {
578  "Error converting constraints for step", step));
579  }
580  }
581  }
582  }
583 }
584 
588  prop_convt &prop_conv)
589 {
590  // we find out if there is only _one_ assertion,
591  // which allows for a simpler formula
592 
593  std::size_t number_of_assertions=count_assertions();
594 
595  if(number_of_assertions==0)
596  return;
597 
598  if(number_of_assertions==1)
599  {
600  for(auto &step : SSA_steps)
601  {
602  if(step.is_assert())
603  {
604  prop_conv.set_to_false(step.cond_expr);
605  step.cond_literal=const_literal(false);
606  return; // prevent further assumptions!
607  }
608  else if(step.is_assume())
609  prop_conv.set_to_true(step.cond_expr);
610  }
611 
612  UNREACHABLE; // unreachable
613  }
614 
615  // We do (NOT a1) OR (NOT a2) ...
616  // where the a's are the assertions
617  or_exprt::operandst disjuncts;
618  disjuncts.reserve(number_of_assertions);
619 
621 
622  for(auto &step : SSA_steps)
623  {
624  if(step.is_assert())
625  {
626  implies_exprt implication(
627  assumption,
628  step.cond_expr);
629 
630  // do the conversion
631  try
632  {
633  step.cond_literal = prop_conv.convert(implication);
634  }
635  catch(const bitvector_conversion_exceptiont &)
636  {
639  "Error converting assertions for step", step));
640  }
641 
642  // store disjunct
643  disjuncts.push_back(literal_exprt(!step.cond_literal));
644  }
645  else if(step.is_assume())
646  {
647  // the assumptions have been converted before
648  // avoid deep nesting of ID_and expressions
649  if(assumption.id()==ID_and)
650  assumption.copy_to_operands(literal_exprt(step.cond_literal));
651  else
652  assumption=
653  and_exprt(assumption, literal_exprt(step.cond_literal));
654  }
655  }
656 
657  // the below is 'true' if there are no assertions
658  prop_conv.set_to_true(disjunction(disjuncts));
659 }
660 
665  decision_proceduret &dec_proc)
666 {
667  std::size_t io_count=0;
668 
669  for(auto &step : SSA_steps)
670  if(!step.ignore)
671  {
672  for(const auto &arg : step.io_args)
673  {
674  if(arg.is_constant() ||
675  arg.id()==ID_string_constant)
676  step.converted_io_args.push_back(arg);
677  else
678  {
679  symbol_exprt symbol;
680  symbol.type()=arg.type();
681  symbol.set_identifier("symex::io::"+std::to_string(io_count++));
682 
683  equal_exprt eq(arg, symbol);
684  merge_irep(eq);
685 
686  dec_proc.set_to(eq, true);
687  step.converted_io_args.push_back(symbol);
688  }
689  }
690  }
691 }
692 
693 
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  // converted_io_args is merged in convert_io
709 }
710 
712  std::ostream &out,
713  const namespacet &ns) const
714 {
715  for(const auto &step : SSA_steps)
716  {
717  step.output(ns, out);
718  out << "--------------\n";
719  }
720 }
721 
723  const namespacet &ns,
724  std::ostream &out) const
725 {
726  if(source.is_set)
727  {
728  out << "Thread " << source.thread_nr;
729 
730  if(source.pc->source_location.is_not_nil())
731  out << " " << source.pc->source_location << '\n';
732  else
733  out << '\n';
734  }
735 
736  switch(type)
737  {
739  out << "ASSERT " << from_expr(ns, source.pc->function, cond_expr) << '\n';
740  break;
742  out << "ASSUME " << from_expr(ns, source.pc->function, cond_expr) << '\n';
743  break;
745  out << "LOCATION" << '\n'; break;
747  out << "INPUT" << '\n'; break;
749  out << "OUTPUT" << '\n'; break;
750 
752  out << "DECL" << '\n';
753  out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
754  break;
755 
757  out << "ASSIGNMENT (";
758  switch(assignment_type)
759  {
761  out << "HIDDEN";
762  break;
764  out << "STATE";
765  break;
767  out << "VISIBLE_ACTUAL_PARAMETER";
768  break;
770  out << "HIDDEN_ACTUAL_PARAMETER";
771  break;
773  out << "PHI";
774  break;
776  out << "GUARD";
777  break;
778  default:
779  {
780  }
781  }
782 
783  out << ")\n";
784  break;
785 
787  out << "DEAD\n"; break;
789  out << "FUNCTION_CALL\n"; break;
791  out << "FUNCTION_RETURN\n"; break;
793  out << "CONSTRAINT\n"; break;
795  out << "SHARED READ\n"; break;
797  out << "SHARED WRITE\n"; break;
799  out << "ATOMIC_BEGIN\n"; break;
801  out << "AUTOMIC_END\n"; break;
803  out << "SPAWN\n"; break;
805  out << "MEMORY_BARRIER\n"; break;
807  out << "IF " << from_expr(ns, source.pc->function, cond_expr) << " GOTO\n";
808  break;
809 
810  default: UNREACHABLE;
811  }
812 
813  if(is_assert() || is_assume() || is_assignment() || is_constraint())
814  out << from_expr(ns, source.pc->function, cond_expr) << '\n';
815 
816  if(is_assert() || is_constraint())
817  out << comment << '\n';
818 
820  out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
821 
822  out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
823 }
824 
825 void symex_target_equationt::SSA_stept::output(std::ostream &out) const
826 {
827  if(source.is_set)
828  {
829  out << "Thread " << source.thread_nr;
830 
831  if(source.pc->source_location.is_not_nil())
832  out << " " << source.pc->source_location << '\n';
833  else
834  out << '\n';
835  }
836 
837  switch(type)
838  {
840  out << "ASSERT " << format(cond_expr) << '\n';
841  break;
843  out << "ASSUME " << format(cond_expr) << '\n';
844  break;
846  out << "LOCATION" << '\n';
847  break;
849  out << "INPUT" << '\n';
850  break;
852  out << "OUTPUT" << '\n';
853  break;
854 
856  out << "DECL" << '\n';
857  out << format(ssa_lhs) << '\n';
858  break;
859 
861  out << "ASSIGNMENT (";
862  switch(assignment_type)
863  {
865  out << "HIDDEN";
866  break;
868  out << "STATE";
869  break;
871  out << "VISIBLE_ACTUAL_PARAMETER";
872  break;
874  out << "HIDDEN_ACTUAL_PARAMETER";
875  break;
877  out << "PHI";
878  break;
880  out << "GUARD";
881  break;
882  default:
883  {
884  }
885  }
886 
887  out << ")\n";
888  break;
889 
891  out << "DEAD\n";
892  break;
894  out << "FUNCTION_CALL\n";
895  break;
897  out << "FUNCTION_RETURN\n";
898  break;
900  out << "CONSTRAINT\n";
901  break;
903  out << "SHARED READ\n";
904  break;
906  out << "SHARED WRITE\n";
907  break;
909  out << "ATOMIC_BEGIN\n";
910  break;
912  out << "AUTOMIC_END\n";
913  break;
915  out << "SPAWN\n";
916  break;
918  out << "MEMORY_BARRIER\n";
919  break;
921  out << "IF " << format(cond_expr) << " GOTO\n";
922  break;
923 
924  default:
925  UNREACHABLE;
926  }
927 
928  if(is_assert() || is_assume() || is_assignment() || is_constraint())
929  out << format(cond_expr) << '\n';
930 
931  if(is_assert() || is_constraint())
932  out << comment << '\n';
933 
934  if(is_shared_read() || is_shared_write())
935  out << format(ssa_lhs) << '\n';
936 
937  out << "Guard: " << format(guard) << '\n';
938 }
virtual void spawn(const exprt &guard, const sourcet &source)
spawn a new thread
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
virtual void memory_barrier(const exprt &guard, const sourcet &source)
bool is_not_nil() const
Definition: irep.h:173
Generate Equation using Symbolic Execution.
void convert(prop_convt &prop_conv)
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
void convert_assumptions(prop_convt &prop_conv)
converts assumptions
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
Symbolic Execution.
typet & type()
Definition: expr.h:56
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
std::string unwrap_exception(const std::exception &e, int level)
Given a potentially nested exception, produce a string with all of nested exceptions information...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end an atomic section
boolean implication
Definition: std_expr.h:2339
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
equality
Definition: std_expr.h:1354
The boolean constant true.
Definition: std_expr.h:4486
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
Exceptions that can be raised during the equation conversion phase.
void util_throw_with_nested(T &&t)
void convert_constraints(decision_proceduret &decision_procedure) const
converts constraints
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
declare a fresh variable
Exceptions that can be raised in bv_conversion.
boolean AND
Definition: std_expr.h:2255
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
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 variable
virtual literalt convert(const exprt &expr)=0
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just record formatted output
virtual void set_to(const exprt &expr, bool value)=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
std::vector< exprt > operandst
Definition: expr.h:45
void convert_goto_instructions(prop_convt &prop_conv)
converts goto instructions
literalt const_literal(bool value)
Definition: literal.h:187
void convert_assignments(decision_proceduret &decision_procedure) const
converts assignments
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
read from a shared variable
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
void convert_assertions(prop_convt &prop_conv)
converts assertions
void set_to_false(const exprt &expr)
void convert_decls(prop_convt &prop_conv) const
converts declarations
Base class for all expressions.
Definition: expr.h:42
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
void set_to_true(const exprt &expr)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to mstream using output_generator if the configured verbosity is at least as high as ...
Definition: message.cpp:113
#define UNREACHABLE
Definition: invariant.h:271
virtual void location(const exprt &guard, const sourcet &source)
just record a location
std::size_t count_assertions() const
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
Expression to hold a symbol (variable)
Definition: std_expr.h:90
mstreamt & debug() const
Definition: message.h:332
void output(const namespacet &ns, std::ostream &out) const
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
declare a fresh variable
void merge_ireps(SSA_stept &SSA_step)
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void convert_guards(prop_convt &prop_conv)
converts guards
void convert_io(decision_proceduret &decision_procedure)
converts I/O
static format_containert< T > format(const T &o)
Definition: format.h:35