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 }
The type of an expression, extends irept.
Definition: type.h:27
Semantic type conversion.
Definition: std_expr.h:2277
exprt & op0()
Definition: expr.h:84
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
Structure type, corresponds to C style structs.
Definition: std_types.h:276
Extract member of struct or union.
Definition: std_expr.h:3890
bool find_superclass_with_type(exprt &ptr, const typet &target_type, const namespacet &ns)
const irep_idt & id() const
Definition: irep.h:259
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
The empty type.
Definition: std_types.h:48
Operator to dereference a pointer.
Definition: std_expr.h:3355
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
Operator to return the address of an object.
Definition: std_expr.h:3255
Pre-defined types.
Base class for all expressions.
Definition: expr.h:54
JAVA Pointer Casts.
static exprt clean_deref(const exprt &ptr)
dereference pointer expression
static const exprt & look_through_casts(const exprt &in)
const typet & subtype() const
Definition: type.h:38
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)