cprover
class_identifier.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Extract class identifier
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "class_identifier.h"
13 
14 #include <util/std_expr.h>
15 #include <util/c_types.h>
16 #include <util/namespace.h>
17 
22  const exprt &src,
23  const namespacet &ns)
24 {
25  // the class identifier is in the root class
26  exprt e=src;
27 
28  while(1)
29  {
30  const typet &type=ns.follow(e.type());
31  const struct_typet &struct_type=to_struct_type(type);
32  const struct_typet::componentst &components=struct_type.components();
33  INVARIANT(!components.empty(), "class structs cannot be empty");
34 
35  const auto &first_member_name=components.front().get_name();
36  member_exprt member_expr(
37  e,
38  first_member_name,
39  components.front().type());
40 
41  if(first_member_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME)
42  {
43  // found it
44  return std::move(member_expr);
45  }
46  else
47  {
48  e.swap(member_expr);
49  }
50  }
51 }
52 
57  const exprt &this_expr_in,
58  const struct_tag_typet &suggested_type,
59  const namespacet &ns)
60 {
61  // Get a pointer from which we can extract a clsid.
62  // If it's already a pointer to an object of some sort, just use it;
63  // if it's void* then use the suggested type.
64  PRECONDITION(this_expr_in.type().id() == ID_pointer);
65 
66  exprt this_expr=this_expr_in;
67  const auto &points_to=this_expr.type().subtype();
68  if(points_to==empty_typet())
69  this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
70  const dereference_exprt deref{this_expr};
71  return build_class_identifier(deref, ns);
72 }
73 
83  struct_exprt &expr,
84  const namespacet &ns,
85  const struct_tag_typet &class_type)
86 {
87  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
88  const struct_typet::componentst &components=struct_type.components();
89 
90  if(components.empty())
91  // Presumably this means the type has not yet been determined
92  return;
93  PRECONDITION(!expr.operands().empty());
94 
95  if(components.front().get_name() == JAVA_CLASS_IDENTIFIER_FIELD_NAME)
96  {
97  INVARIANT(
98  expr.op0().id()==ID_constant, "@class_identifier must be a constant");
99  expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
100  }
101  else
102  {
103  // The first member must be the base class
104  INVARIANT(
105  expr.op0().id()==ID_struct, "Non @class_identifier must be a structure");
106  set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
107  }
108 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
typet::subtype
const typet & subtype() const
Definition: type.h:47
JAVA_CLASS_IDENTIFIER_FIELD_NAME
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Definition: class_identifier.h:20
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
get_class_identifier_field
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Definition: class_identifier.cpp:56
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
namespace.h
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1633
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
set_class_identifier
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Definition: class_identifier.cpp:82
empty_typet
The empty type.
Definition: std_types.h:46
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
build_class_identifier
static exprt build_class_identifier(const exprt &src, const namespacet &ns)
Definition: class_identifier.cpp:21
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
string_typet
String type.
Definition: std_types.h:1655
class_identifier.h
Extract class identifier.
exprt::operands
operandst & operands()
Definition: expr.h:95
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
std_expr.h
API to expression classes.
c_types.h
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656