cprover
path_symex.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Concrete Symbolic Transformer
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "path_symex.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/simplify_expr.h>
16 #include <util/string2int.h>
17 #include <util/byte_operators.h>
19 #include <util/base_type.h>
20 #include <util/prefix.h>
21 #include <util/c_types.h>
22 
24 
26 
27 #include "path_symex_class.h"
28 
29 #ifdef DEBUG
30 #include <iostream>
31 #endif
32 
33 bool path_symext::propagate(const exprt &src)
34 {
35  // propagate things that are 'simple enough'
36  if(src.is_constant())
37  return true;
38  else if(src.id()==ID_member)
39  return propagate(to_member_expr(src).struct_op());
40  else if(src.id()==ID_index)
41  return false;
42  else if(src.id()==ID_typecast)
43  return propagate(to_typecast_expr(src).op());
44  else if(src.id()==ID_symbol)
45  return true;
46  else if(src.id()==ID_address_of)
47  return true;
48  else if(src.id()==ID_plus)
49  {
50  forall_operands(it, src)
51  if(!propagate(*it))
52  return false;
53  return true;
54  }
55  else if(src.id()==ID_array)
56  {
57  forall_operands(it, src)
58  if(!propagate(*it))
59  return false;
60  return true;
61  }
62  else if(src.id()==ID_vector)
63  {
64  forall_operands(it, src)
65  if(!propagate(*it))
66  return false;
67  return true;
68  }
69  else if(src.id()==ID_if)
70  {
71  const if_exprt &if_expr=to_if_expr(src);
72  if(!propagate(if_expr.true_case()))
73  return false;
74  if(!propagate(if_expr.false_case()))
75  return false;
76  return true;
77  }
78  else if(src.id()==ID_array_of)
79  {
80  return propagate(to_array_of_expr(src).what());
81  }
82  else if(src.id()==ID_union)
83  {
84  return propagate(to_union_expr(src).op());
85  }
86  else
87  {
88  return false;
89  }
90 }
91 
93  path_symex_statet &state,
94  const exprt &lhs,
95  const exprt &rhs)
96 {
97  if(rhs.id()==ID_side_effect) // catch side effects on rhs
98  {
99  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
100  const irep_idt &statement=side_effect_expr.get_statement();
101 
102  if(statement==ID_malloc)
103  {
104  symex_malloc(state, lhs, side_effect_expr);
105  return;
106  }
107  else if(statement==ID_nondet)
108  {
109  // done in statet:instantiate_rec
110  }
111  else if(statement==ID_gcc_builtin_va_arg_next)
112  {
113  symex_va_arg_next(state, lhs, side_effect_expr);
114  return;
115  }
116  else
117  throw "unexpected side-effect on rhs: "+id2string(statement);
118  }
119 
120  // read the address of the lhs, with propagation
121  exprt lhs_address=state.read(address_of_exprt(lhs));
122 
123  // now SSA the lhs, no propagation
124  exprt ssa_lhs=
125  state.read_no_propagate(dereference_exprt(lhs_address));
126 
127  // read the rhs
128  exprt ssa_rhs=state.read(rhs);
129 
130  // start recursion on lhs
131  exprt::operandst _guard; // start with empty guard
132  assign_rec(state, _guard, ssa_lhs, ssa_rhs);
133 }
134 
135 inline static typet c_sizeof_type_rec(const exprt &expr)
136 {
137  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
138 
139  if(!sizeof_type.is_nil())
140  {
141  return static_cast<const typet &>(sizeof_type);
142  }
143  else if(expr.id()==ID_mult)
144  {
145  forall_operands(it, expr)
146  {
147  typet t=c_sizeof_type_rec(*it);
148  if(t.is_not_nil())
149  return t;
150  }
151  }
152 
153  return nil_typet();
154 }
155 
157  path_symex_statet &state,
158  const exprt &lhs,
159  const side_effect_exprt &code)
160 {
161  if(code.operands().size()!=1)
162  throw "malloc expected to have one operand";
163 
164  // increment dynamic object counter
165  unsigned dynamic_count=++state.var_map.dynamic_count;
166 
167  exprt size=code.op0();
168  typet object_type=nil_typet();
169 
170  {
171  exprt tmp_size=state.read(size); // to allow constant propagation
172 
173  // special treatment for sizeof(T)*x
174  if(tmp_size.id()==ID_mult &&
175  tmp_size.operands().size()==2 &&
176  tmp_size.op0().find(ID_C_c_sizeof_type).is_not_nil())
177  {
178  object_type=array_typet(
179  c_sizeof_type_rec(tmp_size.op0()),
180  tmp_size.op1());
181  }
182  else
183  {
184  typet tmp_type=c_sizeof_type_rec(tmp_size);
185 
186  if(tmp_type.is_not_nil())
187  {
188  // Did the size get multiplied?
189  mp_integer elem_size=pointer_offset_size(tmp_type, state.var_map.ns);
190  mp_integer alloc_size;
191  if(elem_size<0 || to_integer(tmp_size, alloc_size))
192  {
193  }
194  else
195  {
196  if(alloc_size==elem_size)
197  object_type=tmp_type;
198  else
199  {
200  mp_integer elements=alloc_size/elem_size;
201 
202  if(elements*elem_size==alloc_size)
203  object_type=
204  array_typet(tmp_type, from_integer(elements, tmp_size.type()));
205  }
206  }
207  }
208  }
209 
210  if(object_type.is_nil())
211  object_type=array_typet(unsigned_char_type(), tmp_size);
212 
213  // we introduce a fresh symbol for the size
214  // to prevent any issues of the size getting ever changed
215 
216  if(object_type.id()==ID_array &&
217  !to_array_type(object_type).size().is_constant())
218  {
219  exprt &size=to_array_type(object_type).size();
220 
221  symbolt size_symbol;
222 
223  size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_count);
224  size_symbol.name="symex::"+id2string(size_symbol.base_name);
225  size_symbol.is_lvalue=true;
226  size_symbol.type=tmp_size.type();
227  size_symbol.mode=ID_C;
228 
229  assign(state,
230  size_symbol.symbol_expr(),
231  size);
232 
233  size=size_symbol.symbol_expr();
234  }
235  }
236 
237  // value
238  symbolt value_symbol;
239 
240  value_symbol.base_name=
241  "dynamic_object"+std::to_string(state.var_map.dynamic_count);
242  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
243  value_symbol.is_lvalue=true;
244  value_symbol.type=object_type;
245  value_symbol.type.set("#dynamic", true);
246  value_symbol.mode=ID_C;
247 
248  address_of_exprt rhs;
249 
250  if(object_type.id()==ID_array)
251  {
252  rhs.type()=pointer_type(value_symbol.type.subtype());
253  index_exprt index_expr(value_symbol.type.subtype());
254  index_expr.array()=value_symbol.symbol_expr();
255  index_expr.index()=from_integer(0, index_type());
256  rhs.op0()=index_expr;
257  }
258  else
259  {
260  rhs.op0()=value_symbol.symbol_expr();
261  rhs.type()=pointer_type(value_symbol.type);
262  }
263 
264  if(rhs.type()!=lhs.type())
265  rhs.make_typecast(lhs.type());
266 
267  assign(state, lhs, rhs);
268 }
269 
270 
272  const path_symex_statet &state,
273  const exprt &src)
274 {
275  if(src.id()==ID_typecast)
276  return get_old_va_symbol(state, to_typecast_expr(src).op());
277  else if(src.id()==ID_address_of)
278  {
279  const exprt &op=to_address_of_expr(src).object();
280 
281  if(op.id()==ID_symbol)
282  return to_symbol_expr(op).get_identifier();
283  }
284 
285  return irep_idt();
286 }
287 
289  path_symex_statet &state,
290  const exprt &lhs,
291  const side_effect_exprt &code)
292 {
293  if(code.operands().size()!=1)
294  throw "va_arg_next expected to have one operand";
295 
296  if(lhs.is_nil())
297  return; // ignore
298 
299  exprt tmp=state.read(code.op0()); // constant prop on va_arg parameter
300 
301  // Get old symbol of va_arg and modify it to generate a new one.
302  irep_idt id=get_old_va_symbol(state, tmp);
303  exprt rhs=
305  lhs.type(),
306  code.source_location(),
307  state.var_map.ns);
308 
309  if(!id.empty())
310  {
311  // strip last name off id to get function name
312  std::size_t pos=id2string(id).rfind("::");
313  if(pos!=std::string::npos)
314  {
315  irep_idt function_identifier=std::string(id2string(id), 0, pos);
316  std::string base=id2string(function_identifier)+"::va_arg";
317 
318  /*
319  * Construct the identifier of the va_arg argument such that it
320  * corresponds to the respective one set upon function call
321  */
322  if(has_prefix(id2string(id), base))
323  id=base
324  +std::to_string(
326  std::string(id2string(id), base.size(), std::string::npos))
327  +1);
328  else
329  id=base+"0";
330 
331  const var_mapt::var_infot &var_info=state.var_map[id];
332 
333  if(var_info.full_identifier==id)
334  {
335  const path_symex_statet::var_statet &var_state
336  =state.get_var_state(var_info);
337  const exprt symbol_expr=symbol_exprt(id, var_state.ssa_symbol.type());
338  rhs=address_of_exprt(symbol_expr);
339  rhs.make_typecast(lhs.type());
340  }
341  }
342  }
343 
344  assign(state, lhs, rhs);
345 }
346 
348  path_symex_statet &state,
349  exprt::operandst &guard,
350  const exprt &ssa_lhs,
351  const exprt &ssa_rhs)
352 {
353  // const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type());
354 
355  #ifdef DEBUG
356  std::cout << "assign_rec: " << ssa_lhs.pretty() << '\n';
357  // std::cout << "ssa_lhs_type: " << ssa_lhs_type.id() << '\n';
358  #endif
359 
360  if(ssa_lhs.id()==ID_symbol)
361  {
362  // These are expected to be SSA symbols
363  assert(ssa_lhs.get_bool(ID_C_SSA_symbol));
364 
365  const symbol_exprt &symbol_expr=to_symbol_expr(ssa_lhs);
366  const irep_idt &full_identifier=symbol_expr.get(ID_C_full_identifier);
367 
368  #ifdef DEBUG
369  const irep_idt &ssa_identifier=symbol_expr.get_identifier();
370  std::cout << "SSA symbol identifier: " << ssa_identifier << '\n';
371  std::cout << "full identifier: " << full_identifier << '\n';
372  #endif
373 
374  var_mapt::var_infot &var_info=state.var_map[full_identifier];
375  assert(var_info.full_identifier==full_identifier);
376 
377  // increase the SSA counter and produce new SSA symbol expression
378  var_info.increment_ssa_counter();
379  symbol_exprt new_lhs=var_info.ssa_symbol();
380 
381  #ifdef DEBUG
382  std::cout << "new_lhs: " << new_lhs.get_identifier() << '\n';
383  #endif
384 
385  // record new state of lhs
386  {
387  // reference is not stable
388  path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
389  var_state.ssa_symbol=new_lhs;
390  }
391 
392  // rhs nil means non-det assignment
393  if(ssa_rhs.is_nil())
394  {
395  path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
396  var_state.value=nil_exprt();
397  }
398  else
399  {
400  // consistency check
401  if(!base_type_eq(ssa_rhs.type(), new_lhs.type(), state.var_map.ns))
402  {
403  #ifdef DEBUG
404  std::cout << "ssa_rhs: " << ssa_rhs.pretty() << '\n';
405  std::cout << "new_lhs: " << new_lhs.pretty() << '\n';
406  #endif
407  throw "assign_rec got different types";
408  }
409 
410  // record the step
411  state.record_step();
412  stept &step=*state.history;
413 
414  if(!guard.empty())
415  step.guard=conjunction(guard);
416  step.full_lhs=ssa_lhs;
417  step.ssa_lhs=new_lhs;
418  step.ssa_rhs=ssa_rhs;
419 
420  // propagate the rhs?
421  path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
422  var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
423  }
424  }
425  else if(ssa_lhs.id()==ID_typecast)
426  {
427  // dereferencing might yield a typecast
428  const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
429  typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
430 
431  assign_rec(state, guard, new_lhs, new_rhs);
432  }
433  else if(ssa_lhs.id()==ID_member)
434  {
435  #ifdef DEBUG
436  std::cout << "assign_rec ID_member\n";
437  #endif
438 
439  const member_exprt &ssa_lhs_member_expr=to_member_expr(ssa_lhs);
440  const exprt &struct_op=ssa_lhs_member_expr.struct_op();
441 
442  const typet &compound_type=
443  state.var_map.ns.follow(struct_op.type());
444 
445  if(compound_type.id()==ID_struct)
446  {
447  // We flatten the top-level structs, so this one is inside an
448  // array or a union.
449 
450  exprt member_name(ID_member_name);
451  member_name.set(
452  ID_component_name,
453  ssa_lhs_member_expr.get_component_name());
454 
455  with_exprt new_rhs(struct_op, member_name, ssa_rhs);
456 
457  assign_rec(state, guard, struct_op, new_rhs);
458  }
459  else if(compound_type.id()==ID_union)
460  {
461  // rewrite into byte_extract, and do again
462  exprt offset=from_integer(0, index_type());
463 
465  new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());
466 
467  assign_rec(state, guard, new_lhs, ssa_rhs);
468  }
469  else
470  throw "assign_rec: member expects struct or union type";
471  }
472  else if(ssa_lhs.id()==ID_index)
473  {
474  #ifdef DEBUG
475  std::cout << "assign_rec ID_index\n";
476  #endif
477 
478  throw "unexpected array index on lhs";
479  }
480  else if(ssa_lhs.id()==ID_dereference)
481  {
482  #ifdef DEBUG
483  std::cout << "assign_rec ID_dereference\n";
484  #endif
485 
486  throw "unexpected dereference on lhs";
487  }
488  else if(ssa_lhs.id()==ID_if)
489  {
490  #ifdef DEBUG
491  std::cout << "assign_rec ID_if\n";
492  #endif
493 
494  const if_exprt &lhs_if_expr=to_if_expr(ssa_lhs);
495  exprt cond=lhs_if_expr.cond();
496 
497  // true
498  guard.push_back(cond);
499  assign_rec(state, guard, lhs_if_expr.true_case(), ssa_rhs);
500  guard.pop_back();
501 
502  // false
503  guard.push_back(not_exprt(cond));
504  assign_rec(state, guard, lhs_if_expr.false_case(), ssa_rhs);
505  guard.pop_back();
506  }
507  else if(ssa_lhs.id()==ID_byte_extract_little_endian ||
508  ssa_lhs.id()==ID_byte_extract_big_endian)
509  {
510  #ifdef DEBUG
511  std::cout << "assign_rec ID_byte_extract\n";
512  #endif
513 
514  const byte_extract_exprt &byte_extract_expr=
515  to_byte_extract_expr(ssa_lhs);
516 
517  // assignment to byte_extract operators:
518  // turn into byte_update operator
519 
520  irep_idt new_id;
521 
522  if(ssa_lhs.id()==ID_byte_extract_little_endian)
523  new_id=ID_byte_update_little_endian;
524  else if(ssa_lhs.id()==ID_byte_extract_big_endian)
525  new_id=ID_byte_update_big_endian;
526  else
527  assert(false);
528 
529  byte_update_exprt new_rhs(new_id);
530 
531  new_rhs.type()=byte_extract_expr.op().type();
532  new_rhs.op()=byte_extract_expr.op();
533  new_rhs.offset()=byte_extract_expr.offset();
534  new_rhs.value()=ssa_rhs;
535 
536  const exprt new_lhs=byte_extract_expr.op();
537 
538  assign_rec(state, guard, new_lhs, new_rhs);
539  }
540  else if(ssa_lhs.id()==ID_struct)
541  {
542  const struct_typet &struct_type=
543  to_struct_type(state.var_map.ns.follow(ssa_lhs.type()));
544  const struct_typet::componentst &components=
545  struct_type.components();
546 
547  // split up into components
548  const exprt::operandst &operands=ssa_lhs.operands();
549 
550  assert(operands.size()==components.size());
551 
552  if(ssa_rhs.id()==ID_struct &&
553  ssa_rhs.operands().size()==components.size())
554  {
555  exprt::operandst::const_iterator lhs_it=operands.begin();
556  forall_operands(it, ssa_rhs)
557  {
558  assign_rec(state, guard, *lhs_it, *it);
559  ++lhs_it;
560  }
561  }
562  else
563  {
564  for(std::size_t i=0; i<components.size(); i++)
565  {
566  exprt new_rhs=
567  ssa_rhs.is_nil()?ssa_rhs:
569  member_exprt(
570  ssa_rhs,
571  components[i].get_name(),
572  components[i].type()),
573  state.var_map.ns);
574  assign_rec(state, guard, operands[i], new_rhs);
575  }
576  }
577  }
578  else if(ssa_lhs.id()==ID_array)
579  {
580  const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type());
581 
582  if(ssa_lhs_type.id()!=ID_array)
583  throw "array constructor must have array type";
584 
585  const array_typet &array_type=
586  to_array_type(ssa_lhs_type);
587 
588  const exprt::operandst &operands=ssa_lhs.operands();
589 
590  // split up into elements
591  if(ssa_rhs.id()==ID_array &&
592  ssa_rhs.operands().size()==operands.size())
593  {
594  exprt::operandst::const_iterator lhs_it=operands.begin();
595  forall_operands(it, ssa_rhs)
596  {
597  assign_rec(state, guard, *lhs_it, *it);
598  ++lhs_it;
599  }
600  }
601  else
602  {
603  for(std::size_t i=0; i<operands.size(); i++)
604  {
605  exprt new_rhs=
606  ssa_rhs.is_nil()?ssa_rhs:
608  index_exprt(
609  ssa_rhs,
610  from_integer(i, index_type()),
611  array_type.subtype()),
612  state.var_map.ns);
613  assign_rec(state, guard, operands[i], new_rhs);
614  }
615  }
616  }
617  else if(ssa_lhs.id()==ID_string_constant ||
618  ssa_lhs.id()=="NULL-object" ||
619  ssa_lhs.id()=="zero_string" ||
620  ssa_lhs.id()=="is_zero_string" ||
621  ssa_lhs.id()=="zero_string_length")
622  {
623  // ignore
624  }
625  else
626  {
627  // ignore
628  throw "path_symext::assign_rec(): unexpected lhs: "+ssa_lhs.id_string();
629  }
630 }
631 
633  path_symex_statet &state,
634  const code_function_callt &call,
635  const exprt &function,
636  std::list<path_symex_statet> &further_states)
637 {
638  #ifdef DEBUG
639  std::cout << "function_call_rec: " << function.pretty() << '\n';
640  #endif
641 
642  if(function.id()==ID_symbol)
643  {
644  const irep_idt &function_identifier=
645  to_symbol_expr(function).get_identifier();
646 
647  // find the function
648  locst::function_mapt::const_iterator f_it=
649  state.locs.function_map.find(function_identifier);
650 
651  if(f_it==state.locs.function_map.end())
652  throw
653  "failed to find `"+id2string(function_identifier)+"' in function_map";
654 
655  const locst::function_entryt &function_entry=f_it->second;
656 
657  loc_reft function_entry_point=function_entry.first_loc;
658 
659  // do we have a body?
660  if(function_entry_point==loc_reft())
661  {
662  // no body
663 
664  // this is a skip
665  if(call.lhs().is_not_nil())
666  assign(state, call.lhs(), nil_exprt());
667 
668  state.next_pc();
669  return;
670  }
671 
672  // push a frame on the call stack
674  state.threads[state.get_current_thread()];
675  thread.call_stack.push_back(path_symex_statet::framet());
676  thread.call_stack.back().current_function=function_identifier;
677  thread.call_stack.back().return_location=thread.pc.next_loc();
678  thread.call_stack.back().return_lhs=call.lhs();
679  thread.call_stack.back().return_rhs=nil_exprt();
680 
681  #if 0
682  for(loc_reft l=function_entry_point; ; ++l)
683  {
684  if(locs[l].target->is_end_function())
685  break;
686  if(locs[l].target->is_decl())
687  {
688  // make sure we have the local in the var_map
689  state.
690  }
691  }
692 
693  // save the locals into the frame
694  for(locst::local_variablest::const_iterator
695  it=function_entry.local_variables.begin();
696  it!=function_entry.local_variables.end();
697  it++)
698  {
699  unsigned nr=state.var_map[*it].number;
700  thread.call_stack.back().saved_local_vars[nr]=thread.local_vars[nr];
701  }
702  #endif
703 
704  const code_typet &code_type=function_entry.type;
705 
706  const code_typet::parameterst &function_parameters=code_type.parameters();
707 
708  const exprt::operandst &call_arguments=call.arguments();
709 
710  // keep track when va arguments begin.
711  std::size_t va_args_start_index=0;
712 
713  // now assign the argument values to parameters
714  for(std::size_t i=0; i<call_arguments.size(); i++)
715  {
716  if(i<function_parameters.size())
717  {
718  const code_typet::parametert &function_parameter=function_parameters[i];
719  irep_idt identifier=function_parameter.get_identifier();
720 
721  if(identifier.empty())
722  throw "function_call " + id2string(function_identifier)
723  + " no identifier for function parameter";
724 
725  symbol_exprt lhs(identifier, function_parameter.type());
726  exprt rhs=call_arguments[i];
727 
728  // lhs/rhs types might not match
729  if(lhs.type()!=rhs.type())
730  rhs.make_typecast(lhs.type());
731 
732  assign(state, lhs, rhs);
733  }
734  else if(va_args_start_index==0)
735  va_args_start_index=i;
736  }
737 
738  if(code_type.has_ellipsis())
739  {
740  std::size_t va_count=0;
741 
742  auto call_arguments_it = std::begin(call_arguments);
743  std::advance(call_arguments_it, va_args_start_index);
744  auto call_arguments_end = std::end(call_arguments);
745 
746  for(; call_arguments_it!=call_arguments_end; ++call_arguments_it)
747  {
748  exprt rhs=*call_arguments_it;
749 
750  irep_idt id=id2string(function_identifier)+"::va_arg"
751  +std::to_string(va_count);
752 
753  symbolt symbol;
754  symbol.name=id;
755  symbol.base_name="va_arg"+std::to_string(va_count);
756  symbol.type=rhs.type();
757 
758  va_count++;
759 
760  symbol_exprt lhs=symbol.symbol_expr();
761 
762  // lhs/rhs types might not match
763  if(lhs.type()!=rhs.type())
764  rhs.make_typecast(lhs.type());
765 
766  assign(state, lhs, rhs);
767  }
768  }
769 
770  // update statistics
771  state.recursion_map[function_identifier]++;
772 
773  // set the new PC
774  thread.pc=function_entry_point;
775  }
776  else if(function.id()==ID_dereference)
777  {
778  // should not happen, we read() before
779  throw "function_call_rec got dereference";
780  }
781  else if(function.id()==ID_if)
782  {
783  const if_exprt &if_expr=to_if_expr(function);
784  exprt guard=if_expr.cond();
785 
786  // add a 'further state' for the false-case
787 
788  {
789  further_states.push_back(state);
790  path_symex_statet &false_state=further_states.back();
791  false_state.record_step();
792  false_state.history->guard=not_exprt(guard);
794  further_states.back(), call, if_expr.false_case(), further_states);
795  }
796 
797  // do the true-case in 'state'
798  {
799  state.record_step();
800  state.history->guard=guard;
801  function_call_rec(state, call, if_expr.true_case(), further_states);
802  }
803  }
804  else if(function.id()==ID_typecast)
805  {
806  // ignore
808  state, call, to_typecast_expr(function).op(), further_states);
809  }
810  else
811  // NOLINTNEXTLINE(readability/throw)
812  throw "TODO: function_call "+function.id_string();
813 }
814 
816 {
818 
819  // returning from very last function?
820  if(thread.call_stack.empty())
821  {
822  state.disable_current_thread();
823  }
824  else
825  {
826  // update statistics
827  state.recursion_map[thread.call_stack.back().current_function]--;
828 
829  // set PC to return location
830  thread.pc=thread.call_stack.back().return_location;
831 
832  // assign the return value
833  if(thread.call_stack.back().return_rhs.is_not_nil() &&
834  thread.call_stack.back().return_lhs.is_not_nil())
835  assign(state, thread.call_stack.back().return_lhs,
836  thread.call_stack.back().return_rhs);
837 
838  // restore the local variables
839  for(path_symex_statet::var_state_mapt::const_iterator
840  it=thread.call_stack.back().saved_local_vars.begin();
841  it!=thread.call_stack.back().saved_local_vars.end();
842  it++)
843  thread.local_vars[it->first]=it->second;
844 
845  // kill the frame
846  thread.call_stack.pop_back();
847  }
848 }
849 
851  path_symex_statet &state,
852  const exprt &v)
853 {
855  state.threads[state.get_current_thread()];
856 
857  // returning from very last function?
858  if(!thread.call_stack.empty())
859  thread.call_stack.back().return_rhs=v;
860 }
861 
863  path_symex_statet &state,
864  std::list<path_symex_statet> &further_states)
865 {
866  const goto_programt::instructiont &instruction=
867  *state.get_instruction();
868 
869  if(instruction.is_backwards_goto())
870  {
871  // we keep a statistic on how many times we execute backwards gotos
872  state.unwinding_map[state.pc()]++;
873  }
874 
875  const loct &loc=state.locs[state.pc()];
876  assert(!loc.branch_target.is_nil());
877 
878  exprt guard=state.read(instruction.guard);
879 
880  if(guard.is_true()) // branch taken always
881  {
882  state.record_step();
884  state.set_pc(loc.branch_target);
885  return; // we are done
886  }
887 
888  if(!guard.is_false())
889  {
890  // branch taken case
891  // copy the state into 'further_states'
892  further_states.push_back(state);
893  further_states.back().record_step();
895  further_states.back().set_pc(loc.branch_target);
896  further_states.back().history->guard=guard;
897  }
898 
899  // branch not taken case
900  exprt negated_guard=not_exprt(guard);
901  state.record_step();
903  state.next_pc();
904  state.history->guard=negated_guard;
905 }
906 
908  path_symex_statet &state,
909  bool taken)
910 {
911  state.record_step();
912 
913  const goto_programt::instructiont &instruction=
914  *state.get_instruction();
915 
916  if(instruction.is_backwards_goto())
917  {
918  // we keep a statistic on how many times we execute backwards gotos
919  state.unwinding_map[state.pc()]++;
920  }
921 
922  exprt guard=state.read(instruction.guard);
923 
924  if(taken)
925  {
926  // branch taken case
927  const loct &loc=state.locs[state.pc()];
928  assert(!loc.branch_target.is_nil());
929  state.set_pc(loc.branch_target);
930  state.history->guard=guard;
932  }
933  else
934  {
935  // branch not taken case
936  exprt negated_guard=not_exprt(guard);
937  state.next_pc();
938  state.history->guard=negated_guard;
940  }
941 }
942 
944  path_symex_statet &state,
945  std::list<path_symex_statet> &further_states)
946 {
947  const goto_programt::instructiont &instruction=
948  *state.get_instruction();
949 
950  #ifdef DEBUG
951  std::cout << "path_symext::operator(): "
952  << state.pc() << " "
953  << instruction.type
954  << '\n';
955  #endif
956 
957  switch(instruction.type)
958  {
959  case END_FUNCTION:
960  // pop the call stack
961  state.record_step();
962  return_from_function(state);
963  break;
964 
965  case RETURN:
966  // sets the return value
967  state.record_step();
968  state.next_pc();
969 
970  if(instruction.code.operands().size()==1)
971  set_return_value(state, instruction.code.op0());
972 
973  break;
974 
975  case START_THREAD:
976  {
977  const loct &loc=state.locs[state.pc()];
978  assert(!loc.branch_target.is_nil());
979 
980  state.record_step();
981  state.next_pc();
982 
983  // ordering of the following matters due to vector instability
984  path_symex_statet::threadt &new_thread=state.add_thread();
985  path_symex_statet::threadt &old_thread=
986  state.threads[state.get_current_thread()];
987  new_thread.pc=loc.branch_target;
988  new_thread.local_vars=old_thread.local_vars;
989  }
990  break;
991 
992  case END_THREAD:
993  state.record_step();
994  state.disable_current_thread();
995  break;
996 
997  case GOTO:
998  do_goto(state, further_states);
999  break;
1000 
1001  case CATCH:
1002  // ignore for now
1003  state.record_step();
1004  state.next_pc();
1005  break;
1006 
1007  case THROW:
1008  state.record_step();
1009  throw "THROW not yet implemented"; // NOLINT(readability/throw)
1010 
1011  case ASSUME:
1012  state.record_step();
1013  state.next_pc();
1014  if(instruction.guard.is_false())
1015  state.disable_current_thread();
1016  else
1017  {
1018  exprt guard=state.read(instruction.guard);
1019  state.history->guard=guard;
1020  }
1021  break;
1022 
1023  case ASSERT:
1024  case SKIP:
1025  case LOCATION:
1026  case DEAD:
1027  state.record_step();
1028  state.next_pc();
1029  break;
1030 
1031  case DECL:
1032  // assigning an RHS of NIL means 'nondet'
1033  assign(state, to_code_decl(instruction.code).symbol(), nil_exprt());
1034  state.next_pc();
1035  break;
1036 
1037  case ATOMIC_BEGIN:
1038  if(state.inside_atomic_section)
1039  throw "nested ATOMIC_BEGIN";
1040 
1041  state.record_step();
1042  state.next_pc();
1043  state.inside_atomic_section=true;
1044  break;
1045 
1046  case ATOMIC_END:
1047  if(!state.inside_atomic_section)
1048  throw "ATOMIC_END unmatched"; // NOLINT(readability/throw)
1049 
1050  state.record_step();
1051  state.next_pc();
1052  state.inside_atomic_section=false;
1053  break;
1054 
1055  case ASSIGN:
1056  assign(state, to_code_assign(instruction.code));
1057  state.next_pc();
1058  break;
1059 
1060  case FUNCTION_CALL:
1061  state.record_step();
1062  function_call(
1063  state, to_code_function_call(instruction.code), further_states);
1064  break;
1065 
1066  case OTHER:
1067  state.record_step();
1068 
1069  {
1070  const codet &code=instruction.code;
1071  const irep_idt &statement=code.get_statement();
1072 
1073  if(statement==ID_expression)
1074  {
1075  // like SKIP
1076  }
1077  else if(statement==ID_printf)
1078  {
1079  // ignore for now (should record stuff printed)
1080  }
1081  else if(statement==ID_asm)
1082  {
1083  // ignore for now
1084  }
1085  else if(statement==ID_fence)
1086  {
1087  // ignore for SC
1088  }
1089  else if(statement==ID_input)
1090  {
1091  // just needs to be recorded
1092  }
1093  else
1094  throw "unexpected OTHER statement: "+id2string(statement);
1095  }
1096 
1097  state.next_pc();
1098  break;
1099 
1100  default:
1101  throw "path_symext: unexpected instruction";
1102  }
1103 }
1104 
1106 {
1107  std::list<path_symex_statet> further_states;
1108  operator()(state, further_states);
1109  if(!further_states.empty())
1110  throw "path_symext got unexpected further states";
1111 }
1112 
1114  path_symex_statet &state,
1115  std::list<path_symex_statet> &further_states)
1116 {
1118  path_symex(state, further_states);
1119 }
1120 
1122 {
1124  path_symex(state);
1125 }
1126 
1128  path_symex_statet &state,
1129  bool taken)
1130 {
1132  path_symex.do_goto(state, taken);
1133 }
1134 
1136 {
1138  path_symex.do_assert_fail(state);
1139 }
#define loc()
const irep_idt & get_statement() const
Definition: std_code.h:37
virtual void operator()(path_symex_statet &state, std::list< path_symex_statet > &furter_states)
Definition: path_symex.cpp:943
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
code_typet type
Definition: locs.h:50
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1286
Base type of functions.
Definition: std_types.h:734
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
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
exprt & object()
Definition: std_expr.h:2608
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
irep_idt mode
Language mode.
Definition: symbol.h:55
exprt & symbol()
Definition: std_code.h:205
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
bool has_ellipsis() const
Definition: std_types.h:803
void assign_rec(path_symex_statet &state, exprt::operandst &guard, const exprt &ssa_lhs, const exprt &ssa_rhs)
Definition: path_symex.cpp:347
void symex_malloc(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
Definition: path_symex.cpp:156
const irep_idt & get_identifier() const
Definition: std_expr.h:120
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
literalt pos(literalt a)
Definition: literal.h:193
std::vector< parametert > parameterst
Definition: std_types.h:829
const componentst & components() const
Definition: std_types.h:242
exprt read_no_propagate(const exprt &src)
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void path_symex_assert_fail(path_symex_statet &state)
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
exprt & op()
Definition: std_expr.h:1739
unwinding_mapt unwinding_map
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
void function_call(path_symex_statet &state, const code_function_callt &call, std::list< path_symex_statet > &further_states)
void do_goto(path_symex_statet &state, bool taken)
Definition: path_symex.cpp:907
symbol_exprt ssa_symbol() const
Definition: var_map.h:61
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
Extract member of struct or union.
Definition: std_expr.h:3214
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
enum path_symex_stept::kindt branch
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
Concrete Symbolic Transformer.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:2629
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
Expression classes for byte-level operators.
argumentst & arguments()
Definition: std_code.h:689
const locst & locs
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
void path_symex(path_symex_statet &state, std::list< path_symex_statet > &further_states)
The NIL expression.
Definition: std_expr.h:3764
Operator to dereference a pointer.
Definition: std_expr.h:2701
threadt & add_thread()
exprt & op1()
Definition: expr.h:87
void symex_va_arg_next(path_symex_statet &state, const exprt &lhs, const side_effect_exprt &code)
Definition: path_symex.cpp:288
void assign(path_symex_statet &state, const exprt &lhs, const exprt &rhs)
Definition: path_symex.cpp:92
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
var_statet & get_var_state(const var_mapt::var_infot &var_info)
bitvector_typet index_type()
Definition: c_types.cpp:15
unsigned get_current_thread() const
void return_from_function(path_symex_statet &state)
Definition: path_symex.cpp:815
Operator to return the address of an object.
Definition: std_expr.h:2593
exprt & false_case()
Definition: std_expr.h:2815
bool is_constant() const
Definition: expr.cpp:128
loc_reft next_loc() const
Definition: loc_ref.h:22
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:51
typet type
Type of symbol.
Definition: symbol.h:37
recursion_mapt recursion_map
static bool propagate(const exprt &src)
Definition: path_symex.cpp:33
goto_programt::const_targett get_instruction() const
void increment_ssa_counter()
Definition: var_map.h:69
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
const parameterst & parameters() const
Definition: std_types.h:841
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
Definition: locs.h:21
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
const source_locationt & source_location() const
Definition: expr.h:142
irep_idt get_component_name() const
Definition: std_expr.h:3249
void set_pc(loc_reft new_pc)
The NIL type.
Definition: std_types.h:43
function_mapt function_map
Definition: locs.h:54
Concrete Symbolic Transformer.
void path_symex_goto(path_symex_statet &state, bool taken)
const std::string & id_string() const
Definition: irep.h:192
void function_call_rec(path_symex_statet &state, const code_function_callt &function_call, const exprt &function, std::list< path_symex_statet > &further_states)
Definition: path_symex.cpp:632
void set_return_value(path_symex_statet &, const exprt &)
Definition: path_symex.cpp:850
static irep_idt get_old_va_symbol(const path_symex_statet &state, const exprt &src)
Definition: path_symex.cpp:271
arrays with given size
Definition: std_types.h:901
TO_BE_DOCUMENTED.
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const namespacet ns
Definition: var_map.h:101
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:19
loc_reft first_loc
Definition: locs.h:49
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:134
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Pointer Dereferencing.
unsigned dynamic_count
Definition: var_map.h:111
loc_reft pc() const
const irep_idt & get_identifier() const
Definition: std_types.h:782
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
static typet c_sizeof_type_rec(const exprt &expr)
Definition: path_symex.cpp:135
path_symex_step_reft history
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
irep_idt full_identifier
Definition: var_map.h:48
const irep_idt & get_statement() const
Definition: std_code.h:1012
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
irep_idt byte_update_id()
bool is_lvalue
Definition: symbol.h:71
array index operator
Definition: std_expr.h:1170