cprover
goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_program.h"
13 
14 #include <ostream>
15 #include <iomanip>
16 
17 #include <util/std_expr.h>
18 
19 #include <langapi/language_util.h>
20 
35  const namespacet &ns,
36  const irep_idt &identifier,
37  std::ostream &out,
38  const instructiont &instruction) const
39 {
40  out << " // " << instruction.location_number << " ";
41 
42  if(!instruction.source_location.is_nil())
43  out << instruction.source_location.as_string();
44  else
45  out << "no location";
46 
47  out << "\n";
48 
49  if(!instruction.labels.empty())
50  {
51  out << " // Labels:";
52  for(const auto &label : instruction.labels)
53  out << " " << label;
54 
55  out << '\n';
56  }
57 
58  if(instruction.is_target())
59  out << std::setw(6) << instruction.target_number << ": ";
60  else
61  out << " ";
62 
63  switch(instruction.type)
64  {
66  out << "NO INSTRUCTION TYPE SET" << '\n';
67  break;
68 
69  case GOTO:
70  if(!instruction.guard.is_true())
71  {
72  out << "IF "
73  << from_expr(ns, identifier, instruction.guard)
74  << " THEN ";
75  }
76 
77  out << "GOTO ";
78 
79  for(instructiont::targetst::const_iterator
80  gt_it=instruction.targets.begin();
81  gt_it!=instruction.targets.end();
82  gt_it++)
83  {
84  if(gt_it!=instruction.targets.begin())
85  out << ", ";
86  out << (*gt_it)->target_number;
87  }
88 
89  out << '\n';
90  break;
91 
92  case RETURN:
93  case OTHER:
94  case DECL:
95  case DEAD:
96  case FUNCTION_CALL:
97  case ASSIGN:
98  out << from_expr(ns, identifier, instruction.code) << '\n';
99  break;
100 
101  case ASSUME:
102  case ASSERT:
103  if(instruction.is_assume())
104  out << "ASSUME ";
105  else
106  out << "ASSERT ";
107 
108  {
109  out << from_expr(ns, identifier, instruction.guard);
110 
111  const irep_idt &comment=instruction.source_location.get_comment();
112  if(comment!="")
113  out << " // " << comment;
114  }
115 
116  out << '\n';
117  break;
118 
119  case SKIP:
120  out << "SKIP" << '\n';
121  break;
122 
123  case END_FUNCTION:
124  out << "END_FUNCTION" << '\n';
125  break;
126 
127  case LOCATION:
128  out << "LOCATION" << '\n';
129  break;
130 
131  case THROW:
132  out << "THROW";
133 
134  {
135  const irept::subt &exception_list=
136  instruction.code.find(ID_exception_list).get_sub();
137 
138  for(const auto &ex : exception_list)
139  out << " " << ex.id();
140  }
141 
142  if(instruction.code.operands().size()==1)
143  out << ": " << from_expr(ns, identifier, instruction.code.op0());
144 
145  out << '\n';
146  break;
147 
148  case CATCH:
149  {
150  if(instruction.code.get_statement()==ID_exception_landingpad)
151  {
152  const auto &landingpad=to_code_landingpad(instruction.code);
153  out << "EXCEPTION LANDING PAD ("
154  << from_type(ns, identifier, landingpad.catch_expr().type())
155  << ' '
156  << from_expr(ns, identifier, landingpad.catch_expr())
157  << ")";
158  }
159  else if(instruction.code.get_statement()==ID_push_catch)
160  {
161  out << "CATCH-PUSH ";
162 
163  unsigned i=0;
164  const irept::subt &exception_list=
165  instruction.code.find(ID_exception_list).get_sub();
166  DATA_INVARIANT(instruction.targets.size()==exception_list.size(),
167  "size of target list");
168  for(instructiont::targetst::const_iterator
169  gt_it=instruction.targets.begin();
170  gt_it!=instruction.targets.end();
171  gt_it++, i++)
172  {
173  if(gt_it!=instruction.targets.begin())
174  out << ", ";
175  out << exception_list[i].id() << "->"
176  << (*gt_it)->target_number;
177  }
178  }
179  else if(instruction.code.get_statement()==ID_pop_catch)
180  {
181  out << "CATCH-POP";
182  }
183  else
184  {
185  UNREACHABLE;
186  }
187 
188  out << '\n';
189  break;
190  }
191 
192  case ATOMIC_BEGIN:
193  out << "ATOMIC_BEGIN" << '\n';
194  break;
195 
196  case ATOMIC_END:
197  out << "ATOMIC_END" << '\n';
198  break;
199 
200  case START_THREAD:
201  out << "START THREAD "
202  << instruction.get_target()->target_number
203  << '\n';
204  break;
205 
206  case END_THREAD:
207  out << "END THREAD" << '\n';
208  break;
209 
210  default:
211  throw "unknown statement";
212  }
213 
214  return out;
215 }
216 
218  decl_identifierst &decl_identifiers) const
219 {
221  {
222  if(it->is_decl())
223  {
224  DATA_INVARIANT(it->code.get_statement()==ID_decl,
225  "declaration statements");
226  DATA_INVARIANT(it->code.operands().size()==1,
227  "operand of declaration statement");
228  const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
229  decl_identifiers.insert(symbol_expr.get_identifier());
230  }
231  }
232 }
233 
234 void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
235 {
236  if(src.id()==ID_dereference)
237  {
238  assert(src.operands().size()==1);
239  dest.push_back(src.op0());
240  }
241  else if(src.id()==ID_index)
242  {
243  assert(src.operands().size()==2);
244  dest.push_back(src.op1());
245  parse_lhs_read(src.op0(), dest);
246  }
247  else if(src.id()==ID_member)
248  {
249  assert(src.operands().size()==1);
250  parse_lhs_read(src.op0(), dest);
251  }
252  else if(src.id()==ID_if)
253  {
254  assert(src.operands().size()==3);
255  dest.push_back(src.op0());
256  parse_lhs_read(src.op1(), dest);
257  parse_lhs_read(src.op2(), dest);
258  }
259 }
260 
261 std::list<exprt> expressions_read(
262  const goto_programt::instructiont &instruction)
263 {
264  std::list<exprt> dest;
265 
266  switch(instruction.type)
267  {
268  case ASSUME:
269  case ASSERT:
270  case GOTO:
271  dest.push_back(instruction.guard);
272  break;
273 
274  case RETURN:
275  if(to_code_return(instruction.code).return_value().is_not_nil())
276  dest.push_back(to_code_return(instruction.code).return_value());
277  break;
278 
279  case FUNCTION_CALL:
280  {
281  const code_function_callt &function_call=
282  to_code_function_call(instruction.code);
283  forall_expr(it, function_call.arguments())
284  dest.push_back(*it);
285  if(function_call.lhs().is_not_nil())
286  parse_lhs_read(function_call.lhs(), dest);
287  }
288  break;
289 
290  case ASSIGN:
291  {
292  const code_assignt &assignment=to_code_assign(instruction.code);
293  dest.push_back(assignment.rhs());
294  parse_lhs_read(assignment.lhs(), dest);
295  }
296  break;
297 
298  default:
299  {
300  }
301  }
302 
303  return dest;
304 }
305 
306 std::list<exprt> expressions_written(
307  const goto_programt::instructiont &instruction)
308 {
309  std::list<exprt> dest;
310 
311  switch(instruction.type)
312  {
313  case FUNCTION_CALL:
314  {
315  const code_function_callt &function_call=
316  to_code_function_call(instruction.code);
317  if(function_call.lhs().is_not_nil())
318  dest.push_back(function_call.lhs());
319  }
320  break;
321 
322  case ASSIGN:
323  dest.push_back(to_code_assign(instruction.code).lhs());
324  break;
325 
326  default:
327  {
328  }
329  }
330 
331  return dest;
332 }
333 
335  const exprt &src,
336  std::list<exprt> &dest)
337 {
338  if(src.id()==ID_symbol)
339  dest.push_back(src);
340  else if(src.id()==ID_address_of)
341  {
342  // don't traverse!
343  }
344  else if(src.id()==ID_dereference)
345  {
346  // this reads what is pointed to plus the pointer
347  assert(src.operands().size()==1);
348  dest.push_back(src);
349  objects_read(src.op0(), dest);
350  }
351  else
352  {
353  forall_operands(it, src)
354  objects_read(*it, dest);
355  }
356 }
357 
358 std::list<exprt> objects_read(
359  const goto_programt::instructiont &instruction)
360 {
361  std::list<exprt> expressions=expressions_read(instruction);
362 
363  std::list<exprt> dest;
364 
365  for(const auto &expr : expressions)
366  objects_read(expr, dest);
367 
368  return dest;
369 }
370 
372  const exprt &src,
373  std::list<exprt> &dest)
374 {
375  if(src.id()==ID_if)
376  {
377  assert(src.operands().size()==3);
378  objects_written(src.op1(), dest);
379  objects_written(src.op2(), dest);
380  }
381  else
382  dest.push_back(src);
383 }
384 
385 std::list<exprt> objects_written(
386  const goto_programt::instructiont &instruction)
387 {
388  std::list<exprt> expressions=expressions_written(instruction);
389 
390  std::list<exprt> dest;
391 
392  for(const auto &expr : expressions)
393  objects_written(expr, dest);
394 
395  return dest;
396 }
397 
398 std::string as_string(
399  const class namespacet &ns,
401 {
402  std::string result;
403 
404  switch(i.type)
405  {
406  case NO_INSTRUCTION_TYPE:
407  return "(NO INSTRUCTION TYPE)";
408 
409  case GOTO:
410  if(!i.guard.is_true())
411  {
412  result+="IF "
413  +from_expr(ns, i.function, i.guard)
414  +" THEN ";
415  }
416 
417  result+="GOTO ";
418 
419  for(goto_programt::instructiont::targetst::const_iterator
420  gt_it=i.targets.begin();
421  gt_it!=i.targets.end();
422  gt_it++)
423  {
424  if(gt_it!=i.targets.begin())
425  result+=", ";
426  result+=std::to_string((*gt_it)->target_number);
427  }
428  return result;
429 
430  case RETURN:
431  case OTHER:
432  case DECL:
433  case DEAD:
434  case FUNCTION_CALL:
435  case ASSIGN:
436  return from_expr(ns, i.function, i.code);
437 
438  case ASSUME:
439  case ASSERT:
440  if(i.is_assume())
441  result+="ASSUME ";
442  else
443  result+="ASSERT ";
444 
445  result+=from_expr(ns, i.function, i.guard);
446 
447  {
449  if(comment!="")
450  result+=" /* "+id2string(comment)+" */";
451  }
452  return result;
453 
454  case SKIP:
455  return "SKIP";
456 
457  case END_FUNCTION:
458  return "END_FUNCTION";
459 
460  case LOCATION:
461  return "LOCATION";
462 
463  case THROW:
464  return "THROW";
465 
466  case CATCH:
467  return "CATCH";
468 
469  case ATOMIC_BEGIN:
470  return "ATOMIC_BEGIN";
471 
472  case ATOMIC_END:
473  return "ATOMIC_END";
474 
475  case START_THREAD:
476  result+="START THREAD ";
477 
478  if(i.targets.size()==1)
479  result+=std::to_string(i.targets.front()->target_number);
480  return result;
481 
482  case END_THREAD:
483  return "END THREAD";
484 
485  default:
486  throw "unknown statement";
487  }
488 }
489 
491 {
492  unsigned nr=0;
493  for(auto &i : instructions)
494  if(i.is_backwards_goto())
495  i.loop_number=nr++;
496 }
497 
499 {
504 }
505 
506 std::ostream &goto_programt::output(
507  const namespacet &ns,
508  const irep_idt &identifier,
509  std::ostream &out) const
510 {
511  // output program
512 
513  for(const auto &instruction : instructions)
514  output_instruction(ns, identifier, out, instruction);
515 
516  return out;
517 }
518 
520 {
521  // reset marking
522 
523  for(auto &i : instructions)
524  i.target_number=instructiont::nil_target;
525 
526  // mark the goto targets
527 
528  for(const auto &i : instructions)
529  {
530  for(const auto &t : i.targets)
531  {
532  if(t!=instructions.end())
533  t->target_number=0;
534  }
535  }
536 
537  // number the targets properly
538  unsigned cnt=0;
539 
540  for(auto &i : instructions)
541  {
542  if(i.is_target())
543  {
544  i.target_number=++cnt;
545  DATA_INVARIANT(i.target_number!=0, "target numbers");
546  }
547  }
548 
549  // check the targets!
550  // (this is a consistency check only)
551 
552  for(const auto &i : instructions)
553  {
554  for(const auto &t : i.targets)
555  {
556  if(t!=instructions.end())
557  {
558  DATA_INVARIANT(t->target_number!=0,
559  "target numbers");
560  DATA_INVARIANT(t->target_number!=instructiont::nil_target,
561  "target numbers");
562  }
563  }
564  }
565 }
566 
568 {
569  // Definitions for mapping between the two programs
570  typedef std::map<const_targett, targett> targets_mappingt;
571  targets_mappingt targets_mapping;
572 
573  clear();
574 
575  // Loop over program - 1st time collects targets and copy
576 
577  for(instructionst::const_iterator
578  it=src.instructions.begin();
579  it!=src.instructions.end();
580  ++it)
581  {
582  auto new_instruction=add_instruction();
583  targets_mapping[it]=new_instruction;
584  *new_instruction=*it;
585  }
586 
587  // Loop over program - 2nd time updates targets
588 
589  for(auto &i : instructions)
590  {
591  for(auto &t : i.targets)
592  {
593  targets_mappingt::iterator
594  m_target_it=targets_mapping.find(t);
595 
596  if(m_target_it==targets_mapping.end())
597  throw "copy_from: target not found";
598 
599  t=m_target_it->second;
600  }
601  }
602 
605 }
606 
607 // number them
609 {
610  for(const auto &i : instructions)
611  if(i.is_assert() && !i.guard.is_true())
612  return true;
613 
614  return false;
615 }
616 
618 {
619  for(auto &i : instructions)
620  {
621  i.incoming_edges.clear();
622  }
623 
624  for(instructionst::iterator
625  it=instructions.begin();
626  it!=instructions.end();
627  ++it)
628  {
629  for(const auto &s : get_successors(it))
630  {
631  if(s!=instructions.end())
632  s->incoming_edges.insert(it);
633  }
634  }
635 }
636 
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
const irep_idt & get_statement() const
Definition: std_code.h:39
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
void update()
Update all indices.
const exprt & return_value() const
Definition: std_code.h:907
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
void compute_loop_numbers()
Compute loop numbers.
exprt & op0()
Definition: expr.h:72
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:364
std::vector< irept > subt
Definition: irep.h:90
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
#define forall_expr(it, expr)
Definition: expr.h:28
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool has_assertion() const
Does the goto program have an assertion?
bool is_true() const
Definition: expr.cpp:124
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:357
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:202
subt & get_sub()
Definition: irep.h:245
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void clear()
Clear the goto program.
Definition: goto_program.h:611
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:371
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:640
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
argumentst & arguments()
Definition: std_code.h:860
void compute_incoming_edges()
exprt & rhs()
Definition: std_code.h:213
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
exprt & op1()
Definition: expr.h:75
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:933
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
void objects_read(const exprt &src, std::list< exprt > &dest)
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:570
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1607
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
void compute_target_numbers()
Compute the target numbers.
#define UNREACHABLE
Definition: invariant.h:250
void objects_written(const exprt &src, std::list< exprt > &dest)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
const irep_idt & get_comment() const
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:229
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Concrete Goto Program.
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879