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  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 
200  DEPRECATED("use the object_type version instead")
201  struct_typet::componentt get_component(
202  const irep_idt &object,
203  const mp_integer &offset);
204 
205  struct_typet::componentt
206  get_component(const typet &object_type, const mp_integer &offset);
207 
208  typet get_type(const irep_idt &id) const;
209 
211  const typet &type,
212  const mp_integer &offset=0,
213  bool use_non_det=false);
214 
216  const typet &type,
217  mp_vectort &rhs,
218  const mp_integer &offset=0);
219 
220  exprt get_value(const irep_idt &id);
221 
222  void step();
223 
224  void execute_assert();
225  void execute_assume();
226  void execute_assign();
227  void execute_goto();
228  void execute_function_call();
229  void execute_other();
230  void execute_decl();
231  void clear_input_flags();
232 
233  void allocate(
234  const mp_integer &address,
235  const mp_integer &size);
236 
237  void assign(
238  const mp_integer &address,
239  const mp_vectort &rhs);
240 
241  void read(
242  const mp_integer &address,
243  mp_vectort &dest) const;
244 
245  void read_unbounded(
246  const mp_integer &address,
247  mp_vectort &dest) const;
248 
249  virtual void command();
250 
252  {
253  public:
255  goto_functionst::function_mapt::const_iterator return_function;
259  };
260 
261  typedef std::stack<stack_framet> call_stackt;
262 
266 
267  goto_functionst::function_mapt::const_iterator function;
270  bool done;
271  bool show;
273  static const size_t npos;
274  size_t num_steps;
275  size_t total_steps;
276 
280  unsigned thread_id;
281 
282  bool evaluate_boolean(const exprt &expr)
283  {
284  mp_vectort v;
285  evaluate(expr, v);
286  if(v.size()!=1)
287  throw "invalid boolean value";
288  return v.front()!=0;
289  }
290 
291  bool count_type_leaves(
292  const typet &source_type,
293  mp_integer &result);
294 
296  const typet &source_type,
297  const mp_integer &byte_offset,
298  mp_integer &result);
299 
301  const typet &source_type,
302  const mp_integer &cell_offset,
303  mp_integer &result);
304 
305  void evaluate(
306  const exprt &expr,
307  mp_vectort &dest);
308 
309  mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false);
310 
311  void initialize(bool init);
312  void show_state();
313 
314  friend class interpreter_testt;
315 };
316 
317 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
interpretert::base_address_to_actual_size
mp_integer base_address_to_actual_size(const mp_integer &address) const
Definition: interpreter_class.h:146
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
interpretert::interpretert
interpretert(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler)
Definition: interpreter_class.h:30
interpretert::stack_framet
Definition: interpreter_class.h:252
sparse_vectort< memory_cellt >
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
interpretert::show_state
void show_state()
displays the current position of the pc and corresponding code
Definition: interpreter.cpp:105
arith_tools.h
interpretert::allocate
void allocate(const mp_integer &address, const mp_integer &size)
reserves memory block of size at address
Definition: interpreter_evaluate.cpp:80
interpretert::stack_depth
mp_integer stack_depth
Definition: interpreter_class.h:279
interpretert::execute_decl
void execute_decl()
Definition: interpreter.cpp:419
interpretert::interpreter_testt
friend class interpreter_testt
Definition: interpreter_class.h:314
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
sparse_vectort::end
iteratort end()
Definition: sparse_vector.h:60
interpretert::memoryt
sparse_vectort< memory_cellt > memoryt
Definition: interpreter_class.h:180
interpretert::execute_goto
void execute_goto()
executes a goto instruction
Definition: interpreter.cpp:370
interpretert::pc
goto_programt::const_targett pc
Definition: interpreter_class.h:268
interpretert::symbol_table
const symbol_tablet & symbol_table
Definition: interpreter_class.h:101
interpretert::memory
memoryt memory
Definition: interpreter_class.h:189
interpretert::assign
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
Definition: interpreter.cpp:710
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
interpretert::function_assignments_contextt::param_assignments
function_assignmentst param_assignments
Definition: interpreter_class.h:87
sparse_vectort::size
uint64_t size() const
Definition: sparse_vector.h:43
interpretert::address_to_symbol
symbol_exprt address_to_symbol(const mp_integer &address) const
Definition: interpreter_class.h:125
invariant.h
interpretert::evaluate_boolean
bool evaluate_boolean(const exprt &expr)
Definition: interpreter_class.h:282
interpretert::memory_cellt::initializedt::READ_BEFORE_WRITTEN
@ READ_BEFORE_WRITTEN
interpretert::unbounded_size
bool unbounded_size(const typet &)
Definition: interpreter.cpp:958
interpretert::diff_pairt
std::pair< exprt, exprt > diff_pairt
Definition: interpreter_class.h:65
interpretert::memory_cellt::value
mp_integer value
Definition: interpreter_class.h:168
interpretert::get_component
struct_typet::componentt get_component(const irep_idt &object, const mp_integer &offset)
retrieves the member at offset
Definition: interpreter.cpp:426
exprt
Base class for all expressions.
Definition: expr.h:53
interpretert::function_assignments_contextt::calling_function
irep_idt calling_function
Definition: interpreter_class.h:85
interpretert::assignment_idt
std::pair< irep_idt, irep_idt > assignment_idt
Definition: interpreter_class.h:62
interpretert::next_pc
goto_programt::const_targett next_pc
Definition: interpreter_class.h:268
interpretert::function_assignmentst
std::vector< function_assignmentt > function_assignmentst
Definition: interpreter_class.h:57
interpretert::stop_on_assertion
bool stop_on_assertion
Definition: interpreter_class.h:272
interpretert::call_stack
call_stackt call_stack
Definition: interpreter_class.h:263
interpretert::num_steps
size_t num_steps
Definition: interpreter_class.h:274
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
interpretert::dynamic_typest
std::map< irep_idt, typet > dynamic_typest
Definition: interpreter_class.h:77
interpretert::list_input_varst
std::map< irep_idt, std::list< function_assignments_contextt > > list_input_varst
Definition: interpreter_class.h:96
interpretert::memory_mapt
std::unordered_map< irep_idt, mp_integer > memory_mapt
Definition: interpreter_class.h:108
interpretert::print_memory
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members,...
Definition: interpreter.cpp:1066
interpretert::dynamic_types
dynamic_typest dynamic_types
Definition: interpreter_class.h:277
interpretert::total_steps
size_t total_steps
Definition: interpreter_class.h:275
interpretert::build_memory_map
void build_memory_map()
Creates a memory map of all static symbols in the program.
Definition: interpreter.cpp:860
interpretert::count_type_leaves
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.
Definition: interpreter_evaluate.cpp:113
goto_trace.h
Traces of GOTO Programs.
interpretert::base_address_to_alloc_size
mp_integer base_address_to_alloc_size(const mp_integer &address) const
Definition: interpreter_class.h:135
interpretert::memory_cellt::initializedt
initializedt
Definition: interpreter_class.h:171
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
interpretert::memory_cellt
Definition: interpreter_class.h:162
interpretert
Definition: interpreter_class.h:28
sparse_vector.h
Sparse Vectors.
messaget::result
mstreamt & result() const
Definition: message.h:409
interpretert::struct_valuest
std::map< struct_member_idt, const exprt > struct_valuest
Definition: interpreter_class.h:184
file_typet::UNKNOWN
@ UNKNOWN
interpretert::get_size
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
Definition: interpreter.cpp:981
interpretert::execute_other
void execute_other()
executes side effects of 'other' instructions
Definition: interpreter.cpp:385
interpretert::get_value
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
Definition: interpreter.cpp:469
interpretert::command
virtual void command()
reads a user command and executes it.
Definition: interpreter.cpp:128
interpretert::step
void step()
executes a single step and updates the program counter
Definition: interpreter.cpp:233
interpretert::inverse_memory_mapt
std::map< mp_integer, optionalt< symbol_exprt > > inverse_memory_mapt
Definition: interpreter_class.h:109
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
interpretert::function_assignmentt
Definition: interpreter_class.h:51
interpretert::function_assignments_contextt::exception_assignments
function_assignmentst exception_assignments
Definition: interpreter_class.h:88
std_types.h
Pre-defined types.
interpretert::memory_cellt::memory_cellt
memory_cellt()
Definition: interpreter_class.h:164
interpretert::num_dynamic_objects
int num_dynamic_objects
Definition: interpreter_class.h:278
interpretert::memory_cellt::initialized
initializedt initialized
Definition: interpreter_class.h:177
interpretert::stack_framet::old_stack_pointer
mp_integer old_stack_pointer
Definition: interpreter_class.h:258
interpretert::read_unbounded
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
Definition: interpreter_evaluate.cpp:50
interpretert::execute_function_call
void execute_function_call()
Definition: interpreter.cpp:753
interpretert::goto_functions
const goto_functionst & goto_functions
Definition: interpreter_class.h:106
interpretert::address_to_object_record
const inverse_memory_mapt::value_type & address_to_object_record(const mp_integer &address) const
Definition: interpreter_class.h:113
interpretert::get_type
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
Definition: interpreter.cpp:459
message_handlert
Definition: message.h:28
interpretert::mp_vectort
std::vector< mp_integer > mp_vectort
Definition: interpreter_class.h:59
interpretert::input_entryt
std::pair< irep_idt, exprt > input_entryt
Definition: interpreter_class.h:71
interpretert::function_assignments_contextst
std::list< function_assignments_contextt > function_assignments_contextst
Definition: interpreter_class.h:94
interpretert::steps
goto_tracet steps
Definition: interpreter_class.h:269
json_goto_trace.h
Traces of GOTO Programs.
interpretert::stack_framet::local_map
memory_mapt local_map
Definition: interpreter_class.h:257
interpretert::concretize_type
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
Definition: interpreter.cpp:900
interpretert::show
bool show
Definition: interpreter_class.h:271
interpretert::execute_assign
void execute_assign()
executes the assign statement at the current pc value
Definition: interpreter.cpp:663
interpretert::evaluate
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
Definition: interpreter_evaluate.cpp:313
interpretert::ns
const namespacet ns
Definition: interpreter_class.h:104
interpretert::side_effects_differencet
std::map< assignment_idt, diff_pairt > side_effects_differencet
Definition: interpreter_class.h:68
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
interpretert::output_valuest
std::map< irep_idt, function_assignmentst > output_valuest
Definition: interpreter_class.h:79
interpretert::get_dynamic_types
const dynamic_typest & get_dynamic_types()
Definition: interpreter_class.h:98
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
interpretert::stack_pointer
mp_integer stack_pointer
Definition: interpreter_class.h:191
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
interpretert::memory_offset_to_byte_offset
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-...
Definition: interpreter_evaluate.cpp:238
interpretert::memory_cellt::initializedt::UNKNOWN
@ UNKNOWN
symbolt
Symbol table entry.
Definition: symbol.h:28
interpretert::function_assignmentt::id
irep_idt id
Definition: interpreter_class.h:52
interpretert::stack_framet::return_value_address
mp_integer return_value_address
Definition: interpreter_class.h:256
interpretert::inverse_memory_map
inverse_memory_mapt inverse_memory_map
Definition: interpreter_class.h:111
interpretert::clear_input_flags
void clear_input_flags()
Clears memoy r/w flag initialization.
Definition: interpreter_evaluate.cpp:97
interpretert::function_assignmentt::value
exprt value
Definition: interpreter_class.h:53
interpretert::read
void read(const mp_integer &address, mp_vectort &dest) const
Reads a memory address and loads it into the dest variable.
Definition: interpreter_evaluate.cpp:26
goto_functions.h
Goto Programs with Functions.
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
interpretert::input_vars
input_valuest input_vars
Definition: interpreter_class.h:264
interpretert::memory_cellt::initializedt::WRITTEN_BEFORE_READ
@ WRITTEN_BEFORE_READ
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
sparse_vectort::find
const_iteratort find(uint64_t idx)
Definition: sparse_vector.h:63
interpretert::function_assignments_contextt::return_assignments
function_assignmentst return_assignments
Definition: interpreter_class.h:86
interpretert::address_to_offset
mp_integer address_to_offset(const mp_integer &address) const
Definition: interpreter_class.h:130
interpretert::done
bool done
Definition: interpreter_class.h:270
interpretert::operator()
void operator()()
Definition: interpreter.cpp:40
interpretert::stack_framet::return_function
goto_functionst::function_mapt::const_iterator return_function
Definition: interpreter_class.h:255
interpretert::struct_member_idt
std::pair< const irep_idt, const irep_idt > struct_member_idt
Definition: interpreter_class.h:183
interpretert::output_values
output_valuest output_values
Definition: interpreter_class.h:80
interpretert::call_stackt
std::stack< stack_framet > call_stackt
Definition: interpreter_class.h:261
message.h
interpretert::function_input_vars
list_input_varst function_input_vars
Definition: interpreter_class.h:265
interpretert::thread_id
unsigned thread_id
Definition: interpreter_class.h:280
interpretert::target_assert
goto_programt::const_targett target_assert
Definition: interpreter_class.h:268
interpretert::byte_offset_to_memory_offset
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',...
Definition: interpreter_evaluate.cpp:156
interpretert::memory_map
memory_mapt memory_map
Definition: interpreter_class.h:110
interpretert::function_assignments_contextt
Definition: interpreter_class.h:84
interpretert::npos
static const size_t npos
Definition: interpreter_class.h:273
interpretert::execute_assume
void execute_assume()
Definition: interpreter.cpp:735
interpretert::execute_assert
void execute_assert()
Definition: interpreter.cpp:741
interpretert::input_valuest
std::map< irep_idt, exprt > input_valuest
Definition: interpreter_class.h:74
interpretert::parameter_sett
std::map< std::string, const irep_idt & > parameter_sett
Definition: interpreter_class.h:181
interpretert::stack_framet::return_pc
goto_programt::const_targett return_pc
Definition: interpreter_class.h:254
interpretert::evaluate_address
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
Definition: interpreter_evaluate.cpp:1055
interpretert::initialize
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
Definition: interpreter.cpp:64