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#include "interpreter_class.h"
14
15#include <util/c_types.h>
16#include <util/fixedbv.h>
17#include <util/ieee_float.h>
18#include <util/invariant.h>
20#include <util/message.h>
21#include <util/pointer_expr.h>
22#include <util/std_code.h>
23#include <util/std_expr.h>
24#include <util/string2int.h>
26
27#include "goto_model.h"
28#include "json_goto_trace.h"
29
30#include <algorithm>
31#include <cctype>
32#include <climits>
33#include <cstdio>
34#include <fstream>
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();
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 pc->output(output.status());
124
126}
127
130{
131 #define BUFSIZE 100
132 char command[BUFSIZE];
133 if(fgets(command, BUFSIZE-1, stdin)==nullptr)
134 {
135 done=true;
136 return;
137 }
138
139 char ch=tolower(command[0]);
140 if(ch=='q')
141 done=true;
142 else if(ch=='h')
143 {
144 output.status() << "Interpreter help\n"
145 << "h: display this menu\n"
146 << "j: output json trace\n"
147 << "m: output memory dump\n"
148 << "o: output goto trace\n"
149 << "q: quit\n"
150 << "r: run up to entry point\n"
151 << "s#: step a number of instructions\n"
152 << "sa: step across a function\n"
153 << "so: step out of a function\n"
154 << "se: step until end of program\n"
155 << messaget::eom;
156 }
157 else if(ch=='j')
158 {
161 ch=tolower(command[1]);
162 if(ch==' ')
163 {
164 std::ofstream file;
165 file.open(command+2);
166 if(file.is_open())
167 {
169 file.close();
170 return;
171 }
172 }
174 }
175 else if(ch=='m')
176 {
177 ch=tolower(command[1]);
178 print_memory(ch=='i');
179 }
180 else if(ch=='o')
181 {
182 ch=tolower(command[1]);
183 if(ch==' ')
184 {
185 std::ofstream file;
186 file.open(command+2);
187 if(file.is_open())
188 {
190 file.close();
191 return;
192 }
193 }
195 }
196 else if(ch=='r')
197 {
198 ch=tolower(command[1]);
199 initialize(ch!='0');
200 }
201 else if((ch=='s') || (ch==0))
202 {
203 num_steps=1;
204 std::size_t stack_depth = npos;
205 ch=tolower(command[1]);
206 if(ch=='e')
208 else if(ch=='o')
209 stack_depth=call_stack.size();
210 else if(ch=='a')
211 stack_depth=call_stack.size()+1;
212 else
213 {
215 if(num_steps==0)
216 num_steps=1;
217 }
218 while(!done && ((num_steps==npos) || ((num_steps--)>0)))
219 {
220 step();
221 show_state();
222 }
223 while(!done && (stack_depth<=call_stack.size()) && (stack_depth!=npos))
224 {
225 step();
226 show_state();
227 }
228 return;
229 }
230 show_state();
231}
232
235{
236 total_steps++;
237 if(pc==function->second.body.instructions.end())
238 {
239 if(call_stack.empty())
240 done=true;
241 else
242 {
243 pc=call_stack.top().return_pc;
244 function=call_stack.top().return_function;
245 // TODO: this increases memory size quite quickly.
246 // Should check alternatives
247 call_stack.pop();
248 }
249
250 return;
251 }
252
253 next_pc=pc;
254 next_pc++;
255
258 trace_step.thread_nr=thread_id;
259 trace_step.pc=pc;
260 switch(pc->type())
261 {
262 case GOTO:
264 execute_goto();
265 break;
266
267 case ASSUME:
270 break;
271
272 case ASSERT:
275 break;
276
277 case OTHER:
279 break;
280
281 case DECL:
283 execute_decl();
284 break;
285
286 case SKIP:
287 case LOCATION:
289 break;
290 case END_FUNCTION:
292 break;
293
294 case SET_RETURN_VALUE:
296 if(call_stack.empty())
297 throw "SET_RETURN_VALUE without call"; // NOLINT(readability/throw)
298
299 if(call_stack.top().return_value_address != 0)
300 {
301 mp_vectort rhs = evaluate(pc->return_value());
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:
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 case INCOMPLETE_GOTO:
363 throw "encountered instruction with undefined instruction type";
364 }
365 pc=next_pc;
366}
367
370{
371 if(evaluate_boolean(pc->condition()))
372 {
373 if(pc->targets.empty())
374 throw "taken goto without target";
375
376 if(pc->targets.size()>=2)
377 throw "non-deterministic goto encountered";
378
379 next_pc=pc->targets.front();
380 }
381}
382
385{
386 const irep_idt &statement = pc->get_other().get_statement();
387 if(statement==ID_expression)
388 {
390 pc->code().operands().size() == 1,
391 "expression statement expected to have one operand");
392 mp_vectort rhs = evaluate(pc->code().op0());
393 }
394 else if(statement==ID_array_set)
395 {
396 mp_vectort tmp = evaluate(pc->code().op1());
397 mp_integer address = evaluate_address(pc->code().op0());
398 mp_integer size = get_size(pc->code().op0().type());
399 mp_vectort rhs;
400 while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
401 if(size!=rhs.size())
402 output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
403 << size << ")\n"
404 << messaget::eom;
405 else
406 {
407 assign(address, rhs);
408 }
409 }
410 else if(can_cast_expr<code_outputt>(pc->get_other()))
411 {
412 return;
413 }
414 else
415 throw "unexpected OTHER statement: "+id2string(statement);
416}
417
419{
420 PRECONDITION(pc->code().get_statement() == ID_decl);
421}
422
425interpretert::get_component(const typet &object_type, const mp_integer &offset)
426{
427 const typet real_type = ns.follow(object_type);
428 if(real_type.id()!=ID_struct)
429 throw "request for member of non-struct";
430
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);
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 std::move(result);
484 }
485 else if(real_type.id()==ID_array)
486 {
487 // Get size of array
489 const exprt &size_expr = to_array_type(type).size();
490 mp_integer subtype_size = get_size(to_array_type(type).element_type());
491 mp_integer count;
492 if(!size_expr.is_constant())
493 {
495 }
496 else
497 {
499 }
500
501 // Retrieve the value for each member in the array
502 result.reserve_operands(numeric_cast_v<std::size_t>(count));
503 for(mp_integer i=0; i<count; ++i)
504 {
505 const exprt operand = get_value(
506 to_array_type(type).element_type(), offset + i * subtype_size);
507 result.copy_to_operands(operand);
508 }
509 return std::move(result);
510 }
511 if(
512 use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
514 {
516 }
517 mp_vectort rhs;
518 rhs.push_back(memory[numeric_cast_v<std::size_t>(offset)].value);
519 return get_value(type, rhs);
520}
521
525 const typet &type,
526 mp_vectort &rhs,
527 const mp_integer &offset)
528{
529 const typet real_type=ns.follow(type);
530 PRECONDITION(!rhs.empty());
531
532 if(real_type.id()==ID_struct)
533 {
534 struct_exprt result({}, real_type);
536 const struct_typet::componentst &components=struct_type.components();
537
538 // Retrieve the values for the individual members
539 result.reserve_operands(components.size());
540 mp_integer tmp_offset=offset;
541
542 for(const struct_union_typet::componentt &expr : components)
543 {
544 mp_integer size=get_size(expr.type());
545 const exprt operand=get_value(expr.type(), rhs, tmp_offset);
546 tmp_offset+=size;
547 result.copy_to_operands(operand);
548 }
549 return std::move(result);
550 }
551 else if(real_type.id()==ID_array)
552 {
554 const exprt &size_expr = to_array_type(real_type).size();
555
556 // Get size of array
557 mp_integer subtype_size = get_size(to_array_type(type).element_type());
558
559 mp_integer count;
560 if(unbounded_size(type))
561 {
563 }
564 else
565 {
567 }
568
569 // Retrieve the value for each member in the array
570 result.reserve_operands(numeric_cast_v<std::size_t>(count));
571 for(mp_integer i=0; i<count; ++i)
572 {
573 const exprt operand = get_value(
574 to_array_type(type).element_type(), rhs, offset + i * subtype_size);
575 result.copy_to_operands(operand);
576 }
577 return std::move(result);
578 }
579 else if(real_type.id()==ID_floatbv)
580 {
582 f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
583 return f.to_expr();
584 }
585 else if(real_type.id()==ID_fixedbv)
586 {
587 fixedbvt f;
589 return f.to_expr();
590 }
591 else if(real_type.id()==ID_bool)
592 {
593 if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
594 return true_exprt();
595 else
596 false_exprt();
597 }
598 else if(real_type.id()==ID_c_bool)
599 {
600 return from_integer(
601 rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
602 }
603 else if(real_type.id() == ID_pointer)
604 {
605 if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
606 return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
607
608 if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
609 {
610 // We want the symbol pointed to
611 mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
612 const symbol_exprt &symbol_expr = address_to_symbol(address);
614
615 if(offset_from_address == 0)
616 return address_of_exprt(symbol_expr);
617
618 if(
619 symbol_expr.type().id() == ID_struct ||
620 symbol_expr.type().id() == ID_struct_tag)
621 {
622 const auto c = get_component(symbol_expr.type(), offset_from_address);
623 member_exprt member_expr(symbol_expr, c);
625 }
626
627 return index_exprt(
629 }
630
631 output.error() << "interpreter: invalid pointer "
632 << rhs[numeric_cast_v<std::size_t>(offset)]
633 << " > object count " << memory.size() << messaget::eom;
634
635 throw "interpreter: reading from invalid pointer";
636 }
637 else if(real_type.id()==ID_string)
638 {
639 // Strings are currently encoded by their irep_idt ID.
640 return constant_exprt(
641 get_string_container().get_string(
643 type);
644 }
645
646 // Retrieve value of basic data type
647 return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
648}
649
652{
653 const exprt &assign_lhs = pc->assign_lhs();
654 const exprt &assign_rhs = pc->assign_rhs();
655
656 mp_vectort rhs = evaluate(assign_rhs);
657
658 if(!rhs.empty())
659 {
660 mp_integer address = evaluate_address(assign_lhs);
661 mp_integer size = get_size(assign_lhs.type());
662
663 if(size!=rhs.size())
664 output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
665 << size << ")\n"
666 << messaget::eom;
667 else
668 {
670 assign(address, rhs);
671 trace_step.full_lhs = assign_lhs;
672 trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
673 }
674 }
675 else if(assign_rhs.id() == ID_side_effect)
676 {
678 if(side_effect.get_statement()==ID_nondet)
679 {
680 mp_integer address =
682
683 mp_integer size = get_size(assign_lhs.type());
684
685 for(mp_integer i=0; i<size; ++i)
686 {
687 memory[numeric_cast_v<std::size_t>(address + i)].initialized =
689 }
690 }
691 }
692}
693
696 const mp_integer &address,
697 const mp_vectort &rhs)
698{
699 for(mp_integer i=0; i<rhs.size(); ++i)
700 {
701 if((address+i)<memory.size())
702 {
703 mp_integer address_val=address+i;
705 if(show)
706 {
707 output.status() << total_steps << " ** assigning "
710 << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
711 << messaget::eom;
712 }
713 cell.value = rhs[numeric_cast_v<std::size_t>(i)];
716 }
717 }
718}
719
721{
722 if(!evaluate_boolean(pc->condition()))
723 throw "assumption failed";
724}
725
727{
728 if(!evaluate_boolean(pc->condition()))
729 {
730 if(show)
731 output.error() << "assertion failed at " << pc->location_number << "\n"
732 << messaget::eom;
733 }
734}
735
737{
738 const auto &call_lhs = pc->call_lhs();
739 const auto &call_function = pc->call_function();
740 const auto &call_arguments = pc->call_arguments();
741
742 // function to be called
743 mp_integer address = evaluate_address(call_function);
744
745 if(address==0)
746 throw "function call to NULL";
747 else if(address>=memory.size())
748 throw "out-of-range function call";
749
750 // Retrieve the empty last trace step struct we pushed for this step
751 // of the interpreter run to fill it with the corresponding data
753#if 0
754 const memory_cellt &cell=memory[address];
755#endif
756 const irep_idt &identifier = address_to_symbol(address).get_identifier();
757 trace_step.called_function = identifier;
758
759 const goto_functionst::function_mapt::const_iterator f_it=
760 goto_functions.function_map.find(identifier);
761
762 if(f_it==goto_functions.function_map.end())
763 throw "failed to find function "+id2string(identifier);
764
765 // return value
766 mp_integer return_value_address;
767
768 if(call_lhs.is_not_nil())
769 return_value_address = evaluate_address(call_lhs);
770 else
771 return_value_address=0;
772
773 // values of the arguments
774 std::vector<mp_vectort> argument_values;
775
776 argument_values.resize(call_arguments.size());
777
778 for(std::size_t i = 0; i < call_arguments.size(); i++)
779 argument_values[i] = evaluate(call_arguments[i]);
780
781 // do the call
782
783 if(f_it->second.body_available())
784 {
785 call_stack.push(stack_framet());
786 stack_framet &frame=call_stack.top();
787
788 frame.return_pc=next_pc;
791 frame.return_value_address=return_value_address;
792
793 // local variables
794 std::set<irep_idt> locals;
795 get_local_identifiers(f_it->second, locals);
796
797 for(const auto &id : locals)
798 {
799 const symbolt &symbol=ns.lookup(id);
800 frame.local_map[id] = build_memory_map(symbol.symbol_expr());
801 }
802
803 // assign the arguments
804 const auto &parameter_identifiers = f_it->second.parameter_identifiers;
805 if(argument_values.size() < parameter_identifiers.size())
806 throw "not enough arguments";
807
808 for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
809 {
810 const symbol_exprt symbol_expr =
811 ns.lookup(parameter_identifiers[i]).symbol_expr();
812 assign(evaluate_address(symbol_expr), argument_values[i]);
813 }
814
815 // set up new pc
817 next_pc=f_it->second.body.instructions.begin();
818 }
819 else
820 {
821 list_input_varst::iterator it =
822 function_input_vars.find(to_symbol_expr(call_function).get_identifier());
823
824 if(it!=function_input_vars.end())
825 {
826 PRECONDITION(!it->second.empty());
827 PRECONDITION(!it->second.front().return_assignments.empty());
828 mp_vectort value =
829 evaluate(it->second.front().return_assignments.back().value);
830 if(return_value_address>0)
831 {
832 assign(return_value_address, value);
833 }
834 it->second.pop_front();
835 return;
836 }
837
838 if(show)
839 output.error() << "no body for " << identifier << messaget::eom;
840 }
841}
842
845{
846 // put in a dummy for NULL
847 memory.clear();
848 memory.resize(1);
849 inverse_memory_map[0] = {};
850
852 dynamic_types.clear();
853
854 // now do regular static symbols
855 for(const auto &s : symbol_table.symbols)
856 build_memory_map(s.second);
857
858 // for the locals
860}
861
863{
864 mp_integer size=0;
865
866 if(symbol.type.id()==ID_code)
867 {
868 size=1;
869 }
870 else if(symbol.is_static_lifetime)
871 {
872 size=get_size(symbol.type);
873 }
874
875 if(size!=0)
876 {
877 mp_integer address=memory.size();
879 memory_map[symbol.name]=address;
880 inverse_memory_map[address] = symbol.symbol_expr();
881 }
882}
883
886{
887 if(type.id()==ID_array)
888 {
889 const exprt &size_expr = to_array_type(type).size();
891 if(computed_size.size()==1 &&
892 computed_size[0]>=0)
893 {
894 output.result() << "Concretized array with size " << computed_size[0]
895 << messaget::eom;
896 return array_typet(
897 to_array_type(type).element_type(),
899 }
900 else
901 {
902 output.warning() << "Failed to concretize variable array"
903 << messaget::eom;
904 }
905 }
906 return type;
907}
908
912{
913 typet alloc_type = concretize_type(symbol_expr.type());
915 auto it = dynamic_types.find(symbol_expr.get_identifier());
916
917 if(it!=dynamic_types.end())
918 {
919 mp_integer address = memory_map[symbol_expr.get_identifier()];
921 // current size <= size already recorded
922 if(size<=current_size)
923 return memory_map[symbol_expr.get_identifier()];
924 }
925
926 // The current size is bigger then the one previously recorded
927 // in the memory map
928
929 if(size==0)
930 size=1; // This is a hack to create existence
931
932 mp_integer address=memory.size();
934 memory_map[symbol_expr.get_identifier()] = address;
935 inverse_memory_map[address] = symbol_expr;
936 dynamic_types.insert(
937 std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
938
939 return address;
940}
941
943{
944 if(type.id()==ID_array)
945 {
946 const exprt &size=to_array_type(type).size();
947 if(size.id()==ID_infinity)
948 return true;
949 return unbounded_size(to_array_type(type).element_type());
950 }
951 else if(type.id()==ID_struct)
952 {
953 const auto &st=to_struct_type(type);
954 if(st.components().empty())
955 return false;
956 return unbounded_size(st.components().back().type());
957 }
958 return false;
959}
960
966{
967 if(unbounded_size(type))
968 return mp_integer(2) << (sizeof(std::size_t) * CHAR_BIT / 2);
969
970 if(type.id()==ID_struct)
971 {
972 const struct_typet::componentst &components=
973 to_struct_type(type).components();
974
975 mp_integer sum=0;
976
977 for(const auto &comp : components)
978 {
980 comp.type().id() != ID_code, "struct member must not be of code type");
981 sum += get_size(comp.type());
982 }
983
984 return sum;
985 }
986 else if(type.id()==ID_union)
987 {
988 const union_typet::componentst &components=
989 to_union_type(type).components();
990
992
993 for(const auto &comp : components)
994 {
996 comp.type().id() != ID_code, "union member must not be of code type");
997 max_size = std::max(max_size, get_size(comp.type()));
998 }
999
1000 return max_size;
1001 }
1002 else if(type.id()==ID_array)
1003 {
1004 const exprt &size_expr = to_array_type(type).size();
1005
1006 mp_integer subtype_size = get_size(to_array_type(type).element_type());
1007
1009 if(i.size()==1)
1010 {
1011 // Go via the binary representation to reproduce any
1012 // overflow behaviour.
1013 const constant_exprt size_const = from_integer(i[0], size_expr.type());
1015 return subtype_size*size_mp;
1016 }
1017 return subtype_size;
1018 }
1019 else if(type.id() == ID_struct_tag)
1020 {
1021 return get_size(ns.follow_tag(to_struct_tag_type(type)));
1022 }
1023
1024 return 1;
1025}
1026
1028{
1029 // The dynamic type and the static symbol type may differ for VLAs,
1030 // where the symbol carries a size expression and the dynamic type
1031 // registry contains its actual length.
1032 auto findit=dynamic_types.find(id);
1034 if(findit!=dynamic_types.end())
1035 get_type=findit->second;
1036 else
1037 get_type=symbol_table.lookup_ref(id).type;
1038
1039 symbol_exprt symbol_expr(id, get_type);
1041
1043}
1044
1048{
1049 for(const auto &cell_address : memory)
1050 {
1051 mp_integer i=cell_address.first;
1052 const memory_cellt &cell=cell_address.second;
1053 const auto identifier = address_to_symbol(i).get_identifier();
1054 const auto offset=address_to_offset(i);
1055 output.status() << identifier << "[" << offset << "]"
1056 << "=" << cell.value << messaget::eom;
1057 if(input_flags)
1058 output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1059 << messaget::eom;
1061 }
1062}
1063
1065 const goto_modelt &goto_model,
1066 message_handlert &message_handler)
1067{
1069 goto_model.symbol_table,
1070 goto_model.goto_functions,
1071 message_handler);
1072 interpreter();
1073}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
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:184
Operator to return the address of an object.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Array constructor from list of elements.
Definition std_expr.h:1563
Arrays with given size.
Definition std_types.h:763
A constant literal expression.
Definition std_expr.h:2942
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
void from_integer(const mp_integer &i)
Definition fixedbv.cpp:32
constant_exprt to_expr() const
Definition fixedbv.cpp:43
::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:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
Step of the trace of a GOTO program.
Definition goto_trace.h:50
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition goto_trace.h:198
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
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:205
void unpack(const mp_integer &i)
constant_exprt to_expr() const
Array index operator.
Definition std_expr.h:1410
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()()
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
const symbol_table_baset & symbol_table
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.
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...
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
Extract member of struct or union.
Definition std_expr.h:2794
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
The null pointer constant.
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
void resize(uint64_t new_size)
uint64_t size() const
Struct constructor from list of elements.
Definition std_expr.h:1819
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:70
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:3008
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...
Symbol Table + CFG.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
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.
BigInt mp_integer
Definition smt_terms.h:18
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#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)
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:2992
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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:844
std::size_t unsafe_string2size_t(const std::string &str, int base)
Container for C-Strings.
string_containert & get_string_container()
Get a reference to the global string container.
Definition kdev_t.h:19