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