class_identifier.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Extract class identifier
 
Author: Chris Smowton, [email protected]
 
\*******************************************************************/
 
 
#include "class_identifier.h"
 
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
 
static exprt build_class_identifier(
  const exprt &src,
  const namespacet &ns)
{
  // the class identifier is in the root class
  exprt e=src;
 
  while(1)
  {
    const struct_typet &struct_type =
      ns.follow_tag(to_struct_tag_type(e.type()));
    const struct_typet::componentst &components=struct_type.components();
    INVARIANT(!components.empty(), "class structs cannot be empty");
 
    const auto &first_member_name=components.front().get_name();
    member_exprt member_expr(
      e,
      first_member_name,
      components.front().type());
 
    if(first_member_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME)
    {
      // found it
      return std::move(member_expr);
    }
    else
    {
      e.swap(member_expr);
    }
  }
}
 
exprt get_class_identifier_field(
  const exprt &this_expr_in,
  const struct_tag_typet &suggested_type,
  const namespacet &ns)
{
  // Get a pointer from which we can extract a clsid.
  // If it's already a pointer to an object of some sort, just use it;
  // if it's void* then use the suggested type.
  PRECONDITION(this_expr_in.type().id() == ID_pointer);
 
  exprt this_expr=this_expr_in;
  const auto &points_to = to_pointer_type(this_expr.type()).base_type();
  if(points_to==empty_typet())
    this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
  const dereference_exprt deref{this_expr};
  return build_class_identifier(deref, ns);
}
 
void set_class_identifier(
  struct_exprt &expr,
  const namespacet &ns,
  const struct_tag_typet &class_type)
{
  const struct_typet &struct_type =
    ns.follow_tag(to_struct_tag_type(expr.type()));
  const struct_typet::componentst &components=struct_type.components();
 
  if(components.empty())
    // Presumably this means the type has not yet been determined
    return;
  PRECONDITION(!expr.operands().empty());
 
  if(components.front().get_name() == JAVA_CLASS_IDENTIFIER_FIELD_NAME)
  {
    INVARIANT(expr.op0().is_constant(), "@class_identifier must be a constant");
    expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
  }
  else
  {
    // The first member must be the base class
    INVARIANT(
      expr.op0().id()==ID_struct, "Non @class_identifier must be a structure");
    set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
  }
}