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