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 #include <util/invariant.h>
19 #include <util/std_types.h>
20 #include <util/sparse_vector.h>
21 #include <util/message.h>
22 
23 #include "goto_functions.h"
24 #include "goto_trace.h"
25 #include "json_goto_trace.h"
26 
27 class interpretert:public messaget
28 {
29 public:
31  const symbol_tablet &_symbol_table,
32  const goto_functionst &_goto_functions,
33  message_handlert &_message_handler):
34  messaget(_message_handler),
35  symbol_table(_symbol_table),
36  ns(_symbol_table),
37  goto_functions(_goto_functions),
38  stack_pointer(0),
39  done(false),
40  stop_on_assertion(false)
41  {
42  show=true;
43  }
44 
45  void operator()();
46  void print_memory(bool input_flags);
47 
48  // An assertion that identifier 'id' carries value in some particular context.
49  // Used to record parameter (id) assignment (value) lists for function calls.
51  {
54  };
55 
56  // A list of such assignments.
57  typedef std::vector<function_assignmentt> function_assignmentst;
58 
59  typedef std::vector<mp_integer> mp_vectort;
60 
61  // Maps an assignment id to the name of the parameter being assigned
62  typedef std::pair<irep_idt, irep_idt> assignment_idt;
63 
64  // Identifies an expression before and after some change;
65  typedef std::pair<exprt, exprt> diff_pairt;
66 
67  // Records a diff between an assignment pre and post conditions
68  typedef std::map<assignment_idt, diff_pairt> side_effects_differencet;
69 
70  // A entry in the input_valuest map
71  typedef std::pair<irep_idt, exprt> input_entryt;
72 
73  // List of the input variables with their corresponding initial values
74  typedef std::map<irep_idt, exprt> input_valuest;
75 
76  // List of dynamically allocated symbols that are not in the symbol table
77  typedef std::map<irep_idt, typet> dynamic_typest;
78 
79  typedef std::map<irep_idt, function_assignmentst> output_valuest;
81 
82  // An assignment list annotated with the calling context.
84  {
89  };
90 
91  // list_input_varst maps function identifiers onto a vector of [name = value]
92  // assignments per call to that function.
93  typedef std::list<function_assignments_contextt>
95  typedef std::map<irep_idt, std::list<function_assignments_contextt> >
97 
99 
100 protected:
102 
103  // This is a cache so that we don't have to create it when a call needs it
104  const namespacet ns;
105 
107 
108  typedef std::unordered_map<irep_idt, mp_integer> memory_mapt;
109  typedef std::map<mp_integer, irep_idt> inverse_memory_mapt;
112 
113  const inverse_memory_mapt::value_type &address_to_object_record(
114  const mp_integer &address) const
115  {
116  auto lower_bound=inverse_memory_map.lower_bound(address);
117  if(lower_bound->first!=address)
118  {
119  CHECK_RETURN(lower_bound!=inverse_memory_map.begin());
120  --lower_bound;
121  }
122  return *lower_bound;
123  }
124 
126  {
127  return address_to_object_record(address).second;
128  }
129 
131  {
132  return address-(address_to_object_record(address).first);
133  }
134 
136  {
137  PRECONDITION(address_to_offset(address)==0);
138  auto upper_bound=inverse_memory_map.upper_bound(address);
139  mp_integer next_alloc_address=
140  upper_bound==inverse_memory_map.end() ?
141  memory.size() :
142  upper_bound->first;
143  return next_alloc_address-address;
144  }
145 
147  {
148  auto memory_iter=memory.find(integer2ulong(address));
149  if(memory_iter==memory.end())
150  return 0;
151  mp_integer ret=0;
152  mp_integer alloc_size=base_address_to_alloc_size(address);
153  while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
154  {
155  ++ret;
156  ++memory_iter;
157  }
158  return ret;
159  }
160 
162  {
163  public:
165  value(0),
167  {}
169  // Initialized is annotated even during reads
170  enum class initializedt
171  {
172  UNKNOWN,
175  };
176  // Set to 1 when written-before-read, -1 when read-before-written
178  };
179 
181  typedef std::map<std::string, const irep_idt &> parameter_sett;
182  // mapping <structure, field> -> value
183  typedef std::pair<const irep_idt, const irep_idt> struct_member_idt;
184  typedef std::map<struct_member_idt, const exprt> struct_valuest;
185 
186  // The memory is being annotated/reshaped even during reads
187  // (ie to find a read-before-write location) thus memory
188  // properties need to be mutable to avoid making all calls nonconst
189  mutable memoryt memory;
190 
192 
193  void build_memory_map();
194  void build_memory_map(const symbolt &symbol);
195  mp_integer build_memory_map(const irep_idt &id, const typet &type);
196  typet concretize_type(const typet &type);
197  bool unbounded_size(const typet &);
198  mp_integer get_size(const typet &type);
199 
201  const irep_idt &object,
202  const mp_integer &offset);
203 
204  typet get_type(const irep_idt &id) const;
205 
207  const typet &type,
208  const mp_integer &offset=0,
209  bool use_non_det=false);
210 
212  const typet &type,
213  mp_vectort &rhs,
214  const mp_integer &offset=0);
215 
216  exprt get_value(const irep_idt &id);
217 
218  void step();
219 
220  void execute_assert();
221  void execute_assume();
222  void execute_assign();
223  void execute_goto();
224  void execute_function_call();
225  void execute_other();
226  void execute_decl();
227  void clear_input_flags();
228 
229  void allocate(
230  const mp_integer &address,
231  const mp_integer &size);
232 
233  void assign(
234  const mp_integer &address,
235  const mp_vectort &rhs);
236 
237  void read(
238  const mp_integer &address,
239  mp_vectort &dest) const;
240 
241  void read_unbounded(
242  const mp_integer &address,
243  mp_vectort &dest) const;
244 
245  virtual void command();
246 
248  {
249  public:
251  goto_functionst::function_mapt::const_iterator return_function;
255  };
256 
257  typedef std::stack<stack_framet> call_stackt;
258 
262 
263  goto_functionst::function_mapt::const_iterator function;
266  bool done;
267  bool show;
269  static const size_t npos;
270  size_t num_steps;
271  size_t total_steps;
272 
276  unsigned thread_id;
277 
278  bool evaluate_boolean(const exprt &expr)
279  {
280  mp_vectort v;
281  evaluate(expr, v);
282  if(v.size()!=1)
283  throw "invalid boolean value";
284  return v.front()!=0;
285  }
286 
287  bool count_type_leaves(
288  const typet &source_type,
289  mp_integer &result);
290 
292  const typet &source_type,
293  const mp_integer &byte_offset,
294  mp_integer &result);
295 
297  const typet &source_type,
298  const mp_integer &cell_offset,
299  mp_integer &result);
300 
301  void evaluate(
302  const exprt &expr,
303  mp_vectort &dest);
304 
305  mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false);
306 
307  void initialize(bool init);
308  void show_state();
309 
310  friend class interpreter_testt;
311 };
312 
313 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
bool byte_offset_to_memory_offset(const typet &source_type, const mp_integer &byte_offset, mp_integer &result)
Supposing the caller has an mp_vector representing a value with type &#39;source_type&#39;, this yields the offset into that vector at which to find a value at byte address &#39;offset&#39;.
The type of an expression, extends irept.
Definition: type.h:27
void execute_goto()
executes a goto instruction
BigInt mp_integer
Definition: mp_arith.h:22
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
iteratort end()
Definition: sparse_vector.h:60
irep_idt address_to_identifier(const mp_integer &address) const
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
std::map< std::string, const irep_idt & > parameter_sett
std::list< function_assignments_contextt > function_assignments_contextst
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
goto_programt::const_targett return_pc
interpretert(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler)
bool evaluate_boolean(const exprt &expr)
std::map< irep_idt, std::list< function_assignments_contextt > > list_input_varst
std::pair< exprt, exprt > diff_pairt
std::vector< mp_integer > mp_vectort
std::map< assignment_idt, diff_pairt > side_effects_differencet
Goto Programs with Functions.
bool memory_offset_to_byte_offset(const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
Similarly to the above, the interpreter&#39;s memory objects contain mp_integers that represent variable-...
Traces of GOTO Programs.
input_valuest input_vars
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
std::vector< function_assignmentt > function_assignmentst
const dynamic_typest & get_dynamic_types()
mp_integer stack_pointer
std::stack< stack_framet > call_stackt
std::pair< irep_idt, irep_idt > assignment_idt
std::map< mp_integer, irep_idt > inverse_memory_mapt
std::map< irep_idt, exprt > input_valuest
static const size_t npos
void execute_assert()
exprt get_value(const typet &type, const mp_integer &offset=0, bool use_non_det=false)
retrives the constant value at memory location offset as an object of type type
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
std::unordered_map< irep_idt, mp_integer > memory_mapt
const goto_functionst & goto_functions
Traces of GOTO Programs.
std::pair< const irep_idt, const irep_idt > struct_member_idt
void execute_decl()
void show_state()
displays the current position of the pc and corresponding code
mp_integer address_to_offset(const mp_integer &address) const
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
Definition: interpreter.cpp:63
void operator()()
Definition: interpreter.cpp:39
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
const inverse_memory_mapt::value_type & address_to_object_record(const mp_integer &address) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void execute_assume()
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
output_valuest output_values
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
mp_integer base_address_to_actual_size(const mp_integer &address) const
A collection of goto functions.
void execute_assign()
executes the assign statement at the current pc value
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
goto_tracet steps
std::map< struct_member_idt, const exprt > struct_valuest
bool unbounded_size(const typet &)
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
sparse_vectort< memory_cellt > memoryt
void step()
executes a single step and updates the program counter
inverse_memory_mapt inverse_memory_map
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
const symbol_tablet & symbol_table
friend class interpreter_testt
const_iteratort find(uint64_t idx)
Definition: sparse_vector.h:63
mp_integer stack_depth
std::pair< irep_idt, exprt > input_entryt
goto_programt::const_targett next_pc
std::map< irep_idt, function_assignmentst > output_valuest
void clear_input_flags()
Clears memoy r/w flag initialization.
Pre-defined types.
const namespacet ns
goto_functionst::function_mapt::const_iterator return_function
mstreamt & result() const
Definition: message.h:396
Base class for all expressions.
Definition: expr.h:54
struct_typet::componentt get_component(const irep_idt &object, const mp_integer &offset)
retrieves the member at offset
void build_memory_map()
Creates a memory map of all static symbols in the program.
goto_programt::const_targett pc
std::map< irep_idt, typet > dynamic_typest
memory_mapt memory_map
call_stackt call_stack
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst.
goto_programt::const_targett target_assert
virtual void command()
reads a user command and executes it.
dynamic_typest dynamic_types
uint64_t size() const
Definition: sparse_vector.h:43
bool count_type_leaves(const typet &source_type, mp_integer &result)
Count the number of leaf subtypes of ty, a leaf type is a type that is not an array or a struct...
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
Sparse Vectors.
void execute_other()
executes side effects of &#39;other&#39; instructions
mp_integer base_address_to_alloc_size(const mp_integer &address) const
list_input_varst function_input_vars
void execute_function_call()