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 
18 #include "bytecode_info.h"
21 #include "java_types.h"
22 #include "java_utils.h"
23 #include "remove_exceptions.h"
24 
25 #include <util/arith_tools.h>
26 #include <util/c_types.h>
27 #include <util/expr_initializer.h>
28 #include <util/ieee_float.h>
29 #include <util/invariant.h>
30 #include <util/namespace.h>
31 #include <util/prefix.h>
32 #include <util/simplify_expr.h>
33 #include <util/std_expr.h>
34 #include <util/string2int.h>
35 #include <util/string_constant.h>
36 
37 #include <goto-programs/cfg.h>
40 
43 
44 #include <limits>
45 #include <algorithm>
46 #include <functional>
47 #include <unordered_set>
48 #include <regex>
49 
53 class patternt
54 {
55 public:
56  explicit patternt(const char *_p):p(_p)
57  {
58  }
59 
60  // match with '?'
61  bool operator==(const irep_idt &what) const
62  {
63  for(std::size_t i=0; i<what.size(); i++)
64  if(p[i]==0)
65  return false;
66  else if(p[i]!='?' && p[i]!=what[i])
67  return false;
68 
69  return p[what.size()]==0;
70  }
71 
72 protected:
73  const char *p;
74 };
75 
89  code_typet &ftype,
90  const irep_idt &name_prefix,
91  symbol_table_baset &symbol_table)
92 {
93  code_typet::parameterst &parameters=ftype.parameters();
94 
95  // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out.
96  // assign names to parameters
97  for(std::size_t i=0; i<parameters.size(); ++i)
98  {
99  irep_idt base_name, identifier;
100 
101  if(i==0 && parameters[i].get_this())
102  base_name="this";
103  else
104  base_name="stub_ignored_arg"+std::to_string(i);
105 
106  identifier=id2string(name_prefix)+"::"+id2string(base_name);
107  parameters[i].set_base_name(base_name);
108  parameters[i].set_identifier(identifier);
109 
110  // add to symbol table
111  parameter_symbolt parameter_symbol;
112  parameter_symbol.base_name=base_name;
113  parameter_symbol.mode=ID_java;
114  parameter_symbol.name=identifier;
115  parameter_symbol.type=parameters[i].type();
116  symbol_table.add(parameter_symbol);
117  }
118 }
119 
120 static bool operator==(const irep_idt &what, const patternt &pattern)
121 {
122  return pattern==what;
123 }
124 
125 static bool is_constructor(const irep_idt &method_name)
126 {
127  return id2string(method_name).find("<init>") != std::string::npos;
128 }
129 
131 {
132  if(stack.size()<n)
133  {
134  error() << "malformed bytecode (pop too high)" << eom;
135  throw 0;
136  }
137 
138  exprt::operandst operands;
139  operands.resize(n);
140  for(std::size_t i=0; i<n; i++)
141  operands[i]=stack[stack.size()-n+i];
142 
143  stack.resize(stack.size()-n);
144  return operands;
145 }
146 
149 {
150  std::size_t residue_size=std::min(n, stack.size());
151 
152  stack.resize(stack.size()-residue_size);
153 }
154 
156 {
157  stack.resize(stack.size()+o.size());
158 
159  for(std::size_t i=0; i<o.size(); i++)
160  stack[stack.size()-o.size()+i]=o[i];
161 }
162 
163 // JVM program locations
165 {
166  return "pc"+id2string(address);
167 }
168 
170  const std::string &prefix,
171  const typet &type)
172 {
173  irep_idt base_name=prefix+"_tmp"+std::to_string(tmp_vars.size());
174  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
175 
176  auxiliary_symbolt tmp_symbol;
177  tmp_symbol.base_name=base_name;
178  tmp_symbol.is_static_lifetime=false;
179  tmp_symbol.mode=ID_java;
180  tmp_symbol.name=identifier;
181  tmp_symbol.type=type;
182  symbol_table.add(tmp_symbol);
183 
184  symbol_exprt result(identifier, type);
185  result.set(ID_C_base_name, base_name);
186  tmp_vars.push_back(result);
187 
188  return result;
189 }
190 
207  const exprt &arg,
208  char type_char,
209  size_t address,
211 {
212  mp_integer number;
213  bool ret=to_integer(to_constant_expr(arg), number);
214  CHECK_RETURN(!ret);
215 
216  std::size_t number_int=integer2size_t(number);
217  typet t=java_type_from_char(type_char);
218  variablest &var_list=variables[number_int];
219 
220  // search variable in list for correct frame / address if necessary
221  const variablet &var=
222  find_variable_for_slot(address, var_list);
223 
224  if(var.symbol_expr.get_identifier().empty())
225  {
226  // an unnamed local variable
227  irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
228  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
229 
230  symbol_exprt result(identifier, t);
231  result.set(ID_C_base_name, base_name);
232  used_local_names.insert(result);
233  return result;
234  }
235  else
236  {
238  if(do_cast==CAST_AS_NEEDED && t!=result.type())
240  return result;
241  }
242 }
243 
258  const std::string &descriptor,
259  const optionalt<std::string> &signature,
260  const std::string &class_name,
261  const std::string &method_name,
263 {
264  // In order to construct the method type, we can either use signature or
265  // descriptor. Since only signature contains the generics info, we want to
266  // use signature whenever possible. We revert to using descriptor if (1) the
267  // signature does not exist, (2) an unsupported generics are present or
268  // (3) in the special case when the number of parameters in the descriptor
269  // does not match the number of parameters in the signature - e.g. for
270  // certain types of inner classes and enums (see unit tests for examples).
271 
272  messaget message(message_handler);
273 
274  typet member_type_from_descriptor=java_type_from_string(descriptor);
275  INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
276  if(signature.has_value())
277  {
278  try
279  {
280  typet member_type_from_signature=java_type_from_string(
281  signature.value(),
282  class_name);
283  INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
284  if(to_code_type(member_type_from_signature).parameters().size()==
285  to_code_type(member_type_from_descriptor).parameters().size())
286  {
287  return to_code_type(member_type_from_signature);
288  }
289  else
290  {
291  message.warning() << "Method: " << class_name << "." << method_name
292  << "\n signature: " << signature.value()
293  << "\n descriptor: " << descriptor
294  << "\n different number of parameters, reverting to "
295  "descriptor"
296  << message.eom;
297  }
298  }
300  {
301  message.warning() << "Method: " << class_name << "." << method_name
302  << "\n could not parse signature: " << signature.value()
303  << "\n " << e.what() << "\n"
304  << " reverting to descriptor: " << descriptor
305  << message.eom;
306  }
307  }
308  return to_code_type(member_type_from_descriptor);
309 }
310 
318  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
319  const size_t index)
320 {
321  const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
322  // If the lambda method handle has an unknown type, it does not refer to
323  // any symbol (it is a symbol expression with empty identifier)
324  if(!lambda_method_handle.get_identifier().empty())
325  return symbol_table.lookup_ref(lambda_method_handle.get_identifier());
326  return {};
327 }
328 
339  const symbolt &class_symbol,
340  const irep_idt &method_identifier,
342  symbol_tablet &symbol_table,
344 {
345  symbolt method_symbol;
346 
347  code_typet member_type = member_type_lazy(
348  m.descriptor,
349  m.signature,
350  id2string(class_symbol.name),
351  id2string(m.base_name),
353 
354  method_symbol.name=method_identifier;
355  method_symbol.base_name=m.base_name;
356  method_symbol.mode=ID_java;
357  method_symbol.location=m.source_location;
358  method_symbol.location.set_function(method_identifier);
359 
360  if(m.is_public)
361  member_type.set_access(ID_public);
362  else if(m.is_protected)
363  member_type.set_access(ID_protected);
364  else if(m.is_private)
365  member_type.set_access(ID_private);
366  else
367  member_type.set_access(ID_default);
368 
369  // do we need to add 'this' as a parameter?
370  if(!m.is_static)
371  {
372  code_typet::parameterst &parameters = member_type.parameters();
373  code_typet::parametert this_p;
374  const reference_typet object_ref_type=
375  java_reference_type(symbol_typet(class_symbol.name));
376  this_p.type()=object_ref_type;
377  this_p.set_this();
378  parameters.insert(parameters.begin(), this_p);
379  }
380 
381  const std::string signature_string = pretty_signature(member_type);
382 
383  if(is_constructor(method_symbol.base_name))
384  {
385  // we use full.class_name(...) as pretty name
386  // for constructors -- the idea is that they have
387  // an empty declarator.
388  method_symbol.pretty_name=
389  id2string(class_symbol.pretty_name) + signature_string;
390 
391  member_type.set_is_constructor();
392  }
393  else
394  {
395  method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
396  id2string(m.base_name) + signature_string;
397  }
398 
399  // Load annotations
400  if(!m.annotations.empty())
401  {
403  m.annotations,
404  type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
405  .get_annotations());
406  }
407 
408  method_symbol.type=member_type;
409  // Not used in jbmc at present, but other codebases that use jbmc as a library
410  // use this information.
411  method_symbol.type.set(ID_C_abstract, m.is_abstract);
412 
414  m.annotations, "java::org.cprover.MustNotThrow"))
415  {
416  method_symbol.type.set(ID_C_must_not_throw, true);
417  }
418 
419  symbol_table.add(method_symbol);
420 }
421 
423  const symbolt &class_symbol,
424  const methodt &m)
425 {
426  // Construct the fully qualified method name
427  // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
428  // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
429  // associated to the method
430  const irep_idt method_identifier=
431  id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
432  method_id=method_identifier;
433 
434  symbolt &method_symbol=*symbol_table.get_writeable(method_identifier);
435 
436  // Obtain a std::vector of code_typet::parametert objects from the
437  // (function) type of the symbol
438  code_typet code_type = to_code_type(method_symbol.type);
439  code_type.set(ID_C_class, class_symbol.name);
440  method_return_type=code_type.return_type();
441  code_typet::parameterst &parameters=code_type.parameters();
442 
443  // Determine the number of local variable slots used by the JVM to maintan the
444  // formal parameters
446 
447  debug() << "Generating codet: class "
448  << class_symbol.name << ", method "
449  << m.name << eom;
450 
451  // We now set up the local variables for the method parameters
452  variables.clear();
453 
454  // Find parameter names in the local variable table:
455  for(const auto &v : m.local_variable_table)
456  {
457  // Skip this variable if it is not a method parameter
458  if(!is_parameter(v))
459  continue;
460 
461  // Construct a fully qualified name for the parameter v,
462  // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
463  // symbol_exprt with the parameter and its type
464  typet t;
465  if(v.signature.has_value())
466  {
468  v.descriptor,
469  v.signature,
470  id2string(class_symbol.name));
471  }
472  else
473  t=java_type_from_string(v.descriptor);
474 
475  std::ostringstream id_oss;
476  id_oss << method_id << "::" << v.name;
477  irep_idt identifier(id_oss.str());
478  symbol_exprt result(identifier, t);
479  result.set(ID_C_base_name, v.name);
480 
481  // Create a new variablet in the variables vector; in fact this entry will
482  // be rewritten below in the loop that iterates through the method
483  // parameters; the only field that seem to be useful to write here is the
484  // symbol_expr, others will be rewritten
485  variables[v.index].push_back(variablet());
486  auto &newv=variables[v.index].back();
487  newv.symbol_expr=result;
488  newv.start_pc=v.start_pc;
489  newv.length=v.length;
490  }
491 
492  // The variables is a expanding_vectort, and the loop above may have expanded
493  // the vector introducing gaps where the entries are empty vectors. We now
494  // make sure that the vector of each LV slot contains exactly one variablet,
495  // possibly default-initialized
496  std::size_t param_index=0;
497  for(const auto &param : parameters)
498  {
499  variables[param_index].resize(1);
500  param_index+=java_local_variable_slots(param.type());
501  }
502  INVARIANT(
503  param_index==slots_for_parameters,
504  "java_parameter_count and local computation must agree");
505 
506  // Assign names to parameters
507  param_index=0;
508  for(auto &param : parameters)
509  {
510  irep_idt base_name, identifier;
511 
512  // Construct a sensible base name (base_name) and a fully qualified name
513  // (identifier) for every parameter of the method under translation,
514  // regardless of whether we have an LVT or not; and assign it to the
515  // parameter object (which is stored in the type of the symbol, not in the
516  // symbol table)
517  if(param_index==0 && param.get_this())
518  {
519  // my.package.ClassName.myMethodName:(II)I::this
520  base_name="this";
521  identifier=id2string(method_identifier)+"::"+id2string(base_name);
522  }
523  else
524  {
525  // if already present in the LVT ...
526  base_name=variables[param_index][0].symbol_expr.get(ID_C_base_name);
527  identifier=variables[param_index][0].symbol_expr.get(ID_identifier);
528 
529  // ... then base_name will not be empty
530  if(base_name.empty())
531  {
532  // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
533  // variable slot where the parameter is stored and T is a character
534  // indicating the type
535  const typet &type=param.type();
536  char suffix=java_char_from_type(type);
537  base_name="arg"+std::to_string(param_index)+suffix;
538  identifier=id2string(method_identifier)+"::"+id2string(base_name);
539  }
540  }
541  param.set_base_name(base_name);
542  param.set_identifier(identifier);
543 
544  // Build a new symbol for the parameter and add it to the symbol table
545  parameter_symbolt parameter_symbol;
546  parameter_symbol.base_name=base_name;
547  parameter_symbol.mode=ID_java;
548  parameter_symbol.name=identifier;
549  parameter_symbol.type=param.type();
550  symbol_table.add(parameter_symbol);
551 
552  // Add as a JVM local variable
553  variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
554  variables[param_index][0].is_parameter=true;
555  variables[param_index][0].start_pc=0;
556  variables[param_index][0].length=std::numeric_limits<size_t>::max();
557  param_index+=java_local_variable_slots(param.type());
558  }
559 
560  // The parameter slots detected in this function should agree with what
561  // java_parameter_count() thinks about this method
562  INVARIANT(
563  param_index==slots_for_parameters,
564  "java_parameter_count and local computation must agree");
565 
566  // Check the fields that can't change are valid
567  INVARIANT(
568  method_symbol.name == method_identifier,
569  "Name of method symbol shouldn't change");
570  INVARIANT(
571  method_symbol.base_name == m.base_name,
572  "Base name of method symbol shouldn't change");
573  INVARIANT(
574  method_symbol.module.empty(),
575  "Method symbol shouldn't have module");
576  // Update the symbol for the method
577  method_symbol.mode=ID_java;
578  method_symbol.location=m.source_location;
579  method_symbol.location.set_function(method_identifier);
580 
581  const std::string signature_string = pretty_signature(code_type);
582 
583  // Set up the pretty name for the method entry in the symbol table.
584  // The pretty name of a constructor includes the base name of the class
585  // instead of the internal method name "<init>". For regular methods, it's
586  // just the base name of the method.
587  if(is_constructor(method_symbol.base_name))
588  {
589  // we use full.class_name(...) as pretty name
590  // for constructors -- the idea is that they have
591  // an empty declarator.
592  method_symbol.pretty_name =
593  id2string(class_symbol.pretty_name) + signature_string;
594  INVARIANT(
595  code_type.get_is_constructor(),
596  "Member type should have already been marked as a constructor");
597  }
598  else
599  {
600  method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
601  id2string(m.base_name) + signature_string;
602  }
603 
604  method_symbol.type = code_type;
605 
606  current_method=method_symbol.name;
607  method_has_this=code_type.has_this();
608  if((!m.is_abstract) && (!m.is_native))
609  method_symbol.value = convert_instructions(
610  m,
611  code_type,
612  method_symbol.name,
614 }
615 
617  const irep_idt &statement)
618 {
619  for(const bytecode_infot *p=bytecode_info; p->mnemonic!=nullptr; p++)
620  if(statement==p->mnemonic)
621  return *p;
622 
623  error() << "failed to find bytecode mnemonic `"
624  << statement << '\'' << eom;
625  throw 0;
626 }
627 
629 {
630  if(stmt==patternt("if_?cmplt"))
631  return ID_lt;
632  if(stmt==patternt("if_?cmple"))
633  return ID_le;
634  if(stmt==patternt("if_?cmpgt"))
635  return ID_gt;
636  if(stmt==patternt("if_?cmpge"))
637  return ID_ge;
638  if(stmt==patternt("if_?cmpeq"))
639  return ID_equal;
640  if(stmt==patternt("if_?cmpne"))
641  return ID_notequal;
642 
643  throw "unhandled java comparison instruction";
644 }
645 
646 static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
647 {
648  symbol_typet class_type(fieldref.get(ID_class));
649 
650  const typecast_exprt pointer2(pointer, java_reference_type(class_type));
651 
652  dereference_exprt obj_deref=checked_dereference(pointer2, class_type);
653 
654  const member_exprt member_expr(
655  obj_deref,
656  fieldref.get(ID_component_name),
657  fieldref.type());
658 
659  return member_expr;
660 }
661 
669  codet &repl,
670  const irep_idt &old_label,
671  const irep_idt &new_label)
672 {
673  const auto &stmt=repl.get_statement();
674  if(stmt==ID_goto)
675  {
676  auto &g=to_code_goto(repl);
677  if(g.get_destination()==old_label)
678  g.set_destination(new_label);
679  }
680  else
681  {
682  for(auto &op : repl.operands())
683  if(op.id()==ID_code)
684  replace_goto_target(to_code(op), old_label, new_label);
685  }
686 }
687 
703  block_tree_nodet &tree,
704  code_blockt &this_block,
705  unsigned address_start,
706  unsigned address_limit,
707  unsigned next_block_start_address)
708 {
709  address_mapt dummy;
711  tree,
712  this_block,
713  address_start,
714  address_limit,
715  next_block_start_address,
716  dummy,
717  false);
718 }
719 
735  block_tree_nodet &tree,
736  code_blockt &this_block,
737  unsigned address_start,
738  unsigned address_limit,
739  unsigned next_block_start_address,
740  const address_mapt &amap,
741  bool allow_merge)
742 {
743  // Check the tree shape invariant:
744  assert(tree.branch.size()==tree.branch_addresses.size());
745 
746  // If there are no child blocks, return this.
747  if(tree.leaf)
748  return this_block;
749  assert(!tree.branch.empty());
750 
751  // Find child block starting > address_start:
752  const auto afterstart=
753  std::upper_bound(
754  tree.branch_addresses.begin(),
755  tree.branch_addresses.end(),
756  address_start);
757  assert(afterstart!=tree.branch_addresses.begin());
758  auto findstart=afterstart;
759  --findstart;
760  auto child_offset=
761  std::distance(tree.branch_addresses.begin(), findstart);
762 
763  // Find child block starting >= address_limit:
764  auto findlim=
765  std::lower_bound(
766  tree.branch_addresses.begin(),
767  tree.branch_addresses.end(),
768  address_limit);
769  unsigned findlim_block_start_address=
770  findlim==tree.branch_addresses.end() ?
771  next_block_start_address :
772  (*findlim);
773 
774  // If all children are in scope, return this.
775  if(findstart==tree.branch_addresses.begin() &&
776  findlim==tree.branch_addresses.end())
777  return this_block;
778 
779  // Find the child code_blockt where the queried range begins:
780  auto child_iter=this_block.operands().begin();
781  // Skip any top-of-block declarations;
782  // all other children are labelled subblocks.
783  while(child_iter!=this_block.operands().end() &&
784  to_code(*child_iter).get_statement()==ID_decl)
785  ++child_iter;
786  assert(child_iter!=this_block.operands().end());
787  std::advance(child_iter, child_offset);
788  assert(child_iter!=this_block.operands().end());
789  auto &child_label=to_code_label(to_code(*child_iter));
790  auto &child_block=to_code_block(child_label.code());
791 
792  bool single_child(afterstart==findlim);
793  if(single_child)
794  {
795  // Range wholly contained within a child block
797  tree.branch[child_offset],
798  child_block,
799  address_start,
800  address_limit,
801  findlim_block_start_address,
802  amap,
803  allow_merge);
804  }
805 
806  // Otherwise we're being asked for a range of subblocks, but not all of them.
807  // If it's legal to draw a new lexical scope around the requested subset,
808  // do so; otherwise just return this block.
809 
810  // This can be a new lexical scope if all incoming edges target the
811  // new block header, or come from within the suggested new block.
812 
813  // If modifying the block tree is forbidden, give up and return this:
814  if(!allow_merge)
815  return this_block;
816 
817  // Check for incoming control-flow edges targeting non-header
818  // blocks of the new proposed block range:
819  auto checkit=amap.find(*findstart);
820  assert(checkit!=amap.end());
821  ++checkit; // Skip the header, which can have incoming edges from outside.
822  for(;
823  checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
824  ++checkit)
825  {
826  for(auto p : checkit->second.predecessors)
827  {
828  if(p<(*findstart) || p>=findlim_block_start_address)
829  {
830  debug() << "Generating codet: "
831  << "warning: refusing to create lexical block spanning "
832  << (*findstart) << "-" << findlim_block_start_address
833  << " due to incoming edge " << p << " -> "
834  << checkit->first << eom;
835  return this_block;
836  }
837  }
838  }
839 
840  // All incoming edges are acceptable! Create a new block wrapping
841  // the relevant children. Borrow the header block's label, and redirect
842  // any block-internal edges to target the inner header block.
843 
844  const irep_idt child_label_name=child_label.get_label();
845  std::string new_label_str = id2string(child_label_name);
846  new_label_str+='$';
847  irep_idt new_label_irep(new_label_str);
848 
849  code_labelt newlabel(child_label_name, code_blockt());
850  code_blockt &newblock=to_code_block(newlabel.code());
851  auto nblocks=std::distance(findstart, findlim);
852  assert(nblocks>=2);
853  debug() << "Generating codet: combining "
854  << std::distance(findstart, findlim)
855  << " blocks for addresses " << (*findstart) << "-"
856  << findlim_block_start_address << eom;
857 
858  // Make a new block containing every child of interest:
859  auto &this_block_children=this_block.operands();
860  assert(tree.branch.size()==this_block_children.size());
861  for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
862  blockidx!=blocklim;
863  ++blockidx)
864  newblock.move_to_operands(this_block_children[blockidx]);
865 
866  // Relabel the inner header:
867  to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
868  // Relabel internal gotos:
869  replace_goto_target(newblock, child_label_name, new_label_irep);
870 
871  // Remove the now-empty sibling blocks:
872  auto delfirst=this_block_children.begin();
873  std::advance(delfirst, child_offset+1);
874  auto dellim=delfirst;
875  std::advance(dellim, nblocks-1);
876  this_block_children.erase(delfirst, dellim);
877  this_block_children[child_offset].swap(newlabel);
878 
879  // Perform the same transformation on the index tree:
880  block_tree_nodet newnode;
881  auto branchstart=tree.branch.begin();
882  std::advance(branchstart, child_offset);
883  auto branchlim=branchstart;
884  std::advance(branchlim, nblocks);
885  for(auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
886  newnode.branch.push_back(std::move(*branchiter));
887  ++branchstart;
888  tree.branch.erase(branchstart, branchlim);
889 
890  assert(tree.branch.size()==this_block_children.size());
891 
892  auto branchaddriter=tree.branch_addresses.begin();
893  std::advance(branchaddriter, child_offset);
894  auto branchaddrlim=branchaddriter;
895  std::advance(branchaddrlim, nblocks);
896  newnode.branch_addresses.insert(
897  newnode.branch_addresses.begin(),
898  branchaddriter,
899  branchaddrlim);
900 
901  ++branchaddriter;
902  tree.branch_addresses.erase(branchaddriter, branchaddrlim);
903 
904  tree.branch[child_offset]=std::move(newnode);
905 
906  assert(tree.branch.size()==tree.branch_addresses.size());
907 
908  return
911  to_code(this_block_children[child_offset])).code());
912 }
913 
915  unsigned pc,
916  const exprt &e,
917  std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
918 {
919  if(e.id()==ID_symbol)
920  {
921  const auto &symexpr=to_symbol_expr(e);
922  auto findit = result.insert(
923  {symexpr.get_identifier(), java_bytecode_convert_methodt::variablet()});
924  auto &var=findit.first->second;
925  if(findit.second)
926  {
927  var.symbol_expr=symexpr;
928  var.start_pc=pc;
929  var.length=1;
930  }
931  else
932  {
933  if(pc<var.start_pc)
934  {
935  var.length+=(var.start_pc-pc);
936  var.start_pc=pc;
937  }
938  else
939  {
940  var.length=std::max(var.length, (pc-var.start_pc)+1);
941  }
942  }
943  }
944  else
945  {
946  forall_operands(it, e)
947  gather_symbol_live_ranges(pc, *it, result);
948  }
949 }
950 
957  const irep_idt &classname)
958 {
959  auto findit = symbol_table.symbols.find(clinit_wrapper_name(classname));
960  if(findit == symbol_table.symbols.end())
961  return code_skipt();
962  else
963  {
965  ret.function() = findit->second.symbol_expr();
967  needed_lazy_methods->add_needed_method(findit->second.name);
968  return ret;
969  }
970 }
971 
972 static unsigned get_bytecode_type_width(const typet &ty)
973 {
974  if(ty.id()==ID_pointer)
975  return 32;
976  return ty.get_unsigned_int(ID_width);
977 }
978 
980  const methodt &method,
981  const code_typet &method_type,
982  const irep_idt &method_name,
983  const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
984 {
985  const instructionst &instructions=method.instructions;
986 
987  // Run a worklist algorithm, assuming that the bytecode has not
988  // been tampered with. See "Leroy, X. (2003). Java bytecode
989  // verification: algorithms and formalizations. Journal of Automated
990  // Reasoning, 30(3-4), 235-269." for a more complete treatment.
991 
992  // first pass: get targets and map addresses to instructions
993 
994  address_mapt address_map;
995  std::set<unsigned> targets;
996 
997  std::vector<unsigned> jsr_ret_targets;
998  std::vector<instructionst::const_iterator> ret_instructions;
999 
1000  for(auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1001  {
1003  std::pair<address_mapt::iterator, bool> a_entry=
1004  address_map.insert(std::make_pair(i_it->address, ins));
1005  assert(a_entry.second);
1006  // addresses are strictly increasing, hence we must have inserted
1007  // a new maximal key
1008  assert(a_entry.first==--address_map.end());
1009 
1010  if(i_it->statement!="goto" &&
1011  i_it->statement!="return" &&
1012  !(i_it->statement==patternt("?return")) &&
1013  i_it->statement!="athrow" &&
1014  i_it->statement!="jsr" &&
1015  i_it->statement!="jsr_w" &&
1016  i_it->statement!="ret")
1017  {
1018  instructionst::const_iterator next=i_it;
1019  if(++next!=instructions.end())
1020  a_entry.first->second.successors.push_back(next->address);
1021  }
1022 
1023  if(i_it->statement=="athrow" ||
1024  i_it->statement=="putfield" ||
1025  i_it->statement=="getfield" ||
1026  i_it->statement=="checkcast" ||
1027  i_it->statement=="newarray" ||
1028  i_it->statement=="anewarray" ||
1029  i_it->statement=="idiv" ||
1030  i_it->statement=="ldiv" ||
1031  i_it->statement=="irem" ||
1032  i_it->statement=="lrem" ||
1033  i_it->statement==patternt("?astore") ||
1034  i_it->statement==patternt("?aload") ||
1035  i_it->statement=="invokestatic" ||
1036  i_it->statement=="invokevirtual" ||
1037  i_it->statement=="invokespecial" ||
1038  i_it->statement=="invokeinterface")
1039  {
1040  const std::vector<unsigned int> handler =
1041  try_catch_handler(i_it->address, method.exception_table);
1042  std::list<unsigned int> &successors = a_entry.first->second.successors;
1043  successors.insert(successors.end(), handler.begin(), handler.end());
1044  targets.insert(handler.begin(), handler.end());
1045  }
1046 
1047  if(i_it->statement=="goto" ||
1048  i_it->statement==patternt("if_?cmp??") ||
1049  i_it->statement==patternt("if??") ||
1050  i_it->statement=="ifnonnull" ||
1051  i_it->statement=="ifnull" ||
1052  i_it->statement=="jsr" ||
1053  i_it->statement=="jsr_w")
1054  {
1055  PRECONDITION(!i_it->args.empty());
1056 
1057  unsigned target;
1058  bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
1059  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
1060  targets.insert(target);
1061 
1062  a_entry.first->second.successors.push_back(target);
1063 
1064  if(i_it->statement=="jsr" ||
1065  i_it->statement=="jsr_w")
1066  {
1067  auto next = std::next(i_it);
1069  next != instructions.end(), "jsr should have valid return address");
1070  targets.insert(next->address);
1071  jsr_ret_targets.push_back(next->address);
1072  }
1073  }
1074  else if(i_it->statement=="tableswitch" ||
1075  i_it->statement=="lookupswitch")
1076  {
1077  bool is_label=true;
1078  for(const auto &arg : i_it->args)
1079  {
1080  if(is_label)
1081  {
1082  unsigned target;
1083  bool ret=to_unsigned_integer(to_constant_expr(arg), target);
1084  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
1085  targets.insert(target);
1086  a_entry.first->second.successors.push_back(target);
1087  }
1088  is_label=!is_label;
1089  }
1090  }
1091  else if(i_it->statement=="ret")
1092  {
1093  // Finish these later, once we've seen all jsr instructions.
1094  ret_instructions.push_back(i_it);
1095  }
1096  }
1097  draw_edges_from_ret_to_jsr(address_map, jsr_ret_targets, ret_instructions);
1098 
1099  for(const auto &address : address_map)
1100  {
1101  for(unsigned s : address.second.successors)
1102  {
1103  const auto a_it = address_map.find(s);
1104  CHECK_RETURN(a_it != address_map.end());
1105  a_it->second.predecessors.insert(address.first);
1106  }
1107  }
1108 
1109  // Clean the list of temporary variables created by a call to `tmp_variable`.
1110  // These are local variables in the goto function used to represent temporary
1111  // values of the JVM operand stack, newly allocated objects before the
1112  // constructor is called, ...
1113  tmp_vars.clear();
1114 
1115  // Now that the control flow graph is built, set up our local variables
1116  // (these require the graph to determine live ranges)
1117  setup_local_variables(method, address_map);
1118 
1119  std::set<unsigned> working_set;
1120 
1121  if(!instructions.empty())
1122  working_set.insert(instructions.front().address);
1123 
1124  while(!working_set.empty())
1125  {
1126  auto cur = working_set.begin();
1127  auto address_it = address_map.find(*cur);
1128  CHECK_RETURN(address_it != address_map.end());
1129  auto &instruction = address_it->second;
1130  unsigned cur_pc=*cur;
1131  working_set.erase(cur);
1132 
1133  if(instruction.done)
1134  continue;
1135  working_set.insert(
1136  instruction.successors.begin(), instruction.successors.end());
1137 
1138  instructionst::const_iterator i_it = instruction.source;
1139  stack.swap(instruction.stack);
1140  instruction.stack.clear();
1141  codet &c = instruction.code;
1142 
1143  assert(
1144  stack.empty() || instruction.predecessors.size() <= 1 ||
1145  has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
1146 
1147  irep_idt statement=i_it->statement;
1148  exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
1149  exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
1150 
1152 
1153  // deal with _idx suffixes
1154  if(statement.size()>=2 &&
1155  statement[statement.size()-2]=='_' &&
1156  isdigit(statement[statement.size()-1]))
1157  {
1158  arg0=
1159  from_integer(
1161  std::string(id2string(statement), statement.size()-1, 1)),
1162  java_int_type());
1163  statement=std::string(id2string(statement), 0, statement.size()-2);
1164  }
1165 
1166  typet catch_type;
1167 
1168  // Find catch blocks that begin here. For now we assume if more than
1169  // one catch targets the same bytecode then we must be indifferent to
1170  // its type and just call it a Throwable.
1171  auto it=method.exception_table.begin();
1172  for(; it!=method.exception_table.end(); ++it)
1173  {
1174  if(cur_pc==it->handler_pc)
1175  {
1176  if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
1177  {
1178  catch_type=symbol_typet("java::java.lang.Throwable");
1179  break;
1180  }
1181  else
1182  catch_type=it->catch_type;
1183  }
1184  }
1185 
1186  codet catch_instruction;
1187 
1188  if(catch_type!=typet())
1189  {
1190  // at the beginning of a handler, clear the stack and
1191  // push the corresponding exceptional return variable
1192  // We also create a catch exception instruction that
1193  // precedes the catch block, and which remove_exceptionst
1194  // will transform into something like:
1195  // catch_var = GLOBAL_THROWN_EXCEPTION;
1196  // GLOBAL_THROWN_EXCEPTION = null;
1197  stack.clear();
1198  symbol_exprt catch_var=
1199  tmp_variable(
1200  "caught_exception",
1201  java_reference_type(catch_type));
1202  stack.push_back(catch_var);
1203  code_landingpadt catch_statement(catch_var);
1204  catch_instruction=catch_statement;
1205  }
1206 
1208  exprt::operandst results;
1209  results.resize(bytecode_info.push, nil_exprt());
1210 
1211  if(statement=="aconst_null")
1212  {
1213  assert(results.size()==1);
1215  }
1216  else if(statement=="athrow")
1217  {
1218  PRECONDITION(op.size() == 1 && results.size() == 1);
1219  convert_athrow(i_it->source_location, op, c, results);
1220  }
1221  else if(statement=="checkcast")
1222  {
1223  // checkcast throws an exception in case a cast of object
1224  // on stack to given type fails.
1225  // The stack isn't modified.
1226  PRECONDITION(op.size() == 1 && results.size() == 1);
1227  convert_checkcast(arg0, op, c, results);
1228  }
1229  else if(statement=="invokedynamic")
1230  {
1231  // not used in Java
1232  if(
1233  const auto res = convert_invoke_dynamic(
1234  lambda_method_handles, i_it->source_location, arg0))
1235  {
1236  results.resize(1);
1237  results[0] = *res;
1238  }
1239  }
1240  else if(statement=="invokestatic" &&
1241  id2string(arg0.get(ID_identifier))==
1242  "java::org.cprover.CProver.assume:(Z)V")
1243  {
1244  const code_typet &code_type=to_code_type(arg0.type());
1245  INVARIANT(code_type.parameters().size()==1,
1246  "function expected to have exactly one parameter");
1247  c = replace_call_to_cprover_assume(i_it->source_location, c);
1248  }
1249  else if(statement=="invokeinterface" ||
1250  statement=="invokespecial" ||
1251  statement=="invokevirtual" ||
1252  statement=="invokestatic")
1253  {
1254  convert_invoke(i_it->source_location, statement, arg0, c, results);
1255  }
1256  else if(statement=="return")
1257  {
1258  PRECONDITION(op.empty() && results.empty());
1259  c=code_returnt();
1260  }
1261  else if(statement==patternt("?return"))
1262  {
1263  // Return types are promoted in java, so this might need
1264  // conversion.
1265  PRECONDITION(op.size() == 1 && results.empty());
1266  exprt r=op[0];
1267  if(r.type()!=method_return_type)
1269  c=code_returnt(r);
1270  }
1271  else if(statement==patternt("?astore"))
1272  {
1273  assert(op.size()==3 && results.empty());
1274  c = convert_astore(statement, op, i_it->source_location);
1275  }
1276  else if(statement==patternt("?store"))
1277  {
1278  // store value into some local variable
1279  PRECONDITION(op.size() == 1 && results.empty());
1280  c = convert_store(
1281  statement, arg0, op, i_it->address, i_it->source_location);
1282  }
1283  else if(statement==patternt("?aload"))
1284  {
1285  PRECONDITION(op.size() == 2 && results.size() == 1);
1286  results[0] = convert_aload(statement, op);
1287  }
1288  else if(statement==patternt("?load"))
1289  {
1290  // load a value from a local variable
1291  results[0]=
1292  variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED);
1293  }
1294  else if(statement=="ldc" || statement=="ldc_w" ||
1295  statement=="ldc2" || statement=="ldc2_w")
1296  {
1297  PRECONDITION(op.empty() && results.size() == 1);
1298 
1299  INVARIANT(
1300  arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
1301  "String and Class literals should have been lowered in "
1302  "generate_constant_global_variables");
1303 
1304  results[0] = arg0;
1305  }
1306  else if(statement=="goto" || statement=="goto_w")
1307  {
1308  PRECONDITION(op.empty() && results.empty());
1309  mp_integer number;
1310  bool ret=to_integer(to_constant_expr(arg0), number);
1311  INVARIANT(!ret, "goto argument should be an integer");
1312  code_gotot code_goto(label(integer2string(number)));
1313  c=code_goto;
1314  }
1315  else if(statement=="jsr" || statement=="jsr_w")
1316  {
1317  // As 'goto', except we must also push the subroutine return address:
1318  PRECONDITION(op.empty() && results.size() == 1);
1319  mp_integer number;
1320  bool ret=to_integer(to_constant_expr(arg0), number);
1321  INVARIANT(!ret, "jsr argument should be an integer");
1322  code_gotot code_goto(label(integer2string(number)));
1323  c=code_goto;
1324  results[0]=
1325  from_integer(
1326  std::next(i_it)->address,
1327  unsignedbv_typet(64));
1328  results[0].type()=pointer_type(void_typet());
1329  }
1330  else if(statement=="ret")
1331  {
1332  // Since we have a bounded target set, make life easier on our analyses
1333  // and write something like:
1334  // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
1335  PRECONDITION(op.empty() && results.empty());
1336  assert(!jsr_ret_targets.empty());
1337  c = convert_ret(
1338  jsr_ret_targets, arg0, i_it->source_location, i_it->address);
1339  }
1340  else if(statement=="iconst_m1")
1341  {
1342  assert(results.size()==1);
1343  results[0]=from_integer(-1, java_int_type());
1344  }
1345  else if(statement==patternt("?const"))
1346  {
1347  assert(results.size()==1);
1348  results = convert_const(statement, arg0, results);
1349  }
1350  else if(statement==patternt("?ipush"))
1351  {
1352  PRECONDITION(results.size()==1);
1354  arg0.id()==ID_constant,
1355  "ipush argument expected to be constant");
1356  results[0]=arg0;
1357  if(arg0.type()!=java_int_type())
1358  results[0].make_typecast(java_int_type());
1359  }
1360  else if(statement==patternt("if_?cmp??"))
1361  {
1362  PRECONDITION(op.size() == 2 && results.empty());
1363  mp_integer number;
1364  bool ret=to_integer(to_constant_expr(arg0), number);
1365  INVARIANT(!ret, "if_?cmp?? argument should be an integer");
1366  c = convert_if_cmp(
1367  address_map, statement, op, number, i_it->source_location);
1368  }
1369  else if(statement==patternt("if??"))
1370  {
1371  const irep_idt id=
1372  statement=="ifeq"?ID_equal:
1373  statement=="ifne"?ID_notequal:
1374  statement=="iflt"?ID_lt:
1375  statement=="ifge"?ID_ge:
1376  statement=="ifgt"?ID_gt:
1377  statement=="ifle"?ID_le:
1378  irep_idt();
1379 
1380  INVARIANT(!id.empty(), "unexpected bytecode-if");
1381  PRECONDITION(op.size() == 1 && results.empty());
1382  mp_integer number;
1383  bool ret=to_integer(to_constant_expr(arg0), number);
1384  INVARIANT(!ret, "if?? argument should be an integer");
1385  c = convert_if(address_map, op, id, number, i_it->source_location);
1386  }
1387  else if(statement==patternt("ifnonnull"))
1388  {
1389  PRECONDITION(op.size() == 1 && results.empty());
1390  mp_integer number;
1391  bool ret=to_integer(to_constant_expr(arg0), number);
1392  INVARIANT(!ret, "ifnonnull argument should be an integer");
1393  c = convert_ifnonull(address_map, op, number, i_it->source_location);
1394  }
1395  else if(statement==patternt("ifnull"))
1396  {
1397  PRECONDITION(op.size() == 1 && results.empty());
1398  mp_integer number;
1399  bool ret=to_integer(to_constant_expr(arg0), number);
1400  INVARIANT(!ret, "ifnull argument should be an integer");
1401  c = convert_ifnull(address_map, op, number, i_it->source_location);
1402  }
1403  else if(statement=="iinc")
1404  {
1405  c = convert_iinc(arg0, arg1, i_it->source_location, i_it->address);
1406  }
1407  else if(statement==patternt("?xor"))
1408  {
1409  PRECONDITION(op.size() == 2 && results.size() == 1);
1410  results[0]=bitxor_exprt(op[0], op[1]);
1411  }
1412  else if(statement==patternt("?or"))
1413  {
1414  PRECONDITION(op.size() == 2 && results.size() == 1);
1415  results[0]=bitor_exprt(op[0], op[1]);
1416  }
1417  else if(statement==patternt("?and"))
1418  {
1419  PRECONDITION(op.size() == 2 && results.size() == 1);
1420  results[0]=bitand_exprt(op[0], op[1]);
1421  }
1422  else if(statement==patternt("?shl"))
1423  {
1424  PRECONDITION(op.size() == 2 && results.size() == 1);
1425  results[0]=shl_exprt(op[0], op[1]);
1426  }
1427  else if(statement==patternt("?shr"))
1428  {
1429  PRECONDITION(op.size() == 2 && results.size() == 1);
1430  results[0]=ashr_exprt(op[0], op[1]);
1431  }
1432  else if(statement==patternt("?ushr"))
1433  {
1434  PRECONDITION(op.size() == 2 && results.size() == 1);
1435  results = convert_ushr(statement, op, results);
1436  }
1437  else if(statement==patternt("?add"))
1438  {
1439  PRECONDITION(op.size() == 2 && results.size() == 1);
1440  results[0]=plus_exprt(op[0], op[1]);
1441  }
1442  else if(statement==patternt("?sub"))
1443  {
1444  PRECONDITION(op.size() == 2 && results.size() == 1);
1445  results[0]=minus_exprt(op[0], op[1]);
1446  }
1447  else if(statement==patternt("?div"))
1448  {
1449  PRECONDITION(op.size() == 2 && results.size() == 1);
1450  results[0]=div_exprt(op[0], op[1]);
1451  }
1452  else if(statement==patternt("?mul"))
1453  {
1454  PRECONDITION(op.size() == 2 && results.size() == 1);
1455  results[0]=mult_exprt(op[0], op[1]);
1456  }
1457  else if(statement==patternt("?neg"))
1458  {
1459  PRECONDITION(op.size() == 1 && results.size() == 1);
1460  results[0]=unary_minus_exprt(op[0], op[0].type());
1461  }
1462  else if(statement==patternt("?rem"))
1463  {
1464  PRECONDITION(op.size() == 2 && results.size() == 1);
1465  if(statement=="frem" || statement=="drem")
1466  results[0]=rem_exprt(op[0], op[1]);
1467  else
1468  results[0]=mod_exprt(op[0], op[1]);
1469  }
1470  else if(statement==patternt("?cmp"))
1471  {
1472  PRECONDITION(op.size() == 2 && results.size() == 1);
1473  results = convert_cmp(op, results);
1474  }
1475  else if(statement==patternt("?cmp?"))
1476  {
1477  PRECONDITION(op.size() == 2 && results.size() == 1);
1478  results = convert_cmp2(statement, op, results);
1479  }
1480  else if(statement==patternt("?cmpl"))
1481  {
1482  PRECONDITION(op.size() == 2 && results.size() == 1);
1483  results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
1484  }
1485  else if(statement=="dup")
1486  {
1487  PRECONDITION(op.size() == 1 && results.size() == 2);
1488  results[0]=results[1]=op[0];
1489  }
1490  else if(statement=="dup_x1")
1491  {
1492  PRECONDITION(op.size() == 2 && results.size() == 3);
1493  results[0]=op[1];
1494  results[1]=op[0];
1495  results[2]=op[1];
1496  }
1497  else if(statement=="dup_x2")
1498  {
1499  PRECONDITION(op.size() == 3 && results.size() == 4);
1500  results[0]=op[2];
1501  results[1]=op[0];
1502  results[2]=op[1];
1503  results[3]=op[2];
1504  }
1505  // dup2* behaviour depends on the size of the operands on the
1506  // stack
1507  else if(statement=="dup2")
1508  {
1509  PRECONDITION(!stack.empty() && results.empty());
1510  convert_dup2(op, results);
1511  }
1512  else if(statement=="dup2_x1")
1513  {
1514  PRECONDITION(!stack.empty() && results.empty());
1515  convert_dup2_x1(op, results);
1516  }
1517  else if(statement=="dup2_x2")
1518  {
1519  PRECONDITION(!stack.empty() && results.empty());
1520  convert_dup2_x2(op, results);
1521  }
1522  else if(statement=="dconst")
1523  {
1524  PRECONDITION(op.empty() && results.size() == 1);
1525  }
1526  else if(statement=="fconst")
1527  {
1528  PRECONDITION(op.empty() && results.size() == 1);
1529  }
1530  else if(statement=="getfield")
1531  {
1532  PRECONDITION(op.size() == 1 && results.size() == 1);
1533  results[0]=java_bytecode_promotion(to_member(op[0], arg0));
1534  }
1535  else if(statement=="getstatic")
1536  {
1537  PRECONDITION(op.empty() && results.size() == 1);
1538  symbol_exprt symbol_expr(arg0.type());
1539  const auto &field_name=arg0.get_string(ID_component_name);
1540  const bool is_assertions_disabled_field=
1541  field_name.find("$assertionsDisabled")!=std::string::npos;
1542 
1543  symbol_expr.set_identifier(
1544  get_static_field(arg0.get_string(ID_class), field_name));
1545 
1546  INVARIANT(
1547  symbol_table.has_symbol(symbol_expr.get_identifier()),
1548  "getstatic symbol should have been created before method conversion");
1549 
1551  arg0, symbol_expr, is_assertions_disabled_field, c, results);
1552  }
1553  else if(statement=="putfield")
1554  {
1555  PRECONDITION(op.size() == 2 && results.empty());
1556  c = convert_putfield(arg0, op);
1557  }
1558  else if(statement=="putstatic")
1559  {
1560  PRECONDITION(op.size() == 1 && results.empty());
1561  symbol_exprt symbol_expr(arg0.type());
1562  const auto &field_name=arg0.get_string(ID_component_name);
1563  symbol_expr.set_identifier(
1564  get_static_field(arg0.get_string(ID_class), field_name));
1565 
1566  INVARIANT(
1567  symbol_table.has_symbol(symbol_expr.get_identifier()),
1568  "putstatic symbol should have been created before method conversion");
1569 
1570  c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr);
1571  }
1572  else if(statement==patternt("?2?")) // i2c etc.
1573  {
1574  PRECONDITION(op.size() == 1 && results.size() == 1);
1575  typet type=java_type_from_char(statement[2]);
1576  results[0]=op[0];
1577  if(results[0].type()!=type)
1578  results[0].make_typecast(type);
1579  }
1580  else if(statement=="new")
1581  {
1582  // use temporary since the stack symbol might get duplicated
1583  PRECONDITION(op.empty() && results.size() == 1);
1584  convert_new(i_it->source_location, arg0, c, results);
1585  }
1586  else if(statement=="newarray" ||
1587  statement=="anewarray")
1588  {
1589  // the op is the array size
1590  PRECONDITION(op.size() == 1 && results.size() == 1);
1591  convert_newarray(i_it->source_location, statement, arg0, op, c, results);
1592  }
1593  else if(statement=="multianewarray")
1594  {
1595  // The first argument is the type, the second argument is the number of
1596  // dimensions. The size of each dimension is on the stack.
1597  mp_integer number;
1598  bool ret=to_integer(to_constant_expr(arg1), number);
1599  INVARIANT(!ret, "multianewarray argument should be an integer");
1600  std::size_t dimension=integer2size_t(number);
1601 
1602  op=pop(dimension);
1603  assert(results.size()==1);
1604  convert_multianewarray(i_it->source_location, arg0, op, c, results);
1605  }
1606  else if(statement=="arraylength")
1607  {
1608  PRECONDITION(op.size() == 1 && results.size() == 1);
1609 
1610  const typecast_exprt pointer(op[0], java_array_type(statement[0]));
1611 
1612  dereference_exprt array(pointer, pointer.type().subtype());
1613  assert(pointer.type().subtype().id()==ID_symbol);
1614  array.set(ID_java_member_access, true);
1615 
1616  const member_exprt length(array, "length", java_int_type());
1617 
1618  results[0]=length;
1619  }
1620  else if(statement=="tableswitch" ||
1621  statement=="lookupswitch")
1622  {
1623  PRECONDITION(op.size() == 1 && results.empty());
1624  c = convert_switch(address_map, op, i_it->args, i_it->source_location);
1625  }
1626  else if(statement=="pop" || statement=="pop2")
1627  {
1628  c = convert_pop(statement, op);
1629  }
1630  else if(statement=="instanceof")
1631  {
1632  PRECONDITION(op.size() == 1 && results.size() == 1);
1633 
1634  results[0]=
1635  binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
1636  }
1637  else if(statement=="monitorenter")
1638  {
1639  c = convert_monitorenter(i_it->source_location, op);
1640  }
1641  else if(statement=="monitorexit")
1642  {
1643  c = convert_monitorexit(i_it->source_location, op);
1644  }
1645  else if(statement=="swap")
1646  {
1647  PRECONDITION(op.size() == 2 && results.size() == 2);
1648  results[1]=op[0];
1649  results[0]=op[1];
1650  }
1651  else if(statement=="nop")
1652  {
1653  c=code_skipt();
1654  }
1655  else
1656  {
1657  c=codet(statement);
1658  c.operands()=op;
1659  }
1660 
1661  c = do_exception_handling(method, working_set, cur_pc, c);
1662 
1663  // Finally if this is the beginning of a catch block (already determined
1664  // before the big bytecode switch), insert the exception 'landing pad'
1665  // instruction before the actual instruction:
1666  if(catch_instruction!=codet())
1667  {
1668  c.make_block();
1669  c.operands().insert(c.operands().begin(), catch_instruction);
1670  }
1671 
1672  if(!i_it->source_location.get_line().empty())
1674 
1675  push(results);
1676 
1677  instruction.done = true;
1678  for(const unsigned address : instruction.successors)
1679  {
1680  address_mapt::iterator a_it2=address_map.find(address);
1681  CHECK_RETURN(a_it2 != address_map.end());
1682 
1683  // clear the stack if this is an exception handler
1684  for(const auto &exception_row : method.exception_table)
1685  {
1686  if(address==exception_row.handler_pc)
1687  {
1688  stack.clear();
1689  break;
1690  }
1691  }
1692 
1693  if(!stack.empty() && a_it2->second.predecessors.size()>1)
1694  {
1695  // copy into temporaries
1696  code_blockt more_code;
1697 
1698  // introduce temporaries when successor is seen for the first
1699  // time
1700  if(a_it2->second.stack.empty())
1701  {
1702  for(stackt::iterator s_it=stack.begin();
1703  s_it!=stack.end();
1704  ++s_it)
1705  {
1706  symbol_exprt lhs=tmp_variable("$stack", s_it->type());
1707  code_assignt a(lhs, *s_it);
1708  more_code.copy_to_operands(a);
1709 
1710  s_it->swap(lhs);
1711  }
1712  }
1713  else
1714  {
1715  INVARIANT(
1716  a_it2->second.stack.size() == stack.size(),
1717  "Stack sizes should be the same.");
1718  stackt::const_iterator os_it=a_it2->second.stack.begin();
1719  for(auto &expr : stack)
1720  {
1721  assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
1722  symbol_exprt lhs=to_symbol_expr(*os_it);
1723  code_assignt a(lhs, expr);
1724  more_code.copy_to_operands(a);
1725 
1726  expr.swap(lhs);
1727  ++os_it;
1728  }
1729  }
1730 
1731  if(results.empty())
1732  {
1733  more_code.copy_to_operands(c);
1734  c.swap(more_code);
1735  }
1736  else
1737  {
1738  c.make_block();
1739  auto &last_statement=to_code_block(c).find_last_statement();
1740  if(last_statement.get_statement()==ID_goto)
1741  {
1742  // Insert stack twiddling before branch:
1743  last_statement.make_block();
1744  last_statement.operands().insert(
1745  last_statement.operands().begin(),
1746  more_code.operands().begin(),
1747  more_code.operands().end());
1748  }
1749  else
1750  forall_operands(o_it, more_code)
1751  c.copy_to_operands(*o_it);
1752  }
1753  }
1754  a_it2->second.stack=stack;
1755  }
1756  }
1757 
1758  code_blockt code;
1759 
1760  // Add anonymous locals to the symtab:
1761  for(const auto &var : used_local_names)
1762  {
1763  symbolt new_symbol;
1764  new_symbol.name=var.get_identifier();
1765  new_symbol.type=var.type();
1766  new_symbol.base_name=var.get(ID_C_base_name);
1767  new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
1768  new_symbol.mode=ID_java;
1769  new_symbol.is_type=false;
1770  new_symbol.is_file_local=true;
1771  new_symbol.is_thread_local=true;
1772  new_symbol.is_lvalue=true;
1773  symbol_table.add(new_symbol);
1774  }
1775 
1776  // Try to recover block structure as indicated in the local variable table:
1777 
1778  // The block tree node mirrors the block structure of root_block,
1779  // indexing the Java PCs where each subblock starts and ends.
1780  block_tree_nodet root;
1781  code_blockt root_block;
1782 
1783  // First create a simple flat list of basic blocks. We'll add lexical nesting
1784  // constructs as variable live-ranges require next.
1785  bool start_new_block=true;
1786  bool has_seen_previous_address=false;
1787  unsigned previous_address=0;
1788  for(const auto &address_pair : address_map)
1789  {
1790  const unsigned address=address_pair.first;
1791  assert(address_pair.first==address_pair.second.source->address);
1792  const codet &c=address_pair.second.code;
1793 
1794  // Start a new lexical block if this is a branch target:
1795  if(!start_new_block)
1796  start_new_block=targets.find(address)!=targets.end();
1797  // Start a new lexical block if this is a control flow join
1798  // (e.g. due to exceptional control flow)
1799  if(!start_new_block)
1800  start_new_block=address_pair.second.predecessors.size()>1;
1801  // Start a new lexical block if we've just entered a try block
1802  if(!start_new_block && has_seen_previous_address)
1803  {
1804  for(const auto &exception_row : method.exception_table)
1805  if(exception_row.start_pc==previous_address)
1806  {
1807  start_new_block=true;
1808  break;
1809  }
1810  }
1811 
1812  if(start_new_block)
1813  {
1814  code_labelt newlabel(label(std::to_string(address)), code_blockt());
1815  root_block.move_to_operands(newlabel);
1816  root.branch.push_back(block_tree_nodet::get_leaf());
1817  assert((root.branch_addresses.empty() ||
1818  root.branch_addresses.back()<address) &&
1819  "Block addresses should be unique and increasing");
1820  root.branch_addresses.push_back(address);
1821  }
1822 
1823  if(c.get_statement()!=ID_skip)
1824  {
1825  auto &lastlabel=to_code_label(to_code(root_block.operands().back()));
1826  auto &add_to_block=to_code_block(lastlabel.code());
1827  add_to_block.add(c);
1828  }
1829  start_new_block=address_pair.second.successors.size()>1;
1830 
1831  previous_address=address;
1832  has_seen_previous_address=true;
1833  }
1834 
1835  // Find out where temporaries are used:
1836  std::map<irep_idt, variablet> temporary_variable_live_ranges;
1837  for(const auto &aentry : address_map)
1839  aentry.first,
1840  aentry.second.code,
1841  temporary_variable_live_ranges);
1842 
1843  std::vector<const variablet*> vars_to_process;
1844  for(const auto &vlist : variables)
1845  for(const auto &v : vlist)
1846  vars_to_process.push_back(&v);
1847 
1848  for(const auto &v : tmp_vars)
1849  vars_to_process.push_back(
1850  &temporary_variable_live_ranges.at(v.get_identifier()));
1851 
1852  for(const auto &v : used_local_names)
1853  vars_to_process.push_back(
1854  &temporary_variable_live_ranges.at(v.get_identifier()));
1855 
1856  for(const auto vp : vars_to_process)
1857  {
1858  const auto &v=*vp;
1859  if(v.is_parameter)
1860  continue;
1861  // Merge lexical scopes as far as possible to allow us to
1862  // declare these variable scopes faithfully.
1863  // Don't insert yet, as for the time being the blocks' only
1864  // operands must be other blocks.
1865  // The declarations will be inserted in the next pass instead.
1867  root,
1868  root_block,
1869  v.start_pc,
1870  v.start_pc+v.length,
1871  std::numeric_limits<unsigned>::max(),
1872  address_map);
1873  }
1874  for(const auto vp : vars_to_process)
1875  {
1876  const auto &v=*vp;
1877  if(v.is_parameter)
1878  continue;
1879  // Skip anonymous variables:
1880  if(v.symbol_expr.get_identifier().empty())
1881  continue;
1882  auto &block=get_block_for_pcrange(
1883  root,
1884  root_block,
1885  v.start_pc,
1886  v.start_pc+v.length,
1887  std::numeric_limits<unsigned>::max());
1888  code_declt d(v.symbol_expr);
1889  block.operands().insert(block.operands().begin(), d);
1890  }
1891 
1892  for(auto &block : root_block.operands())
1893  code.move_to_operands(block);
1894 
1895  return code;
1896 }
1897 
1899  const irep_idt &statement,
1900  const exprt::operandst &op)
1901 {
1902  // these are skips
1903  codet c = code_skipt();
1904 
1905  // pop2 removes two single-word items from the stack (e.g. two
1906  // integers, or an integer and an object reference) or one
1907  // two-word item (i.e. a double or a long).
1908  // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
1909  if(statement == "pop2" && get_bytecode_type_width(op[0].type()) == 32)
1910  pop(1);
1911  return c;
1912 }
1913 
1916  const exprt::operandst &op,
1918  const source_locationt &location)
1919 {
1920  // we turn into switch-case
1921  code_switcht code_switch;
1922  code_switch.add_source_location() = location;
1923  code_switch.value() = op[0];
1924  code_blockt code_block;
1925  code_block.add_source_location() = location;
1926 
1927  bool is_label = true;
1928  for(auto a_it = args.begin(); a_it != args.end();
1929  a_it++, is_label = !is_label)
1930  {
1931  if(is_label)
1932  {
1933  code_switch_caset code_case;
1934  code_case.add_source_location() = location;
1935 
1936  mp_integer number;
1937  bool ret = to_integer(to_constant_expr(*a_it), number);
1938  DATA_INVARIANT(!ret, "case label expected to be integer");
1939  code_case.code() = code_gotot(label(integer2string(number)));
1940  code_case.code().add_source_location() =
1941  address_map.at(integer2unsigned(number)).source->source_location;
1942 
1943  if(a_it == args.begin())
1944  code_case.set_default();
1945  else
1946  {
1947  auto prev = a_it;
1948  prev--;
1949  code_case.case_op() = *prev;
1950  if(code_case.case_op().type() != op[0].type())
1951  code_case.case_op().make_typecast(op[0].type());
1952  code_case.case_op().add_source_location() = location;
1953  }
1954 
1955  code_block.add(code_case);
1956  }
1957  }
1958 
1959  code_switch.body() = code_block;
1960  return code_switch;
1961 }
1962 
1964  exprt::operandst &op,
1965  exprt::operandst &results)
1966 {
1967  if(get_bytecode_type_width(stack.back().type()) == 32)
1968  op = pop(2);
1969  else
1970  op = pop(1);
1971 
1972  results.insert(results.end(), op.begin(), op.end());
1973  results.insert(results.end(), op.begin(), op.end());
1974 }
1975 
1977  exprt::operandst &op,
1978  exprt::operandst &results)
1979 {
1980  if(get_bytecode_type_width(stack.back().type()) == 32)
1981  op = pop(3);
1982  else
1983  op = pop(2);
1984 
1985  results.insert(results.end(), op.begin() + 1, op.end());
1986  results.insert(results.end(), op.begin(), op.end());
1987 }
1988 
1990  exprt::operandst &op,
1991  exprt::operandst &results)
1992 {
1993  if(get_bytecode_type_width(stack.back().type()) == 32)
1994  op = pop(2);
1995  else
1996  op = pop(1);
1997 
1998  exprt::operandst op2;
1999 
2000  if(get_bytecode_type_width(stack.back().type()) == 32)
2001  op2 = pop(2);
2002  else
2003  op2 = pop(1);
2004 
2005  results.insert(results.end(), op.begin(), op.end());
2006  results.insert(results.end(), op2.begin(), op2.end());
2007  results.insert(results.end(), op.begin(), op.end());
2008 }
2009 
2011  const irep_idt &statement,
2012  const exprt &arg0,
2013  exprt::operandst &results) const
2014 {
2015  const char type_char = statement[0];
2016  const bool is_double('d' == type_char);
2017  const bool is_float('f' == type_char);
2018 
2019  if(is_double || is_float)
2020  {
2021  const ieee_float_spect spec(
2024 
2025  ieee_floatt value(spec);
2026  if(arg0.type().id() != ID_floatbv)
2027  {
2028  mp_integer number;
2029  bool ret = to_integer(to_constant_expr(arg0), number);
2030  DATA_INVARIANT(!ret, "failed to convert constant");
2031  value.from_integer(number);
2032  }
2033  else
2034  value.from_expr(to_constant_expr(arg0));
2035 
2036  results[0] = value.to_expr();
2037  }
2038  else
2039  {
2040  mp_integer value;
2041  bool ret = to_integer(to_constant_expr(arg0), value);
2042  DATA_INVARIANT(!ret, "failed to convert constant");
2043  const typet type = java_type_from_char(statement[0]);
2044  results[0] = from_integer(value, type);
2045  }
2046  return results;
2047 }
2048 
2050  source_locationt location,
2051  const irep_idt &statement,
2052  exprt &arg0,
2053  codet &c,
2054  exprt::operandst &results)
2055 {
2056  const bool use_this(statement != "invokestatic");
2057  const bool is_virtual(
2058  statement == "invokevirtual" || statement == "invokeinterface");
2059 
2060  code_typet &code_type = to_code_type(arg0.type());
2061  code_typet::parameterst &parameters(code_type.parameters());
2062 
2063  if(use_this)
2064  {
2065  if(parameters.empty() || !parameters[0].get_this())
2066  {
2067  irep_idt classname = arg0.get(ID_C_class);
2068  typet thistype = symbol_typet(classname);
2069  // Note invokespecial is used for super-method calls as well as
2070  // constructors.
2071  if(statement == "invokespecial")
2072  {
2073  if(is_constructor(arg0.get(ID_identifier)))
2074  {
2076  needed_lazy_methods->add_needed_class(classname);
2077  code_type.set_is_constructor();
2078  }
2079  else
2080  code_type.set(ID_java_super_method_call, true);
2081  }
2082  reference_typet object_ref_type = java_reference_type(thistype);
2083  code_typet::parametert this_p(object_ref_type);
2084  this_p.set_this();
2085  this_p.set_base_name("this");
2086  parameters.insert(parameters.begin(), this_p);
2087  }
2088  }
2089 
2090  code_function_callt call;
2091  location.set_function(method_id);
2092 
2093  call.add_source_location() = location;
2094  call.arguments() = pop(parameters.size());
2095 
2096  // double-check a bit
2097  if(use_this)
2098  {
2099  const exprt &this_arg = call.arguments().front();
2100  INVARIANT(
2101  this_arg.type().id() == ID_pointer, "first argument must be a pointer");
2102  }
2103 
2104  // do some type adjustment for the arguments,
2105  // as Java promotes arguments
2106  // Also cast pointers since intermediate locals
2107  // can be void*.
2108 
2109  for(std::size_t i = 0; i < parameters.size(); i++)
2110  {
2111  const typet &type = parameters[i].type();
2112  if(
2113  type == java_boolean_type() || type == java_char_type() ||
2114  type == java_byte_type() || type == java_short_type() ||
2115  type.id() == ID_pointer)
2116  {
2117  assert(i < call.arguments().size());
2118  if(type != call.arguments()[i].type())
2119  call.arguments()[i].make_typecast(type);
2120  }
2121  }
2122 
2123  // do some type adjustment for return values
2124 
2125  const typet &return_type = code_type.return_type();
2126 
2127  if(return_type.id() != ID_empty)
2128  {
2129  // return types are promoted in Java
2130  call.lhs() = tmp_variable("return", return_type);
2131  exprt promoted = java_bytecode_promotion(call.lhs());
2132  results.resize(1);
2133  results[0] = promoted;
2134  }
2135 
2136  assert(arg0.id() == ID_virtual_function);
2137 
2138  // If we don't have a definition for the called symbol, and we won't
2139  // inherit a definition from a super-class, we create a new symbol and
2140  // insert it in the symbol table. The name and type of the method are
2141  // derived from the information we have in the call.
2142  // We fix the access attribute to ID_public, because of the following
2143  // reasons:
2144  // - We don't know the orignal access attribute and since the .class file
2145  // unavailable, we have no way to know.
2146  // - Whatever it was, we assume that the bytecode we are translating
2147  // compiles correctly, so such a method has to be accessible from this
2148  // method.
2149  // - We will never generate code that calls that method unless we
2150  // translate bytecode that calls that method. As a result we will never
2151  // generate code that may wrongly assume that such a method is
2152  // accessible if we assume that its access attribute is "more
2153  // accessible" than it actually is.
2154  irep_idt id = arg0.get(ID_identifier);
2155  if(
2156  symbol_table.symbols.find(id) == symbol_table.symbols.end() &&
2157  !(is_virtual &&
2158  is_method_inherited(arg0.get(ID_C_class), arg0.get(ID_component_name))))
2159  {
2160  symbolt symbol;
2161  symbol.name = id;
2162  symbol.base_name = arg0.get(ID_C_base_name);
2163  symbol.pretty_name = id2string(arg0.get(ID_C_class)).substr(6) + "." +
2164  id2string(symbol.base_name) + "()";
2165  symbol.type = arg0.type();
2166  symbol.type.set(ID_access, ID_public);
2167  symbol.value.make_nil();
2168  symbol.mode = ID_java;
2170  to_code_type(symbol.type), symbol.name, symbol_table);
2171 
2172  debug() << "Generating codet: new opaque symbol: method '" << symbol.name
2173  << "'" << eom;
2174  symbol_table.add(symbol);
2175  }
2176 
2177  if(is_virtual)
2178  {
2179  // dynamic binding
2180  assert(use_this);
2181  assert(!call.arguments().empty());
2182  call.function() = arg0;
2183  // Populate needed methods later,
2184  // once we know what object types can exist.
2185  }
2186  else
2187  {
2188  // static binding
2189  call.function() = symbol_exprt(arg0.get(ID_identifier), arg0.type());
2191  {
2192  needed_lazy_methods->add_needed_method(arg0.get(ID_identifier));
2193  // Calling a static method causes static initialization:
2194  needed_lazy_methods->add_needed_class(arg0.get(ID_C_class));
2195  }
2196  }
2197 
2198  call.function().add_source_location() = location;
2199 
2200  // Replacing call if it is a function of the Character library,
2201  // returning the same call otherwise
2203 
2204  if(!use_this)
2205  {
2206  codet clinit_call = get_clinit_call(arg0.get(ID_C_class));
2207  if(clinit_call.get_statement() != ID_skip)
2208  {
2209  code_blockt ret_block;
2210  ret_block.move_to_operands(clinit_call);
2211  ret_block.move_to_operands(c);
2212  c = std::move(ret_block);
2213  }
2214  }
2215 }
2216 
2218  source_locationt location,
2219  codet &c)
2220 {
2221  exprt operand = pop(1)[0];
2222  // we may need to adjust the type of the argument
2223  if(operand.type() != bool_typet())
2224  operand.make_typecast(bool_typet());
2225 
2226  c = code_assumet(operand);
2227  location.set_function(method_id);
2228  c.add_source_location() = location;
2229  return c;
2230 }
2231 
2233  const exprt &arg0,
2234  const exprt::operandst &op,
2235  codet &c,
2236  exprt::operandst &results) const
2237 {
2238  binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
2239  code_assertt assert_class(check);
2240  assert_class.add_source_location().set_comment("Dynamic cast check");
2241  assert_class.add_source_location().set_property_class("bad-dynamic-cast");
2242  // we add this assert such that we can recognise it
2243  // during the instrumentation phase
2244  c = std::move(assert_class);
2245  results[0] = op[0];
2246 }
2247 
2249  const source_locationt &location,
2250  const exprt::operandst &op,
2251  codet &c,
2252  exprt::operandst &results) const
2253 {
2254  if(
2257  "java::java.lang.AssertionError")
2258  {
2259  // we translate athrow into
2260  // ASSERT false;
2261  // ASSUME false:
2262  code_assertt assert_code;
2263  assert_code.assertion() = false_exprt();
2264  source_locationt assert_location = location; // copy
2265  assert_location.set_comment("assertion at " + location.as_string());
2266  assert_location.set("user-provided", true);
2267  assert_location.set_property_class(ID_assertion);
2268  assert_code.add_source_location() = assert_location;
2269 
2270  code_assumet assume_code;
2271  assume_code.assumption() = false_exprt();
2272  source_locationt assume_location = location; // copy
2273  assume_location.set("user-provided", true);
2274  assume_code.add_source_location() = assume_location;
2275 
2276  code_blockt ret_block;
2277  ret_block.move_to_operands(assert_code);
2278  ret_block.move_to_operands(assume_code);
2279  c = ret_block;
2280  }
2281  else
2282  {
2283  side_effect_expr_throwt throw_expr;
2284  throw_expr.add_source_location() = location;
2285  throw_expr.copy_to_operands(op[0]);
2286  c = code_expressiont(throw_expr);
2287  }
2288  results[0] = op[0];
2289 }
2290 
2293  const std::set<unsigned int> &working_set,
2294  unsigned int cur_pc,
2295  codet &c)
2296 {
2297  std::vector<irep_idt> exception_ids;
2298  std::vector<irep_idt> handler_labels;
2299 
2300  // for each try-catch add a CATCH-PUSH instruction
2301  // each CATCH-PUSH records a list of all the handler labels
2302  // together with a list of all the exception ids
2303 
2304  // be aware of different try-catch blocks with the same starting pc
2305  std::size_t pos = 0;
2306  std::size_t end_pc = 0;
2307  while(pos < method.exception_table.size())
2308  {
2309  // check if this is the beginning of a try block
2310  for(; pos < method.exception_table.size(); ++pos)
2311  {
2312  // unexplored try-catch?
2313  if(cur_pc == method.exception_table[pos].start_pc && end_pc == 0)
2314  {
2315  end_pc = method.exception_table[pos].end_pc;
2316  }
2317 
2318  // currently explored try-catch?
2319  if(
2320  cur_pc == method.exception_table[pos].start_pc &&
2321  method.exception_table[pos].end_pc == end_pc)
2322  {
2323  exception_ids.push_back(
2324  method.exception_table[pos].catch_type.get_identifier());
2325  // record the exception handler in the CATCH-PUSH
2326  // instruction by generating a label corresponding to
2327  // the handler's pc
2328  handler_labels.push_back(
2329  label(std::to_string(method.exception_table[pos].handler_pc)));
2330  }
2331  else
2332  break;
2333  }
2334 
2335  // add the actual PUSH-CATCH instruction
2336  if(!exception_ids.empty())
2337  {
2338  code_push_catcht catch_push;
2339  INVARIANT(
2340  exception_ids.size() == handler_labels.size(),
2341  "Exception tags and handler labels should be 1-to-1");
2342  code_push_catcht::exception_listt &exception_list =
2343  catch_push.exception_list();
2344  for(size_t i = 0; i < exception_ids.size(); ++i)
2345  {
2346  exception_list.push_back(
2348  exception_ids[i], handler_labels[i]));
2349  }
2350 
2351  code_blockt try_block;
2352  try_block.move_to_operands(catch_push);
2353  try_block.move_to_operands(c);
2354  c = try_block;
2355  }
2356  else
2357  {
2358  // advance
2359  ++pos;
2360  }
2361 
2362  // reset
2363  end_pc = 0;
2364  exception_ids.clear();
2365  handler_labels.clear();
2366  }
2367 
2368  // next add the CATCH-POP instructions
2369  size_t start_pc = 0;
2370  // as the first try block may have start_pc 0, we
2371  // must track it separately
2372  bool first_handler = false;
2373  // check if this is the end of a try block
2374  for(const auto &exception_row : method.exception_table)
2375  {
2376  // add the CATCH-POP before the end of the try block
2377  if(
2378  cur_pc < exception_row.end_pc && !working_set.empty() &&
2379  *working_set.begin() == exception_row.end_pc)
2380  {
2381  // have we already added a CATCH-POP for the current try-catch?
2382  // (each row corresponds to a handler)
2383  if(exception_row.start_pc != start_pc || !first_handler)
2384  {
2385  if(!first_handler)
2386  first_handler = true;
2387  // remember the beginning of the try-catch so that we don't add
2388  // another CATCH-POP for the same try-catch
2389  start_pc = exception_row.start_pc;
2390  // add CATCH_POP instruction
2391  code_pop_catcht catch_pop;
2392  code_blockt end_try_block;
2393  end_try_block.move_to_operands(c);
2394  end_try_block.move_to_operands(catch_pop);
2395  c = end_try_block;
2396  }
2397  }
2398  }
2399  return c;
2400 }
2401 
2403  const source_locationt &location,
2404  const exprt::operandst &op) const
2405 {
2406  code_typet type;
2407  type.return_type() = void_typet();
2408  type.parameters().resize(1);
2409  type.parameters()[0].type() = java_reference_type(void_typet());
2410  code_function_callt call;
2411  call.function() = symbol_exprt("java::monitorexit", type);
2412  call.lhs().make_nil();
2413  call.arguments().push_back(op[0]);
2414  call.add_source_location() = location;
2415  return call;
2416 }
2417 
2419  const source_locationt &location,
2420  const exprt::operandst &op) const
2421 {
2422  code_typet type;
2423  type.return_type() = void_typet();
2424  type.parameters().resize(1);
2425  type.parameters()[0].type() = java_reference_type(void_typet());
2426  code_function_callt call;
2427  call.function() = symbol_exprt("java::monitorenter", type);
2428  call.lhs().make_nil();
2429  call.arguments().push_back(op[0]);
2430  call.add_source_location() = location;
2431  return call;
2432 }
2433 
2435  const source_locationt &location,
2436  const exprt &arg0,
2437  const exprt::operandst &op,
2438  codet &c,
2439  exprt::operandst &results)
2440 {
2441  const reference_typet ref_type = java_reference_type(arg0.type());
2442 
2443  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
2444  java_new_array.operands() = op;
2445 
2446  if(!location.get_line().empty())
2447  java_new_array.add_source_location() = location;
2448 
2449  code_blockt create;
2450 
2451  if(max_array_length != 0)
2452  {
2454  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2455  code_assumet assume_le_max_size(le_max_size);
2456  create.move_to_operands(assume_le_max_size);
2457  }
2458 
2459  const exprt tmp = tmp_variable("newarray", ref_type);
2460  create.copy_to_operands(code_assignt(tmp, java_new_array));
2461  c = std::move(create);
2462  results[0] = tmp;
2463 }
2464 
2466  const source_locationt &location,
2467  const irep_idt &statement,
2468  const exprt &arg0,
2469  const exprt::operandst &op,
2470  codet &c,
2471  exprt::operandst &results)
2472 {
2473  char element_type;
2474 
2475  if(statement == "newarray")
2476  {
2477  irep_idt id = arg0.type().id();
2478 
2479  if(id == ID_bool)
2480  element_type = 'z';
2481  else if(id == ID_char)
2482  element_type = 'c';
2483  else if(id == ID_float)
2484  element_type = 'f';
2485  else if(id == ID_double)
2486  element_type = 'd';
2487  else if(id == ID_byte)
2488  element_type = 'b';
2489  else if(id == ID_short)
2490  element_type = 's';
2491  else if(id == ID_int)
2492  element_type = 'i';
2493  else if(id == ID_long)
2494  element_type = 'j';
2495  else
2496  element_type = '?';
2497  }
2498  else
2499  element_type = 'a';
2500 
2501  const reference_typet ref_type = java_array_type(element_type);
2502 
2503  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
2504  java_new_array.copy_to_operands(op[0]);
2505 
2506  if(!location.get_line().empty())
2507  java_new_array.add_source_location() = location;
2508 
2509  c = code_blockt();
2510 
2511  if(max_array_length != 0)
2512  {
2514  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2515  code_assumet assume_le_max_size(le_max_size);
2516  c.move_to_operands(assume_le_max_size);
2517  }
2518  const exprt tmp = tmp_variable("newarray", ref_type);
2519  c.copy_to_operands(code_assignt(tmp, java_new_array));
2520  results[0] = tmp;
2521 }
2522 
2524  const source_locationt &location,
2525  const exprt &arg0,
2526  codet &c,
2527  exprt::operandst &results)
2528 {
2529  const reference_typet ref_type = java_reference_type(arg0.type());
2530  side_effect_exprt java_new_expr(ID_java_new, ref_type);
2531 
2532  if(!location.get_line().empty())
2533  java_new_expr.add_source_location() = location;
2534 
2535  const exprt tmp = tmp_variable("new", ref_type);
2536  c = code_assignt(tmp, java_new_expr);
2537  c.add_source_location() = location;
2538  codet clinit_call =
2539  get_clinit_call(to_symbol_type(arg0.type()).get_identifier());
2540  if(clinit_call.get_statement() != ID_skip)
2541  {
2542  code_blockt ret_block;
2543  ret_block.move_to_operands(clinit_call);
2544  ret_block.move_to_operands(c);
2545  c = std::move(ret_block);
2546  }
2547  results[0] = tmp;
2548 }
2549 
2551  const source_locationt &location,
2552  const exprt &arg0,
2553  const exprt::operandst &op,
2554  const symbol_exprt &symbol_expr)
2555 {
2556  if(needed_lazy_methods && arg0.type().id() == ID_symbol)
2557  {
2558  needed_lazy_methods->add_needed_class(
2559  to_symbol_type(arg0.type()).get_identifier());
2560  }
2561 
2562  code_blockt block;
2563  block.add_source_location() = location;
2564 
2565  // Note this initializer call deliberately inits the class used to make
2566  // the reference, which may be a child of the class that actually defines
2567  // the field.
2568  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2569  if(clinit_call.get_statement() != ID_skip)
2570  block.move_to_operands(clinit_call);
2571 
2573  "stack_static_field",
2574  symbol_expr.type(),
2575  block,
2577  symbol_expr.get_identifier());
2578  block.copy_to_operands(code_assignt(symbol_expr, op[0]));
2579  return block;
2580 }
2581 
2583  const exprt &arg0,
2584  const exprt::operandst &op)
2585 {
2586  code_blockt block;
2588  "stack_field",
2589  op[1].type(),
2590  block,
2592  arg0.get(ID_component_name));
2593  block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
2594  return block;
2595 }
2596 
2598  const exprt &arg0,
2599  const symbol_exprt &symbol_expr,
2600  const bool is_assertions_disabled_field,
2601  codet &c,
2602  exprt::operandst &results)
2603 {
2605  {
2606  if(arg0.type().id() == ID_symbol)
2607  {
2608  needed_lazy_methods->add_needed_class(
2609  to_symbol_type(arg0.type()).get_identifier());
2610  }
2611  else if(arg0.type().id() == ID_pointer)
2612  {
2613  const auto &pointer_type = to_pointer_type(arg0.type());
2614  if(pointer_type.subtype().id() == ID_symbol)
2615  {
2616  needed_lazy_methods->add_needed_class(
2617  to_symbol_type(pointer_type.subtype()).get_identifier());
2618  }
2619  }
2620  else if(is_assertions_disabled_field)
2621  {
2622  needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
2623  }
2624  }
2625  results[0] = java_bytecode_promotion(symbol_expr);
2626 
2627  // Note this initializer call deliberately inits the class used to make
2628  // the reference, which may be a child of the class that actually defines
2629  // the field.
2630  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2631  if(clinit_call.get_statement() != ID_skip)
2632  c = clinit_call;
2633  else if(is_assertions_disabled_field)
2634  {
2635  // set $assertionDisabled to false
2636  c = code_assignt(symbol_expr, false_exprt());
2637  }
2638 }
2639 
2641  const irep_idt &statement,
2642  const exprt::operandst &op,
2643  exprt::operandst &results) const
2644 {
2645  const int nan_value(statement[4] == 'l' ? -1 : 1);
2646  const typet result_type(java_int_type());
2647  const exprt nan_result(from_integer(nan_value, result_type));
2648 
2649  // (value1 == NaN || value2 == NaN) ?
2650  // nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0;
2651  // (value1 == NaN || value2 == NaN) ?
2652  // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0;
2653 
2654  isnan_exprt nan_op0(op[0]);
2655  isnan_exprt nan_op1(op[1]);
2656  exprt one = from_integer(1, result_type);
2657  exprt minus_one = from_integer(-1, result_type);
2658  results[0] = if_exprt(
2659  or_exprt(nan_op0, nan_op1),
2660  nan_result,
2661  if_exprt(
2662  ieee_float_equal_exprt(op[0], op[1]),
2663  from_integer(0, result_type),
2664  if_exprt(binary_relation_exprt(op[0], ID_lt, op[1]), minus_one, one)));
2665  return results;
2666 }
2667 
2669  const exprt::operandst &op,
2670  exprt::operandst &results) const
2671 { // The integer result on the stack is:
2672  // 0 if op[0] equals op[1]
2673  // -1 if op[0] is less than op[1]
2674  // 1 if op[0] is greater than op[1]
2675 
2676  const typet t = java_int_type();
2677  exprt one = from_integer(1, t);
2678  exprt minus_one = from_integer(-1, t);
2679 
2680  if_exprt greater =
2681  if_exprt(binary_relation_exprt(op[0], ID_gt, op[1]), one, minus_one);
2682 
2683  results[0] = if_exprt(
2684  binary_relation_exprt(op[0], ID_equal, op[1]), from_integer(0, t), greater);
2685  return results;
2686 }
2687 
2689  const irep_idt &statement,
2690  const exprt::operandst &op,
2691  exprt::operandst &results) const
2692 {
2693  const typet type = java_type_from_char(statement[0]);
2694 
2695  const std::size_t width = type.get_size_t(ID_width);
2696  typet target = unsignedbv_typet(width);
2697 
2698  exprt lhs = op[0];
2699  if(lhs.type() != target)
2700  lhs.make_typecast(target);
2701  exprt rhs = op[1];
2702  if(rhs.type() != target)
2703  rhs.make_typecast(target);
2704 
2705  results[0] = lshr_exprt(lhs, rhs);
2706  if(results[0].type() != op[0].type())
2707  results[0].make_typecast(op[0].type());
2708  return results;
2709 }
2710 
2712  const exprt &arg0,
2713  const exprt &arg1,
2714  const source_locationt &location,
2715  const unsigned address)
2716 {
2717  code_blockt block;
2718  block.add_source_location() = location;
2719  // search variable on stack
2720  const exprt &locvar = variable(arg0, 'i', address, NO_CAST);
2722  "stack_iinc",
2723  java_int_type(),
2724  block,
2726  to_symbol_expr(locvar).get_identifier());
2727 
2728  code_assignt code_assign;
2729  code_assign.lhs() = variable(arg0, 'i', address, NO_CAST);
2730  exprt arg1_int_type = arg1;
2731  if(arg1.type() != java_int_type())
2732  arg1_int_type.make_typecast(java_int_type());
2733  code_assign.rhs() =
2734  plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
2735  block.copy_to_operands(code_assign);
2736  return block;
2737 }
2738 
2741  const exprt::operandst &op,
2742  const mp_integer &number,
2743  const source_locationt &location) const
2744 {
2745  code_ifthenelset code_branch;
2746  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
2747  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2748  code_branch.cond() = binary_relation_exprt(lhs, ID_equal, rhs);
2749  code_branch.then_case() = code_gotot(label(integer2string(number)));
2750  code_branch.then_case().add_source_location() =
2751  address_map.at(integer2unsigned(number)).source->source_location;
2752  code_branch.add_source_location() = location;
2753  return code_branch;
2754 }
2755 
2758  const exprt::operandst &op,
2759  const mp_integer &number,
2760  const source_locationt &location) const
2761 {
2762  code_ifthenelset code_branch;
2763  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
2764  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2765  code_branch.cond() = binary_relation_exprt(lhs, ID_notequal, rhs);
2766  code_branch.then_case() = code_gotot(label(integer2string(number)));
2767  code_branch.then_case().add_source_location() =
2768  address_map.at(integer2unsigned(number)).source->source_location;
2769  code_branch.add_source_location() = location;
2770  return code_branch;
2771 }
2772 
2775  const exprt::operandst &op,
2776  const irep_idt &id,
2777  const mp_integer &number,
2778  const source_locationt &location) const
2779 {
2780  code_ifthenelset code_branch;
2781  code_branch.cond() =
2782  binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
2783  code_branch.cond().add_source_location() = location;
2785  code_branch.then_case() = code_gotot(label(integer2string(number)));
2786  code_branch.then_case().add_source_location() =
2787  address_map.at(integer2unsigned(number)).source->source_location;
2789  code_branch.add_source_location() = location;
2791  return code_branch;
2792 }
2793 
2796  const irep_idt &statement,
2797  const exprt::operandst &op,
2798  const mp_integer &number,
2799  const source_locationt &location) const
2800 {
2801  code_ifthenelset code_branch;
2802  const irep_idt cmp_op = get_if_cmp_operator(statement);
2803 
2804  binary_relation_exprt condition(op[0], cmp_op, op[1]);
2805 
2806  exprt &lhs(condition.lhs());
2807  exprt &rhs(condition.rhs());
2808  const typet &lhs_type(lhs.type());
2809  if(lhs_type != rhs.type())
2810  rhs = typecast_exprt(rhs, lhs_type);
2811 
2812  code_branch.cond() = condition;
2813  code_branch.cond().add_source_location() = location;
2814  code_branch.then_case() = code_gotot(label(integer2string(number)));
2815  code_branch.then_case().add_source_location() =
2816  address_map.at(integer2unsigned(number)).source->source_location;
2817  code_branch.add_source_location() = location;
2818 
2819  return code_branch;
2820 }
2821 
2823  const std::vector<unsigned int> &jsr_ret_targets,
2824  const exprt &arg0,
2825  const source_locationt &location,
2826  const unsigned address)
2827 {
2828  code_blockt c;
2829  auto retvar = variable(arg0, 'a', address, NO_CAST);
2830  for(size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2831  {
2832  irep_idt number = std::to_string(jsr_ret_targets[idx]);
2833  code_gotot g(label(number));
2834  g.add_source_location() = location;
2835  if(idx == idxlim - 1)
2836  c.move_to_operands(g);
2837  else
2838  {
2840  auto address_ptr =
2841  from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
2842  address_ptr.type() = pointer_type(void_typet());
2843  branch.cond() = equal_exprt(retvar, address_ptr);
2844  branch.cond().add_source_location() = location;
2845  branch.then_case() = g;
2846  branch.add_source_location() = location;
2848  }
2849  }
2850  return c;
2851 }
2852 
2854  const irep_idt &statement,
2855  const exprt::operandst &op) const
2856 {
2857  const char &type_char = statement[0];
2858  const typecast_exprt pointer(op[0], java_array_type(type_char));
2859 
2860  dereference_exprt deref(pointer, pointer.type().subtype());
2861  deref.set(ID_java_member_access, true);
2862 
2863  const member_exprt data_ptr(
2864  deref, "data", pointer_type(java_type_from_char(type_char)));
2865 
2866  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
2867  // tag it so it's easy to identify during instrumentation
2868  data_plus_offset.set(ID_java_array_access, true);
2869  const typet &element_type = data_ptr.type().subtype();
2870  const dereference_exprt element(data_plus_offset, element_type);
2871  return java_bytecode_promotion(element);
2872 }
2873 
2875  const irep_idt &statement,
2876  const exprt &arg0,
2877  const exprt::operandst &op,
2878  const unsigned address,
2879  const source_locationt &location)
2880 {
2881  const exprt var = variable(arg0, statement[0], address, NO_CAST);
2882  const irep_idt &var_name = to_symbol_expr(var).get_identifier();
2883 
2884  exprt toassign = op[0];
2885  if('a' == statement[0] && toassign.type() != var.type())
2886  toassign = typecast_exprt(toassign, var.type());
2887 
2888  code_blockt block;
2889 
2891  "stack_store",
2892  toassign.type(),
2893  block,
2895  var_name);
2896  code_assignt assign(var, toassign);
2897  assign.add_source_location() = location;
2898  block.move(assign);
2899  return block;
2900 }
2901 
2903  const irep_idt &statement,
2904  const exprt::operandst &op,
2905  const source_locationt &location)
2906 {
2907  const char type_char = statement[0];
2908  const typecast_exprt pointer(op[0], java_array_type(type_char));
2909 
2910  dereference_exprt deref(pointer, pointer.type().subtype());
2911  deref.set(ID_java_member_access, true);
2912 
2913  const member_exprt data_ptr(
2914  deref, "data", pointer_type(java_type_from_char(type_char)));
2915 
2916  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
2917  // tag it so it's easy to identify during instrumentation
2918  data_plus_offset.set(ID_java_array_access, true);
2919  const typet &element_type = data_ptr.type().subtype();
2920  const dereference_exprt element(data_plus_offset, element_type);
2921 
2922  code_blockt block;
2923  block.add_source_location() = location;
2924 
2926  "stack_astore", element_type, block, bytecode_write_typet::ARRAY_REF, "");
2927 
2928  code_assignt array_put(element, op[2]);
2929  array_put.add_source_location() = location;
2930  block.move(array_put);
2931  return block;
2932 }
2933 
2935  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
2936  const source_locationt &location,
2937  const exprt &arg0)
2938 {
2939  const code_typet &code_type = to_code_type(arg0.type());
2940 
2941  const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
2942  lambda_method_handles,
2943  code_type.get_int(ID_java_lambda_method_handle_index));
2944  if(lambda_method_symbol.has_value())
2945  debug() << "Converting invokedynamic for lambda: "
2946  << lambda_method_symbol.value().name << eom;
2947  else
2948  debug() << "Converting invokedynamic for lambda with unknown handle "
2949  "type"
2950  << eom;
2951 
2952  const code_typet::parameterst &parameters(code_type.parameters());
2953 
2954  pop(parameters.size());
2955 
2956  const typet &return_type = code_type.return_type();
2957 
2958  if(return_type.id() == ID_empty)
2959  return {};
2960 
2961  return zero_initializer(
2962  return_type, location, namespacet(symbol_table), get_message_handler());
2963 }
2964 
2967  const std::vector<unsigned int> &jsr_ret_targets,
2968  const std::vector<
2969  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2970  &ret_instructions) const
2971 { // Draw edges from every `ret` to every `jsr` successor. Could do better with
2972  // flow analysis to distinguish multiple subroutines within the same function.
2973  for(const auto &retinst : ret_instructions)
2974  {
2975  auto &a_entry = address_map.at(retinst->address);
2976  a_entry.successors.insert(
2977  a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
2978  }
2979 }
2980 
2982  const unsigned int address,
2984  const
2985 {
2986  std::vector<unsigned> result;
2987  for(const auto &exception_row : exception_table)
2988  {
2989  if(address >= exception_row.start_pc && address < exception_row.end_pc)
2990  result.push_back(exception_row.handler_pc);
2991  }
2992  return result;
2993 }
2994 
3008  symbolt &method_symbol,
3010  &local_variable_table,
3011  symbol_table_baset &symbol_table)
3012 {
3013  // Obtain a std::vector of code_typet::parametert objects from the
3014  // (function) type of the symbol
3015  code_typet &code_type = to_code_type(method_symbol.type);
3016  code_typet::parameterst &parameters = code_type.parameters();
3017 
3018  // Find number of parameters
3019  unsigned slots_for_parameters = java_method_parameter_slots(code_type);
3020 
3021  // Find parameter names in the local variable table:
3022  typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3023  std::map<std::size_t, base_name_and_identifiert> param_names;
3024  for(const auto &v : local_variable_table)
3025  {
3026  if(v.index < slots_for_parameters)
3027  param_names.emplace(
3028  v.index,
3029  make_pair(
3030  v.name, id2string(method_symbol.name) + "::" + id2string(v.name)));
3031  }
3032 
3033  // Assign names to parameters
3034  std::size_t param_index = 0;
3035  for(auto &param : parameters)
3036  {
3037  irep_idt base_name, identifier;
3038 
3039  // Construct a sensible base name (base_name) and a fully qualified name
3040  // (identifier) for every parameter of the method under translation,
3041  // regardless of whether we have an LVT or not; and assign it to the
3042  // parameter object (which is stored in the type of the symbol, not in the
3043  // symbol table)
3044  if(param_index == 0 && param.get_this())
3045  {
3046  // my.package.ClassName.myMethodName:(II)I::this
3047  base_name = "this";
3048  identifier = id2string(method_symbol.name) + "::" + id2string(base_name);
3049  }
3050  else
3051  {
3052  auto param_name = param_names.find(param_index);
3053  if(param_name != param_names.end())
3054  {
3055  base_name = param_name->second.first;
3056  identifier = param_name->second.second;
3057  }
3058  else
3059  {
3060  // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
3061  // variable slot where the parameter is stored and T is a character
3062  // indicating the type
3063  const typet &type = param.type();
3064  char suffix = java_char_from_type(type);
3065  base_name = "arg" + std::to_string(param_index) + suffix;
3066  identifier =
3067  id2string(method_symbol.name) + "::" + id2string(base_name);
3068  }
3069  }
3070  param.set_base_name(base_name);
3071  param.set_identifier(identifier);
3072 
3073  // Build a new symbol for the parameter and add it to the symbol table
3074  parameter_symbolt parameter_symbol;
3075  parameter_symbol.base_name = base_name;
3076  parameter_symbol.mode = ID_java;
3077  parameter_symbol.name = identifier;
3078  parameter_symbol.type = param.type();
3079  symbol_table.insert(parameter_symbol);
3080 
3081  param_index += java_local_variable_slots(param.type());
3082  }
3083 }
3084 
3086  const symbolt &class_symbol,
3087  const java_bytecode_parse_treet::methodt &method,
3088  symbol_table_baset &symbol_table,
3090  size_t max_array_length,
3091  bool throw_assertion_error,
3092  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
3093  java_string_library_preprocesst &string_preprocess,
3094  const class_hierarchyt &class_hierarchy)
3095 {
3096  if(std::regex_match(
3097  id2string(class_symbol.name),
3098  std::regex(".*org\\.cprover\\.CProver.*")) &&
3099  cprover_methods_to_ignore.count(id2string(method.name)))
3100  {
3101  // Ignore these methods; fall back to the driver program's
3102  // stubbing behaviour.
3103  return;
3104  }
3105 
3107  symbol_table,
3109  max_array_length,
3110  throw_assertion_error,
3111  needed_lazy_methods,
3112  string_preprocess,
3113  class_hierarchy);
3114 
3115  java_bytecode_convert_method(class_symbol, method);
3116 }
3117 
3124  const irep_idt &classname,
3125  const irep_idt &methodid) const
3126 {
3129  classname,
3130  methodid,
3131  classname,
3132  symbol_table,
3134  false);
3135  return inherited_method.is_valid();
3136 }
3137 
3144  const irep_idt &class_identifier,
3145  const irep_idt &component_name) const
3146 {
3149  class_identifier,
3150  component_name,
3152  symbol_table,
3154  true);
3155 
3156  INVARIANT(
3157  inherited_method.is_valid(), "static field should be in symbol table");
3158 
3159  return inherited_method.get_full_component_identifier();
3160 }
3161 
3165  const std::string &tmp_var_prefix,
3166  const typet &tmp_var_type,
3167  code_blockt &block,
3168  const bytecode_write_typet write_type,
3169  const irep_idt &identifier)
3170 {
3171  for(auto &stack_entry : stack)
3172  {
3173  // remove typecasts if existing
3174  while(stack_entry.id()==ID_typecast)
3175  stack_entry=to_typecast_expr(stack_entry).op();
3176 
3177  // variables or static fields and symbol -> save symbols with same id
3178  if((write_type==bytecode_write_typet::VARIABLE ||
3179  write_type==bytecode_write_typet::STATIC_FIELD) &&
3180  stack_entry.id()==ID_symbol)
3181  {
3182  const symbol_exprt &var=to_symbol_expr(stack_entry);
3183  if(var.get_identifier()==identifier)
3184  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
3185  }
3186 
3187  // array reference and dereference -> save all references on the stack
3188  else if(write_type==bytecode_write_typet::ARRAY_REF &&
3189  stack_entry.id()==ID_dereference)
3190  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
3191 
3192  // field and member access -> compare component name
3193  else if(write_type==bytecode_write_typet::FIELD &&
3194  stack_entry.id()==ID_member)
3195  {
3196  const irep_idt &entry_id=
3197  to_member_expr(stack_entry).get_component_name();
3198  if(entry_id==identifier)
3199  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
3200  }
3201  }
3202 }
3203 
3206  const std::string &tmp_var_prefix,
3207  const typet &tmp_var_type,
3208  code_blockt &block,
3209  exprt &stack_entry)
3210 {
3211  const exprt tmp_var=
3212  tmp_variable(tmp_var_prefix, tmp_var_type);
3213  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
3214  stack_entry=tmp_var;
3215 }
The void type.
Definition: std_types.h:64
const irep_idt & get_statement() const
Definition: std_code.h:39
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
const codet & then_case() const
Definition: std_code.h:481
codet convert_monitorenter(const source_locationt &location, const exprt::operandst &op) const
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
void set_function(const irep_idt &function)
void set_access(const irep_idt &access)
Definition: std_types.h:930
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1503
semantic type conversion
Definition: std_expr.h:2111
static int8_t r
Definition: irep_hash.h:59
codet convert_monitorexit(const source_locationt &location, const exprt::operandst &op) const
static bool is_constructor(const irep_idt &method_name)
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
BigInt mp_integer
Definition: mp_arith.h:22
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
JAVA Bytecode Language Conversion.
codet convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
A ‘switch’ instruction.
Definition: std_code.h:533
Base type of functions.
Definition: std_types.h:764
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void convert(const symbolt &class_symbol, const methodt &)
bool is_thread_local
Definition: symbol.h:67
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
codet convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:124
void set_label(const irep_idt &label)
Definition: std_code.h:974
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Definition: java_utils.cpp:179
Remove function exceptional returns.
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Over-approximative uncaught exceptions analysis.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:161
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
boolean OR
Definition: std_expr.h:2391
typet java_boolean_type()
Definition: java_types.cpp:72
irep_idt method_id
Fully qualified name of the method under translation.
void set_property_class(const irep_idt &property_class)
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address ...
Control Flow Graph.
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
optionalt< symbolt > get_lambda_method_symbol(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
static void gather_symbol_live_ranges(unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:126
irep_idt mode
Language mode.
Definition: symbol.h:52
code_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.
const exprt & op() const
Definition: std_expr.h:340
const exprt & cond() const
Definition: std_code.h:471
codet & code()
Definition: std_code.h:1048
void from_expr(const constant_exprt &expr)
bool is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const
Returns true iff method methodid from class classname is a method inherited from a class (and not an ...
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned 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...
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
void set_comment(const irep_idt &comment)
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
static irep_idt label(const irep_idt &address)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1458
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::string as_string() const
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
struct bytecode_infot const bytecode_info[]
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4520
literalt pos(literalt a)
Definition: literal.h:193
std::vector< parametert > parameterst
Definition: std_types.h:767
exprt value
Initial value of symbol.
Definition: symbol.h:37
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
The trinary if-then-else operator.
Definition: std_expr.h:3361
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
A ‘goto’ instruction.
Definition: std_code.h:774
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
An exception that is raised for unsupported class signature.
Definition: java_types.h:528
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1546
bool operator==(const irep_idt &what) const
codet convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address)
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::vector< unsigned int > try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
A constant literal expression.
Definition: std_expr.h:4424
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
bool get_is_constructor() const
Definition: std_types.h:935
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
std::map< unsigned, converted_instructiont > address_mapt
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:90
codet convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
An expression statement.
Definition: std_code.h:1188
void set_default()
Definition: std_code.h:1033
A side effect that throws an exception.
Definition: std_code.h:1409
codet convert_instructions(const methodt &, const code_typet &, const irep_idt &, const java_class_typet::java_lambda_method_handlest &)
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const exprt & case_op() const
Definition: std_code.h:1038
unsigned java_method_parameter_slots(const code_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
Definition: java_utils.cpp:51
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
&#39;tree&#39; describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
Extract member of struct or union.
Definition: std_expr.h:3871
mstreamt & warning() const
Definition: message.h:307
codet convert_putfield(const exprt &arg0, const exprt::operandst &op)
equality
Definition: std_expr.h:1354
irep_idt current_method
A copy of method_id :/.
Class Hierarchy.
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:94
void set_is_constructor()
Definition: std_types.h:940
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3988
Bit-wise OR.
Definition: std_expr.h:2583
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:428
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
class code_blockt & make_block()
Definition: std_code.cpp:24
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
Given a string of the format &#39;?blah?&#39;, will return true when compared against a string that matches a...
argumentst & arguments()
Definition: std_code.h:860
const irep_idt & get_line() const
division (integer and real)
Definition: std_expr.h:1075
A reference into the symbol table.
Definition: std_types.h:110
A declaration of a local variable.
Definition: std_code.h:253
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)
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:301
The NIL expression.
Definition: std_expr.h:4510
exprt & rhs()
Definition: std_code.h:213
The empty type.
Definition: std_types.h:54
codet & code()
Definition: std_code.h:979
codet replace_character_call(code_function_callt call)
Operator to dereference a pointer.
Definition: std_expr.h:3284
void convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
typet java_type_from_char(char t)
Definition: java_types.cpp:147
nonstd::optional< T > optionalt
Definition: optional.h:35
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:807
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
API to expression classes.
exprt::operandst & convert_const(const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const
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...
patternt(const char *_p)
codet convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location)
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
Left shift.
Definition: std_expr.h:2848
A label for branch targets.
Definition: std_code.h:947
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
static unsigned get_bytecode_type_width(const typet &ty)
Given a class and a component (either field or method), find the closest parent that defines that com...
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
Definition: java_utils.cpp:433
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
typet java_byte_type()
Definition: java_types.cpp:52
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
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:30
size_t size() const
Definition: dstring.h:77
Logical right shift.
Definition: std_expr.h:2888
java_string_library_preprocesst & string_preprocess
codet & find_last_statement()
Definition: std_code.h:130
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...
The unary minus expression.
Definition: std_expr.h:444
typet java_short_type()
Definition: java_types.cpp:47
const symbolst & symbols
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
typet method_return_type
Return type of the method under conversion.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The boolean constant false.
Definition: std_expr.h:4499
const codet & body() const
Definition: std_code.h:551
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Definition: java_types.h:538
exprt::operandst pop(std::size_t n)
void java_bytecode_convert_method_lazy(const 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&#39;t actually perform method conversion just yet...
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
The reference type.
Definition: std_types.h:1483
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:400
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
const exprt & value() const
Definition: std_code.h:541
Bit-wise XOR.
Definition: std_expr.h:2644
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
static void assign_parameter_names(code_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...
message_handlert & get_message_handler()
Definition: message.h:153
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
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
mstreamt & result() const
Definition: message.h:312
const char * mnemonic
Definition: bytecode_info.h:46
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
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:107
exprt & function()
Definition: std_code.h:848
void convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
Base class for all expressions.
Definition: expr.h:42
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
Convert parsed annotations into the symbol table.
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void move(codet &code)
Definition: std_code.h:106
bool has_this() const
Definition: std_types.h:866
const exprt & assumption() const
Definition: std_code.h:367
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
Definition: expr.h:125
irep_idt get_component_name() const
Definition: std_expr.h:3895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
bool is_file_local
Definition: symbol.h:68
remainder of division
Definition: std_expr.h:1187
std::vector< local_variablet > local_variable_tablet
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
create temporary variables if a write instruction can have undesired side- effects ...
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
void make_nil()
Definition: irep.h:243
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
void swap(irept &irep)
Definition: irep.h:231
void push(const exprt::operandst &o)
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
binary minus
Definition: std_expr.h:959
codet & do_exception_handling(const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c)
Skip.
Definition: std_code.h:178
An if-then-else.
Definition: std_code.h:461
Bit-wise AND.
Definition: std_expr.h:2704
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:166
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
A switch-case.
Definition: std_code.h:1014
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:31
mstreamt & debug() const
Definition: message.h:332
A statement in a programming language.
Definition: std_code.h:21
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
Return from a function.
Definition: std_code.h:893
unsigned slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
Arithmetic right shift.
Definition: std_expr.h:2868
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
bool is_type
Definition: symbol.h:63
codet convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
typet java_char_type()
Definition: java_types.cpp:57
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1000
JAVA Bytecode Language Conversion.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
An expression containing a side effect.
Definition: std_code.h:1238
Compute dominators for CFG of goto_function.
codet 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
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...
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
Definition: java_utils.cpp:345
operandst & operands()
Definition: expr.h:66
void push_back(const T &t)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in &#39;repl&#39; that target &#39;old_label&#39; and redirect them to &#39;new_label&#39;.
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
exception_listt & exception_list()
Definition: std_code.h:1514
optionalt< exprt > convert_invoke_dynamic(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0)
bool empty() const
Definition: dstring.h:61
void convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
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...
codet convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
irep_idt get_full_component_identifier() const
Get the full name of this function.
codet convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
const typet & return_type() const
Definition: std_types.h:895
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:163
binary modulo
Definition: std_expr.h:1133
Assignment.
Definition: std_code.h:195
char java_char_from_type(const typet &type)
Definition: java_types.cpp:569
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1577
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:19
const exprt & assertion() const
Definition: std_code.h:413
Produce code for simple implementation of String Java libraries.
code_blockt convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address)
IEEE-floating-point equality.
Definition: std_expr.h:4200
std::string pretty_signature(const code_typet &code_type)
Definition: java_types.cpp:935
bool is_lvalue
Definition: symbol.h:68