cprover
goto_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_functions.h"
15 
16 #include <algorithm>
17 
19 {
21  for(auto &func : function_map)
22  {
23  // Side-effect: bumps unused_location_number.
24  func.second.body.compute_location_numbers(unused_location_number);
25  }
26 }
27 
29  goto_programt &program)
30 {
31  // Renumber just this single function. Use fresh numbers in case it has
32  // grown since it was last numbered.
34 }
35 
37 {
38  for(auto &func : function_map)
39  {
40  func.second.body.compute_incoming_edges();
41  }
42 }
43 
45 {
46  for(auto &func : function_map)
47  {
48  func.second.body.compute_target_numbers();
49  }
50 }
51 
53 {
54  for(auto &func : function_map)
55  {
56  func.second.body.compute_loop_numbers();
57  }
58 }
59 
61 std::vector<goto_functionst::function_mapt::const_iterator>
63 {
64  std::vector<function_mapt::const_iterator> result;
65 
66  result.reserve(function_map.size());
67 
68  for(auto it = function_map.begin(); it != function_map.end(); it++)
69  result.push_back(it);
70 
71  std::sort(
72  result.begin(),
73  result.end(),
74  [](function_mapt::const_iterator a, function_mapt::const_iterator b) {
75  return id2string(a->first) < id2string(b->first);
76  });
77 
78  return result;
79 }
80 
82 std::vector<goto_functionst::function_mapt::iterator> goto_functionst::sorted()
83 {
84  std::vector<function_mapt::iterator> result;
85 
86  result.reserve(function_map.size());
87 
88  for(auto it = function_map.begin(); it != function_map.end(); it++)
89  result.push_back(it);
90 
91  std::sort(
92  result.begin(),
93  result.end(),
94  [](function_mapt::iterator a, function_mapt::iterator b) {
95  return id2string(a->first) < id2string(b->first);
96  });
97 
98  return result;
99 }
100 
102  const
103 {
104  for(const auto &entry : function_map)
105  {
106  const goto_functiont &goto_function = entry.second;
107  const auto &function_name = entry.first;
108  const symbolt &function_symbol = ns.lookup(function_name);
109  const code_typet::parameterst &parameters =
110  to_code_type(function_symbol.type).parameters();
111 
112  DATA_CHECK(
113  vm,
114  goto_function.type == ns.lookup(function_name).type,
115  id2string(function_name) + " type inconsistency\ngoto program type: " +
116  goto_function.type.id_string() +
117  "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
118 
119  DATA_CHECK(
120  vm,
121  goto_function.parameter_identifiers.size() == parameters.size(),
122  id2string(function_name) + " parameter count inconsistency\n" +
123  "goto program: " +
124  std::to_string(goto_function.parameter_identifiers.size()) +
125  "\nsymbol table: " + std::to_string(parameters.size()));
126 
127  auto it = goto_function.parameter_identifiers.begin();
128  for(const auto &parameter : parameters)
129  {
130  DATA_CHECK(
131  vm,
132  it->empty() || ns.lookup(*it).type == parameter.type(),
133  id2string(function_name) + " parameter type inconsistency\n" +
134  "goto program: " + ns.lookup(*it).type.id_string() +
135  "\nsymbol table: " + parameter.type().id_string());
136  ++it;
137  }
138 
139  goto_function.validate(ns, vm);
140  }
141 }
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
goto_functionst::validate
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
Definition: goto_functions.cpp:101
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_functiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
Definition: goto_function.cpp:36
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
goto_functionst::compute_target_numbers
void compute_target_numbers()
Definition: goto_functions.cpp:44
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:729
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
goto_functionst::compute_incoming_edges
void compute_incoming_edges()
Definition: goto_functions.cpp:36
goto_functionst::unused_location_number
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
Definition: goto_functions.h:35