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 
16 
17 #include <util/fresh_symbol.h>
19 
20 #include <sstream>
21 
23 {
24 public:
27  {
29  }
30 
31  // Lower instanceof for a single function
33 
34  // Lower instanceof for a single instruction
36 
37 protected:
41 
42  std::size_t lower_instanceof(
44 };
45 
54  exprt &expr,
56  goto_programt::targett this_inst)
57 {
58  if(expr.id()!=ID_java_instanceof)
59  {
60  std::size_t replacements=0;
61  Forall_operands(it, expr)
62  replacements+=lower_instanceof(*it, goto_program, this_inst);
63  return replacements;
64  }
65 
66  INVARIANT(
67  expr.operands().size()==2,
68  "java_instanceof should have two operands");
69 
70  const exprt &check_ptr=expr.op0();
71  INVARIANT(
72  check_ptr.type().id()==ID_pointer,
73  "instanceof first operand should be a pointer");
74 
75  const exprt &target_arg=expr.op1();
76  INVARIANT(
77  target_arg.id()==ID_type,
78  "instanceof second operand should be a type");
79  const typet &target_type=target_arg.type();
80 
81  // Find all types we know about that satisfy the given requirement:
82  INVARIANT(
83  target_type.id()==ID_symbol,
84  "instanceof second operand should have a simple type");
85  const irep_idt &target_name=
86  to_symbol_type(target_type).get_identifier();
87  std::vector<irep_idt> children=
89  children.push_back(target_name);
90  // Sort alphabetically to make order of generated disjuncts
91  // independent of class loading order
92  std::sort(
93  children.begin(), children.end(), [](const irep_idt &a, const irep_idt &b) {
94  return a.compare(b) < 0;
95  });
96 
97  // Insert an instruction before the new check that assigns the clsid we're
98  // checking for to a temporary, as GOTO program if-expressions should
99  // not contain derefs.
100  // We actually insert the assignment instruction after the existing one.
101  // This will briefly be ill-formed (use before def of instanceof_tmp) but the
102  // two will subsequently switch places. This makes sure that the inserted
103  // assignement doesn't end up before any labels pointing at this instruction.
105  exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
106 
107  symbolt &newsym = get_fresh_aux_symbol(
108  object_clsid.type(),
109  id2string(this_inst->function),
110  "instanceof_tmp",
112  ID_java,
113  symbol_table);
114 
115  auto newinst=goto_program.insert_after(this_inst);
116  newinst->make_assignment();
117  newinst->code=code_assignt(newsym.symbol_expr(), object_clsid);
118  newinst->source_location=this_inst->source_location;
119  newinst->function=this_inst->function;
120 
121  // Replace the instanceof construct with a conjunction of non-null and the
122  // disjunction of all possible object types. According to the Java
123  // specification, null instanceof T is false for all possible values of T.
124  // (http://docs.oracle.com/javase/specs/jls/se7/html/jls-15.html#jls-15.20.2)
125  notequal_exprt non_null_expr(
126  check_ptr, null_pointer_exprt(to_pointer_type(check_ptr.type())));
127  exprt::operandst or_ops;
128  for(const auto &clsname : children)
129  {
130  constant_exprt clsexpr(clsname, string_typet());
131  equal_exprt test(newsym.symbol_expr(), clsexpr);
132  or_ops.push_back(test);
133  }
134  expr = and_exprt(non_null_expr, disjunction(or_ops));
135 
136  return 1;
137 }
138 
147  goto_programt::targett target)
148 {
149  std::size_t replacements=
150  lower_instanceof(target->code, goto_program, target)+
151  lower_instanceof(target->guard, goto_program, target);
152 
153  if(replacements==0)
154  return false;
155  // Swap the original instruction with the last assignment added after it
156  target->swap(*std::next(target, replacements));
157  return true;
158 }
159 
166 {
167  bool changed=false;
168  for(goto_programt::instructionst::iterator target=
169  goto_program.instructions.begin();
170  target!=goto_program.instructions.end();
171  ++target)
172  {
173  changed=lower_instanceof(goto_program, target) || changed;
174  }
175  if(!changed)
176  return false;
178  return true;
179 }
180 
181 
189  goto_programt::targett target,
191  symbol_table_baset &symbol_table)
192 {
193  remove_instanceoft rem(symbol_table);
194  rem.lower_instanceof(goto_program, target);
195 }
196 
204  symbol_table_baset &symbol_table)
205 {
206  remove_instanceoft rem(symbol_table);
207  rem.lower_instanceof(function.body);
208 }
209 
216  goto_functionst &goto_functions,
217  symbol_table_baset &symbol_table)
218 {
219  remove_instanceoft rem(symbol_table);
220  bool changed=false;
221  for(auto &f : goto_functions.function_map)
222  changed=rem.lower_instanceof(f.second.body) || changed;
223  if(changed)
224  goto_functions.compute_location_numbers();
225 }
226 
233 {
234  remove_instanceof(goto_model.goto_functions, goto_model.symbol_table);
235 }
The type of an expression.
Definition: type.h:22
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
Remove Instance-of Operators.
exprt & op0()
Definition: expr.h:72
remove_instanceoft(symbol_table_baset &symbol_table)
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:4520
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...
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:4424
reference_typet java_lang_object_type()
Definition: java_types.cpp:85
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
equality
Definition: std_expr.h:1354
Class Hierarchy.
const irep_idt & id() const
Definition: irep.h:189
void remove_instanceof(goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
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
boolean AND
Definition: std_expr.h:2255
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
exprt & op1()
Definition: expr.h:75
inequality
Definition: std_expr.h:1406
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
symbol_table_baset & symbol_table
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
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: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
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.
const source_locationt & source_location() const
Definition: expr.h:125
int compare(const dstringt &b) const
Definition: dstring.h:106
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
class_hierarchyt class_hierarchy
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
idst get_children_trans(const irep_idt &id) const
operandst & operands()
Definition: expr.h:66
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:195