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=
49  ns.follow(base_struct.components()[0].type());
50  ptr=clean_deref(ptr);
51  ptr=member_exprt(
52  ptr,
53  base_struct.components()[0].get_name(),
54  first_field_type);
55  ptr=address_of_exprt(ptr);
56 
57  if(first_field_type==target_type)
58  return true;
59  }
60 }
61 
62 
65 static const exprt &look_through_casts(const exprt &in)
66 {
67  if(in.id()==ID_typecast)
68  {
69  assert(in.type().id()==ID_pointer);
70  return look_through_casts(in.op0());
71  }
72  else
73  return in;
74 }
75 
76 
82  const exprt &rawptr,
83  const typet &target_type,
84  const namespacet &ns)
85 {
86  assert(
87  target_type.id()==ID_pointer &&
88  "Non-pointer target in make_clean_pointer_cast?");
89 
90  const exprt &ptr=look_through_casts(rawptr);
91 
92  if(ptr.type()==target_type)
93  return ptr;
94 
95  if(ptr.type().subtype()==empty_typet() ||
96  target_type.subtype()==empty_typet())
97  return typecast_exprt(ptr, target_type);
98 
99  const typet &target_base=ns.follow(target_type.subtype());
100 
101  exprt bare_ptr=ptr;
102  while(bare_ptr.id()==ID_typecast)
103  {
104  assert(
105  bare_ptr.type().id()==ID_pointer &&
106  "Non-pointer in make_clean_pointer_cast?");
107  if(bare_ptr.type().subtype()==empty_typet())
108  bare_ptr=bare_ptr.op0();
109  }
110 
111  assert(
112  bare_ptr.type().id()==ID_pointer &&
113  "Non-pointer in make_clean_pointer_cast?");
114 
115  if(bare_ptr.type()==target_type)
116  return bare_ptr;
117 
118  exprt superclass_ptr=bare_ptr;
119  if(find_superclass_with_type(superclass_ptr, target_base, ns))
120  return superclass_ptr;
121 
122  return typecast_exprt(bare_ptr, target_type);
123 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
exprt & op0()
Definition: expr.h:84
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
Extract member of struct or union.
Definition: std_expr.h:3214
bool find_superclass_with_type(exprt &ptr, const typet &target_type, const namespacet &ns)
const irep_idt & id() const
Definition: irep.h:189
The empty type.
Definition: std_types.h:53
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Operator to return the address of an object.
Definition: std_expr.h:2593
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
API to type classes.
Base class for all expressions.
Definition: expr.h:46
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:31
exprt make_clean_pointer_cast(const exprt &rawptr, const typet &target_type, const namespacet &ns)