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