CBMC
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 {
168 json_steps.output(file);
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 {
189 steps.output(ns, file);
190 file.close();
191 return;
192 }
193 }
195 }
196 else if(ch=='r')
197 {
198 ch=tolower(command[1]);
199 initialize(ch!='0');
200 }
201 else if((ch=='s') || (ch==0))
202 {
203 num_steps=1;
204 std::size_t stack_depth = npos;
205 ch=tolower(command[1]);
206 if(ch=='e')
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 if(object_type.id() != ID_struct_tag)
428 throw "request for member of non-struct";
429
431 ns.follow_tag(to_struct_tag_type(object_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 if(type.id() == ID_struct_tag)
464 {
465 struct_exprt result({}, type);
466 const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
467 const struct_typet::componentst &components=struct_type.components();
468
469 // Retrieve the values for the individual members
470 result.reserve_operands(components.size());
471
472 mp_integer tmp_offset=offset;
473
474 for(const auto &c : components)
475 {
476 mp_integer size=get_size(c.type());
477 const exprt operand=get_value(c.type(), tmp_offset);
478 tmp_offset+=size;
479 result.copy_to_operands(operand);
480 }
481
482 return std::move(result);
483 }
484 else if(type.id() == ID_array)
485 {
486 // Get size of array
487 array_exprt result({}, to_array_type(type));
488 const exprt &size_expr = to_array_type(type).size();
489 mp_integer subtype_size = get_size(to_array_type(type).element_type());
490 mp_integer count;
491 if(!size_expr.is_constant())
492 {
494 }
495 else
496 {
498 }
499
500 // Retrieve the value for each member in the array
501 result.reserve_operands(numeric_cast_v<std::size_t>(count));
502 for(mp_integer i=0; i<count; ++i)
503 {
504 const exprt operand = get_value(
505 to_array_type(type).element_type(), offset + i * subtype_size);
506 result.copy_to_operands(operand);
507 }
508 return std::move(result);
509 }
510 if(
511 use_non_det && memory[numeric_cast_v<std::size_t>(offset)].initialized !=
513 {
515 }
516 mp_vectort rhs;
517 rhs.push_back(memory[numeric_cast_v<std::size_t>(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 PRECONDITION(!rhs.empty());
529
530 if(type.id() == ID_struct_tag)
531 {
532 struct_exprt result({}, type);
533 const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
534 const struct_typet::componentst &components=struct_type.components();
535
536 // Retrieve the values for the individual members
537 result.reserve_operands(components.size());
538 mp_integer tmp_offset=offset;
539
540 for(const struct_union_typet::componentt &expr : components)
541 {
542 mp_integer size=get_size(expr.type());
543 const exprt operand=get_value(expr.type(), rhs, tmp_offset);
544 tmp_offset+=size;
545 result.copy_to_operands(operand);
546 }
547 return std::move(result);
548 }
549 else if(type.id() == ID_array)
550 {
551 array_exprt result({}, to_array_type(type));
552 const exprt &size_expr = to_array_type(type).size();
553
554 // Get size of array
555 mp_integer subtype_size = get_size(to_array_type(type).element_type());
556
557 mp_integer count;
558 if(unbounded_size(type))
559 {
561 }
562 else
563 {
565 }
566
567 // Retrieve the value for each member in the array
568 result.reserve_operands(numeric_cast_v<std::size_t>(count));
569 for(mp_integer i=0; i<count; ++i)
570 {
571 const exprt operand = get_value(
572 to_array_type(type).element_type(), rhs, offset + i * subtype_size);
573 result.copy_to_operands(operand);
574 }
575 return std::move(result);
576 }
577 else if(type.id() == ID_floatbv)
578 {
580 f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
581 return f.to_expr();
582 }
583 else if(type.id() == ID_fixedbv)
584 {
585 fixedbvt f;
587 return f.to_expr();
588 }
589 else if(type.id() == ID_bool)
590 {
591 if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
592 return true_exprt();
593 else
594 false_exprt();
595 }
596 else if(type.id() == ID_c_bool)
597 {
598 return from_integer(
599 rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
600 }
601 else if(type.id() == ID_pointer)
602 {
603 if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
604 return null_pointer_exprt(to_pointer_type(type)); // NULL pointer
605
606 if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
607 {
608 // We want the symbol pointed to
609 mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
610 const symbol_exprt symbol_expr = address_to_symbol(address);
612
613 if(offset_from_address == 0)
614 return address_of_exprt(symbol_expr);
615
616 if(
617 symbol_expr.type().id() == ID_struct ||
618 symbol_expr.type().id() == ID_struct_tag)
619 {
620 const auto c = get_component(symbol_expr.type(), offset_from_address);
621 member_exprt member_expr(symbol_expr, c);
623 }
624
625 return index_exprt(
627 }
628
629 output.error() << "interpreter: invalid pointer "
630 << rhs[numeric_cast_v<std::size_t>(offset)]
631 << " > object count " << memory.size() << messaget::eom;
632
633 throw "interpreter: reading from invalid pointer";
634 }
635 else if(type.id() == ID_string)
636 {
637 // Strings are currently encoded by their irep_idt ID.
638 return constant_exprt(
639 get_string_container().get_string(
641 type);
642 }
643
644 // Retrieve value of basic data type
645 return from_integer(rhs[numeric_cast_v<std::size_t>(offset)], type);
646}
647
650{
651 const exprt &assign_lhs = pc->assign_lhs();
652 const exprt &assign_rhs = pc->assign_rhs();
653
654 mp_vectort rhs = evaluate(assign_rhs);
655
656 if(!rhs.empty())
657 {
658 mp_integer address = evaluate_address(assign_lhs);
659 mp_integer size = get_size(assign_lhs.type());
660
661 if(size!=rhs.size())
662 output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
663 << size << ")\n"
664 << messaget::eom;
665 else
666 {
668 assign(address, rhs);
669 trace_step.full_lhs = assign_lhs;
670 trace_step.full_lhs_value=get_value(trace_step.full_lhs.type(), rhs);
671 }
672 }
673 else if(assign_rhs.id() == ID_side_effect)
674 {
676 if(side_effect.get_statement()==ID_nondet)
677 {
678 mp_integer address =
680
681 mp_integer size = get_size(assign_lhs.type());
682
683 for(mp_integer i=0; i<size; ++i)
684 {
685 memory[numeric_cast_v<std::size_t>(address + i)].initialized =
687 }
688 }
689 }
690}
691
694 const mp_integer &address,
695 const mp_vectort &rhs)
696{
697 for(mp_integer i=0; i<rhs.size(); ++i)
698 {
699 if((address+i)<memory.size())
700 {
701 mp_integer address_val=address+i;
703 if(show)
704 {
705 output.status() << total_steps << " ** assigning "
708 << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
709 << messaget::eom;
710 }
711 cell.value = rhs[numeric_cast_v<std::size_t>(i)];
714 }
715 }
716}
717
719{
720 if(!evaluate_boolean(pc->condition()))
721 throw "assumption failed";
722}
723
725{
726 if(!evaluate_boolean(pc->condition()))
727 {
728 if(show)
729 output.error() << "assertion failed at " << pc->location_number << "\n"
730 << messaget::eom;
731 }
732}
733
735{
736 const auto &call_lhs = pc->call_lhs();
737 const auto &call_function = pc->call_function();
738 const auto &call_arguments = pc->call_arguments();
739
740 // function to be called
741 mp_integer address = evaluate_address(call_function);
742
743 if(address==0)
744 throw "function call to NULL";
745 else if(address>=memory.size())
746 throw "out-of-range function call";
747
748 // Retrieve the empty last trace step struct we pushed for this step
749 // of the interpreter run to fill it with the corresponding data
751#if 0
752 const memory_cellt &cell=memory[address];
753#endif
754 const irep_idt identifier = address_to_symbol(address).get_identifier();
755 trace_step.called_function = identifier;
756
757 const goto_functionst::function_mapt::const_iterator f_it=
758 goto_functions.function_map.find(identifier);
759
760 if(f_it==goto_functions.function_map.end())
761 throw "failed to find function "+id2string(identifier);
762
763 // return value
764 mp_integer return_value_address;
765
766 if(call_lhs.is_not_nil())
767 return_value_address = evaluate_address(call_lhs);
768 else
769 return_value_address=0;
770
771 // values of the arguments
772 std::vector<mp_vectort> argument_values;
773
774 argument_values.resize(call_arguments.size());
775
776 for(std::size_t i = 0; i < call_arguments.size(); i++)
777 argument_values[i] = evaluate(call_arguments[i]);
778
779 // do the call
780
781 if(f_it->second.body_available())
782 {
783 call_stack.push(stack_framet());
784 stack_framet &frame=call_stack.top();
785
786 frame.return_pc=next_pc;
789 frame.return_value_address=return_value_address;
790
791 // local variables
792 std::set<irep_idt> locals;
793 get_local_identifiers(f_it->second, locals);
794
795 for(const auto &id : locals)
796 {
797 const symbolt &symbol=ns.lookup(id);
798 frame.local_map[id] = build_memory_map(symbol.symbol_expr());
799 }
800
801 // assign the arguments
802 const auto &parameter_identifiers = f_it->second.parameter_identifiers;
803 if(argument_values.size() < parameter_identifiers.size())
804 throw "not enough arguments";
805
806 for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
807 {
808 const symbol_exprt symbol_expr =
809 ns.lookup(parameter_identifiers[i]).symbol_expr();
810 assign(evaluate_address(symbol_expr), argument_values[i]);
811 }
812
813 // set up new pc
815 next_pc=f_it->second.body.instructions.begin();
816 }
817 else
818 {
819 list_input_varst::iterator it =
820 function_input_vars.find(to_symbol_expr(call_function).get_identifier());
821
822 if(it!=function_input_vars.end())
823 {
824 PRECONDITION(!it->second.empty());
825 PRECONDITION(!it->second.front().return_assignments.empty());
826 mp_vectort value =
827 evaluate(it->second.front().return_assignments.back().value);
828 if(return_value_address>0)
829 {
830 assign(return_value_address, value);
831 }
832 it->second.pop_front();
833 return;
834 }
835
836 if(show)
837 output.error() << "no body for " << identifier << messaget::eom;
838 }
839}
840
843{
844 // put in a dummy for NULL
845 memory.clear();
846 memory.resize(1);
847 inverse_memory_map[0] = {};
848
851
852 // now do regular static symbols
853 for(const auto &s : symbol_table.symbols)
854 build_memory_map(s.second);
855
856 // for the locals
858}
859
861{
862 mp_integer size=0;
863
864 if(symbol.type.id()==ID_code)
865 {
866 size=1;
867 }
868 else if(symbol.is_static_lifetime)
869 {
870 size=get_size(symbol.type);
871 }
872
873 if(size!=0)
874 {
875 mp_integer address=memory.size();
877 memory_map[symbol.name]=address;
878 inverse_memory_map[address] = symbol.symbol_expr();
879 }
880}
881
884{
885 if(type.id()==ID_array)
886 {
887 const exprt &size_expr = to_array_type(type).size();
889 if(computed_size.size()==1 &&
890 computed_size[0]>=0)
891 {
892 output.result() << "Concretized array with size " << computed_size[0]
893 << messaget::eom;
894 return array_typet(
895 to_array_type(type).element_type(),
897 }
898 else
899 {
900 output.warning() << "Failed to concretize variable array"
901 << messaget::eom;
902 }
903 }
904 return type;
905}
906
910{
911 typet alloc_type = concretize_type(symbol_expr.type());
913 auto it = dynamic_types.find(symbol_expr.get_identifier());
914
915 if(it!=dynamic_types.end())
916 {
917 mp_integer address = memory_map[symbol_expr.get_identifier()];
919 // current size <= size already recorded
920 if(size<=current_size)
921 return memory_map[symbol_expr.get_identifier()];
922 }
923
924 // The current size is bigger then the one previously recorded
925 // in the memory map
926
927 if(size==0)
928 size=1; // This is a hack to create existence
929
930 mp_integer address=memory.size();
932 memory_map[symbol_expr.get_identifier()] = address;
933 inverse_memory_map[address] = symbol_expr;
934 dynamic_types.insert(
935 std::pair<const irep_idt, typet>(symbol_expr.get_identifier(), alloc_type));
936
937 return address;
938}
939
941{
942 if(type.id()==ID_array)
943 {
944 const exprt &size=to_array_type(type).size();
945 if(size.id()==ID_infinity)
946 return true;
947 return unbounded_size(to_array_type(type).element_type());
948 }
949 else if(type.id()==ID_struct)
950 {
951 const auto &st=to_struct_type(type);
952 if(st.components().empty())
953 return false;
954 return unbounded_size(st.components().back().type());
955 }
956 return false;
957}
958
964{
965 if(unbounded_size(type))
966 return mp_integer(2) << (sizeof(std::size_t) * CHAR_BIT / 2);
967
968 if(type.id()==ID_struct)
969 {
970 const struct_typet::componentst &components=
971 to_struct_type(type).components();
972
973 mp_integer sum=0;
974
975 for(const auto &comp : components)
976 {
978 comp.type().id() != ID_code, "struct member must not be of code type");
979 sum += get_size(comp.type());
980 }
981
982 return sum;
983 }
984 else if(type.id()==ID_union)
985 {
986 const union_typet::componentst &components=
987 to_union_type(type).components();
988
990
991 for(const auto &comp : components)
992 {
994 comp.type().id() != ID_code, "union member must not be of code type");
995 max_size = std::max(max_size, get_size(comp.type()));
996 }
997
998 return max_size;
999 }
1000 else if(type.id()==ID_array)
1001 {
1002 const exprt &size_expr = to_array_type(type).size();
1003
1004 mp_integer subtype_size = get_size(to_array_type(type).element_type());
1005
1007 if(i.size()==1)
1008 {
1009 // Go via the binary representation to reproduce any
1010 // overflow behaviour.
1011 const constant_exprt size_const = from_integer(i[0], size_expr.type());
1013 return subtype_size*size_mp;
1014 }
1015 return subtype_size;
1016 }
1017 else if(type.id() == ID_struct_tag)
1018 {
1019 return get_size(ns.follow_tag(to_struct_tag_type(type)));
1020 }
1021
1022 return 1;
1023}
1024
1026{
1027 // The dynamic type and the static symbol type may differ for VLAs,
1028 // where the symbol carries a size expression and the dynamic type
1029 // registry contains its actual length.
1030 auto findit=dynamic_types.find(id);
1032 if(findit!=dynamic_types.end())
1033 get_type=findit->second;
1034 else
1035 get_type=symbol_table.lookup_ref(id).type;
1036
1037 symbol_exprt symbol_expr(id, get_type);
1039
1041}
1042
1046{
1047 for(const auto &cell_address : memory)
1048 {
1049 mp_integer i=cell_address.first;
1050 const memory_cellt &cell=cell_address.second;
1051 const auto identifier = address_to_symbol(i).get_identifier();
1052 const auto offset=address_to_offset(i);
1053 output.status() << identifier << "[" << offset << "]"
1054 << "=" << cell.value << messaget::eom;
1055 if(input_flags)
1056 output.status() << "(" << static_cast<int>(cell.initialized) << ")"
1057 << messaget::eom;
1059 }
1060}
1061
1063 const goto_modelt &goto_model,
1064 message_handlert &message_handler)
1065{
1067 goto_model.symbol_table,
1068 goto_model.goto_functions,
1069 message_handler);
1070 interpreter();
1071}
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
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
A constant literal expression.
Definition std_expr.h:3118
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:3200
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
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
constant_exprt to_expr() const
void unpack(const mp_integer &)
Array index operator.
Definition std_expr.h:1470
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 irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2972
mstreamt & error() const
Definition message.h:391
mstreamt & warning() const
Definition message.h:396
mstreamt & result() const
Definition message.h:401
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
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:1877
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:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
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:3191
The type of an expression, extends irept.
Definition type.h:29
int tolower(int c)
Definition ctype.c:109
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:44
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:17
#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:3173
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
char * fgets(char *str, int size, FILE *stream)
Definition stdio.c:321
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.