cprover
Loading...
Searching...
No Matches
cpp_typecheck_virtual_table.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include <util/c_types.h>
13#include <util/pointer_expr.h>
14#include <util/std_expr.h>
16
17#include "cpp_typecheck.h"
18
20{
21 PRECONDITION(symbol.type.id() == ID_struct);
22
23 // builds virtual-table value maps: (class x virtual_name x value)
24 std::map<irep_idt, std::map<irep_idt, exprt> > vt_value_maps;
25
26 const struct_typet &struct_type=to_struct_type(symbol.type);
27
28 for(std::size_t i=0; i < struct_type.components().size(); i++)
29 {
30 const struct_typet::componentt &compo=struct_type.components()[i];
31 if(!compo.get_bool(ID_is_virtual))
32 continue;
33
34 const code_typet &code_type=to_code_type(compo.type());
35 DATA_INVARIANT(code_type.parameters().size() > 0, "parameters expected");
36
37 const pointer_typet &parameter_pointer_type=
38 to_pointer_type(code_type.parameters()[0].type());
39
40 const irep_idt &class_id =
41 parameter_pointer_type.base_type().get(ID_identifier);
42
43 std::map<irep_idt, exprt> &value_map =
44 vt_value_maps[class_id];
45
46 exprt e=symbol_exprt(compo.get_name(), code_type);
47
48 if(compo.get_bool(ID_is_pure_virtual))
49 {
50 pointer_typet code_pointer_type=pointer_type(code_type);
51 e=null_pointer_exprt(code_pointer_type);
52 value_map[compo.get(ID_virtual_name)] = e;
53 }
54 else
55 {
56 address_of_exprt address(e);
57 value_map[compo.get(ID_virtual_name)] = address;
58 }
59 }
60
61 // create virtual-table symbol variables
62 for(std::map<irep_idt, std::map<irep_idt, exprt> >::const_iterator cit =
63 vt_value_maps.begin(); cit!=vt_value_maps.end(); cit++)
64 {
65 const std::map<irep_idt, exprt> &value_map=cit->second;
66
67 const symbolt &late_cast_symb = lookup(cit->first);
68 const symbolt &vt_symb_type =
69 lookup("virtual_table::" + id2string(late_cast_symb.name));
70
71 symbolt vt_symb_var{
72 id2string(vt_symb_type.name) + "@" + id2string(symbol.name),
73 struct_tag_typet(vt_symb_type.name),
74 symbol.mode};
75 vt_symb_var.base_name=
76 id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
77 vt_symb_var.module=module;
78 vt_symb_var.location=vt_symb_type.location;
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 CHECK_RETURN(cit2 != value_map.end());
92 const exprt &value=cit2->second;
93 DATA_INVARIANT(value.type() == compo.type(), "component type mismatch");
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:235
Operator to return the address of an object.
symbol_table_baset & symbol_table
Base type of functions.
Definition std_types.h:583
const parameterst & parameters() const
Definition std_types.h:699
void do_virtual_table(const symbolt &symbol)
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Struct constructor from list of elements.
Definition std_expr.h:1877
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
const irep_idt & get_name() const
Definition std_types.h:79
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:70
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:72
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
Author: Diffblue Ltd.
static bool failed(bool error_indicator)
dstringt irep_idt