CBMC
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 <util/arith_tools.h>
16 #include <util/invariant.h>
17 #include <util/message.h>
18 #include <util/namespace.h>
19 #include <util/sparse_vector.h>
20 #include <util/std_types.h>
21 
22 #include "goto_functions.h"
23 #include "goto_trace.h"
24 #include "json_goto_trace.h"
25 
26 #include <stack>
27 
29 {
30 public:
32  const symbol_table_baset &_symbol_table,
33  const goto_functionst &_goto_functions,
34  message_handlert &_message_handler)
35  : output(_message_handler),
36  symbol_table(_symbol_table),
37  ns(_symbol_table),
38  goto_functions(_goto_functions),
39  stack_pointer(0),
40  done(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:
103 
104  // This is a cache so that we don't have to create it when a call needs it
105  const namespacet ns;
106 
108 
109  typedef std::unordered_map<irep_idt, mp_integer> memory_mapt;
110  using inverse_memory_mapt = std::map<mp_integer, std::optional<symbol_exprt>>;
113 
114  const inverse_memory_mapt::value_type &address_to_object_record(
115  const mp_integer &address) const
116  {
117  auto lower_bound=inverse_memory_map.lower_bound(address);
118  if(lower_bound->first!=address)
119  {
120  CHECK_RETURN(lower_bound!=inverse_memory_map.begin());
121  --lower_bound;
122  }
123  return *lower_bound;
124  }
125 
127  {
128  return *address_to_object_record(address).second;
129  }
130 
132  {
133  return address-(address_to_object_record(address).first);
134  }
135 
137  {
138  PRECONDITION(address_to_offset(address)==0);
139  auto upper_bound=inverse_memory_map.upper_bound(address);
140  mp_integer next_alloc_address=
141  upper_bound==inverse_memory_map.end() ?
142  memory.size() :
143  upper_bound->first;
144  return next_alloc_address-address;
145  }
146 
148  {
149  auto memory_iter = memory.find(numeric_cast_v<std::size_t>(address));
150  if(memory_iter==memory.end())
151  return 0;
152  mp_integer ret=0;
153  mp_integer alloc_size=base_address_to_alloc_size(address);
154  while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
155  {
156  ++ret;
157  ++memory_iter;
158  }
159  return ret;
160  }
161 
163  {
164  public:
166  value(0),
168  {}
170  // Initialized is annotated even during reads
171  enum class initializedt
172  {
173  UNKNOWN,
176  };
177  // Set to 1 when written-before-read, -1 when read-before-written
179  };
180 
182  typedef std::map<std::string, const irep_idt &> parameter_sett;
183  // mapping <structure, field> -> value
184  typedef std::pair<const irep_idt, const irep_idt> struct_member_idt;
185  typedef std::map<struct_member_idt, const exprt> struct_valuest;
186 
187  // The memory is being annotated/reshaped even during reads
188  // (ie to find a read-before-write location) thus memory
189  // properties need to be mutable to avoid making all calls nonconst
190  mutable memoryt memory;
191 
193 
194  void build_memory_map();
195  void build_memory_map(const symbolt &symbol);
196  mp_integer build_memory_map(const symbol_exprt &symbol_expr);
197  typet concretize_type(const typet &type);
198  bool unbounded_size(const typet &);
199  mp_integer get_size(const typet &type);
200 
202  get_component(const typet &object_type, 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;
268  static const size_t npos;
269  size_t num_steps;
270  size_t total_steps;
271 
274  unsigned thread_id;
275 
276  bool evaluate_boolean(const exprt &expr)
277  {
278  mp_vectort v = evaluate(expr);
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  mp_vectort evaluate(const exprt &);
299 
300  mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false);
301 
302  void initialize(bool init);
303  void show_state();
304 
305  friend class interpreter_testt;
306 };
307 
308 #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:38
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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:38
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',...
std::map< mp_integer, std::optional< symbol_exprt > > inverse_memory_mapt
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()
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
mp_vectort evaluate(const exprt &)
Evaluate an expression.
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
const symbol_table_baset & symbol_table
void step()
executes a single step and updates the program counter
std::unordered_map< irep_idt, mp_integer > memory_mapt
interpretert(const symbol_table_baset &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler)
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.
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:62
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:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:131
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
Goto Programs with Functions.
Traces of GOTO Programs.
Traces of GOTO Programs.
BigInt mp_integer
Definition: smt_terms.h:17
Sparse Vectors.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Pre-defined types.