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 
17 
18 #include <util/fresh_symbol.h>
20 
21 #include <sstream>
22 
24 {
25 public:
34  {
35  }
36 
37  // Lower instanceof for a single function
39 
40  // Lower instanceof for a single instruction
42 
43 protected:
48 
49  bool lower_instanceof(
51 };
52 
61  exprt &expr,
62  goto_programt &goto_program,
63  goto_programt::targett this_inst)
64 {
65  if(expr.id()!=ID_java_instanceof)
66  {
67  bool changed = false;
68  Forall_operands(it, expr)
69  changed |= lower_instanceof(*it, goto_program, this_inst);
70  return changed;
71  }
72 
73  INVARIANT(
74  expr.operands().size()==2,
75  "java_instanceof should have two operands");
76 
77  const exprt &check_ptr=expr.op0();
78  INVARIANT(
79  check_ptr.type().id()==ID_pointer,
80  "instanceof first operand should be a pointer");
81 
82  const exprt &target_arg=expr.op1();
83  INVARIANT(
84  target_arg.id()==ID_type,
85  "instanceof second operand should be a type");
86  const typet &target_type=target_arg.type();
87 
88  // Find all types we know about that satisfy the given requirement:
89  INVARIANT(
90  target_type.id() == ID_struct_tag,
91  "instanceof second operand should have a simple type");
92  const irep_idt &target_name =
93  to_struct_tag_type(target_type).get_identifier();
94  std::vector<irep_idt> children=
96  children.push_back(target_name);
97  // Sort alphabetically to make order of generated disjuncts
98  // independent of class loading order
99  std::sort(
100  children.begin(), children.end(), [](const irep_idt &a, const irep_idt &b) {
101  return a.compare(b) < 0;
102  });
103 
104  // Make temporaries to store the class identifier (avoids repeated derefs) and
105  // the instanceof result:
106 
107  auto jlo = to_struct_tag_type(java_lang_object_type().subtype());
108  exprt object_clsid = get_class_identifier_field(check_ptr, jlo, ns);
109 
110  symbolt &clsid_tmp_sym = get_fresh_aux_symbol(
111  object_clsid.type(),
112  id2string(this_inst->function),
113  "class_identifier_tmp",
115  ID_java,
116  symbol_table);
117 
118  symbolt &instanceof_result_sym = get_fresh_aux_symbol(
119  bool_typet(),
120  id2string(this_inst->function),
121  "instanceof_result_tmp",
123  ID_java,
124  symbol_table);
125 
126  // Create
127  // if(expr == null)
128  // instanceof_result = false;
129  // else
130  // string clsid = expr->@class_identifier
131  // instanceof_result = clsid == "A" || clsid == "B" || ...
132 
133  // According to the Java specification, null instanceof T is false for all
134  // possible values of T.
135  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
136 
137  code_blockt else_block;
138  else_block.add(code_declt(clsid_tmp_sym.symbol_expr()));
139  else_block.add(code_assignt(clsid_tmp_sym.symbol_expr(), object_clsid));
140 
141  exprt::operandst or_ops;
142  for(const auto &clsname : children)
143  {
144  constant_exprt clsexpr(clsname, string_typet());
145  equal_exprt test(clsid_tmp_sym.symbol_expr(), clsexpr);
146  or_ops.push_back(test);
147  }
148  else_block.add(
149  code_assignt(instanceof_result_sym.symbol_expr(), disjunction(or_ops)));
150 
151  const code_ifthenelset is_null_branch(
152  equal_exprt(
153  check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type()))),
154  code_assignt(instanceof_result_sym.symbol_expr(), false_exprt()),
155  std::move(else_block));
156 
157  // Replace the instanceof construct with instanceof_result:
158  expr = instanceof_result_sym.symbol_expr();
159 
160  // Insert the new test block before it:
161  goto_programt new_check_program;
162  goto_convert(
163  is_null_branch,
164  symbol_table,
165  new_check_program,
167  ID_java);
168 
169  goto_program.destructive_insert(this_inst, new_check_program);
170 
171  return true;
172 }
173 
174 static bool contains_instanceof(const exprt &e)
175 {
176  if(e.id() == ID_java_instanceof)
177  return true;
178 
179  for(const exprt &subexpr : e.operands())
180  {
181  if(contains_instanceof(subexpr))
182  return true;
183  }
184 
185  return false;
186 }
187 
195  goto_programt &goto_program,
196  goto_programt::targett target)
197 {
198  if(target->is_target() &&
199  (contains_instanceof(target->code) || contains_instanceof(target->guard)))
200  {
201  // If this is a branch target, add a skip beforehand so we can splice new
202  // GOTO programs before the target instruction without inserting into the
203  // wrong basic block.
204  goto_program.insert_before_swap(target);
205  target->make_skip();
206  // Actually alter the now-moved instruction:
207  ++target;
208  }
209 
210  return lower_instanceof(target->code, goto_program, target) |
211  lower_instanceof(target->guard, goto_program, target);
212 }
213 
220 {
221  bool changed=false;
222  for(goto_programt::instructionst::iterator target=
223  goto_program.instructions.begin();
224  target!=goto_program.instructions.end();
225  ++target)
226  {
227  changed=lower_instanceof(goto_program, target) || changed;
228  }
229  if(!changed)
230  return false;
231  goto_program.update();
232  return true;
233 }
234 
244  goto_programt::targett target,
245  goto_programt &goto_program,
246  symbol_table_baset &symbol_table,
247  const class_hierarchyt &class_hierarchy,
248  message_handlert &message_handler)
249 {
250  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
251  rem.lower_instanceof(goto_program, target);
252 }
253 
263  symbol_table_baset &symbol_table,
264  const class_hierarchyt &class_hierarchy,
265  message_handlert &message_handler)
266 {
267  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
268  rem.lower_instanceof(function.body);
269 }
270 
279  goto_functionst &goto_functions,
280  symbol_table_baset &symbol_table,
281  const class_hierarchyt &class_hierarchy,
282  message_handlert &message_handler)
283 {
284  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
285  bool changed=false;
286  for(auto &f : goto_functions.function_map)
287  changed=rem.lower_instanceof(f.second.body) || changed;
288  if(changed)
289  goto_functions.compute_location_numbers();
290 }
291 
301  goto_modelt &goto_model,
302  const class_hierarchyt &class_hierarchy,
303  message_handlert &message_handler)
304 {
306  goto_model.goto_functions,
307  goto_model.symbol_table,
308  class_hierarchy,
309  message_handler);
310 }
The type of an expression, extends irept.
Definition: type.h:27
void update()
Update all indices.
const irep_idt & get_identifier() const
Definition: std_types.h:479
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:477
Remove Instance-of Operators.
exprt & op0()
Definition: expr.h:84
Non-graph-based representation of the class hierarchy.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4471
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
bool lower_instanceof(goto_programt &)
Replace every instanceof in the passed function body with an explicit class-identifier test.
The Boolean type.
Definition: std_types.h:28
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
remove_instanceoft(symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
A constant literal expression.
Definition: std_expr.h:4384
static bool contains_instanceof(const exprt &e)
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
String type.
Definition: std_types.h:1662
Equality.
Definition: std_expr.h:1484
Class Hierarchy.
const irep_idt & id() const
Definition: irep.h:259
const class_hierarchyt & class_hierarchy
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
void compute_location_numbers()
instructionst::iterator targett
Definition: goto_program.h:414
A codet representing the declaration of a local variable.
Definition: std_code.h:352
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
exprt & op1()
Definition: expr.h:87
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
The Boolean constant false.
Definition: std_expr.h:4452
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:26
std::vector< exprt > operandst
Definition: expr.h:57
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
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_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
Definition: expr.h:54
The symbol table base class interface.
int compare(const dstringt &b) const
Definition: dstring.h:120
Program Transformation.
#define Forall_operands(it, expr)
Definition: expr.h:26
A codet representing sequential composition of program statements.
Definition: std_code.h:150
message_handlert & message_handler
codet representation of an if-then-else statement.
Definition: std_code.h:614
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
idst get_children_trans(const irep_idt &id) const
operandst & operands()
Definition: expr.h:78
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256