cprover
interpreter_class.h
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 #ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
13 #define CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
14 
15 #include <stack>
16 
17 #include <util/arith_tools.h>
18 
19 #include "goto_functions.h"
20 
22 {
23 public:
25  const symbol_tablet &_symbol_table,
26  const goto_functionst &_goto_functions):
27  symbol_table(_symbol_table),
28  ns(_symbol_table),
29  goto_functions(_goto_functions)
30  {
31  }
32 
33  void operator()();
34 
35 protected:
37  const namespacet ns;
39 
40  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> memory_mapt;
41  memory_mapt memory_map;
42 
44  {
45  public:
47  unsigned offset;
49  };
50 
51  typedef std::vector<memory_cellt> memoryt;
52  memoryt memory;
53 
54  std::size_t stack_pointer;
55 
56  void build_memory_map();
57  void build_memory_map(const symbolt &symbol);
58  unsigned get_size(const typet &type) const;
59  void step();
60 
61  void execute_assert();
62  void execute_assume();
63  void execute_assign();
64  void execute_goto();
65  void execute_function_call();
66  void execute_other();
67  void execute_decl();
68 
69  void assign(
70  mp_integer address,
71  const std::vector<mp_integer> &rhs);
72 
73  void read(
74  mp_integer address,
75  std::vector<mp_integer> &dest) const;
76 
77  void command();
78 
80  {
81  public:
83  goto_functionst::function_mapt::const_iterator return_function;
85  memory_mapt local_map;
87  };
88 
89  typedef std::stack<stack_framet> call_stackt;
90  call_stackt call_stack;
91 
92  goto_functionst::function_mapt::const_iterator function;
94  bool done;
95 
96  bool evaluate_boolean(const exprt &expr) const
97  {
98  std::vector<mp_integer> v;
99  evaluate(expr, v);
100  if(v.size()!=1)
101  throw "invalid boolean value";
102  return v.front()!=0;
103  }
104 
105  void evaluate(
106  const exprt &expr,
107  std::vector<mp_integer> &dest) const;
108 
109  mp_integer evaluate_address(const exprt &expr) const;
110 
111  void show_state();
112 };
113 
114 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
The type of an expression.
Definition: type.h:20
void execute_goto()
BigInt mp_integer
Definition: mp_arith.h:19
goto_programt::const_targett PC
goto_programt::const_targett next_PC
Goto Programs with Functions.
void read(mp_integer address, std::vector< mp_integer > &dest) const
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
std::vector< memory_cellt > memoryt
std::unordered_map< irep_idt, unsigned, irep_id_hash > memory_mapt
std::stack< stack_framet > call_stackt
instructionst::const_iterator const_targett
interpretert(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
void execute_assert()
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
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void execute_assume()
bool evaluate_boolean(const exprt &expr) const
void execute_assign()
const symbol_tablet & symbol_table
unsigned get_size(const typet &type) const
void assign(mp_integer address, const std::vector< mp_integer > &rhs)
const namespacet ns
goto_functionst::function_mapt::const_iterator return_function
Base class for all expressions.
Definition: expr.h:46
void build_memory_map()
mp_integer evaluate_address(const exprt &expr) const
memory_mapt memory_map
call_stackt call_stack
void command()
Definition: interpreter.cpp:69
goto_programt::const_targett return_PC
void execute_other()
void execute_function_call()