cprover
lambda_synthesis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java lambda code synthesis
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #include "lambda_synthesis.h"
13 
16 #include "java_types.h"
17 #include "java_utils.h"
18 #include "synthetic_methods_map.h"
19 
20 #include <util/message.h>
21 #include <util/namespace.h>
22 #include <util/prefix.h>
23 #include <util/symbol_table.h>
24 
25 #include <string.h>
26 
27 static std::string escape_symbol_special_chars(std::string input)
28 {
29  for(auto &c : input)
30  {
31  if(c == '$' || c == ':' || c == '.')
32  c = '_';
33  }
34  return input;
35 }
36 
38  const irep_idt &method_identifier,
39  std::size_t instruction_address)
40 {
41  return "java::lambda_synthetic_class$" +
43  id2string(strip_java_namespace_prefix(method_identifier))) +
44  "$" + std::to_string(instruction_address);
45 }
46 
55  const symbol_table_baset &symbol_table,
56  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
57  const size_t index)
58 {
59  // Check if we don't have enough bootstrap methods to satisfy the requested
60  // lambda. This could happen if we fail to parse one of the methods, or if
61  // the class type is partly or entirely synthetic, such as the types created
62  // internally by the string solver.
63  if(index >= lambda_method_handles.size())
64  return {};
65  const irept &lambda_method_handle = lambda_method_handles.at(index);
66  // If the lambda method handle has an unknown type, it does not refer to
67  // any symbol (it has an empty identifier)
68  if(!lambda_method_handle.id().empty())
69  return symbol_table.lookup_ref(lambda_method_handle.id());
70  return {};
71 }
72 
74  const symbol_tablet &symbol_table,
75  const irep_idt &method_identifier,
76  const java_method_typet &dynamic_method_type)
77 {
78  const namespacet ns{symbol_table};
79  const auto &method_symbol = ns.lookup(method_identifier);
80  const auto &declaring_class_symbol =
81  ns.lookup(*declaring_class(method_symbol));
82 
83  const auto &class_type = to_java_class_type(declaring_class_symbol.type);
84  const auto &lambda_method_handles = class_type.lambda_method_handles();
85  auto lambda_handle_index =
86  dynamic_method_type.get_int(ID_java_lambda_method_handle_index);
87  const auto lambda_method_symbol = get_lambda_method_symbol(
88  symbol_table, lambda_method_handles, lambda_handle_index);
89  if(lambda_method_symbol)
90  return lambda_method_symbol->name;
91  return {};
92 }
93 
95  const symbol_tablet &symbol_table,
96  const struct_tag_typet &functional_interface_tag,
97  const irep_idt &method_identifier,
98  const int instruction_address,
99  const messaget &log)
100 {
101  const namespacet ns{symbol_table};
102  const java_class_typet &implemented_interface_type = [&] {
103  const symbolt &implemented_interface_symbol =
104  ns.lookup(functional_interface_tag.get_identifier());
105  return to_java_class_type(implemented_interface_symbol.type);
106  }();
107 
108  if(implemented_interface_type.get_is_stub())
109  {
110  log.debug() << "ignoring invokedynamic at " << method_identifier
111  << " address " << instruction_address
112  << " which produces a stub type "
113  << functional_interface_tag.get_identifier() << messaget::eom;
114  return {};
115  }
116  else if(implemented_interface_type.methods().size() != 1)
117  {
118  log.debug()
119  << "ignoring invokedynamic at " << method_identifier << " address "
120  << instruction_address << " which produces type "
121  << functional_interface_tag.get_identifier()
122  << " which should have exactly one abstract method but actually has "
123  << implemented_interface_type.methods().size()
124  << ". Note default methods are not supported yet."
125  << "Also note methods declared in an inherited interface are not "
126  << "supported either." << messaget::eom;
127  return {};
128  }
129  return implemented_interface_type.methods().at(0).get_name();
130 }
131 
133  const irep_idt &synthetic_class_name,
135  const struct_tag_typet &functional_interface_tag,
136  const java_method_typet &dynamic_method_type)
137 {
138  java_class_typet synthetic_class_type;
139  // Tag = name without 'java::' prefix, matching the convention used by
140  // java_bytecode_convert_class.cpp
141  synthetic_class_type.set_tag(
142  strip_java_namespace_prefix(synthetic_class_name));
143  synthetic_class_type.set_name(synthetic_class_name);
144  synthetic_class_type.set_synthetic(true);
145  synthetic_class_type.set(
146  ID_java_lambda_method_identifier, lambda_method_name);
147  struct_tag_typet base_tag("java::java.lang.Object");
148  synthetic_class_type.add_base(base_tag);
149  synthetic_class_type.add_base(functional_interface_tag);
150 
151  // Add the class fields:
152 
153  {
154  java_class_typet::componentt base_field;
155  const irep_idt base_field_name("@java.lang.Object");
156  base_field.set_name(base_field_name);
157  base_field.set_base_name(base_field_name);
158  base_field.set_pretty_name(base_field_name);
159  base_field.set_access(ID_private);
160  base_field.type() = base_tag;
161  synthetic_class_type.components().emplace_back(std::move(base_field));
162 
163  std::size_t field_idx = 0;
164  for(const auto &param : dynamic_method_type.parameters())
165  {
166  irep_idt field_basename = "capture_" + std::to_string(field_idx++);
167 
169  new_field.set_name(field_basename);
170  new_field.set_base_name(field_basename);
171  new_field.set_pretty_name(field_basename);
172  new_field.set_access(ID_private);
173  new_field.type() = param.type();
174  synthetic_class_type.components().emplace_back(std::move(new_field));
175  }
176  }
177 
178  symbolt synthetic_class_symbol = type_symbolt{synthetic_class_type};
179  synthetic_class_symbol.name = synthetic_class_name;
180  synthetic_class_symbol.mode = ID_java;
181  return synthetic_class_symbol;
182 }
183 
185  synthetic_methods_mapt &synthetic_methods,
186  const irep_idt &synthetic_class_name,
187  java_method_typet constructor_type) // dynamic_method_type
188 {
190  irep_idt constructor_name = id2string(synthetic_class_name) + ".<init>";
191  constructor_symbol.name = constructor_name;
193  constructor_symbol.base_name = "<init>";
194  constructor_symbol.mode = ID_java;
195 
196  synthetic_methods[constructor_name] =
198 
199  constructor_type.set_is_constructor();
200  constructor_type.return_type() = empty_typet();
201 
202  size_t field_idx = 0;
203  for(auto &param : constructor_type.parameters())
204  {
205  irep_idt param_basename = "param_" + std::to_string(field_idx++);
206  param.set_base_name(param_basename);
207  param.set_identifier(
208  id2string(constructor_name) + "::" + id2string(param_basename));
209  }
210 
211  java_method_typet::parametert constructor_this_param;
212  constructor_this_param.set_this();
213  constructor_this_param.set_base_name("this");
214  constructor_this_param.set_identifier(id2string(constructor_name) + "::this");
215  constructor_this_param.type() =
216  java_reference_type(struct_tag_typet(synthetic_class_name));
217 
218  constructor_type.parameters().insert(
219  constructor_type.parameters().begin(), constructor_this_param);
220 
221  constructor_symbol.type = constructor_type;
222  set_declaring_class(constructor_symbol, synthetic_class_name);
223  return constructor_symbol;
224 }
225 
227  synthetic_methods_mapt &synthetic_methods,
228  const symbolt &interface_method_symbol,
229  const struct_tag_typet &functional_interface_tag,
230  const irep_idt &synthetic_class_name)
231 {
232  const std::string implemented_method_name = [&] {
233  std::string implemented_method_name =
234  id2string(interface_method_symbol.name);
235  const std::string &functional_interface_tag_str =
236  id2string(functional_interface_tag.get_identifier());
237  INVARIANT(
238  has_prefix(implemented_method_name, functional_interface_tag_str),
239  "method names should be prefixed by their defining type");
240  implemented_method_name.replace(
241  0,
242  functional_interface_tag_str.length(),
243  id2string(synthetic_class_name));
244  return implemented_method_name;
245  }();
246 
248  implemented_method_symbol.name = implemented_method_name;
249  synthetic_methods[implemented_method_symbol.name] =
252  implemented_method_symbol.base_name = interface_method_symbol.base_name;
254  implemented_method_symbol.type = interface_method_symbol.type;
255  auto &implemented_method_type = to_code_type(implemented_method_symbol.type);
256  implemented_method_type.parameters()[0].type() =
257  java_reference_type(struct_tag_typet(synthetic_class_name));
258 
259  size_t field_idx = 0;
260  for(auto &param : implemented_method_type.parameters())
261  {
262  irep_idt param_basename =
263  field_idx == 0 ? "this" : "param_" + std::to_string(field_idx);
264  param.set_base_name(param_basename);
265  param.set_identifier(
266  id2string(implemented_method_name) + "::" + id2string(param_basename));
267 
268  ++field_idx;
269  }
270 
271  set_declaring_class(implemented_method_symbol, synthetic_class_name);
273 }
274 
275 // invokedynamic will be called with operands that should be stored in a
276 // synthetic object implementing the interface type that it returns. For
277 // example, "invokedynamic f(a, b, c) -> MyInterface" should result in the
278 // creation of the synthetic class:
279 // public class SyntheticCapture implements MyInterface {
280 // private int a;
281 // private float b;
282 // private Other c;
283 // public SyntheticCapture(int a, float b, Other c) {
284 // this.a = a; this.b = b; this.c = c;
285 // }
286 // public void myInterfaceMethod(int d) {
287 // f(a, b, c, d);
288 // }
289 // }
290 // This method just creates the outline; the methods will be populated on
291 // demand via java_bytecode_languaget::convert_lazy_method.
292 
293 // Check that we understand the lambda method handle; if we don't then
294 // we will not create a synthetic class at all, and the corresponding
295 // invoke instruction will return null when eventually converted by
296 // java_bytecode_convert_method.
298  const irep_idt &method_identifier,
300  symbol_tablet &symbol_table,
301  synthetic_methods_mapt &synthetic_methods,
302  message_handlert &message_handler)
303 {
304  const messaget log{message_handler};
305 
306  for(const auto &instruction : instructions)
307  {
308  if(strcmp(bytecode_info[instruction.bytecode].mnemonic, "invokedynamic"))
309  continue;
310  const auto &dynamic_method_type =
311  to_java_method_type(instruction.args.at(0).type());
313  symbol_table, method_identifier, dynamic_method_type);
314  if(!lambda_method_name)
315  {
316  log.debug() << "ignoring invokedynamic at " << method_identifier
317  << " address " << instruction.address
318  << " with unknown handle type" << messaget::eom;
319  continue;
320  }
321  const auto &functional_interface_tag = to_struct_tag_type(
322  to_java_reference_type(dynamic_method_type.return_type()).subtype());
324  symbol_table,
325  functional_interface_tag,
326  method_identifier,
327  instruction.address,
328  log);
330  continue;
331  log.debug() << "identified invokedynamic at " << method_identifier
332  << " address " << instruction.address
333  << " for lambda: " << *lambda_method_name << messaget::eom;
334  const irep_idt synthetic_class_name =
335  lambda_synthetic_class_name(method_identifier, instruction.address);
336  symbol_table.add(constructor_symbol(
337  synthetic_methods, synthetic_class_name, dynamic_method_type));
338  symbol_table.add(implemented_method_symbol(
339  synthetic_methods,
340  symbol_table.lookup_ref(*interface_method_id),
341  functional_interface_tag,
342  synthetic_class_name));
343  symbol_table.add(synthetic_class_symbol(
344  synthetic_class_name,
346  functional_interface_tag,
347  dynamic_method_type));
348  }
349 }
350 
352  const irep_idt &identifier,
353  const irep_idt &base_name,
354  const irep_idt &pretty_name,
355  const typet &type,
356  const irep_idt &declaring_class,
357  symbol_table_baset &symbol_table,
358  message_handlert &log)
359 {
360  const auto *existing_symbol = symbol_table.lookup(identifier);
361  if(existing_symbol)
362  return *existing_symbol;
363 
365  identifier,
366  base_name,
367  pretty_name,
368  type,
370  symbol_table,
371  log);
372  return symbol_table.lookup_ref(identifier);
373 }
374 
376  const irep_idt &function_id,
377  symbol_table_baset &symbol_table,
378  message_handlert &message_handler)
379 {
380  code_blockt result;
381  namespacet ns(symbol_table);
382 
383  const symbolt &function_symbol = ns.lookup(function_id);
384  const auto &parameters = to_code_type(function_symbol.type).parameters();
385 
386  const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
387  const class_typet &class_type = to_class_type(class_symbol.type);
388 
389  const symbol_exprt this_param(
390  parameters.at(0).get_identifier(), parameters.at(0).type());
391  const dereference_exprt deref_this(this_param);
392 
393  // Call super-constructor (always java.lang.Object):
394  const irep_idt jlo("java::java.lang.Object");
395  const irep_idt jlo_constructor(id2string(jlo) + ".<init>:()V");
396  const auto jlo_reference = java_reference_type(struct_tag_typet(jlo));
397  code_typet::parametert jlo_this_param{jlo_reference};
398  jlo_this_param.set_this();
399 
400  java_method_typet jlo_constructor_type(
401  code_typet::parameterst{jlo_this_param}, empty_typet());
402  const auto &jlo_constructor_symbol = get_or_create_method_symbol(
403  jlo_constructor,
404  "<init>",
405  jlo_constructor,
406  jlo_constructor_type,
407  jlo,
408  symbol_table,
409  message_handler);
410  code_function_callt super_constructor_call(
411  jlo_constructor_symbol.symbol_expr(),
412  code_function_callt::argumentst{typecast_exprt(this_param, jlo_reference)});
413  result.add(super_constructor_call);
414 
415  // Store captured parameters:
416  auto field_iterator = std::next(class_type.components().begin());
417  for(const auto &parameter : parameters)
418  {
419  // Give the parameter its symbol:
420  parameter_symbolt param_symbol;
421  param_symbol.name = parameter.get_identifier();
422  param_symbol.base_name = parameter.get_base_name();
423  param_symbol.mode = ID_java;
424  param_symbol.type = parameter.type();
425  symbol_table.add(param_symbol);
426 
427  if(parameter.get_this())
428  continue;
429 
430  code_assignt assign_field(
431  member_exprt(deref_this, field_iterator->get_name(), parameter.type()),
432  symbol_exprt(parameter.get_identifier(), parameter.type()));
433  result.add(assign_field);
434 
435  ++field_iterator;
436  }
437 
438  return std::move(result);
439 }
440 
442  const irep_idt &function_id,
443  symbol_table_baset &symbol_table,
444  message_handlert &message_handler)
445 {
446  // Call the bound method with the capture parameters, then the actual
447  // parameters. Note one of the capture params might be the `this` parameter
448  // of a virtual call -- that depends on whether the callee is a static or an
449  // instance method.
450 
451  code_blockt result;
452  namespacet ns(symbol_table);
453 
454  const symbolt &function_symbol = ns.lookup(function_id);
455  const auto &function_type = to_code_type(function_symbol.type);
456  const auto &parameters = function_type.parameters();
457  const auto &return_type = function_type.return_type();
458 
459  const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
460  const java_class_typet &class_type = to_java_class_type(class_symbol.type);
461 
462  const symbol_exprt this_param(
463  parameters.at(0).get_identifier(), parameters.at(0).type());
464  const dereference_exprt deref_this(this_param);
465 
466  code_function_callt::argumentst lambda_method_args;
467  for(const auto &field : class_type.components())
468  {
469  if(field.get_name() == "@java.lang.Object")
470  continue;
471  lambda_method_args.push_back(
472  member_exprt(deref_this, field.get_name(), field.type()));
473  }
474 
475  for(const auto &parameter : parameters)
476  {
477  // Give the parameter its symbol:
478  parameter_symbolt param_symbol;
479  param_symbol.name = parameter.get_identifier();
480  param_symbol.base_name = parameter.get_base_name();
481  param_symbol.mode = ID_java;
482  param_symbol.type = parameter.type();
483  symbol_table.add(param_symbol);
484 
485  if(parameter.get_this())
486  continue;
487 
488  lambda_method_args.push_back(param_symbol.symbol_expr());
489  }
490 
491  const auto &lambda_method_symbol =
492  ns.lookup(class_type.get(ID_java_lambda_method_identifier));
493 
494  if(return_type != empty_typet())
495  {
497  lambda_method_symbol.symbol_expr(),
498  lambda_method_args,
499  return_type,
500  source_locationt())));
501  }
502  else
503  {
504  result.add(code_function_callt(
505  lambda_method_symbol.symbol_expr(), lambda_method_args));
506  }
507 
508  return std::move(result);
509 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:173
irept::get_int
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:69
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_class_typet::componentt
Definition: java_types.h:202
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
class_typet
Class type.
Definition: std_types.h:320
invokedynamic_synthetic_method
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic method.
Definition: lambda_synthesis.cpp:441
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:89
java_class_typet::set_synthetic
void set_synthetic(bool synthetic)
marks class synthetic
Definition: java_types.h:424
set_declaring_class
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
Definition: java_utils.cpp:506
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:91
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:376
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2917
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2127
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:782
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
create_invokedynamic_synthetic_classes
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
Definition: lambda_synthesis.cpp:297
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:500
prefix.h
synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.
synthetic_method_typet::INVOKEDYNAMIC_METHOD
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:283
java_class_typet::methods
const methodst & methods() const
Definition: java_types.h:290
lambda_method_name
static optionalt< irep_idt > lambda_method_name(const symbol_tablet &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
Definition: lambda_synthesis.cpp:73
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:199
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:338
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
implemented_method_symbol
symbolt implemented_method_symbol(synthetic_methods_mapt &synthetic_methods, const symbolt &interface_method_symbol, const struct_tag_typet &functional_interface_tag, const irep_idt &synthetic_class_name)
Definition: lambda_synthesis.cpp:226
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_reference_typet::subtype
struct_tag_typet & subtype()
Definition: java_types.h:557
empty_typet
The empty type.
Definition: std_types.h:46
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
code_typet::set_is_constructor
void set_is_constructor()
Definition: std_types.h:892
java_bytecode_parse_tree.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
to_java_reference_type
const java_reference_typet & to_java_reference_type(const typet &type)
Definition: java_types.h:575
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:27
create_method_stub_symbol
void create_method_stub_symbol(const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition: java_bytecode_convert_method.cpp:99
java_bytecode_convert_method.h
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1195
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:211
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
escape_symbol_special_chars
static std::string escape_symbol_special_chars(std::string input)
Definition: lambda_synthesis.cpp:27
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:787
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:807
java_class_typet::java_lambda_method_handlest
irept::subt java_lambda_method_handlest
Definition: java_types.h:465
source_locationt
Definition: source_location.h:20
invokedynamic_synthetic_constructor
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
Definition: lambda_synthesis.cpp:375
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3434
lambda_synthesis.h
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1313
get_lambda_method_symbol
static optionalt< symbolt > get_lambda_method_symbol(const symbol_table_baset &symbol_table, const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
Definition: lambda_synthesis.cpp:54
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
synthetic_class_symbol
symbolt synthetic_class_symbol(const irep_idt &synthetic_class_name, const irep_idt &lambda_method_name, const struct_tag_typet &functional_interface_tag, const java_method_typet &dynamic_method_type)
Definition: lambda_synthesis.cpp:132
code_typet::parametert
Definition: std_types.h:753
java_class_typet::set_name
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:509
type_symbolt
Symbol table entry describing a data type.
Definition: symbol.h:146
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
constructor_symbol
static symbolt constructor_symbol(synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type)
Definition: lambda_synthesis.cpp:184
get_or_create_method_symbol
static const symbolt & get_or_create_method_symbol(const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &log)
Definition: lambda_synthesis.cpp:351
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:527
messaget::debug
mstreamt & debug() const
Definition: message.h:415
parameter_symbolt
Symbol table entry of function parameter.
Definition: symbol.h:184
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
java_types.h
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:388
symbol_table.h
Author: Diffblue Ltd.
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:298
message.h
java_utils.h
java_method_typet
Definition: java_types.h:103
lambda_synthetic_class_name
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
Definition: lambda_synthesis.cpp:37
synthetic_methods_map.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
interface_method_id
static optionalt< irep_idt > interface_method_id(const symbol_tablet &symbol_table, const struct_tag_typet &functional_interface_tag, const irep_idt &method_identifier, const int instruction_address, const messaget &log)
Definition: lambda_synthesis.cpp:94