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
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
interpretert::output
messaget output
Definition: interpreter_class.h:100
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:247
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:114
interpretert::get_component
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.
Definition: interpreter.cpp:432
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:83
interpretert::execute_decl
void execute_decl()
Definition: interpreter.cpp:425
interpretert::interpreter_testt
friend class interpreter_testt
Definition: interpreter_class.h:307
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
sparse_vectort::end
iteratort end()
Definition: sparse_vector.h:66
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:375
interpretert::pc
goto_programt::const_targett pc
Definition: interpreter_class.h:263
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:704
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
interpretert::function_assignments_contextt::param_assignments
function_assignmentst param_assignments
Definition: interpreter_class.h:86
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:275
interpretert::memory_cellt::initializedt::READ_BEFORE_WRITTEN
@ READ_BEFORE_WRITTEN
interpretert::unbounded_size
bool unbounded_size(const typet &)
Definition: interpreter.cpp:952
interpretert::diff_pairt
std::pair< exprt, exprt > diff_pairt
Definition: interpreter_class.h:64
interpretert::memory_cellt::value
mp_integer value
Definition: interpreter_class.h:168
exprt
Base class for all expressions.
Definition: expr.h:54
interpretert::function_assignments_contextt::calling_function
irep_idt calling_function
Definition: interpreter_class.h:84
interpretert::assignment_idt
std::pair< irep_idt, irep_idt > assignment_idt
Definition: interpreter_class.h:61
interpretert::next_pc
goto_programt::const_targett next_pc
Definition: interpreter_class.h:263
interpretert::function_assignmentst
std::vector< function_assignmentt > function_assignmentst
Definition: interpreter_class.h:56
interpretert::call_stack
call_stackt call_stack
Definition: interpreter_class.h:258
interpretert::num_steps
size_t num_steps
Definition: interpreter_class.h:268
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
interpretert::dynamic_typest
std::map< irep_idt, typet > dynamic_typest
Definition: interpreter_class.h:76
interpretert::list_input_varst
std::map< irep_idt, std::list< function_assignments_contextt > > list_input_varst
Definition: interpreter_class.h:95
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:1060
interpretert::dynamic_types
dynamic_typest dynamic_types
Definition: interpreter_class.h:271
interpretert::total_steps
size_t total_steps
Definition: interpreter_class.h:269
interpretert::build_memory_map
void build_memory_map()
Creates a memory map of all static symbols in the program.
Definition: interpreter.cpp:852
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:116
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.
interpretert::struct_valuest
std::map< struct_member_idt, const exprt > struct_valuest
Definition: interpreter_class.h:184
interpretert::get_size
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
Definition: interpreter.cpp:975
interpretert::execute_other
void execute_other()
executes side effects of 'other' instructions
Definition: interpreter.cpp:390
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:465
interpretert::command
virtual void command()
reads a user command and executes it.
Definition: interpreter.cpp:134
interpretert::step
void step()
executes a single step and updates the program counter
Definition: interpreter.cpp:239
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:50
interpretert::function_assignments_contextt::exception_assignments
function_assignmentst exception_assignments
Definition: interpreter_class.h:87
std_types.h
Pre-defined types.
ai_verifier_statust::TRUE
@ TRUE
interpretert::memory_cellt::memory_cellt
memory_cellt()
Definition: interpreter_class.h:164
interpretert::num_dynamic_objects
int num_dynamic_objects
Definition: interpreter_class.h:272
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:253
interpretert::read_unbounded
void read_unbounded(const mp_integer &address, mp_vectort &dest) const
Definition: interpreter_evaluate.cpp:53
interpretert::execute_function_call
void execute_function_call()
Definition: interpreter.cpp:745
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:455
message_handlert
Definition: message.h:28
interpretert::mp_vectort
std::vector< mp_integer > mp_vectort
Definition: interpreter_class.h:58
interpretert::input_entryt
std::pair< irep_idt, exprt > input_entryt
Definition: interpreter_class.h:70
interpretert::function_assignments_contextst
std::list< function_assignments_contextt > function_assignments_contextst
Definition: interpreter_class.h:93
interpretert::steps
goto_tracet steps
Definition: interpreter_class.h:264
json_goto_trace.h
Traces of GOTO Programs.
interpretert::stack_framet::local_map
memory_mapt local_map
Definition: interpreter_class.h:252
interpretert::concretize_type
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
Definition: interpreter.cpp:893
interpretert::show
bool show
Definition: interpreter_class.h:266
interpretert::execute_assign
void execute_assign()
executes the assign statement at the current pc value
Definition: interpreter.cpp:659
interpretert::evaluate
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
Definition: interpreter_evaluate.cpp:316
interpretert::ns
const namespacet ns
Definition: interpreter_class.h:104
struct_union_typet::componentt
Definition: std_types.h:63
interpretert::side_effects_differencet
std::map< assignment_idt, diff_pairt > side_effects_differencet
Definition: interpreter_class.h:67
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:78
interpretert::get_dynamic_types
const dynamic_typest & get_dynamic_types()
Definition: interpreter_class.h:97
interpretert::stack_pointer
mp_integer stack_pointer
Definition: interpreter_class.h:191
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:241
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:51
interpretert::stack_framet::return_value_address
mp_integer return_value_address
Definition: interpreter_class.h:251
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:100
interpretert::function_assignmentt::value
exprt value
Definition: interpreter_class.h:52
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:29
goto_functions.h
Goto Programs with Functions.
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:177
interpretert::input_vars
input_valuest input_vars
Definition: interpreter_class.h:259
interpretert::memory_cellt::initializedt::WRITTEN_BEFORE_READ
@ WRITTEN_BEFORE_READ
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
sparse_vectort::find
const_iteratort find(uint64_t idx)
Definition: sparse_vector.h:69
interpretert::function_assignments_contextt::return_assignments
function_assignmentst return_assignments
Definition: interpreter_class.h:85
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:265
interpretert::operator()
void operator()()
Definition: interpreter.cpp:42
interpretert::stack_framet::return_function
goto_functionst::function_mapt::const_iterator return_function
Definition: interpreter_class.h:250
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:79
interpretert::call_stackt
std::stack< stack_framet > call_stackt
Definition: interpreter_class.h:256
message.h
interpretert::function_input_vars
list_input_varst function_input_vars
Definition: interpreter_class.h:260
interpretert::thread_id
unsigned thread_id
Definition: interpreter_class.h:273
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:159
interpretert::memory_map
memory_mapt memory_map
Definition: interpreter_class.h:110
interpretert::function_assignments_contextt
Definition: interpreter_class.h:83
interpretert::npos
static const size_t npos
Definition: interpreter_class.h:267
interpretert::execute_assume
void execute_assume()
Definition: interpreter.cpp:729
interpretert::execute_assert
void execute_assert()
Definition: interpreter.cpp:735
interpretert::input_valuest
std::map< irep_idt, exprt > input_valuest
Definition: interpreter_class.h:73
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:249
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:66