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 
28 {
29 public:
31  const symbol_tablet &_symbol_table,
32  const goto_functionst &_goto_functions,
33  message_handlert &_message_handler)
34  : output(_message_handler),
35  symbol_table(_symbol_table),
36  ns(_symbol_table),
37  goto_functions(_goto_functions),
38  stack_pointer(0),
39  done(false)
40  {
41  show=true;
42  }
43 
44  void operator()();
45  void print_memory(bool input_flags);
46 
47  // An assertion that identifier 'id' carries value in some particular context.
48  // Used to record parameter (id) assignment (value) lists for function calls.
50  {
53  };
54 
55  // A list of such assignments.
56  typedef std::vector<function_assignmentt> function_assignmentst;
57 
58  typedef std::vector<mp_integer> mp_vectort;
59 
60  // Maps an assignment id to the name of the parameter being assigned
61  typedef std::pair<irep_idt, irep_idt> assignment_idt;
62 
63  // Identifies an expression before and after some change;
64  typedef std::pair<exprt, exprt> diff_pairt;
65 
66  // Records a diff between an assignment pre and post conditions
67  typedef std::map<assignment_idt, diff_pairt> side_effects_differencet;
68 
69  // A entry in the input_valuest map
70  typedef std::pair<irep_idt, exprt> input_entryt;
71 
72  // List of the input variables with their corresponding initial values
73  typedef std::map<irep_idt, exprt> input_valuest;
74 
75  // List of dynamically allocated symbols that are not in the symbol table
76  typedef std::map<irep_idt, typet> dynamic_typest;
77 
78  typedef std::map<irep_idt, function_assignmentst> output_valuest;
80 
81  // An assignment list annotated with the calling context.
83  {
88  };
89 
90  // list_input_varst maps function identifiers onto a vector of [name = value]
91  // assignments per call to that function.
92  typedef std::list<function_assignments_contextt>
94  typedef std::map<irep_idt, std::list<function_assignments_contextt> >
96 
98 
99 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  using inverse_memory_mapt = std::map<mp_integer, optionalt<symbol_exprt>>;
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(numeric_cast_v<std::size_t>(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 symbol_exprt &symbol_expr);
196  typet concretize_type(const typet &type);
197  bool unbounded_size(const typet &);
198  mp_integer get_size(const typet &type);
199 
201  get_component(const typet &object_type, const mp_integer &offset);
202 
203  typet get_type(const irep_idt &id) const;
204 
206  const typet &type,
207  const mp_integer &offset=0,
208  bool use_non_det=false);
209 
211  const typet &type,
212  mp_vectort &rhs,
213  const mp_integer &offset=0);
214 
215  exprt get_value(const irep_idt &id);
216 
217  void step();
218 
219  void execute_assert();
220  void execute_assume();
221  void execute_assign();
222  void execute_goto();
223  void execute_function_call();
224  void execute_other();
225  void execute_decl();
226  void clear_input_flags();
227 
228  void allocate(
229  const mp_integer &address,
230  const mp_integer &size);
231 
232  void assign(
233  const mp_integer &address,
234  const mp_vectort &rhs);
235 
236  void read(
237  const mp_integer &address,
238  mp_vectort &dest) const;
239 
240  void read_unbounded(
241  const mp_integer &address,
242  mp_vectort &dest) const;
243 
244  virtual void command();
245 
247  {
248  public:
250  goto_functionst::function_mapt::const_iterator return_function;
254  };
255 
256  typedef std::stack<stack_framet> call_stackt;
257 
261 
262  goto_functionst::function_mapt::const_iterator function;
265  bool done;
266  bool show;
267  static const size_t npos;
268  size_t num_steps;
269  size_t total_steps;
270 
273  unsigned thread_id;
274 
275  bool evaluate_boolean(const exprt &expr)
276  {
277  mp_vectort v;
278  evaluate(expr, v);
279  if(v.size()!=1)
280  throw "invalid boolean value";
281  return v.front()!=0;
282  }
283 
284  bool count_type_leaves(
285  const typet &source_type,
286  mp_integer &result);
287 
289  const typet &source_type,
290  const mp_integer &byte_offset,
291  mp_integer &result);
292 
294  const typet &source_type,
295  const mp_integer &cell_offset,
296  mp_integer &result);
297 
298  void evaluate(
299  const exprt &expr,
300  mp_vectort &dest);
301 
302  mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false);
303 
304  void initialize(bool init);
305  void show_state();
306 
307  friend class interpreter_testt;
308 };
309 
310 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:551
Trace of a GOTO program.
Definition: goto_trace.h:177
goto_programt::const_targett return_pc
goto_functionst::function_mapt::const_iterator return_function
void clear_input_flags()
Clears memoy r/w flag initialization.
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
std::map< irep_idt, function_assignmentst > output_valuest
std::map< assignment_idt, diff_pairt > side_effects_differencet
std::map< irep_idt, std::list< function_assignments_contextt > > list_input_varst
void execute_function_call()
std::list< function_assignments_contextt > function_assignments_contextst
mp_integer stack_pointer
void execute_assert()
std::map< struct_member_idt, const exprt > struct_valuest
std::pair< exprt, exprt > diff_pairt
static const size_t npos
mp_integer base_address_to_actual_size(const mp_integer &address) const
void operator()()
Definition: interpreter.cpp:41
memory_mapt memory_map
friend class interpreter_testt
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members,...
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
virtual void command()
reads a user command and executes it.
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 'source_type',...
inverse_memory_mapt inverse_memory_map
sparse_vectort< memory_cellt > memoryt
output_valuest output_values
symbol_exprt address_to_symbol(const mp_integer &address) const
call_stackt call_stack
void execute_assume()
std::map< mp_integer, optionalt< symbol_exprt > > inverse_memory_mapt
void execute_goto()
executes a goto instruction
std::map< std::string, const irep_idt & > parameter_sett
goto_tracet steps
void build_memory_map()
Creates a memory map of all static symbols in the program.
std::pair< irep_idt, exprt > input_entryt
std::vector< mp_integer > mp_vectort
void execute_assign()
executes the assign statement at the current pc value
void execute_decl()
std::map< irep_idt, exprt > input_valuest
list_input_varst function_input_vars
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
std::stack< stack_framet > call_stackt
const inverse_memory_mapt::value_type & address_to_object_record(const mp_integer &address) const
const dynamic_typest & get_dynamic_types()
std::vector< function_assignmentt > function_assignmentst
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
mp_integer address_to_offset(const mp_integer &address) const
interpretert(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler)
void step()
executes a single step and updates the program counter
std::unordered_map< irep_idt, mp_integer > memory_mapt
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.
struct_typet::componentt get_component(const typet &object_type, const mp_integer &offset)
Retrieves the member at offset of an object of type object_type.
mp_integer base_address_to_alloc_size(const mp_integer &address) const
input_valuest input_vars
const namespacet ns
goto_programt::const_targett next_pc
bool evaluate_boolean(const exprt &expr)
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
const symbol_tablet & symbol_table
void show_state()
displays the current position of the pc and corresponding code
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
Definition: interpreter.cpp:65
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
bool unbounded_size(const typet &)
void execute_other()
executes side effects of 'other' instructions
bool memory_offset_to_byte_offset(const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-...
std::map< irep_idt, typet > dynamic_typest
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
goto_programt::const_targett pc
dynamic_typest dynamic_types
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const goto_functionst & goto_functions
std::pair< const irep_idt, const irep_idt > struct_member_idt
std::pair< irep_idt, irep_idt > assignment_idt
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
const_iteratort find(uint64_t idx)
Definition: sparse_vector.h:69
iteratort end()
Definition: sparse_vector.h:66
uint64_t size() const
Definition: sparse_vector.h:43
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
Goto Programs with Functions.
Traces of GOTO Programs.
Traces of GOTO Programs.
BigInt mp_integer
Definition: mp_arith.h:19
Sparse Vectors.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
Pre-defined types.