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/pointer_expr.h>
15 
16 #include "goto_functions.h"
17 
18 namespace
19 {
20 class validate_goto_modelt
21 {
22 public:
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 
30 private:
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 
55 validate_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 
73 void validate_goto_modelt::entry_point_exists()
74 {
75  DATA_CHECK(
76  vm,
77  function_map.find(goto_functionst::entry_point()) != function_map.end(),
78  "an entry point must exist");
79 }
80 
81 void 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  {
89  DATA_CHECK(
90  vm,
91  instr.call_function().id() == ID_symbol,
92  "no calls via function pointer should be present");
93  }
94  }
95  }
96 }
97 
98 void 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 
110  DATA_CHECK(
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 
129  DATA_CHECK(
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 }
exprt & object()
Definition: pointer_expr.h:370
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.
Definition: pointer_expr.h:398
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