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 
20 static exprt clean_deref(const exprt &ptr)
21 {
22  return ptr.id()==ID_address_of
23  ? ptr.op0()
24  : dereference_exprt(ptr, ptr.type().subtype());
25 }
26 
31  exprt &ptr,
32  const typet &target_type,
33  const namespacet &ns)
34 {
35  assert(ptr.type().id()==ID_pointer);
36  while(true)
37  {
38  const typet ptr_base=ns.follow(ptr.type().subtype());
39 
40  if(ptr_base.id()!=ID_struct)
41  return false;
42 
43  const struct_typet &base_struct=to_struct_type(ptr_base);
44 
45  if(base_struct.components().empty())
46  return false;
47 
48  const typet &first_field_type=base_struct.components()[0].type();
49  ptr=clean_deref(ptr);
50  // Careful not to use the followed type here, as stub types may be
51  // extended by later method conversion adding fields (e.g. an access
52  // against x->y might add a new field `y` to the type of `*x`)
53  ptr=member_exprt(
54  ptr,
55  base_struct.components()[0].get_name(),
56  first_field_type);
57  ptr=address_of_exprt(ptr);
58 
59  // Compare the real (underlying) type, as target_type is already a non-
60  // symbolic type.
61  if(ns.follow(first_field_type)==target_type)
62  return true;
63  }
64 }
65 
66 
69 static const exprt &look_through_casts(const exprt &in)
70 {
71  if(in.id()==ID_typecast)
72  {
73  assert(in.type().id()==ID_pointer);
74  return look_through_casts(in.op0());
75  }
76  else
77  return in;
78 }
79 
80 
86  const exprt &rawptr,
87  const pointer_typet &target_type,
88  const namespacet &ns)
89 {
90  const exprt &ptr=look_through_casts(rawptr);
91 
92  PRECONDITION(ptr.type().id()==ID_pointer);
93 
94  if(ptr.type()==target_type)
95  return ptr;
96 
97  if(ptr.type().subtype()==empty_typet() ||
98  target_type.subtype()==empty_typet())
99  return typecast_exprt(ptr, target_type);
100 
101  const typet &target_base=ns.follow(target_type.subtype());
102 
103  exprt bare_ptr=ptr;
104  while(bare_ptr.id()==ID_typecast)
105  {
106  assert(
107  bare_ptr.type().id()==ID_pointer &&
108  "Non-pointer in make_clean_pointer_cast?");
109  if(bare_ptr.type().subtype()==empty_typet())
110  bare_ptr=bare_ptr.op0();
111  }
112 
113  assert(
114  bare_ptr.type().id()==ID_pointer &&
115  "Non-pointer in make_clean_pointer_cast?");
116 
117  if(bare_ptr.type()==target_type)
118  return bare_ptr;
119 
120  exprt superclass_ptr=bare_ptr;
121  if(find_superclass_with_type(superclass_ptr, target_base, ns))
122  return superclass_ptr;
123 
124  return typecast_exprt(bare_ptr, target_type);
125 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
typet
The type of an expression, extends irept.
Definition: type.h:27
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:3355
exprt
Base class for all expressions.
Definition: expr.h:54
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:85
exprt::op0
exprt & op0()
Definition: expr.h:84
find_superclass_with_type
bool find_superclass_with_type(exprt &ptr, const typet &target_type, const namespacet &ns)
Definition: java_pointer_casts.cpp:30
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
java_pointer_casts.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
clean_deref
static exprt clean_deref(const exprt &ptr)
dereference pointer expression
Definition: java_pointer_casts.cpp:20
empty_typet
The empty type.
Definition: std_types.h:48
std_types.h
irept::id
const irep_idt & id() const
Definition: irep.h:259
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
std_expr.h
look_through_casts
static const exprt & look_through_casts(const exprt &in)
Definition: java_pointer_casts.cpp:69