cprover
Loading...
Searching...
No Matches
validate_goto_model.cpp
Go to the documentation of this file.
1/*******************************************************************\
2Module: Validate Goto Programs
3
4Author: Diffblue
5
6Date: Oct 2018
7
8\*******************************************************************/
9
10#include "validate_goto_model.h"
11
12#include <set>
13
14#include <util/pointer_expr.h>
15
16#include "goto_functions.h"
17
18namespace
19{
20class validate_goto_modelt
21{
22public:
23 using function_mapt = goto_functionst::function_mapt;
24
25 validate_goto_modelt(
26 const goto_functionst &goto_functions,
27 const validation_modet vm,
28 const goto_model_validation_optionst goto_model_validation_options);
29
30private:
35 void entry_point_exists();
36
38 void function_pointer_calls_removed();
39
49 void check_called_functions();
50
51 const validation_modet vm;
52 const function_mapt &function_map;
53};
54
55validate_goto_modelt::validate_goto_modelt(
56 const goto_functionst &goto_functions,
57 const validation_modet vm,
58 const goto_model_validation_optionst validation_options)
59 : vm{vm}, function_map{goto_functions.function_map}
60{
61 if(validation_options.entry_point_exists)
62 entry_point_exists();
63
64 if(validation_options.function_pointer_calls_removed)
65 {
66 function_pointer_calls_removed();
67 }
68
69 if(validation_options.check_called_functions)
70 check_called_functions();
71}
72
73void validate_goto_modelt::entry_point_exists()
74{
76 vm,
77 function_map.find(goto_functionst::entry_point()) != function_map.end(),
78 "an entry point must exist");
79}
80
81void validate_goto_modelt::function_pointer_calls_removed()
82{
83 for(const auto &fun : function_map)
84 {
85 for(const auto &instr : fun.second.body.instructions)
86 {
87 if(instr.is_function_call())
88 {
90 vm,
91 instr.call_function().id() == ID_symbol,
92 "no calls via function pointer should be present");
93 }
94 }
95 }
96}
97
98void validate_goto_modelt::check_called_functions()
99{
100 auto test_for_function_address =
101 [this](const exprt &expr) {
102 if(expr.id() == ID_address_of)
103 {
104 const auto &pointee = to_address_of_expr(expr).object();
105
106 if(pointee.id() == ID_symbol && pointee.type().id() == ID_code)
107 {
108 const auto &identifier = to_symbol_expr(pointee).get_identifier();
109
111 vm,
112 function_map.find(identifier) != function_map.end(),
113 "every function whose address is taken must be in the "
114 "function map");
115 }
116 }
117 };
118
119 for(const auto &fun : function_map)
120 {
121 for(const auto &instr : fun.second.body.instructions)
122 {
123 // check functions that are called
124 if(instr.is_function_call())
125 {
126 const irep_idt &identifier =
127 to_symbol_expr(instr.call_function()).get_identifier();
128
130 vm,
131 function_map.find(identifier) != function_map.end(),
132 "every function call callee must be in the function map");
133 }
134
135 // check functions of which the address is taken
136 const auto &src = static_cast<const exprt &>(instr.get_code());
137 src.visit_pre(test_for_function_address);
138 }
139 }
140}
141
142} // namespace
143
145 const goto_functionst &goto_functions,
146 const validation_modet vm,
147 const goto_model_validation_optionst validation_options)
148{
149 validate_goto_modelt{goto_functions, vm, validation_options};
150}
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
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:245
A collection of goto functions.
std::map< irep_idt, goto_functiont > function_mapt
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
const irep_idt & get_identifier() const
Definition std_expr.h:109
Goto Programs with Functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
validation_modet