cprover
interpreter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interpreter for GOTO Programs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "interpreter.h"
13 
14 #include <cctype>
15 #include <cstdio>
16 #include <iostream>
17 #include <algorithm>
18 
19 #include <util/std_types.h>
20 #include <util/symbol_table.h>
21 
22 #include "interpreter_class.h"
23 
25 {
27 
28  const goto_functionst::function_mapt::const_iterator
30 
31  if(main_it==goto_functions.function_map.end())
32  throw "main not found";
33 
34  const goto_functionst::goto_functiont &goto_function=main_it->second;
35 
36  if(!goto_function.body_available())
37  throw "main has no body";
38 
39  PC=goto_function.body.instructions.begin();
40  function=main_it;
41 
42  done=false;
43 
44  while(!done)
45  {
46  show_state();
47  command();
48  if(!done)
49  step();
50  }
51 }
52 
54 {
55  std::cout << "\n----------------------------------------------------\n";
56 
57  if(PC==function->second.body.instructions.end())
58  {
59  std::cout << "End of function `"
60  << function->first << "'\n";
61  }
62  else
63  function->second.body.output_instruction(
64  ns, function->first, std::cout, PC);
65 
66  std::cout << '\n';
67 }
68 
70 {
71  #define BUFSIZE 100
72  char command[BUFSIZE];
73  if(fgets(command, BUFSIZE-1, stdin)==nullptr)
74  {
75  done=true;
76  return;
77  }
78 
79  char ch=tolower(command[0]);
80 
81  if(ch=='q')
82  done=true;
83 }
84 
86 {
87  if(PC==function->second.body.instructions.end())
88  {
89  if(call_stack.empty())
90  done=true;
91  else
92  {
93  PC=call_stack.top().return_PC;
94  function=call_stack.top().return_function;
95  stack_pointer=call_stack.top().old_stack_pointer;
96  call_stack.pop();
97  }
98 
99  return;
100  }
101 
102  next_PC=PC;
103  next_PC++;
104 
105  switch(PC->type)
106  {
107  case GOTO:
108  execute_goto();
109  break;
110 
111  case ASSUME:
112  execute_assume();
113  break;
114 
115  case ASSERT:
116  execute_assert();
117  break;
118 
119  case OTHER:
120  execute_other();
121  break;
122 
123  case DECL:
124  execute_decl();
125  break;
126 
127  case SKIP:
128  case LOCATION:
129  case END_FUNCTION:
130  break;
131 
132  case RETURN:
133  if(call_stack.empty())
134  throw "RETURN without call"; // NOLINT(readability/throw)
135 
136  if(PC->code.operands().size()==1 &&
137  call_stack.top().return_value_address!=0)
138  {
139  std::vector<mp_integer> rhs;
140  evaluate(PC->code.op0(), rhs);
141  assign(call_stack.top().return_value_address, rhs);
142  }
143 
144  next_PC=function->second.body.instructions.end();
145  break;
146 
147  case ASSIGN:
148  execute_assign();
149  break;
150 
151  case FUNCTION_CALL:
153  break;
154 
155  case START_THREAD:
156  throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
157 
158  case END_THREAD:
159  throw "END_THREAD not yet implemented"; // NOLINT(readability/throw)
160  break;
161 
162  case ATOMIC_BEGIN:
163  throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw)
164 
165  case ATOMIC_END:
166  throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw)
167 
168  case DEAD:
169  throw "DEAD not yet implemented"; // NOLINT(readability/throw)
170 
171  default:
172  throw "encountered instruction with undefined instruction type";
173  }
174 
175  PC=next_PC;
176 }
177 
179 {
180  if(evaluate_boolean(PC->guard))
181  {
182  if(PC->targets.empty())
183  throw "taken goto without target";
184 
185  if(PC->targets.size()>=2)
186  throw "non-deterministic goto encountered";
187 
188  next_PC=PC->targets.front();
189  }
190 }
191 
193 {
194  const irep_idt &statement=PC->code.get_statement();
195 
196  if(statement==ID_expression)
197  {
198  assert(PC->code.operands().size()==1);
199  std::vector<mp_integer> rhs;
200  evaluate(PC->code.op0(), rhs);
201  }
202  else
203  throw "unexpected OTHER statement: "+id2string(statement);
204 }
205 
207 {
208  assert(PC->code.get_statement()==ID_decl);
209 }
210 
212 {
213  const code_assignt &code_assign=
214  to_code_assign(PC->code);
215 
216  std::vector<mp_integer> rhs;
217  evaluate(code_assign.rhs(), rhs);
218 
219  if(!rhs.empty())
220  {
221  mp_integer address=evaluate_address(code_assign.lhs());
222  unsigned size=get_size(code_assign.lhs().type());
223 
224  if(size!=rhs.size())
225  std::cout << "!! failed to obtain rhs ("
226  << rhs.size() << " vs. "
227  << size << ")\n";
228  else
229  assign(address, rhs);
230  }
231 }
232 
234  mp_integer address,
235  const std::vector<mp_integer> &rhs)
236 {
237  for(unsigned i=0; i<rhs.size(); i++, ++address)
238  {
239  if(address<memory.size())
240  {
241  memory_cellt &cell=memory[integer2unsigned(address)];
242  std::cout << "** assigning " << cell.identifier
243  << "[" << cell.offset << "]:=" << rhs[i] << '\n';
244  cell.value=rhs[i];
245  }
246  }
247 }
248 
250 {
251  if(!evaluate_boolean(PC->guard))
252  throw "assumption failed";
253 }
254 
256 {
257  if(!evaluate_boolean(PC->guard))
258  throw "assertion failed";
259 }
260 
262 {
263  const code_function_callt &function_call=
264  to_code_function_call(PC->code);
265 
266  // function to be called
267  mp_integer a=evaluate_address(function_call.function());
268 
269  if(a==0)
270  throw "function call to NULL";
271  else if(a>=memory.size())
272  throw "out-of-range function call";
273 
274  const memory_cellt &cell=memory[integer2size_t(a)];
275  const irep_idt &identifier=cell.identifier;
276 
277  const goto_functionst::function_mapt::const_iterator f_it=
278  goto_functions.function_map.find(identifier);
279 
280  if(f_it==goto_functions.function_map.end())
281  throw "failed to find function "+id2string(identifier);
282 
283  // return value
284  mp_integer return_value_address;
285 
286  if(function_call.lhs().is_not_nil())
287  return_value_address=
288  evaluate_address(function_call.lhs());
289  else
290  return_value_address=0;
291 
292  // values of the arguments
293  std::vector<std::vector<mp_integer> > argument_values;
294 
295  argument_values.resize(function_call.arguments().size());
296 
297  for(std::size_t i=0; i<function_call.arguments().size(); i++)
298  evaluate(function_call.arguments()[i], argument_values[i]);
299 
300  // do the call
301 
302  if(f_it->second.body_available())
303  {
304  call_stack.push(stack_framet());
305  stack_framet &frame=call_stack.top();
306 
307  frame.return_PC=next_PC;
308  frame.return_function=function;
310  frame.return_value_address=return_value_address;
311 
312  // local variables
313  std::set<irep_idt> locals;
314  get_local_identifiers(f_it->second, locals);
315 
316  for(const auto &id : locals)
317  {
318  const symbolt &symbol=ns.lookup(id);
319  unsigned size=get_size(symbol.type);
320 
321  if(size!=0)
322  {
323  frame.local_map[id]=stack_pointer;
324 
325  for(unsigned i=0; i<stack_pointer; i++)
326  {
327  unsigned address=stack_pointer+i;
328  if(address>=memory.size())
329  memory.resize(address+1);
330  memory[address].value=0;
331  memory[address].identifier=id;
332  memory[address].offset=i;
333  }
334 
335  stack_pointer+=size;
336  }
337  }
338 
339  // assign the arguments
340  const code_typet::parameterst &parameters=
341  to_code_type(f_it->second.type).parameters();
342 
343  if(argument_values.size()<parameters.size())
344  throw "not enough arguments";
345 
346  for(unsigned i=0; i<parameters.size(); i++)
347  {
348  const code_typet::parametert &a=parameters[i];
349  exprt symbol_expr(ID_symbol, a.type());
350  symbol_expr.set(ID_identifier, a.get_identifier());
351  assert(i<argument_values.size());
352  assign(evaluate_address(symbol_expr), argument_values[i]);
353  }
354 
355  // set up new PC
356  function=f_it;
357  next_PC=f_it->second.body.instructions.begin();
358  }
359  else
360  throw "no body for "+id2string(identifier);
361 }
362 
364 {
365  // put in a dummy for NULL
366  memory.resize(1);
367  memory[0].offset=0;
368  memory[0].identifier="NULL-OBJECT";
369 
370  // now do regular static symbols
371  for(const auto &s : symbol_table.symbols)
372  build_memory_map(s.second);
373 
374  // for the locals
375  stack_pointer=memory.size();
376 }
377 
379 {
380  unsigned size=0;
381 
382  if(symbol.type.id()==ID_code)
383  {
384  size=1;
385  }
386  else if(symbol.is_static_lifetime)
387  {
388  size=get_size(symbol.type);
389  }
390 
391  if(size!=0)
392  {
393  unsigned address=memory.size();
394  memory.resize(address+size);
395  memory_map[symbol.name]=address;
396 
397  for(unsigned i=0; i<size; i++)
398  {
399  memory_cellt &cell=memory[address+i];
400  cell.identifier=symbol.name;
401  cell.offset=i;
402  cell.value=0;
403  }
404  }
405 }
406 
407 unsigned interpretert::get_size(const typet &type) const
408 {
409  if(type.id()==ID_struct)
410  {
411  const struct_typet::componentst &components=
412  to_struct_type(type).components();
413 
414  unsigned sum=0;
415 
416  for(const auto &comp : components)
417  {
418  const typet &sub_type=comp.type();
419 
420  if(sub_type.id()!=ID_code)
421  sum+=get_size(sub_type);
422  }
423 
424  return sum;
425  }
426  else if(type.id()==ID_union)
427  {
428  const union_typet::componentst &components=
429  to_union_type(type).components();
430 
431  unsigned max_size=0;
432 
433  for(const auto &comp : components)
434  {
435  const typet &sub_type=comp.type();
436 
437  if(sub_type.id()!=ID_code)
438  max_size=std::max(max_size, get_size(sub_type));
439  }
440 
441  return max_size;
442  }
443  else if(type.id()==ID_array)
444  {
445  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
446 
447  unsigned subtype_size=get_size(type.subtype());
448 
449  mp_integer i;
450  if(!to_integer(size_expr, i))
451  return subtype_size*integer2unsigned(i);
452  else
453  return subtype_size;
454  }
455  else if(type.id()==ID_symbol)
456  {
457  return get_size(ns.follow(type));
458  }
459  else
460  return 1;
461 }
462 
464  const symbol_tablet &symbol_table,
465  const goto_functionst &goto_functions)
466 {
467  interpretert interpreter(symbol_table, goto_functions);
468  interpreter();
469 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
void execute_goto()
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
goto_programt::const_targett PC
goto_programt::const_targett next_PC
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
std::vector< componentt > componentst
Definition: std_types.h:240
std::vector< parametert > parameterst
Definition: std_types.h:829
const componentst & components() const
Definition: std_types.h:242
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
typet & type()
Definition: expr.h:60
Interpreter for GOTO Programs.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
Interpreter for GOTO Programs.
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
void execute_assert()
goto_functionst::function_mapt::const_iterator function
exprt & rhs()
Definition: std_code.h:162
const goto_functionst & goto_functions
std::size_t stack_pointer
void execute_decl()
void show_state()
Definition: interpreter.cpp:53
void operator()()
Definition: interpreter.cpp:24
The symbol table.
Definition: symbol_table.h:52
void execute_assume()
A function call.
Definition: std_code.h:657
bool evaluate_boolean(const exprt &expr) const
void execute_assign()
Symbol table.
#define BUFSIZE
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const symbol_tablet & symbol_table
unsigned get_size(const typet &type) const
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
void assign(mp_integer address, const std::vector< mp_integer > &rhs)
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
const namespacet ns
goto_functionst::function_mapt::const_iterator return_function
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
void build_memory_map()
mp_integer evaluate_address(const exprt &expr) const
memory_mapt memory_map
call_stackt call_stack
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void interpreter(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
void command()
Definition: interpreter.cpp:69
goto_programt::const_targett return_PC
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:31
void execute_other()
const irep_idt & get_identifier() const
Definition: std_types.h:782
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void execute_function_call()
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700