cprover
remove_instanceof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove Instance-of Operators
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "remove_instanceof.h"
13 
14 #include "class_hierarchy.h"
15 #include "class_identifier.h"
16 
17 #include <util/fresh_symbol.h>
18 
19 #include <sstream>
20 
22 {
23 public:
25  symbol_tablet &_symbol_table,
26  goto_functionst &_goto_functions):
27  symbol_table(_symbol_table),
28  ns(_symbol_table),
29  goto_functions(_goto_functions)
30  {
31  class_hierarchy(_symbol_table);
32  }
33 
34  // Lower instanceof for all functions:
35  void lower_instanceof();
36 
37 protected:
42 
44 
45  typedef std::vector<
46  std::pair<goto_programt::targett, goto_programt::targett>> instanceof_instt;
47 
48  void lower_instanceof(
49  goto_programt &,
51  instanceof_instt &);
52 
53  void lower_instanceof(
54  exprt &,
55  goto_programt &,
57  instanceof_instt &);
58 
59  bool contains_instanceof(const exprt &);
60 };
61 
67  const exprt &expr)
68 {
69  if(expr.id()==ID_java_instanceof)
70  return true;
71  forall_operands(it, expr)
72  if(contains_instanceof(*it))
73  return true;
74  return false;
75 }
76 
84  exprt &expr,
85  goto_programt &goto_program,
86  goto_programt::targett this_inst,
87  instanceof_instt &inst_switch)
88 {
89  if(expr.id()==ID_java_instanceof)
90  {
91  const exprt &check_ptr=expr.op0();
92  assert(check_ptr.type().id()==ID_pointer);
93  const exprt &target_arg=expr.op1();
94  assert(target_arg.id()==ID_type);
95  const typet &target_type=target_arg.type();
96 
97  // Find all types we know about that satisfy the given requirement:
98  assert(target_type.id()==ID_symbol);
99  const irep_idt &target_name=
100  to_symbol_type(target_type).get_identifier();
101  std::vector<irep_idt> children=
102  class_hierarchy.get_children_trans(target_name);
103  children.push_back(target_name);
104 
105  assert(!children.empty() && "Unable to execute instanceof");
106 
107  // Insert an instruction before this one that assigns the clsid we're
108  // checking against to a temporary, as GOTO program if-expressions should
109  // not contain derefs.
110 
111  symbol_typet jlo("java::java.lang.Object");
112  exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
113 
114  symbolt &newsym=
116  object_clsid.type(),
117  "instanceof_tmp",
118  "instanceof_tmp",
120  ID_java,
121  symbol_table);
122 
123  auto newinst=goto_program.insert_after(this_inst);
124  newinst->make_assignment();
125  newinst->code=code_assignt(newsym.symbol_expr(), object_clsid);
126  newinst->source_location=this_inst->source_location;
127 
128  // Insert the check instruction after the existing one.
129  // This will briefly be ill-formed (use before def of
130  // instanceof_tmp) but the two will subsequently switch
131  // places in lower_instanceof(goto_programt &) below.
132  inst_switch.push_back(make_pair(this_inst, newinst));
133  // Replace the instanceof construct with a big-or.
134  exprt::operandst or_ops;
135  for(const auto &clsname : children)
136  {
137  constant_exprt clsexpr(clsname, string_typet());
138  equal_exprt test(newsym.symbol_expr(), clsexpr);
139  or_ops.push_back(test);
140  }
141  expr=disjunction(or_ops);
142  }
143  else
144  {
145  Forall_operands(it, expr)
146  lower_instanceof(*it, goto_program, this_inst, inst_switch);
147  }
148 }
149 
157  goto_programt &goto_program,
158  goto_programt::targett target,
159  instanceof_instt &inst_switch)
160 {
161  bool code_iof=contains_instanceof(target->code);
162  bool guard_iof=contains_instanceof(target->guard);
163  // The instruction-switching step below will malfunction if a check
164  // has been added for the code *and* for the guard. This should
165  // be impossible, because guarded instructions currently have simple
166  // code (e.g. a guarded-goto), but this assertion checks that this
167  // assumption is correct and remains true on future evolution of the
168  // allowable goto instruction types.
169  assert(!(code_iof && guard_iof));
170  if(code_iof)
171  lower_instanceof(target->code, goto_program, target, inst_switch);
172  if(guard_iof)
173  lower_instanceof(target->guard, goto_program, target, inst_switch);
174 }
175 
181 {
182  instanceof_instt inst_switch;
183  Forall_goto_program_instructions(target, goto_program)
184  lower_instanceof(goto_program, target, inst_switch);
185  if(!inst_switch.empty())
186  {
187  for(auto &p : inst_switch)
188  {
189  const goto_programt::targett &this_inst=p.first;
190  const goto_programt::targett &newinst=p.second;
191  this_inst->swap(*newinst);
192  }
193  goto_program.update();
194  return true;
195  }
196  else
197  return false;
198 }
199 
204 {
205  bool changed=false;
206  for(auto &f : goto_functions.function_map)
207  changed=(lower_instanceof(f.second.body) || changed);
208  if(changed)
210 }
211 
221 {
222  remove_instanceoft rem(symbol_table, goto_functions);
223  rem.lower_instanceof();
224 }
225 
227 {
229  goto_model.symbol_table, goto_model.goto_functions);
230 }
void lower_instanceof()
See function above.
The type of an expression.
Definition: type.h:20
void update()
Update all indices.
Remove Instance-of Operators.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & op0()
Definition: expr.h:84
Fresh auxiliary symbol creation.
bool contains_instanceof(const exprt &)
Avoid breaking sharing by checking for instanceof before calling lower_instanceof.
typet & type()
Definition: expr.h:60
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
equality
Definition: std_expr.h:1082
Class Hierarchy.
const irep_idt & id() const
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
A reference into the symbol table.
Definition: std_types.h:109
void remove_instanceof(symbol_tablet &symbol_table, goto_functionst &goto_functions)
See function above.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define forall_operands(it, expr)
Definition: expr.h:17
goto_functionst & goto_functions
targett insert_after(const_targett target)
Insertion after the given target.
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:26
std::vector< exprt > operandst
Definition: expr.h:49
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
symbol_tablet & symbol_table
Base class for all expressions.
Definition: expr.h:46
std::vector< std::pair< goto_programt::targett, goto_programt::targett > > instanceof_instt
const source_locationt & source_location() const
Definition: expr.h:142
remove_instanceoft(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
#define Forall_operands(it, expr)
Definition: expr.h:23
class_hierarchyt class_hierarchy
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Extract class identifier.
idst get_children_trans(const irep_idt &id) const
goto_functionst goto_functions
Definition: goto_model.h:26
const irep_idt & get_identifier() const
Definition: std_types.h:126
Assignment.
Definition: std_code.h:144