CBMC
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 #include "interpreter_class.h"
14 
15 #include <util/c_types.h>
16 #include <util/fixedbv.h>
17 #include <util/ieee_float.h>
18 #include <util/invariant.h>
20 #include <util/message.h>
21 #include <util/pointer_expr.h>
22 #include <util/std_code.h>
23 #include <util/std_expr.h>
24 #include <util/string2int.h>
25 #include <util/string_container.h>
26 
27 #include "goto_model.h"
28 #include "json_goto_trace.h"
29 
30 #include <algorithm>
31 #include <cctype>
32 #include <climits>
33 #include <cstdio>
34 #include <fstream>
35 
36 const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
37 
39 {
40  output.status() << "0- Initialize:" << messaget::eom;
41  initialize(true);
42  try
43  {
44  output.status() << "Type h for help\n" << messaget::eom;
45 
46  while(!done)
47  command();
48 
49  output.status() << total_steps << "- Program End.\n" << messaget::eom;
50  }
51  catch (const char *e)
52  {
53  output.error() << e << "\n" << messaget::eom;
54  }
55 
56  while(!done)
57  command();
58 }
59 
62 void interpretert::initialize(bool init)
63 {
65  // reset the call stack
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  // execute instructions up to and including __CPROVER_initialize()
87  while(!done && call_stack.size() == 0)
88  {
89  show_state();
90  step();
91  }
92  // initialization
93  while(!done && call_stack.size() > 0)
94  {
95  show_state();
96  step();
97  }
98  // invoke the user entry point
99  while(!done && call_stack.size() == 0)
100  {
101  show_state();
102  step();
103  }
105  input_vars.clear();
106  }
107 }
108 
111 {
112  if(!show)
113  return;
114  output.status() << "\n"
115  << total_steps + 1
116  << " ----------------------------------------------------\n";
117 
118  if(pc==function->second.body.instructions.end())
119  {
120  output.status() << "End of function '" << function->first << "'\n";
121  }
122  else
123  pc->output(output.status());
124 
126 }
127 
130 {
131  #define BUFSIZE 100
132  char command[BUFSIZE];
133  if(fgets(command, BUFSIZE-1, stdin)==nullptr)
134  {
135  done=true;
136  return;
137  }
138 
139  char ch=tolower(command[0]);
140  if(ch=='q')
141  done=true;
142  else if(ch=='h')
143  {
144  output.status() << "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 up to entry point\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  << "se: step until end of program\n"
155  << messaget::eom;
156  }
157  else if(ch=='j')
158  {
159  json_arrayt json_steps;
160  convert<json_arrayt>(ns, steps, json_steps);
161  ch=tolower(command[1]);
162  if(ch==' ')
163  {
164  std::ofstream file;
165  file.open(command+2);
166  if(file.is_open())
167  {
168  json_steps.output(file);
169  file.close();
170  return;
171  }
172  }
173  json_steps.output(output.result());
174  }
175  else if(ch=='m')
176  {
177  ch=tolower(command[1]);
178  print_memory(ch=='i');
179  }
180  else if(ch=='o')
181  {
182  ch=tolower(command[1]);
183  if(ch==' ')
184  {
185  std::ofstream file;
186  file.open(command+2);
187  if(file.is_open())
188  {
189  steps.output(ns, file);
190  file.close();
191  return;
192  }
193  }
195  }
196  else if(ch=='r')
197  {
198  ch=tolower(command[1]);
199  initialize(ch!='0');
200  }
201  else if((ch=='s') || (ch==0))
202  {
203  num_steps=1;
204  std::size_t stack_depth = npos;
205  ch=tolower(command[1]);
206  if(ch=='e')
207  num_steps=npos;
208  else if(ch=='o')
209  stack_depth=call_stack.size();
210  else if(ch=='a')
211  stack_depth=call_stack.size()+1;
212  else
213  {
215  if(num_steps==0)
216  num_steps=1;
217  }
218  while(!done && ((num_steps==npos) || ((num_steps--)>0)))
219  {
220  step();
221  show_state();
222  }
223  while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
224  {
225  step();
226  show_state();
227  }
228  return;
229  }
230  show_state();
231 }
232 
235 {
236  total_steps++;
237  if(pc==function->second.body.instructions.end())
238  {
239  if(call_stack.empty())
240  done=true;
241  else
242  {
243  pc=call_stack.top().return_pc;
244  function=call_stack.top().return_function;
245  // TODO: this increases memory size quite quickly.
246  // Should check alternatives
247  call_stack.pop();
248  }
249 
250  return;
251  }
252 
253  next_pc=pc;
254  next_pc++;
255 
257  goto_trace_stept &trace_step=steps.get_last_step();
258  trace_step.thread_nr=thread_id;
259  trace_step.pc=pc;
260  switch(pc->type())
261  {
262  case GOTO:
264  execute_goto();
265  break;
266 
267  case ASSUME:
269  execute_assume();
270  break;
271 
272  case ASSERT:
274  execute_assert();
275  break;
276 
277  case OTHER:
278  execute_other();
279  break;
280 
281  case DECL:
283  execute_decl();
284  break;
285 
286  case SKIP:
287  case LOCATION:
289  break;
290  case END_FUNCTION:
292  break;
293 
294  case SET_RETURN_VALUE:
296  if(call_stack.empty())
297  throw "SET_RETURN_VALUE without call"; // NOLINT(readability/throw)
298 
299  if(call_stack.top().return_value_address != 0)
300  {
301  mp_vectort rhs = evaluate(pc->return_value());
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  case INCOMPLETE_GOTO:
362  case NO_INSTRUCTION_TYPE:
363  throw "encountered instruction with undefined instruction type";
364  }
365  pc=next_pc;
366 }
367 
370 {
371  if(evaluate_boolean(pc->condition()))
372  {
373  if(pc->targets.empty())
374  throw "taken goto without target";
375 
376  if(pc->targets.size()>=2)
377  throw "non-deterministic goto encountered";
378 
379  next_pc=pc->targets.front();
380  }
381 }
382 
385 {
386  const irep_idt &statement = pc->get_other().get_statement();
387  if(statement==ID_expression)
388  {
390  pc->code().operands().size() == 1,
391  "expression statement expected to have one operand");
392  mp_vectort rhs = evaluate(pc->code().op0());
393  }
394  else if(statement==ID_array_set)
395  {
396  mp_vectort tmp = evaluate(pc->code().op1());
397  mp_integer address = evaluate_address(pc->code().op0());
398  mp_integer size = get_size(pc->code().op0().type());
399  mp_vectort rhs;
400  while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
401  if(size!=rhs.size())
402  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
403  << size << ")\n"
404  << messaget::eom;
405  else
406  {
407  assign(address, rhs);
408  }
409  }
410  else if(can_cast_expr<code_outputt>(pc->get_other()))
411  {
412  return;
413  }
414  else
415  throw "unexpected OTHER statement: "+id2string(statement);
416 }
417 
419 {
420  PRECONDITION(pc->code().get_statement() == ID_decl);
421 }
422 
425 interpretert::get_component(const typet &object_type, const mp_integer &offset)
426 {
427  if(object_type.id() != ID_struct_tag)
428  throw "request for member of non-struct";
429 
430  const struct_typet &struct_type =
431  ns.follow_tag(to_struct_tag_type(object_type));
432  const struct_typet::componentst &components=struct_type.components();
433 
434  mp_integer tmp_offset=offset;
435 
436  for(const auto &c : components)
437  {
438  if(tmp_offset<=0)
439  return c;
440 
441  tmp_offset-=get_size(c.type());
442  }
443 
444  throw "access out of struct bounds";
445 }
446 
449 {
450  dynamic_typest::const_iterator it=dynamic_types.find(id);
451  if(it==dynamic_types.end())
452  return symbol_table.lookup_ref(id).type;
453  return it->second;
454 }
455 
459  const typet &type,
460  const mp_integer &offset,
461  bool use_non_det)
462 {
463  if(type.id() == ID_struct_tag)
464  {
465  struct_exprt result({}, type);
466  const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
467  const struct_typet::componentst &components=struct_type.components();
468 
469  // Retrieve the values for the individual members
470  result.reserve_operands(components.size());
471 
472  mp_integer tmp_offset=offset;
473 
474  for(const auto &c : components)
475  {
476  mp_integer size=get_size(c.type());
477  const exprt operand=get_value(c.type(), tmp_offset);
478  tmp_offset+=size;
479  result.copy_to_operands(operand);
480  }
481 
482  return std::move(result);
483  }
484  else if(type.id() == ID_array)
485  {
486  // Get size of array
487  array_exprt result({}, to_array_type(type));
488  const exprt &size_expr = to_array_type(type).size();
489  mp_integer subtype_size = get_size(to_array_type(type).element_type());
490  mp_integer count;
491  if(!size_expr.is_constant())
492  {
493  count=base_address_to_actual_size(offset)/subtype_size;
494  }
495  else
496  {
497  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
498  }
499 
500  // Retrieve the value for each member in the array
501  result.reserve_operands(numeric_cast_v<std::size_t>(count));
502  for(mp_integer i=0; i<count; ++i)
503  {
504  const exprt operand = get_value(
505  to_array_type(type).element_type(), offset + i * subtype_size);
506  result.copy_to_operands(operand);
507  }
508  return std::move(result);
509  }
510  if(
511  use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
513  {
515  }
516  mp_vectort rhs;
517  rhs.push_back(memory[numeric_cast_v<std::size_t>(offset)].value);
518  return get_value(type, rhs);
519 }
520 
524  const typet &type,
525  mp_vectort &rhs,
526  const mp_integer &offset)
527 {
528  PRECONDITION(!rhs.empty());
529 
530  if(type.id() == ID_struct_tag)
531  {
532  struct_exprt result({}, type);
533  const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
534  const struct_typet::componentst &components=struct_type.components();
535 
536  // Retrieve the values for the individual members
537  result.reserve_operands(components.size());
538  mp_integer tmp_offset=offset;
539 
540  for(const struct_union_typet::componentt &expr : components)
541  {
542  mp_integer size=get_size(expr.type());
543  const exprt operand=get_value(expr.type(), rhs, tmp_offset);
544  tmp_offset+=size;
545  result.copy_to_operands(operand);
546  }
547  return std::move(result);
548  }
549  else if(type.id() == ID_array)
550  {
551  array_exprt result({}, to_array_type(type));
552  const exprt &size_expr = to_array_type(type).size();
553 
554  // Get size of array
555  mp_integer subtype_size = get_size(to_array_type(type).element_type());
556 
557  mp_integer count;
558  if(unbounded_size(type))
559  {
560  count=base_address_to_actual_size(offset)/subtype_size;
561  }
562  else
563  {
564  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
565  }
566 
567  // Retrieve the value for each member in the array
568  result.reserve_operands(numeric_cast_v<std::size_t>(count));
569  for(mp_integer i=0; i<count; ++i)
570  {
571  const exprt operand = get_value(
572  to_array_type(type).element_type(), rhs, offset + i * subtype_size);
573  result.copy_to_operands(operand);
574  }
575  return std::move(result);
576  }
577  else if(type.id() == ID_floatbv)
578  {
579  ieee_floatt f(to_floatbv_type(type));
580  f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
581  return f.to_expr();
582  }
583  else if(type.id() == ID_fixedbv)
584  {
585  fixedbvt f;
586  f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
587  return f.to_expr();
588  }
589  else if(type.id() == ID_bool)
590  {
591  if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
592  return true_exprt();
593  else
594  false_exprt();
595  }
596  else if(type.id() == ID_c_bool)
597  {
598  return from_integer(
599  rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
600  }
601  else if(type.id() == ID_pointer)
602  {
603  if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
604  return null_pointer_exprt(to_pointer_type(type)); // NULL pointer
605 
606  if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
607  {
608  // We want the symbol pointed to
609  mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
610  const symbol_exprt symbol_expr = address_to_symbol(address);
611  mp_integer offset_from_address = address_to_offset(address);
612 
613  if(offset_from_address == 0)
614  return address_of_exprt(symbol_expr);
615 
616  if(
617  symbol_expr.type().id() == ID_struct ||
618  symbol_expr.type().id() == ID_struct_tag)
619  {
620  const auto c = get_component(symbol_expr.type(), offset_from_address);
621  member_exprt member_expr(symbol_expr, c);
622  return address_of_exprt(member_expr);
623  }
624 
625  return index_exprt(
626  symbol_expr, from_integer(offset_from_address, integer_typet()));
627  }
628 
629  output.error() << "interpreter: invalid pointer "
630  << rhs[numeric_cast_v<std::size_t>(offset)]
631  << " > object count " << memory.size() << messaget::eom;
632 
633  throw "interpreter: reading from invalid pointer";
634  }
635  else if(type.id() == ID_string)
636  {
637  // Strings are currently encoded by their irep_idt ID.
638  return constant_exprt(
639  get_string_container().get_string(
640  numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
641  type);
642  }
643 
644  // Retrieve value of basic data type
645  return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
646 }
647 
650 {
651  const exprt &assign_lhs = pc->assign_lhs();
652  const exprt &assign_rhs = pc->assign_rhs();
653 
654  mp_vectort rhs = evaluate(assign_rhs);
655 
656  if(!rhs.empty())
657  {
658  mp_integer address = evaluate_address(assign_lhs);
659  mp_integer size = get_size(assign_lhs.type());
660 
661  if(size!=rhs.size())
662  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
663  << size << ")\n"
664  << messaget::eom;
665  else
666  {
667  goto_trace_stept &trace_step=steps.get_last_step();
668  assign(address, rhs);
669  trace_step.full_lhs = assign_lhs;
670  trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
671  }
672  }
673  else if(assign_rhs.id() == ID_side_effect)
674  {
675  side_effect_exprt side_effect = to_side_effect_expr(assign_rhs);
676  if(side_effect.get_statement()==ID_nondet)
677  {
678  mp_integer address =
679  numeric_cast_v<std::size_t>(evaluate_address(assign_lhs));
680 
681  mp_integer size = get_size(assign_lhs.type());
682 
683  for(mp_integer i=0; i<size; ++i)
684  {
685  memory[numeric_cast_v<std::size_t>(address + i)].initialized =
687  }
688  }
689  }
690 }
691 
694  const mp_integer &address,
695  const mp_vectort &rhs)
696 {
697  for(mp_integer i=0; i<rhs.size(); ++i)
698  {
699  if((address+i)<memory.size())
700  {
701  mp_integer address_val=address+i;
702  memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
703  if(show)
704  {
705  output.status() << total_steps << " ** assigning "
706  << address_to_symbol(address_val).get_identifier()
707  << "[" << address_to_offset(address_val)
708  << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
709  << messaget::eom;
710  }
711  cell.value = rhs[numeric_cast_v<std::size_t>(i)];
714  }
715  }
716 }
717 
719 {
720  if(!evaluate_boolean(pc->condition()))
721  throw "assumption failed";
722 }
723 
725 {
726  if(!evaluate_boolean(pc->condition()))
727  {
728  if(show)
729  output.error() << "assertion failed at " << pc->location_number << "\n"
730  << messaget::eom;
731  }
732 }
733 
735 {
736  const auto &call_lhs = pc->call_lhs();
737  const auto &call_function = pc->call_function();
738  const auto &call_arguments = pc->call_arguments();
739 
740  // function to be called
741  mp_integer address = evaluate_address(call_function);
742 
743  if(address==0)
744  throw "function call to NULL";
745  else if(address>=memory.size())
746  throw "out-of-range function call";
747 
748  // Retrieve the empty last trace step struct we pushed for this step
749  // of the interpreter run to fill it with the corresponding data
750  goto_trace_stept &trace_step=steps.get_last_step();
751 #if 0
752  const memory_cellt &cell=memory[address];
753 #endif
754  const irep_idt identifier = address_to_symbol(address).get_identifier();
755  trace_step.called_function = identifier;
756 
757  const goto_functionst::function_mapt::const_iterator f_it=
758  goto_functions.function_map.find(identifier);
759 
760  if(f_it==goto_functions.function_map.end())
761  throw "failed to find function "+id2string(identifier);
762 
763  // return value
764  mp_integer return_value_address;
765 
766  if(call_lhs.is_not_nil())
767  return_value_address = evaluate_address(call_lhs);
768  else
769  return_value_address=0;
770 
771  // values of the arguments
772  std::vector<mp_vectort> argument_values;
773 
774  argument_values.resize(call_arguments.size());
775 
776  for(std::size_t i = 0; i < call_arguments.size(); i++)
777  argument_values[i] = evaluate(call_arguments[i]);
778 
779  // do the call
780 
781  if(f_it->second.body_available())
782  {
783  call_stack.push(stack_framet());
784  stack_framet &frame=call_stack.top();
785 
786  frame.return_pc=next_pc;
787  frame.return_function=function;
789  frame.return_value_address=return_value_address;
790 
791  // local variables
792  std::set<irep_idt> locals;
793  get_local_identifiers(f_it->second, locals);
794 
795  for(const auto &id : locals)
796  {
797  const symbolt &symbol=ns.lookup(id);
798  frame.local_map[id] = build_memory_map(symbol.symbol_expr());
799  }
800 
801  // assign the arguments
802  const auto &parameter_identifiers = f_it->second.parameter_identifiers;
803  if(argument_values.size() < parameter_identifiers.size())
804  throw "not enough arguments";
805 
806  for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
807  {
808  const symbol_exprt symbol_expr =
809  ns.lookup(parameter_identifiers[i]).symbol_expr();
810  assign(evaluate_address(symbol_expr), argument_values[i]);
811  }
812 
813  // set up new pc
814  function=f_it;
815  next_pc=f_it->second.body.instructions.begin();
816  }
817  else
818  {
819  list_input_varst::iterator it =
820  function_input_vars.find(to_symbol_expr(call_function).get_identifier());
821 
822  if(it!=function_input_vars.end())
823  {
824  PRECONDITION(!it->second.empty());
825  PRECONDITION(!it->second.front().return_assignments.empty());
826  mp_vectort value =
827  evaluate(it->second.front().return_assignments.back().value);
828  if(return_value_address>0)
829  {
830  assign(return_value_address, value);
831  }
832  it->second.pop_front();
833  return;
834  }
835 
836  if(show)
837  output.error() << "no body for " << identifier << messaget::eom;
838  }
839 }
840 
843 {
844  // put in a dummy for NULL
845  memory.clear();
846  memory.resize(1);
847  inverse_memory_map[0] = {};
848 
850  dynamic_types.clear();
851 
852  // now do regular static symbols
853  for(const auto &s : symbol_table.symbols)
854  build_memory_map(s.second);
855 
856  // for the locals
858 }
859 
861 {
862  mp_integer size=0;
863 
864  if(symbol.type.id()==ID_code)
865  {
866  size=1;
867  }
868  else if(symbol.is_static_lifetime)
869  {
870  size=get_size(symbol.type);
871  }
872 
873  if(size!=0)
874  {
875  mp_integer address=memory.size();
876  memory.resize(numeric_cast_v<std::size_t>(address + size));
877  memory_map[symbol.name]=address;
878  inverse_memory_map[address] = symbol.symbol_expr();
879  }
880 }
881 
884 {
885  if(type.id()==ID_array)
886  {
887  const exprt &size_expr = to_array_type(type).size();
888  mp_vectort computed_size = evaluate(size_expr);
889  if(computed_size.size()==1 &&
890  computed_size[0]>=0)
891  {
892  output.result() << "Concretized array with size " << computed_size[0]
893  << messaget::eom;
894  return array_typet(
895  to_array_type(type).element_type(),
896  from_integer(computed_size[0], integer_typet()));
897  }
898  else
899  {
900  output.warning() << "Failed to concretize variable array"
901  << messaget::eom;
902  }
903  }
904  return type;
905 }
906 
910 {
911  typet alloc_type = concretize_type(symbol_expr.type());
912  mp_integer size=get_size(alloc_type);
913  auto it = dynamic_types.find(symbol_expr.get_identifier());
914 
915  if(it!=dynamic_types.end())
916  {
917  mp_integer address = memory_map[symbol_expr.get_identifier()];
918  mp_integer current_size=base_address_to_alloc_size(address);
919  // current size <= size already recorded
920  if(size<=current_size)
921  return memory_map[symbol_expr.get_identifier()];
922  }
923 
924  // The current size is bigger then the one previously recorded
925  // in the memory map
926 
927  if(size==0)
928  size=1; // This is a hack to create existence
929 
930  mp_integer address=memory.size();
931  memory.resize(numeric_cast_v<std::size_t>(address + size));
932  memory_map[symbol_expr.get_identifier()] = address;
933  inverse_memory_map[address] = symbol_expr;
934  dynamic_types.insert(
935  std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
936 
937  return address;
938 }
939 
941 {
942  if(type.id()==ID_array)
943  {
944  const exprt &size=to_array_type(type).size();
945  if(size.id()==ID_infinity)
946  return true;
947  return unbounded_size(to_array_type(type).element_type());
948  }
949  else if(type.id()==ID_struct)
950  {
951  const auto &st=to_struct_type(type);
952  if(st.components().empty())
953  return false;
954  return unbounded_size(st.components().back().type());
955  }
956  return false;
957 }
958 
964 {
965  if(unbounded_size(type))
966  return mp_integer(2) << (sizeof(std::size_t) * CHAR_BIT / 2);
967 
968  if(type.id()==ID_struct)
969  {
970  const struct_typet::componentst &components=
971  to_struct_type(type).components();
972 
973  mp_integer sum=0;
974 
975  for(const auto &comp : components)
976  {
978  comp.type().id() != ID_code, "struct member must not be of code type");
979  sum += get_size(comp.type());
980  }
981 
982  return sum;
983  }
984  else if(type.id()==ID_union)
985  {
986  const union_typet::componentst &components=
987  to_union_type(type).components();
988 
989  mp_integer max_size=0;
990 
991  for(const auto &comp : components)
992  {
994  comp.type().id() != ID_code, "union member must not be of code type");
995  max_size = std::max(max_size, get_size(comp.type()));
996  }
997 
998  return max_size;
999  }
1000  else if(type.id()==ID_array)
1001  {
1002  const exprt &size_expr = to_array_type(type).size();
1003 
1004  mp_integer subtype_size = get_size(to_array_type(type).element_type());
1005 
1006  mp_vectort i = evaluate(size_expr);
1007  if(i.size()==1)
1008  {
1009  // Go via the binary representation to reproduce any
1010  // overflow behaviour.
1011  const constant_exprt size_const = from_integer(i[0], size_expr.type());
1012  const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
1013  return subtype_size*size_mp;
1014  }
1015  return subtype_size;
1016  }
1017  else if(type.id() == ID_struct_tag)
1018  {
1019  return get_size(ns.follow_tag(to_struct_tag_type(type)));
1020  }
1021 
1022  return 1;
1023 }
1024 
1026 {
1027  // The dynamic type and the static symbol type may differ for VLAs,
1028  // where the symbol carries a size expression and the dynamic type
1029  // registry contains its actual length.
1030  auto findit=dynamic_types.find(id);
1031  typet get_type;
1032  if(findit!=dynamic_types.end())
1033  get_type=findit->second;
1034  else
1036 
1037  symbol_exprt symbol_expr(id, get_type);
1038  mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
1039 
1040  return get_value(get_type, whole_lhs_object_address);
1041 }
1042 
1045 void interpretert::print_memory(bool input_flags)
1046 {
1047  for(const auto &cell_address : memory)
1048  {
1049  mp_integer i=cell_address.first;
1050  const memory_cellt &cell=cell_address.second;
1051  const auto identifier = address_to_symbol(i).get_identifier();
1052  const auto offset=address_to_offset(i);
1053  output.status() << identifier << "[" << offset << "]"
1054  << "=" << cell.value << messaget::eom;
1055  if(input_flags)
1056  output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1057  << messaget::eom;
1059  }
1060 }
1061 
1063  const goto_modelt &goto_model,
1064  message_handlert &message_handler)
1065 {
1067  goto_model.symbol_table,
1068  goto_model.goto_functions,
1069  message_handler);
1070  interpreter();
1071 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
Operator to return the address of an object.
Definition: pointer_expr.h:540
Array constructor from list of elements.
Definition: std_expr.h:1616
Arrays with given size.
Definition: std_types.h:807
const exprt & size() const
Definition: std_types.h:840
A constant literal expression.
Definition: std_expr.h:2990
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
The Boolean constant false.
Definition: std_expr.h:3072
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:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
exprt full_lhs_value
Definition: goto_trace.h:133
goto_programt::const_targett pc
Definition: goto_trace.h:112
unsigned thread_nr
Definition: goto_trace.h:115
irep_idt called_function
Definition: goto_trace.h:142
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:57
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:320
constant_exprt to_expr() const
Definition: ieee_float.cpp:703
Array index operator.
Definition: std_expr.h:1465
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:38
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
mp_vectort evaluate(const exprt &)
Evaluate an expression.
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
const symbol_table_baset & symbol_table
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.
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:62
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 irep_idt & id() const
Definition: irep.h:388
void output(std::ostream &out) const
Definition: json.h:90
Extract member of struct or union.
Definition: std_expr.h:2844
mstreamt & error() const
Definition: message.h:391
mstreamt & warning() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:406
mstreamt & result() const
Definition: message.h:401
static eomt eom
Definition: message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The null pointer constant.
Definition: pointer_expr.h:909
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
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:1872
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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:70
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:3063
The type of an expression, extends irept.
Definition: type.h:29
int tolower(int c)
Definition: ctype.c:109
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...
bool can_cast_expr< code_outputt >(const exprt &base)
Symbol Table + CFG.
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
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:44
Traces of GOTO Programs.
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
BigInt mp_integer
Definition: smt_terms.h:17
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
static 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:49
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
char * fgets(char *str, int size, FILE *stream)
Definition: stdio.c:321
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:40
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.