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