cprover
parameter_assignments.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Add parameter assignments
4 
5 Author: Daniel Kroening
6 
7 Date: September 2015
8 
9 \*******************************************************************/
10 
13 
14 #include "parameter_assignments.h"
15 
16 #include <util/std_expr.h>
17 #include <util/symbol_table.h>
18 
20 {
21 public:
22  explicit parameter_assignmentst(symbol_tablet &_symbol_table):
23  symbol_table(_symbol_table)
24  {
25  }
26 
27  void operator()(
28  goto_functionst &goto_functions);
29 
30 protected:
32 
33  void do_function_calls(
34  goto_programt &goto_program);
35 };
36 
39  goto_programt &goto_program)
40 {
41  Forall_goto_program_instructions(i_it, goto_program)
42  {
43  if(i_it->is_function_call())
44  {
45  const code_function_callt &function_call = i_it->get_function_call();
46 
47  // add x=y for f(y) where x is the parameter
48 
49  PRECONDITION(function_call.function().id() == ID_symbol);
50 
51  const irep_idt &identifier=
52  to_symbol_expr(function_call.function()).get_identifier();
53 
54  // see if we have it
55  const namespacet ns(symbol_table);
56  const symbolt &function_symbol=ns.lookup(identifier);
57  const code_typet &code_type=to_code_type(function_symbol.type);
58 
59  goto_programt tmp;
60 
61  for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
62  {
63  irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
64 
65  if(p_identifier.empty())
66  continue;
67 
68  if(nr<function_call.arguments().size())
69  {
70  const symbolt &lhs_symbol=ns.lookup(p_identifier);
71  symbol_exprt lhs=lhs_symbol.symbol_expr();
73  function_call.arguments()[nr], lhs.type());
75  code_assignt(lhs, rhs), i_it->source_location));
76  }
77  }
78 
79  std::size_t count=tmp.instructions.size();
80  goto_program.insert_before_swap(i_it, tmp);
81 
82  for(; count!=0; count--) i_it++;
83  }
84  }
85 }
86 
88 {
89  Forall_goto_functions(it, goto_functions)
90  do_function_calls(it->second.body);
91 }
92 
95  symbol_tablet &symbol_table,
96  goto_functionst &goto_functions)
97 {
98  parameter_assignmentst rr(symbol_table);
99  rr(goto_functions);
100 }
101 
104 {
105  parameter_assignmentst rr(goto_model.symbol_table);
106  rr(goto_model.goto_functions);
107 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
parameter_assignments
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Definition: parameter_assignments.cpp:94
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
parameter_assignmentst::do_function_calls
void do_function_calls(goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
Definition: parameter_assignments.cpp:38
parameter_assignmentst::operator()
void operator()(goto_functionst &goto_functions)
Definition: parameter_assignments.cpp:87
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
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
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbolt
Symbol table entry.
Definition: symbol.h:28
parameter_assignments.h
Add parameter assignments.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
parameter_assignmentst::parameter_assignmentst
parameter_assignmentst(symbol_tablet &_symbol_table)
Definition: parameter_assignments.cpp:22
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
symbol_table.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
parameter_assignmentst::symbol_table
symbol_tablet & symbol_table
Definition: parameter_assignments.cpp:31
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
parameter_assignmentst
Definition: parameter_assignments.cpp:20