cprover
ci_lazy_methods_needed.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Context-insensitive lazy methods container
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ci_lazy_methods.h"
13 
15 #include <string>
16 #include <util/namespace.h>
17 #include <util/std_types.h>
18 
23  const irep_idt &method_symbol_name)
24 {
25  callable_methods.insert(method_symbol_name);
26 }
27 
34  const irep_idt &class_symbol_name)
35 {
36  if(!instantiated_classes.insert(class_symbol_name).second)
37  return false;
38 
39  const std::string &class_name_string = id2string(class_symbol_name);
40  const irep_idt cprover_validate(
41  class_name_string + ".cproverNondetInitialize:()V");
42  if(symbol_table.symbols.count(cprover_validate))
43  add_needed_method(cprover_validate);
44 
45  return true;
46 }
47 
53 {
55 
57 
58  // TODO we should be passing here a map that maps generic parameters
59  // to concrete types in the current context TG-2664
60  const pointer_typet &subbed_pointer_type =
62 
63  if(subbed_pointer_type != pointer_type)
64  {
65  initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns);
66  }
67 }
68 
75  const namespacet &ns)
76 {
77  const symbol_typet &class_type = to_symbol_type(pointer_type.subtype());
78  const auto &param_classid = class_type.get_identifier();
79 
80  // Note here: different arrays may have different element types, so we should
81  // explore again even if we've seen this classid before in the array case.
82  if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
83  {
85  }
86 
88  {
89  // Assume if this is a generic like X<A, B, C>, then any concrete parameters
90  // will at some point be instantiated.
91  const auto &generic_args =
93  for(const auto &generic_arg : generic_args)
94  {
95  if(!is_java_generic_parameter(generic_arg))
96  {
98  }
99  }
100  }
101 }
102 
107  const typet &class_type,
108  const namespacet &ns)
109 {
110  const auto &underlying_type = to_struct_type(ns.follow(class_type));
111  if(is_java_array_tag(underlying_type.get_tag()))
112  {
113  // If class_type is not a symbol this may be a reference array,
114  // but we can't tell what type.
115  if(class_type.id() == ID_symbol)
116  {
117  const typet &element_type =
119  if(element_type.id() == ID_pointer)
120  {
121  // This is a reference array -- mark its element type available.
123  }
124  }
125  }
126  else
127  {
128  for(const auto &field : underlying_type.components())
129  {
130  if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
131  gather_field_types(field.type(), ns);
132  else if(field.type().id() == ID_pointer)
133  {
134  if(field.type().subtype().id() == ID_symbol)
135  {
137  }
138  else
139  {
140  // If raw structs were possible this would lead to missed
141  // dependencies, as both array element and specialised generic type
142  // information cannot be obtained in this case.
143  // We should therefore only be skipping pointers such as the uint16t*
144  // in our internal String representation.
145  INVARIANT(
146  field.type().subtype().id() != ID_struct,
147  "struct types should be referred to by symbol at this stage");
148  }
149  }
150  }
151  }
152 }
The type of an expression.
Definition: type.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. ...
Definition: java_types.h:281
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:137
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const select_pointer_typet & pointer_type_selector
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:330
const irep_idt & id() const
Definition: irep.h:189
std::unordered_set< irep_idt > & instantiated_classes
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1426
Collect methods needed to be loaded using the lazy method.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
const symbolst & symbols
void initialize_instantiated_classes_from_pointer(const pointer_typet &pointer_type, const namespacet &ns)
Build up list of methods for types for a specific pointer type.
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:353
API to type classes.
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
Definition: java_types.cpp:126
std::unordered_set< irep_idt > & callable_methods
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced...
bool is_java_generic_type(const typet &type)
Definition: java_types.h:346
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
const typet & subtype() const
Definition: type.h:33
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
const irep_idt & get_identifier() const
Definition: std_types.h:123