cprover
link_to_library.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Library Linking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "link_to_library.h"
13 
15 #include "goto_convert_functions.h"
16 
25  goto_modelt &goto_model,
26  message_handlert &message_handler,
27  const std::function<
28  void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
29  &library)
30 {
31  // this needs a fixedpoint, as library functions
32  // may depend on other library functions
33 
34  std::set<irep_idt> added_functions;
35 
36  while(true)
37  {
38  std::unordered_set<irep_idt> called_functions =
40 
41  // eliminate those for which we already have a body
42 
43  std::set<irep_idt> missing_functions;
44 
45  for(const auto &id : called_functions)
46  {
47  goto_functionst::function_mapt::const_iterator f_it =
48  goto_model.goto_functions.function_map.find(id);
49 
50  if(
51  f_it != goto_model.goto_functions.function_map.end() &&
52  f_it->second.body_available())
53  {
54  // it's overridden!
55  }
56  else if(added_functions.find(id) != added_functions.end())
57  {
58  // already added
59  }
60  else
61  missing_functions.insert(id);
62  }
63 
64  // done?
65  if(missing_functions.empty())
66  break;
67 
68  library(missing_functions, goto_model.symbol_table, message_handler);
69 
70  // convert to CFG
71  for(const auto &id : missing_functions)
72  {
73  if(
74  goto_model.symbol_table.symbols.find(id) !=
75  goto_model.symbol_table.symbols.end())
76  {
78  id,
79  goto_model.symbol_table,
80  goto_model.goto_functions,
81  message_handler);
82  }
83 
84  added_functions.insert(id);
85  }
86  }
87 }
88 
99  symbol_tablet &symbol_table,
100  goto_functionst &goto_functions,
101  message_handlert &message_handler,
102  const std::function<
103  void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
104  &library)
105 {
106  // this needs a fixedpoint, as library functions
107  // may depend on other library functions
108 
109  std::set<irep_idt> added_functions;
110 
111  while(true)
112  {
113  std::unordered_set<irep_idt> called_functions =
114  compute_called_functions(goto_functions);
115 
116  // eliminate those for which we already have a body
117 
118  std::set<irep_idt> missing_functions;
119 
120  for(const auto &id : called_functions)
121  {
122  goto_functionst::function_mapt::const_iterator
123  f_it=goto_functions.function_map.find(id);
124 
125  if(f_it!=goto_functions.function_map.end() &&
126  f_it->second.body_available())
127  {
128  // it's overridden!
129  }
130  else if(added_functions.find(id)!=added_functions.end())
131  {
132  // already added
133  }
134  else
135  missing_functions.insert(id);
136  }
137 
138  // done?
139  if(missing_functions.empty())
140  break;
141 
142  library(missing_functions, symbol_table, message_handler);
143 
144  // convert to CFG
145  for(const auto &id : missing_functions)
146  {
147  if(symbol_table.symbols.find(id)!=symbol_table.symbols.end())
148  goto_convert(id, symbol_table, goto_functions, message_handler);
149 
150  added_functions.insert(id);
151  }
152  }
153 }
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_modelt
Definition: goto_model.h:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
compute_called_functions
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
Definition: compute_called_functions.cpp:85
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1846
message_handlert
Definition: message.h:28
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
compute_called_functions.h
Query Called Functions.
goto_convert_functions.h
Goto Programs with Functions.
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30