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