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/pointer_expr.h>
16 #include <util/std_expr.h>
17 
19 {
20  assert(symbol.type.id()==ID_struct);
21 
22  // builds virtual-table value maps: (class x virtual_name x value)
23  std::map<irep_idt, std::map<irep_idt, exprt> > vt_value_maps;
24 
25  const struct_typet &struct_type=to_struct_type(symbol.type);
26 
27  for(std::size_t i=0; i < struct_type.components().size(); i++)
28  {
29  const struct_typet::componentt &compo=struct_type.components()[i];
30  if(!compo.get_bool(ID_is_virtual))
31  continue;
32 
33  const code_typet &code_type=to_code_type(compo.type());
34  assert(code_type.parameters().size() > 0);
35 
36  const pointer_typet &parameter_pointer_type=
37  to_pointer_type(code_type.parameters()[0].type());
38 
39  const irep_idt &class_id =
40  parameter_pointer_type.subtype().get(ID_identifier);
41 
42  std::map<irep_idt, exprt> &value_map =
43  vt_value_maps[class_id];
44 
45  exprt e=symbol_exprt(compo.get_name(), code_type);
46 
47  if(compo.get_bool(ID_is_pure_virtual))
48  {
49  pointer_typet code_pointer_type=pointer_type(code_type);
50  e=null_pointer_exprt(code_pointer_type);
51  value_map[compo.get(ID_virtual_name)] = e;
52  }
53  else
54  {
55  address_of_exprt address(e);
56  value_map[compo.get(ID_virtual_name)] = address;
57  }
58  }
59 
60  // create virtual-table symbol variables
61  for(std::map<irep_idt, std::map<irep_idt, exprt> >::const_iterator cit =
62  vt_value_maps.begin(); cit!=vt_value_maps.end(); cit++)
63  {
64  const std::map<irep_idt, exprt> &value_map=cit->second;
65 
66  const symbolt &late_cast_symb = lookup(cit->first);
67  const symbolt &vt_symb_type =
68  lookup("virtual_table::" + id2string(late_cast_symb.name));
69 
70  symbolt vt_symb_var;
71  vt_symb_var.name=
72  id2string(vt_symb_type.name) + "@"+ id2string(symbol.name);
73  vt_symb_var.base_name=
74  id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
75  vt_symb_var.mode = symbol.mode;
76  vt_symb_var.module=module;
77  vt_symb_var.location=vt_symb_type.location;
78  vt_symb_var.type = struct_tag_typet(vt_symb_type.name);
79  vt_symb_var.is_lvalue=true;
80  vt_symb_var.is_static_lifetime=true;
81 
82  // do the values
83  const struct_typet &vt_type=to_struct_type(vt_symb_type.type);
84 
85  struct_exprt values({}, struct_tag_typet(vt_symb_type.name));
86 
87  for(const auto &compo : vt_type.components())
88  {
89  std::map<irep_idt, exprt>::const_iterator cit2 =
90  value_map.find(compo.get_base_name());
91  assert(cit2!=value_map.end());
92  const exprt &value=cit2->second;
93  assert(value.type()==compo.type());
94  values.operands().push_back(value);
95  }
96  vt_symb_var.value=values;
97 
98  bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
100  }
101 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Operator to return the address of an object.
Definition: pointer_expr.h:200
symbol_tablet & symbol_table
const irep_idt module
Base type of functions.
Definition: std_types.h:744
const parameterst & parameters() const
Definition: std_types.h:860
void do_virtual_table(const symbolt &symbol)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
std::string::const_iterator begin() const
Definition: dstring.h:176
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
The null pointer constant.
Definition: std_expr.h:2751
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
Struct constructor from list of elements.
Definition: std_expr.h:1583
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:498
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const irep_idt & get_name() const
Definition: std_types.h:74
const componentst & components() const
Definition: std_types.h:142
Expression to hold a symbol (variable)
Definition: std_expr.h:81
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
const typet & subtype() const
Definition: type.h:47
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
static bool failed(bool error_indicator)