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_expr.h>
27 #include <util/string2int.h>
28 #include <util/string_container.h>
29 #include <util/symbol_table.h>
30 
31 #include "goto_model.h"
32 #include "interpreter_class.h"
33 #include "json_goto_trace.h"
34 
35 const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
36 
38 {
39  output.status() << "0- Initialize:" << messaget::eom;
40  initialize(true);
41  try
42  {
43  output.status() << "Type h for help\n" << messaget::eom;
44 
45  while(!done)
46  command();
47 
48  output.status() << total_steps << "- Program End.\n" << messaget::eom;
49  }
50  catch (const char *e)
51  {
52  output.error() << e << "\n" << messaget::eom;
53  }
54 
55  while(!done)
56  command();
57 }
58 
61 void interpretert::initialize(bool init)
62 {
64  // reset the call stack
66 
67  total_steps=0;
68  const goto_functionst::function_mapt::const_iterator
70 
71  if(main_it==goto_functions.function_map.end())
72  throw "main not found";
73 
74  const goto_functionst::goto_functiont &goto_function=main_it->second;
75 
76  if(!goto_function.body_available())
77  throw "main has no body";
78 
79  pc=goto_function.body.instructions.begin();
80  function=main_it;
81 
82  done=false;
83  if(init)
84  {
85  // execute instructions up to and including __CPROVER_initialize()
86  while(!done && call_stack.size() == 0)
87  {
88  show_state();
89  step();
90  }
91  // initialization
92  while(!done && call_stack.size() > 0)
93  {
94  show_state();
95  step();
96  }
97  // invoke the user entry point
98  while(!done && call_stack.size() == 0)
99  {
100  show_state();
101  step();
102  }
104  input_vars.clear();
105  }
106 }
107 
110 {
111  if(!show)
112  return;
113  output.status() << "\n"
114  << total_steps + 1
115  << " ----------------------------------------------------\n";
116 
117  if(pc==function->second.body.instructions.end())
118  {
119  output.status() << "End of function '" << function->first << "'\n";
120  }
121  else
122  function->second.body.output_instruction(
123  ns, function->first, output.status(), *pc);
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;
302  evaluate(pc->return_value(), 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->get_code().operands().size() == 1,
392  "expression statement expected to have one operand");
393  mp_vectort rhs;
394  evaluate(pc->get_code().op0(), rhs);
395  }
396  else if(statement==ID_array_set)
397  {
398  mp_vectort tmp, rhs;
399  evaluate(pc->get_code().op1(), tmp);
400  mp_integer address = evaluate_address(pc->get_code().op0());
401  mp_integer size = get_size(pc->get_code().op0().type());
402  while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
403  if(size!=rhs.size())
404  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
405  << size << ")\n"
406  << messaget::eom;
407  else
408  {
409  assign(address, rhs);
410  }
411  }
412  else if(can_cast_expr<code_outputt>(pc->get_other()))
413  {
414  return;
415  }
416  else
417  throw "unexpected OTHER statement: "+id2string(statement);
418 }
419 
421 {
422  PRECONDITION(pc->get_code().get_statement() == ID_decl);
423 }
424 
427 interpretert::get_component(const typet &object_type, const mp_integer &offset)
428 {
429  const typet real_type = ns.follow(object_type);
430  if(real_type.id()!=ID_struct)
431  throw "request for member of non-struct";
432 
433  const struct_typet &struct_type=to_struct_type(real_type);
434  const struct_typet::componentst &components=struct_type.components();
435 
436  mp_integer tmp_offset=offset;
437 
438  for(const auto &c : components)
439  {
440  if(tmp_offset<=0)
441  return c;
442 
443  tmp_offset-=get_size(c.type());
444  }
445 
446  throw "access out of struct bounds";
447 }
448 
451 {
452  dynamic_typest::const_iterator it=dynamic_types.find(id);
453  if(it==dynamic_types.end())
454  return symbol_table.lookup_ref(id).type;
455  return it->second;
456 }
457 
461  const typet &type,
462  const mp_integer &offset,
463  bool use_non_det)
464 {
465  const typet real_type=ns.follow(type);
466  if(real_type.id()==ID_struct)
467  {
468  struct_exprt result({}, real_type);
469  const struct_typet &struct_type=to_struct_type(real_type);
470  const struct_typet::componentst &components=struct_type.components();
471 
472  // Retrieve the values for the individual members
473  result.reserve_operands(components.size());
474 
475  mp_integer tmp_offset=offset;
476 
477  for(const auto &c : components)
478  {
479  mp_integer size=get_size(c.type());
480  const exprt operand=get_value(c.type(), tmp_offset);
481  tmp_offset+=size;
482  result.copy_to_operands(operand);
483  }
484 
485  return std::move(result);
486  }
487  else if(real_type.id()==ID_array)
488  {
489  // Get size of array
490  array_exprt result({}, to_array_type(real_type));
491  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
492  mp_integer subtype_size=get_size(type.subtype());
493  mp_integer count;
494  if(size_expr.id()!=ID_constant)
495  {
496  count=base_address_to_actual_size(offset)/subtype_size;
497  }
498  else
499  {
500  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
501  }
502 
503  // Retrieve the value for each member in the array
504  result.reserve_operands(numeric_cast_v<std::size_t>(count));
505  for(mp_integer i=0; i<count; ++i)
506  {
507  const exprt operand=get_value(
508  type.subtype(),
509  offset+i*subtype_size);
510  result.copy_to_operands(operand);
511  }
512  return std::move(result);
513  }
514  if(
515  use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
517  {
519  }
520  mp_vectort rhs;
521  rhs.push_back(memory[numeric_cast_v<std::size_t>(offset)].value);
522  return get_value(type, rhs);
523 }
524 
528  const typet &type,
529  mp_vectort &rhs,
530  const mp_integer &offset)
531 {
532  const typet real_type=ns.follow(type);
533  PRECONDITION(!rhs.empty());
534 
535  if(real_type.id()==ID_struct)
536  {
537  struct_exprt result({}, real_type);
538  const struct_typet &struct_type=to_struct_type(real_type);
539  const struct_typet::componentst &components=struct_type.components();
540 
541  // Retrieve the values for the individual members
542  result.reserve_operands(components.size());
543  mp_integer tmp_offset=offset;
544 
545  for(const struct_union_typet::componentt &expr : components)
546  {
547  mp_integer size=get_size(expr.type());
548  const exprt operand=get_value(expr.type(), rhs, tmp_offset);
549  tmp_offset+=size;
550  result.copy_to_operands(operand);
551  }
552  return std::move(result);
553  }
554  else if(real_type.id()==ID_array)
555  {
556  array_exprt result({}, to_array_type(real_type));
557  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
558 
559  // Get size of array
560  mp_integer subtype_size=get_size(type.subtype());
561 
562  mp_integer count;
563  if(unbounded_size(type))
564  {
565  count=base_address_to_actual_size(offset)/subtype_size;
566  }
567  else
568  {
569  count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
570  }
571 
572  // Retrieve the value for each member in the array
573  result.reserve_operands(numeric_cast_v<std::size_t>(count));
574  for(mp_integer i=0; i<count; ++i)
575  {
576  const exprt operand=get_value(type.subtype(), rhs,
577  offset+i*subtype_size);
578  result.copy_to_operands(operand);
579  }
580  return std::move(result);
581  }
582  else if(real_type.id()==ID_floatbv)
583  {
584  ieee_floatt f(to_floatbv_type(type));
585  f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
586  return f.to_expr();
587  }
588  else if(real_type.id()==ID_fixedbv)
589  {
590  fixedbvt f;
591  f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
592  return f.to_expr();
593  }
594  else if(real_type.id()==ID_bool)
595  {
596  if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
597  return true_exprt();
598  else
599  false_exprt();
600  }
601  else if(real_type.id()==ID_c_bool)
602  {
603  return from_integer(
604  rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
605  }
606  else if(real_type.id() == ID_pointer)
607  {
608  if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
609  return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
610 
611  if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
612  {
613  // We want the symbol pointed to
614  mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
615  const symbol_exprt &symbol_expr = address_to_symbol(address);
616  mp_integer offset_from_address = address_to_offset(address);
617 
618  if(offset_from_address == 0)
619  return address_of_exprt(symbol_expr);
620 
621  if(
622  symbol_expr.type().id() == ID_struct ||
623  symbol_expr.type().id() == ID_struct_tag)
624  {
625  const auto c = get_component(symbol_expr.type(), offset_from_address);
626  member_exprt member_expr(symbol_expr, c);
627  return address_of_exprt(member_expr);
628  }
629 
630  return index_exprt(
631  symbol_expr, from_integer(offset_from_address, integer_typet()));
632  }
633 
634  output.error() << "interpreter: invalid pointer "
635  << rhs[numeric_cast_v<std::size_t>(offset)]
636  << " > object count " << memory.size() << messaget::eom;
637 
638  throw "interpreter: reading from invalid pointer";
639  }
640  else if(real_type.id()==ID_string)
641  {
642  // Strings are currently encoded by their irep_idt ID.
643  return constant_exprt(
644  get_string_container().get_string(
645  numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
646  type);
647  }
648 
649  // Retrieve value of basic data type
650  return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
651 }
652 
655 {
656  const code_assignt &code_assign = pc->get_assign();
657 
658  mp_vectort rhs;
659  evaluate(code_assign.rhs(), rhs);
660 
661  if(!rhs.empty())
662  {
663  mp_integer address=evaluate_address(code_assign.lhs());
664  mp_integer size=get_size(code_assign.lhs().type());
665 
666  if(size!=rhs.size())
667  output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
668  << size << ")\n"
669  << messaget::eom;
670  else
671  {
672  goto_trace_stept &trace_step=steps.get_last_step();
673  assign(address, rhs);
674  trace_step.full_lhs=code_assign.lhs();
675  trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
676  }
677  }
678  else if(code_assign.rhs().id()==ID_side_effect)
679  {
680  side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
681  if(side_effect.get_statement()==ID_nondet)
682  {
683  mp_integer address =
684  numeric_cast_v<std::size_t>(evaluate_address(code_assign.lhs()));
685 
686  mp_integer size=
687  get_size(code_assign.lhs().type());
688 
689  for(mp_integer i=0; i<size; ++i)
690  {
691  memory[numeric_cast_v<std::size_t>(address + i)].initialized =
693  }
694  }
695  }
696 }
697 
700  const mp_integer &address,
701  const mp_vectort &rhs)
702 {
703  for(mp_integer i=0; i<rhs.size(); ++i)
704  {
705  if((address+i)<memory.size())
706  {
707  mp_integer address_val=address+i;
708  memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
709  if(show)
710  {
711  output.status() << total_steps << " ** assigning "
712  << address_to_symbol(address_val).get_identifier()
713  << "[" << address_to_offset(address_val)
714  << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
715  << messaget::eom;
716  }
717  cell.value = rhs[numeric_cast_v<std::size_t>(i)];
720  }
721  }
722 }
723 
725 {
726  if(!evaluate_boolean(pc->get_condition()))
727  throw "assumption failed";
728 }
729 
731 {
732  if(!evaluate_boolean(pc->get_condition()))
733  {
734  if(show)
735  output.error() << "assertion failed at " << pc->location_number << "\n"
736  << messaget::eom;
737  }
738 }
739 
741 {
742  const auto &call_lhs = pc->call_lhs();
743  const auto &call_function = pc->call_function();
744  const auto &call_arguments = pc->call_arguments();
745 
746  // function to be called
747  mp_integer address = evaluate_address(call_function);
748 
749  if(address==0)
750  throw "function call to NULL";
751  else if(address>=memory.size())
752  throw "out-of-range function call";
753 
754  // Retrieve the empty last trace step struct we pushed for this step
755  // of the interpreter run to fill it with the corresponding data
756  goto_trace_stept &trace_step=steps.get_last_step();
757 #if 0
758  const memory_cellt &cell=memory[address];
759 #endif
760  const irep_idt &identifier = address_to_symbol(address).get_identifier();
761  trace_step.called_function = identifier;
762 
763  const goto_functionst::function_mapt::const_iterator f_it=
764  goto_functions.function_map.find(identifier);
765 
766  if(f_it==goto_functions.function_map.end())
767  throw "failed to find function "+id2string(identifier);
768 
769  // return value
770  mp_integer return_value_address;
771 
772  if(call_lhs.is_not_nil())
773  return_value_address = evaluate_address(call_lhs);
774  else
775  return_value_address=0;
776 
777  // values of the arguments
778  std::vector<mp_vectort> argument_values;
779 
780  argument_values.resize(call_arguments.size());
781 
782  for(std::size_t i = 0; i < call_arguments.size(); i++)
783  evaluate(call_arguments[i], argument_values[i]);
784 
785  // do the call
786 
787  if(f_it->second.body_available())
788  {
789  call_stack.push(stack_framet());
790  stack_framet &frame=call_stack.top();
791 
792  frame.return_pc=next_pc;
793  frame.return_function=function;
795  frame.return_value_address=return_value_address;
796 
797  // local variables
798  std::set<irep_idt> locals;
799  get_local_identifiers(f_it->second, locals);
800 
801  for(const auto &id : locals)
802  {
803  const symbolt &symbol=ns.lookup(id);
804  frame.local_map[id] = build_memory_map(symbol.symbol_expr());
805  }
806 
807  // assign the arguments
808  const auto &parameter_identifiers = f_it->second.parameter_identifiers;
809  if(argument_values.size() < parameter_identifiers.size())
810  throw "not enough arguments";
811 
812  for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
813  {
814  const symbol_exprt symbol_expr =
815  ns.lookup(parameter_identifiers[i]).symbol_expr();
816  assign(evaluate_address(symbol_expr), argument_values[i]);
817  }
818 
819  // set up new pc
820  function=f_it;
821  next_pc=f_it->second.body.instructions.begin();
822  }
823  else
824  {
825  list_input_varst::iterator it =
826  function_input_vars.find(to_symbol_expr(call_function).get_identifier());
827 
828  if(it!=function_input_vars.end())
829  {
830  mp_vectort value;
831  PRECONDITION(!it->second.empty());
832  PRECONDITION(!it->second.front().return_assignments.empty());
833  evaluate(it->second.front().return_assignments.back().value, value);
834  if(return_value_address>0)
835  {
836  assign(return_value_address, value);
837  }
838  it->second.pop_front();
839  return;
840  }
841 
842  if(show)
843  output.error() << "no body for " << identifier << messaget::eom;
844  }
845 }
846 
849 {
850  // put in a dummy for NULL
851  memory.clear();
852  memory.resize(1);
853  inverse_memory_map[0] = {};
854 
856  dynamic_types.clear();
857 
858  // now do regular static symbols
859  for(const auto &s : symbol_table.symbols)
860  build_memory_map(s.second);
861 
862  // for the locals
864 }
865 
867 {
868  mp_integer size=0;
869 
870  if(symbol.type.id()==ID_code)
871  {
872  size=1;
873  }
874  else if(symbol.is_static_lifetime)
875  {
876  size=get_size(symbol.type);
877  }
878 
879  if(size!=0)
880  {
881  mp_integer address=memory.size();
882  memory.resize(numeric_cast_v<std::size_t>(address + size));
883  memory_map[symbol.name]=address;
884  inverse_memory_map[address] = symbol.symbol_expr();
885  }
886 }
887 
890 {
891  if(type.id()==ID_array)
892  {
893  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
894  mp_vectort computed_size;
895  evaluate(size_expr, computed_size);
896  if(computed_size.size()==1 &&
897  computed_size[0]>=0)
898  {
899  output.result() << "Concretized array with size " << computed_size[0]
900  << messaget::eom;
901  return
902  array_typet(
903  type.subtype(),
904  from_integer(computed_size[0], integer_typet()));
905  }
906  else
907  {
908  output.warning() << "Failed to concretize variable array"
909  << messaget::eom;
910  }
911  }
912  return type;
913 }
914 
918 {
919  typet alloc_type = concretize_type(symbol_expr.type());
920  mp_integer size=get_size(alloc_type);
921  auto it = dynamic_types.find(symbol_expr.get_identifier());
922 
923  if(it!=dynamic_types.end())
924  {
925  mp_integer address = memory_map[symbol_expr.get_identifier()];
926  mp_integer current_size=base_address_to_alloc_size(address);
927  // current size <= size already recorded
928  if(size<=current_size)
929  return memory_map[symbol_expr.get_identifier()];
930  }
931 
932  // The current size is bigger then the one previously recorded
933  // in the memory map
934 
935  if(size==0)
936  size=1; // This is a hack to create existence
937 
938  mp_integer address=memory.size();
939  memory.resize(numeric_cast_v<std::size_t>(address + size));
940  memory_map[symbol_expr.get_identifier()] = address;
941  inverse_memory_map[address] = symbol_expr;
942  dynamic_types.insert(
943  std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
944 
945  return address;
946 }
947 
949 {
950  if(type.id()==ID_array)
951  {
952  const exprt &size=to_array_type(type).size();
953  if(size.id()==ID_infinity)
954  return true;
955  return unbounded_size(type.subtype());
956  }
957  else if(type.id()==ID_struct)
958  {
959  const auto &st=to_struct_type(type);
960  if(st.components().empty())
961  return false;
962  return unbounded_size(st.components().back().type());
963  }
964  return false;
965 }
966 
972 {
973  if(unbounded_size(type))
974  return mp_integer(2) << 32;
975 
976  if(type.id()==ID_struct)
977  {
978  const struct_typet::componentst &components=
979  to_struct_type(type).components();
980 
981  mp_integer sum=0;
982 
983  for(const auto &comp : components)
984  {
985  const typet &sub_type=comp.type();
986 
987  if(sub_type.id()!=ID_code)
988  sum+=get_size(sub_type);
989  }
990 
991  return sum;
992  }
993  else if(type.id()==ID_union)
994  {
995  const union_typet::componentst &components=
996  to_union_type(type).components();
997 
998  mp_integer max_size=0;
999 
1000  for(const auto &comp : components)
1001  {
1002  const typet &sub_type=comp.type();
1003 
1004  if(sub_type.id()!=ID_code)
1005  max_size=std::max(max_size, get_size(sub_type));
1006  }
1007 
1008  return max_size;
1009  }
1010  else if(type.id()==ID_array)
1011  {
1012  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
1013 
1014  mp_integer subtype_size=get_size(type.subtype());
1015 
1016  mp_vectort i;
1017  evaluate(size_expr, i);
1018  if(i.size()==1)
1019  {
1020  // Go via the binary representation to reproduce any
1021  // overflow behaviour.
1022  const constant_exprt size_const = from_integer(i[0], size_expr.type());
1023  const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
1024  return subtype_size*size_mp;
1025  }
1026  return subtype_size;
1027  }
1028  else if(type.id() == ID_struct_tag)
1029  {
1030  return get_size(ns.follow_tag(to_struct_tag_type(type)));
1031  }
1032 
1033  return 1;
1034 }
1035 
1037 {
1038  // The dynamic type and the static symbol type may differ for VLAs,
1039  // where the symbol carries a size expression and the dynamic type
1040  // registry contains its actual length.
1041  auto findit=dynamic_types.find(id);
1042  typet get_type;
1043  if(findit!=dynamic_types.end())
1044  get_type=findit->second;
1045  else
1047 
1048  symbol_exprt symbol_expr(id, get_type);
1049  mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
1050 
1051  return get_value(get_type, whole_lhs_object_address);
1052 }
1053 
1056 void interpretert::print_memory(bool input_flags)
1057 {
1058  for(const auto &cell_address : memory)
1059  {
1060  mp_integer i=cell_address.first;
1061  const memory_cellt &cell=cell_address.second;
1062  const auto identifier = address_to_symbol(i).get_identifier();
1063  const auto offset=address_to_offset(i);
1064  output.status() << identifier << "[" << offset << "]"
1065  << "=" << cell.value << messaget::eom;
1066  if(input_flags)
1067  output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1068  << messaget::eom;
1070  }
1071 }
1072 
1074  const goto_modelt &goto_model,
1075  message_handlert &message_handler)
1076 {
1078  goto_model.symbol_table,
1079  goto_model.goto_functions,
1080  message_handler);
1081  interpreter();
1082 }
interpretert::base_address_to_actual_size
mp_integer base_address_to_actual_size(const mp_integer &address) const
Definition: interpreter_class.h:147
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
interpretert::output
messaget output
Definition: interpreter_class.h:101
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
ieee_floatt
Definition: ieee_float.h:117
interpretert::stack_framet
Definition: interpreter_class.h:248
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:109
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
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition: goto_program.h:43
interpretert::get_component
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.
Definition: interpreter.cpp:427
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
goto_trace_stept::typet::ASSUME
@ ASSUME
interpretert::execute_decl
void execute_decl()
Definition: interpreter.cpp:420
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
stack_depth
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:44
jsont::output
void output(std::ostream &out) const
Definition: json.h:90
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
messaget::status
mstreamt & status() const
Definition: message.h:414
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
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:264
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
interpretert::symbol_table
const symbol_tablet & symbol_table
Definition: interpreter_class.h:102
interpretert::memory
memoryt memory
Definition: interpreter_class.h:190
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:699
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
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:319
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:126
invariant.h
interpretert::evaluate_boolean
bool evaluate_boolean(const exprt &expr)
Definition: interpreter_class.h:276
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:948
goto_model.h
Symbol Table + CFG.
interpreter.h
Interpreter for GOTO Programs.
interpretert::memory_cellt::value
mp_integer value
Definition: interpreter_class.h:169
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
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:264
interpretert::call_stack
call_stackt call_stack
Definition: interpreter_class.h:259
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
interpretert::num_steps
size_t num_steps
Definition: interpreter_class.h:269
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
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:1073
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
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:1056
interpretert::dynamic_types
dynamic_typest dynamic_types
Definition: interpreter_class.h:272
interpretert::total_steps
size_t total_steps
Definition: interpreter_class.h:270
sparse_vectort::clear
void clear()
Definition: sparse_vector.h:54
interpretert::build_memory_map
void build_memory_map()
Creates a memory map of all static symbols in the program.
Definition: interpreter.cpp:848
json_arrayt
Definition: json.h:165
interpretert::base_address_to_alloc_size
mp_integer base_address_to_alloc_size(const mp_integer &address) const
Definition: interpreter_class.h:136
mathematical_types.h
Mathematical types.
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
array_typet::size
const exprt & size() const
Definition: std_types.h:771
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
THROW
@ THROW
Definition: goto_program.h:48
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:138
interpretert::memory_cellt
Definition: interpreter_class.h:163
GOTO
@ GOTO
Definition: goto_program.h:32
interpretert::function
goto_functionst::function_mapt::const_iterator function
Definition: interpreter_class.h:263
interpretert
Definition: interpreter_class.h:29
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:971
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:510
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:460
interpretert::command
virtual void command()
reads a user command and executes it.
Definition: interpreter.cpp:129
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
BUFSIZE
#define BUFSIZE
interpretert::step
void step()
executes a single step and updates the program counter
Definition: interpreter.cpp:234
goto_trace_stept::typet::ASSERT
@ ASSERT
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
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:273
interpretert::memory_cellt::initialized
initializedt initialized
Definition: interpreter_class.h:178
interpretert::stack_framet::old_stack_pointer
mp_integer old_stack_pointer
Definition: interpreter_class.h:254
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
interpretert::execute_function_call
void execute_function_call()
Definition: interpreter.cpp:740
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
interpretert::goto_functions
const goto_functionst & goto_functions
Definition: interpreter_class.h:107
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:56
interpretert::get_type
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
Definition: interpreter.cpp:450
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
OTHER
@ OTHER
Definition: goto_program.h:35
sparse_vectort::resize
void resize(uint64_t new_size)
Definition: sparse_vector.h:48
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:474
interpretert::mp_vectort
std::vector< mp_integer > mp_vectort
Definition: interpreter_class.h:59
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
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:20
interpretert::steps
goto_tracet steps
Definition: interpreter_class.h:265
json_goto_trace.h
Traces of GOTO Programs.
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:40
SKIP
@ SKIP
Definition: goto_program.h:36
interpretert::stack_framet::local_map
memory_mapt local_map
Definition: interpreter_class.h:253
interpretert::concretize_type
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
Definition: interpreter.cpp:889
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:267
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1918
source_locationt
Definition: source_location.h:19
interpretert::execute_assign
void execute_assign()
executes the assign statement at the current pc value
Definition: interpreter.cpp:654
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:27
interpretert::evaluate
void evaluate(const exprt &expr, mp_vectort &dest)
Evaluate an expression.
Definition: interpreter_evaluate.cpp:317
interpretert::ns
const namespacet ns
Definition: interpreter_class.h:105
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
struct_union_typet::componentt
Definition: std_types.h:69
ASSIGN
@ ASSIGN
Definition: goto_program.h:44
goto_trace_stept::typet::GOTO
@ GOTO
can_cast_expr< code_outputt >
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:749
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
CATCH
@ CATCH
Definition: goto_program.h:49
array_typet
Arrays with given size.
Definition: std_types.h:763
interpretert::stack_pointer
mp_integer stack_pointer
Definition: interpreter_class.h:192
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:45
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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:33
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:252
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
interpretert::inverse_memory_map
inverse_memory_mapt inverse_memory_map
Definition: interpreter_class.h:112
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
interpretert::clear_input_flags
void clear_input_flags()
Clears memoy r/w flag initialization.
Definition: interpreter_evaluate.cpp:101
START_THREAD
@ START_THREAD
Definition: goto_program.h:37
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:47
unsafe_string2size_t
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:40
interpretert::input_vars
input_valuest input_vars
Definition: interpreter_class.h:260
interpretert::memory_cellt::initializedt::WRITTEN_BEFORE_READ
@ WRITTEN_BEFORE_READ
fixedbvt
Definition: fixedbv.h:42
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:42
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
interpretert::address_to_offset
mp_integer address_to_offset(const mp_integer &address) const
Definition: interpreter_class.h:131
DEAD
@ DEAD
Definition: goto_program.h:46
interpretert::done
bool done
Definition: interpreter_class.h:266
interpretert::operator()
void operator()()
Definition: interpreter.cpp:37
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:203
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
interpretert::stack_framet::return_function
goto_functionst::function_mapt::const_iterator return_function
Definition: interpreter_class.h:251
index_exprt
Array index operator.
Definition: std_expr.h:1328
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:41
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
symbol_table.h
Author: Diffblue Ltd.
interpretert::call_stackt
std::stack< stack_framet > call_stackt
Definition: interpreter_class.h:257
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
interpretert::function_input_vars
list_input_varst function_input_vars
Definition: interpreter_class.h:261
LOCATION
@ LOCATION
Definition: goto_program.h:39
messaget::warning
mstreamt & warning() const
Definition: message.h:404
ASSERT
@ ASSERT
Definition: goto_program.h:34
std_expr.h
API to expression classes.
interpretert::thread_id
unsigned thread_id
Definition: interpreter_class.h:274
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:1467
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
END_THREAD
@ END_THREAD
Definition: goto_program.h:38
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
interpretert::memory_map
memory_mapt memory_map
Definition: interpreter_class.h:111
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
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:196
interpretert::npos
static const size_t npos
Definition: interpreter_class.h:268
interpretert::execute_assume
void execute_assume()
Definition: interpreter.cpp:724
goto_trace_stept::typet::DEAD
@ DEAD
interpretert::execute_assert
void execute_assert()
Definition: interpreter.cpp:730
interpretert::stack_framet::return_pc
goto_programt::const_targett return_pc
Definition: interpreter_class.h:250
interpretert::evaluate_address
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
Definition: interpreter_evaluate.cpp:1056
get_string_container
string_containert & get_string_container()
Get a reference to the global string container.
Definition: string_container.h:111
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
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:61