cprover
java_pointer_casts.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Pointer Casts
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "java_pointer_casts.h"
13 
14 #include <util/namespace.h>
15 #include <util/pointer_expr.h>
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 
19 #include "java_types.h"
20 
23 static exprt clean_deref(const exprt &ptr)
24 {
25  return ptr.id() == ID_address_of ? to_address_of_expr(ptr).object()
26  : dereference_exprt{ptr};
27 }
28 
33  exprt &ptr,
34  const typet &target_type,
35  const namespacet &ns)
36 {
37  assert(ptr.type().id()==ID_pointer);
38  while(true)
39  {
40  const typet ptr_base=ns.follow(ptr.type().subtype());
41 
42  if(ptr_base.id()!=ID_struct)
43  return false;
44 
45  const struct_typet &base_struct=to_struct_type(ptr_base);
46 
47  if(base_struct.components().empty())
48  return false;
49 
50  const typet &first_field_type=base_struct.components()[0].type();
51  ptr=clean_deref(ptr);
52  // Careful not to use the followed type here, as stub types may be
53  // extended by later method conversion adding fields (e.g. an access
54  // against x->y might add a new field `y` to the type of `*x`)
55  ptr=member_exprt(
56  ptr,
57  base_struct.components()[0].get_name(),
58  first_field_type);
59  ptr=address_of_exprt(ptr);
60 
61  // Compare the real (underlying) type, as target_type is already a non-
62  // symbolic type.
63  if(ns.follow(first_field_type)==target_type)
64  return true;
65  }
66 }
67 
68 
71 static const exprt &look_through_casts(const exprt &in)
72 {
73  if(in.id()==ID_typecast)
74  {
75  assert(in.type().id()==ID_pointer);
76  return look_through_casts(to_typecast_expr(in).op());
77  }
78  else
79  return in;
80 }
81 
82 
88  const exprt &rawptr,
89  const pointer_typet &target_type,
90  const namespacet &ns)
91 {
92  const exprt &ptr=look_through_casts(rawptr);
93 
94  PRECONDITION(ptr.type().id()==ID_pointer);
95 
96  if(ptr.type()==target_type)
97  return ptr;
98 
99  if(
100  ptr.type().subtype() == java_void_type() ||
101  target_type.subtype() == java_void_type())
102  return typecast_exprt(ptr, target_type);
103 
104  const typet &target_base=ns.follow(target_type.subtype());
105 
106  exprt bare_ptr=ptr;
107  while(bare_ptr.id()==ID_typecast)
108  {
109  assert(
110  bare_ptr.type().id()==ID_pointer &&
111  "Non-pointer in make_clean_pointer_cast?");
112  if(bare_ptr.type().subtype() == java_void_type())
113  bare_ptr = to_typecast_expr(bare_ptr).op();
114  }
115 
116  assert(
117  bare_ptr.type().id()==ID_pointer &&
118  "Non-pointer in make_clean_pointer_cast?");
119 
120  if(bare_ptr.type()==target_type)
121  return bare_ptr;
122 
123  exprt superclass_ptr=bare_ptr;
124  // Looking at base types discards generic qualifiers (because those are
125  // recorded on the pointer, not the pointee), so it may still be necessary
126  // to use a cast to reintroduce the qualifier (for example, the base might
127  // be recorded as a List, when we're looking for a List<E>)
128  if(find_superclass_with_type(superclass_ptr, target_base, ns))
129  return typecast_exprt::conditional_cast(superclass_ptr, target_type);
130 
131  return typecast_exprt(bare_ptr, target_type);
132 }
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt & object()
Definition: pointer_expr.h:209
Operator to dereference a pointer.
Definition: pointer_expr.h:256
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentst & components() const
Definition: std_types.h:142
Semantic type conversion.
Definition: std_expr.h:1781
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
const exprt & op() const
Definition: std_expr.h:294
bool find_superclass_with_type(exprt &ptr, const typet &target_type, const namespacet &ns)
static exprt clean_deref(const exprt &ptr)
dereference pointer expression
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
static const exprt & look_through_casts(const exprt &in)
JAVA Pointer Casts.
empty_typet java_void_type()
Definition: java_types.cpp:38
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303