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 
16 #include "goto_functions.h"
17 #include "remove_returns.h"
18 
19 namespace
20 {
21 class validate_goto_modelt
22 {
23 public:
24  using function_mapt = goto_functionst::function_mapt;
25 
26  validate_goto_modelt(
27  const goto_functionst &goto_functions,
28  const validation_modet vm,
29  const goto_model_validation_optionst goto_model_validation_options);
30 
31 private:
36  void entry_point_exists();
37 
39  void function_pointer_calls_removed();
40 
51  void check_returns_removed();
52 
62  void check_called_functions();
63 
64  const validation_modet vm;
65  const function_mapt &function_map;
66 };
67 
68 validate_goto_modelt::validate_goto_modelt(
69  const goto_functionst &goto_functions,
70  const validation_modet vm,
71  const goto_model_validation_optionst validation_options)
72  : vm{vm}, function_map{goto_functions.function_map}
73 {
74  if(validation_options.entry_point_exists)
75  entry_point_exists();
76 
79  // 'function_pointer_calls_removed'
80  if(
81  validation_options.function_pointer_calls_removed ||
82  validation_options.check_returns_removed)
83  {
84  function_pointer_calls_removed();
85  }
86 
87  if(validation_options.check_returns_removed)
88  check_returns_removed();
89 
90  if(validation_options.check_called_functions)
91  check_called_functions();
92 }
93 
94 void validate_goto_modelt::entry_point_exists()
95 {
96  DATA_CHECK(
97  vm,
98  function_map.find(goto_functionst::entry_point()) != function_map.end(),
99  "an entry point must exist");
100 }
101 
102 void validate_goto_modelt::function_pointer_calls_removed()
103 {
104  for(const auto &fun : function_map)
105  {
106  for(const auto &instr : fun.second.body.instructions)
107  {
108  if(instr.is_function_call())
109  {
110  const code_function_callt &function_call = instr.get_function_call();
111  DATA_CHECK(
112  vm,
113  function_call.function().id() == ID_symbol,
114  "no calls via function pointer should be present");
115  }
116  }
117  }
118 }
119 
120 void validate_goto_modelt::check_returns_removed()
121 {
122  for(const auto &fun : function_map)
123  {
124  const goto_functiont &goto_function = fun.second;
125 
126  for(const auto &instr : goto_function.body.instructions)
127  {
128  DATA_CHECK(
129  vm, !instr.is_return(), "no return instructions should be present");
130 
131  if(instr.is_function_call())
132  {
133  const auto &function_call = instr.get_function_call();
134  DATA_CHECK(
135  vm,
136  !does_function_call_return(function_call),
137  "function call lhs return should be nil");
138  }
139  }
140  }
141 }
142 
143 void validate_goto_modelt::check_called_functions()
144 {
145  auto test_for_function_address =
146  [this](const exprt &expr) {
147  if(expr.id() == ID_address_of)
148  {
149  const auto &pointee = to_address_of_expr(expr).object();
150 
151  if(pointee.id() == ID_symbol && pointee.type().id() == ID_code)
152  {
153  const auto &identifier = to_symbol_expr(pointee).get_identifier();
154 
155  DATA_CHECK(
156  vm,
157  function_map.find(identifier) != function_map.end(),
158  "every function whose address is taken must be in the "
159  "function map");
160  }
161  }
162  };
163 
164  for(const auto &fun : function_map)
165  {
166  for(const auto &instr : fun.second.body.instructions)
167  {
168  // check functions that are called
169  if(instr.is_function_call())
170  {
171  const auto &function_call = instr.get_function_call();
172  const irep_idt &identifier =
173  to_symbol_expr(function_call.function()).get_identifier();
174 
175  DATA_CHECK(
176  vm,
177  function_map.find(identifier) != function_map.end(),
178  "every function call callee must be in the function map");
179  }
180 
181  // check functions of which the address is taken
182  const auto &src = static_cast<const exprt &>(instr.code);
183  src.visit_pre(test_for_function_address);
184  }
185  }
186 }
187 
188 } // namespace
189 
191  const goto_functionst &goto_functions,
192  const validation_modet vm,
193  const goto_model_validation_optionst validation_options)
194 {
195  validate_goto_modelt{goto_functions, vm, validation_options};
196 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
invariant.h
goto_model_validation_optionst
Definition: validate_goto_model.h:16
exprt
Base class for all expressions.
Definition: expr.h:53
validate_goto_model.h
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
goto_functionst::function_mapt
std::map< irep_idt, goto_functiont > function_mapt
Definition: goto_functions.h:26
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
does_function_call_return
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
Definition: remove_returns.cpp:432
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
remove_returns.h
Replace function returns by assignments to global variables.
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:311
validate_goto_model
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
Definition: validate_goto_model.cpp:190
goto_functions.h
Goto Programs with Functions.
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
code_function_callt::function
exprt & function()
Definition: std_code.h:1218