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 
16 #include <util/std_expr.h>
17 
18 #include <langapi/language_util.h>
19 
28  const class namespacet &ns,
29  const irep_idt &identifier,
30  std::ostream &out,
31  instructionst::const_iterator it) const
32 {
33  return output_instruction(ns, identifier, out, *it);
34 }
35 
50  const namespacet &ns,
51  const irep_idt &identifier,
52  std::ostream &out,
53  const goto_program_templatet::instructiont &instruction) const
54 {
55  out << " // " << instruction.location_number << " ";
56 
57  if(!instruction.source_location.is_nil())
58  out << instruction.source_location.as_string();
59  else
60  out << "no location";
61 
62  out << "\n";
63 
64  if(!instruction.labels.empty())
65  {
66  out << " // Labels:";
67  for(const auto &label : instruction.labels)
68  out << " " << label;
69 
70  out << '\n';
71  }
72 
73  if(instruction.is_target())
74  out << std::setw(6) << instruction.target_number << ": ";
75  else
76  out << " ";
77 
78  switch(instruction.type)
79  {
81  out << "NO INSTRUCTION TYPE SET" << '\n';
82  break;
83 
84  case GOTO:
85  if(!instruction.guard.is_true())
86  {
87  out << "IF "
88  << from_expr(ns, identifier, instruction.guard)
89  << " THEN ";
90  }
91 
92  out << "GOTO ";
93 
94  for(instructiont::targetst::const_iterator
95  gt_it=instruction.targets.begin();
96  gt_it!=instruction.targets.end();
97  gt_it++)
98  {
99  if(gt_it!=instruction.targets.begin())
100  out << ", ";
101  out << (*gt_it)->target_number;
102  }
103 
104  out << '\n';
105  break;
106 
107  case RETURN:
108  case OTHER:
109  case DECL:
110  case DEAD:
111  case FUNCTION_CALL:
112  case ASSIGN:
113  out << from_expr(ns, identifier, instruction.code) << '\n';
114  break;
115 
116  case ASSUME:
117  case ASSERT:
118  if(instruction.is_assume())
119  out << "ASSUME ";
120  else
121  out << "ASSERT ";
122 
123  {
124  out << from_expr(ns, identifier, instruction.guard);
125 
126  const irep_idt &comment=instruction.source_location.get_comment();
127  if(comment!="")
128  out << " // " << comment;
129  }
130 
131  out << '\n';
132  break;
133 
134  case SKIP:
135  out << "SKIP" << '\n';
136  break;
137 
138  case END_FUNCTION:
139  out << "END_FUNCTION" << '\n';
140  break;
141 
142  case LOCATION:
143  out << "LOCATION" << '\n';
144  break;
145 
146  case THROW:
147  out << "THROW";
148 
149  {
150  const irept::subt &exception_list=
151  instruction.code.find(ID_exception_list).get_sub();
152 
153  for(const auto &ex : exception_list)
154  out << " " << ex.id();
155  }
156 
157  if(instruction.code.operands().size()==1)
158  out << ": " << from_expr(ns, identifier, instruction.code.op0());
159 
160  out << '\n';
161  break;
162 
163  case CATCH:
164  if(!instruction.targets.empty())
165  {
166  out << "CATCH-PUSH ";
167 
168  unsigned i=0;
169  const irept::subt &exception_list=
170  instruction.code.find(ID_exception_list).get_sub();
171  assert(instruction.targets.size()==exception_list.size());
172  for(instructiont::targetst::const_iterator
173  gt_it=instruction.targets.begin();
174  gt_it!=instruction.targets.end();
175  gt_it++,
176  i++)
177  {
178  if(gt_it!=instruction.targets.begin())
179  out << ", ";
180  out << exception_list[i].id() << "->"
181  << (*gt_it)->target_number;
182  }
183  }
184  else
185  out << "CATCH-POP";
186 
187  out << '\n';
188  break;
189 
190  case ATOMIC_BEGIN:
191  out << "ATOMIC_BEGIN" << '\n';
192  break;
193 
194  case ATOMIC_END:
195  out << "ATOMIC_END" << '\n';
196  break;
197 
198  case START_THREAD:
199  out << "START THREAD ";
200 
201  if(instruction.targets.size()==1)
202  out << instruction.targets.front()->target_number;
203 
204  out << '\n';
205  break;
206 
207  case END_THREAD:
208  out << "END THREAD" << '\n';
209  break;
210 
211  default:
212  throw "unknown statement";
213  }
214 
215  return out;
216 }
217 
219  decl_identifierst &decl_identifiers) const
220 {
222  {
223  if(it->is_decl())
224  {
225  assert(it->code.get_statement()==ID_decl);
226  assert(it->code.operands().size()==1);
227  const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
228  decl_identifiers.insert(symbol_expr.get_identifier());
229  }
230  }
231 }
232 
233 void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
234 {
235  if(src.id()==ID_dereference)
236  {
237  assert(src.operands().size()==1);
238  dest.push_back(src.op0());
239  }
240  else if(src.id()==ID_index)
241  {
242  assert(src.operands().size()==2);
243  dest.push_back(src.op1());
244  parse_lhs_read(src.op0(), dest);
245  }
246  else if(src.id()==ID_member)
247  {
248  assert(src.operands().size()==1);
249  parse_lhs_read(src.op0(), dest);
250  }
251  else if(src.id()==ID_if)
252  {
253  assert(src.operands().size()==3);
254  dest.push_back(src.op0());
255  parse_lhs_read(src.op1(), dest);
256  parse_lhs_read(src.op2(), dest);
257  }
258 }
259 
260 std::list<exprt> expressions_read(
261  const goto_programt::instructiont &instruction)
262 {
263  std::list<exprt> dest;
264 
265  switch(instruction.type)
266  {
267  case ASSUME:
268  case ASSERT:
269  case GOTO:
270  dest.push_back(instruction.guard);
271  break;
272 
273  case RETURN:
274  if(to_code_return(instruction.code).return_value().is_not_nil())
275  dest.push_back(to_code_return(instruction.code).return_value());
276  break;
277 
278  case FUNCTION_CALL:
279  {
280  const code_function_callt &function_call=
281  to_code_function_call(instruction.code);
282  forall_expr(it, function_call.arguments())
283  dest.push_back(*it);
284  if(function_call.lhs().is_not_nil())
285  parse_lhs_read(function_call.lhs(), dest);
286  }
287  break;
288 
289  case ASSIGN:
290  {
291  const code_assignt &assignment=to_code_assign(instruction.code);
292  dest.push_back(assignment.rhs());
293  parse_lhs_read(assignment.lhs(), dest);
294  }
295  break;
296 
297  default:
298  {
299  }
300  }
301 
302  return dest;
303 }
304 
305 std::list<exprt> expressions_written(
306  const goto_programt::instructiont &instruction)
307 {
308  std::list<exprt> dest;
309 
310  switch(instruction.type)
311  {
312  case FUNCTION_CALL:
313  {
314  const code_function_callt &function_call=
315  to_code_function_call(instruction.code);
316  if(function_call.lhs().is_not_nil())
317  dest.push_back(function_call.lhs());
318  }
319  break;
320 
321  case ASSIGN:
322  dest.push_back(to_code_assign(instruction.code).lhs());
323  break;
324 
325  default:
326  {
327  }
328  }
329 
330  return dest;
331 }
332 
334  const exprt &src,
335  std::list<exprt> &dest)
336 {
337  if(src.id()==ID_symbol)
338  dest.push_back(src);
339  else if(src.id()==ID_address_of)
340  {
341  // don't traverse!
342  }
343  else if(src.id()==ID_dereference)
344  {
345  // this reads what is pointed to plus the pointer
346  assert(src.operands().size()==1);
347  dest.push_back(src);
348  objects_read(src.op0(), dest);
349  }
350  else
351  {
352  forall_operands(it, src)
353  objects_read(*it, dest);
354  }
355 }
356 
357 std::list<exprt> objects_read(
358  const goto_programt::instructiont &instruction)
359 {
360  std::list<exprt> expressions=expressions_read(instruction);
361 
362  std::list<exprt> dest;
363 
364  forall_expr_list(it, expressions)
365  objects_read(*it, dest);
366 
367  return dest;
368 }
369 
371  const exprt &src,
372  std::list<exprt> &dest)
373 {
374  if(src.id()==ID_if)
375  {
376  assert(src.operands().size()==3);
377  objects_written(src.op1(), dest);
378  objects_written(src.op2(), dest);
379  }
380  else
381  dest.push_back(src);
382 }
383 
384 std::list<exprt> objects_written(
385  const goto_programt::instructiont &instruction)
386 {
387  std::list<exprt> expressions=expressions_written(instruction);
388 
389  std::list<exprt> dest;
390 
391  forall_expr_list(it, expressions)
392  objects_written(*it, dest);
393 
394  return dest;
395 }
396 
397 std::string as_string(
398  const class namespacet &ns,
399  const goto_programt::instructiont &i)
400 {
401  std::string result;
402 
403  switch(i.type)
404  {
405  case NO_INSTRUCTION_TYPE:
406  return "(NO INSTRUCTION TYPE)";
407 
408  case GOTO:
409  if(!i.guard.is_true())
410  {
411  result+="IF "
412  +from_expr(ns, i.function, i.guard)
413  +" THEN ";
414  }
415 
416  result+="GOTO ";
417 
418  for(goto_programt::instructiont::targetst::const_iterator
419  gt_it=i.targets.begin();
420  gt_it!=i.targets.end();
421  gt_it++)
422  {
423  if(gt_it!=i.targets.begin())
424  result+=", ";
425  result+=std::to_string((*gt_it)->target_number);
426  }
427  return result;
428 
429  case RETURN:
430  case OTHER:
431  case DECL:
432  case DEAD:
433  case FUNCTION_CALL:
434  case ASSIGN:
435  return from_expr(ns, i.function, i.code);
436 
437  case ASSUME:
438  case ASSERT:
439  if(i.is_assume())
440  result+="ASSUME ";
441  else
442  result+="ASSERT ";
443 
444  result+=from_expr(ns, i.function, i.guard);
445 
446  {
447  const irep_idt &comment=i.source_location.get_comment();
448  if(comment!="")
449  result+=" /* "+id2string(comment)+" */";
450  }
451  return result;
452 
453  case SKIP:
454  return "SKIP";
455 
456  case END_FUNCTION:
457  return "END_FUNCTION";
458 
459  case LOCATION:
460  return "LOCATION";
461 
462  case THROW:
463  return "THROW";
464 
465  case CATCH:
466  return "CATCH";
467 
468  case ATOMIC_BEGIN:
469  return "ATOMIC_BEGIN";
470 
471  case ATOMIC_END:
472  return "ATOMIC_END";
473 
474  case START_THREAD:
475  result+="START THREAD ";
476 
477  if(i.targets.size()==1)
478  result+=std::to_string(i.targets.front()->target_number);
479  return result;
480 
481  case END_THREAD:
482  return "END THREAD";
483 
484  default:
485  throw "unknown statement";
486  }
487 
488  return "";
489 }
const exprt & return_value() const
Definition: std_code.h:728
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
unsigned target_number
A number to identify branch targets.
exprt & op0()
Definition: expr.h:84
std::vector< irept > subt
Definition: irep.h:91
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:115
goto_program_instruction_typet type
What kind of instruction?
#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)
This class represents an instruction in the GOTO intermediate representation.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:64
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
argumentst & arguments()
Definition: std_code.h:689
exprt & rhs()
Definition: std_code.h:162
API to expression classes.
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
void objects_read(const exprt &src, std::list< exprt > &dest)
#define forall_expr_list(it, expr)
Definition: expr.h:36
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
unsigned location_number
A globally unique number to identify a program location.
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
guardT guard
Guard for gotos, assume, assert.
void objects_written(const exprt &src, std::list< exprt > &dest)
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
source_locationt source_location
The location of the instruction in the source file.
const irep_idt & get_comment() const
operandst & operands()
Definition: expr.h:70
targetst targets
The list of successor instructions.
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
Concrete Goto Program.
Assignment.
Definition: std_code.h:144
bool is_target() const
Is this node a branch target?
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700