cprover
java_bytecode_convert_method.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifdef DEBUG
13 #include <iostream>
14 #endif
15 
16 #include "bytecode_info.h"
19 #include "java_expr.h"
23 #include "java_types.h"
24 #include "java_utils.h"
25 #include "lambda_synthesis.h"
26 #include "pattern.h"
27 #include "remove_exceptions.h"
28 
29 #include <util/arith_tools.h>
30 #include <util/c_types.h>
31 #include <util/expr_initializer.h>
32 #include <util/ieee_float.h>
33 #include <util/invariant.h>
34 #include <util/namespace.h>
35 #include <util/prefix.h>
36 #include <util/simplify_expr.h>
37 #include <util/std_expr.h>
38 #include <util/string2int.h>
39 #include <util/threeval.h>
40 
41 #include <goto-programs/cfg.h>
45 
48 
49 #include <algorithm>
50 #include <functional>
51 #include <limits>
52 #include <regex>
53 #include <unordered_set>
54 
68  java_method_typet &ftype,
69  const irep_idt &name_prefix,
70  symbol_table_baset &symbol_table)
71 {
72  java_method_typet::parameterst &parameters = ftype.parameters();
73 
74  // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out.
75  // assign names to parameters
76  for(std::size_t i=0; i<parameters.size(); ++i)
77  {
78  irep_idt base_name, identifier;
79 
80  if(i==0 && parameters[i].get_this())
81  base_name = ID_this;
82  else
83  base_name="stub_ignored_arg"+std::to_string(i);
84 
85  identifier=id2string(name_prefix)+"::"+id2string(base_name);
86  parameters[i].set_base_name(base_name);
87  parameters[i].set_identifier(identifier);
88 
89  // add to symbol table
90  parameter_symbolt parameter_symbol;
91  parameter_symbol.base_name=base_name;
92  parameter_symbol.mode=ID_java;
93  parameter_symbol.name=identifier;
94  parameter_symbol.type=parameters[i].type();
95  symbol_table.add(parameter_symbol);
96  }
97 }
98 
100  const irep_idt &identifier,
101  const irep_idt &base_name,
102  const irep_idt &pretty_name,
103  const typet &type,
104  const irep_idt &declaring_class,
105  symbol_table_baset &symbol_table,
106  message_handlert &message_handler)
107 {
108  messaget log(message_handler);
109 
110  symbolt symbol;
111  symbol.name = identifier;
112  symbol.base_name = base_name;
113  symbol.pretty_name = pretty_name;
114  symbol.type = type;
115  symbol.type.set(ID_access, ID_private);
116  to_java_method_type(symbol.type).set_is_final(true);
117  symbol.value.make_nil();
118  symbol.mode = ID_java;
120  to_java_method_type(symbol.type), symbol.name, symbol_table);
122 
123  log.debug() << "Generating codet: new opaque symbol: method '" << symbol.name
124  << "'" << messaget::eom;
125  symbol_table.add(symbol);
126 }
127 
128 static bool is_constructor(const irep_idt &method_name)
129 {
130  return id2string(method_name).find("<init>") != std::string::npos;
131 }
132 
134 {
135  if(stack.size()<n)
136  {
137  error() << "malformed bytecode (pop too high)" << eom;
138  throw 0;
139  }
140 
141  exprt::operandst operands;
142  operands.resize(n);
143  for(std::size_t i=0; i<n; i++)
144  operands[i]=stack[stack.size()-n+i];
145 
146  stack.resize(stack.size()-n);
147  return operands;
148 }
149 
152 {
153  std::size_t residue_size=std::min(n, stack.size());
154 
155  stack.resize(stack.size()-residue_size);
156 }
157 
159 {
160  stack.resize(stack.size()+o.size());
161 
162  for(std::size_t i=0; i<o.size(); i++)
163  stack[stack.size()-o.size()+i]=o[i];
164 }
165 
166 // JVM program locations
168 {
169  return "pc"+id2string(address);
170 }
171 
173  const std::string &prefix,
174  const typet &type)
175 {
176  irep_idt base_name=prefix+"_tmp"+std::to_string(tmp_vars.size());
177  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
178 
179  auxiliary_symbolt tmp_symbol;
180  tmp_symbol.base_name=base_name;
181  tmp_symbol.is_static_lifetime=false;
182  tmp_symbol.mode=ID_java;
183  tmp_symbol.name=identifier;
184  tmp_symbol.type=type;
185  symbol_table.add(tmp_symbol);
186 
187  symbol_exprt result(identifier, type);
188  result.set(ID_C_base_name, base_name);
189  tmp_vars.push_back(result);
190 
191  return result;
192 }
193 
206  const exprt &arg,
207  char type_char,
208  size_t address)
209 {
210  const std::size_t number_int =
211  numeric_cast_v<std::size_t>(to_constant_expr(arg));
212  variablest &var_list=variables[number_int];
213 
214  // search variable in list for correct frame / address if necessary
215  const variablet &var=
216  find_variable_for_slot(address, var_list);
217 
218  if(!var.symbol_expr.get_identifier().empty())
219  return var.symbol_expr;
220 
221  // an unnamed local variable
222  irep_idt base_name = "anonlocal::" + std::to_string(number_int) + type_char;
223  irep_idt identifier = id2string(current_method) + "::" + id2string(base_name);
224 
225  symbol_exprt result(identifier, java_type_from_char(type_char));
226  result.set(ID_C_base_name, base_name);
227  used_local_names.insert(result);
228  return std::move(result);
229 }
230 
239  const std::string &descriptor,
240  const optionalt<std::string> &signature,
241  const std::string &class_name,
242  const std::string &method_name,
243  message_handlert &message_handler)
244 {
245  // In order to construct the method type, we can either use signature or
246  // descriptor. Since only signature contains the generics info, we want to
247  // use signature whenever possible. We revert to using descriptor if (1) the
248  // signature does not exist, (2) an unsupported generics are present or
249  // (3) in the special case when the number of parameters in the descriptor
250  // does not match the number of parameters in the signature - e.g. for
251  // certain types of inner classes and enums (see unit tests for examples).
252 
253  messaget message(message_handler);
254 
255  auto member_type_from_descriptor = java_type_from_string(descriptor);
256  INVARIANT(
257  member_type_from_descriptor.has_value() &&
258  member_type_from_descriptor->id() == ID_code,
259  "Must be code type");
260  if(signature.has_value())
261  {
262  try
263  {
264  auto member_type_from_signature =
265  java_type_from_string(signature.value(), class_name);
266  INVARIANT(
267  member_type_from_signature.has_value() &&
268  member_type_from_signature->id() == ID_code,
269  "Must be code type");
270  if(
271  to_java_method_type(*member_type_from_signature).parameters().size() ==
272  to_java_method_type(*member_type_from_descriptor).parameters().size())
273  {
274  return to_java_method_type(*member_type_from_signature);
275  }
276  else
277  {
278  message.debug() << "Method: " << class_name << "." << method_name
279  << "\n signature: " << signature.value()
280  << "\n descriptor: " << descriptor
281  << "\n different number of parameters, reverting to "
282  "descriptor"
283  << message.eom;
284  }
285  }
287  {
288  message.debug() << "Method: " << class_name << "." << method_name
289  << "\n could not parse signature: " << signature.value()
290  << "\n " << e.what() << "\n"
291  << " reverting to descriptor: " << descriptor
292  << message.eom;
293  }
294  }
295  return to_java_method_type(*member_type_from_descriptor);
296 }
297 
309  symbolt &class_symbol,
310  const irep_idt &method_identifier,
312  symbol_tablet &symbol_table,
313  message_handlert &message_handler)
314 {
315  symbolt method_symbol;
316 
317  java_method_typet member_type = member_type_lazy(
318  m.descriptor,
319  m.signature,
320  id2string(class_symbol.name),
321  id2string(m.base_name),
322  message_handler);
323 
324  method_symbol.name=method_identifier;
325  method_symbol.base_name=m.base_name;
326  method_symbol.mode=ID_java;
327  method_symbol.location=m.source_location;
328  method_symbol.location.set_function(method_identifier);
329 
330  if(m.is_public)
331  member_type.set_access(ID_public);
332  else if(m.is_protected)
333  member_type.set_access(ID_protected);
334  else if(m.is_private)
335  member_type.set_access(ID_private);
336  else
337  member_type.set_access(ID_default);
338 
339  if(m.is_synchronized)
340  member_type.set(ID_is_synchronized, true);
341  if(m.is_static)
342  member_type.set(ID_is_static, true);
343  member_type.set_native(m.is_native);
344  member_type.set_is_varargs(m.is_varargs);
345  member_type.set_is_synthetic(m.is_synthetic);
346 
347  if(m.is_bridge)
348  member_type.set(ID_is_bridge_method, m.is_bridge);
349 
350  // do we need to add 'this' as a parameter?
351  if(!m.is_static)
352  {
353  java_method_typet::parameterst &parameters = member_type.parameters();
354  const reference_typet object_ref_type =
356  java_method_typet::parametert this_p(object_ref_type);
357  this_p.set_this();
358  parameters.insert(parameters.begin(), this_p);
359  }
360 
361  const std::string signature_string = pretty_signature(member_type);
362 
363  if(is_constructor(method_symbol.base_name))
364  {
365  // we use full.class_name(...) as pretty name
366  // for constructors -- the idea is that they have
367  // an empty declarator.
368  method_symbol.pretty_name=
369  id2string(class_symbol.pretty_name) + signature_string;
370 
371  member_type.set_is_constructor();
372  }
373  else
374  {
375  method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
376  id2string(m.base_name) + signature_string;
377  }
378 
379  // Load annotations
380  if(!m.annotations.empty())
381  {
383  m.annotations,
384  type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
385  .get_annotations());
386  }
387 
388  method_symbol.type=member_type;
389  // Not used in jbmc at present, but other codebases that use jbmc as a library
390  // use this information.
391  method_symbol.type.set(ID_C_abstract, m.is_abstract);
392  set_declaring_class(method_symbol, class_symbol.name);
393 
395  m.annotations, "java::org.cprover.MustNotThrow"))
396  {
397  method_symbol.type.set(ID_C_must_not_throw, true);
398  }
399 
400  // Assign names to parameters in the method symbol
401  java_method_typet &method_type = to_java_method_type(method_symbol.type);
402  method_type.set_is_final(m.is_final);
403  java_method_typet::parameterst &parameters = method_type.parameters();
404  java_bytecode_convert_methodt::method_offsett slots_for_parameters =
405  java_method_parameter_slots(method_type);
407  m, method_identifier, parameters, slots_for_parameters);
408 
409  symbol_table.add(method_symbol);
410 
411  if(!m.is_static)
412  {
413  java_class_typet::methodt new_method{method_symbol.name, method_type};
414  new_method.set_base_name(method_symbol.base_name);
415  new_method.set_pretty_name(method_symbol.pretty_name);
416  new_method.set_access(member_type.get_access());
417  new_method.set_descriptor(m.descriptor);
418 
419  to_java_class_type(class_symbol.type)
420  .methods()
421  .emplace_back(std::move(new_method));
422  }
423 }
424 
426  const irep_idt &class_identifier,
428 {
429  return
430  id2string(class_identifier) + "." + id2string(method.name) + ":" +
431  method.descriptor;
432 }
433 
436  const irep_idt &method_identifier,
437  java_method_typet::parameterst &parameters,
438  const java_bytecode_convert_methodt::method_offsett &slots_for_parameters)
439 {
440  auto variables = variablest{};
441  // Find parameter names in the local variable table
442  // and store the result in the external variables vector
443  for(const auto &v : m.local_variable_table)
444  {
445  // Skip this variable if it is not a method parameter
446  if(v.index >= slots_for_parameters)
447  continue;
448 
449  std::ostringstream id_oss;
450  id_oss << method_identifier << "::" << v.name;
451  irep_idt identifier(id_oss.str());
452  symbol_exprt result = symbol_exprt::typeless(identifier);
453  result.set(ID_C_base_name, v.name);
454 
455  // Create a new variablet in the variables vector; in fact this entry will
456  // be rewritten below in the loop that iterates through the method
457  // parameters; the only field that seem to be useful to write here is the
458  // symbol_expr, others will be rewritten
459  variables[v.index].emplace_back(result, v.start_pc, v.length);
460  }
461 
462  // The variables is a expanding_vectort, and the loop above may have expanded
463  // the vector introducing gaps where the entries are empty vectors. We now
464  // make sure that the vector of each LV slot contains exactly one variablet,
465  // which we will add below
466  std::size_t param_index = 0;
467  for(const auto &param : parameters)
468  {
469  INVARIANT(
470  variables[param_index].size() <= 1,
471  "should have at most one entry per index");
472  param_index += java_local_variable_slots(param.type());
473  }
474  INVARIANT(
475  param_index == slots_for_parameters,
476  "java_parameter_count and local computation must agree");
477  param_index = 0;
478  for(auto &param : parameters)
479  {
480  irep_idt base_name, identifier;
481 
482  // Construct a sensible base name (base_name) and a fully qualified name
483  // (identifier) for every parameter of the method under translation,
484  // regardless of whether we have an LVT or not; and assign it to the
485  // parameter object (which is stored in the type of the symbol, not in the
486  // symbol table)
487  if(param_index == 0 && param.get_this())
488  {
489  // my.package.ClassName.myMethodName:(II)I::this
490  base_name = ID_this;
491  identifier = id2string(method_identifier) + "::" + id2string(base_name);
492  }
493  else if(!variables[param_index].empty())
494  {
495  // if already present in the LVT ...
496  base_name = variables[param_index][0].symbol_expr.get(ID_C_base_name);
497  identifier = variables[param_index][0].symbol_expr.get(ID_identifier);
498  }
499  else
500  {
501  // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
502  // variable slot where the parameter is stored and T is a character
503  // indicating the type
504  char suffix = java_char_from_type(param.type());
505  base_name = "arg" + std::to_string(param_index) + suffix;
506  identifier = id2string(method_identifier) + "::" + id2string(base_name);
507  }
508  param.set_base_name(base_name);
509  param.set_identifier(identifier);
510  param_index += java_local_variable_slots(param.type());
511  }
512  // The parameter slots detected in this function should agree with what
513  // java_parameter_count() thinks about this method
514  INVARIANT(
515  param_index == slots_for_parameters,
516  "java_parameter_count and local computation must agree");
517 }
518 
520  const java_method_typet::parameterst &parameters,
521  expanding_vectort<std::vector<java_bytecode_convert_methodt::variablet>>
522  &variables,
523  symbol_table_baset &symbol_table)
524 {
525  std::size_t param_index = 0;
526  for(const auto &param : parameters)
527  {
528  parameter_symbolt parameter_symbol;
529  parameter_symbol.base_name = param.get_base_name();
530  parameter_symbol.mode = ID_java;
531  parameter_symbol.name = param.get_identifier();
532  parameter_symbol.type = param.type();
533  symbol_table.add(parameter_symbol);
534 
535  // Add as a JVM local variable
536  variables[param_index].clear();
537  variables[param_index].emplace_back(
538  parameter_symbol.symbol_expr(),
539  0,
540  std::numeric_limits<size_t>::max(),
541  true);
542  param_index += java_local_variable_slots(param.type());
543  }
544 }
545 
547  const symbolt &class_symbol,
548  const methodt &m,
549  const optionalt<prefix_filtert> &method_context)
550 {
551  // Construct the fully qualified method name
552  // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
553  // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
554  // associated to the method
555  const irep_idt method_identifier =
556  get_method_identifier(class_symbol.name, m);
557 
558  method_id = method_identifier;
560  symbol_table.get_writeable_ref(method_identifier), class_symbol.name);
561 
562  // Obtain a std::vector of java_method_typet::parametert objects from the
563  // (function) type of the symbol
564  // Don't try to hang on to this reference into the symbol table, as we're
565  // about to create symbols for the method's parameters, which would invalidate
566  // the reference. Instead, copy the type here, set it up, then assign it back
567  // to the symbol later.
568  java_method_typet method_type =
569  to_java_method_type(symbol_table.lookup_ref(method_identifier).type);
570  method_type.set_is_final(m.is_final);
571  method_return_type = method_type.return_type();
572  java_method_typet::parameterst &parameters = method_type.parameters();
573 
574  // Determine the number of local variable slots used by the JVM to maintain
575  // the formal parameters
577 
578  debug() << "Generating codet: class " << class_symbol.name << ", method "
579  << m.name << eom;
580 
581  // Add parameter symbols to the symbol table
583 
584  symbolt &method_symbol = symbol_table.get_writeable_ref(method_identifier);
585 
586  // Check the fields that can't change are valid
587  INVARIANT(
588  method_symbol.name == method_identifier,
589  "Name of method symbol shouldn't change");
590  INVARIANT(
591  method_symbol.base_name == m.base_name,
592  "Base name of method symbol shouldn't change");
593  INVARIANT(
594  method_symbol.module.empty(),
595  "Method symbol shouldn't have module");
596  // Update the symbol for the method
597  method_symbol.mode=ID_java;
598  method_symbol.location=m.source_location;
599  method_symbol.location.set_function(method_identifier);
600 
601  for(const auto &exception_name : m.throws_exception_table)
602  method_type.add_throws_exception(exception_name);
603 
604  const std::string signature_string = pretty_signature(method_type);
605 
606  // Set up the pretty name for the method entry in the symbol table.
607  // The pretty name of a constructor includes the base name of the class
608  // instead of the internal method name "<init>". For regular methods, it's
609  // just the base name of the method.
610  if(is_constructor(method_symbol.base_name))
611  {
612  // we use full.class_name(...) as pretty name
613  // for constructors -- the idea is that they have
614  // an empty declarator.
615  method_symbol.pretty_name =
616  id2string(class_symbol.pretty_name) + signature_string;
617  INVARIANT(
618  method_type.get_is_constructor(),
619  "Member type should have already been marked as a constructor");
620  }
621  else
622  {
623  method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
624  id2string(m.base_name) + signature_string;
625  }
626 
627  method_symbol.type = method_type;
628  current_method = method_symbol.name;
629  method_has_this = method_type.has_this();
630  if((!m.is_abstract) && (!m.is_native))
631  {
632  // Do not convert if method is not in context
633  if(!method_context || (*method_context)(id2string(method_identifier)))
634  {
635  code_blockt code{convert_parameter_annotations(m, method_type)};
636  code.append(convert_instructions(m));
637  method_symbol.value = std::move(code);
638  }
639  }
640 }
641 
642 static irep_idt get_if_cmp_operator(const u1 bytecode)
643 {
644  if(bytecode == patternt("if_?cmplt"))
645  return ID_lt;
646  if(bytecode == patternt("if_?cmple"))
647  return ID_le;
648  if(bytecode == patternt("if_?cmpgt"))
649  return ID_gt;
650  if(bytecode == patternt("if_?cmpge"))
651  return ID_ge;
652  if(bytecode == patternt("if_?cmpeq"))
653  return ID_equal;
654  if(bytecode == patternt("if_?cmpne"))
655  return ID_notequal;
656 
657  throw "unhandled java comparison instruction";
658 }
659 
669  const exprt &pointer,
670  const fieldref_exprt &field_reference,
671  const namespacet &ns)
672 {
673  struct_tag_typet class_type(field_reference.class_name());
674 
675  const exprt typed_pointer =
677 
678  const irep_idt &component_name = field_reference.component_name();
679 
680  exprt accessed_object = checked_dereference(typed_pointer);
681  const auto type_of = [&ns](const exprt &object) {
682  return to_struct_type(ns.follow(object.type()));
683  };
684 
685  // The field access is described as being against a particular type, but it
686  // may in fact belong to any ancestor type.
687  while(type_of(accessed_object).get_component(component_name).is_nil())
688  {
689  const auto components = type_of(accessed_object).components();
690  INVARIANT(
691  components.size() != 0,
692  "infer_opaque_type_fields should guarantee that a member access has a "
693  "corresponding field");
694 
695  // Base class access is always done through the first component
696  accessed_object = member_exprt(accessed_object, components.front());
697  }
698  return member_exprt(
699  accessed_object, type_of(accessed_object).get_component(component_name));
700 }
701 
708  codet &repl,
709  const irep_idt &old_label,
710  const irep_idt &new_label)
711 {
712  const auto &stmt=repl.get_statement();
713  if(stmt==ID_goto)
714  {
715  auto &g=to_code_goto(repl);
716  if(g.get_destination()==old_label)
717  g.set_destination(new_label);
718  }
719  else
720  {
721  for(auto &op : repl.operands())
722  if(op.id()==ID_code)
723  replace_goto_target(to_code(op), old_label, new_label);
724  }
725 }
726 
742  block_tree_nodet &tree,
743  code_blockt &this_block,
744  method_offsett address_start,
745  method_offsett address_limit,
746  method_offsett next_block_start_address)
747 {
748  address_mapt dummy;
750  tree,
751  this_block,
752  address_start,
753  address_limit,
754  next_block_start_address,
755  dummy,
756  false);
757 }
758 
779  block_tree_nodet &tree,
780  code_blockt &this_block,
781  method_offsett address_start,
782  method_offsett address_limit,
783  method_offsett next_block_start_address,
784  const address_mapt &amap,
785  bool allow_merge)
786 {
787  // Check the tree shape invariant:
788  assert(tree.branch.size()==tree.branch_addresses.size());
789 
790  // If there are no child blocks, return this.
791  if(tree.leaf)
792  return this_block;
793  assert(!tree.branch.empty());
794 
795  // Find child block starting > address_start:
796  const auto afterstart=
797  std::upper_bound(
798  tree.branch_addresses.begin(),
799  tree.branch_addresses.end(),
800  address_start);
801  assert(afterstart!=tree.branch_addresses.begin());
802  auto findstart=afterstart;
803  --findstart;
804  auto child_offset=
805  std::distance(tree.branch_addresses.begin(), findstart);
806 
807  // Find child block starting >= address_limit:
808  auto findlim=
809  std::lower_bound(
810  tree.branch_addresses.begin(),
811  tree.branch_addresses.end(),
812  address_limit);
813  const auto findlim_block_start_address =
814  findlim == tree.branch_addresses.end() ? next_block_start_address
815  : (*findlim);
816 
817  // If all children are in scope, return this.
818  if(findstart==tree.branch_addresses.begin() &&
819  findlim==tree.branch_addresses.end())
820  return this_block;
821 
822  // Find the child code_blockt where the queried range begins:
823  auto child_iter = this_block.statements().begin();
824  // Skip any top-of-block declarations;
825  // all other children are labelled subblocks.
826  while(child_iter != this_block.statements().end() &&
827  child_iter->get_statement() == ID_decl)
828  ++child_iter;
829  assert(child_iter != this_block.statements().end());
830  std::advance(child_iter, child_offset);
831  assert(child_iter != this_block.statements().end());
832  auto &child_label=to_code_label(*child_iter);
833  auto &child_block=to_code_block(child_label.code());
834 
835  bool single_child(afterstart==findlim);
836  if(single_child)
837  {
838  // Range wholly contained within a child block
840  tree.branch[child_offset],
841  child_block,
842  address_start,
843  address_limit,
844  findlim_block_start_address,
845  amap,
846  allow_merge);
847  }
848 
849  // Otherwise we're being asked for a range of subblocks, but not all of them.
850  // If it's legal to draw a new lexical scope around the requested subset,
851  // do so; otherwise just return this block.
852 
853  // This can be a new lexical scope if all incoming edges target the
854  // new block header, or come from within the suggested new block.
855 
856  // If modifying the block tree is forbidden, give up and return this:
857  if(!allow_merge)
858  return this_block;
859 
860  // Check for incoming control-flow edges targeting non-header
861  // blocks of the new proposed block range:
862  auto checkit=amap.find(*findstart);
863  assert(checkit!=amap.end());
864  ++checkit; // Skip the header, which can have incoming edges from outside.
865  for(;
866  checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
867  ++checkit)
868  {
869  for(auto p : checkit->second.predecessors)
870  {
871  if(p<(*findstart) || p>=findlim_block_start_address)
872  {
873  debug() << "Generating codet: "
874  << "warning: refusing to create lexical block spanning "
875  << (*findstart) << "-" << findlim_block_start_address
876  << " due to incoming edge " << p << " -> "
877  << checkit->first << eom;
878  return this_block;
879  }
880  }
881  }
882 
883  // All incoming edges are acceptable! Create a new block wrapping
884  // the relevant children. Borrow the header block's label, and redirect
885  // any block-internal edges to target the inner header block.
886 
887  const irep_idt child_label_name=child_label.get_label();
888  std::string new_label_str = id2string(child_label_name);
889  new_label_str+='$';
890  irep_idt new_label_irep(new_label_str);
891 
892  code_labelt newlabel(child_label_name, code_blockt());
893  code_blockt &newblock=to_code_block(newlabel.code());
894  auto nblocks=std::distance(findstart, findlim);
895  assert(nblocks>=2);
896  debug() << "Generating codet: combining "
897  << std::distance(findstart, findlim)
898  << " blocks for addresses " << (*findstart) << "-"
899  << findlim_block_start_address << eom;
900 
901  // Make a new block containing every child of interest:
902  auto &this_block_children = this_block.statements();
903  assert(tree.branch.size()==this_block_children.size());
904  for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
905  blockidx!=blocklim;
906  ++blockidx)
907  newblock.add(this_block_children[blockidx]);
908 
909  // Relabel the inner header:
910  to_code_label(newblock.statements()[0]).set_label(new_label_irep);
911  // Relabel internal gotos:
912  replace_goto_target(newblock, child_label_name, new_label_irep);
913 
914  // Remove the now-empty sibling blocks:
915  auto delfirst=this_block_children.begin();
916  std::advance(delfirst, child_offset+1);
917  auto dellim=delfirst;
918  std::advance(dellim, nblocks-1);
919  this_block_children.erase(delfirst, dellim);
920  this_block_children[child_offset].swap(newlabel);
921 
922  // Perform the same transformation on the index tree:
923  block_tree_nodet newnode;
924  auto branchstart=tree.branch.begin();
925  std::advance(branchstart, child_offset);
926  auto branchlim=branchstart;
927  std::advance(branchlim, nblocks);
928  for(auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
929  newnode.branch.push_back(std::move(*branchiter));
930  ++branchstart;
931  tree.branch.erase(branchstart, branchlim);
932 
933  assert(tree.branch.size()==this_block_children.size());
934 
935  auto branchaddriter=tree.branch_addresses.begin();
936  std::advance(branchaddriter, child_offset);
937  auto branchaddrlim=branchaddriter;
938  std::advance(branchaddrlim, nblocks);
939  newnode.branch_addresses.insert(
940  newnode.branch_addresses.begin(),
941  branchaddriter,
942  branchaddrlim);
943 
944  ++branchaddriter;
945  tree.branch_addresses.erase(branchaddriter, branchaddrlim);
946 
947  tree.branch[child_offset]=std::move(newnode);
948 
949  assert(tree.branch.size()==tree.branch_addresses.size());
950 
951  return
954  this_block_children[child_offset]).code());
955 }
956 
959  const exprt &e,
960  std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
961 {
962  if(e.id()==ID_symbol)
963  {
964  const auto &symexpr=to_symbol_expr(e);
965  auto findit = result.emplace(
966  std::piecewise_construct,
967  std::forward_as_tuple(symexpr.get_identifier()),
968  std::forward_as_tuple(symexpr, pc, 1));
969  if(!findit.second)
970  {
971  auto &var = findit.first->second;
972 
973  if(pc<var.start_pc)
974  {
975  var.length+=(var.start_pc-pc);
976  var.start_pc=pc;
977  }
978  else
979  {
980  var.length=std::max(var.length, (pc-var.start_pc)+1);
981  }
982  }
983  }
984  else
985  {
986  forall_operands(it, e)
987  gather_symbol_live_ranges(pc, *it, result);
988  }
989 }
990 
997  const irep_idt &classname)
998 {
999  auto findit = symbol_table.symbols.find(clinit_wrapper_name(classname));
1000  if(findit == symbol_table.symbols.end())
1001  return code_skipt();
1002  else
1003  {
1004  const code_function_callt ret(findit->second.symbol_expr());
1006  needed_lazy_methods->add_needed_method(findit->second.name);
1007  return ret;
1008  }
1009 }
1010 
1011 static std::size_t get_bytecode_type_width(const typet &ty)
1012 {
1013  if(ty.id()==ID_pointer)
1014  return 32;
1015  return to_bitvector_type(ty).get_width();
1016 }
1017 
1019  const methodt &method,
1020  const java_method_typet &method_type)
1021 {
1022  code_blockt code;
1023 
1024  // Consider parameter annotations
1025  const java_method_typet::parameterst &parameters(method_type.parameters());
1026  std::size_t param_index = method_type.has_this() ? 1 : 0;
1028  parameters.size() >= method.parameter_annotations.size() + param_index,
1029  "parameters and parameter annotations mismatch");
1030  for(const auto &param_annotations : method.parameter_annotations)
1031  {
1032  // NotNull annotations are not standardized. We support these:
1033  if(
1035  param_annotations, "java::javax.validation.constraints.NotNull") ||
1037  param_annotations, "java::org.jetbrains.annotations.NotNull") ||
1039  param_annotations, "org.eclipse.jdt.annotation.NonNull") ||
1041  param_annotations, "java::edu.umd.cs.findbugs.annotations.NonNull"))
1042  {
1043  const irep_idt &param_identifier =
1044  parameters[param_index].get_identifier();
1045  const symbolt &param_symbol = symbol_table.lookup_ref(param_identifier);
1046  const auto param_type =
1047  type_try_dynamic_cast<pointer_typet>(param_symbol.type);
1048  if(param_type)
1049  {
1050  code_assertt code_assert(notequal_exprt(
1051  param_symbol.symbol_expr(), null_pointer_exprt(*param_type)));
1052  source_locationt check_loc = method.source_location;
1053  check_loc.set_comment("Not null annotation check");
1054  check_loc.set_property_class("not-null-annotation-check");
1055  code_assert.add_source_location() = check_loc;
1056 
1057  code.add(std::move(code_assert));
1058  }
1059  }
1060  ++param_index;
1061  }
1062 
1063  return code;
1064 }
1065 
1068 {
1069  const instructionst &instructions=method.instructions;
1070 
1071  // Run a worklist algorithm, assuming that the bytecode has not
1072  // been tampered with. See "Leroy, X. (2003). Java bytecode
1073  // verification: algorithms and formalizations. Journal of Automated
1074  // Reasoning, 30(3-4), 235-269." for a more complete treatment.
1075 
1076  // first pass: get targets and map addresses to instructions
1077 
1078  address_mapt address_map;
1079  std::set<method_offsett> targets;
1080 
1081  std::vector<method_offsett> jsr_ret_targets;
1082  std::vector<instructionst::const_iterator> ret_instructions;
1083 
1084  for(auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1085  {
1087  std::pair<address_mapt::iterator, bool> a_entry=
1088  address_map.insert(std::make_pair(i_it->address, ins));
1089  assert(a_entry.second);
1090  // addresses are strictly increasing, hence we must have inserted
1091  // a new maximal key
1092  assert(a_entry.first==--address_map.end());
1093 
1094  const auto bytecode = i_it->bytecode;
1095  const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
1096 
1097  // clang-format off
1098  if(bytecode != BC_goto &&
1099  bytecode != BC_return &&
1100  bytecode != patternt("?return") &&
1101  bytecode != BC_athrow &&
1102  bytecode != BC_jsr &&
1103  bytecode != BC_jsr_w &&
1104  bytecode != BC_ret)
1105  {
1106  // clang-format on
1107  instructionst::const_iterator next=i_it;
1108  if(++next!=instructions.end())
1109  a_entry.first->second.successors.push_back(next->address);
1110  }
1111 
1112  // clang-format off
1113  if(bytecode == BC_athrow ||
1114  bytecode == BC_putfield ||
1115  bytecode == BC_getfield ||
1116  bytecode == BC_checkcast ||
1117  bytecode == BC_newarray ||
1118  bytecode == BC_anewarray ||
1119  bytecode == BC_idiv ||
1120  bytecode == BC_ldiv ||
1121  bytecode == BC_irem ||
1122  bytecode == BC_lrem ||
1123  bytecode == patternt("?astore") ||
1124  bytecode == patternt("?aload") ||
1125  bytecode == BC_invokestatic ||
1126  bytecode == BC_invokevirtual ||
1127  bytecode == BC_invokespecial ||
1128  bytecode == BC_invokeinterface ||
1129  (threading_support &&
1130  (bytecode == BC_monitorenter || bytecode == BC_monitorexit)))
1131  {
1132  // clang-format on
1133  const std::vector<method_offsett> handler =
1134  try_catch_handler(i_it->address, method.exception_table);
1135  std::list<method_offsett> &successors = a_entry.first->second.successors;
1136  successors.insert(successors.end(), handler.begin(), handler.end());
1137  targets.insert(handler.begin(), handler.end());
1138  }
1139 
1140  // clang-format off
1141  if(bytecode == BC_goto ||
1142  bytecode == patternt("if_?cmp??") ||
1143  bytecode == patternt("if??") ||
1144  bytecode == BC_ifnonnull ||
1145  bytecode == BC_ifnull ||
1146  bytecode == BC_jsr ||
1147  bytecode == BC_jsr_w)
1148  {
1149  // clang-format on
1150  PRECONDITION(!i_it->args.empty());
1151 
1152  auto target = numeric_cast_v<unsigned>(to_constant_expr(i_it->args[0]));
1153  targets.insert(target);
1154 
1155  a_entry.first->second.successors.push_back(target);
1156 
1157  if(bytecode == BC_jsr || bytecode == BC_jsr_w)
1158  {
1159  auto next = std::next(i_it);
1161  next != instructions.end(), "jsr should have valid return address");
1162  targets.insert(next->address);
1163  jsr_ret_targets.push_back(next->address);
1164  }
1165  }
1166  else if(bytecode == BC_tableswitch || bytecode == BC_lookupswitch)
1167  {
1168  bool is_label=true;
1169  for(const auto &arg : i_it->args)
1170  {
1171  if(is_label)
1172  {
1173  auto target = numeric_cast_v<unsigned>(to_constant_expr(arg));
1174  targets.insert(target);
1175  a_entry.first->second.successors.push_back(target);
1176  }
1177  is_label=!is_label;
1178  }
1179  }
1180  else if(bytecode == BC_ret)
1181  {
1182  // Finish these later, once we've seen all jsr instructions.
1183  ret_instructions.push_back(i_it);
1184  }
1185  }
1186  draw_edges_from_ret_to_jsr(address_map, jsr_ret_targets, ret_instructions);
1187 
1188  for(const auto &address : address_map)
1189  {
1190  for(auto s : address.second.successors)
1191  {
1192  const auto a_it = address_map.find(s);
1193  CHECK_RETURN(a_it != address_map.end());
1194  a_it->second.predecessors.insert(address.first);
1195  }
1196  }
1197 
1198  // Clean the list of temporary variables created by a call to `tmp_variable`.
1199  // These are local variables in the goto function used to represent temporary
1200  // values of the JVM operand stack, newly allocated objects before the
1201  // constructor is called, ...
1202  tmp_vars.clear();
1203 
1204  // Now that the control flow graph is built, set up our local variables
1205  // (these require the graph to determine live ranges)
1206  setup_local_variables(method, address_map);
1207 
1208  std::set<method_offsett> working_set;
1209 
1210  if(!instructions.empty())
1211  working_set.insert(instructions.front().address);
1212 
1213  while(!working_set.empty())
1214  {
1215  auto cur = working_set.begin();
1216  auto address_it = address_map.find(*cur);
1217  CHECK_RETURN(address_it != address_map.end());
1218  auto &instruction = address_it->second;
1219  const method_offsett cur_pc = *cur;
1220  working_set.erase(cur);
1221 
1222  if(instruction.done)
1223  continue;
1224  working_set.insert(
1225  instruction.successors.begin(), instruction.successors.end());
1226 
1227  instructionst::const_iterator i_it = instruction.source;
1228  stack.swap(instruction.stack);
1229  instruction.stack.clear();
1230  codet &c = instruction.code;
1231 
1232  assert(
1233  stack.empty() || instruction.predecessors.size() <= 1 ||
1234  has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
1235 
1236  exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
1237  exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
1238 
1239  const auto bytecode = i_it->bytecode;
1240  const bytecode_infot &stmt_bytecode_info = bytecode_info[i_it->bytecode];
1241  const std::string statement = stmt_bytecode_info.mnemonic;
1242 
1243  // deal with _idx suffixes
1244  if(statement.size()>=2 &&
1245  statement[statement.size()-2]=='_' &&
1246  isdigit(statement[statement.size()-1]))
1247  {
1248  arg0=
1249  from_integer(
1251  std::string(id2string(statement), statement.size()-1, 1)),
1252  java_int_type());
1253  }
1254 
1255  typet catch_type;
1256 
1257  // Find catch blocks that begin here. For now we assume if more than
1258  // one catch targets the same bytecode then we must be indifferent to
1259  // its type and just call it a Throwable.
1260  auto it=method.exception_table.begin();
1261  for(; it!=method.exception_table.end(); ++it)
1262  {
1263  if(cur_pc==it->handler_pc)
1264  {
1265  if(
1266  catch_type != typet() ||
1267  it->catch_type == struct_tag_typet(irep_idt()))
1268  {
1269  catch_type = struct_tag_typet("java::java.lang.Throwable");
1270  break;
1271  }
1272  else
1273  catch_type=it->catch_type;
1274  }
1275  }
1276 
1277  optionalt<codet> catch_instruction;
1278 
1279  if(catch_type!=typet())
1280  {
1281  // at the beginning of a handler, clear the stack and
1282  // push the corresponding exceptional return variable
1283  // We also create a catch exception instruction that
1284  // precedes the catch block, and which remove_exceptionst
1285  // will transform into something like:
1286  // catch_var = GLOBAL_THROWN_EXCEPTION;
1287  // GLOBAL_THROWN_EXCEPTION = null;
1288  stack.clear();
1289  symbol_exprt catch_var=
1290  tmp_variable(
1291  "caught_exception",
1292  java_reference_type(catch_type));
1293  stack.push_back(catch_var);
1294  catch_instruction = code_landingpadt(catch_var);
1295  }
1296 
1297  exprt::operandst op = pop(stmt_bytecode_info.pop);
1298  exprt::operandst results;
1299  results.resize(stmt_bytecode_info.push, nil_exprt());
1300 
1301  if(bytecode == BC_aconst_null)
1302  {
1303  assert(results.size()==1);
1305  }
1306  else if(bytecode == BC_athrow)
1307  {
1308  PRECONDITION(op.size() == 1 && results.size() == 1);
1309  convert_athrow(i_it->source_location, op, c, results);
1310  }
1311  else if(bytecode == BC_checkcast)
1312  {
1313  // checkcast throws an exception in case a cast of object
1314  // on stack to given type fails.
1315  // The stack isn't modified.
1316  PRECONDITION(op.size() == 1 && results.size() == 1);
1317  convert_checkcast(arg0, op, c, results);
1318  }
1319  else if(bytecode == BC_invokedynamic)
1320  {
1321  if(
1322  const auto res =
1323  convert_invoke_dynamic(i_it->source_location, i_it->address, arg0, c))
1324  {
1325  results.resize(1);
1326  results[0] = *res;
1327  }
1328  }
1329  else if(
1330  bytecode == BC_invokestatic && id2string(arg0.get(ID_identifier)) ==
1331  "java::org.cprover.CProver.assume:(Z)V")
1332  {
1333  const java_method_typet &method_type = to_java_method_type(arg0.type());
1334  INVARIANT(
1335  method_type.parameters().size() == 1,
1336  "function expected to have exactly one parameter");
1337  c = replace_call_to_cprover_assume(i_it->source_location, c);
1338  }
1339  // replace calls to CProver.atomicBegin
1340  else if(
1341  bytecode == BC_invokestatic &&
1342  arg0.get(ID_identifier) == "java::org.cprover.CProver.atomicBegin:()V")
1343  {
1344  c = codet(ID_atomic_begin);
1345  }
1346  // replace calls to CProver.atomicEnd
1347  else if(
1348  bytecode == BC_invokestatic &&
1349  arg0.get(ID_identifier) == "java::org.cprover.CProver.atomicEnd:()V")
1350  {
1351  c = codet(ID_atomic_end);
1352  }
1353  else if(
1354  bytecode == BC_invokeinterface || bytecode == BC_invokespecial ||
1355  bytecode == BC_invokevirtual || bytecode == BC_invokestatic)
1356  {
1357  class_method_descriptor_exprt *class_method_descriptor =
1358  expr_try_dynamic_cast<class_method_descriptor_exprt>(arg0);
1359 
1360  INVARIANT(
1361  class_method_descriptor,
1362  "invokeinterface, invokespecial, invokevirtual and invokestatic should "
1363  "be called with a class method descriptor expression as arg0");
1364 
1366  i_it->source_location, statement, *class_method_descriptor, c, results);
1367  }
1368  else if(bytecode == BC_return)
1369  {
1370  PRECONDITION(op.empty() && results.empty());
1371  c=code_returnt();
1372  }
1373  else if(bytecode == patternt("?return"))
1374  {
1375  // Return types are promoted in java, so this might need
1376  // conversion.
1377  PRECONDITION(op.size() == 1 && results.empty());
1378  const exprt r =
1380  c=code_returnt(r);
1381  }
1382  else if(bytecode == patternt("?astore"))
1383  {
1384  PRECONDITION(results.empty());
1385  c = convert_astore(statement, op, i_it->source_location);
1386  }
1387  else if(bytecode == patternt("?store") || bytecode == patternt("?store_?"))
1388  {
1389  // store value into some local variable
1390  PRECONDITION(op.size() == 1 && results.empty());
1391  c = convert_store(
1392  statement, arg0, op, i_it->address, i_it->source_location);
1393  }
1394  else if(bytecode == patternt("?aload"))
1395  {
1396  PRECONDITION(results.size() == 1);
1397  results[0] = convert_aload(statement, op);
1398  }
1399  else if(bytecode == patternt("?load") || bytecode == patternt("?load_?"))
1400  {
1401  // load a value from a local variable
1402  results[0] = convert_load(arg0, statement[0], i_it->address);
1403  }
1404  else if(bytecode == BC_ldc || bytecode == BC_ldc_w || bytecode == BC_ldc2_w)
1405  {
1406  PRECONDITION(op.empty() && results.size() == 1);
1407 
1408  INVARIANT(
1409  !can_cast_expr<java_string_literal_exprt>(arg0) && arg0.id() != ID_type,
1410  "String and Class literals should have been lowered in "
1411  "generate_constant_global_variables");
1412 
1413  results[0] = arg0;
1414  }
1415  else if(bytecode == BC_goto || bytecode == BC_goto_w)
1416  {
1417  PRECONDITION(op.empty() && results.empty());
1418  const mp_integer number =
1419  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1420  code_gotot code_goto(label(integer2string(number)));
1421  c=code_goto;
1422  }
1423  else if(bytecode == BC_jsr || bytecode == BC_jsr_w)
1424  {
1425  // As 'goto', except we must also push the subroutine return address:
1426  PRECONDITION(op.empty() && results.size() == 1);
1427  const mp_integer number =
1428  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1429  code_gotot code_goto(label(integer2string(number)));
1430  c=code_goto;
1431  results[0]=
1432  from_integer(
1433  std::next(i_it)->address,
1434  unsignedbv_typet(64));
1435  results[0].type() = pointer_type(java_void_type());
1436  }
1437  else if(bytecode == BC_ret)
1438  {
1439  // Since we have a bounded target set, make life easier on our analyses
1440  // and write something like:
1441  // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
1442  PRECONDITION(op.empty() && results.empty());
1443  assert(!jsr_ret_targets.empty());
1444  c = convert_ret(
1445  jsr_ret_targets, arg0, i_it->source_location, i_it->address);
1446  }
1447  else if(bytecode == BC_iconst_m1)
1448  {
1449  assert(results.size()==1);
1450  results[0]=from_integer(-1, java_int_type());
1451  }
1452  else if(bytecode == patternt("?const_?"))
1453  {
1454  assert(results.size()==1);
1455  results = convert_const(statement, to_constant_expr(arg0), results);
1456  }
1457  else if(bytecode == patternt("?ipush"))
1458  {
1459  PRECONDITION(results.size()==1);
1461  arg0.id()==ID_constant,
1462  "ipush argument expected to be constant");
1463  results[0] = typecast_exprt::conditional_cast(arg0, java_int_type());
1464  }
1465  else if(bytecode == patternt("if_?cmp??"))
1466  {
1467  PRECONDITION(op.size() == 2 && results.empty());
1468  const mp_integer number =
1469  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1470  c = convert_if_cmp(
1471  address_map, bytecode, op, number, i_it->source_location);
1472  }
1473  else if(bytecode == patternt("if??"))
1474  {
1475  // clang-format off
1476  const irep_idt id=
1477  bytecode == BC_ifeq ? ID_equal :
1478  bytecode == BC_ifne ? ID_notequal :
1479  bytecode == BC_iflt ? ID_lt :
1480  bytecode == BC_ifge ? ID_ge :
1481  bytecode == BC_ifgt ? ID_gt :
1482  bytecode == BC_ifle ? ID_le :
1483  irep_idt();
1484  // clang-format on
1485 
1486  INVARIANT(!id.empty(), "unexpected bytecode-if");
1487  PRECONDITION(op.size() == 1 && results.empty());
1488  const mp_integer number =
1489  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1490  c = convert_if(address_map, op, id, number, i_it->source_location);
1491  }
1492  else if(bytecode == patternt("ifnonnull"))
1493  {
1494  PRECONDITION(op.size() == 1 && results.empty());
1495  const mp_integer number =
1496  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1497  c = convert_ifnonull(address_map, op, number, i_it->source_location);
1498  }
1499  else if(bytecode == patternt("ifnull"))
1500  {
1501  PRECONDITION(op.size() == 1 && results.empty());
1502  const mp_integer number =
1503  numeric_cast_v<mp_integer>(to_constant_expr(arg0));
1504  c = convert_ifnull(address_map, op, number, i_it->source_location);
1505  }
1506  else if(bytecode == BC_iinc)
1507  {
1508  c = convert_iinc(arg0, arg1, i_it->source_location, i_it->address);
1509  }
1510  else if(bytecode == patternt("?xor"))
1511  {
1512  PRECONDITION(op.size() == 2 && results.size() == 1);
1513  results[0]=bitxor_exprt(op[0], op[1]);
1514  }
1515  else if(bytecode == patternt("?or"))
1516  {
1517  PRECONDITION(op.size() == 2 && results.size() == 1);
1518  results[0]=bitor_exprt(op[0], op[1]);
1519  }
1520  else if(bytecode == patternt("?and"))
1521  {
1522  PRECONDITION(op.size() == 2 && results.size() == 1);
1523  results[0]=bitand_exprt(op[0], op[1]);
1524  }
1525  else if(bytecode == patternt("?shl"))
1526  {
1527  PRECONDITION(op.size() == 2 && results.size() == 1);
1528  results[0]=shl_exprt(op[0], op[1]);
1529  }
1530  else if(bytecode == patternt("?shr"))
1531  {
1532  PRECONDITION(op.size() == 2 && results.size() == 1);
1533  results[0]=ashr_exprt(op[0], op[1]);
1534  }
1535  else if(bytecode == patternt("?ushr"))
1536  {
1537  PRECONDITION(op.size() == 2 && results.size() == 1);
1538  results = convert_ushr(statement, op, results);
1539  }
1540  else if(bytecode == patternt("?add"))
1541  {
1542  PRECONDITION(op.size() == 2 && results.size() == 1);
1543  results[0]=plus_exprt(op[0], op[1]);
1544  }
1545  else if(bytecode == patternt("?sub"))
1546  {
1547  PRECONDITION(op.size() == 2 && results.size() == 1);
1548  results[0]=minus_exprt(op[0], op[1]);
1549  }
1550  else if(bytecode == patternt("?div"))
1551  {
1552  PRECONDITION(op.size() == 2 && results.size() == 1);
1553  results[0]=div_exprt(op[0], op[1]);
1554  }
1555  else if(bytecode == patternt("?mul"))
1556  {
1557  PRECONDITION(op.size() == 2 && results.size() == 1);
1558  results[0]=mult_exprt(op[0], op[1]);
1559  }
1560  else if(bytecode == patternt("?neg"))
1561  {
1562  PRECONDITION(op.size() == 1 && results.size() == 1);
1563  results[0]=unary_minus_exprt(op[0], op[0].type());
1564  }
1565  else if(bytecode == patternt("?rem"))
1566  {
1567  PRECONDITION(op.size() == 2 && results.size() == 1);
1568  if(bytecode == BC_frem || bytecode == BC_drem)
1569  results[0]=rem_exprt(op[0], op[1]);
1570  else
1571  results[0]=mod_exprt(op[0], op[1]);
1572  }
1573  else if(bytecode == patternt("?cmp"))
1574  {
1575  PRECONDITION(op.size() == 2 && results.size() == 1);
1576  results = convert_cmp(op, results);
1577  }
1578  else if(bytecode == patternt("?cmp?"))
1579  {
1580  PRECONDITION(op.size() == 2 && results.size() == 1);
1581  results = convert_cmp2(statement, op, results);
1582  }
1583  else if(bytecode == patternt("?cmpl"))
1584  {
1585  PRECONDITION(op.size() == 2 && results.size() == 1);
1586  results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
1587  }
1588  else if(bytecode == BC_dup)
1589  {
1590  PRECONDITION(op.size() == 1 && results.size() == 2);
1591  results[0]=results[1]=op[0];
1592  }
1593  else if(bytecode == BC_dup_x1)
1594  {
1595  PRECONDITION(op.size() == 2 && results.size() == 3);
1596  results[0]=op[1];
1597  results[1]=op[0];
1598  results[2]=op[1];
1599  }
1600  else if(bytecode == BC_dup_x2)
1601  {
1602  PRECONDITION(op.size() == 3 && results.size() == 4);
1603  results[0]=op[2];
1604  results[1]=op[0];
1605  results[2]=op[1];
1606  results[3]=op[2];
1607  }
1608  // dup2* behaviour depends on the size of the operands on the
1609  // stack
1610  else if(bytecode == BC_dup2)
1611  {
1612  PRECONDITION(!stack.empty() && results.empty());
1613  convert_dup2(op, results);
1614  }
1615  else if(bytecode == BC_dup2_x1)
1616  {
1617  PRECONDITION(!stack.empty() && results.empty());
1618  convert_dup2_x1(op, results);
1619  }
1620  else if(bytecode == BC_dup2_x2)
1621  {
1622  PRECONDITION(!stack.empty() && results.empty());
1623  convert_dup2_x2(op, results);
1624  }
1625  else if(bytecode == BC_getfield)
1626  {
1627  PRECONDITION(op.size() == 1 && results.size() == 1);
1628  results[0] = java_bytecode_promotion(
1629  to_member(op[0], expr_dynamic_cast<fieldref_exprt>(arg0), ns));
1630  }
1631  else if(bytecode == BC_getstatic)
1632  {
1633  PRECONDITION(op.empty() && results.size() == 1);
1634  const auto &field_name=arg0.get_string(ID_component_name);
1635  const bool is_assertions_disabled_field=
1636  field_name.find("$assertionsDisabled")!=std::string::npos;
1637 
1638  const irep_idt field_id(
1639  get_static_field(arg0.get_string(ID_class), field_name));
1640 
1641  // Symbol should have been populated by java_bytecode_convert_class:
1642  const symbol_exprt symbol_expr(
1643  symbol_table.lookup_ref(field_id).symbol_expr());
1644 
1646  i_it->source_location,
1647  arg0,
1648  symbol_expr,
1649  is_assertions_disabled_field,
1650  c,
1651  results);
1652  }
1653  else if(bytecode == BC_putfield)
1654  {
1655  PRECONDITION(op.size() == 2 && results.empty());
1656  c = convert_putfield(expr_dynamic_cast<fieldref_exprt>(arg0), op);
1657  }
1658  else if(bytecode == BC_putstatic)
1659  {
1660  PRECONDITION(op.size() == 1 && results.empty());
1661  const auto &field_name=arg0.get_string(ID_component_name);
1662 
1663  const irep_idt field_id(
1664  get_static_field(arg0.get_string(ID_class), field_name));
1665 
1666  // Symbol should have been populated by java_bytecode_convert_class:
1667  const symbol_exprt symbol_expr(
1668  symbol_table.lookup_ref(field_id).symbol_expr());
1669 
1670  c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr);
1671  }
1672  else if(bytecode == patternt("?2?")) // i2c etc.
1673  {
1674  PRECONDITION(op.size() == 1 && results.size() == 1);
1675  typet type=java_type_from_char(statement[2]);
1676  results[0] = typecast_exprt::conditional_cast(op[0], type);
1677 
1678  // These types get converted/truncated then immediately turned back into
1679  // ints again, so we just double-cast here.
1680  if(
1681  type == java_char_type() || type == java_byte_type() ||
1682  type == java_short_type())
1683  {
1684  results[0] = typecast_exprt(results[0], java_int_type());
1685  }
1686  }
1687  else if(bytecode == BC_new)
1688  {
1689  // use temporary since the stack symbol might get duplicated
1690  PRECONDITION(op.empty() && results.size() == 1);
1691  convert_new(i_it->source_location, arg0, c, results);
1692  }
1693  else if(bytecode == BC_newarray || bytecode == BC_anewarray)
1694  {
1695  // the op is the array size
1696  PRECONDITION(op.size() == 1 && results.size() == 1);
1697  c = convert_newarray(i_it->source_location, statement, arg0, op, results);
1698  }
1699  else if(bytecode == BC_multianewarray)
1700  {
1701  // The first argument is the type, the second argument is the number of
1702  // dimensions. The size of each dimension is on the stack.
1703  const std::size_t dimension =
1704  numeric_cast_v<std::size_t>(to_constant_expr(arg1));
1705 
1706  op=pop(dimension);
1707  assert(results.size()==1);
1708  c = convert_multianewarray(i_it->source_location, arg0, op, results);
1709  }
1710  else if(bytecode == BC_arraylength)
1711  {
1712  PRECONDITION(op.size() == 1 && results.size() == 1);
1713 
1714  // any array type is fine here, so we go for a reference array
1715  dereference_exprt array{typecast_exprt{op[0], java_array_type('a')}};
1716  PRECONDITION(array.type().id() == ID_struct_tag);
1717  array.set(ID_java_member_access, true);
1718 
1719  results[0] = member_exprt{std::move(array), "length", java_int_type()};
1720  }
1721  else if(bytecode == BC_tableswitch || bytecode == BC_lookupswitch)
1722  {
1723  PRECONDITION(op.size() == 1 && results.empty());
1724  c = convert_switch(op, i_it->args, i_it->source_location);
1725  }
1726  else if(bytecode == BC_pop || bytecode == BC_pop2)
1727  {
1728  c = convert_pop(statement, op);
1729  }
1730  else if(bytecode == BC_instanceof)
1731  {
1732  PRECONDITION(op.size() == 1 && results.size() == 1);
1733 
1734  results[0] =
1736  }
1737  else if(bytecode == BC_monitorenter || bytecode == BC_monitorexit)
1738  {
1739  c = convert_monitorenterexit(statement, op, i_it->source_location);
1740  }
1741  else if(bytecode == BC_swap)
1742  {
1743  PRECONDITION(op.size() == 2 && results.size() == 2);
1744  results[1]=op[0];
1745  results[0]=op[1];
1746  }
1747  else if(bytecode == BC_nop)
1748  {
1749  c=code_skipt();
1750  }
1751  else
1752  {
1753  c=codet(statement);
1754  c.operands()=op;
1755  }
1756 
1757  c = do_exception_handling(method, working_set, cur_pc, c);
1758 
1759  // Finally if this is the beginning of a catch block (already determined
1760  // before the big bytecode switch), insert the exception 'landing pad'
1761  // instruction before the actual instruction:
1762  if(catch_instruction.has_value())
1763  {
1764  if(c.get_statement() != ID_block)
1765  c = code_blockt{{c}};
1766  c.operands().insert(c.operands().begin(), *catch_instruction);
1767  }
1768 
1769  if(!i_it->source_location.get_line().empty())
1771 
1772  push(results);
1773 
1774  instruction.done = true;
1775  for(const auto address : instruction.successors)
1776  {
1777  address_mapt::iterator a_it2=address_map.find(address);
1778  CHECK_RETURN(a_it2 != address_map.end());
1779 
1780  // clear the stack if this is an exception handler
1781  for(const auto &exception_row : method.exception_table)
1782  {
1783  if(address==exception_row.handler_pc)
1784  {
1785  stack.clear();
1786  break;
1787  }
1788  }
1789 
1790  if(!stack.empty() && a_it2->second.predecessors.size()>1)
1791  {
1792  // copy into temporaries
1793  code_blockt more_code;
1794 
1795  // introduce temporaries when successor is seen for the first
1796  // time
1797  if(a_it2->second.stack.empty())
1798  {
1799  for(stackt::iterator s_it=stack.begin();
1800  s_it!=stack.end();
1801  ++s_it)
1802  {
1803  symbol_exprt lhs=tmp_variable("$stack", s_it->type());
1804  code_assignt a(lhs, *s_it);
1805  more_code.add(a);
1806 
1807  s_it->swap(lhs);
1808  }
1809  }
1810  else
1811  {
1812  INVARIANT(
1813  a_it2->second.stack.size() == stack.size(),
1814  "Stack sizes should be the same.");
1815  stackt::const_iterator os_it=a_it2->second.stack.begin();
1816  for(auto &expr : stack)
1817  {
1818  assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
1819  symbol_exprt lhs=to_symbol_expr(*os_it);
1820  code_assignt a(lhs, expr);
1821  more_code.add(a);
1822 
1823  expr.swap(lhs);
1824  ++os_it;
1825  }
1826  }
1827 
1828  if(results.empty())
1829  {
1830  more_code.add(c);
1831  c.swap(more_code);
1832  }
1833  else
1834  {
1835  if(c.get_statement() != ID_block)
1836  c = code_blockt{{c}};
1837 
1838  auto &last_statement=to_code_block(c).find_last_statement();
1839  if(last_statement.get_statement()==ID_goto)
1840  {
1841  // Insert stack twiddling before branch:
1842  if(last_statement.get_statement() != ID_block)
1843  last_statement = code_blockt{{last_statement}};
1844 
1845  last_statement.operands().insert(
1846  last_statement.operands().begin(),
1847  more_code.statements().begin(),
1848  more_code.statements().end());
1849  }
1850  else
1851  to_code_block(c).append(more_code);
1852  }
1853  }
1854  a_it2->second.stack=stack;
1855  }
1856  }
1857 
1858  code_blockt code;
1859 
1860  // Add anonymous locals to the symtab:
1861  for(const auto &var : used_local_names)
1862  {
1863  symbolt new_symbol;
1864  new_symbol.name=var.get_identifier();
1865  new_symbol.type=var.type();
1866  new_symbol.base_name=var.get(ID_C_base_name);
1867  new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
1868  new_symbol.mode=ID_java;
1869  new_symbol.is_type=false;
1870  new_symbol.is_file_local=true;
1871  new_symbol.is_thread_local=true;
1872  new_symbol.is_lvalue=true;
1873  symbol_table.add(new_symbol);
1874  }
1875 
1876  // Try to recover block structure as indicated in the local variable table:
1877 
1878  // The block tree node mirrors the block structure of root_block,
1879  // indexing the Java PCs where each subblock starts and ends.
1880  block_tree_nodet root;
1881  code_blockt root_block;
1882 
1883  // First create a simple flat list of basic blocks. We'll add lexical nesting
1884  // constructs as variable live-ranges require next.
1885  bool start_new_block=true;
1886  bool has_seen_previous_address=false;
1887  method_offsett previous_address = 0;
1888  for(const auto &address_pair : address_map)
1889  {
1890  const method_offsett address = address_pair.first;
1891  assert(address_pair.first==address_pair.second.source->address);
1892  const codet &c=address_pair.second.code;
1893 
1894  // Start a new lexical block if this is a branch target:
1895  if(!start_new_block)
1896  start_new_block=targets.find(address)!=targets.end();
1897  // Start a new lexical block if this is a control flow join
1898  // (e.g. due to exceptional control flow)
1899  if(!start_new_block)
1900  start_new_block=address_pair.second.predecessors.size()>1;
1901  // Start a new lexical block if we've just entered a block in which
1902  // exceptions are handled. This is usually the start of a try block, but a
1903  // single try can be represented as multiple non-contiguous blocks in the
1904  // exception table.
1905  if(!start_new_block && has_seen_previous_address)
1906  {
1907  for(const auto &exception_row : method.exception_table)
1908  if(exception_row.start_pc==previous_address)
1909  {
1910  start_new_block=true;
1911  break;
1912  }
1913  }
1914 
1915  if(start_new_block)
1916  {
1917  root_block.add(
1919  root.branch.push_back(block_tree_nodet::get_leaf());
1920  assert((root.branch_addresses.empty() ||
1921  root.branch_addresses.back()<address) &&
1922  "Block addresses should be unique and increasing");
1923  root.branch_addresses.push_back(address);
1924  }
1925 
1926  if(c.get_statement()!=ID_skip)
1927  {
1928  auto &lastlabel = to_code_label(root_block.statements().back());
1929  auto &add_to_block=to_code_block(lastlabel.code());
1930  add_to_block.add(c);
1931  }
1932  start_new_block=address_pair.second.successors.size()>1;
1933 
1934  previous_address=address;
1935  has_seen_previous_address=true;
1936  }
1937 
1938  // Find out where temporaries are used:
1939  std::map<irep_idt, variablet> temporary_variable_live_ranges;
1940  for(const auto &aentry : address_map)
1942  aentry.first,
1943  aentry.second.code,
1944  temporary_variable_live_ranges);
1945 
1946  std::vector<const variablet*> vars_to_process;
1947  for(const auto &vlist : variables)
1948  for(const auto &v : vlist)
1949  vars_to_process.push_back(&v);
1950 
1951  for(const auto &v : tmp_vars)
1952  vars_to_process.push_back(
1953  &temporary_variable_live_ranges.at(v.get_identifier()));
1954 
1955  for(const auto &v : used_local_names)
1956  vars_to_process.push_back(
1957  &temporary_variable_live_ranges.at(v.get_identifier()));
1958 
1959  for(const auto vp : vars_to_process)
1960  {
1961  const auto &v=*vp;
1962  if(v.is_parameter)
1963  continue;
1964  // Merge lexical scopes as far as possible to allow us to
1965  // declare these variable scopes faithfully.
1966  // Don't insert yet, as for the time being the blocks' only
1967  // operands must be other blocks.
1968  // The declarations will be inserted in the next pass instead.
1970  root,
1971  root_block,
1972  v.start_pc,
1973  v.start_pc + v.length,
1974  std::numeric_limits<method_offsett>::max(),
1975  address_map);
1976  }
1977  for(const auto vp : vars_to_process)
1978  {
1979  const auto &v=*vp;
1980  if(v.is_parameter)
1981  continue;
1982  // Skip anonymous variables:
1983  if(v.symbol_expr.get_identifier().empty())
1984  continue;
1985  auto &block = get_block_for_pcrange(
1986  root,
1987  root_block,
1988  v.start_pc,
1989  v.start_pc + v.length,
1990  std::numeric_limits<method_offsett>::max());
1991  code_declt d(v.symbol_expr);
1992  block.statements().insert(block.statements().begin(), d);
1993  }
1994 
1995  for(auto &block : root_block.statements())
1996  code.add(block);
1997 
1998  return code;
1999 }
2000 
2002  const irep_idt &statement,
2003  const exprt::operandst &op)
2004 {
2005  // these are skips
2006  codet c = code_skipt();
2007 
2008  // pop2 removes two single-word items from the stack (e.g. two
2009  // integers, or an integer and an object reference) or one
2010  // two-word item (i.e. a double or a long).
2011  // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
2012  if(statement == "pop2" && get_bytecode_type_width(op[0].type()) == 32)
2013  pop(1);
2014  return c;
2015 }
2016 
2018  const exprt::operandst &op,
2020  const source_locationt &location)
2021 {
2022  // we turn into switch-case
2023  code_blockt code_block;
2024  code_block.add_source_location() = location;
2025 
2026  bool is_label = true;
2027  for(auto a_it = args.begin(); a_it != args.end();
2028  a_it++, is_label = !is_label)
2029  {
2030  if(is_label)
2031  {
2032  const mp_integer number =
2033  numeric_cast_v<mp_integer>(to_constant_expr(*a_it));
2034  // The switch case does not contain any code, it just branches via a GOTO
2035  // to the jump target of the tableswitch/lookupswitch case at
2036  // hand. Therefore we consider this code to belong to the source bytecode
2037  // instruction and not the target instruction.
2038  const method_offsett label_number =
2039  numeric_cast_v<method_offsett>(number);
2040  code_gotot code(label(std::to_string(label_number)));
2041  code.add_source_location() = location;
2042 
2043  if(a_it == args.begin())
2044  {
2045  code_switch_caset code_case(nil_exprt(), std::move(code));
2046  code_case.set_default();
2047 
2048  code_block.add(std::move(code_case), location);
2049  }
2050  else
2051  {
2052  exprt case_op =
2053  typecast_exprt::conditional_cast(*std::prev(a_it), op[0].type());
2054  case_op.add_source_location() = location;
2055 
2056  code_switch_caset code_case(std::move(case_op), std::move(code));
2057  code_block.add(std::move(code_case), location);
2058  }
2059  }
2060  }
2061 
2062  code_switcht code_switch(op[0], std::move(code_block));
2063  code_switch.add_source_location() = location;
2064  return code_switch;
2065 }
2066 
2068  const irep_idt &statement,
2069  const exprt::operandst &op,
2070  const source_locationt &source_location)
2071 {
2072  const irep_idt descriptor = (statement == "monitorenter") ?
2073  "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
2074  "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
2075 
2076  if(!threading_support || !symbol_table.has_symbol(descriptor))
2077  return code_skipt();
2078 
2079  // becomes a function call
2080  java_method_typet type(
2082  java_void_type());
2083  code_function_callt call(symbol_exprt(descriptor, type), {op[0]});
2084  call.add_source_location() = source_location;
2085  if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
2086  needed_lazy_methods->add_needed_method(descriptor);
2087  return std::move(call);
2088 }
2089 
2091  exprt::operandst &op,
2092  exprt::operandst &results)
2093 {
2094  if(get_bytecode_type_width(stack.back().type()) == 32)
2095  op = pop(2);
2096  else
2097  op = pop(1);
2098 
2099  results.insert(results.end(), op.begin(), op.end());
2100  results.insert(results.end(), op.begin(), op.end());
2101 }
2102 
2104  exprt::operandst &op,
2105  exprt::operandst &results)
2106 {
2107  if(get_bytecode_type_width(stack.back().type()) == 32)
2108  op = pop(3);
2109  else
2110  op = pop(2);
2111 
2112  results.insert(results.end(), op.begin() + 1, op.end());
2113  results.insert(results.end(), op.begin(), op.end());
2114 }
2115 
2117  exprt::operandst &op,
2118  exprt::operandst &results)
2119 {
2120  if(get_bytecode_type_width(stack.back().type()) == 32)
2121  op = pop(2);
2122  else
2123  op = pop(1);
2124 
2125  exprt::operandst op2;
2126 
2127  if(get_bytecode_type_width(stack.back().type()) == 32)
2128  op2 = pop(2);
2129  else
2130  op2 = pop(1);
2131 
2132  results.insert(results.end(), op.begin(), op.end());
2133  results.insert(results.end(), op2.begin(), op2.end());
2134  results.insert(results.end(), op.begin(), op.end());
2135 }
2136 
2138  const irep_idt &statement,
2139  const constant_exprt &arg0,
2140  exprt::operandst &results) const
2141 {
2142  const char type_char = statement[0];
2143  const bool is_double('d' == type_char);
2144  const bool is_float('f' == type_char);
2145 
2146  if(is_double || is_float)
2147  {
2148  const ieee_float_spect spec(
2151 
2152  ieee_floatt value(spec);
2153  if(arg0.type().id() != ID_floatbv)
2154  {
2155  const mp_integer number = numeric_cast_v<mp_integer>(arg0);
2156  value.from_integer(number);
2157  }
2158  else
2159  value.from_expr(arg0);
2160 
2161  results[0] = value.to_expr();
2162  }
2163  else
2164  {
2165  const mp_integer value = numeric_cast_v<mp_integer>(arg0);
2166  const typet type = java_type_from_char(statement[0]);
2167  results[0] = from_integer(value, type);
2168  }
2169  return results;
2170 }
2171 
2173  const java_method_typet::parameterst &parameters,
2175 {
2176  // do some type adjustment for the arguments,
2177  // as Java promotes arguments
2178  // Also cast pointers since intermediate locals
2179  // can be void*.
2180  INVARIANT(
2181  parameters.size() == arguments.size(),
2182  "for each parameter there must be exactly one argument");
2183  for(std::size_t i = 0; i < parameters.size(); i++)
2184  {
2185  const typet &type = parameters[i].type();
2186  if(
2187  type == java_boolean_type() || type == java_char_type() ||
2188  type == java_byte_type() || type == java_short_type() ||
2189  type.id() == ID_pointer)
2190  {
2191  arguments[i] = typecast_exprt::conditional_cast(arguments[i], type);
2192  }
2193  }
2194 }
2195 
2197  source_locationt location,
2198  const irep_idt &statement,
2199  class_method_descriptor_exprt &class_method_descriptor,
2200  codet &c,
2201  exprt::operandst &results)
2202 {
2203  const bool use_this(statement != "invokestatic");
2204  const bool is_virtual(
2205  statement == "invokevirtual" || statement == "invokeinterface");
2206 
2207  const irep_idt &invoked_method_id = class_method_descriptor.get_identifier();
2208  INVARIANT(
2209  !invoked_method_id.empty(),
2210  "invoke statement arg0 must have an identifier");
2211 
2212  auto method_symbol = symbol_table.symbols.find(invoked_method_id);
2213 
2214  // Use the most precise type available: the actual symbol has generic info,
2215  // whereas the type given by the invoke instruction doesn't and is therefore
2216  // less accurate.
2217  if(method_symbol != symbol_table.symbols.end())
2218  {
2219  // Note the number of parameters might change here due to constructors using
2220  // invokespecial will have zero arguments (the `this` is added below)
2221  // but the symbol for the <init> will have the this parameter.
2222  INVARIANT(
2223  to_java_method_type(class_method_descriptor.type()).return_type().id() ==
2224  to_code_type(method_symbol->second.type).return_type().id(),
2225  "Function return type must not change in kind");
2226  class_method_descriptor.type() = method_symbol->second.type;
2227  }
2228 
2229  // Note arg0 and arg0.type() are subject to many side-effects in this method,
2230  // then finally used to populate the call instruction.
2231  java_method_typet &method_type =
2232  to_java_method_type(class_method_descriptor.type());
2233 
2234  java_method_typet::parameterst &parameters(method_type.parameters());
2235 
2236  if(use_this)
2237  {
2238  const irep_idt class_id = class_method_descriptor.class_id();
2239 
2240  if(parameters.empty() || !parameters[0].get_this())
2241  {
2242  typet thistype = struct_tag_typet(class_id);
2243  reference_typet object_ref_type = java_reference_type(thistype);
2244  java_method_typet::parametert this_p(object_ref_type);
2245  this_p.set_this();
2246  this_p.set_base_name(ID_this);
2247  parameters.insert(parameters.begin(), this_p);
2248  }
2249 
2250  // Note invokespecial is used for super-method calls as well as
2251  // constructors.
2252  if(statement == "invokespecial")
2253  {
2254  if(is_constructor(invoked_method_id))
2255  {
2257  needed_lazy_methods->add_needed_class(class_id);
2258  method_type.set_is_constructor();
2259  }
2260  else
2261  method_type.set(ID_java_super_method_call, true);
2262  }
2263  }
2264 
2265  location.set_function(method_id);
2266 
2267  code_function_callt::argumentst arguments = pop(parameters.size());
2268 
2269  // double-check a bit
2270  INVARIANT(
2271  !use_this || arguments.front().type().id() == ID_pointer,
2272  "first argument must be a pointer");
2273 
2274  adjust_invoke_argument_types(parameters, arguments);
2275 
2276  // do some type adjustment for return values
2277  exprt lhs = nil_exprt();
2278  const typet &return_type = method_type.return_type();
2279 
2280  if(return_type.id() != ID_empty)
2281  {
2282  // return types are promoted in Java
2283  lhs = tmp_variable("return", return_type);
2284  exprt promoted = java_bytecode_promotion(lhs);
2285  results.resize(1);
2286  results[0] = promoted;
2287  }
2288 
2289  // If we don't have a definition for the called symbol, and we won't
2290  // inherit a definition from a super-class, we create a new symbol and
2291  // insert it in the symbol table. The name and type of the method are
2292  // derived from the information we have in the call.
2293  // We fix the access attribute to ID_private, because of the following
2294  // reasons:
2295  // - We don't know the original access attribute and since the .class file is
2296  // unavailable, we have no way to know.
2297  // - The translated method could be an inherited protected method, hence
2298  // accessible from the original caller, but not from the generated test.
2299  // Therefore we must assume that the method is not accessible.
2300  // We set opaque methods as final to avoid assuming they can be overridden.
2301  if(
2302  method_symbol == symbol_table.symbols.end() &&
2303  !(is_virtual && is_method_inherited(
2304  class_method_descriptor.class_id(),
2305  class_method_descriptor.mangled_method_name())))
2306  {
2308  invoked_method_id,
2309  class_method_descriptor.base_method_name(),
2310  id2string(class_method_descriptor.class_id()).substr(6) + "." +
2311  id2string(class_method_descriptor.base_method_name()) + "()",
2312  method_type,
2313  class_method_descriptor.class_id(),
2314  symbol_table,
2316  }
2317 
2318  exprt function;
2319  if(is_virtual)
2320  {
2321  // dynamic binding
2322  PRECONDITION(use_this);
2323  PRECONDITION(!arguments.empty());
2324  function = class_method_descriptor;
2325  // Populate needed methods later,
2326  // once we know what object types can exist.
2327  }
2328  else
2329  {
2330  // static binding
2331  function = symbol_exprt(invoked_method_id, method_type);
2333  {
2334  needed_lazy_methods->add_needed_method(invoked_method_id);
2335  // Calling a static method causes static initialization:
2336  needed_lazy_methods->add_needed_class(class_method_descriptor.class_id());
2337  }
2338  }
2339 
2340  code_function_callt call(
2341  std::move(lhs), std::move(function), std::move(arguments));
2342  call.add_source_location() = location;
2343  call.function().add_source_location() = location;
2344 
2345  // Replacing call if it is a function of the Character library,
2346  // returning the same call otherwise
2348 
2349  if(!use_this)
2350  {
2351  codet clinit_call = get_clinit_call(class_method_descriptor.class_id());
2352  if(clinit_call.get_statement() != ID_skip)
2353  c = code_blockt({clinit_call, c});
2354  }
2355 }
2356 
2358  source_locationt location,
2359  codet &c)
2360 {
2361  exprt operand = pop(1)[0];
2362 
2363  // we may need to adjust the type of the argument
2364  operand = typecast_exprt::conditional_cast(operand, bool_typet());
2365 
2366  c = code_assumet(operand);
2367  location.set_function(method_id);
2368  c.add_source_location() = location;
2369  return c;
2370 }
2371 
2373  const exprt &arg0,
2374  const exprt::operandst &op,
2375  codet &c,
2376  exprt::operandst &results) const
2377 {
2378  java_instanceof_exprt check(op[0], to_struct_tag_type(arg0.type()));
2379  code_assertt assert_class(check);
2380  assert_class.add_source_location().set_comment("Dynamic cast check");
2381  assert_class.add_source_location().set_property_class("bad-dynamic-cast");
2382  // we add this assert such that we can recognise it
2383  // during the instrumentation phase
2384  c = std::move(assert_class);
2385  results[0] = op[0];
2386 }
2387 
2389  const source_locationt &location,
2390  const exprt::operandst &op,
2391  codet &c,
2392  exprt::operandst &results) const
2393 {
2394  if(
2397  "java::java.lang.AssertionError") &&
2399  {
2400  // we translate athrow into
2401  // ASSERT false;
2402  // ASSUME false:
2403  code_assertt assert_code(false_exprt{});
2404  source_locationt assert_location = location; // copy
2405  assert_location.set_comment("assertion at " + location.as_string());
2406  assert_location.set("user-provided", true);
2407  assert_location.set_property_class(ID_assertion);
2408  assert_code.add_source_location() = assert_location;
2409 
2410  code_assumet assume_code(false_exprt{});
2411  source_locationt assume_location = location; // copy
2412  assume_location.set("user-provided", true);
2413  assume_code.add_source_location() = assume_location;
2414 
2415  c = code_blockt({assert_code, assume_code});
2416  }
2417  else
2418  {
2419  side_effect_expr_throwt throw_expr(irept(), typet(), location);
2420  throw_expr.copy_to_operands(op[0]);
2421  c = code_expressiont(throw_expr);
2422  }
2423  results[0] = op[0];
2424 }
2425 
2428  const std::set<method_offsett> &working_set,
2429  method_offsett cur_pc,
2430  codet &code)
2431 {
2432  // For each exception handler range that starts here add a CATCH-PUSH marker
2433  // Each CATCH-PUSH records a list of all the exception id and handler label
2434  // pairs handled for its exact block
2435 
2436  // Gather all try-catch blocks that have cur_pc as the starting pc
2437  typedef std::vector<std::reference_wrapper<
2439  std::map<std::size_t, exceptionst> exceptions_by_end;
2441  : method.exception_table)
2442  {
2443  if(exception.start_pc == cur_pc)
2444  exceptions_by_end[exception.end_pc].push_back(exception);
2445  }
2446  for(const auto &exceptions : exceptions_by_end)
2447  {
2448  // For each block with a distinct end position create one CATCH-PUSH
2449  code_push_catcht catch_push;
2450  // Fill in its exception_list
2451  code_push_catcht::exception_listt &exception_list =
2452  catch_push.exception_list();
2454  : exceptions.second)
2455  {
2456  exception_list.emplace_back(
2457  exception.catch_type.get_identifier(),
2458  // Record the exception handler in the CATCH-PUSH instruction by
2459  // generating a label corresponding to the handler's pc
2460  label(std::to_string(exception.handler_pc)));
2461  }
2462  // Prepend the CATCH-PUSH instruction
2463  code = code_blockt({ std::move(catch_push), code });
2464  }
2465 
2466  // Next add the CATCH-POP instructions
2467  // exception_row.end_pc is exclusive so append a CATCH-POP instruction if
2468  // this is the instruction before it.
2469  // To do this, attempt to find all exception handlers that end at the
2470  // earliest known instruction after this one.
2471 
2472  // Dangerously, we assume that the next opcode in the bytecode after the end
2473  // of the exception handler block (whose address matches the exclusive end
2474  // position of the block) will be a successor of some code investigated
2475  // before the instruction at the end of that handler and therefore in the
2476  // working set.
2477  // As an example of where this may fail, for non-obfuscated bytecode
2478  // generated by most compilers the next opcode after the block ending at the
2479  // end of the try block is the lexically next bit of code after the try
2480  // block, i.e. the catch block. When there aren't any throwing statements in
2481  // the try block this block will not be the successor of any instruction.
2482 
2483  auto next_opcode_it = std::find_if(
2484  working_set.begin(),
2485  working_set.end(),
2486  [cur_pc](method_offsett offset) { return offset > cur_pc; });
2487  if(next_opcode_it != working_set.end())
2488  {
2489  // Count the distinct start positions of handlers that end at this location
2490  std::set<std::size_t> start_positions; // Use a set to deduplicate
2491  for(const auto &exception_row : method.exception_table)
2492  {
2493  // Check if the next instruction found is the (exclusive) end of a block
2494  if(*next_opcode_it == exception_row.end_pc)
2495  start_positions.insert(exception_row.start_pc);
2496  }
2497  for(std::size_t handler = 0; handler < start_positions.size(); ++handler)
2498  {
2499  // Append a CATCH-POP instruction before the end of the block
2500  code = code_blockt({ code, code_pop_catcht() });
2501  }
2502  }
2503 
2504  return code;
2505 }
2506 
2508  const source_locationt &location,
2509  const exprt &arg0,
2510  const exprt::operandst &op,
2511  exprt::operandst &results)
2512 {
2513  const reference_typet ref_type = java_reference_type(arg0.type());
2514  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
2515  java_new_array.operands() = op;
2516 
2517  code_blockt create;
2518 
2519  if(max_array_length != 0)
2520  {
2522  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2523  code_assumet assume_le_max_size(le_max_size);
2524  create.add(assume_le_max_size);
2525  }
2526 
2527  const exprt tmp = tmp_variable("newarray", ref_type);
2528  create.add(code_assignt(tmp, java_new_array));
2529  results[0] = tmp;
2530 
2531  return create;
2532 }
2533 
2535  const source_locationt &location,
2536  const irep_idt &statement,
2537  const exprt &arg0,
2538  const exprt::operandst &op,
2539  exprt::operandst &results)
2540 {
2541  java_reference_typet ref_type = [&]() {
2542  if(statement == "newarray")
2543  {
2544  irep_idt id = arg0.type().id();
2545 
2546  char element_type;
2547  if(id == ID_bool)
2548  element_type = 'z';
2549  else if(id == ID_char)
2550  element_type = 'c';
2551  else if(id == ID_float)
2552  element_type = 'f';
2553  else if(id == ID_double)
2554  element_type = 'd';
2555  else if(id == ID_byte)
2556  element_type = 'b';
2557  else if(id == ID_short)
2558  element_type = 's';
2559  else if(id == ID_int)
2560  element_type = 'i';
2561  else if(id == ID_long)
2562  element_type = 'j';
2563  else
2564  element_type = '?';
2565  return java_array_type(element_type);
2566  }
2567  else
2568  {
2570  }
2571  }();
2572 
2573  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
2574  java_new_array.copy_to_operands(op[0]);
2575 
2576  code_blockt block;
2577 
2578  if(max_array_length != 0)
2579  {
2581  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2582  code_assumet assume_le_max_size(le_max_size);
2583  block.add(std::move(assume_le_max_size));
2584  }
2585  const exprt tmp = tmp_variable("newarray", ref_type);
2586  block.add(code_assignt(tmp, java_new_array));
2587  results[0] = tmp;
2588 
2589  return block;
2590 }
2591 
2593  const source_locationt &location,
2594  const exprt &arg0,
2595  codet &c,
2596  exprt::operandst &results)
2597 {
2598  const reference_typet ref_type = java_reference_type(arg0.type());
2599  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
2600 
2601  if(!location.get_line().empty())
2602  java_new_expr.add_source_location() = location;
2603 
2604  const exprt tmp = tmp_variable("new", ref_type);
2605  c = code_assignt(tmp, java_new_expr);
2606  c.add_source_location() = location;
2607  codet clinit_call =
2609  if(clinit_call.get_statement() != ID_skip)
2610  {
2611  c = code_blockt({clinit_call, c});
2612  }
2613  results[0] = tmp;
2614 }
2615 
2617  const source_locationt &location,
2618  const exprt &arg0,
2619  const exprt::operandst &op,
2620  const symbol_exprt &symbol_expr)
2621 {
2622  if(needed_lazy_methods && arg0.type().id() == ID_struct_tag)
2623  {
2624  needed_lazy_methods->add_needed_class(
2626  }
2627 
2628  code_blockt block;
2629  block.add_source_location() = location;
2630 
2631  // Note this initializer call deliberately inits the class used to make
2632  // the reference, which may be a child of the class that actually defines
2633  // the field.
2634  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2635  if(clinit_call.get_statement() != ID_skip)
2636  block.add(clinit_call);
2637 
2639  "stack_static_field",
2640  block,
2642  symbol_expr.get_identifier());
2643  block.add(code_assignt(symbol_expr, op[0]));
2644  return block;
2645 }
2646 
2648  const fieldref_exprt &arg0,
2649  const exprt::operandst &op)
2650 {
2651  code_blockt block;
2653  "stack_field", block, bytecode_write_typet::FIELD, arg0.component_name());
2654  block.add(code_assignt(to_member(op[0], arg0, ns), op[1]));
2655  return block;
2656 }
2657 
2659  const source_locationt &source_location,
2660  const exprt &arg0,
2661  const symbol_exprt &symbol_expr,
2662  const bool is_assertions_disabled_field,
2663  codet &c,
2664  exprt::operandst &results)
2665 {
2667  {
2668  if(arg0.type().id() == ID_struct_tag)
2669  {
2670  needed_lazy_methods->add_needed_class(
2672  }
2673  else if(arg0.type().id() == ID_pointer)
2674  {
2675  const auto &pointer_type = to_pointer_type(arg0.type());
2676  if(pointer_type.subtype().id() == ID_struct_tag)
2677  {
2678  needed_lazy_methods->add_needed_class(
2680  }
2681  }
2682  else if(is_assertions_disabled_field)
2683  {
2684  needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
2685  }
2686  }
2687  symbol_exprt symbol_with_location = symbol_expr;
2688  symbol_with_location.add_source_location() = source_location;
2689  results[0] = java_bytecode_promotion(symbol_with_location);
2690 
2691  // Note this initializer call deliberately inits the class used to make
2692  // the reference, which may be a child of the class that actually defines
2693  // the field.
2694  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2695  if(clinit_call.get_statement() != ID_skip)
2696  c = clinit_call;
2697  else if(is_assertions_disabled_field)
2698  {
2699  // set $assertionDisabled to false
2700  c = code_assignt(symbol_expr, false_exprt());
2701  }
2702 }
2703 
2705  const irep_idt &statement,
2706  const exprt::operandst &op,
2707  exprt::operandst &results) const
2708 {
2709  const int nan_value(statement[4] == 'l' ? -1 : 1);
2710  const typet result_type(java_int_type());
2711  const exprt nan_result(from_integer(nan_value, result_type));
2712 
2713  // (value1 == NaN || value2 == NaN) ?
2714  // nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0;
2715  // (value1 == NaN || value2 == NaN) ?
2716  // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0;
2717 
2718  isnan_exprt nan_op0(op[0]);
2719  isnan_exprt nan_op1(op[1]);
2720  exprt one = from_integer(1, result_type);
2721  exprt minus_one = from_integer(-1, result_type);
2722  results[0] = if_exprt(
2723  or_exprt(nan_op0, nan_op1),
2724  nan_result,
2725  if_exprt(
2726  ieee_float_equal_exprt(op[0], op[1]),
2727  from_integer(0, result_type),
2728  if_exprt(binary_relation_exprt(op[0], ID_lt, op[1]), minus_one, one)));
2729  return results;
2730 }
2731 
2733  const exprt::operandst &op,
2734  exprt::operandst &results) const
2735 { // The integer result on the stack is:
2736  // 0 if op[0] equals op[1]
2737  // -1 if op[0] is less than op[1]
2738  // 1 if op[0] is greater than op[1]
2739 
2740  const typet t = java_int_type();
2741  exprt one = from_integer(1, t);
2742  exprt minus_one = from_integer(-1, t);
2743 
2744  if_exprt greater =
2745  if_exprt(binary_relation_exprt(op[0], ID_gt, op[1]), one, minus_one);
2746 
2747  results[0] = if_exprt(
2748  binary_relation_exprt(op[0], ID_equal, op[1]), from_integer(0, t), greater);
2749  return results;
2750 }
2751 
2753  const irep_idt &statement,
2754  const exprt::operandst &op,
2755  exprt::operandst &results) const
2756 {
2757  const typet type = java_type_from_char(statement[0]);
2758 
2759  const std::size_t width = get_bytecode_type_width(type);
2760  typet target = unsignedbv_typet(width);
2761 
2762  exprt lhs = typecast_exprt::conditional_cast(op[0], target);
2763  exprt rhs = typecast_exprt::conditional_cast(op[1], target);
2764 
2765  results[0] =
2766  typecast_exprt::conditional_cast(lshr_exprt(lhs, rhs), op[0].type());
2767 
2768  return results;
2769 }
2770 
2772  const exprt &arg0,
2773  const exprt &arg1,
2774  const source_locationt &location,
2775  const method_offsett address)
2776 {
2777  code_blockt block;
2778  block.add_source_location() = location;
2779  // search variable on stack
2780  const exprt &locvar = variable(arg0, 'i', address);
2782  "stack_iinc",
2783  block,
2785  to_symbol_expr(locvar).get_identifier());
2786 
2787  const exprt arg1_int_type =
2789  code_assignt code_assign(
2790  variable(arg0, 'i', address),
2791  plus_exprt(
2793  variable(arg0, 'i', address), java_int_type()),
2794  arg1_int_type));
2795  block.add(std::move(code_assign));
2796 
2797  return block;
2798 }
2799 
2802  const exprt::operandst &op,
2803  const mp_integer &number,
2804  const source_locationt &location) const
2805 {
2806  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
2807  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2808 
2809  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2810 
2811  code_ifthenelset code_branch(
2812  binary_relation_exprt(lhs, ID_equal, rhs),
2813  code_gotot(label(std::to_string(label_number))));
2814 
2815  code_branch.then_case().add_source_location() =
2816  address_map.at(label_number).source->source_location;
2817  code_branch.add_source_location() = location;
2818 
2819  return code_branch;
2820 }
2821 
2824  const exprt::operandst &op,
2825  const mp_integer &number,
2826  const source_locationt &location) const
2827 {
2828  const typecast_exprt lhs(op[0], java_reference_type(java_void_type()));
2829  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2830 
2831  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2832 
2833  code_ifthenelset code_branch(
2834  binary_relation_exprt(lhs, ID_notequal, rhs),
2835  code_gotot(label(std::to_string(label_number))));
2836 
2837  code_branch.then_case().add_source_location() =
2838  address_map.at(label_number).source->source_location;
2839  code_branch.add_source_location() = location;
2840 
2841  return code_branch;
2842 }
2843 
2846  const exprt::operandst &op,
2847  const irep_idt &id,
2848  const mp_integer &number,
2849  const source_locationt &location) const
2850 {
2851  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2852 
2853  code_ifthenelset code_branch(
2854  binary_relation_exprt(op[0], id, from_integer(0, op[0].type())),
2855  code_gotot(label(std::to_string(label_number))));
2856 
2857  code_branch.cond().add_source_location() = location;
2859  code_branch.then_case().add_source_location() =
2860  address_map.at(label_number).source->source_location;
2862  code_branch.add_source_location() = location;
2864 
2865  return code_branch;
2866 }
2867 
2870  const u1 bytecode,
2871  const exprt::operandst &op,
2872  const mp_integer &number,
2873  const source_locationt &location) const
2874 {
2875  const irep_idt cmp_op = get_if_cmp_operator(bytecode);
2876  binary_relation_exprt condition(
2877  op[0], cmp_op, typecast_exprt::conditional_cast(op[1], op[0].type()));
2878  condition.add_source_location() = location;
2879 
2880  const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2881 
2882  code_ifthenelset code_branch(
2883  std::move(condition), code_gotot(label(std::to_string(label_number))));
2884 
2885  code_branch.then_case().add_source_location() =
2886  address_map.at(label_number).source->source_location;
2887  code_branch.add_source_location() = location;
2888 
2889  return code_branch;
2890 }
2891 
2893  const std::vector<method_offsett> &jsr_ret_targets,
2894  const exprt &arg0,
2895  const source_locationt &location,
2896  const method_offsett address)
2897 {
2898  code_blockt c;
2899  auto retvar = variable(arg0, 'a', address);
2900  for(size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2901  {
2902  irep_idt number = std::to_string(jsr_ret_targets[idx]);
2903  code_gotot g(label(number));
2904  g.add_source_location() = location;
2905  if(idx == idxlim - 1)
2906  c.add(g);
2907  else
2908  {
2909  auto address_ptr =
2910  from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
2911  address_ptr.type() = pointer_type(java_void_type());
2912 
2913  code_ifthenelset branch(equal_exprt(retvar, address_ptr), std::move(g));
2914 
2915  branch.cond().add_source_location() = location;
2916  branch.add_source_location() = location;
2917 
2918  c.add(std::move(branch));
2919  }
2920  }
2921  return c;
2922 }
2923 
2929 static exprt conditional_array_cast(const exprt &expr, char type_char)
2930 {
2931  const auto ref_type =
2932  type_try_dynamic_cast<java_reference_typet>(expr.type());
2933  const bool typecast_not_needed =
2934  ref_type && ((type_char == 'b' && ref_type->subtype().get_identifier() ==
2935  "java::array[boolean]") ||
2936  *ref_type == java_array_type(type_char));
2937  return typecast_not_needed ? expr
2938  : typecast_exprt(expr, java_array_type(type_char));
2939 }
2940 
2942  const irep_idt &statement,
2943  const exprt::operandst &op)
2944 {
2945  PRECONDITION(op.size() == 2);
2946  const char type_char = statement[0];
2947  const exprt op_with_right_type = conditional_array_cast(op[0], type_char);
2948  dereference_exprt deref{op_with_right_type};
2949  deref.set(ID_java_member_access, true);
2950 
2951  auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
2952  INVARIANT(java_array_type, "Java array type should be a struct_tag_typet");
2953  member_exprt data_ptr{
2955  plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
2956  // tag it so it's easy to identify during instrumentation
2957  data_plus_offset.set(ID_java_array_access, true);
2958  return java_bytecode_promotion(dereference_exprt{data_plus_offset});
2959 }
2960 
2962  const exprt &index,
2963  char type_char,
2964  size_t address)
2965 {
2966  const exprt var = variable(index, type_char, address);
2967  if(type_char == 'i')
2968  {
2969  INVARIANT(
2971  type_try_dynamic_cast<bitvector_typet>(var.type())->get_width() <= 32,
2972  "iload can be used for boolean, byte, short, int and char");
2974  }
2975  INVARIANT(
2976  (type_char == 'a' && can_cast_type<reference_typet>(var.type())) ||
2977  var.type() == java_type_from_char(type_char),
2978  "Variable type must match [adflv]load return type");
2979  return var;
2980 }
2981 
2983  const irep_idt &statement,
2984  const exprt &arg0,
2985  const exprt::operandst &op,
2986  const method_offsett address,
2987  const source_locationt &location)
2988 {
2989  const exprt var = variable(arg0, statement[0], address);
2990  const irep_idt &var_name = to_symbol_expr(var).get_identifier();
2991 
2992  code_blockt block;
2993  block.add_source_location() = location;
2994 
2996  "stack_store",
2997  block,
2999  var_name);
3000 
3001  block.add(
3003  location);
3004  return block;
3005 }
3006 
3008  const irep_idt &statement,
3009  const exprt::operandst &op,
3010  const source_locationt &location)
3011 {
3012  PRECONDITION(op.size() == 3);
3013  const char type_char = statement[0];
3014  const exprt op_with_right_type = conditional_array_cast(op[0], type_char);
3015  dereference_exprt deref{op_with_right_type};
3016  deref.set(ID_java_member_access, true);
3017 
3018  auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
3019  INVARIANT(java_array_type, "Java array type should be a struct_tag_typet");
3020  member_exprt data_ptr{
3022  plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
3023  // tag it so it's easy to identify during instrumentation
3024  data_plus_offset.set(ID_java_array_access, true);
3025 
3026  code_blockt block;
3027  block.add_source_location() = location;
3028 
3030  "stack_astore", block, bytecode_write_typet::ARRAY_REF, "");
3031 
3032  code_assignt array_put{dereference_exprt{data_plus_offset}, op[2]};
3033  block.add(std::move(array_put), location);
3034  return block;
3035 }
3036 
3038  const source_locationt &location,
3039  std::size_t instruction_address,
3040  const exprt &arg0,
3041  codet &result_code)
3042 {
3043  const java_method_typet &method_type = to_java_method_type(arg0.type());
3044  const java_method_typet::parameterst &parameters(method_type.parameters());
3045  const typet &return_type = method_type.return_type();
3046 
3047  // Note these must be popped regardless of whether we understand the lambda
3048  // method or not
3049  code_function_callt::argumentst arguments = pop(parameters.size());
3050 
3051  irep_idt synthetic_class_name =
3052  lambda_synthetic_class_name(method_id, instruction_address);
3053 
3054  if(!symbol_table.has_symbol(synthetic_class_name))
3055  {
3056  // We failed to parse the invokedynamic handle as a Java 8+ lambda;
3057  // give up and return null.
3058  const auto value = zero_initializer(return_type, location, ns);
3059  if(!value.has_value())
3060  {
3061  error().source_location = location;
3062  error() << "failed to zero-initialize return type" << eom;
3063  throw 0;
3064  }
3065  return value;
3066  }
3067 
3068  // Construct an instance of the synthetic class created for this invokedynamic
3069  // site:
3070 
3071  irep_idt constructor_name = id2string(synthetic_class_name) + ".<init>";
3072 
3073  const symbolt &constructor_symbol = ns.lookup(constructor_name);
3074 
3076 
3077  // SyntheticType lambda_new = new SyntheticType;
3078  const reference_typet ref_type =
3079  java_reference_type(struct_tag_typet(synthetic_class_name));
3080  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
3081  const exprt new_instance = tmp_variable("lambda_new", ref_type);
3082  result.add(code_assignt(new_instance, java_new_expr, location));
3083 
3084  // lambda_new.<init>(capture_1, capture_2, ...);
3085  // Add the implicit 'this' parameter:
3086  arguments.insert(arguments.begin(), new_instance);
3089 
3090  code_function_callt constructor_call(
3091  constructor_symbol.symbol_expr(), arguments);
3092  constructor_call.add_source_location() = location;
3093  result.add(constructor_call);
3095  {
3096  needed_lazy_methods->add_needed_method(constructor_symbol.name);
3097  needed_lazy_methods->add_needed_class(synthetic_class_name);
3098  }
3099 
3100  result_code = std::move(result);
3101 
3102  if(return_type.id() == ID_empty)
3103  return {};
3104  else
3105  return new_instance;
3106 }
3107 
3110  const std::vector<method_offsett> &jsr_ret_targets,
3111  const std::vector<
3112  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
3113  &ret_instructions) const
3114 { // Draw edges from every `ret` to every `jsr` successor. Could do better with
3115  // flow analysis to distinguish multiple subroutines within the same function.
3116  for(const auto &retinst : ret_instructions)
3117  {
3118  auto &a_entry = address_map.at(retinst->address);
3119  a_entry.successors.insert(
3120  a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
3121  }
3122 }
3123 
3124 std::vector<java_bytecode_convert_methodt::method_offsett>
3126  const method_offsett address,
3128  const
3129 {
3130  std::vector<method_offsett> result;
3131  for(const auto &exception_row : exception_table)
3132  {
3133  if(address >= exception_row.start_pc && address < exception_row.end_pc)
3134  result.push_back(exception_row.handler_pc);
3135  }
3136  return result;
3137 }
3138 
3152  symbolt &method_symbol,
3154  &local_variable_table,
3155  symbol_table_baset &symbol_table)
3156 {
3157  // Obtain a std::vector of java_method_typet::parametert objects from the
3158  // (function) type of the symbol
3159  java_method_typet &method_type = to_java_method_type(method_symbol.type);
3160  java_method_typet::parameterst &parameters = method_type.parameters();
3161 
3162  // Find number of parameters
3163  unsigned slots_for_parameters = java_method_parameter_slots(method_type);
3164 
3165  // Find parameter names in the local variable table:
3166  typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3167  std::map<std::size_t, base_name_and_identifiert> param_names;
3168  for(const auto &v : local_variable_table)
3169  {
3170  if(v.index < slots_for_parameters)
3171  param_names.emplace(
3172  v.index,
3173  make_pair(
3174  v.name, id2string(method_symbol.name) + "::" + id2string(v.name)));
3175  }
3176 
3177  // Assign names to parameters
3178  std::size_t param_index = 0;
3179  for(auto &param : parameters)
3180  {
3181  irep_idt base_name, identifier;
3182 
3183  // Construct a sensible base name (base_name) and a fully qualified name
3184  // (identifier) for every parameter of the method under translation,
3185  // regardless of whether we have an LVT or not; and assign it to the
3186  // parameter object (which is stored in the type of the symbol, not in the
3187  // symbol table)
3188  if(param_index == 0 && param.get_this())
3189  {
3190  // my.package.ClassName.myMethodName:(II)I::this
3191  base_name = ID_this;
3192  identifier = id2string(method_symbol.name) + "::" + id2string(base_name);
3193  }
3194  else
3195  {
3196  auto param_name = param_names.find(param_index);
3197  if(param_name != param_names.end())
3198  {
3199  base_name = param_name->second.first;
3200  identifier = param_name->second.second;
3201  }
3202  else
3203  {
3204  // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
3205  // variable slot where the parameter is stored and T is a character
3206  // indicating the type
3207  const typet &type = param.type();
3208  char suffix = java_char_from_type(type);
3209  base_name = "arg" + std::to_string(param_index) + suffix;
3210  identifier =
3211  id2string(method_symbol.name) + "::" + id2string(base_name);
3212  }
3213  }
3214  param.set_base_name(base_name);
3215  param.set_identifier(identifier);
3216 
3217  // Build a new symbol for the parameter and add it to the symbol table
3218  parameter_symbolt parameter_symbol;
3219  parameter_symbol.base_name = base_name;
3220  parameter_symbol.mode = ID_java;
3221  parameter_symbol.name = identifier;
3222  parameter_symbol.type = param.type();
3223  symbol_table.insert(parameter_symbol);
3224 
3225  param_index += java_local_variable_slots(param.type());
3226  }
3227 }
3228 
3230  const symbolt &class_symbol,
3231  const java_bytecode_parse_treet::methodt &method,
3232  symbol_table_baset &symbol_table,
3233  message_handlert &message_handler,
3234  size_t max_array_length,
3235  bool throw_assertion_error,
3236  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
3237  java_string_library_preprocesst &string_preprocess,
3238  const class_hierarchyt &class_hierarchy,
3239  bool threading_support,
3240  const optionalt<prefix_filtert> &method_context,
3241  bool assert_no_exceptions_thrown)
3242 
3243 {
3245  symbol_table,
3246  message_handler,
3247  max_array_length,
3248  throw_assertion_error,
3249  needed_lazy_methods,
3250  string_preprocess,
3251  class_hierarchy,
3252  threading_support,
3253  assert_no_exceptions_thrown);
3254 
3255  java_bytecode_convert_method(class_symbol, method, method_context);
3256 }
3257 
3264  const irep_idt &classname,
3265  const irep_idt &mangled_method_name) const
3266 {
3267  const auto inherited_method = get_inherited_method_implementation(
3268  mangled_method_name, classname, symbol_table);
3269 
3270  return inherited_method.has_value();
3271 }
3272 
3279  const irep_idt &class_identifier,
3280  const irep_idt &component_name) const
3281 {
3282  const auto inherited_method = get_inherited_component(
3283  class_identifier, component_name, symbol_table, true);
3284 
3285  INVARIANT(
3286  inherited_method.has_value(), "static field should be in symbol table");
3287 
3288  return inherited_method->get_full_component_identifier();
3289 }
3290 
3298  const std::string &tmp_var_prefix,
3299  code_blockt &block,
3300  const bytecode_write_typet write_type,
3301  const irep_idt &identifier)
3302 {
3303  const std::function<bool(
3304  const std::function<tvt(const exprt &expr)>, const exprt &expr)>
3305  entry_matches = [&entry_matches](
3306  const std::function<tvt(const exprt &expr)> predicate,
3307  const exprt &expr) {
3308  const tvt &tvres = predicate(expr);
3309  if(tvres.is_unknown())
3310  {
3311  return std::any_of(
3312  expr.operands().begin(),
3313  expr.operands().end(),
3314  [&predicate, &entry_matches](const exprt &expr) {
3315  return entry_matches(predicate, expr);
3316  });
3317  }
3318  else
3319  {
3320  return tvres.is_true();
3321  }
3322  };
3323 
3324  // Function that checks whether the expression accesses a member with the
3325  // given identifier name. These accesses are created in the case of `iinc`, or
3326  // non-array `?store` instructions.
3327  const std::function<tvt(const exprt &expr)> has_member_entry = [&identifier](
3328  const exprt &expr) {
3329  const auto member_expr = expr_try_dynamic_cast<member_exprt>(expr);
3330  return !member_expr ? tvt::unknown()
3331  : tvt(member_expr->get_component_name() == identifier);
3332  };
3333 
3334  // Function that checks whether the expression is a symbol with the given
3335  // identifier name. These accesses are created in the case of `putstatic` or
3336  // `putfield` instructions.
3337  const std::function<tvt(const exprt &expr)> is_symbol_entry =
3338  [&identifier](const exprt &expr) {
3339  const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
3340  return !symbol_expr ? tvt::unknown()
3341  : tvt(symbol_expr->get_identifier() == identifier);
3342  };
3343 
3344  // Function that checks whether the expression is a dereference
3345  // expression. These accesses are created in `?astore` array write
3346  // instructions.
3347  const std::function<tvt(const exprt &expr)> is_dereference_entry =
3348  [](const exprt &expr) {
3349  const auto dereference_expr =
3350  expr_try_dynamic_cast<dereference_exprt>(expr);
3351  return !dereference_expr ? tvt::unknown() : tvt(true);
3352  };
3353 
3354  for(auto &stack_entry : stack)
3355  {
3356  bool replace = false;
3357  switch(write_type)
3358  {
3361  replace = entry_matches(is_symbol_entry, stack_entry);
3362  break;
3364  replace = entry_matches(is_dereference_entry, stack_entry);
3365  break;
3367  replace = entry_matches(has_member_entry, stack_entry);
3368  break;
3369  }
3370  if(replace)
3371  {
3373  tmp_var_prefix, stack_entry.type(), block, stack_entry);
3374  }
3375  }
3376 }
3377 
3380  const std::string &tmp_var_prefix,
3381  const typet &tmp_var_type,
3382  code_blockt &block,
3383  exprt &stack_entry)
3384 {
3385  const exprt tmp_var=
3386  tmp_variable(tmp_var_prefix, tmp_var_type);
3387  block.add(code_assignt(tmp_var, stack_entry));
3388  stack_entry=tmp_var;
3389 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
java_bytecode_convert_methodt::instructionst
methodt::instructionst instructionst
Definition: java_bytecode_convert_method_class.h:62
java_bytecode_convert_methodt::convert_invoke
void convert_invoke(source_locationt location, const irep_idt &statement, class_method_descriptor_exprt &class_method_descriptor, codet &c, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2196
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
java_bytecode_convert_methodt::convert_pop
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2001
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
java_static_initializers.h
BC_iinc
#define BC_iinc
Definition: bytecode_info.h:197
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_parse_treet::methodt::throws_exception_table
std::vector< irep_idt > throws_exception_table
Definition: java_bytecode_parse_tree.h:125
java_bytecode_parse_treet::membert::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:68
java_char_from_type
char java_char_from_type(const typet &type)
Definition: java_types.cpp:706
ieee_floatt
Definition: ieee_float.h:120
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
cfg.h
Control Flow Graph.
java_method_typet::add_throws_exception
void add_throws_exception(irep_idt exception)
Definition: java_types.h:134
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_bytecode_convert_methodt::threading_support
const bool threading_support
Definition: java_bytecode_convert_method_class.h:82
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
typet::subtype
const typet & subtype() const
Definition: type.h:47
java_bytecode_convert_methodt::convert_load
exprt convert_load(const exprt &index, char type_char, size_t address)
Load reference from local variable.
Definition: java_bytecode_convert_method.cpp:2961
java_bytecode_parse_treet::methodt::exceptiont::catch_type
struct_tag_typet catch_type
Definition: java_bytecode_parse_tree.h:119
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1439
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:26
java_bytecode_parse_treet::membert::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:70
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
bytecode_infot
Definition: bytecode_info.h:45
BC_ifeq
#define BC_ifeq
Definition: bytecode_info.h:218
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
java_bytecode_convert_methodt::current_method
irep_idt current_method
A copy of method_id :/.
Definition: java_bytecode_convert_method_class.h:91
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:4545
BC_putstatic
#define BC_putstatic
Definition: bytecode_info.h:244
java_bytecode_convert_methodt::method_id
irep_idt method_id
Fully qualified name of the method under translation.
Definition: java_bytecode_convert_method_class.h:88
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
arith_tools.h
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:89
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:126
java_bytecode_parse_treet::methodt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:88
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
java_bytecode_parse_treet::membert::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:71
java_bytecode_convert_methodt::setup_local_variables
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
Definition: java_local_variable_table.cpp:744
get_inherited_method_implementation
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
Definition: resolve_inherited_component.cpp:124
java_bytecode_convert_methodt::convert_if_cmp
code_ifthenelset convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const u1 bytecode, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
Definition: java_bytecode_convert_method.cpp:2868
assign_parameter_names
static void assign_parameter_names(java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
Iterates through the parameters of the function type ftype, finds a new new name for each parameter a...
Definition: java_bytecode_convert_method.cpp:67
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:585
reference_typet
The reference type.
Definition: std_types.h:1553
BC_goto_w
#define BC_goto_w
Definition: bytecode_info.h:265
java_bytecode_convert_methodt::convert_dup2
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2090
BC_ifnonnull
#define BC_ifnonnull
Definition: bytecode_info.h:264
irept::make_nil
void make_nil()
Definition: irep.h:475
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
create_parameter_symbols
void create_parameter_symbols(const java_method_typet::parameterst &parameters, expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet >> &variables, symbol_table_baset &symbol_table)
Definition: java_bytecode_convert_method.cpp:519
java_bytecode_convert_method_class.h
JAVA Bytecode Language Conversion.
typet
The type of an expression, extends irept.
Definition: type.h:29
can_cast_type< reference_typet >
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: std_types.h:1566
BC_pop2
#define BC_pop2
Definition: bytecode_info.h:153
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:86
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:774
BC_jsr
#define BC_jsr
Definition: bytecode_info.h:233
BC_ifgt
#define BC_ifgt
Definition: bytecode_info.h:222
code_switch_caset::set_default
void set_default()
Definition: std_code.h:1451
threeval.h
get_if_cmp_operator
static irep_idt get_if_cmp_operator(const u1 bytecode)
Definition: java_bytecode_convert_method.cpp:642
java_array_element_type
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:145
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
java_bytecode_convert_methodt::try_catch_handler
std::vector< method_offsett > try_catch_handler(method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
Definition: java_bytecode_convert_method.cpp:3125
unsupported_java_class_signature_exceptiont
An exception that is raised for unsupported class signature.
Definition: java_types.h:1132
java_bytecode_parse_treet::methodt::local_variable_table
local_variable_tablet local_variable_table
Definition: java_bytecode_parse_tree.h:138
checked_dereference
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:291
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
java_bytecode_convert_methodt::needed_lazy_methods
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
Definition: java_bytecode_convert_method_class.h:83
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
fieldref_exprt
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Definition: java_bytecode_parse_tree.h:335
java_bytecode_convert_methodt::ns
namespacet ns
Definition: java_bytecode_convert_method_class.h:78
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
java_bytecode_convert_methodt::label
static irep_idt label(const irep_idt &address)
Definition: java_bytecode_convert_method.cpp:167
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:579
java_bytecode_convert_methodt::variable
exprt variable(const exprt &arg, char type_char, size_t address)
Returns an expression indicating a local variable suitable to load/store from a bytecode at address a...
Definition: java_bytecode_convert_method.cpp:205
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:67
java_class_typet::methodt
Definition: java_types.h:243
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:587
java_string_literal_expr.h
Representation of a constant Java string.
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
can_cast_expr< java_string_literal_exprt >
bool can_cast_expr< java_string_literal_exprt >(const exprt &base)
Definition: java_string_literal_expr.h:33
java_bytecode_convert_methodt::convert_iinc
code_blockt convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)
Definition: java_bytecode_convert_method.cpp:2771
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
rem_exprt
Remainder of division.
Definition: std_expr.h:1145
exprt
Base class for all expressions.
Definition: expr.h:53
java_bytecode_convert_methodt::convert_ifnonull
code_ifthenelset convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
Definition: java_bytecode_convert_method.cpp:2822
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
code_push_catcht
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:2248
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
java_bytecode_convert_methodt::block_tree_nodet::branch
std::vector< block_tree_nodet > branch
Definition: java_bytecode_convert_method_class.h:261
java_bytecode_convert_method
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const optionalt< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)
Definition: java_bytecode_convert_method.cpp:3229
java_bytecode_convert_methodt::convert_multianewarray
code_blockt convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2507
java_bytecode_parse_treet::find_annotation
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
Definition: java_bytecode_parse_tree.cpp:97
java_expr.h
Java-specific exprt subclasses.
fieldref_exprt::component_name
irep_idt component_name() const
Definition: java_bytecode_parse_tree.h:352
irep_idt
dstringt irep_idt
Definition: irep.h:32
java_bytecode_convert_methodt::converted_instructiont
Definition: java_bytecode_convert_method_class.h:221
bool_typet
The Boolean type.
Definition: std_types.h:37
tvt::is_unknown
bool is_unknown() const
Definition: threeval.h:27
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:764
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
BC_getstatic
#define BC_getstatic
Definition: bytecode_info.h:243
messaget::eom
static eomt eom
Definition: message.h:297
create_parameter_names
void create_parameter_names(const java_bytecode_parse_treet::methodt &m, const irep_idt &method_identifier, java_method_typet::parameterst &parameters, const java_bytecode_convert_methodt::method_offsett &slots_for_parameters)
Extracts the names of parameters from the local variable table in the method, and uses it to construc...
Definition: java_bytecode_convert_method.cpp:434
java_bytecode_convert_methodt::convert_newarray
code_blockt convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2534
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
BC_irem
#define BC_irem
Definition: bytecode_info.h:177
java_class_typet::methods
const methodst & methods() const
Definition: java_types.h:302
java_bytecode_convert_methodt::convert_ret
code_blockt convert_ret(const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
Definition: java_bytecode_convert_method.cpp:2892
adjust_invoke_argument_types
static void adjust_invoke_argument_types(const java_method_typet::parameterst &parameters, code_function_callt::argumentst &arguments)
Definition: java_bytecode_convert_method.cpp:2172
lshr_exprt
Logical right shift.
Definition: std_expr.h:2614
java_method_typet::set_is_varargs
void set_is_varargs(bool is_varargs)
Definition: java_types.h:164
get_method_identifier
static irep_idt get_method_identifier(const irep_idt &class_identifier, const java_bytecode_parse_treet::methodt &method)
Definition: java_bytecode_convert_method.cpp:425
div_exprt
Division.
Definition: std_expr.h:1031
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
code_pop_catcht
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:2342
java_bytecode_convert_methodt::variables
expanding_vectort< variablest > variables
Definition: java_bytecode_convert_method_class.h:167
java_bytecode_parse_treet::methodt::parameter_annotations
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
Definition: java_bytecode_parse_tree.h:107
namespace.h
java_bytecode_convert_methodt::convert_cmp2
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2704
get_bytecode_type_width
static std::size_t get_bytecode_type_width(const typet &ty)
Definition: java_bytecode_convert_method.cpp:1011
equal_exprt
Equality.
Definition: std_expr.h:1190
java_bytecode_convert_methodt::convert_cmp
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2732
expanding_vectort
Definition: expanding_vector.h:17
BC_putfield
#define BC_putfield
Definition: bytecode_info.h:246
code_typet::get_is_constructor
bool get_is_constructor() const
Definition: std_types.h:887
pattern.h
Pattern matching for bytecode instructions.
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
notequal_exprt
Disequality.
Definition: std_expr.h:1248
code_labelt::code
codet & code()
Definition: std_code.h:1393
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
conditional_array_cast
static exprt conditional_array_cast(const exprt &expr, char type_char)
Add typecast if necessary to expr to make it compatible with array type corresponding to type_char (s...
Definition: java_bytecode_convert_method.cpp:2929
java_bytecode_convert_methodt::convert_instructions
code_blockt convert_instructions(const methodt &)
Definition: java_bytecode_convert_method.cpp:1067
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
cfg_dominators.h
Compute dominators for CFG of goto_function.
ieee_float_spect
Definition: ieee_float.h:26
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
java_bytecode_convert_methodt::block_tree_nodet::get_leaf
static block_tree_nodet get_leaf()
Definition: java_bytecode_convert_method_class.h:271
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
BC_drem
#define BC_drem
Definition: bytecode_info.h:180
BC_monitorenter
#define BC_monitorenter
Definition: bytecode_info.h:259
java_bytecode_convert_methodt::variablet::symbol_expr
symbol_exprt symbol_expr
Definition: java_bytecode_convert_method_class.h:124
java_bytecode_parse_treet::membert::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:67
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:417
BC_ldc
#define BC_ldc
Definition: bytecode_info.h:83
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
string2int.h
class_method_descriptor_exprt::get_identifier
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition: std_expr.h:4568
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
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:1183
java_method_typet::set_native
void set_native(bool is_native)
Definition: java_types.h:154
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
expr_initializer.h
Expression Initialization.
java_bytecode_convert_methodt::convert_new
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2592
bitxor_exprt
Bit-wise XOR.
Definition: std_expr.h:2424
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_bytecode_convert_methodt::convert_switch
code_switcht convert_switch(const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:2017
java_type_from_char
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
Definition: java_types.cpp:247
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2388
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
ieee_float_spect::double_precision
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
BC_dup2
#define BC_dup2
Definition: bytecode_info.h:157
or_exprt
Boolean OR.
Definition: std_expr.h:2245
java_bytecode_convert_methodt::get_clinit_call
codet get_clinit_call(const irep_idt &classname)
Each static access to classname should be prefixed with a check for necessary static init; this retur...
Definition: java_bytecode_convert_method.cpp:996
code_typet::get_access
const irep_idt & get_access() const
Definition: std_types.h:877
java_bytecode_convert_methodt::convert_if
code_ifthenelset convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const
Definition: java_bytecode_convert_method.cpp:2844
convert_annotations
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
Convert parsed annotations into the symbol table.
Definition: java_bytecode_convert_class.cpp:1134
java_bytecode_parse_treet::membert::is_static
bool is_static
Definition: java_bytecode_parse_tree.h:70
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
class_method_descriptor_exprt::base_method_name
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
Definition: std_expr.h:4560
member_type_lazy
java_method_typet member_type_lazy(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler)
Returns the member type for a method, based on signature or descriptor.
Definition: java_bytecode_convert_method.cpp:238
java_bytecode_convert_methodt::method_return_type
typet method_return_type
Return type of the method under conversion.
Definition: java_bytecode_convert_method_class.h:95
java_bytecode_convert_methodt::max_array_length
const size_t max_array_length
Definition: java_bytecode_convert_method_class.h:79
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_bytecode_convert_methodt::tmp_vars
std::list< symbol_exprt > tmp_vars
Definition: java_bytecode_convert_method_class.h:195
BC_nop
#define BC_nop
Definition: bytecode_info.h:65
java_bytecode_convert_methodt::get_static_field
irep_idt get_static_field(const irep_idt &class_identifier, const irep_idt &component_name) const
Get static field identifier referred to by class_identifier.component_name Note this may be inherited...
Definition: java_bytecode_convert_method.cpp:3278
java_bytecode_convert_methodt::get_or_create_block_for_pcrange
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge=true)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
Definition: java_bytecode_convert_method.cpp:778
java_bytecode_convert_methodt::method_offsett
uint16_t method_offsett
Definition: java_bytecode_convert_method_class.h:74
java_bytecode_parse_treet::methodt::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:90
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
branch
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:20
java_bytecode_convert_methodt::throw_assertion_error
const bool throw_assertion_error
Definition: java_bytecode_convert_method_class.h:80
BC_newarray
#define BC_newarray
Definition: bytecode_info.h:253
to_code_goto
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1161
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
code_typet::set_is_constructor
void set_is_constructor()
Definition: std_types.h:892
bytecode_infot::pop
unsigned pop
Definition: bytecode_info.h:49
java_bytecode_parse_treet::methodt::instructions
instructionst instructions
Definition: java_bytecode_parse_tree.h:93
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1127
java_bytecode_convert_methodt::assert_no_exceptions_thrown
const bool assert_no_exceptions_thrown
Definition: java_bytecode_convert_method_class.h:81
java_bytecode_convert_methodt::bytecode_write_typet::STATIC_FIELD
@ STATIC_FIELD
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
BC_new
#define BC_new
Definition: bytecode_info.h:252
BC_multianewarray
#define BC_multianewarray
Definition: bytecode_info.h:262
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
java_bytecode_convert_methodt::find_variable_for_slot
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
Definition: java_local_variable_table.cpp:858
BC_frem
#define BC_frem
Definition: bytecode_info.h:179
BC_swap
#define BC_swap
Definition: bytecode_info.h:160
java_string_library_preprocesst::replace_character_call
codet replace_character_call(code_function_callt call)
Definition: java_string_library_preprocess.h:54
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1420
BC_iconst_m1
#define BC_iconst_m1
Definition: bytecode_info.h:67
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
java_array_type
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:110
BC_aconst_null
#define BC_aconst_null
Definition: bytecode_info.h:66
java_bytecode_convert_methodt::block_tree_nodet::branch_addresses
std::vector< method_offsett > branch_addresses
Definition: java_bytecode_convert_method_class.h:260
java_bytecode_convert_methodt::slots_for_parameters
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
Definition: java_bytecode_convert_method_class.h:102
BC_ifge
#define BC_ifge
Definition: bytecode_info.h:221
bytecode_info.h
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
uncaught_exceptions_domaint::get_exception_type
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Definition: uncaught_exceptions_analysis.cpp:18
java_bytecode_parse_treet::methodt::exceptiont
Definition: java_bytecode_parse_tree.h:110
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:2303
BC_anewarray
#define BC_anewarray
Definition: bytecode_info.h:254
BC_invokedynamic
#define BC_invokedynamic
Definition: bytecode_info.h:251
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
BC_invokespecial
#define BC_invokespecial
Definition: bytecode_info.h:248
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
BC_iflt
#define BC_iflt
Definition: bytecode_info.h:220
java_bytecode_convert_methodt::convert_dup2_x1
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2103
java_bytecode_parse_treet::methodt::base_name
irep_idt base_name
Definition: java_bytecode_parse_tree.h:87
irept::swap
void swap(irept &irep)
Definition: irep.h:463
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
java_bytecode_convert_methodt::method_has_this
bool method_has_this
Definition: java_bytecode_convert_method_class.h:169
pretty_signature
std::string pretty_signature(const java_method_typet &method_type)
Definition: java_types.cpp:1123
java_bytecode_convert_methodt::convert_putstatic
code_blockt convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
Definition: java_bytecode_convert_method.cpp:2616
java_bytecode_convert_methodt::bytecode_write_typet::VARIABLE
@ VARIABLE
java_bytecode_parse_treet::methodt::exceptiont::handler_pc
std::size_t handler_pc
Definition: java_bytecode_parse_tree.h:118
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
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_methodt::convert_ushr
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2752
java_bytecode_convert_method.h
JAVA Bytecode Language Conversion.
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
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
java_bytecode_convert_methodt::convert_getstatic
void convert_getstatic(const source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2658
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
dstringt::empty
bool empty() const
Definition: dstring.h:88
BC_ifne
#define BC_ifne
Definition: bytecode_info.h:219
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
java_reference_array_type
java_reference_typet java_reference_array_type(const struct_tag_typet &subtype)
Definition: java_types.cpp:540
java_bytecode_convert_methodt::bytecode_write_typet::ARRAY_REF
@ ARRAY_REF
BC_dup_x1
#define BC_dup_x1
Definition: bytecode_info.h:155
BC_invokevirtual
#define BC_invokevirtual
Definition: bytecode_info.h:247
java_bytecode_parse_treet::membert::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:70
code_labelt::set_label
void set_label(const irep_idt &label)
Definition: std_code.h:1388
java_local_variable_slots
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Definition: java_utils.cpp:134
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2460
BC_ifle
#define BC_ifle
Definition: bytecode_info.h:223
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
ieee_floatt::from_integer
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:511
java_bytecode_convert_methodt::convert_checkcast
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2372
java_bytecode_convert_methodt::get_block_for_pcrange
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
Definition: java_bytecode_convert_method.cpp:741
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_type_from_string
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
Definition: java_types.cpp:560
get_inherited_component
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:458
tvt
Definition: threeval.h:20
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
minus_exprt
Binary minus.
Definition: std_expr.h:940
java_bytecode_parse_treet::methodt::exceptiont::end_pc
std::size_t end_pc
Definition: java_bytecode_parse_tree.h:117
code_typet::has_this
bool has_this() const
Definition: std_types.h:818
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:787
java_bytecode_parse_treet::methodt::exception_tablet
std::vector< exceptiont > exception_tablet
Definition: java_bytecode_parse_tree.h:122
remove_returns.h
Replace function returns by assignments to global variables.
remove_exceptions.h
Remove function exceptional returns.
java_bytecode_convert_methodt
Definition: java_bytecode_convert_method_class.h:33
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:807
source_locationt
Definition: source_location.h:20
java_bytecode_convert_methodt::convert_putfield
code_blockt convert_putfield(const fieldref_exprt &arg0, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2647
java_bytecode_parse_treet::methodt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:89
simplify_expr.h
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
java_bytecode_convert_methodt::convert_const
exprt::operandst & convert_const(const irep_idt &statement, const constant_exprt &arg0, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2137
bytecode_infot::push
unsigned push
Definition: bytecode_info.h:49
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:3405
java_bytecode_convert_methodt::string_preprocess
java_string_library_preprocesst & string_preprocess
Definition: java_bytecode_convert_method_class.h:97
lambda_synthesis.h
Java lambda code synthesis.
merge_source_location_rec
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:207
java_bytecode_convert_methodt::do_exception_handling
codet & do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)
Definition: java_bytecode_convert_method.cpp:2426
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
java_method_typet::set_is_final
void set_is_final(bool is_final)
Definition: java_types.h:144
java_bytecode_convert_methodt::create_stack_tmp_var
void create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)
actually create a temporary variable to hold the value of a stack entry
Definition: java_bytecode_convert_method.cpp:3379
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
BC_ret
#define BC_ret
Definition: bytecode_info.h:234
BC_athrow
#define BC_athrow
Definition: bytecode_info.h:256
BC_dup_x2
#define BC_dup_x2
Definition: bytecode_info.h:156
class_hierarchy.h
Class Hierarchy.
BC_tableswitch
#define BC_tableswitch
Definition: bytecode_info.h:235
java_bytecode_parse_treet::membert::name
irep_idt name
Definition: java_bytecode_parse_tree.h:69
fieldref_exprt::class_name
irep_idt class_name() const
Definition: java_bytecode_parse_tree.h:347
java_bytecode_convert_methodt::block_tree_nodet::leaf
bool leaf
Definition: java_bytecode_convert_method_class.h:259
java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:137
java_bytecode_parse_treet::instructiont::argst
std::vector< exprt > argst
Definition: java_bytecode_parse_tree.h:61
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
java_bytecode_convert_method_lazy
void java_bytecode_convert_method_lazy(symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.
Definition: java_bytecode_convert_method.cpp:308
java_method_parameter_slots
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call,...
Definition: java_utils.cpp:153
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
java_bytecode_parse_treet::membert::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:70
java_bytecode_convert_methodt::convert_ifnull
code_ifthenelset convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
Definition: java_bytecode_convert_method.cpp:2800
code_landingpadt
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:2379
u1
uint8_t u1
Definition: bytecode_info.h:55
java_bytecode_parse_treet::membert::is_private
bool is_private
Definition: java_bytecode_parse_tree.h:70
java_bytecode_convert_methodt::pop
exprt::operandst pop(std::size_t n)
Definition: java_bytecode_convert_method.cpp:133
java_bytecode_parse_treet::methodt::is_native
bool is_native
Definition: java_bytecode_parse_tree.h:88
BC_idiv
#define BC_idiv
Definition: bytecode_info.h:173
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
java_bytecode_convert_methodt::used_local_names
std::set< symbol_exprt > used_local_names
Definition: java_bytecode_convert_method_class.h:168
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
java_bytecode_parse_treet::methodt::is_bridge
bool is_bridge
Definition: java_bytecode_parse_tree.h:89
code_push_catcht::exception_listt
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2292
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
java_bytecode_parse_treet::methodt::exception_table
exception_tablet exception_table
Definition: java_bytecode_parse_tree.h:123
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
ieee_float.h
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:87
java_bytecode_convert_methodt::address_mapt
std::map< method_offsett, converted_instructiont > address_mapt
Definition: java_bytecode_convert_method_class.h:238
ashr_exprt
Arithmetic right shift.
Definition: std_expr.h:2599
uncaught_exceptions_analysis.h
Over-approximative uncaught exceptions analysis.
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
symbolt::is_type
bool is_type
Definition: symbol.h:61
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:36
java_bytecode_parse_treet::methodt::is_varargs
bool is_varargs
Definition: java_bytecode_parse_tree.h:89
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
BC_monitorexit
#define BC_monitorexit
Definition: bytecode_info.h:260
BC_return
#define BC_return
Definition: bytecode_info.h:242
java_bytecode_parse_treet::methodt::is_synchronized
bool is_synchronized
Definition: java_bytecode_parse_tree.h:88
BC_lookupswitch
#define BC_lookupswitch
Definition: bytecode_info.h:236
java_bytecode_promotion
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:268
BC_dup
#define BC_dup
Definition: bytecode_info.h:154
code_typet::parametert
Definition: std_types.h:753
java_bytecode_parse_treet::methodt::exceptiont::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:116
java_bytecode_convert_methodt::push
void push(const exprt::operandst &o)
Definition: java_bytecode_convert_method.cpp:158
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
BC_invokestatic
#define BC_invokestatic
Definition: bytecode_info.h:249
clinit_wrapper_name
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
Definition: java_static_initializers.cpp:65
BC_instanceof
#define BC_instanceof
Definition: bytecode_info.h:258
class_method_descriptor_exprt::class_id
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition: std_expr.h:4553
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
java_bytecode_convert_methodt::convert_monitorenterexit
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
Definition: java_bytecode_convert_method.cpp:2067
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2200
java_bytecode_convert_methodt::convert_parameter_annotations
code_blockt convert_parameter_annotations(const methodt &method, const java_method_typet &method_type)
Definition: java_bytecode_convert_method.cpp:1018
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
java_bytecode_convert_methodt::block_tree_nodet
Definition: java_bytecode_convert_method_class.h:258
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< method_offsett > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
Definition: java_bytecode_convert_method.cpp:3108
java_method_typet::set_is_synthetic
void set_is_synthetic(bool is_synthetic)
Definition: java_types.h:174
java_bytecode_convert_methodt::tmp_variable
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
Definition: java_bytecode_convert_method.cpp:172
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
java_bytecode_convert_methodt::convert_astore
code_blockt convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:3007
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:301
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:97
java_reference_typet
This is a specialization of reference_typet.
Definition: java_types.h:605
patternt
Given a string of the format '?blah?', will return true when compared against a string that matches a...
Definition: pattern.h:21
java_bytecode_convert_methodt::variablest
std::vector< variablet > variablest
Definition: java_bytecode_convert_method_class.h:166
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
exprt::operands
operandst & operands()
Definition: expr.h:95
r
static int8_t r
Definition: irep_hash.h:59
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
messaget::debug
mstreamt & debug() const
Definition: message.h:429
java_bytecode_convert_methodt::convert
void convert(const symbolt &class_symbol, const methodt &, const optionalt< prefix_filtert > &method_context)
Definition: java_bytecode_convert_method.cpp:546
BC_arraylength
#define BC_arraylength
Definition: bytecode_info.h:255
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
BC_jsr_w
#define BC_jsr_w
Definition: bytecode_info.h:266
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
java_types.h
java_bytecode_convert_methodt::convert_dup2_x2
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
Definition: java_bytecode_convert_method.cpp:2116
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
BC_dup2_x1
#define BC_dup2_x1
Definition: bytecode_info.h:158
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_bytecode_convert_methodt::pop_residue
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
Definition: java_bytecode_convert_method.cpp:151
BC_ldc_w
#define BC_ldc_w
Definition: bytecode_info.h:84
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:38
is_constructor
static bool is_constructor(const irep_idt &method_name)
Definition: java_bytecode_convert_method.cpp:128
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
java_bytecode_convert_methodt::convert_invoke_dynamic
optionalt< exprt > convert_invoke_dynamic(const source_locationt &location, std::size_t instruction_address, const exprt &arg0, codet &result_code)
Definition: java_bytecode_convert_method.cpp:3037
BC_lrem
#define BC_lrem
Definition: bytecode_info.h:178
java_utils.h
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3689
BC_checkcast
#define BC_checkcast
Definition: bytecode_info.h:257
BC_ldiv
#define BC_ldiv
Definition: bytecode_info.h:174
to_member
static member_exprt to_member(const exprt &pointer, const fieldref_exprt &field_reference, const namespacet &ns)
Build a member exprt for accessing a specific field that may come from a base class.
Definition: java_bytecode_convert_method.cpp:668
BC_pop
#define BC_pop
Definition: bytecode_info.h:152
std_expr.h
API to expression classes.
java_bytecode_convert_methodt::variablet
Definition: java_bytecode_convert_method_class.h:122
java_bytecode_convert_methodt::bytecode_write_typet
bytecode_write_typet
Definition: java_bytecode_convert_method_class.h:320
java_bytecode_convert_methodt::convert_athrow
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Definition: java_bytecode_convert_method.cpp:2388
ieee_float_spect::single_precision
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
java_method_typet
Definition: java_types.h:103
BC_goto
#define BC_goto
Definition: bytecode_info.h:232
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
java_bytecode_convert_methodt::replace_call_to_cprover_assume
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
Definition: java_bytecode_convert_method.cpp:2357
java_bytecode_convert_methodt::is_method_inherited
bool is_method_inherited(const irep_idt &classname, const irep_idt &mangled_method_name) const
Returns true iff method methodid from class classname is a method inherited from a class or interface...
Definition: java_bytecode_convert_method.cpp:3263
c_types.h
java_bytecode_convert_methodt::replace_goto_target
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
Definition: java_bytecode_convert_method.cpp:707
code_typet::set_access
void set_access(const irep_idt &access)
Definition: std_types.h:882
java_bytecode_convert_methodt::stack
stackt stack
Definition: java_bytecode_convert_method_class.h:204
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
java_bytecode_convert_methodt::bytecode_write_typet::FIELD
@ FIELD
gather_symbol_live_ranges
static void gather_symbol_live_ranges(java_bytecode_convert_methodt::method_offsett pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
Definition: java_bytecode_convert_method.cpp:957
java_bytecode_initialize_parameter_names
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
Definition: java_bytecode_convert_method.cpp:3151
java_bytecode_convert_methodt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_convert_method_class.h:77
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
can_cast_type< bitvector_typet >
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:1064
java_instanceof_exprt
Definition: java_expr.h:18
BC_invokeinterface
#define BC_invokeinterface
Definition: bytecode_info.h:250
validation_modet::INVARIANT
@ INVARIANT
mod_exprt
Modulo.
Definition: std_expr.h:1100
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
java_bytecode_convert_methodt::convert_aload
static exprt convert_aload(const irep_idt &statement, const exprt::operandst &op)
Definition: java_bytecode_convert_method.cpp:2941
tvt::is_true
bool is_true() const
Definition: threeval.h:25
BC_ldc2_w
#define BC_ldc2_w
Definition: bytecode_info.h:85
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
shl_exprt
Left shift.
Definition: std_expr.h:2561
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3509
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:136
ieee_floatt::from_expr
void from_expr(const constant_exprt &expr)
Definition: ieee_float.cpp:1063
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
BC_getfield
#define BC_getfield
Definition: bytecode_info.h:245
java_bytecode_convert_methodt::convert_store
code_blockt convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
Definition: java_bytecode_convert_method.cpp:2982
java_bytecode_convert_methodt::save_stack_entries
void save_stack_entries(const std::string &, code_blockt &, const bytecode_write_typet, const irep_idt &)
Create temporary variables if a write instruction can have undesired side- effects.
Definition: java_bytecode_convert_method.cpp:3297
BC_dup2_x2
#define BC_dup2_x2
Definition: bytecode_info.h:159
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
BC_ifnull
#define BC_ifnull
Definition: bytecode_info.h:263