cprover
java_pointer_casts.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Pointer Casts
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "java_pointer_casts.h"
13
14#include <util/expr_util.h>
15#include <util/namespace.h>
16#include <util/pointer_expr.h>
17#include <util/std_expr.h>
18
19#include "java_types.h"
20
23static 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
73 const exprt &rawptr,
74 const pointer_typet &target_type,
75 const namespacet &ns)
76{
77 const exprt &ptr = skip_typecast(rawptr);
78
79 PRECONDITION(ptr.type().id()==ID_pointer);
80
81 if(ptr.type()==target_type)
82 return ptr;
83
84 if(
86 target_type.base_type() == java_void_type())
87 {
88 return typecast_exprt(ptr, target_type);
89 }
90
91 const typet &target_base = ns.follow(target_type.base_type());
92
93 exprt bare_ptr=ptr;
94 while(bare_ptr.id()==ID_typecast)
95 {
96 assert(
97 bare_ptr.type().id()==ID_pointer &&
98 "Non-pointer in make_clean_pointer_cast?");
99 if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
100 bare_ptr = to_typecast_expr(bare_ptr).op();
101 }
102
103 assert(
104 bare_ptr.type().id()==ID_pointer &&
105 "Non-pointer in make_clean_pointer_cast?");
106
107 if(bare_ptr.type()==target_type)
108 return bare_ptr;
109
110 exprt superclass_ptr=bare_ptr;
111 // Looking at base types discards generic qualifiers (because those are
112 // recorded on the pointer, not the pointee), so it may still be necessary
113 // to use a cast to reintroduce the qualifier (for example, the base might
114 // be recorded as a List, when we're looking for a List<E>)
115 if(find_superclass_with_type(superclass_ptr, target_base, ns))
116 return typecast_exprt::conditional_cast(superclass_ptr, target_type);
117
118 return typecast_exprt(bare_ptr, target_type);
119}
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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:396
Extract member of struct or union.
Definition: std_expr.h:2667
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
const exprt & op() const
Definition: std_expr.h:293
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
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)
JAVA Pointer Casts.
empty_typet java_void_type()
Definition: java_types.cpp:37
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:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308