cprover
cpp_typecheck_virtual_table.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #include <util/c_types.h>
15 #include <util/std_expr.h>
16 
18 {
19  assert(symbol.type.id()==ID_struct);
20 
21  // builds virtual-table value maps: (class x virtual_name x value)
22  std::map<irep_idt, std::map<irep_idt, exprt> > vt_value_maps;
23 
24  const struct_typet &struct_type=to_struct_type(symbol.type);
25 
26  for(std::size_t i=0; i < struct_type.components().size(); i++)
27  {
28  const struct_typet::componentt &compo=struct_type.components()[i];
29  if(!compo.get_bool("is_virtual"))
30  continue;
31 
32  const code_typet &code_type=to_code_type(compo.type());
33  assert(code_type.parameters().size() > 0);
34 
35  const pointer_typet &parameter_pointer_type=
36  to_pointer_type(code_type.parameters()[0].type());
37 
38  irep_idt class_id=parameter_pointer_type.subtype().get("identifier");
39 
40  std::map<irep_idt, exprt> &value_map =
41  vt_value_maps[class_id];
42 
43  exprt e=symbol_exprt(compo.get_name(), code_type);
44 
45  if(compo.get_bool("is_pure_virtual"))
46  {
47  pointer_typet code_pointer_type=pointer_type(code_type);
48  e=null_pointer_exprt(code_pointer_type);
49  value_map[compo.get("virtual_name")]=e;
50  }
51  else
52  {
53  address_of_exprt address(e);
54  value_map[compo.get("virtual_name")]=address;
55  }
56  }
57 
58  // create virtual-table symbol variables
59  for(std::map<irep_idt, std::map<irep_idt, exprt> >::const_iterator cit =
60  vt_value_maps.begin(); cit!=vt_value_maps.end(); cit++)
61  {
62  const std::map<irep_idt, exprt> &value_map=cit->second;
63 
64  const symbolt &late_cast_symb = lookup(cit->first);
65  const symbolt &vt_symb_type =
66  lookup("virtual_table::" + id2string(late_cast_symb.name));
67 
68  symbolt vt_symb_var;
69  vt_symb_var.name=
70  id2string(vt_symb_type.name) + "@"+ id2string(symbol.name);
71  vt_symb_var.base_name=
72  id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
73  vt_symb_var.mode=ID_cpp;
74  vt_symb_var.module=module;
75  vt_symb_var.location=vt_symb_type.location;
76  vt_symb_var.type=symbol_typet(vt_symb_type.name);
77  vt_symb_var.is_lvalue=true;
78  vt_symb_var.is_static_lifetime=true;
79 
80  // do the values
81  const struct_typet &vt_type=to_struct_type(vt_symb_type.type);
82 
83  struct_exprt values(symbol_typet(vt_symb_type.name));
84 
85  for(std::size_t i=0; i < vt_type.components().size(); i++)
86  {
87  const struct_typet::componentt &compo=vt_type.components()[i];
88  std::map<irep_idt, exprt>::const_iterator cit2 =
89  value_map.find(compo.get("base_name"));
90  assert(cit2!=value_map.end());
91  const exprt &value=cit2->second;
92  assert(value.type()==compo.type());
93  values.operands().push_back(value);
94  }
95  vt_symb_var.value=values;
96 
97  bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
98  CHECK_RETURN(!failed);
99  }
100 }
const irep_idt & get_name() const
Definition: std_types.h:182
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
The null pointer constant.
Definition: std_expr.h:4520
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool is_static_lifetime
Definition: symbol.h:67
symbol_tablet & symbol_table
const irep_idt & id() const
Definition: irep.h:189
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1426
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void do_virtual_table(const symbolt &symbol)
C++ Language Type Checking.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Operator to return the address of an object.
Definition: std_expr.h:3170
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const irep_idt module
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
operandst & operands()
Definition: expr.h:66
struct constructor from list of elements
Definition: std_expr.h:1815
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
bool is_lvalue
Definition: symbol.h:68