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 <cassert>
15 
16 #include <util/std_expr.h>
17 
18 #include <langapi/language_util.h>
19 #include <solvers/prop/prop_conv.h>
20 #include <solvers/prop/prop.h>
22 
23 #include "goto_symex_state.h"
24 
26  const namespacet &_ns):ns(_ns)
27 {
28 }
29 
31 {
32 }
33 
36  const exprt &guard,
37  const ssa_exprt &ssa_object,
38  unsigned atomic_section_id,
39  const sourcet &source)
40 {
41  SSA_steps.push_back(SSA_stept());
42  SSA_stept &SSA_step=SSA_steps.back();
43 
44  SSA_step.guard=guard;
45  SSA_step.ssa_lhs=ssa_object;
47  SSA_step.atomic_section_id=atomic_section_id;
48  SSA_step.source=source;
49 
50  merge_ireps(SSA_step);
51 }
52 
55  const exprt &guard,
56  const ssa_exprt &ssa_object,
57  unsigned atomic_section_id,
58  const sourcet &source)
59 {
60  SSA_steps.push_back(SSA_stept());
61  SSA_stept &SSA_step=SSA_steps.back();
62 
63  SSA_step.guard=guard;
64  SSA_step.ssa_lhs=ssa_object;
66  SSA_step.atomic_section_id=atomic_section_id;
67  SSA_step.source=source;
68 
69  merge_ireps(SSA_step);
70 }
71 
74  const exprt &guard,
75  const sourcet &source)
76 {
77  SSA_steps.push_back(SSA_stept());
78  SSA_stept &SSA_step=SSA_steps.back();
79  SSA_step.guard=guard;
81  SSA_step.source=source;
82 
83  merge_ireps(SSA_step);
84 }
85 
87  const exprt &guard,
88  const sourcet &source)
89 {
90  SSA_steps.push_back(SSA_stept());
91  SSA_stept &SSA_step=SSA_steps.back();
92  SSA_step.guard=guard;
94  SSA_step.source=source;
95 
96  merge_ireps(SSA_step);
97 }
98 
101  const exprt &guard,
102  unsigned atomic_section_id,
103  const sourcet &source)
104 {
105  SSA_steps.push_back(SSA_stept());
106  SSA_stept &SSA_step=SSA_steps.back();
107  SSA_step.guard=guard;
109  SSA_step.atomic_section_id=atomic_section_id;
110  SSA_step.source=source;
111 
112  merge_ireps(SSA_step);
113 }
114 
117  const exprt &guard,
118  unsigned atomic_section_id,
119  const sourcet &source)
120 {
121  SSA_steps.push_back(SSA_stept());
122  SSA_stept &SSA_step=SSA_steps.back();
123  SSA_step.guard=guard;
125  SSA_step.atomic_section_id=atomic_section_id;
126  SSA_step.source=source;
127 
128  merge_ireps(SSA_step);
129 }
130 
133  const exprt &guard,
134  const ssa_exprt &ssa_lhs,
135  const exprt &ssa_full_lhs,
136  const exprt &original_full_lhs,
137  const exprt &ssa_rhs,
138  const sourcet &source,
139  assignment_typet assignment_type)
140 {
141  assert(ssa_lhs.is_not_nil());
142 
143  SSA_steps.push_back(SSA_stept());
144  SSA_stept &SSA_step=SSA_steps.back();
145 
146  SSA_step.guard=guard;
147  SSA_step.ssa_lhs=ssa_lhs;
148  SSA_step.ssa_full_lhs=ssa_full_lhs;
149  SSA_step.original_full_lhs=original_full_lhs;
150  SSA_step.ssa_rhs=ssa_rhs;
151  SSA_step.assignment_type=assignment_type;
152 
153  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs);
155  SSA_step.hidden=(assignment_type!=assignment_typet::STATE &&
157  SSA_step.source=source;
158 
159  merge_ireps(SSA_step);
160 }
161 
164  const exprt &guard,
165  const ssa_exprt &ssa_lhs,
166  const sourcet &source,
167  assignment_typet assignment_type)
168 {
169  assert(ssa_lhs.is_not_nil());
170 
171  SSA_steps.push_back(SSA_stept());
172  SSA_stept &SSA_step=SSA_steps.back();
173 
174  SSA_step.guard=guard;
175  SSA_step.ssa_lhs=ssa_lhs;
176  SSA_step.ssa_full_lhs=ssa_lhs;
177  SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
179  SSA_step.source=source;
180  SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
181 
182  // the condition is trivially true, and only
183  // there so we see the symbols
184  SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_lhs);
185 
186  merge_ireps(SSA_step);
187 }
188 
191  const exprt &guard,
192  const ssa_exprt &ssa_lhs,
193  const sourcet &source)
194 {
195  // we currently don't record these
196 }
197 
200  const exprt &guard,
201  const sourcet &source)
202 {
203  SSA_steps.push_back(SSA_stept());
204  SSA_stept &SSA_step=SSA_steps.back();
205 
206  SSA_step.guard=guard;
208  SSA_step.source=source;
209 
210  merge_ireps(SSA_step);
211 }
212 
215  const exprt &guard,
216  const irep_idt &identifier,
217  const sourcet &source)
218 {
219  SSA_steps.push_back(SSA_stept());
220  SSA_stept &SSA_step=SSA_steps.back();
221 
222  SSA_step.guard=guard;
224  SSA_step.source=source;
225  SSA_step.identifier=identifier;
226 
227  merge_ireps(SSA_step);
228 }
229 
232  const exprt &guard,
233  const irep_idt &identifier,
234  const sourcet &source)
235 {
236  SSA_steps.push_back(SSA_stept());
237  SSA_stept &SSA_step=SSA_steps.back();
238 
239  SSA_step.guard=guard;
241  SSA_step.source=source;
242  SSA_step.identifier=identifier;
243 
244  merge_ireps(SSA_step);
245 }
246 
249  const exprt &guard,
250  const sourcet &source,
251  const irep_idt &output_id,
252  const std::list<exprt> &args)
253 {
254  SSA_steps.push_back(SSA_stept());
255  SSA_stept &SSA_step=SSA_steps.back();
256 
257  SSA_step.guard=guard;
259  SSA_step.source=source;
260  SSA_step.io_args=args;
261  SSA_step.io_id=output_id;
262 
263  merge_ireps(SSA_step);
264 }
265 
268  const exprt &guard,
269  const sourcet &source,
270  const irep_idt &output_id,
271  const irep_idt &fmt,
272  const std::list<exprt> &args)
273 {
274  SSA_steps.push_back(SSA_stept());
275  SSA_stept &SSA_step=SSA_steps.back();
276 
277  SSA_step.guard=guard;
279  SSA_step.source=source;
280  SSA_step.io_args=args;
281  SSA_step.io_id=output_id;
282  SSA_step.formatted=true;
283  SSA_step.format_string=fmt;
284 
285  merge_ireps(SSA_step);
286 }
287 
290  const exprt &guard,
291  const sourcet &source,
292  const irep_idt &input_id,
293  const std::list<exprt> &args)
294 {
295  SSA_steps.push_back(SSA_stept());
296  SSA_stept &SSA_step=SSA_steps.back();
297 
298  SSA_step.guard=guard;
300  SSA_step.source=source;
301  SSA_step.io_args=args;
302  SSA_step.io_id=input_id;
303 
304  merge_ireps(SSA_step);
305 }
306 
309  const exprt &guard,
310  const exprt &cond,
311  const sourcet &source)
312 {
313  SSA_steps.push_back(SSA_stept());
314  SSA_stept &SSA_step=SSA_steps.back();
315 
316  SSA_step.guard=guard;
317  SSA_step.cond_expr=cond;
319  SSA_step.source=source;
320 
321  merge_ireps(SSA_step);
322 }
323 
326  const exprt &guard,
327  const exprt &cond,
328  const std::string &msg,
329  const sourcet &source)
330 {
331  SSA_steps.push_back(SSA_stept());
332  SSA_stept &SSA_step=SSA_steps.back();
333 
334  SSA_step.guard=guard;
335  SSA_step.cond_expr=cond;
337  SSA_step.source=source;
338  SSA_step.comment=msg;
339 
340  merge_ireps(SSA_step);
341 }
342 
345  const exprt &guard,
346  const exprt &cond,
347  const sourcet &source)
348 {
349  SSA_steps.push_back(SSA_stept());
350  SSA_stept &SSA_step=SSA_steps.back();
351 
352  SSA_step.guard=guard;
353  SSA_step.cond_expr=cond;
355  SSA_step.source=source;
356 
357  merge_ireps(SSA_step);
358 }
359 
362  const exprt &cond,
363  const std::string &msg,
364  const sourcet &source)
365 {
366  // like assumption, but with global effect
367  SSA_steps.push_back(SSA_stept());
368  SSA_stept &SSA_step=SSA_steps.back();
369 
370  SSA_step.guard=true_exprt();
371  SSA_step.cond_expr=cond;
373  SSA_step.source=source;
374  SSA_step.comment=msg;
375 
376  merge_ireps(SSA_step);
377 }
378 
380  prop_convt &prop_conv)
381 {
382  convert_guards(prop_conv);
383  convert_assignments(prop_conv);
384  convert_decls(prop_conv);
385  convert_assumptions(prop_conv);
386  convert_assertions(prop_conv);
387  convert_goto_instructions(prop_conv);
388  convert_io(prop_conv);
389  convert_constraints(prop_conv);
390 }
391 
396  decision_proceduret &decision_procedure) const
397 {
398  for(const auto &step : SSA_steps)
399  {
400  if(step.is_assignment() && !step.ignore)
401  decision_procedure.set_to_true(step.cond_expr);
402  }
403 }
404 
408  prop_convt &prop_conv) const
409 {
410  for(const auto &step : SSA_steps)
411  {
412  if(step.is_decl() && !step.ignore)
413  {
414  // The result is not used, these have no impact on
415  // the satisfiability of the formula.
416  prop_conv.convert(step.cond_expr);
417  }
418  }
419 }
420 
424  prop_convt &prop_conv)
425 {
426  for(auto &step : SSA_steps)
427  {
428  if(step.ignore)
429  step.guard_literal=const_literal(false);
430  else
431  step.guard_literal=prop_conv.convert(step.guard);
432  }
433 }
434 
438  prop_convt &prop_conv)
439 {
440  for(auto &step : SSA_steps)
441  {
442  if(step.is_assume())
443  {
444  if(step.ignore)
445  step.cond_literal=const_literal(true);
446  else
447  step.cond_literal=prop_conv.convert(step.cond_expr);
448  }
449  }
450 }
451 
455  prop_convt &prop_conv)
456 {
457  for(auto &step : SSA_steps)
458  {
459  if(step.is_goto())
460  {
461  if(step.ignore)
462  step.cond_literal=const_literal(true);
463  else
464  step.cond_literal=prop_conv.convert(step.cond_expr);
465  }
466  }
467 }
468 
473  decision_proceduret &decision_procedure) const
474 {
475  for(const auto &step : SSA_steps)
476  {
477  if(step.is_constraint())
478  {
479  if(step.ignore)
480  continue;
481 
482  decision_procedure.set_to_true(step.cond_expr);
483  }
484  }
485 }
486 
490  prop_convt &prop_conv)
491 {
492  // we find out if there is only _one_ assertion,
493  // which allows for a simpler formula
494 
495  unsigned number_of_assertions=count_assertions();
496 
497  if(number_of_assertions==0)
498  return;
499 
500  if(number_of_assertions==1)
501  {
502  for(auto &step : SSA_steps)
503  {
504  if(step.is_assert())
505  {
506  prop_conv.set_to_false(step.cond_expr);
507  step.cond_literal=const_literal(false);
508  return; // prevent further assumptions!
509  }
510  else if(step.is_assume())
511  prop_conv.set_to_true(step.cond_expr);
512  }
513 
514  assert(false); // unreachable
515  }
516 
517  // We do (NOT a1) OR (NOT a2) ...
518  // where the a's are the assertions
519  or_exprt::operandst disjuncts;
520  disjuncts.reserve(number_of_assertions);
521 
523 
524  for(auto &step : SSA_steps)
525  {
526  if(step.is_assert())
527  {
528  implies_exprt implication(
529  assumption,
530  step.cond_expr);
531 
532  // do the conversion
533  step.cond_literal=prop_conv.convert(implication);
534 
535  // store disjunct
536  disjuncts.push_back(literal_exprt(!step.cond_literal));
537  }
538  else if(step.is_assume())
539  {
540  // the assumptions have been converted before
541  // avoid deep nesting of ID_and expressions
542  if(assumption.id()==ID_and)
543  assumption.copy_to_operands(literal_exprt(step.cond_literal));
544  else
545  assumption=
546  and_exprt(assumption, literal_exprt(step.cond_literal));
547  }
548  }
549 
550  // the below is 'true' if there are no assertions
551  prop_conv.set_to_true(disjunction(disjuncts));
552 }
553 
558  decision_proceduret &dec_proc)
559 {
560  unsigned io_count=0;
561 
562  for(auto &step : SSA_steps)
563  if(!step.ignore)
564  {
565  for(const auto &arg : step.io_args)
566  {
567  if(arg.is_constant() ||
568  arg.id()==ID_string_constant)
569  step.converted_io_args.push_back(arg);
570  else
571  {
572  symbol_exprt symbol;
573  symbol.type()=arg.type();
574  symbol.set_identifier("symex::io::"+std::to_string(io_count++));
575 
576  equal_exprt eq(arg, symbol);
577  merge_irep(eq);
578 
579  dec_proc.set_to(eq, true);
580  step.converted_io_args.push_back(symbol);
581  }
582  }
583  }
584 }
585 
586 
588 {
589  merge_irep(SSA_step.guard);
590 
591  merge_irep(SSA_step.ssa_lhs);
592  merge_irep(SSA_step.ssa_full_lhs);
593  merge_irep(SSA_step.original_full_lhs);
594  merge_irep(SSA_step.ssa_rhs);
595 
596  merge_irep(SSA_step.cond_expr);
597 
598  for(auto &step : SSA_step.io_args)
599  merge_irep(step);
600 
601  // converted_io_args is merged in convert_io
602 }
603 
604 void symex_target_equationt::output(std::ostream &out) const
605 {
606  for(const auto &step : SSA_steps)
607  {
608  step.output(ns, out);
609  out << "--------------\n";
610  }
611 }
612 
614  const namespacet &ns,
615  std::ostream &out) const
616 {
617  if(source.is_set)
618  {
619  out << "Thread " << source.thread_nr;
620 
621  if(source.pc->source_location.is_not_nil())
622  out << " " << source.pc->source_location << '\n';
623  else
624  out << '\n';
625  }
626 
627  switch(type)
628  {
630  out << "ASSERT " << from_expr(ns, "", cond_expr) << '\n'; break;
632  out << "ASSUME " << from_expr(ns, "", cond_expr) << '\n'; break;
634  out << "LOCATION" << '\n'; break;
636  out << "INPUT" << '\n'; break;
638  out << "OUTPUT" << '\n'; break;
639 
641  out << "DECL" << '\n';
642  out << from_expr(ns, "", ssa_lhs) << '\n';
643  break;
644 
646  out << "ASSIGNMENT (";
647  switch(assignment_type)
648  {
650  out << "HIDDEN";
651  break;
653  out << "STATE";
654  break;
656  out << "VISIBLE_ACTUAL_PARAMETER";
657  break;
659  out << "HIDDEN_ACTUAL_PARAMETER";
660  break;
662  out << "PHI";
663  break;
665  out << "GUARD";
666  break;
667  default:
668  {
669  }
670  }
671 
672  out << ")\n";
673  break;
674 
676  out << "DEAD\n"; break;
678  out << "FUNCTION_CALL\n"; break;
680  out << "FUNCTION_RETURN\n"; break;
682  out << "CONSTRAINT\n"; break;
684  out << "SHARED READ\n"; break;
686  out << "SHARED WRITE\n"; break;
688  out << "ATOMIC_BEGIN\n"; break;
690  out << "AUTOMIC_END\n"; break;
692  out << "SPAWN\n"; break;
694  out << "MEMORY_BARRIER\n"; break;
696  out << "IF " << from_expr(ns, "", cond_expr) << " GOTO\n"; break;
697 
698  default: assert(false);
699  }
700 
701  if(is_assert() || is_assume() || is_assignment() || is_constraint())
702  out << from_expr(ns, "", cond_expr) << '\n';
703 
704  if(is_assert() || is_constraint())
705  out << comment << '\n';
706 
708  out << from_expr(ns, "", ssa_lhs) << '\n';
709 
710  out << "Guard: " << from_expr(ns, "", guard) << '\n';
711 }
712 
713 std::ostream &operator<<(
714  std::ostream &out,
715  const symex_target_equationt &equation)
716 {
717  equation.output(out);
718  return out;
719 }
720 
721 std::ostream &operator<<(
722  std::ostream &out,
724 {
725  // may cause lookup failures, since it's blank
726  symbol_tablet symbol_table;
727  namespacet ns(symbol_table);
728  step.output(ns, out);
729  return out;
730 }
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:104
Generate Equation using Symbolic Execution.
void convert(prop_convt &prop_conv)
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:60
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end an atomic section
boolean implication
Definition: std_expr.h:1926
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:1082
The boolean constant true.
Definition: std_expr.h:3742
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
symex_target_equationt(const namespacet &_ns)
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
boolean AND
Definition: std_expr.h:1852
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
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
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:26
std::vector< exprt > operandst
Definition: expr.h:49
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:46
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)
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
virtual void location(const exprt &guard, const sourcet &source)
just record a location
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::ostream & operator<<(std::ostream &out, const symex_target_equationt &equation)
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)
unsigned count_assertions() const
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