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/invariant.h>
22 #include <util/std_types.h>
23 #include <util/string_container.h>
24 #include <util/symbol_table.h>
25 #include <util/ieee_float.h>
26 #include <util/fixedbv.h>
27 #include <util/std_expr.h>
28 #include <util/message.h>
29 #include <json/json_parser.h>
30 
31 #include "interpreter_class.h"
32 #include "json_goto_trace.h"
33 #include "remove_returns.h"
34 
35 const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
36 
38 {
39  status() << "0- Initialize:" << eom;
40  initialize(true);
41  try
42  {
43  status() << "Type h for help\n" << eom;
44 
45  while(!done)
46  command();
47 
48  status() << total_steps << "- Program End.\n" << eom;
49  }
50  catch (const char *e)
51  {
52  error() << e << "\n" << eom;
53  }
54 
55  while(!done)
56  command();
57 }
58 
61 void interpretert::initialize(bool init)
62 {
64 
65  total_steps=0;
66  const goto_functionst::function_mapt::const_iterator
68 
69  if(main_it==goto_functions.function_map.end())
70  throw "main not found";
71 
72  const goto_functionst::goto_functiont &goto_function=main_it->second;
73 
74  if(!goto_function.body_available())
75  throw "main has no body";
76 
77  pc=goto_function.body.instructions.begin();
78  function=main_it;
79 
80  done=false;
81  if(init)
82  {
83  stack_depth=call_stack.size()+1;
84  show_state();
85  step();
86  while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
87  {
88  show_state();
89  step();
90  }
91  while(!done && (call_stack.size()==0))
92  {
93  show_state();
94  step();
95  }
97  input_vars.clear();
98  }
99 }
100 
103 {
104  if(!show)
105  return;
106  status() << "\n"
107  << total_steps+1
108  << " ----------------------------------------------------\n";
109 
110  if(pc==function->second.body.instructions.end())
111  {
112  status() << "End of function `" << function->first << "'\n";
113  }
114  else
115  function->second.body.output_instruction(
116  ns,
117  function->first,
118  status(),
119  *pc);
120 
121  status() << eom;
122 }
123 
126 {
127  #define BUFSIZE 100
128  char command[BUFSIZE];
129  if(fgets(command, BUFSIZE-1, stdin)==nullptr)
130  {
131  done=true;
132  return;
133  }
134 
135  char ch=tolower(command[0]);
136  if(ch=='q')
137  done=true;
138  else if(ch=='h')
139  {
140  status()
141  << "Interpreter help\n"
142  << "h: display this menu\n"
143  << "j: output json trace\n"
144  << "m: output memory dump\n"
145  << "o: output goto trace\n"
146  << "q: quit\n"
147  << "r: run until completion\n"
148  << "s#: step a number of instructions\n"
149  << "sa: step across a function\n"
150  << "so: step out of a function\n"
151  << eom;
152  }
153  else if(ch=='j')
154  {
155  json_arrayt json_steps;
156  convert<json_arrayt>(ns, steps, json_steps);
157  ch=tolower(command[1]);
158  if(ch==' ')
159  {
160  std::ofstream file;
161  file.open(command+2);
162  if(file.is_open())
163  {
164  json_steps.output(file);
165  file.close();
166  return;
167  }
168  }
169  json_steps.output(result());
170  }
171  else if(ch=='m')
172  {
173  ch=tolower(command[1]);
174  print_memory(ch=='i');
175  }
176  else if(ch=='o')
177  {
178  ch=tolower(command[1]);
179  if(ch==' ')
180  {
181  std::ofstream file;
182  file.open(command+2);
183  if(file.is_open())
184  {
185  steps.output(ns, file);
186  file.close();
187  return;
188  }
189  }
190  steps.output(ns, result());
191  }
192  else if(ch=='r')
193  {
194  ch=tolower(command[1]);
195  initialize(ch!='0');
196  }
197  else if((ch=='s') || (ch==0))
198  {
199  num_steps=1;
201  ch=tolower(command[1]);
202  if(ch=='e')
203  num_steps=npos;
204  else if(ch=='o')
205  stack_depth=call_stack.size();
206  else if(ch=='a')
207  stack_depth=call_stack.size()+1;
208  else
209  {
210  num_steps=atoi(command+1);
211  if(num_steps==0)
212  num_steps=1;
213  }
214  while(!done && ((num_steps==npos) || ((num_steps--)>0)))
215  {
216  step();
217  show_state();
218  }
219  while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
220  {
221  step();
222  show_state();
223  }
224  return;
225  }
226  show_state();
227 }
228 
231 {
232  total_steps++;
233  if(pc==function->second.body.instructions.end())
234  {
235  if(call_stack.empty())
236  done=true;
237  else
238  {
239  pc=call_stack.top().return_pc;
240  function=call_stack.top().return_function;
241  // TODO: this increases memory size quite quickly.
242  // Should check alternatives
243  call_stack.pop();
244  }
245 
246  return;
247  }
248 
249  next_pc=pc;
250  next_pc++;
251 
253  goto_trace_stept &trace_step=steps.get_last_step();
254  trace_step.thread_nr=thread_id;
255  trace_step.pc=pc;
256  switch(pc->type)
257  {
258  case GOTO:
260  execute_goto();
261  break;
262 
263  case ASSUME:
265  execute_assume();
266  break;
267 
268  case ASSERT:
270  execute_assert();
271  break;
272 
273  case OTHER:
274  execute_other();
275  break;
276 
277  case DECL:
279  execute_decl();
280  break;
281 
282  case SKIP:
283  case LOCATION:
285  break;
286  case END_FUNCTION:
288  break;
289 
290  case RETURN:
292  if(call_stack.empty())
293  throw "RETURN without call"; // NOLINT(readability/throw)
294 
295  if(pc->code.operands().size()==1 &&
296  call_stack.top().return_value_address!=0)
297  {
298  mp_vectort rhs;
299  evaluate(pc->code.op0(), rhs);
300  assign(call_stack.top().return_value_address, rhs);
301  }
302 
303  next_pc=function->second.body.instructions.end();
304  break;
305 
306  case ASSIGN:
308  execute_assign();
309  break;
310 
311  case FUNCTION_CALL:
314  break;
315 
316  case START_THREAD:
318  throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
319 
320  case END_THREAD:
321  throw "END_THREAD not yet implemented"; // NOLINT(readability/throw)
322  break;
323 
324  case ATOMIC_BEGIN:
326  throw "ATOMIC_BEGIN not yet implemented"; // NOLINT(readability/throw)
327 
328  case ATOMIC_END:
330  throw "ATOMIC_END not yet implemented"; // NOLINT(readability/throw)
331 
332  case DEAD:
334  break;
335  case THROW:
337  while(!done && (pc->type!=CATCH))
338  {
339  if(pc==function->second.body.instructions.end())
340  {
341  if(call_stack.empty())
342  done=true;
343  else
344  {
345  pc=call_stack.top().return_pc;
346  function=call_stack.top().return_function;
347  call_stack.pop();
348  }
349  }
350  else
351  {
352  next_pc=pc;
353  next_pc++;
354  }
355  }
356  break;
357  case CATCH:
358  break;
359  default:
360  throw "encountered instruction with undefined instruction type";
361  }
362  pc=next_pc;
363 }
364 
367 {
368  if(evaluate_boolean(pc->guard))
369  {
370  if(pc->targets.empty())
371  throw "taken goto without target";
372 
373  if(pc->targets.size()>=2)
374  throw "non-deterministic goto encountered";
375 
376  next_pc=pc->targets.front();
377  }
378 }
379 
382 {
383  const irep_idt &statement=pc->code.get_statement();
384  if(statement==ID_expression)
385  {
387  pc->code.operands().size()==1,
388  "expression statement expected to have one operand");
389  mp_vectort rhs;
390  evaluate(pc->code.op0(), rhs);
391  }
392  else if(statement==ID_array_set)
393  {
394  mp_vectort tmp, rhs;
395  evaluate(pc->code.op1(), tmp);
396  mp_integer address=evaluate_address(pc->code.op0());
397  mp_integer size=get_size(pc->code.op0().type());
398  while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
399  if(size!=rhs.size())
400  error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
401  << size << ")\n" << eom;
402  else
403  {
404  assign(address, rhs);
405  }
406  }
407  else if(statement==ID_output)
408  {
409  return;
410  }
411  else
412  throw "unexpected OTHER statement: "+id2string(statement);
413 }
414 
416 {
417  PRECONDITION(pc->code.get_statement()==ID_decl);
418 }
419 
423  const irep_idt &object,
424  const mp_integer &offset)
425 {
426  const symbolt &symbol=ns.lookup(object);
427  const typet real_type=ns.follow(symbol.type);
428  if(real_type.id()!=ID_struct)
429  throw "request for member of non-struct";
430 
431  const struct_typet &struct_type=to_struct_type(real_type);
432  const struct_typet::componentst &components=struct_type.components();
433 
434  mp_integer tmp_offset=offset;
435 
436  for(const auto &c : components)
437  {
438  if(tmp_offset<=0)
439  return c;
440 
441  tmp_offset-=get_size(c.type());
442  }
443 
444  throw "access out of struct bounds";
445 }
446 
449 {
450  dynamic_typest::const_iterator it=dynamic_types.find(id);
451  if(it==dynamic_types.end())
452  return symbol_table.lookup_ref(id).type;
453  return it->second;
454 }
455 
459  const typet &type,
460  const mp_integer &offset,
461  bool use_non_det)
462 {
463  const typet real_type=ns.follow(type);
464  if(real_type.id()==ID_struct)
465  {
466  struct_exprt result(real_type);
467  const struct_typet &struct_type=to_struct_type(real_type);
468  const struct_typet::componentst &components=struct_type.components();
469 
470  // Retrieve the values for the individual members
471  result.reserve_operands(components.size());
472 
473  mp_integer tmp_offset=offset;
474 
475  for(const auto &c : components)
476  {
477  mp_integer size=get_size(c.type());
478  const exprt operand=get_value(c.type(), tmp_offset);
479  tmp_offset+=size;
480  result.copy_to_operands(operand);
481  }
482 
483  return result;
484  }
485  else if(real_type.id()==ID_array)
486  {
487  // Get size of array
488  array_exprt result(to_array_type(real_type));
489  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
490  mp_integer subtype_size=get_size(type.subtype());
491  mp_integer count;
492  if(size_expr.id()!=ID_constant)
493  {
494  count=base_address_to_actual_size(offset)/subtype_size;
495  }
496  else
497  {
498  to_integer(size_expr, count);
499  }
500 
501  // Retrieve the value for each member in the array
502  result.reserve_operands(integer2size_t(count));
503  for(mp_integer i=0; i<count; ++i)
504  {
505  const exprt operand=get_value(
506  type.subtype(),
507  offset+i*subtype_size);
508  result.copy_to_operands(operand);
509  }
510  return result;
511  }
512  if(use_non_det &&
513  memory[integer2ulong(offset)].initialized!=
515  return side_effect_expr_nondett(type);
516  mp_vectort rhs;
517  rhs.push_back(memory[integer2ulong(offset)].value);
518  return get_value(type, rhs);
519 }
520 
524  const typet &type,
525  mp_vectort &rhs,
526  const mp_integer &offset)
527 {
528  const typet real_type=ns.follow(type);
529  PRECONDITION(!rhs.empty());
530 
531  if(real_type.id()==ID_struct)
532  {
533  struct_exprt result(real_type);
534  const struct_typet &struct_type=to_struct_type(real_type);
535  const struct_typet::componentst &components=struct_type.components();
536 
537  // Retrieve the values for the individual members
538  result.reserve_operands(components.size());
539  mp_integer tmp_offset=offset;
540 
541  for(const struct_union_typet::componentt &expr : components)
542  {
543  mp_integer size=get_size(expr.type());
544  const exprt operand=get_value(expr.type(), rhs, tmp_offset);
545  tmp_offset+=size;
546  result.copy_to_operands(operand);
547  }
548  return result;
549  }
550  else if(real_type.id()==ID_array)
551  {
552  constant_exprt result(type);
553  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
554 
555  // Get size of array
556  mp_integer subtype_size=get_size(type.subtype());
557 
558  mp_integer count;
559  if(unbounded_size(type))
560  {
561  count=base_address_to_actual_size(offset)/subtype_size;
562  }
563  else
564  {
565  to_integer(size_expr, count);
566  }
567 
568  // Retrieve the value for each member in the array
569  result.reserve_operands(integer2size_t(count));
570  for(mp_integer i=0; i<count; ++i)
571  {
572  const exprt operand=get_value(type.subtype(), rhs,
573  offset+i*subtype_size);
574  result.copy_to_operands(operand);
575  }
576  return result;
577  }
578  else if(real_type.id()==ID_floatbv)
579  {
580  ieee_floatt f(to_floatbv_type(type));
581  f.unpack(rhs[integer2size_t(offset)]);
582  return f.to_expr();
583  }
584  else if(real_type.id()==ID_fixedbv)
585  {
586  fixedbvt f;
587  f.from_integer(rhs[integer2size_t(offset)]);
588  return f.to_expr();
589  }
590  else if(real_type.id()==ID_bool)
591  {
592  if(rhs[integer2size_t(offset)]!=0)
593  return true_exprt();
594  else
595  false_exprt();
596  }
597  else if(real_type.id()==ID_c_bool)
598  {
599  return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
600  }
601  else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of))
602  {
603  if(rhs[integer2size_t(offset)]==0)
604  {
605  // NULL pointer
606  constant_exprt result(type);
607  result.set_value(ID_NULL);
608  return result;
609  }
610 
611  if(rhs[integer2size_t(offset)]<memory.size())
612  {
613  // We want the symbol pointed to
614  mp_integer address=rhs[integer2size_t(offset)];
615  irep_idt identifier=address_to_identifier(address);
616  mp_integer offset=address_to_offset(address);
617  const typet type=get_type(identifier);
618  const symbol_exprt symbol_expr(identifier, type);
619 
620  if(offset==0)
621  return address_of_exprt(symbol_expr);
622 
623  if(ns.follow(type).id()==ID_struct)
624  {
625  const auto c=get_component(identifier, offset);
626  member_exprt member_expr(symbol_expr, c);
627  return address_of_exprt(member_expr);
628  }
629 
630  index_exprt index_expr(
631  symbol_expr,
632  from_integer(offset, integer_typet()));
633 
634  return index_expr;
635  }
636 
637  error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
638  << " > object count " << memory.size() << eom;
639 
640  throw "interpreter: reading from invalid pointer";
641  }
642  else if(real_type.id()==ID_string)
643  {
644  // Strings are currently encoded by their irep_idt ID.
645  return constant_exprt(
646  get_string_container().get_string(rhs[integer2size_t(offset)].to_long()),
647  type);
648  }
649 
650  // Retrieve value of basic data type
651  return from_integer(rhs[integer2ulong(offset)], type);
652 }
653 
656 {
657  const code_assignt &code_assign=
658  to_code_assign(pc->code);
659 
660  mp_vectort rhs;
661  evaluate(code_assign.rhs(), rhs);
662 
663  if(!rhs.empty())
664  {
665  mp_integer address=evaluate_address(code_assign.lhs());
666  mp_integer size=get_size(code_assign.lhs().type());
667 
668  if(size!=rhs.size())
669  error() << "!! failed to obtain rhs ("
670  << rhs.size() << " vs. "
671  << size << ")\n"
672  << eom;
673  else
674  {
675  goto_trace_stept &trace_step=steps.get_last_step();
676  assign(address, rhs);
677  trace_step.full_lhs=code_assign.lhs();
678 
679  // TODO: need to look at other cases on ssa_exprt
680  // (dereference should be handled on ssa)
682  {
683  trace_step.lhs_object=ssa_exprt(trace_step.full_lhs);
684  }
685  trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
686  trace_step.lhs_object_value=trace_step.full_lhs_value;
687  }
688  }
689  else if(code_assign.rhs().id()==ID_side_effect)
690  {
691  side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
692  if(side_effect.get_statement()==ID_nondet)
693  {
694  mp_integer address=
695  integer2size_t(evaluate_address(code_assign.lhs()));
696 
697  mp_integer size=
698  get_size(code_assign.lhs().type());
699 
700  for(mp_integer i=0; i<size; ++i)
701  {
702  memory[integer2ulong(address+i)].initialized=
704  }
705  }
706  }
707 }
708 
711  const mp_integer &address,
712  const mp_vectort &rhs)
713 {
714  for(mp_integer i=0; i<rhs.size(); ++i)
715  {
716  if((address+i)<memory.size())
717  {
718  mp_integer address_val=address+i;
719  memory_cellt &cell=memory[integer2ulong(address_val)];
720  if(show)
721  {
722  status() << total_steps << " ** assigning "
723  << address_to_identifier(address_val) << "["
724  << address_to_offset(address_val) << "]:="
725  << rhs[integer2size_t(i)]
726  << "\n" << eom;
727  }
728  cell.value=rhs[integer2size_t(i)];
731  }
732  }
733 }
734 
736 {
737  if(!evaluate_boolean(pc->guard))
738  throw "assumption failed";
739 }
740 
742 {
743  if(!evaluate_boolean(pc->guard))
744  {
746  throw "program assertion reached";
747  else if(show)
748  error() << "assertion failed at " << pc->location_number
749  << "\n" << eom;
750  }
751 }
752 
754 {
755  const code_function_callt &function_call=
756  to_code_function_call(pc->code);
757 
758  // function to be called
759  mp_integer address=evaluate_address(function_call.function());
760 
761  if(address==0)
762  throw "function call to NULL";
763  else if(address>=memory.size())
764  throw "out-of-range function call";
765 
766  // Retrieve the empty last trace step struct we pushed for this step
767  // of the interpreter run to fill it with the corresponding data
768  goto_trace_stept &trace_step=steps.get_last_step();
769 #if 0
770  const memory_cellt &cell=memory[address];
771 #endif
772  const irep_idt &identifier=address_to_identifier(address);
773  trace_step.identifier=identifier;
774 
775  const goto_functionst::function_mapt::const_iterator f_it=
776  goto_functions.function_map.find(identifier);
777 
778  if(f_it==goto_functions.function_map.end())
779  throw "failed to find function "+id2string(identifier);
780 
781  // return value
782  mp_integer return_value_address;
783 
784  if(function_call.lhs().is_not_nil())
785  return_value_address=
786  evaluate_address(function_call.lhs());
787  else
788  return_value_address=0;
789 
790  // values of the arguments
791  std::vector<mp_vectort> argument_values;
792 
793  argument_values.resize(function_call.arguments().size());
794 
795  for(std::size_t i=0; i<function_call.arguments().size(); i++)
796  evaluate(function_call.arguments()[i], argument_values[i]);
797 
798  // do the call
799 
800  if(f_it->second.body_available())
801  {
802  call_stack.push(stack_framet());
803  stack_framet &frame=call_stack.top();
804 
805  frame.return_pc=next_pc;
806  frame.return_function=function;
808  frame.return_value_address=return_value_address;
809 
810  // local variables
811  std::set<irep_idt> locals;
812  get_local_identifiers(f_it->second, locals);
813 
814  for(const auto &id : locals)
815  {
816  const symbolt &symbol=ns.lookup(id);
817  frame.local_map[id]=build_memory_map(id, symbol.type);
818  }
819 
820  // assign the arguments
821  const code_typet::parameterst &parameters=
822  to_code_type(f_it->second.type).parameters();
823 
824  if(argument_values.size()<parameters.size())
825  throw "not enough arguments";
826 
827  for(std::size_t i=0; i<parameters.size(); i++)
828  {
829  const code_typet::parametert &a=parameters[i];
830  const symbol_exprt symbol_expr(a.get_identifier(), a.type());
831  assign(evaluate_address(symbol_expr), argument_values[i]);
832  }
833 
834  // set up new pc
835  function=f_it;
836  next_pc=f_it->second.body.instructions.begin();
837  }
838  else
839  {
840  list_input_varst::iterator it = function_input_vars.find(
841  to_symbol_expr(function_call.function()).get_identifier());
842 
843  if(it!=function_input_vars.end())
844  {
845  mp_vectort value;
846  PRECONDITION(!it->second.empty());
847  PRECONDITION(!it->second.front().return_assignments.empty());
848  evaluate(it->second.front().return_assignments.back().value, value);
849  if(return_value_address>0)
850  {
851  assign(return_value_address, value);
852  }
853  it->second.pop_front();
854  return;
855  }
856 
857  if(show)
858  error() << "no body for "+id2string(identifier) << eom;
859  }
860 }
861 
864 {
865  // put in a dummy for NULL
866  memory.resize(1);
867  inverse_memory_map[0] = ID_null_object;
868 
870  dynamic_types.clear();
871 
872  // now do regular static symbols
873  for(const auto &s : symbol_table.symbols)
874  build_memory_map(s.second);
875 
876  // for the locals
878 }
879 
881 {
882  mp_integer size=0;
883 
884  if(symbol.type.id()==ID_code)
885  {
886  size=1;
887  }
888  else if(symbol.is_static_lifetime)
889  {
890  size=get_size(symbol.type);
891  }
892 
893  if(size!=0)
894  {
895  mp_integer address=memory.size();
896  memory.resize(integer2ulong(address+size));
897  memory_map[symbol.name]=address;
898  inverse_memory_map[address]=symbol.name;
899  }
900 }
901 
904 {
905  if(type.id()==ID_array)
906  {
907  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
908  mp_vectort computed_size;
909  evaluate(size_expr, computed_size);
910  if(computed_size.size()==1 &&
911  computed_size[0]>=0)
912  {
913  result() << "Concretized array with size " << computed_size[0]
914  << eom;
915  return
916  array_typet(
917  type.subtype(),
918  from_integer(computed_size[0], integer_typet()));
919  }
920  else
921  {
922  warning() << "Failed to concretize variable array" << eom;
923  }
924  }
925  return type;
926 }
927 
931  const irep_idt &id,
932  const typet &type)
933 {
934  typet alloc_type=concretize_type(type);
935  mp_integer size=get_size(alloc_type);
936  auto it=dynamic_types.find(id);
937 
938  if(it!=dynamic_types.end())
939  {
940  mp_integer address=memory_map[id];
941  mp_integer current_size=base_address_to_alloc_size(address);
942  // current size <= size already recorded
943  if(size<=current_size)
944  return memory_map[id];
945  }
946 
947  // The current size is bigger then the one previously recorded
948  // in the memory map
949 
950  if(size==0)
951  size=1; // This is a hack to create existence
952 
953  mp_integer address=memory.size();
954  memory.resize(integer2ulong(address+size));
955  memory_map[id]=address;
956  inverse_memory_map[address]=id;
957  dynamic_types.insert(std::pair<const irep_idt, typet>(id, alloc_type));
958 
959  return address;
960 }
961 
963 {
964  if(type.id()==ID_array)
965  {
966  const exprt &size=to_array_type(type).size();
967  if(size.id()==ID_infinity)
968  return true;
969  return unbounded_size(type.subtype());
970  }
971  else if(type.id()==ID_struct)
972  {
973  const auto &st=to_struct_type(type);
974  if(st.components().empty())
975  return false;
976  return unbounded_size(st.components().back().type());
977  }
978  return false;
979 }
980 
986 {
987  if(unbounded_size(type))
988  return mp_integer(2) << 32;
989 
990  if(type.id()==ID_struct)
991  {
992  const struct_typet::componentst &components=
993  to_struct_type(type).components();
994 
995  mp_integer sum=0;
996 
997  for(const auto &comp : components)
998  {
999  const typet &sub_type=comp.type();
1000 
1001  if(sub_type.id()!=ID_code)
1002  sum+=get_size(sub_type);
1003  }
1004 
1005  return sum;
1006  }
1007  else if(type.id()==ID_union)
1008  {
1009  const union_typet::componentst &components=
1010  to_union_type(type).components();
1011 
1012  mp_integer max_size=0;
1013 
1014  for(const auto &comp : components)
1015  {
1016  const typet &sub_type=comp.type();
1017 
1018  if(sub_type.id()!=ID_code)
1019  max_size=std::max(max_size, get_size(sub_type));
1020  }
1021 
1022  return max_size;
1023  }
1024  else if(type.id()==ID_array)
1025  {
1026  const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
1027 
1028  mp_integer subtype_size=get_size(type.subtype());
1029 
1030  mp_vectort i;
1031  evaluate(size_expr, i);
1032  if(i.size()==1)
1033  {
1034  // Go via the binary representation to reproduce any
1035  // overflow behaviour.
1036  exprt size_const=from_integer(i[0], size_expr.type());
1037  mp_integer size_mp;
1038  bool ret=to_integer(size_const, size_mp);
1039  CHECK_RETURN(!ret);
1040  return subtype_size*size_mp;
1041  }
1042  return subtype_size;
1043  }
1044  else if(type.id()==ID_symbol)
1045  {
1046  return get_size(ns.follow(type));
1047  }
1048  return 1;
1049 }
1050 
1052 {
1053  // The dynamic type and the static symbol type may differ for VLAs,
1054  // where the symbol carries a size expression and the dynamic type
1055  // registry contains its actual length.
1056  auto findit=dynamic_types.find(id);
1057  typet get_type;
1058  if(findit!=dynamic_types.end())
1059  get_type=findit->second;
1060  else
1062 
1063  symbol_exprt symbol_expr(id, get_type);
1064  mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
1065 
1066  return get_value(get_type, whole_lhs_object_address);
1067 }
1068 
1071 void interpretert::print_memory(bool input_flags)
1072 {
1073  for(const auto &cell_address : memory)
1074  {
1075  mp_integer i=cell_address.first;
1076  const memory_cellt &cell=cell_address.second;
1077  const auto identifier=address_to_identifier(i);
1078  const auto offset=address_to_offset(i);
1079  debug() << identifier << "[" << offset << "]"
1080  << "=" << cell.value << eom;
1081  if(input_flags)
1082  debug() << "(" << static_cast<int>(cell.initialized) << ")"
1083  << eom;
1084  debug() << eom;
1085  }
1086 }
1087 
1089  const goto_modelt &goto_model,
1091 {
1093  goto_model.symbol_table,
1094  goto_model.goto_functions,
1095  message_handler);
1096  interpreter();
1097 }
1098 
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:43
bool is_not_nil() const
Definition: irep.h:103
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:987
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::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:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
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:1287
Extract member of struct or union.
Definition: std_expr.h:3871
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:239
const irep_idt & id() const
Definition: irep.h:189
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
exprt & lhs()
Definition: std_code.h:208
Interpreter for GOTO Programs.
The boolean constant true.
Definition: std_expr.h:4488
argumentst & arguments()
Definition: std_code.h:860
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:213
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:61
void operator()()
Definition: interpreter.cpp:37
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:230
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
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:1014
mp_integer base_address_to_actual_size(const mp_integer &address) const
A function call.
Definition: std_code.h:828
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
Author: Diffblue Ltd.
goto_tracet steps
Operator to return the address of an object.
Definition: std_expr.h:3170
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:4499
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:1373
mstreamt & status() const
Definition: message.h:317
exprt & function()
Definition: std_code.h:848
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
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:1004
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:257
An expression containing a side effect.
Definition: std_code.h:1238
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:130
Assignment.
Definition: std_code.h:195
list_input_varst function_input_vars
const irep_idt & get_statement() const
Definition: std_code.h:1253
void execute_function_call()
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
array index operator
Definition: std_expr.h:1462
Definition: kdev_t.h:19