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 
19 #include "goto_model.h"
20 
22 {
23 public:
24  explicit parameter_assignmentst(symbol_tablet &_symbol_table):
25  symbol_table(_symbol_table)
26  {
27  }
28 
29  void operator()(
30  goto_functionst &goto_functions);
31 
32 protected:
34 
35  void do_function_calls(
36  goto_programt &goto_program);
37 };
38 
41  goto_programt &goto_program)
42 {
43  Forall_goto_program_instructions(i_it, goto_program)
44  {
45  if(i_it->is_function_call())
46  {
47  // add x=y for f(y) where x is the parameter
48  PRECONDITION(as_const(*i_it).call_function().id() == ID_symbol);
49 
50  const irep_idt &identifier =
51  to_symbol_expr(as_const(*i_it).call_function()).get_identifier();
52 
53  // see if we have it
54  const namespacet ns(symbol_table);
55  const symbolt &function_symbol=ns.lookup(identifier);
56  const code_typet &code_type=to_code_type(function_symbol.type);
57 
58  goto_programt tmp;
59 
60  for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
61  {
62  irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
63 
64  if(p_identifier.empty())
65  continue;
66 
67  if(nr < as_const(*i_it).call_arguments().size())
68  {
69  const symbolt &lhs_symbol=ns.lookup(p_identifier);
70  symbol_exprt lhs=lhs_symbol.symbol_expr();
72  as_const(*i_it).call_arguments()[nr], lhs.type());
74  code_assignt(lhs, rhs), i_it->source_location()));
75  }
76  }
77 
78  std::size_t count=tmp.instructions.size();
79  goto_program.insert_before_swap(i_it, tmp);
80 
81  for(; count!=0; count--) i_it++;
82  }
83  }
84 }
85 
87 {
88  for(auto &gf_entry : goto_functions.function_map)
89  do_function_calls(gf_entry.second.body);
90 }
91 
94  symbol_tablet &symbol_table,
95  goto_functionst &goto_functions)
96 {
97  parameter_assignmentst rr(symbol_table);
98  rr(goto_functions);
99 }
100 
103 {
104  parameter_assignmentst rr(goto_model.symbol_table);
105  rr(goto_model.goto_functions);
106 }
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
A codet representing an assignment in the program.
Base type of functions.
Definition: std_types.h:539
const parameterst & parameters() const
Definition: std_types.h:655
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
void do_function_calls(goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
void operator()(goto_functionst &goto_functions)
parameter_assignmentst(symbol_tablet &_symbol_table)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Author: Diffblue Ltd.