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 #include <util/throw_with_nested.h>
19 
20 // Can be removed once deprecated SSA_stept::output is removed
21 #include <langapi/language_util.h>
22 
25 #include <solvers/prop/prop.h>
26 #include <solvers/prop/prop_conv.h>
27 
29 #include "goto_symex_state.h"
30 
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 
50  const exprt &guard,
51  const ssa_exprt &ssa_object,
52  unsigned atomic_section_id,
53  const sourcet &source)
54 {
55  SSA_steps.push_back(SSA_stept());
56  SSA_stept &SSA_step=SSA_steps.back();
57 
58  SSA_step.guard=guard;
59  SSA_step.ssa_lhs=ssa_object;
61  SSA_step.atomic_section_id=atomic_section_id;
62  SSA_step.source=source;
63 
64  merge_ireps(SSA_step);
65 }
66 
69  const exprt &guard,
70  const sourcet &source)
71 {
72  SSA_steps.push_back(SSA_stept());
73  SSA_stept &SSA_step=SSA_steps.back();
74  SSA_step.guard=guard;
76  SSA_step.source=source;
77 
78  merge_ireps(SSA_step);
79 }
80 
82  const exprt &guard,
83  const sourcet &source)
84 {
85  SSA_steps.push_back(SSA_stept());
86  SSA_stept &SSA_step=SSA_steps.back();
87  SSA_step.guard=guard;
89  SSA_step.source=source;
90 
91  merge_ireps(SSA_step);
92 }
93 
96  const exprt &guard,
97  unsigned atomic_section_id,
98  const sourcet &source)
99 {
100  SSA_steps.push_back(SSA_stept());
101  SSA_stept &SSA_step=SSA_steps.back();
102  SSA_step.guard=guard;
104  SSA_step.atomic_section_id=atomic_section_id;
105  SSA_step.source=source;
106 
107  merge_ireps(SSA_step);
108 }
109 
112  const exprt &guard,
113  unsigned atomic_section_id,
114  const sourcet &source)
115 {
116  SSA_steps.push_back(SSA_stept());
117  SSA_stept &SSA_step=SSA_steps.back();
118  SSA_step.guard=guard;
120  SSA_step.atomic_section_id=atomic_section_id;
121  SSA_step.source=source;
122 
123  merge_ireps(SSA_step);
124 }
125 
127  const exprt &guard,
128  const ssa_exprt &ssa_lhs,
129  const exprt &ssa_full_lhs,
130  const exprt &original_full_lhs,
131  const exprt &ssa_rhs,
132  const sourcet &source,
133  assignment_typet assignment_type)
134 {
135  PRECONDITION(ssa_lhs.is_not_nil());
136 
137  SSA_steps.push_back(SSA_stept());
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=ssa_full_lhs;
143  SSA_step.original_full_lhs=original_full_lhs;
144  SSA_step.ssa_rhs=ssa_rhs;
145  SSA_step.assignment_type=assignment_type;
146 
147  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
149  SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
151  SSA_step.source=source;
152 
153  merge_ireps(SSA_step);
154 }
155 
157  const exprt &guard,
158  const ssa_exprt &ssa_lhs,
159  const sourcet &source,
160  assignment_typet assignment_type)
161 {
162  PRECONDITION(ssa_lhs.is_not_nil());
163 
164  SSA_steps.push_back(SSA_stept());
165  SSA_stept &SSA_step=SSA_steps.back();
166 
167  SSA_step.guard=guard;
168  SSA_step.ssa_lhs=ssa_lhs;
169  SSA_step.ssa_full_lhs=ssa_lhs;
170  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
172  SSA_step.source=source;
173  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
174 
175  // the condition is trivially true, and only
176  // there so we see the symbols
177  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
178 
179  merge_ireps(SSA_step);
180 }
181 
184  const exprt &,
185  const ssa_exprt &,
186  const sourcet &)
187 {
188  // we currently don't record these
189 }
190 
192  const exprt &guard,
193  const sourcet &source)
194 {
195  SSA_steps.push_back(SSA_stept());
196  SSA_stept &SSA_step=SSA_steps.back();
197 
198  SSA_step.guard=guard;
200  SSA_step.source=source;
201 
202  merge_ireps(SSA_step);
203 }
204 
206  const exprt &guard,
207  const irep_idt &function_identifier,
208  const std::vector<exprt> &ssa_function_arguments,
209  const sourcet &source,
210  const bool hidden)
211 {
212  SSA_steps.push_back(SSA_stept());
213  SSA_stept &SSA_step=SSA_steps.back();
214 
215  SSA_step.guard = guard;
217  SSA_step.source = source;
218  SSA_step.called_function = function_identifier;
219  SSA_step.ssa_function_arguments = ssa_function_arguments;
220  SSA_step.hidden = hidden;
221 
222  merge_ireps(SSA_step);
223 }
224 
226  const exprt &guard,
227  const sourcet &source,
228  const bool hidden)
229 {
230  SSA_steps.push_back(SSA_stept());
231  SSA_stept &SSA_step=SSA_steps.back();
232 
233  SSA_step.guard = guard;
235  SSA_step.source = source;
236  SSA_step.hidden = hidden;
237 
238  merge_ireps(SSA_step);
239 }
240 
242  const exprt &guard,
243  const sourcet &source,
244  const irep_idt &output_id,
245  const std::list<exprt> &args)
246 {
247  SSA_steps.push_back(SSA_stept());
248  SSA_stept &SSA_step=SSA_steps.back();
249 
250  SSA_step.guard=guard;
252  SSA_step.source=source;
253  SSA_step.io_args=args;
254  SSA_step.io_id=output_id;
255 
256  merge_ireps(SSA_step);
257 }
258 
260  const exprt &guard,
261  const sourcet &source,
262  const irep_idt &output_id,
263  const irep_idt &fmt,
264  const std::list<exprt> &args)
265 {
266  SSA_steps.push_back(SSA_stept());
267  SSA_stept &SSA_step=SSA_steps.back();
268 
269  SSA_step.guard=guard;
271  SSA_step.source=source;
272  SSA_step.io_args=args;
273  SSA_step.io_id=output_id;
274  SSA_step.formatted=true;
275  SSA_step.format_string=fmt;
276 
277  merge_ireps(SSA_step);
278 }
279 
281  const exprt &guard,
282  const sourcet &source,
283  const irep_idt &input_id,
284  const std::list<exprt> &args)
285 {
286  SSA_steps.push_back(SSA_stept());
287  SSA_stept &SSA_step=SSA_steps.back();
288 
289  SSA_step.guard=guard;
291  SSA_step.source=source;
292  SSA_step.io_args=args;
293  SSA_step.io_id=input_id;
294 
295  merge_ireps(SSA_step);
296 }
297 
299  const exprt &guard,
300  const exprt &cond,
301  const sourcet &source)
302 {
303  SSA_steps.push_back(SSA_stept());
304  SSA_stept &SSA_step=SSA_steps.back();
305 
306  SSA_step.guard=guard;
307  SSA_step.cond_expr=cond;
309  SSA_step.source=source;
310 
311  merge_ireps(SSA_step);
312 }
313 
315  const exprt &guard,
316  const exprt &cond,
317  const std::string &msg,
318  const sourcet &source)
319 {
320  SSA_steps.push_back(SSA_stept());
321  SSA_stept &SSA_step=SSA_steps.back();
322 
323  SSA_step.guard=guard;
324  SSA_step.cond_expr=cond;
326  SSA_step.source=source;
327  SSA_step.comment=msg;
328 
329  merge_ireps(SSA_step);
330 }
331 
333  const exprt &guard,
334  const exprt &cond,
335  const sourcet &source)
336 {
337  SSA_steps.push_back(SSA_stept());
338  SSA_stept &SSA_step=SSA_steps.back();
339 
340  SSA_step.guard=guard;
341  SSA_step.cond_expr=cond;
343  SSA_step.source=source;
344 
345  merge_ireps(SSA_step);
346 }
347 
349  const exprt &cond,
350  const std::string &msg,
351  const sourcet &source)
352 {
353  // like assumption, but with global effect
354  SSA_steps.push_back(SSA_stept());
355  SSA_stept &SSA_step=SSA_steps.back();
356 
357  SSA_step.guard=true_exprt();
358  SSA_step.cond_expr=cond;
360  SSA_step.source=source;
361  SSA_step.comment=msg;
362 
363  merge_ireps(SSA_step);
364 }
365 
367  prop_convt &prop_conv)
368 {
369  try
370  {
371  convert_guards(prop_conv);
372  convert_assignments(prop_conv);
373  convert_decls(prop_conv);
374  convert_assumptions(prop_conv);
375  convert_assertions(prop_conv);
376  convert_goto_instructions(prop_conv);
377  convert_function_calls(prop_conv);
378  convert_io(prop_conv);
379  convert_constraints(prop_conv);
380  }
381  catch(const equation_conversion_exceptiont &conversion_exception)
382  {
383  // unwrap the except and throw like normal
384  const std::string full_error = unwrap_exception(conversion_exception);
385  throw full_error;
386  }
387 }
388 
390  decision_proceduret &decision_procedure) const
391 {
392  for(const auto &step : SSA_steps)
393  {
394  if(step.is_assignment() && !step.ignore)
395  {
396  decision_procedure.conditional_output(
397  decision_procedure.debug(),
398  [&step](messaget::mstreamt &mstream) {
399  step.output(mstream);
400  mstream << messaget::eom;
401  });
402 
403  decision_procedure.set_to_true(step.cond_expr);
404  }
405  }
406 }
407 
409  prop_convt &prop_conv) const
410 {
411  for(const auto &step : SSA_steps)
412  {
413  if(step.is_decl() && !step.ignore)
414  {
415  // The result is not used, these have no impact on
416  // the satisfiability of the formula.
417  try
418  {
419  prop_conv.convert(step.cond_expr);
420  }
421  catch(const bitvector_conversion_exceptiont &)
422  {
425  "Error converting decls for step", step));
426  }
427  }
428  }
429 }
430 
432  prop_convt &prop_conv)
433 {
434  for(auto &step : SSA_steps)
435  {
436  if(step.ignore)
437  step.guard_literal=const_literal(false);
438  else
439  {
440  prop_conv.conditional_output(
441  prop_conv.debug(),
442  [&step](messaget::mstreamt &mstream) {
443  step.output(mstream);
444  mstream << messaget::eom;
445  });
446 
447  try
448  {
449  step.guard_literal = prop_conv.convert(step.guard);
450  }
451  catch(const bitvector_conversion_exceptiont &)
452  {
455  "Error converting guard for step", step));
456  }
457  }
458  }
459 }
460 
462  prop_convt &prop_conv)
463 {
464  for(auto &step : SSA_steps)
465  {
466  if(step.is_assume())
467  {
468  if(step.ignore)
469  step.cond_literal=const_literal(true);
470  else
471  {
472  prop_conv.conditional_output(
473  prop_conv.debug(),
474  [&step](messaget::mstreamt &mstream) {
475  step.output(mstream);
476  mstream << messaget::eom;
477  });
478 
479  try
480  {
481  step.cond_literal = prop_conv.convert(step.cond_expr);
482  }
483  catch(const bitvector_conversion_exceptiont &)
484  {
487  "Error converting assumptions for step", step));
488  }
489  }
490  }
491  }
492 }
493 
495  prop_convt &prop_conv)
496 {
497  for(auto &step : SSA_steps)
498  {
499  if(step.is_goto())
500  {
501  if(step.ignore)
502  step.cond_literal=const_literal(true);
503  else
504  {
505  prop_conv.conditional_output(
506  prop_conv.debug(),
507  [&step](messaget::mstreamt &mstream) {
508  step.output(mstream);
509  mstream << messaget::eom;
510  });
511 
512  try
513  {
514  step.cond_literal = prop_conv.convert(step.cond_expr);
515  }
516  catch(const bitvector_conversion_exceptiont &)
517  {
520  "Error converting goto instructions for step", step));
521  }
522  }
523  }
524  }
525 }
526 
528  decision_proceduret &decision_procedure) const
529 {
530  for(const auto &step : SSA_steps)
531  {
532  if(step.is_constraint())
533  {
534  if(!step.ignore)
535  {
536  decision_procedure.conditional_output(
537  decision_procedure.debug(),
538  [&step](messaget::mstreamt &mstream) {
539  step.output(mstream);
540  mstream << messaget::eom;
541  });
542 
543  try
544  {
545  decision_procedure.set_to_true(step.cond_expr);
546  }
547  catch(const bitvector_conversion_exceptiont &)
548  {
551  "Error converting constraints for step", step));
552  }
553  }
554  }
555  }
556 }
557 
559  prop_convt &prop_conv)
560 {
561  // we find out if there is only _one_ assertion,
562  // which allows for a simpler formula
563 
564  std::size_t number_of_assertions=count_assertions();
565 
566  if(number_of_assertions==0)
567  return;
568 
569  if(number_of_assertions==1)
570  {
571  for(auto &step : SSA_steps)
572  {
573  if(step.is_assert())
574  {
575  prop_conv.set_to_false(step.cond_expr);
576  step.cond_literal=const_literal(false);
577  return; // prevent further assumptions!
578  }
579  else if(step.is_assume())
580  prop_conv.set_to_true(step.cond_expr);
581  }
582 
583  UNREACHABLE; // unreachable
584  }
585 
586  // We do (NOT a1) OR (NOT a2) ...
587  // where the a's are the assertions
588  or_exprt::operandst disjuncts;
589  disjuncts.reserve(number_of_assertions);
590 
592 
593  for(auto &step : SSA_steps)
594  {
595  if(step.is_assert())
596  {
597  prop_conv.conditional_output(
598  prop_conv.debug(),
599  [&step](messaget::mstreamt &mstream) {
600  step.output(mstream);
601  mstream << messaget::eom;
602  });
603 
604  implies_exprt implication(
605  assumption,
606  step.cond_expr);
607 
608  // do the conversion
609  try
610  {
611  step.cond_literal = prop_conv.convert(implication);
612  }
613  catch(const bitvector_conversion_exceptiont &)
614  {
617  "Error converting assertions for step", step));
618  }
619 
620  // store disjunct
621  disjuncts.push_back(literal_exprt(!step.cond_literal));
622  }
623  else if(step.is_assume())
624  {
625  // the assumptions have been converted before
626  // avoid deep nesting of ID_and expressions
627  if(assumption.id()==ID_and)
628  assumption.copy_to_operands(literal_exprt(step.cond_literal));
629  else
630  assumption=
631  and_exprt(assumption, literal_exprt(step.cond_literal));
632  }
633  }
634 
635  // the below is 'true' if there are no assertions
636  prop_conv.set_to_true(disjunction(disjuncts));
637 }
638 
640  decision_proceduret &dec_proc)
641 {
642  std::size_t argument_count=0;
643 
644  for(auto &step : SSA_steps)
645  if(!step.ignore)
646  {
647  step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
648 
649  for(const auto &arg : step.ssa_function_arguments)
650  {
651  if(arg.is_constant() ||
652  arg.id()==ID_string_constant)
653  step.converted_function_arguments.push_back(arg);
654  else
655  {
656  const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
657  symbol_exprt symbol(identifier, arg.type());
658 
659  equal_exprt eq(arg, symbol);
660  merge_irep(eq);
661 
662  dec_proc.set_to(eq, true);
663  step.converted_function_arguments.push_back(symbol);
664  }
665  }
666  }
667 }
668 
670  decision_proceduret &dec_proc)
671 {
672  std::size_t io_count=0;
673 
674  for(auto &step : SSA_steps)
675  if(!step.ignore)
676  {
677  for(const auto &arg : step.io_args)
678  {
679  if(arg.is_constant() ||
680  arg.id()==ID_string_constant)
681  step.converted_io_args.push_back(arg);
682  else
683  {
684  symbol_exprt symbol;
685  symbol.type()=arg.type();
686  symbol.set_identifier("symex::io::"+std::to_string(io_count++));
687 
688  equal_exprt eq(arg, symbol);
689  merge_irep(eq);
690 
691  dec_proc.set_to(eq, true);
692  step.converted_io_args.push_back(symbol);
693  }
694  }
695  }
696 }
697 
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 
719  std::ostream &out,
720  const namespacet &ns) const
721 {
722  for(const auto &step : SSA_steps)
723  {
724  step.output(ns, out);
725  out << "--------------\n";
726  }
727 }
728 
730  const namespacet &ns,
731  std::ostream &out) const
732 {
733  if(source.is_set)
734  {
735  out << "Thread " << source.thread_nr;
736 
737  if(source.pc->source_location.is_not_nil())
738  out << " " << source.pc->source_location << '\n';
739  else
740  out << '\n';
741  }
742 
743  switch(type)
744  {
746  out << "ASSERT " << from_expr(ns, source.function, cond_expr) << '\n';
747  break;
749  out << "ASSUME " << from_expr(ns, source.function, cond_expr) << '\n';
750  break;
752  out << "LOCATION" << '\n'; break;
754  out << "INPUT" << '\n'; break;
756  out << "OUTPUT" << '\n'; break;
757 
759  out << "DECL" << '\n';
760  out << from_expr(ns, source.function, ssa_lhs) << '\n';
761  break;
762 
764  out << "ASSIGNMENT (";
765  switch(assignment_type)
766  {
768  out << "HIDDEN";
769  break;
771  out << "STATE";
772  break;
774  out << "VISIBLE_ACTUAL_PARAMETER";
775  break;
777  out << "HIDDEN_ACTUAL_PARAMETER";
778  break;
780  out << "PHI";
781  break;
783  out << "GUARD";
784  break;
785  default:
786  {
787  }
788  }
789 
790  out << ")\n";
791  break;
792 
794  out << "DEAD\n"; break;
796  out << "FUNCTION_CALL\n"; break;
798  out << "FUNCTION_RETURN\n"; break;
800  out << "CONSTRAINT\n"; break;
802  out << "SHARED READ\n"; break;
804  out << "SHARED WRITE\n"; break;
806  out << "ATOMIC_BEGIN\n"; break;
808  out << "AUTOMIC_END\n"; break;
810  out << "SPAWN\n"; break;
812  out << "MEMORY_BARRIER\n"; break;
814  out << "IF " << from_expr(ns, source.function, cond_expr) << " GOTO\n";
815  break;
816 
817  default: UNREACHABLE;
818  }
819 
820  if(is_assert() || is_assume() || is_assignment() || is_constraint())
821  out << from_expr(ns, source.function, cond_expr) << '\n';
822 
823  if(is_assert() || is_constraint())
824  out << comment << '\n';
825 
827  out << from_expr(ns, source.function, ssa_lhs) << '\n';
828 
829  out << "Guard: " << from_expr(ns, source.function, guard) << '\n';
830 }
831 
832 void symex_target_equationt::SSA_stept::output(std::ostream &out) const
833 {
834  if(source.is_set)
835  {
836  out << "Thread " << source.thread_nr;
837 
838  if(source.pc->source_location.is_not_nil())
839  out << " " << source.pc->source_location << '\n';
840  else
841  out << '\n';
842  }
843 
844  switch(type)
845  {
847  out << "ASSERT " << format(cond_expr) << '\n';
848  break;
850  out << "ASSUME " << format(cond_expr) << '\n';
851  break;
853  out << "LOCATION" << '\n';
854  break;
856  out << "INPUT" << '\n';
857  break;
859  out << "OUTPUT" << '\n';
860  break;
861 
863  out << "DECL" << '\n';
864  out << format(ssa_lhs) << '\n';
865  break;
866 
868  out << "ASSIGNMENT (";
869  switch(assignment_type)
870  {
872  out << "HIDDEN";
873  break;
875  out << "STATE";
876  break;
878  out << "VISIBLE_ACTUAL_PARAMETER";
879  break;
881  out << "HIDDEN_ACTUAL_PARAMETER";
882  break;
884  out << "PHI";
885  break;
887  out << "GUARD";
888  break;
889  default:
890  {
891  }
892  }
893 
894  out << ")\n";
895  break;
896 
898  out << "DEAD\n";
899  break;
901  out << "FUNCTION_CALL\n";
902  break;
904  out << "FUNCTION_RETURN\n";
905  break;
907  out << "CONSTRAINT\n";
908  break;
910  out << "SHARED READ\n";
911  break;
913  out << "SHARED WRITE\n";
914  break;
916  out << "ATOMIC_BEGIN\n";
917  break;
919  out << "AUTOMIC_END\n";
920  break;
922  out << "SPAWN\n";
923  break;
925  out << "MEMORY_BARRIER\n";
926  break;
928  out << "IF " << format(cond_expr) << " GOTO\n";
929  break;
930 
931  default:
932  UNREACHABLE;
933  }
934 
935  if(is_assert() || is_assume() || is_assignment() || is_constraint())
936  out << format(cond_expr) << '\n';
937 
938  if(is_assert() || is_constraint())
939  out << comment << '\n';
940 
941  if(is_shared_read() || is_shared_write())
942  out << format(ssa_lhs) << '\n';
943 
944  out << "Guard: " << format(guard) << '\n';
945 }
946 
951  const namespacet &ns,
952  const validation_modet vm) const
953 {
954  validate_full_expr(guard, ns, vm);
955 
956  switch(type)
957  {
962  validate_full_expr(cond_expr, ns, vm);
963  break;
966  validate_full_expr(ssa_lhs, ns, vm);
967  validate_full_expr(ssa_full_lhs, ns, vm);
968  validate_full_expr(original_full_lhs, ns, vm);
969  validate_full_expr(ssa_rhs, ns, vm);
970  DATA_CHECK(
971  vm,
972  base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
973  "Type inequality in SSA assignment\nlhs-type: " +
974  ssa_lhs.get_original_expr().type().id_string() +
975  "\nrhs-type: " + ssa_rhs.type().id_string());
976  break;
979  for(const auto &expr : io_args)
980  validate_full_expr(expr, ns, vm);
981  break;
983  for(const auto &expr : ssa_function_arguments)
984  validate_full_expr(expr, ns, vm);
986  {
987  const symbolt *symbol;
988  DATA_CHECK(
989  vm,
990  called_function.empty() || !ns.lookup(called_function, symbol),
991  "unknown function identifier " + id2string(called_function));
992  }
993  break;
1003  break;
1004  }
1005 }
symex_target_equationt::convert_assignments
void convert_assignments(decision_proceduret &decision_procedure) const
Converts assignments: set the equality lhs==rhs to True.
Definition: symex_target_equation.cpp:389
symex_target_equationt::SSA_stept::ssa_full_lhs
exprt ssa_full_lhs
Definition: symex_target_equation.h:290
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:64
symex_target_equationt::SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: symex_target_equation.h:291
symex_target_equation.h
format
static format_containert< T > format(const T &o)
Definition: format.h:35
symex_targett::sourcet::is_set
bool is_set
Definition: symex_target.h:42
symex_target_equationt::SSA_stept::output
void output(const namespacet &ns, std::ostream &out) const
Definition: symex_target_equation.cpp:729
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_trace_stept::typet::LOCATION
@ LOCATION
symex_target_equationt::SSA_stept::guard
exprt guard
Definition: symex_target_equation.h:285
symex_target_equationt::SSA_stept::is_constraint
bool is_constraint() const
Definition: symex_target_equation.h:258
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
symex_target_equationt::SSA_stept::original_full_lhs
exprt original_full_lhs
Definition: symex_target_equation.h:290
goto_trace_stept::typet::ASSUME
@ ASSUME
symex_target_equationt::SSA_stept::assignment_type
assignment_typet assignment_type
Definition: symex_target_equation.h:292
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:298
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
symex_target_equationt::convert
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:366
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:81
symex_target_equationt::convert_guards
void convert_guards(prop_convt &prop_conv)
Converts guards: convert the expression the guard represents.
Definition: symex_target_equation.cpp:431
prop_convt
Definition: prop_conv.h:27
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
symex_target_equationt::SSA_stept::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
Definition: symex_target_equation.cpp:950
decision_proceduret
Definition: decision_procedure.h:20
symex_target_equationt::SSA_stept::is_shared_write
bool is_shared_write() const
Definition: symex_target_equation.h:272
symex_target_equationt::SSA_stept::type
goto_trace_stept::typet type
Definition: symex_target_equation.h:247
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:37
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:408
and_exprt
Boolean AND.
Definition: std_expr.h:2409
symex_target_equationt::convert_assumptions
void convert_assumptions(prop_convt &prop_conv)
Converts assumptions: convert the expression the assumption represents.
Definition: symex_target_equation.cpp:461
exprt
Base class for all expressions.
Definition: expr.h:54
decision_proceduret::set_to_true
void set_to_true(const exprt &expr)
Definition: decision_procedure.h:40
util_throw_with_nested
void util_throw_with_nested(T &&t)
Definition: throw_with_nested.h:37
symex_target_equationt::goto_instruction
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
Definition: symex_target_equation.cpp:332
symex_target_equationt::SSA_stept::is_assert
bool is_assert() const
Definition: symex_target_equation.h:250
bv_conversion_exceptions.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
symex_target_equationt::convert_assertions
void convert_assertions(prop_convt &prop_conv)
Converts assertions: build a disjunction of negated assertions.
Definition: symex_target_equation.cpp:558
symex_target_equationt::SSA_stept::is_shared_read
bool is_shared_read() const
Definition: symex_target_equation.h:270
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
equal_exprt
Equality.
Definition: std_expr.h:1484
symex_target_equationt::decl
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Definition: symex_target_equation.cpp:156
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
decision_proceduret::set_to_false
void set_to_false(const exprt &expr)
Definition: decision_procedure.h:43
symex_targett::assignment_typet::STATE
@ STATE
symex_target_equationt::SSA_stept::source
sourcet source
Definition: symex_target_equation.h:246
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER
@ VISIBLE_ACTUAL_PARAMETER
symex_target_equationt::SSA_stept::io_args
std::list< exprt > io_args
Definition: symex_target_equation.h:302
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:191
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
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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:111
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:346
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
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:26
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
prop_conv.h
symex_target_equationt::function_call
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Definition: symex_target_equation.cpp:205
goto_trace_stept::typet::DECL
@ DECL
symex_target_equationt::convert_goto_instructions
void convert_goto_instructions(prop_convt &prop_conv)
Converts goto instructions: convert the expression representing the condition of this goto.
Definition: symex_target_equation.cpp:494
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER
@ HIDDEN_ACTUAL_PARAMETER
goto_trace_stept::typet::ASSERT
@ ASSERT
symex_target_equationt::convert_decls
void convert_decls(prop_convt &prop_conv) const
Converts declarations: these are effectively ignored by the decision procedure.
Definition: symex_target_equation.cpp:408
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
language_util.h
goto_trace_stept::typet::NONE
@ NONE
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
equation_conversion_exceptions.h
literal_exprt
Definition: literal_expr.h:17
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:183
prop.h
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
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:669
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
validation_modet
validation_modet
Definition: validation_mode.h:12
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
symex_target_equationt::SSA_stept::ssa_function_arguments
std::vector< exprt > ssa_function_arguments
Definition: symex_target_equation.h:309
symex_target_equationt::SSA_stept::formatted
bool formatted
Definition: symex_target_equation.h:301
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:68
unwrap_nested_exception.h
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:49
symex_target_equationt::SSA_stept::io_id
irep_idt io_id
Definition: symex_target_equation.h:300
goto_trace_stept::typet::SPAWN
@ SPAWN
symex_target_equationt::merge_ireps
void merge_ireps(SSA_stept &SSA_step)
Definition: symex_target_equation.cpp:698
symex_target_equationt::SSA_stept::hidden
bool hidden
Definition: symex_target_equation.h:283
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
symex_target_equationt::SSA_stept::called_function
irep_idt called_function
Definition: symex_target_equation.h:306
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:95
symex_targett::sourcet::function
irep_idt function
Definition: symex_target.h:38
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:314
format_expr.h
symex_targett::assignment_typet::PHI
@ PHI
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:259
goto_trace_stept::typet::GOTO
@ GOTO
goto_symex_state.h
unwrap_exception
std::string unwrap_exception(const std::exception &e, int level)
Given a potentially nested exception, produce a string with all of nested exceptions information.
Definition: unwrap_nested_exception.cpp:24
symex_target_equationt::SSA_stept::is_assignment
bool is_assignment() const
Definition: symex_target_equation.h:254
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:639
symbolt
Symbol table entry.
Definition: symbol.h:27
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
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:132
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:31
symex_target_equationt::output
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)
Record an output.
Definition: symex_target_equation.cpp:241
validate_full_expr
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
Definition: validate_expressions.cpp:88
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:348
symex_target_equationt::SSA_stept::atomic_section_id
unsigned atomic_section_id
Definition: symex_target_equation.h:313
symex_target_equationt::SSA_stept::comment
std::string comment
Definition: symex_target_equation.h:297
symex_target_equationt::SSA_stept::cond_expr
exprt cond_expr
Definition: symex_target_equation.h:295
symex_targett::assignment_typet::GUARD
@ GUARD
messaget::mstreamt
Definition: message.h:212
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
messaget::debug
mstreamt & debug() const
Definition: message.h:416
symex_targett::assignment_typet::HIDDEN
@ HIDDEN
symex_target_equationt::function_return
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)
Record return from a function.
Definition: symex_target_equation.cpp:225
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
symex_target_equationt::SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: symex_target_equation.h:289
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
symex_target_equationt::SSA_stept::format_string
irep_idt format_string
Definition: symex_target_equation.h:300
std_expr.h
symex_target_equationt::SSA_stept::is_assume
bool is_assume() const
Definition: symex_target_equation.h:252
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
bitvector_conversion_exceptiont
Definition: bv_conversion_exceptions.h:20
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
symex_target_equationt::convert_constraints
void convert_constraints(decision_proceduret &decision_procedure) const
Converts constraints: set the represented condition to True.
Definition: symex_target_equation.cpp:527
throw_with_nested.h
literal_expr.h
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:280
equation_conversion_exceptiont
Definition: equation_conversion_exceptions.h:21
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
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:126