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:
29  , ns(symbol_table)
31  {
33  }
34 
35  // Lower instanceof for a single function
37 
38  // Lower instanceof for a single instruction
40 
41 protected:
46 
47  bool lower_instanceof(
49 };
50 
59  exprt &expr,
61  goto_programt::targett this_inst)
62 {
63  if(expr.id()!=ID_java_instanceof)
64  {
65  bool changed = false;
66  Forall_operands(it, expr)
67  changed |= lower_instanceof(*it, goto_program, this_inst);
68  return changed;
69  }
70 
71  INVARIANT(
72  expr.operands().size()==2,
73  "java_instanceof should have two operands");
74 
75  const exprt &check_ptr=expr.op0();
76  INVARIANT(
77  check_ptr.type().id()==ID_pointer,
78  "instanceof first operand should be a pointer");
79 
80  const exprt &target_arg=expr.op1();
81  INVARIANT(
82  target_arg.id()==ID_type,
83  "instanceof second operand should be a type");
84  const typet &target_type=target_arg.type();
85 
86  // Find all types we know about that satisfy the given requirement:
87  INVARIANT(
88  target_type.id()==ID_symbol,
89  "instanceof second operand should have a simple type");
90  const irep_idt &target_name=
91  to_symbol_type(target_type).get_identifier();
92  std::vector<irep_idt> children=
94  children.push_back(target_name);
95  // Sort alphabetically to make order of generated disjuncts
96  // independent of class loading order
97  std::sort(
98  children.begin(), children.end(), [](const irep_idt &a, const irep_idt &b) {
99  return a.compare(b) < 0;
100  });
101 
102  // Make temporaries to store the class identifier (avoids repeated derefs) and
103  // the instanceof result:
104 
106  exprt object_clsid = get_class_identifier_field(check_ptr, jlo, ns);
107 
108  symbolt &clsid_tmp_sym = get_fresh_aux_symbol(
109  object_clsid.type(),
110  id2string(this_inst->function),
111  "class_identifier_tmp",
113  ID_java,
114  symbol_table);
115 
116  symbolt &instanceof_result_sym = get_fresh_aux_symbol(
117  bool_typet(),
118  id2string(this_inst->function),
119  "instanceof_result_tmp",
121  ID_java,
122  symbol_table);
123 
124  // Create
125  // if(expr == null)
126  // instanceof_result = false;
127  // else
128  // string clsid = expr->@class_identifier
129  // instanceof_result = clsid == "A" || clsid == "B" || ...
130 
131  // According to the Java specification, null instanceof T is false for all
132  // possible values of T.
133  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
134 
135  code_ifthenelset is_null_branch;
136  is_null_branch.cond() =
137  equal_exprt(
138  check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
139  is_null_branch.then_case() =
140  code_assignt(instanceof_result_sym.symbol_expr(), false_exprt());
141 
142  code_blockt else_block;
143  else_block.add(code_declt(clsid_tmp_sym.symbol_expr()));
144  else_block.add(code_assignt(clsid_tmp_sym.symbol_expr(), object_clsid));
145 
146  exprt::operandst or_ops;
147  for(const auto &clsname : children)
148  {
149  constant_exprt clsexpr(clsname, string_typet());
150  equal_exprt test(clsid_tmp_sym.symbol_expr(), clsexpr);
151  or_ops.push_back(test);
152  }
153  else_block.add(
154  code_assignt(instanceof_result_sym.symbol_expr(), disjunction(or_ops)));
155 
156  is_null_branch.else_case() = std::move(else_block);
157 
158  // Replace the instanceof construct with instanceof_result:
159  expr = instanceof_result_sym.symbol_expr();
160 
161  // Insert the new test block before it:
162  goto_programt new_check_program;
163  goto_convert(
164  is_null_branch,
165  symbol_table,
166  new_check_program,
168  ID_java);
169 
170  goto_program.destructive_insert(this_inst, new_check_program);
171 
172  return true;
173 }
174 
175 static bool contains_instanceof(const exprt &e)
176 {
177  if(e.id() == ID_java_instanceof)
178  return true;
179 
180  for(const exprt &subexpr : e.operands())
181  {
182  if(contains_instanceof(subexpr))
183  return true;
184  }
185 
186  return false;
187 }
188 
197  goto_programt::targett target)
198 {
199  if(target->is_target() &&
200  (contains_instanceof(target->code) || contains_instanceof(target->guard)))
201  {
202  // If this is a branch target, add a skip beforehand so we can splice new
203  // GOTO programs before the target instruction without inserting into the
204  // wrong basic block.
206  target->make_skip();
207  // Actually alter the now-moved instruction:
208  ++target;
209  }
210 
211  return lower_instanceof(target->code, goto_program, target) |
212  lower_instanceof(target->guard, goto_program, target);
213 }
214 
221 {
222  bool changed=false;
223  for(goto_programt::instructionst::iterator target=
224  goto_program.instructions.begin();
225  target!=goto_program.instructions.end();
226  ++target)
227  {
228  changed=lower_instanceof(goto_program, target) || changed;
229  }
230  if(!changed)
231  return false;
233  return true;
234 }
235 
236 
245  goto_programt::targett target,
247  symbol_table_baset &symbol_table,
249 {
250  remove_instanceoft rem(symbol_table, message_handler);
251  rem.lower_instanceof(goto_program, target);
252 }
253 
262  symbol_table_baset &symbol_table,
264 {
265  remove_instanceoft rem(symbol_table, message_handler);
266  rem.lower_instanceof(function.body);
267 }
268 
276  goto_functionst &goto_functions,
277  symbol_table_baset &symbol_table,
279 {
280  remove_instanceoft rem(symbol_table, message_handler);
281  bool changed=false;
282  for(auto &f : goto_functions.function_map)
283  changed=rem.lower_instanceof(f.second.body) || changed;
284  if(changed)
285  goto_functions.compute_location_numbers();
286 }
287 
295  goto_modelt &goto_model,
297 {
299  goto_model.goto_functions, goto_model.symbol_table, message_handler);
300 }
The type of an expression.
Definition: type.h:22
const codet & then_case() const
Definition: std_code.h:486
void update()
Update all indices.
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:441
Remove Instance-of Operators.
exprt & op0()
Definition: expr.h:72
Non-graph-based representation of the class hierarchy.
const exprt & cond() const
Definition: std_code.h:476
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.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4518
function_mapt function_map
typet & type()
Definition: expr.h:56
bool lower_instanceof(goto_programt &)
Replace every instanceof in the passed function body with an explicit class-identifier test...
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
A constant literal expression.
Definition: std_expr.h:4422
remove_instanceoft(symbol_table_baset &symbol_table, message_handlert &message_handler)
static bool contains_instanceof(const exprt &e)
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
equality
Definition: std_expr.h:1354
Class Hierarchy.
const irep_idt & id() const
Definition: irep.h:259
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
void compute_location_numbers()
A reference into the symbol table.
Definition: std_types.h:110
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:254
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
exprt & op1()
Definition: expr.h:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
The boolean constant false.
Definition: std_expr.h:4497
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:24
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
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:42
The symbol table base class interface.
int compare(const dstringt &b) const
Definition: dstring.h:118
Program Transformation.
irept & add(const irep_namet &name)
Definition: irep.cpp:306
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
class_hierarchyt class_hierarchy
Sequential composition.
Definition: std_code.h:89
message_handlert & message_handler
An if-then-else.
Definition: std_code.h:466
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
idst get_children_trans(const irep_idt &id) const
operandst & operands()
Definition: expr.h:66
const codet & else_case() const
Definition: std_code.h:496
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
const irep_idt & get_identifier() const
Definition: std_types.h:123
Assignment.
Definition: std_code.h:196