cprover
validate_goto_model.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 Module: Validate Goto Programs
3 
4 Author: Diffblue
5 
6 Date: Oct 2018
7 
8 \*******************************************************************/
9 
10 #include "validate_goto_model.h"
11 
12 #include <set>
13 
14 #include <util/invariant.h>
15 #include <util/pointer_expr.h>
16 
17 #include "goto_functions.h"
18 #include "remove_returns.h"
19 
20 namespace
21 {
22 class validate_goto_modelt
23 {
24 public:
25  using function_mapt = goto_functionst::function_mapt;
26 
27  validate_goto_modelt(
28  const goto_functionst &goto_functions,
29  const validation_modet vm,
30  const goto_model_validation_optionst goto_model_validation_options);
31 
32 private:
37  void entry_point_exists();
38 
40  void function_pointer_calls_removed();
41 
52  void check_returns_removed();
53 
63  void check_called_functions();
64 
65  const validation_modet vm;
66  const function_mapt &function_map;
67 };
68 
69 validate_goto_modelt::validate_goto_modelt(
70  const goto_functionst &goto_functions,
71  const validation_modet vm,
72  const goto_model_validation_optionst validation_options)
73  : vm{vm}, function_map{goto_functions.function_map}
74 {
75  if(validation_options.entry_point_exists)
76  entry_point_exists();
77 
80  // 'function_pointer_calls_removed'
81  if(
82  validation_options.function_pointer_calls_removed ||
83  validation_options.check_returns_removed)
84  {
85  function_pointer_calls_removed();
86  }
87 
88  if(validation_options.check_returns_removed)
89  check_returns_removed();
90 
91  if(validation_options.check_called_functions)
92  check_called_functions();
93 }
94 
95 void validate_goto_modelt::entry_point_exists()
96 {
97  DATA_CHECK(
98  vm,
99  function_map.find(goto_functionst::entry_point()) != function_map.end(),
100  "an entry point must exist");
101 }
102 
103 void validate_goto_modelt::function_pointer_calls_removed()
104 {
105  for(const auto &fun : function_map)
106  {
107  for(const auto &instr : fun.second.body.instructions)
108  {
109  if(instr.is_function_call())
110  {
111  const code_function_callt &function_call = instr.get_function_call();
112  DATA_CHECK(
113  vm,
114  function_call.function().id() == ID_symbol,
115  "no calls via function pointer should be present");
116  }
117  }
118  }
119 }
120 
121 void validate_goto_modelt::check_returns_removed()
122 {
123  for(const auto &fun : function_map)
124  {
125  const goto_functiont &goto_function = fun.second;
126 
127  for(const auto &instr : goto_function.body.instructions)
128  {
129  DATA_CHECK(
130  vm, !instr.is_return(), "no return instructions should be present");
131 
132  if(instr.is_function_call())
133  {
134  const auto &function_call = instr.get_function_call();
135  DATA_CHECK(
136  vm,
137  !does_function_call_return(function_call),
138  "function call lhs return should be nil");
139  }
140  }
141  }
142 }
143 
144 void validate_goto_modelt::check_called_functions()
145 {
146  auto test_for_function_address =
147  [this](const exprt &expr) {
148  if(expr.id() == ID_address_of)
149  {
150  const auto &pointee = to_address_of_expr(expr).object();
151 
152  if(pointee.id() == ID_symbol && pointee.type().id() == ID_code)
153  {
154  const auto &identifier = to_symbol_expr(pointee).get_identifier();
155 
156  DATA_CHECK(
157  vm,
158  function_map.find(identifier) != function_map.end(),
159  "every function whose address is taken must be in the "
160  "function map");
161  }
162  }
163  };
164 
165  for(const auto &fun : function_map)
166  {
167  for(const auto &instr : fun.second.body.instructions)
168  {
169  // check functions that are called
170  if(instr.is_function_call())
171  {
172  const auto &function_call = instr.get_function_call();
173  const irep_idt &identifier =
174  to_symbol_expr(function_call.function()).get_identifier();
175 
176  DATA_CHECK(
177  vm,
178  function_map.find(identifier) != function_map.end(),
179  "every function call callee must be in the function map");
180  }
181 
182  // check functions of which the address is taken
183  const auto &src = static_cast<const exprt &>(instr.code);
184  src.visit_pre(test_for_function_address);
185  }
186  }
187 }
188 
189 } // namespace
190 
192  const goto_functionst &goto_functions,
193  const validation_modet vm,
194  const goto_model_validation_optionst validation_options)
195 {
196  validate_goto_modelt{goto_functions, vm, validation_options};
197 }
exprt & object()
Definition: pointer_expr.h:209
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
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:259
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.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_programt body
Definition: goto_function.h:29
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get_identifier() const
Definition: std_expr.h:110
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.
Definition: pointer_expr.h:237
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
Replace function returns by assignments to global variables.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
#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