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 <fstream>
17 #include <algorithm>
18 
19 #include <util/c_types.h>
20 #include <util/fixedbv.h>
21 #include <util/ieee_float.h>
22 #include <util/invariant.h>
24 #include <util/message.h>
25 #include <util/pointer_expr.h>
26 #include <util/std_code.h>
27 #include <util/std_expr.h>
28 #include <util/string2int.h>
29 #include <util/string_container.h>
30 #include <util/symbol_table.h>
31 
32 #include "goto_model.h"
33 #include "interpreter_class.h"
34 #include "json_goto_trace.h"
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  function->second.body.output_instruction(
124  ns, function->first, output.status(), *pc);
125 
127 }
128 
131 {
132  #define BUFSIZE 100
133  char command[BUFSIZE];
134  if(fgets(command, BUFSIZE-1, stdin)==nullptr)
135  {
136  done=true;
137  return;
138  }
139 
140  char ch=tolower(command[0]);
141  if(ch=='q')
142  done=true;
143  else if(ch=='h')
144  {
145  output.status() << "Interpreter help\n"
146  << "h: display this menu\n"
147  << "j: output json trace\n"
148  << "m: output memory dump\n"
149  << "o: output goto trace\n"
150  << "q: quit\n"
151  << "r: run up to entry point\n"
152  << "s#: step a number of instructions\n"
153  << "sa: step across a function\n"
154  << "so: step out of a function\n"
155  << "se: step until end of program\n"
156  << messaget::eom;
157  }
158  else if(ch=='j')
159  {
160  json_arrayt json_steps;
161  convert<json_arrayt>(ns, steps, json_steps);
162  ch=tolower(command[1]);
163  if(ch==' ')
164  {
165  std::ofstream file;
166  file.open(command+2);
167  if(file.is_open())
168  {
169  json_steps.output(file);
170  file.close();
171  return;
172  }
173  }
174  json_steps.output(output.result());
175  }
176  else if(ch=='m')
177  {
178  ch=tolower(command[1]);
179  print_memory(ch=='i');
180  }
181  else if(ch=='o')
182  {
183  ch=tolower(command[1]);
184  if(ch==' ')
185  {
186  std::ofstream file;
187  file.open(command+2);
188  if(file.is_open())
189  {
190  steps.output(ns, file);
191  file.close();
192  return;
193  }
194  }
196  }
197  else if(ch=='r')
198  {
199  ch=tolower(command[1]);
200  initialize(ch!='0');
201  }
202  else if((ch=='s') || (ch==0))
203  {
204  num_steps=1;
205  std::size_t stack_depth = npos;
206  ch=tolower(command[1]);
207  if(ch=='e')
208  num_steps=npos;
209  else if(ch=='o')
210  stack_depth=call_stack.size();
211  else if(ch=='a')
212  stack_depth=call_stack.size()+1;
213  else
214  {
216  if(num_steps==0)
217  num_steps=1;
218  }
219  while(!done && ((num_steps==npos) || ((num_steps--)>0)))
220  {
221  step();
222  show_state();
223  }
224  while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
225  {
226  step();
227  show_state();
228  }
229  return;
230  }
231  show_state();
232 }
233 
236 {
237  total_steps++;
238  if(pc==function->second.body.instructions.end())
239  {
240  if(call_stack.empty())
241  done=true;
242  else
243  {
244  pc=call_stack.top().return_pc;
245  function=call_stack.top().return_function;
246  // TODO: this increases memory size quite quickly.
247  // Should check alternatives
248  call_stack.pop();
249  }
250 
251  return;
252  }
253 
254  next_pc=pc;
255  next_pc++;
256 
258  goto_trace_stept &trace_step=steps.get_last_step();
259  trace_step.thread_nr=thread_id;
260  trace_step.pc=pc;
261  switch(pc->type())
262  {
263  case GOTO:
265  execute_goto();
266  break;
267 
268  case ASSUME:
270  execute_assume();
271  break;
272 
273  case ASSERT:
275  execute_assert();
276  break;
277 
278  case OTHER:
279  execute_other();
280  break;
281 
282  case DECL:
284  execute_decl();
285  break;
286 
287  case SKIP:
288  case LOCATION:
290  break;
291  case END_FUNCTION:
293  break;
294 
295  case SET_RETURN_VALUE:
297  if(call_stack.empty())
298  throw "SET_RETURN_VALUE without call"; // NOLINT(readability/throw)
299 
300  if(call_stack.top().return_value_address != 0)
301  {
302  mp_vectort rhs = evaluate(pc->return_value());
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->get_code().operands().size() == 1,
392  "expression statement expected to have one operand");
393  mp_vectort rhs = evaluate(pc->get_code().op0());
394  }
395  else if(statement==ID_array_set)
396  {
397  mp_vectort tmp = evaluate(pc->get_code().op1());
398  mp_integer address = evaluate_address(pc->get_code().op0());
399  mp_integer size = get_size(pc->get_code().op0().type());
400  mp_vectort rhs;
401  while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
402  if(size!=rhs.size())
403  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
404  << size << ")\n"
405  << messaget::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->get_code().get_statement() == ID_decl);
422 }
423 
426 interpretert::get_component(const typet &object_type, const mp_integer &offset)
427 {
428  const typet real_type = ns.follow(object_type);
429  if(real_type.id()!=ID_struct)
430  throw "request for member of non-struct";
431 
432  const struct_typet &struct_type=to_struct_type(real_type);
433  const struct_typet::componentst &components=struct_type.components();
434 
435  mp_integer tmp_offset=offset;
436 
437  for(const auto &c : components)
438  {
439  if(tmp_offset<=0)
440  return c;
441 
442  tmp_offset-=get_size(c.type());
443  }
444 
445  throw "access out of struct bounds";
446 }
447 
450 {
451  dynamic_typest::const_iterator it=dynamic_types.find(id);
452  if(it==dynamic_types.end())
453  return symbol_table.lookup_ref(id).type;
454  return it->second;
455 }
456 
460  const typet &type,
461  const mp_integer &offset,
462  bool use_non_det)
463 {
464  const typet real_type=ns.follow(type);
465  if(real_type.id()==ID_struct)
466  {
467  struct_exprt result({}, real_type);
468  const struct_typet &struct_type=to_struct_type(real_type);
469  const struct_typet::componentst &components=struct_type.components();
470 
471  // Retrieve the values for the individual members
472  result.reserve_operands(components.size());
473 
474  mp_integer tmp_offset=offset;
475 
476  for(const auto &c : components)
477  {
478  mp_integer size=get_size(c.type());
479  const exprt operand=get_value(c.type(), tmp_offset);
480  tmp_offset+=size;
481  result.copy_to_operands(operand);
482  }
483 
484  return std::move(result);
485  }
486  else if(real_type.id()==ID_array)
487  {
488  // Get size of array
489  array_exprt result({}, to_array_type(real_type));
490  const exprt &size_expr = to_array_type(type).size();
491  mp_integer subtype_size = get_size(to_array_type(type).element_type());
492  mp_integer count;
493  if(size_expr.id()!=ID_constant)
494  {
495  count=base_address_to_actual_size(offset)/subtype_size;
496  }
497  else
498  {
499  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
500  }
501 
502  // Retrieve the value for each member in the array
503  result.reserve_operands(numeric_cast_v<std::size_t>(count));
504  for(mp_integer i=0; i<count; ++i)
505  {
506  const exprt operand = get_value(
507  to_array_type(type).element_type(), offset + i * subtype_size);
508  result.copy_to_operands(operand);
509  }
510  return std::move(result);
511  }
512  if(
513  use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
515  {
517  }
518  mp_vectort rhs;
519  rhs.push_back(memory[numeric_cast_v<std::size_t>(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 = to_array_type(real_type).size();
556 
557  // Get size of array
558  mp_integer subtype_size = get_size(to_array_type(type).element_type());
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>(to_constant_expr(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(
575  to_array_type(type).element_type(), rhs, 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  const symbol_exprt &symbol_expr = address_to_symbol(address);
614  mp_integer offset_from_address = address_to_offset(address);
615 
616  if(offset_from_address == 0)
617  return address_of_exprt(symbol_expr);
618 
619  if(
620  symbol_expr.type().id() == ID_struct ||
621  symbol_expr.type().id() == ID_struct_tag)
622  {
623  const auto c = get_component(symbol_expr.type(), offset_from_address);
624  member_exprt member_expr(symbol_expr, c);
625  return address_of_exprt(member_expr);
626  }
627 
628  return index_exprt(
629  symbol_expr, from_integer(offset_from_address, integer_typet()));
630  }
631 
632  output.error() << "interpreter: invalid pointer "
633  << rhs[numeric_cast_v<std::size_t>(offset)]
634  << " > object count " << memory.size() << messaget::eom;
635 
636  throw "interpreter: reading from invalid pointer";
637  }
638  else if(real_type.id()==ID_string)
639  {
640  // Strings are currently encoded by their irep_idt ID.
641  return constant_exprt(
642  get_string_container().get_string(
643  numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
644  type);
645  }
646 
647  // Retrieve value of basic data type
648  return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
649 }
650 
653 {
654  const exprt &assign_lhs = pc->assign_lhs();
655  const exprt &assign_rhs = pc->assign_rhs();
656 
657  mp_vectort rhs = evaluate(assign_rhs);
658 
659  if(!rhs.empty())
660  {
661  mp_integer address = evaluate_address(assign_lhs);
662  mp_integer size = get_size(assign_lhs.type());
663 
664  if(size!=rhs.size())
665  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
666  << size << ")\n"
667  << messaget::eom;
668  else
669  {
670  goto_trace_stept &trace_step=steps.get_last_step();
671  assign(address, rhs);
672  trace_step.full_lhs = assign_lhs;
673  trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
674  }
675  }
676  else if(assign_rhs.id() == ID_side_effect)
677  {
678  side_effect_exprt side_effect = to_side_effect_expr(assign_rhs);
679  if(side_effect.get_statement()==ID_nondet)
680  {
681  mp_integer address =
682  numeric_cast_v<std::size_t>(evaluate_address(assign_lhs));
683 
684  mp_integer size = get_size(assign_lhs.type());
685 
686  for(mp_integer i=0; i<size; ++i)
687  {
688  memory[numeric_cast_v<std::size_t>(address + i)].initialized =
690  }
691  }
692  }
693 }
694 
697  const mp_integer &address,
698  const mp_vectort &rhs)
699 {
700  for(mp_integer i=0; i<rhs.size(); ++i)
701  {
702  if((address+i)<memory.size())
703  {
704  mp_integer address_val=address+i;
705  memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
706  if(show)
707  {
708  output.status() << total_steps << " ** assigning "
709  << address_to_symbol(address_val).get_identifier()
710  << "[" << address_to_offset(address_val)
711  << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
712  << messaget::eom;
713  }
714  cell.value = rhs[numeric_cast_v<std::size_t>(i)];
717  }
718  }
719 }
720 
722 {
723  if(!evaluate_boolean(pc->get_condition()))
724  throw "assumption failed";
725 }
726 
728 {
729  if(!evaluate_boolean(pc->get_condition()))
730  {
731  if(show)
732  output.error() << "assertion failed at " << pc->location_number << "\n"
733  << messaget::eom;
734  }
735 }
736 
738 {
739  const auto &call_lhs = pc->call_lhs();
740  const auto &call_function = pc->call_function();
741  const auto &call_arguments = pc->call_arguments();
742 
743  // function to be called
744  mp_integer address = evaluate_address(call_function);
745 
746  if(address==0)
747  throw "function call to NULL";
748  else if(address>=memory.size())
749  throw "out-of-range function call";
750 
751  // Retrieve the empty last trace step struct we pushed for this step
752  // of the interpreter run to fill it with the corresponding data
753  goto_trace_stept &trace_step=steps.get_last_step();
754 #if 0
755  const memory_cellt &cell=memory[address];
756 #endif
757  const irep_idt &identifier = address_to_symbol(address).get_identifier();
758  trace_step.called_function = identifier;
759 
760  const goto_functionst::function_mapt::const_iterator f_it=
761  goto_functions.function_map.find(identifier);
762 
763  if(f_it==goto_functions.function_map.end())
764  throw "failed to find function "+id2string(identifier);
765 
766  // return value
767  mp_integer return_value_address;
768 
769  if(call_lhs.is_not_nil())
770  return_value_address = evaluate_address(call_lhs);
771  else
772  return_value_address=0;
773 
774  // values of the arguments
775  std::vector<mp_vectort> argument_values;
776 
777  argument_values.resize(call_arguments.size());
778 
779  for(std::size_t i = 0; i < call_arguments.size(); i++)
780  argument_values[i] = evaluate(call_arguments[i]);
781 
782  // do the call
783 
784  if(f_it->second.body_available())
785  {
786  call_stack.push(stack_framet());
787  stack_framet &frame=call_stack.top();
788 
789  frame.return_pc=next_pc;
790  frame.return_function=function;
792  frame.return_value_address=return_value_address;
793 
794  // local variables
795  std::set<irep_idt> locals;
796  get_local_identifiers(f_it->second, locals);
797 
798  for(const auto &id : locals)
799  {
800  const symbolt &symbol=ns.lookup(id);
801  frame.local_map[id] = build_memory_map(symbol.symbol_expr());
802  }
803 
804  // assign the arguments
805  const auto &parameter_identifiers = f_it->second.parameter_identifiers;
806  if(argument_values.size() < parameter_identifiers.size())
807  throw "not enough arguments";
808 
809  for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
810  {
811  const symbol_exprt symbol_expr =
812  ns.lookup(parameter_identifiers[i]).symbol_expr();
813  assign(evaluate_address(symbol_expr), argument_values[i]);
814  }
815 
816  // set up new pc
817  function=f_it;
818  next_pc=f_it->second.body.instructions.begin();
819  }
820  else
821  {
822  list_input_varst::iterator it =
823  function_input_vars.find(to_symbol_expr(call_function).get_identifier());
824 
825  if(it!=function_input_vars.end())
826  {
827  PRECONDITION(!it->second.empty());
828  PRECONDITION(!it->second.front().return_assignments.empty());
829  mp_vectort value =
830  evaluate(it->second.front().return_assignments.back().value);
831  if(return_value_address>0)
832  {
833  assign(return_value_address, value);
834  }
835  it->second.pop_front();
836  return;
837  }
838 
839  if(show)
840  output.error() << "no body for " << identifier << messaget::eom;
841  }
842 }
843 
846 {
847  // put in a dummy for NULL
848  memory.clear();
849  memory.resize(1);
850  inverse_memory_map[0] = {};
851 
853  dynamic_types.clear();
854 
855  // now do regular static symbols
856  for(const auto &s : symbol_table.symbols)
857  build_memory_map(s.second);
858 
859  // for the locals
861 }
862 
864 {
865  mp_integer size=0;
866 
867  if(symbol.type.id()==ID_code)
868  {
869  size=1;
870  }
871  else if(symbol.is_static_lifetime)
872  {
873  size=get_size(symbol.type);
874  }
875 
876  if(size!=0)
877  {
878  mp_integer address=memory.size();
879  memory.resize(numeric_cast_v<std::size_t>(address + size));
880  memory_map[symbol.name]=address;
881  inverse_memory_map[address] = symbol.symbol_expr();
882  }
883 }
884 
887 {
888  if(type.id()==ID_array)
889  {
890  const exprt &size_expr = to_array_type(type).size();
891  mp_vectort computed_size = evaluate(size_expr);
892  if(computed_size.size()==1 &&
893  computed_size[0]>=0)
894  {
895  output.result() << "Concretized array with size " << computed_size[0]
896  << messaget::eom;
897  return array_typet(
898  to_array_type(type).element_type(),
899  from_integer(computed_size[0], integer_typet()));
900  }
901  else
902  {
903  output.warning() << "Failed to concretize variable array"
904  << messaget::eom;
905  }
906  }
907  return type;
908 }
909 
913 {
914  typet alloc_type = concretize_type(symbol_expr.type());
915  mp_integer size=get_size(alloc_type);
916  auto it = dynamic_types.find(symbol_expr.get_identifier());
917 
918  if(it!=dynamic_types.end())
919  {
920  mp_integer address = memory_map[symbol_expr.get_identifier()];
921  mp_integer current_size=base_address_to_alloc_size(address);
922  // current size <= size already recorded
923  if(size<=current_size)
924  return memory_map[symbol_expr.get_identifier()];
925  }
926 
927  // The current size is bigger then the one previously recorded
928  // in the memory map
929 
930  if(size==0)
931  size=1; // This is a hack to create existence
932 
933  mp_integer address=memory.size();
934  memory.resize(numeric_cast_v<std::size_t>(address + size));
935  memory_map[symbol_expr.get_identifier()] = address;
936  inverse_memory_map[address] = symbol_expr;
937  dynamic_types.insert(
938  std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
939 
940  return address;
941 }
942 
944 {
945  if(type.id()==ID_array)
946  {
947  const exprt &size=to_array_type(type).size();
948  if(size.id()==ID_infinity)
949  return true;
950  return unbounded_size(to_array_type(type).element_type());
951  }
952  else if(type.id()==ID_struct)
953  {
954  const auto &st=to_struct_type(type);
955  if(st.components().empty())
956  return false;
957  return unbounded_size(st.components().back().type());
958  }
959  return false;
960 }
961 
967 {
968  if(unbounded_size(type))
969  return mp_integer(2) << 32;
970 
971  if(type.id()==ID_struct)
972  {
973  const struct_typet::componentst &components=
974  to_struct_type(type).components();
975 
976  mp_integer sum=0;
977 
978  for(const auto &comp : components)
979  {
980  const typet &sub_type=comp.type();
981 
982  if(sub_type.id()!=ID_code)
983  sum+=get_size(sub_type);
984  }
985 
986  return sum;
987  }
988  else if(type.id()==ID_union)
989  {
990  const union_typet::componentst &components=
991  to_union_type(type).components();
992 
993  mp_integer max_size=0;
994 
995  for(const auto &comp : components)
996  {
997  const typet &sub_type=comp.type();
998 
999  if(sub_type.id()!=ID_code)
1000  max_size=std::max(max_size, get_size(sub_type));
1001  }
1002 
1003  return max_size;
1004  }
1005  else if(type.id()==ID_array)
1006  {
1007  const exprt &size_expr = to_array_type(type).size();
1008 
1009  mp_integer subtype_size = get_size(to_array_type(type).element_type());
1010 
1011  mp_vectort i = evaluate(size_expr);
1012  if(i.size()==1)
1013  {
1014  // Go via the binary representation to reproduce any
1015  // overflow behaviour.
1016  const constant_exprt size_const = from_integer(i[0], size_expr.type());
1017  const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
1018  return subtype_size*size_mp;
1019  }
1020  return subtype_size;
1021  }
1022  else if(type.id() == ID_struct_tag)
1023  {
1024  return get_size(ns.follow_tag(to_struct_tag_type(type)));
1025  }
1026 
1027  return 1;
1028 }
1029 
1031 {
1032  // The dynamic type and the static symbol type may differ for VLAs,
1033  // where the symbol carries a size expression and the dynamic type
1034  // registry contains its actual length.
1035  auto findit=dynamic_types.find(id);
1036  typet get_type;
1037  if(findit!=dynamic_types.end())
1038  get_type=findit->second;
1039  else
1041 
1042  symbol_exprt symbol_expr(id, get_type);
1043  mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
1044 
1045  return get_value(get_type, whole_lhs_object_address);
1046 }
1047 
1050 void interpretert::print_memory(bool input_flags)
1051 {
1052  for(const auto &cell_address : memory)
1053  {
1054  mp_integer i=cell_address.first;
1055  const memory_cellt &cell=cell_address.second;
1056  const auto identifier = address_to_symbol(i).get_identifier();
1057  const auto offset=address_to_offset(i);
1058  output.status() << identifier << "[" << offset << "]"
1059  << "=" << cell.value << messaget::eom;
1060  if(input_flags)
1061  output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1062  << messaget::eom;
1064  }
1065 }
1066 
1068  const goto_modelt &goto_model,
1069  message_handlert &message_handler)
1070 {
1072  goto_model.symbol_table,
1073  goto_model.goto_functions,
1074  message_handler);
1075  interpreter();
1076 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:162
Operator to return the address of an object.
Definition: pointer_expr.h:361
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:790
A constant literal expression.
Definition: std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
exprt full_lhs_value
Definition: goto_trace.h:132
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:141
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:203
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition: goto_trace.h:196
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:56
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:319
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
Array index operator.
Definition: std_expr.h:1328
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
void step()
executes a single step and updates the program counter
struct_typet::componentt get_component(const typet &object_type, const mp_integer &offset)
Retrieves the member at offset of an object of type object_type.
mp_integer base_address_to_alloc_size(const mp_integer &address) const
input_valuest input_vars
const namespacet ns
goto_programt::const_targett next_pc
bool evaluate_boolean(const exprt &expr)
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
const symbol_tablet & symbol_table
void show_state()
displays the current position of the pc and corresponding code
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
Definition: interpreter.cpp: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:396
void output(std::ostream &out) const
Definition: json.h:90
Extract member of struct or union.
Definition: std_expr.h:2667
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & status() const
Definition: message.h:414
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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:138
The null pointer constant.
Definition: pointer_expr.h:723
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:1722
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:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp: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:2856
The type of an expression, extends irept.
Definition: type.h:29
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:47
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:79
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#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:61
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:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
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:832
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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.
Definition: kdev_t.h:19
Author: Diffblue Ltd.