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