cprover
interpreter_evaluate.cpp
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 #include "interpreter_class.h"
13 
14 #include <cassert>
15 #include <iostream>
16 
17 #include <util/ieee_float.h>
18 #include <util/fixedbv.h>
19 #include <util/std_expr.h>
20 
22  mp_integer address,
23  std::vector<mp_integer> &dest) const
24 {
25  // copy memory region
26  for(auto &d : dest)
27  {
28  mp_integer value;
29 
30  if(address<memory.size())
31  value=memory[integer2size_t(address)].value;
32  else
33  value=0;
34 
35  d=value;
36 
37  ++address;
38  }
39 }
40 
42  const exprt &expr,
43  std::vector<mp_integer> &dest) const
44 {
45  if(expr.id()==ID_constant)
46  {
47  if(expr.type().id()==ID_struct)
48  {
49  }
50  else if(expr.type().id()==ID_floatbv)
51  {
52  ieee_floatt f;
53  f.from_expr(to_constant_expr(expr));
54  dest.push_back(f.pack());
55  return;
56  }
57  else if(expr.type().id()==ID_fixedbv)
58  {
59  fixedbvt f;
60  f.from_expr(to_constant_expr(expr));
61  dest.push_back(f.get_value());
62  return;
63  }
64  else if(expr.type().id()==ID_bool)
65  {
66  dest.push_back(expr.is_true());
67  return;
68  }
69  else
70  {
71  mp_integer i;
72  if(!to_integer(expr, i))
73  {
74  dest.push_back(i);
75  return;
76  }
77  }
78  }
79  else if(expr.id()==ID_struct)
80  {
81  dest.reserve(get_size(expr.type()));
82  bool error=false;
83 
84  forall_operands(it, expr)
85  {
86  if(it->type().id()==ID_code)
87  continue;
88 
89  unsigned sub_size=get_size(it->type());
90  if(sub_size==0)
91  continue;
92 
93  std::vector<mp_integer> tmp;
94  evaluate(*it, tmp);
95 
96  if(tmp.size()==sub_size)
97  {
98  for(unsigned i=0; i<sub_size; i++)
99  dest.push_back(tmp[i]);
100  }
101  else
102  error=true;
103  }
104 
105  if(!error)
106  return;
107 
108  dest.clear();
109  }
110  else if(expr.id()==ID_equal ||
111  expr.id()==ID_notequal ||
112  expr.id()==ID_le ||
113  expr.id()==ID_ge ||
114  expr.id()==ID_lt ||
115  expr.id()==ID_gt)
116  {
117  if(expr.operands().size()!=2)
118  throw id2string(expr.id())+" expects two operands";
119 
120  std::vector<mp_integer> tmp0, tmp1;
121  evaluate(expr.op0(), tmp0);
122  evaluate(expr.op1(), tmp1);
123 
124  if(tmp0.size()==1 && tmp1.size()==1)
125  {
126  const mp_integer &op0=tmp0.front();
127  const mp_integer &op1=tmp1.front();
128 
129  if(expr.id()==ID_equal)
130  dest.push_back(op0==op1);
131  else if(expr.id()==ID_notequal)
132  dest.push_back(op0!=op1);
133  else if(expr.id()==ID_le)
134  dest.push_back(op0<=op1);
135  else if(expr.id()==ID_ge)
136  dest.push_back(op0>=op1);
137  else if(expr.id()==ID_lt)
138  dest.push_back(op0<op1);
139  else if(expr.id()==ID_gt)
140  dest.push_back(op0>op1);
141  }
142 
143  return;
144  }
145  else if(expr.id()==ID_or)
146  {
147  if(expr.operands().empty())
148  throw id2string(expr.id())+" expects at least one operand";
149 
150  bool result=false;
151 
152  forall_operands(it, expr)
153  {
154  std::vector<mp_integer> tmp;
155  evaluate(*it, tmp);
156 
157  if(tmp.size()==1 && tmp.front()!=0)
158  {
159  result=true;
160  break;
161  }
162  }
163 
164  dest.push_back(result);
165 
166  return;
167  }
168  else if(expr.id()==ID_if)
169  {
170  if(expr.operands().size()!=3)
171  throw "if expects three operands";
172 
173  std::vector<mp_integer> tmp0, tmp1, tmp2;
174  evaluate(expr.op0(), tmp0);
175  evaluate(expr.op1(), tmp1);
176  evaluate(expr.op2(), tmp2);
177 
178  if(tmp0.size()==1 && tmp1.size()==1 && tmp2.size()==1)
179  {
180  const mp_integer &op0=tmp0.front();
181  const mp_integer &op1=tmp1.front();
182  const mp_integer &op2=tmp2.front();
183 
184  dest.push_back(op0!=0?op1:op2);
185  }
186 
187  return;
188  }
189  else if(expr.id()==ID_and)
190  {
191  if(expr.operands().empty())
192  throw id2string(expr.id())+" expects at least one operand";
193 
194  bool result=true;
195 
196  forall_operands(it, expr)
197  {
198  std::vector<mp_integer> tmp;
199  evaluate(*it, tmp);
200 
201  if(tmp.size()==1 && tmp.front()==0)
202  {
203  result=false;
204  break;
205  }
206  }
207 
208  dest.push_back(result);
209 
210  return;
211  }
212  else if(expr.id()==ID_not)
213  {
214  if(expr.operands().size()!=1)
215  throw id2string(expr.id())+" expects one operand";
216 
217  std::vector<mp_integer> tmp;
218  evaluate(expr.op0(), tmp);
219 
220  if(tmp.size()==1)
221  dest.push_back(tmp.front()==0);
222 
223  return;
224  }
225  else if(expr.id()==ID_plus)
226  {
227  mp_integer result=0;
228 
229  forall_operands(it, expr)
230  {
231  std::vector<mp_integer> tmp;
232  evaluate(*it, tmp);
233  if(tmp.size()==1)
234  result+=tmp.front();
235  }
236 
237  dest.push_back(result);
238  return;
239  }
240  else if(expr.id()==ID_mult)
241  {
242  // type-dependent!
243  mp_integer result;
244 
245  if(expr.type().id()==ID_fixedbv)
246  {
247  fixedbvt f;
249  f.from_integer(1);
250  result=f.get_value();
251  }
252  else if(expr.type().id()==ID_floatbv)
253  {
254  ieee_floatt f(to_floatbv_type(expr.type()));
255  f.from_integer(1);
256  result=f.pack();
257  }
258  else
259  result=1;
260 
261  forall_operands(it, expr)
262  {
263  std::vector<mp_integer> tmp;
264  evaluate(*it, tmp);
265  if(tmp.size()==1)
266  {
267  if(expr.type().id()==ID_fixedbv)
268  {
269  fixedbvt f1, f2;
271  f2.spec=fixedbv_spect(to_fixedbv_type(it->type()));
272  f1.set_value(result);
273  f2.set_value(tmp.front());
274  f1*=f2;
275  result=f1.get_value();
276  }
277  else if(expr.type().id()==ID_floatbv)
278  {
279  ieee_floatt f1(to_floatbv_type(expr.type()));
280  ieee_floatt f2(to_floatbv_type(it->type()));
281  f1.unpack(result);
282  f2.unpack(tmp.front());
283  f1*=f2;
284  result=f2.pack();
285  }
286  else
287  result*=tmp.front();
288  }
289  }
290 
291  dest.push_back(result);
292  return;
293  }
294  else if(expr.id()==ID_minus)
295  {
296  if(expr.operands().size()!=2)
297  throw "- expects two operands";
298 
299  std::vector<mp_integer> tmp0, tmp1;
300  evaluate(expr.op0(), tmp0);
301  evaluate(expr.op1(), tmp1);
302 
303  if(tmp0.size()==1 && tmp1.size()==1)
304  dest.push_back(tmp0.front()-tmp1.front());
305  return;
306  }
307  else if(expr.id()==ID_div)
308  {
309  if(expr.operands().size()!=2)
310  throw "/ expects two operands";
311 
312  std::vector<mp_integer> tmp0, tmp1;
313  evaluate(expr.op0(), tmp0);
314  evaluate(expr.op1(), tmp1);
315 
316  if(tmp0.size()==1 && tmp1.size()==1)
317  dest.push_back(tmp0.front()/tmp1.front());
318  return;
319  }
320  else if(expr.id()==ID_unary_minus)
321  {
322  if(expr.operands().size()!=1)
323  throw "unary- expects one operand";
324 
325  std::vector<mp_integer> tmp0;
326  evaluate(expr.op0(), tmp0);
327 
328  if(tmp0.size()==1)
329  dest.push_back(-tmp0.front());
330  return;
331  }
332  else if(expr.id()==ID_address_of)
333  {
334  if(expr.operands().size()!=1)
335  throw "address_of expects one operand";
336 
337  dest.push_back(evaluate_address(expr.op0()));
338  return;
339  }
340  else if(expr.id()==ID_dereference ||
341  expr.id()==ID_index ||
342  expr.id()==ID_symbol ||
343  expr.id()==ID_member)
344  {
346  dest.resize(get_size(expr.type()));
347  read(a, dest);
348  return;
349  }
350  else if(expr.id()==ID_typecast)
351  {
352  if(expr.operands().size()!=1)
353  throw "typecast expects one operand";
354 
355  std::vector<mp_integer> tmp;
356  evaluate(expr.op0(), tmp);
357 
358  if(tmp.size()==1)
359  {
360  const mp_integer &value=tmp.front();
361 
362  if(expr.type().id()==ID_pointer)
363  {
364  dest.push_back(value);
365  return;
366  }
367  else if(expr.type().id()==ID_signedbv)
368  {
369  const std::string s=
370  integer2binary(value, to_signedbv_type(expr.type()).get_width());
371  dest.push_back(binary2integer(s, true));
372  return;
373  }
374  else if(expr.type().id()==ID_unsignedbv)
375  {
376  const std::string s=
377  integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
378  dest.push_back(binary2integer(s, false));
379  return;
380  }
381  else if(expr.type().id()==ID_bool)
382  {
383  dest.push_back(value!=0);
384  return;
385  }
386  }
387  }
388  else if(expr.id()==ID_ashr)
389  {
390  if(expr.operands().size()!=2)
391  throw "ashr expects two operands";
392 
393  std::vector<mp_integer> tmp0, tmp1;
394  evaluate(expr.op0(), tmp0);
395  evaluate(expr.op1(), tmp1);
396 
397  if(tmp0.size()==1 && tmp1.size()==1)
398  dest.push_back(tmp0.front()/power(2, tmp1.front()));
399 
400  return;
401  }
402 
403  std::cout << "!! failed to evaluate expression: "
404  << from_expr(ns, function->first, expr)
405  << '\n';
406 }
407 
409 {
410  if(expr.id()==ID_symbol)
411  {
412  const irep_idt &identifier=expr.get(ID_identifier);
413 
414  interpretert::memory_mapt::const_iterator m_it1=
415  memory_map.find(identifier);
416 
417  if(m_it1!=memory_map.end())
418  return m_it1->second;
419 
420  if(!call_stack.empty())
421  {
422  interpretert::memory_mapt::const_iterator m_it2=
423  call_stack.top().local_map.find(identifier);
424 
425  if(m_it2!=call_stack.top().local_map.end())
426  return m_it2->second;
427  }
428  }
429  else if(expr.id()==ID_dereference)
430  {
431  if(expr.operands().size()!=1)
432  throw "dereference expects one operand";
433 
434  std::vector<mp_integer> tmp0;
435  evaluate(expr.op0(), tmp0);
436 
437  if(tmp0.size()==1)
438  return tmp0.front();
439  }
440  else if(expr.id()==ID_index)
441  {
442  if(expr.operands().size()!=2)
443  throw "index expects two operands";
444 
445  std::vector<mp_integer> tmp1;
446  evaluate(expr.op1(), tmp1);
447 
448  if(tmp1.size()==1)
449  return evaluate_address(expr.op0())+tmp1.front();
450  }
451  else if(expr.id()==ID_member)
452  {
453  if(expr.operands().size()!=1)
454  throw "member expects one operand";
455 
456  const struct_typet &struct_type=
457  to_struct_type(ns.follow(expr.op0().type()));
458 
459  const irep_idt &component_name=
461 
462  unsigned offset=0;
463 
464  for(const auto &comp : struct_type.components())
465  {
466  if(comp.get_name()==component_name)
467  break;
468 
469  offset+=get_size(comp.type());
470  }
471 
472  return evaluate_address(expr.op0())+offset;
473  }
474 
475  std::cout << "!! failed to evaluate address: "
476  << from_expr(ns, function->first, expr)
477  << '\n';
478 
479  return 0;
480 }
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
exprt & op0()
Definition: expr.h:84
void from_expr(const constant_exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
void read(mp_integer address, std::vector< mp_integer > &dest) const
const componentst & components() const
Definition: std_types.h:242
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
const mp_integer & get_value() const
Definition: fixedbv.h:95
const irep_idt & id() const
Definition: irep.h:189
Interpreter for GOTO Programs.
fixedbv_spect spec
Definition: fixedbv.h:44
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:312
goto_functionst::function_mapt::const_iterator function
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
#define forall_operands(it, expr)
Definition: expr.h:17
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
unsigned get_size(const typet &type) const
const namespacet ns
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
Base class for all expressions.
Definition: expr.h:46
mp_integer pack() const
Definition: ieee_float.cpp:367
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
irep_idt get_component_name() const
Definition: std_expr.h:3249
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
mp_integer evaluate_address(const exprt &expr) const
memory_mapt memory_map
call_stackt call_stack
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
operandst & operands()
Definition: expr.h:70
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.