cprover
goto_convert_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 
11 #include "goto_convert_functions.h"
12 
13 #include <util/base_type.h>
14 #include <util/fresh_symbol.h>
15 #include <util/prefix.h>
16 #include <util/std_code.h>
17 #include <util/symbol_table.h>
19 
20 #include "goto_inline.h"
21 
23  symbol_table_baset &_symbol_table,
24  message_handlert &_message_handler):
25  goto_convertt(_symbol_table, _message_handler)
26 {
27 }
28 
30 {
31 }
32 
34 {
35  // warning! hash-table iterators are not stable
36 
37  typedef std::list<irep_idt> symbol_listt;
38  symbol_listt symbol_list;
39 
40  for(const auto &symbol_pair : symbol_table.symbols)
41  {
42  if(
43  !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
44  symbol_pair.second.type.id() == ID_code &&
45  (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
46  symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
47  {
48  symbol_list.push_back(symbol_pair.first);
49  }
50  }
51 
52  for(const auto &id : symbol_list)
53  {
54  convert_function(id, functions.function_map[id]);
55  }
56 
57  functions.compute_location_numbers();
58 
59  // this removes the parse tree of the bodies from memory
60  #if 0
61  for(const auto &symbol_pair, symbol_table.symbols)
62  {
63  if(!symbol_pair.second.is_type &&
64  symbol_pair.second.type.id()==ID_code &&
65  symbol_pair.second.value.is_not_nil())
66  {
67  symbol_pair.second.value=codet();
68  }
69  }
70  #endif
71 }
72 
74 {
75  forall_goto_program_instructions(i_it, goto_program)
76  {
77  for(const auto &label : i_it->labels)
78  if(label == CPROVER_PREFIX "HIDE")
79  return true;
80  }
81 
82  return false;
83 }
84 
87  const source_locationt &source_location)
88 {
89  #if 0
90  if(!f.body.instructions.empty() &&
91  f.body.instructions.back().is_return())
92  return; // not needed, we have one already
93 
94  // see if we have an unconditional goto at the end
95  if(!f.body.instructions.empty() &&
96  f.body.instructions.back().is_goto() &&
97  f.body.instructions.back().guard.is_true())
98  return;
99  #else
100 
101  if(!f.body.instructions.empty())
102  {
103  goto_programt::const_targett last_instruction=
104  f.body.instructions.end();
105  last_instruction--;
106 
107  while(true)
108  {
109  // unconditional goto, say from while(1)?
110  if(last_instruction->is_goto() &&
111  last_instruction->guard.is_true())
112  return;
113 
114  // return?
115  if(last_instruction->is_return())
116  return;
117 
118  // advance if it's a 'dead' without branch target
119  if(last_instruction->is_dead() &&
120  last_instruction!=f.body.instructions.begin() &&
121  !last_instruction->is_target())
122  last_instruction--;
123  else
124  break; // give up
125  }
126  }
127 
128  #endif
129 
130  const side_effect_expr_nondett rhs(f.type.return_type(), source_location);
131 
132  goto_programt::targett t=f.body.add_instruction();
133  t->make_return();
134  t->code=code_returnt(rhs);
135  t->source_location=source_location;
136 }
137 
139  const irep_idt &identifier,
141 {
142  const symbolt &symbol=ns.lookup(identifier);
143  const irep_idt mode = symbol.mode;
144 
145  if(f.body_available())
146  return; // already converted
147 
148  // make tmp variables local to function
149  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
150 
151  f.type=to_code_type(symbol.type);
152 
153  if(symbol.value.is_nil() ||
154  symbol.is_compiled()) /* goto_inline may have removed the body */
155  return;
156 
157  const codet &code=to_code(symbol.value);
158 
159  source_locationt end_location;
160 
161  if(code.get_statement()==ID_block)
162  end_location=to_code_block(code).end_location();
163  else
164  end_location.make_nil();
165 
166  goto_programt tmp_end_function;
167  goto_programt::targett end_function=tmp_end_function.add_instruction();
168  end_function->type=END_FUNCTION;
169  end_function->source_location=end_location;
170  end_function->code.set(ID_identifier, identifier);
171 
172  targets=targetst();
173  targets.set_return(end_function);
175  f.type.return_type().id()!=ID_empty &&
176  f.type.return_type().id()!=ID_constructor &&
177  f.type.return_type().id()!=ID_destructor;
178 
179  goto_convert_rec(code, f.body, mode);
180 
181  // add non-det return value, if needed
183  add_return(f, end_location);
184 
185  // handle SV-COMP's __VERIFIER_atomic_
186  if(!f.body.instructions.empty() &&
187  has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
188  {
190  a_begin.make_atomic_begin();
191  a_begin.source_location=f.body.instructions.front().source_location;
192  f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
193 
194  goto_programt::targett a_end=f.body.add_instruction();
195  a_end->make_atomic_end();
196  a_end->source_location=end_location;
197 
199  {
200  if(i_it->is_goto() && i_it->get_target()->is_end_function())
201  i_it->set_target(a_end);
202  }
203  }
204 
205  // add "end of function"
206  f.body.destructive_append(tmp_end_function);
207 
208  // do function tags (they are empty at this point)
209  f.update_instructions_function(identifier);
210 
211  f.body.update();
212 
213  if(hide(f.body))
214  f.make_hidden();
215 }
216 
218  goto_modelt &goto_model,
219  message_handlert &message_handler)
220 {
221  symbol_table_buildert symbol_table_builder =
223 
224  goto_convert(
225  symbol_table_builder, goto_model.goto_functions, message_handler);
226 }
227 
229  symbol_table_baset &symbol_table,
230  goto_functionst &functions,
231  message_handlert &message_handler)
232 {
233  symbol_table_buildert symbol_table_builder =
234  symbol_table_buildert::wrap(symbol_table);
235 
236  goto_convert_functionst goto_convert_functions(
237  symbol_table_builder, message_handler);
238 
239  goto_convert_functions.goto_convert(functions);
240 }
241 
243  const irep_idt &identifier,
244  symbol_table_baset &symbol_table,
245  goto_functionst &functions,
246  message_handlert &message_handler)
247 {
248  symbol_table_buildert symbol_table_builder =
249  symbol_table_buildert::wrap(symbol_table);
250 
251  goto_convert_functionst goto_convert_functions(
252  symbol_table_builder, message_handler);
253 
254  goto_convert_functions.convert_function(
255  identifier, functions.function_map[identifier]);
256 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:48
goto_convert_functionst::add_return
void add_return(goto_functionst::goto_functiont &, const source_locationt &)
Definition: goto_convert_functions.cpp:85
goto_inline.h
irept::make_nil
void make_nil()
Definition: irep.h:315
fresh_symbol.h
goto_convertt::goto_convert_rec
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:49
goto_convert_functionst::convert_function
void convert_function(const irep_idt &identifier, goto_functionst::goto_functiont &result)
Definition: goto_convert_functions.cpp:138
prefix.h
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_modelt
Definition: goto_model.h:24
goto_convert_functionst::goto_convert
void goto_convert(goto_functionst &functions)
Definition: goto_convert_functions.cpp:33
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:371
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
base_type.h
goto_convertt
Definition: goto_convert_class.h:26
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
goto_convert_functionst
Definition: goto_convert_functions.h:39
goto_convertt::targetst::set_return
void set_return(goto_programt::targett _return_target)
Definition: goto_convert_class.h:423
irept::is_nil
bool is_nil() const
Definition: irep.h:172
message_handlert
Definition: message.h:24
END_FUNCTION
Definition: goto_program.h:42
goto_convert
void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
Definition: goto_convert_functions.cpp:217
std_code.h
source_locationt
Definition: source_location.h:20
goto_programt::instructiont::make_atomic_begin
void make_atomic_begin()
Definition: goto_program.h:258
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_convertt::targets
struct goto_convertt::targetst targets
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_convertt::targetst
Definition: goto_convert_class.h:369
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
goto_convert_functionst::~goto_convert_functionst
virtual ~goto_convert_functionst()
Definition: goto_convert_functions.cpp:29
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
symbol_table_buildert::wrap
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Definition: symbol_table_builder.h:42
symbol_table_buildert
Author: Diffblue Ltd.
Definition: symbol_table_builder.h:13
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
symbolt::is_compiled
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
Definition: symbol.h:112
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_convert_functionst::goto_convert_functionst
goto_convert_functionst(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: goto_convert_functions.cpp:22
goto_convert_functionst::hide
static bool hide(const goto_programt &)
Definition: goto_convert_functions.cpp:73
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:47
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_convert_functions.h
symbol_table.h
Author: Diffblue Ltd.
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:56
symbol_table_builder.h
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
code_blockt::end_location
source_locationt end_location() const
Definition: std_code.h:208
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34