cprover
interpreter.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.h"
13 
14 #include <cctype>
15 #include <cstdio>
16 #include <iostream>
17 #include <fstream>
18 #include <algorithm>
19 #include <cstring>
20 
21 #include <util/fixedbv.h>
22 #include <util/ieee_float.h>
23 #include <util/invariant.h>
25 #include <util/message.h>
26 #include <util/pointer_expr.h>
27 #include <util/std_expr.h>
28 #include <util/std_types.h>
29 #include <util/string2int.h>
30 #include <util/string_container.h>
31 #include <util/symbol_table.h>
32 
33 #include <json/json_parser.h>
34 
35 #include "interpreter_class.h"
36 #include "json_goto_trace.h"
37 #include "remove_returns.h"
38 
39 const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
40 
42 {
43  output.status() << "0- Initialize:" << messaget::eom;
44  initialize(true);
45  try
46  {
47  output.status() << "Type h for help\n" << messaget::eom;
48 
49  while(!done)
50  command();
51 
52  output.status() << total_steps << "- Program End.\n" << messaget::eom;
53  }
54  catch (const char *e)
55  {
56  output.error() << e << "\n" << messaget::eom;
57  }
58 
59  while(!done)
60  command();
61 }
62 
65 void interpretert::initialize(bool init)
66 {
68  // reset the call stack
70 
71  total_steps=0;
72  const goto_functionst::function_mapt::const_iterator
74 
75  if(main_it==goto_functions.function_map.end())
76  throw "main not found";
77 
78  const goto_functionst::goto_functiont &goto_function=main_it->second;
79 
80  if(!goto_function.body_available())
81  throw "main has no body";
82 
83  pc=goto_function.body.instructions.begin();
84  function=main_it;
85 
86  done=false;
87  if(init)
88  {
89  // execute instructions up to and including __CPROVER_initialize()
90  while(!done && call_stack.size() == 0)
91  {
92  show_state();
93  step();
94  }
95  // initialization
96  while(!done && call_stack.size() > 0)
97  {
98  show_state();
99  step();
100  }
101  // invoke the user entry point
102  while(!done && call_stack.size() == 0)
103  {
104  show_state();
105  step();
106  }
108  input_vars.clear();
109  }
110 }
111 
114 {
115  if(!show)
116  return;
117  output.status() << "\n"
118  << total_steps + 1
119  << " ----------------------------------------------------\n";
120 
121  if(pc==function->second.body.instructions.end())
122  {
123  output.status() << "End of function '" << function->first << "'\n";
124  }
125  else
126  function->second.body.output_instruction(
127  ns, function->first, output.status(), *pc);
128 
130 }
131 
134 {
135  #define BUFSIZE 100
136  char command[BUFSIZE];
137  if(fgets(command, BUFSIZE-1, stdin)==nullptr)
138  {
139  done=true;
140  return;
141  }
142 
143  char ch=tolower(command[0]);
144  if(ch=='q')
145  done=true;
146  else if(ch=='h')
147  {
148  output.status() << "Interpreter help\n"
149  << "h: display this menu\n"
150  << "j: output json trace\n"
151  << "m: output memory dump\n"
152  << "o: output goto trace\n"
153  << "q: quit\n"
154  << "r: run up to entry point\n"
155  << "s#: step a number of instructions\n"
156  << "sa: step across a function\n"
157  << "so: step out of a function\n"
158  << "se: step until end of program\n"
159  << messaget::eom;
160  }
161  else if(ch=='j')
162  {
163  json_arrayt json_steps;
164  convert<json_arrayt>(ns, steps, json_steps);
165  ch=tolower(command[1]);
166  if(ch==' ')
167  {
168  std::ofstream file;
169  file.open(command+2);
170  if(file.is_open())
171  {
172  json_steps.output(file);
173  file.close();
174  return;
175  }
176  }
177  json_steps.output(output.result());
178  }
179  else if(ch=='m')
180  {
181  ch=tolower(command[1]);
182  print_memory(ch=='i');
183  }
184  else if(ch=='o')
185  {
186  ch=tolower(command[1]);
187  if(ch==' ')
188  {
189  std::ofstream file;
190  file.open(command+2);
191  if(file.is_open())
192  {
193  steps.output(ns, file);
194  file.close();
195  return;
196  }
197  }
199  }
200  else if(ch=='r')
201  {
202  ch=tolower(command[1]);
203  initialize(ch!='0');
204  }
205  else if((ch=='s') || (ch==0))
206  {
207  num_steps=1;
208  std::size_t stack_depth = npos;
209  ch=tolower(command[1]);
210  if(ch=='e')
211  num_steps=npos;
212  else if(ch=='o')
213  stack_depth=call_stack.size();
214  else if(ch=='a')
215  stack_depth=call_stack.size()+1;
216  else
217  {
219  if(num_steps==0)
220  num_steps=1;
221  }
222  while(!done && ((num_steps==npos) || ((num_steps--)>0)))
223  {
224  step();
225  show_state();
226  }
227  while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
228  {
229  step();
230  show_state();
231  }
232  return;
233  }
234  show_state();
235 }
236 
239 {
240  total_steps++;
241  if(pc==function->second.body.instructions.end())
242  {
243  if(call_stack.empty())
244  done=true;
245  else
246  {
247  pc=call_stack.top().return_pc;
248  function=call_stack.top().return_function;
249  // TODO: this increases memory size quite quickly.
250  // Should check alternatives
251  call_stack.pop();
252  }
253 
254  return;
255  }
256 
257  next_pc=pc;
258  next_pc++;
259 
261  goto_trace_stept &trace_step=steps.get_last_step();
262  trace_step.thread_nr=thread_id;
263  trace_step.pc=pc;
264  switch(pc->type)
265  {
266  case GOTO:
268  execute_goto();
269  break;
270 
271  case ASSUME:
273  execute_assume();
274  break;
275 
276  case ASSERT:
278  execute_assert();
279  break;
280 
281  case OTHER:
282  execute_other();
283  break;
284 
285  case DECL:
287  execute_decl();
288  break;
289 
290  case SKIP:
291  case LOCATION:
293  break;
294  case END_FUNCTION:
296  break;
297 
298  case RETURN:
300  if(call_stack.empty())
301  throw "RETURN without call"; // NOLINT(readability/throw)
302 
303  if(call_stack.top().return_value_address != 0)
304  {
305  mp_vectort rhs;
306  evaluate(pc->return_value(), rhs);
307  assign(call_stack.top().return_value_address, rhs);
308  }
309 
310  next_pc=function->second.body.instructions.end();
311  break;
312 
313  case ASSIGN:
315  execute_assign();
316  break;
317 
318  case FUNCTION_CALL:
321  break;
322 
323  case START_THREAD:
325  throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
326 
327  case END_THREAD:
328  throw "END_THREAD not yet implemented"; // NOLINT(readability/throw)
329  break;
330 
331  case ATOMIC_BEGIN:
333  throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw)
334 
335  case ATOMIC_END:
337  throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw)
338 
339  case DEAD:
341  break;
342  case THROW:
344  while(!done && (pc->type!=CATCH))
345  {
346  if(pc==function->second.body.instructions.end())
347  {
348  if(call_stack.empty())
349  done=true;
350  else
351  {
352  pc=call_stack.top().return_pc;
353  function=call_stack.top().return_function;
354  call_stack.pop();
355  }
356  }
357  else
358  {
359  next_pc=pc;
360  next_pc++;
361  }
362  }
363  break;
364  case CATCH:
365  break;
366  case INCOMPLETE_GOTO:
367  case NO_INSTRUCTION_TYPE:
368  throw "encountered instruction with undefined instruction type";
369  }
370  pc=next_pc;
371 }
372 
375 {
376  if(evaluate_boolean(pc->get_condition()))
377  {
378  if(pc->targets.empty())
379  throw "taken goto without target";
380 
381  if(pc->targets.size()>=2)
382  throw "non-deterministic goto encountered";
383 
384  next_pc=pc->targets.front();
385  }
386 }
387 
390 {
391  const irep_idt &statement = pc->get_other().get_statement();
392  if(statement==ID_expression)
393  {
395  pc->code.operands().size()==1,
396  "expression statement expected to have one operand");
397  mp_vectort rhs;
398  evaluate(pc->code.op0(), rhs);
399  }
400  else if(statement==ID_array_set)
401  {
402  mp_vectort tmp, rhs;
403  evaluate(pc->code.op1(), tmp);
404  mp_integer address=evaluate_address(pc->code.op0());
405  mp_integer size=get_size(pc->code.op0().type());
406  while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
407  if(size!=rhs.size())
408  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
409  << size << ")\n"
410  << messaget::eom;
411  else
412  {
413  assign(address, rhs);
414  }
415  }
416  else if(can_cast_expr<code_outputt>(pc->get_other()))
417  {
418  return;
419  }
420  else
421  throw "unexpected OTHER statement: "+id2string(statement);
422 }
423 
425 {
426  PRECONDITION(pc->code.get_statement()==ID_decl);
427 }
428 
431 interpretert::get_component(const typet &object_type, const mp_integer &offset)
432 {
433  const typet real_type = ns.follow(object_type);
434  if(real_type.id()!=ID_struct)
435  throw "request for member of non-struct";
436 
437  const struct_typet &struct_type=to_struct_type(real_type);
438  const struct_typet::componentst &components=struct_type.components();
439 
440  mp_integer tmp_offset=offset;
441 
442  for(const auto &c : components)
443  {
444  if(tmp_offset<=0)
445  return c;
446 
447  tmp_offset-=get_size(c.type());
448  }
449 
450  throw "access out of struct bounds";
451 }
452 
455 {
456  dynamic_typest::const_iterator it=dynamic_types.find(id);
457  if(it==dynamic_types.end())
458  return symbol_table.lookup_ref(id).type;
459  return it->second;
460 }
461 
465  const typet &type,
466  const mp_integer &offset,
467  bool use_non_det)
468 {
469  const typet real_type=ns.follow(type);
470  if(real_type.id()==ID_struct)
471  {
472  struct_exprt result({}, real_type);
473  const struct_typet &struct_type=to_struct_type(real_type);
474  const struct_typet::componentst &components=struct_type.components();
475 
476  // Retrieve the values for the individual members
477  result.reserve_operands(components.size());
478 
479  mp_integer tmp_offset=offset;
480 
481  for(const auto &c : components)
482  {
483  mp_integer size=get_size(c.type());
484  const exprt operand=get_value(c.type(), tmp_offset);
485  tmp_offset+=size;
486  result.copy_to_operands(operand);
487  }
488 
489  return std::move(result);
490  }
491  else if(real_type.id()==ID_array)
492  {
493  // Get size of array
494  array_exprt result({}, to_array_type(real_type));
495  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
496  mp_integer subtype_size=get_size(type.subtype());
497  mp_integer count;
498  if(size_expr.id()!=ID_constant)
499  {
500  count=base_address_to_actual_size(offset)/subtype_size;
501  }
502  else
503  {
504  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
505  }
506 
507  // Retrieve the value for each member in the array
508  result.reserve_operands(numeric_cast_v<std::size_t>(count));
509  for(mp_integer i=0; i<count; ++i)
510  {
511  const exprt operand=get_value(
512  type.subtype(),
513  offset+i*subtype_size);
514  result.copy_to_operands(operand);
515  }
516  return std::move(result);
517  }
518  if(
519  use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
521  {
523  }
524  mp_vectort rhs;
525  rhs.push_back(memory[numeric_cast_v<std::size_t>(offset)].value);
526  return get_value(type, rhs);
527 }
528 
532  const typet &type,
533  mp_vectort &rhs,
534  const mp_integer &offset)
535 {
536  const typet real_type=ns.follow(type);
537  PRECONDITION(!rhs.empty());
538 
539  if(real_type.id()==ID_struct)
540  {
541  struct_exprt result({}, real_type);
542  const struct_typet &struct_type=to_struct_type(real_type);
543  const struct_typet::componentst &components=struct_type.components();
544 
545  // Retrieve the values for the individual members
546  result.reserve_operands(components.size());
547  mp_integer tmp_offset=offset;
548 
549  for(const struct_union_typet::componentt &expr : components)
550  {
551  mp_integer size=get_size(expr.type());
552  const exprt operand=get_value(expr.type(), rhs, tmp_offset);
553  tmp_offset+=size;
554  result.copy_to_operands(operand);
555  }
556  return std::move(result);
557  }
558  else if(real_type.id()==ID_array)
559  {
560  array_exprt result({}, to_array_type(real_type));
561  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
562 
563  // Get size of array
564  mp_integer subtype_size=get_size(type.subtype());
565 
566  mp_integer count;
567  if(unbounded_size(type))
568  {
569  count=base_address_to_actual_size(offset)/subtype_size;
570  }
571  else
572  {
573  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
574  }
575 
576  // Retrieve the value for each member in the array
577  result.reserve_operands(numeric_cast_v<std::size_t>(count));
578  for(mp_integer i=0; i<count; ++i)
579  {
580  const exprt operand=get_value(type.subtype(), rhs,
581  offset+i*subtype_size);
582  result.copy_to_operands(operand);
583  }
584  return std::move(result);
585  }
586  else if(real_type.id()==ID_floatbv)
587  {
588  ieee_floatt f(to_floatbv_type(type));
589  f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
590  return f.to_expr();
591  }
592  else if(real_type.id()==ID_fixedbv)
593  {
594  fixedbvt f;
595  f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
596  return f.to_expr();
597  }
598  else if(real_type.id()==ID_bool)
599  {
600  if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
601  return true_exprt();
602  else
603  false_exprt();
604  }
605  else if(real_type.id()==ID_c_bool)
606  {
607  return from_integer(
608  rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
609  }
610  else if(real_type.id() == ID_pointer)
611  {
612  if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
613  return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
614 
615  if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
616  {
617  // We want the symbol pointed to
618  mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
619  const symbol_exprt &symbol_expr = address_to_symbol(address);
620  mp_integer offset_from_address = address_to_offset(address);
621 
622  if(offset_from_address == 0)
623  return address_of_exprt(symbol_expr);
624 
625  if(
626  symbol_expr.type().id() == ID_struct ||
627  symbol_expr.type().id() == ID_struct_tag)
628  {
629  const auto c = get_component(symbol_expr.type(), offset_from_address);
630  member_exprt member_expr(symbol_expr, c);
631  return address_of_exprt(member_expr);
632  }
633 
634  return index_exprt(
635  symbol_expr, from_integer(offset_from_address, integer_typet()));
636  }
637 
638  output.error() << "interpreter: invalid pointer "
639  << rhs[numeric_cast_v<std::size_t>(offset)]
640  << " > object count " << memory.size() << messaget::eom;
641 
642  throw "interpreter: reading from invalid pointer";
643  }
644  else if(real_type.id()==ID_string)
645  {
646  // Strings are currently encoded by their irep_idt ID.
647  return constant_exprt(
648  get_string_container().get_string(
649  numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
650  type);
651  }
652 
653  // Retrieve value of basic data type
654  return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
655 }
656 
659 {
660  const code_assignt &code_assign=
661  to_code_assign(pc->code);
662 
663  mp_vectort rhs;
664  evaluate(code_assign.rhs(), rhs);
665 
666  if(!rhs.empty())
667  {
668  mp_integer address=evaluate_address(code_assign.lhs());
669  mp_integer size=get_size(code_assign.lhs().type());
670 
671  if(size!=rhs.size())
672  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
673  << size << ")\n"
674  << messaget::eom;
675  else
676  {
677  goto_trace_stept &trace_step=steps.get_last_step();
678  assign(address, rhs);
679  trace_step.full_lhs=code_assign.lhs();
680  trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
681  }
682  }
683  else if(code_assign.rhs().id()==ID_side_effect)
684  {
685  side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
686  if(side_effect.get_statement()==ID_nondet)
687  {
688  mp_integer address =
689  numeric_cast_v<std::size_t>(evaluate_address(code_assign.lhs()));
690 
691  mp_integer size=
692  get_size(code_assign.lhs().type());
693 
694  for(mp_integer i=0; i<size; ++i)
695  {
696  memory[numeric_cast_v<std::size_t>(address + i)].initialized =
698  }
699  }
700  }
701 }
702 
705  const mp_integer &address,
706  const mp_vectort &rhs)
707 {
708  for(mp_integer i=0; i<rhs.size(); ++i)
709  {
710  if((address+i)<memory.size())
711  {
712  mp_integer address_val=address+i;
713  memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
714  if(show)
715  {
716  output.status() << total_steps << " ** assigning "
717  << address_to_symbol(address_val).get_identifier()
718  << "[" << address_to_offset(address_val)
719  << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
720  << messaget::eom;
721  }
722  cell.value = rhs[numeric_cast_v<std::size_t>(i)];
725  }
726  }
727 }
728 
730 {
731  if(!evaluate_boolean(pc->get_condition()))
732  throw "assumption failed";
733 }
734 
736 {
737  if(!evaluate_boolean(pc->get_condition()))
738  {
739  if(show)
740  output.error() << "assertion failed at " << pc->location_number << "\n"
741  << messaget::eom;
742  }
743 }
744 
746 {
747  const code_function_callt &function_call = pc->get_function_call();
748 
749  // function to be called
750  mp_integer address=evaluate_address(function_call.function());
751 
752  if(address==0)
753  throw "function call to NULL";
754  else if(address>=memory.size())
755  throw "out-of-range function call";
756 
757  // Retrieve the empty last trace step struct we pushed for this step
758  // of the interpreter run to fill it with the corresponding data
759  goto_trace_stept &trace_step=steps.get_last_step();
760 #if 0
761  const memory_cellt &cell=memory[address];
762 #endif
763  const irep_idt &identifier = address_to_symbol(address).get_identifier();
764  trace_step.called_function = identifier;
765 
766  const goto_functionst::function_mapt::const_iterator f_it=
767  goto_functions.function_map.find(identifier);
768 
769  if(f_it==goto_functions.function_map.end())
770  throw "failed to find function "+id2string(identifier);
771 
772  // return value
773  mp_integer return_value_address;
774 
775  if(function_call.lhs().is_not_nil())
776  return_value_address=
777  evaluate_address(function_call.lhs());
778  else
779  return_value_address=0;
780 
781  // values of the arguments
782  std::vector<mp_vectort> argument_values;
783 
784  argument_values.resize(function_call.arguments().size());
785 
786  for(std::size_t i=0; i<function_call.arguments().size(); i++)
787  evaluate(function_call.arguments()[i], argument_values[i]);
788 
789  // do the call
790 
791  if(f_it->second.body_available())
792  {
793  call_stack.push(stack_framet());
794  stack_framet &frame=call_stack.top();
795 
796  frame.return_pc=next_pc;
797  frame.return_function=function;
799  frame.return_value_address=return_value_address;
800 
801  // local variables
802  std::set<irep_idt> locals;
803  get_local_identifiers(f_it->second, locals);
804 
805  for(const auto &id : locals)
806  {
807  const symbolt &symbol=ns.lookup(id);
808  frame.local_map[id] = build_memory_map(symbol.symbol_expr());
809  }
810 
811  // assign the arguments
812  const auto &parameter_identifiers = f_it->second.parameter_identifiers;
813  if(argument_values.size() < parameter_identifiers.size())
814  throw "not enough arguments";
815 
816  for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
817  {
818  const symbol_exprt symbol_expr =
819  ns.lookup(parameter_identifiers[i]).symbol_expr();
820  assign(evaluate_address(symbol_expr), argument_values[i]);
821  }
822 
823  // set up new pc
824  function=f_it;
825  next_pc=f_it->second.body.instructions.begin();
826  }
827  else
828  {
829  list_input_varst::iterator it = function_input_vars.find(
830  to_symbol_expr(function_call.function()).get_identifier());
831 
832  if(it!=function_input_vars.end())
833  {
834  mp_vectort value;
835  PRECONDITION(!it->second.empty());
836  PRECONDITION(!it->second.front().return_assignments.empty());
837  evaluate(it->second.front().return_assignments.back().value, value);
838  if(return_value_address>0)
839  {
840  assign(return_value_address, value);
841  }
842  it->second.pop_front();
843  return;
844  }
845 
846  if(show)
847  output.error() << "no body for " << identifier << messaget::eom;
848  }
849 }
850 
853 {
854  // put in a dummy for NULL
855  memory.clear();
856  memory.resize(1);
857  inverse_memory_map[0] = {};
858 
860  dynamic_types.clear();
861 
862  // now do regular static symbols
863  for(const auto &s : symbol_table.symbols)
864  build_memory_map(s.second);
865 
866  // for the locals
868 }
869 
871 {
872  mp_integer size=0;
873 
874  if(symbol.type.id()==ID_code)
875  {
876  size=1;
877  }
878  else if(symbol.is_static_lifetime)
879  {
880  size=get_size(symbol.type);
881  }
882 
883  if(size!=0)
884  {
885  mp_integer address=memory.size();
886  memory.resize(numeric_cast_v<std::size_t>(address + size));
887  memory_map[symbol.name]=address;
888  inverse_memory_map[address] = symbol.symbol_expr();
889  }
890 }
891 
894 {
895  if(type.id()==ID_array)
896  {
897  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
898  mp_vectort computed_size;
899  evaluate(size_expr, computed_size);
900  if(computed_size.size()==1 &&
901  computed_size[0]>=0)
902  {
903  output.result() << "Concretized array with size " << computed_size[0]
904  << messaget::eom;
905  return
906  array_typet(
907  type.subtype(),
908  from_integer(computed_size[0], integer_typet()));
909  }
910  else
911  {
912  output.warning() << "Failed to concretize variable array"
913  << messaget::eom;
914  }
915  }
916  return type;
917 }
918 
922 {
923  typet alloc_type = concretize_type(symbol_expr.type());
924  mp_integer size=get_size(alloc_type);
925  auto it = dynamic_types.find(symbol_expr.get_identifier());
926 
927  if(it!=dynamic_types.end())
928  {
929  mp_integer address = memory_map[symbol_expr.get_identifier()];
930  mp_integer current_size=base_address_to_alloc_size(address);
931  // current size <= size already recorded
932  if(size<=current_size)
933  return memory_map[symbol_expr.get_identifier()];
934  }
935 
936  // The current size is bigger then the one previously recorded
937  // in the memory map
938 
939  if(size==0)
940  size=1; // This is a hack to create existence
941 
942  mp_integer address=memory.size();
943  memory.resize(numeric_cast_v<std::size_t>(address + size));
944  memory_map[symbol_expr.get_identifier()] = address;
945  inverse_memory_map[address] = symbol_expr;
946  dynamic_types.insert(
947  std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
948 
949  return address;
950 }
951 
953 {
954  if(type.id()==ID_array)
955  {
956  const exprt &size=to_array_type(type).size();
957  if(size.id()==ID_infinity)
958  return true;
959  return unbounded_size(type.subtype());
960  }
961  else if(type.id()==ID_struct)
962  {
963  const auto &st=to_struct_type(type);
964  if(st.components().empty())
965  return false;
966  return unbounded_size(st.components().back().type());
967  }
968  return false;
969 }
970 
976 {
977  if(unbounded_size(type))
978  return mp_integer(2) << 32;
979 
980  if(type.id()==ID_struct)
981  {
982  const struct_typet::componentst &components=
983  to_struct_type(type).components();
984 
985  mp_integer sum=0;
986 
987  for(const auto &comp : components)
988  {
989  const typet &sub_type=comp.type();
990 
991  if(sub_type.id()!=ID_code)
992  sum+=get_size(sub_type);
993  }
994 
995  return sum;
996  }
997  else if(type.id()==ID_union)
998  {
999  const union_typet::componentst &components=
1000  to_union_type(type).components();
1001 
1002  mp_integer max_size=0;
1003 
1004  for(const auto &comp : components)
1005  {
1006  const typet &sub_type=comp.type();
1007 
1008  if(sub_type.id()!=ID_code)
1009  max_size=std::max(max_size, get_size(sub_type));
1010  }
1011 
1012  return max_size;
1013  }
1014  else if(type.id()==ID_array)
1015  {
1016  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
1017 
1018  mp_integer subtype_size=get_size(type.subtype());
1019 
1020  mp_vectort i;
1021  evaluate(size_expr, i);
1022  if(i.size()==1)
1023  {
1024  // Go via the binary representation to reproduce any
1025  // overflow behaviour.
1026  const constant_exprt size_const = from_integer(i[0], size_expr.type());
1027  const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
1028  return subtype_size*size_mp;
1029  }
1030  return subtype_size;
1031  }
1032  else if(type.id() == ID_struct_tag)
1033  {
1034  return get_size(ns.follow_tag(to_struct_tag_type(type)));
1035  }
1036 
1037  return 1;
1038 }
1039 
1041 {
1042  // The dynamic type and the static symbol type may differ for VLAs,
1043  // where the symbol carries a size expression and the dynamic type
1044  // registry contains its actual length.
1045  auto findit=dynamic_types.find(id);
1046  typet get_type;
1047  if(findit!=dynamic_types.end())
1048  get_type=findit->second;
1049  else
1051 
1052  symbol_exprt symbol_expr(id, get_type);
1053  mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
1054 
1055  return get_value(get_type, whole_lhs_object_address);
1056 }
1057 
1060 void interpretert::print_memory(bool input_flags)
1061 {
1062  for(const auto &cell_address : memory)
1063  {
1064  mp_integer i=cell_address.first;
1065  const memory_cellt &cell=cell_address.second;
1066  const auto identifier = address_to_symbol(i).get_identifier();
1067  const auto offset=address_to_offset(i);
1068  output.status() << identifier << "[" << offset << "]"
1069  << "=" << cell.value << messaget::eom;
1070  if(input_flags)
1071  output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1072  << messaget::eom;
1074  }
1075 }
1076 
1078  const goto_modelt &goto_model,
1079  message_handlert &message_handler)
1080 {
1082  goto_model.symbol_table,
1083  goto_model.goto_functions,
1084  message_handler);
1085  interpreter();
1086 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Operator to return the address of an object.
Definition: pointer_expr.h:200
Array constructor from list of elements.
Definition: std_expr.h:1382
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
argumentst & arguments()
Definition: std_code.h:1260
A constant literal expression.
Definition: std_expr.h:2668
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2726
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Step of the trace of a GOTO program.
Definition: goto_trace.h:52
exprt full_lhs_value
Definition: goto_trace.h:134
goto_programt::const_targett pc
Definition: goto_trace.h:114
unsigned thread_nr
Definition: goto_trace.h:117
irep_idt called_function
Definition: goto_trace.h:143
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:205
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition: goto_trace.h:198
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:55
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:315
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
Array index operator.
Definition: std_expr.h:1243
Unbounded, signed integers (mathematical integers, not bitvectors)
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
void execute_function_call()
mp_integer stack_pointer
void execute_assert()
static const size_t npos
mp_integer base_address_to_actual_size(const mp_integer &address) const
void operator()()
Definition: interpreter.cpp:41
memory_mapt memory_map
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.
goto_functionst::function_mapt::const_iterator function
inverse_memory_mapt inverse_memory_map
symbol_exprt address_to_symbol(const mp_integer &address) const
call_stackt call_stack
void execute_assume()
void execute_goto()
executes a goto instruction
goto_tracet steps
void build_memory_map()
Creates a memory map of all static symbols in the program.
std::vector< mp_integer > mp_vectort
void execute_assign()
executes the assign statement at the current pc value
void execute_decl()
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
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
mp_integer address_to_offset(const mp_integer &address) const
void step()
executes a single step and updates the program counter
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.
const symbol_tablet & symbol_table
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:65
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
bool unbounded_size(const typet &)
void execute_other()
executes side effects of 'other' instructions
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
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void output(std::ostream &out) const
Definition: json.h:90
Extract member of struct or union.
Definition: std_expr.h:2528
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & status() const
Definition: message.h:414
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
The null pointer constant.
Definition: std_expr.h:2751
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
An expression containing a side effect.
Definition: std_code.h:1898
const irep_idt & get_statement() const
Definition: std_code.h:1920
void resize(uint64_t new_size)
Definition: sparse_vector.h:48
uint64_t size() const
Definition: sparse_vector.h:43
Struct constructor from list of elements.
Definition: std_expr.h:1583
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:81
const irep_idt & get_identifier() const
Definition: std_expr.h:110
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
The Boolean constant true.
Definition: std_expr.h:2717
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
@ FUNCTION_CALL
Definition: goto_program.h:50
@ ATOMIC_END
Definition: goto_program.h:45
@ DEAD
Definition: goto_program.h:49
@ END_FUNCTION
Definition: goto_program.h:43
@ RETURN
Definition: goto_program.h:46
@ ASSIGN
Definition: goto_program.h:47
@ ASSERT
Definition: goto_program.h:37
@ ATOMIC_BEGIN
Definition: goto_program.h:44
@ CATCH
Definition: goto_program.h:52
@ END_THREAD
Definition: goto_program.h:41
@ SKIP
Definition: goto_program.h:39
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
@ START_THREAD
Definition: goto_program.h:40
@ THROW
Definition: goto_program.h:51
@ DECL
Definition: goto_program.h:48
@ OTHER
Definition: goto_program.h:38
@ GOTO
Definition: goto_program.h:35
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
@ ASSUME
Definition: goto_program.h:36
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
#define BUFSIZE
Interpreter for GOTO Programs.
Interpreter for GOTO Programs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Traces of GOTO Programs.
Mathematical types.
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes for Pointers.
Replace function returns by assignments to global variables.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
Definition: stack_depth.cpp:43
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:751
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
Pre-defined types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:43
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.
Definition: kdev_t.h:19
Author: Diffblue Ltd.