cprover
path_symex_state_read.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: State of path-based symbolic simulator
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "path_symex_state.h"
13 
14 #include <util/simplify_expr.h>
15 #include <util/arith_tools.h>
16 
18 
19 #ifdef DEBUG
20 #include <iostream>
21 #include <langapi/language_util.h>
22 #endif
23 
24 exprt path_symex_statet::read(const exprt &src, bool propagate)
25 {
26  #ifdef DEBUG
27  // std::cout << "path_symex_statet::read " << src.pretty() << '\n';
28  #endif
29 
30  // This has three phases!
31  // 1. Dereferencing, including propagation of pointers.
32  // 2. Rewriting to SSA symbols
33  // 3. Simplifier
34 
35  // we force propagation for dereferencing
36  exprt tmp3=dereference_rec(src, true);
37 
38  exprt tmp4=instantiate_rec(tmp3, propagate);
39 
40  exprt tmp5=simplify_expr(tmp4, var_map.ns);
41 
42  #ifdef DEBUG
43  // std::cout << " ==> " << tmp.pretty() << '\n';
44  #endif
45 
46  return tmp5;
47 }
48 
50 {
51  #ifdef DEBUG
52  std::cout << "expand_structs_and_arrays: "
53  << from_expr(var_map.ns, "", src) << '\n';
54  #endif
55 
56  const typet &src_type=var_map.ns.follow(src.type());
57 
58  if(src_type.id()==ID_struct) // src is a struct
59  {
60  const struct_typet &struct_type=to_struct_type(src_type);
61  const struct_typet::componentst &components=struct_type.components();
62 
63  struct_exprt result(src.type());
64  result.operands().resize(components.size());
65 
66  // split it up into components
67  for(unsigned i=0; i<components.size(); i++)
68  {
69  const typet &subtype=components[i].type();
70  const irep_idt &component_name=components[i].get_name();
71 
72  exprt new_src;
73  if(src.id()==ID_struct) // struct constructor?
74  {
75  assert(src.operands().size()==components.size());
76  new_src=src.operands()[i];
77  }
78  else
79  new_src=member_exprt(src, component_name, subtype);
80 
81  // recursive call
82  result.operands()[i]=expand_structs_and_arrays(new_src);
83  }
84 
85  return result; // done
86  }
87  else if(src_type.id()==ID_array) // src is an array
88  {
89  const array_typet &array_type=to_array_type(src_type);
90  const typet &subtype=array_type.subtype();
91 
92  if(array_type.size().is_constant())
93  {
94  mp_integer size;
95  if(to_integer(array_type.size(), size))
96  throw "failed to convert array size";
97 
98  std::size_t size_int=integer2size_t(size);
99 
100  array_exprt result(array_type);
101  result.operands().resize(size_int);
102 
103  // split it up into elements
104  for(std::size_t i=0; i<size_int; ++i)
105  {
106  exprt index=from_integer(i, array_type.size().type());
107  exprt new_src=index_exprt(src, index, subtype);
108 
109  // array constructor?
110  if(src.id()==ID_array)
111  new_src=simplify_expr(new_src, var_map.ns);
112 
113  // recursive call
114  result.operands()[i]=expand_structs_and_arrays(new_src);
115  }
116 
117  return result; // done
118  }
119  else
120  {
121  // TODO: variable-sized array
122  }
123  }
124  else if(src_type.id()==ID_vector) // src is a vector
125  {
126  const vector_typet &vector_type=to_vector_type(src_type);
127  const typet &subtype=vector_type.subtype();
128 
129  if(!vector_type.size().is_constant())
130  throw "vector with non-constant size";
131 
132  mp_integer size;
133  if(to_integer(vector_type.size(), size))
134  throw "failed to convert vector size";
135 
136  std::size_t size_int=integer2size_t(size);
137 
138  vector_exprt result(vector_type);
139  exprt::operandst &operands=result.operands();
140  operands.resize(size_int);
141 
142  // split it up into elements
143  for(std::size_t i=0; i<size_int; ++i)
144  {
145  exprt index=from_integer(i, vector_type.size().type());
146  exprt new_src=index_exprt(src, index, subtype);
147 
148  // vector constructor?
149  if(src.id()==ID_vector)
150  new_src=simplify_expr(new_src, var_map.ns);
151 
152  // recursive call
153  operands[i]=expand_structs_and_arrays(new_src);
154  }
155 
156  return result; // done
157  }
158 
159  return src;
160 }
161 
162 exprt path_symex_statet::array_theory(const exprt &src, bool propagate)
163 {
164  // top-level constant-sized arrays only right now
165 
166  if(src.id()==ID_index)
167  {
168  const index_exprt &index_expr=to_index_expr(src);
169  exprt index_tmp1=read(index_expr.index(), propagate);
170  exprt index_tmp2=simplify_expr(index_tmp1, var_map.ns);
171 
172  if(!index_tmp2.is_constant())
173  {
174  const array_typet &array_type=to_array_type(index_expr.array().type());
175  const typet &subtype=array_type.subtype();
176 
177  if(array_type.size().is_constant())
178  {
179  mp_integer size;
180  if(to_integer(array_type.size(), size))
181  throw "failed to convert array size";
182 
183  std::size_t size_int=integer2size_t(size);
184 
185  exprt result=nil_exprt();
186 
187  // split it up
188  for(std::size_t i=0; i<size_int; ++i)
189  {
190  exprt index=from_integer(i, index_expr.index().type());
191  exprt new_src=index_exprt(index_expr.array(), index, subtype);
192 
193  if(result.is_nil())
194  result=new_src;
195  else
196  {
197  equal_exprt index_equal(index_expr.index(), index);
198  result=if_exprt(index_equal, new_src, result);
199  }
200  }
201 
202  return result; // done
203  }
204  else
205  {
206  // TODO: variable-sized array
207  }
208  }
209  }
210 
211  return src;
212 }
213 
215  const exprt &src,
216  bool propagate)
217 {
218  #ifdef DEBUG
219  std::cout << "instantiate_rec: "
220  << from_expr(var_map.ns, "", src) << '\n';
221  #endif
222 
223  // check whether this is a symbol(.member|[index])*
224 
225  if(is_symbol_member_index(src))
226  {
227  exprt tmp_symbol_member_index=
228  read_symbol_member_index(src, propagate);
229 
230  assert(tmp_symbol_member_index.is_not_nil());
231  return tmp_symbol_member_index; // yes!
232  }
233 
234  if(src.id()==ID_address_of)
235  {
236  assert(src.operands().size()==1);
237  exprt tmp=src;
238  tmp.op0()=instantiate_rec_address(tmp.op0(), propagate);
239  return tmp;
240  }
241  else if(src.id()==ID_side_effect)
242  {
243  // could be done separately
244  const irep_idt &statement=to_side_effect_expr(src).get_statement();
245 
246  if(statement==ID_nondet)
247  {
248  irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
250 
251  auxiliary_symbolt nondet_symbol;
252  nondet_symbol.name=id;
253  nondet_symbol.base_name=id;
254  nondet_symbol.type=src.type();
255  var_map.new_symbols.add(nondet_symbol);
256 
257  return nondet_symbol.symbol_expr();
258  }
259  else
260  throw "instantiate_rec: unexpected side effect "+id2string(statement);
261  }
262  else if(src.id()==ID_dereference)
263  {
264  // dereferencet has run already, so we should only be left with
265  // integer addresses. Will transform into __CPROVER_memory[]
266  // eventually.
267  }
268  else if(src.id()==ID_member)
269  {
270  const typet &compound_type=
271  var_map.ns.follow(to_member_expr(src).struct_op().type());
272 
273  if(compound_type.id()==ID_struct)
274  {
275  // do nothing
276  }
277  else if(compound_type.id()==ID_union)
278  {
279  // should already have been rewritten to byte_extract
280  throw "unexpected union member";
281  }
282  else
283  {
284  throw "member expects struct or union type"+src.pretty();
285  }
286  }
287  else if(src.id()==ID_byte_extract_little_endian ||
288  src.id()==ID_byte_extract_big_endian)
289  {
290  }
291  else if(src.id()==ID_symbol)
292  {
293  // must be SSA already, or code
294  assert(src.type().id()==ID_code ||
295  src.get_bool(ID_C_SSA_symbol));
296  }
297 
298  if(!src.has_operands())
299  return src;
300 
301  exprt src2=src;
302 
303  // recursive calls on structure of 'src'
304  Forall_operands(it, src2)
305  {
306  exprt tmp_op=instantiate_rec(*it, propagate);
307  *it=tmp_op;
308  }
309 
310  return src2;
311 }
312 
314  const exprt &src,
315  bool propagate)
316 {
317  const typet &src_type=var_map.ns.follow(src.type());
318 
319  // don't touch function symbols
320  if(src_type.id()==ID_code)
321  return nil_exprt();
322 
323  // is this a struct/array/vector that needs to be expanded?
324  exprt final=expand_structs_and_arrays(src);
325 
326  if(final.id()==ID_struct ||
327  final.id()==ID_array ||
328  final.id()==ID_vector)
329  {
330  Forall_operands(it, final)
331  *it=read_symbol_member_index(*it, propagate); // rec. call
332  return final;
333  }
334 
335  // now do array theory
336  final=array_theory(final, propagate);
337 
338  if(final.id()==ID_if)
339  {
340  assert(final.operands().size()==3);
341  final.op0()=instantiate_rec(final.op0(), propagate); // rec. call
342  final.op1()=read_symbol_member_index(final.op1(), propagate); // rec. call
343  final.op2()=read_symbol_member_index(final.op2(), propagate); // rec. call
344  return final;
345  }
346 
347  std::string suffix="";
348  exprt current=src;
349 
350  // the loop avoids recursion
351  while(current.id()!=ID_symbol)
352  {
353  exprt next=nil_exprt();
354 
355  if(current.id()==ID_member)
356  {
357  const member_exprt &member_expr=to_member_expr(current);
358 
359  const typet &compound_type=
360  var_map.ns.follow(member_expr.struct_op().type());
361 
362  if(compound_type.id()==ID_struct)
363  {
364  // go into next iteration
365  next=member_expr.struct_op();
366  suffix="."+id2string(member_expr.get_component_name())+suffix;
367  }
368  else
369  return nil_exprt(); // includes unions, deliberately
370  }
371  else if(current.id()==ID_index)
372  {
373  const index_exprt &index_expr=to_index_expr(current);
374 
375  exprt index_tmp=read(index_expr.index(), propagate);
376 
377  std::string index_string=array_index_as_string(index_tmp);
378 
379  // go into next iteration
380  next=index_expr.array();
381  suffix=index_string+suffix;
382  }
383  else
384  return nil_exprt();
385 
386  // next round
387  assert(next.is_not_nil());
388  current=next;
389  }
390 
391  assert(current.id()==ID_symbol);
392 
393  if(current.get_bool(ID_C_SSA_symbol))
394  return nil_exprt(); // SSA already
395 
396  irep_idt identifier=
397  to_symbol_expr(current).get_identifier();
398 
399  var_mapt::var_infot &var_info=
400  var_map(identifier, suffix, src.type());
401 
402  #ifdef DEBUG
403  std::cout << "read_symbol_member_index_rec " << identifier
404  << " var_info " << var_info.full_identifier << '\n';
405  #endif
406 
407  // warning: reference is not stable
408  var_statet &var_state=get_var_state(var_info);
409 
410  if(propagate && var_state.value.is_not_nil())
411  {
412  return var_state.value; // propagate a value
413  }
414  else
415  {
416  // we do some SSA symbol
417  if(var_state.ssa_symbol.get_identifier().empty())
418  {
419  // produce one
420  var_state.ssa_symbol=var_info.ssa_symbol();
421  }
422 
423  return var_state.ssa_symbol;
424  }
425 }
426 
428 {
429  const typet final_type=src.type();
430 
431  // don't touch function symbols
432  if(var_map.ns.follow(final_type).id()==ID_code)
433  return false;
434 
435  const exprt *current=&src;
436 
437  // the loop avoids recursion
438  while(true)
439  {
440  const exprt *next=nullptr;
441 
442  if(current->id()==ID_symbol)
443  {
444  if(current->get_bool(ID_C_SSA_symbol))
445  return false; // SSA already
446 
447  return true;
448  }
449  else if(current->id()==ID_member)
450  {
451  const member_exprt &member_expr=to_member_expr(*current);
452 
453  const typet &compound_type=
454  var_map.ns.follow(member_expr.struct_op().type());
455 
456  if(compound_type.id()==ID_struct)
457  {
458  // go into next iteration
459  next=&(member_expr.struct_op());
460  }
461  else
462  return false; // includes unions, deliberately
463  }
464  else if(current->id()==ID_index)
465  {
466  const index_exprt &index_expr=to_index_expr(*current);
467 
468  // go into next iteration
469  next=&(index_expr.array());
470  }
471  else
472  return false;
473 
474  // next round
475  INVARIANT_STRUCTURED(next!=nullptr, nullptr_exceptiont, "next is null");
476  current=next;
477  }
478 }
479 
480 std::string path_symex_statet::array_index_as_string(const exprt &src) const
481 {
482  exprt tmp=simplify_expr(src, var_map.ns);
483  mp_integer i;
484 
485  if(!to_integer(tmp, i))
486  return "["+integer2string(i)+"]";
487  else
488  return "[*]";
489 }
490 
492  const exprt &src,
493  bool propagate)
494 {
495  if(src.id()==ID_dereference)
496  {
497  const dereference_exprt &dereference_expr=to_dereference_expr(src);
498 
499  // read the address to propagate the pointers
500  exprt address=read(dereference_expr.pointer(), propagate);
501 
502  // now hand over to dereference
503  exprt address_dereferenced=::dereference(address, var_map.ns);
504 
505  // the dereferenced address is a mixture of non-SSA and SSA symbols
506  // (e.g., if-guards and array indices)
507  return address_dereferenced;
508  }
509 
510  if(!src.has_operands())
511  return src;
512 
513  exprt src2=src;
514 
515  {
516  // recursive calls on structure of 'src'
517  Forall_operands(it, src2)
518  {
519  exprt tmp_op=dereference_rec(*it, propagate);
520  *it=tmp_op;
521  }
522  }
523 
524  return src2;
525 }
526 
528  const exprt &src,
529  bool propagate)
530 {
531  #ifdef DEBUG
532  std::cout << "instantiate_rec_address: " << src.id() << '\n';
533  #endif
534 
535  if(src.id()==ID_symbol)
536  {
537  return src;
538  }
539  else if(src.id()==ID_index)
540  {
541  assert(src.operands().size()==2);
542  exprt tmp=src;
543  tmp.op0()=instantiate_rec_address(src.op0(), propagate);
544  tmp.op1()=instantiate_rec(src.op1(), propagate);
545  return tmp;
546  }
547  else if(src.id()==ID_dereference)
548  {
549  // dereferenct ran before, and this can only be *(type *)integer-address,
550  // which we simply instantiate as non-address
552  tmp.pointer()=instantiate_rec(tmp.pointer(), propagate);
553  return tmp;
554  }
555  else if(src.id()==ID_member)
556  {
557  member_exprt tmp=to_member_expr(src);
558  tmp.struct_op()=instantiate_rec_address(tmp.struct_op(), propagate);
559  return tmp;
560  }
561  else if(src.id()==ID_string_constant)
562  {
563  return src;
564  }
565  else if(src.id()==ID_label)
566  {
567  return src;
568  }
569  else if(src.id()==ID_byte_extract_big_endian ||
570  src.id()==ID_byte_extract_little_endian)
571  {
572  assert(src.operands().size()==2);
573  exprt tmp=src;
574  tmp.op0()=instantiate_rec_address(src.op0(), propagate);
575  tmp.op1()=instantiate_rec(src.op1(), propagate);
576  return tmp;
577  }
578  else if(src.id()==ID_if)
579  {
580  if_exprt if_expr=to_if_expr(src);
581  if_expr.true_case()=
582  instantiate_rec_address(if_expr.true_case(), propagate);
583  if_expr.false_case()=
584  instantiate_rec_address(if_expr.false_case(), propagate);
585  if_expr.cond()=instantiate_rec(if_expr.cond(), propagate);
586  return if_expr;
587  }
588  else
589  {
590  // this shouldn't really happen
591  #ifdef DEBUG
592  std::cout << "SRC: " << src.pretty() << '\n';
593  #endif
594  throw "address of unexpected `"+src.id_string()+"'";
595  }
596 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:209
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
BigInt mp_integer
Definition: mp_arith.h:19
symbol_tablet new_symbols
Definition: var_map.h:102
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
exprt & op0()
Definition: expr.h:84
exprt instantiate_rec(const exprt &src, bool propagate)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
Definition: std_types.h:240
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const componentst & components() const
Definition: std_types.h:242
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
typet & type()
Definition: expr.h:60
exprt instantiate_rec_address(const exprt &src, bool propagate)
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
symbol_exprt ssa_symbol() const
Definition: var_map.h:61
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
exprt array_theory(const exprt &src, bool propagate)
Extract member of struct or union.
Definition: std_expr.h:3214
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
std::string array_index_as_string(const exprt &) const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
exprt read(const exprt &src)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
The NIL expression.
Definition: std_expr.h:3764
Operator to dereference a pointer.
Definition: std_expr.h:2701
A constant-size array type.
Definition: std_types.h:1554
exprt & op1()
Definition: expr.h:87
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
const exprt & size() const
Definition: std_types.h:1568
const exprt & size() const
Definition: std_types.h:915
var_statet & get_var_state(const var_mapt::var_infot &var_info)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
vector constructor from list of elements
Definition: std_expr.h:1349
exprt & false_case()
Definition: std_expr.h:2815
bool has_operands() const
Definition: expr.h:67
exprt dereference_rec(const exprt &src, bool propagate)
bool is_constant() const
Definition: expr.cpp:128
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
exprt read_symbol_member_index(const exprt &src, bool propagate)
exprt expand_structs_and_arrays(const exprt &src)
typet type
Type of symbol.
Definition: symbol.h:37
State of path-based symbolic simulator.
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
irep_idt get_component_name() const
Definition: std_expr.h:3249
unsigned nondet_count
Definition: var_map.h:110
const std::string & id_string() const
Definition: irep.h:192
#define Forall_operands(it, expr)
Definition: expr.h:23
arrays with given size
Definition: std_types.h:901
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const namespacet ns
Definition: var_map.h:101
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:31
bool is_symbol_member_index(const exprt &src) const
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1464
Pointer Dereferencing.
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
array constructor from list of elements
Definition: std_expr.h:1309
irep_idt full_identifier
Definition: var_map.h:48
const irep_idt & get_statement() const
Definition: std_code.h:1012
array index operator
Definition: std_expr.h:1170