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 
208  const exprt &arg,
209  char type_char,
210  size_t address,
212 {
213  mp_integer number;
214  bool ret=to_integer(to_constant_expr(arg), number);
215  CHECK_RETURN(!ret);
216 
217  std::size_t number_int=integer2size_t(number);
218  typet t=java_type_from_char(type_char);
219  variablest &var_list=variables[number_int];
220 
221  // search variable in list for correct frame / address if necessary
222  const variablet &var=
223  find_variable_for_slot(address, var_list);
224 
225  if(var.symbol_expr.get_identifier().empty())
226  {
227  // an unnamed local variable
228  irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
229  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
230 
231  symbol_exprt result(identifier, t);
232  result.set(ID_C_base_name, base_name);
233  used_local_names.insert(result);
234  return result;
235  }
236  else
237  {
239  if(do_cast==CAST_AS_NEEDED && t!=result.type())
241  return result;
242  }
243 }
244 
259  const std::string &descriptor,
260  const optionalt<std::string> &signature,
261  const std::string &class_name,
262  const std::string &method_name,
264 {
265  // In order to construct the method type, we can either use signature or
266  // descriptor. Since only signature contains the generics info, we want to
267  // use signature whenever possible. We revert to using descriptor if (1) the
268  // signature does not exist, (2) an unsupported generics are present or
269  // (3) in the special case when the number of parameters in the descriptor
270  // does not match the number of parameters in the signature - e.g. for
271  // certain types of inner classes and enums (see unit tests for examples).
272 
273  messaget message(message_handler);
274 
275  typet member_type_from_descriptor=java_type_from_string(descriptor);
276  INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
277  if(signature.has_value())
278  {
279  try
280  {
281  typet member_type_from_signature=java_type_from_string(
282  signature.value(),
283  class_name);
284  INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
285  if(
286  to_java_method_type(member_type_from_signature).parameters().size() ==
287  to_java_method_type(member_type_from_descriptor).parameters().size())
288  {
289  return to_java_method_type(member_type_from_signature);
290  }
291  else
292  {
293  message.warning() << "Method: " << class_name << "." << method_name
294  << "\n signature: " << signature.value()
295  << "\n descriptor: " << descriptor
296  << "\n different number of parameters, reverting to "
297  "descriptor"
298  << message.eom;
299  }
300  }
302  {
303  message.warning() << "Method: " << class_name << "." << method_name
304  << "\n could not parse signature: " << signature.value()
305  << "\n " << e.what() << "\n"
306  << " reverting to descriptor: " << descriptor
307  << message.eom;
308  }
309  }
310  return to_java_method_type(member_type_from_descriptor);
311 }
312 
320  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
321  const size_t index)
322 {
323  const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
324  // If the lambda method handle has an unknown type, it does not refer to
325  // any symbol (it is a symbol expression with empty identifier)
326  if(!lambda_method_handle.get_identifier().empty())
327  return symbol_table.lookup_ref(lambda_method_handle.get_identifier());
328  return {};
329 }
330 
341  const symbolt &class_symbol,
342  const irep_idt &method_identifier,
344  symbol_tablet &symbol_table,
346 {
347  symbolt method_symbol;
348 
349  java_method_typet member_type = member_type_lazy(
350  m.descriptor,
351  m.signature,
352  id2string(class_symbol.name),
353  id2string(m.base_name),
355 
356  method_symbol.name=method_identifier;
357  method_symbol.base_name=m.base_name;
358  method_symbol.mode=ID_java;
359  method_symbol.location=m.source_location;
360  method_symbol.location.set_function(method_identifier);
361 
362  if(m.is_public)
363  member_type.set_access(ID_public);
364  else if(m.is_protected)
365  member_type.set_access(ID_protected);
366  else if(m.is_private)
367  member_type.set_access(ID_private);
368  else
369  member_type.set_access(ID_default);
370 
371  if(m.is_synchronized)
372  member_type.set(ID_is_synchronized, true);
373  if(m.is_static)
374  member_type.set(ID_is_static, true);
375 
376  if(m.is_bridge)
377  member_type.set(ID_is_bridge_method, m.is_bridge);
378 
379  // do we need to add 'this' as a parameter?
380  if(!m.is_static)
381  {
382  java_method_typet::parameterst &parameters = member_type.parameters();
384  const reference_typet object_ref_type=
385  java_reference_type(symbol_typet(class_symbol.name));
386  this_p.type()=object_ref_type;
387  this_p.set_this();
388  parameters.insert(parameters.begin(), this_p);
389  }
390 
391  const std::string signature_string = pretty_signature(member_type);
392 
393  if(is_constructor(method_symbol.base_name))
394  {
395  // we use full.class_name(...) as pretty name
396  // for constructors -- the idea is that they have
397  // an empty declarator.
398  method_symbol.pretty_name=
399  id2string(class_symbol.pretty_name) + signature_string;
400 
401  member_type.set_is_constructor();
402  }
403  else
404  {
405  method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
406  id2string(m.base_name) + signature_string;
407  }
408 
409  // Load annotations
410  if(!m.annotations.empty())
411  {
413  m.annotations,
414  type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
415  .get_annotations());
416  }
417 
418  method_symbol.type=member_type;
419  // Not used in jbmc at present, but other codebases that use jbmc as a library
420  // use this information.
421  method_symbol.type.set(ID_C_abstract, m.is_abstract);
422 
424  m.annotations, "java::org.cprover.MustNotThrow"))
425  {
426  method_symbol.type.set(ID_C_must_not_throw, true);
427  }
428 
429  symbol_table.add(method_symbol);
430 }
431 
433  const symbolt &class_symbol,
434  const methodt &m)
435 {
436  // Construct the fully qualified method name
437  // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table
438  // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
439  // associated to the method
440  const irep_idt method_identifier=
441  id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
442  method_id=method_identifier;
443 
444  symbolt &method_symbol=*symbol_table.get_writeable(method_identifier);
445 
446  // Obtain a std::vector of java_method_typet::parametert objects from the
447  // (function) type of the symbol
448  java_method_typet method_type = to_java_method_type(method_symbol.type);
449  method_type.set(ID_C_class, class_symbol.name);
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  symbol_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 
679  codet &repl,
680  const irep_idt &old_label,
681  const irep_idt &new_label)
682 {
683  const auto &stmt=repl.get_statement();
684  if(stmt==ID_goto)
685  {
686  auto &g=to_code_goto(repl);
687  if(g.get_destination()==old_label)
688  g.set_destination(new_label);
689  }
690  else
691  {
692  for(auto &op : repl.operands())
693  if(op.id()==ID_code)
694  replace_goto_target(to_code(op), old_label, new_label);
695  }
696 }
697 
713  block_tree_nodet &tree,
714  code_blockt &this_block,
715  unsigned address_start,
716  unsigned address_limit,
717  unsigned next_block_start_address)
718 {
719  address_mapt dummy;
721  tree,
722  this_block,
723  address_start,
724  address_limit,
725  next_block_start_address,
726  dummy,
727  false);
728 }
729 
745  block_tree_nodet &tree,
746  code_blockt &this_block,
747  unsigned address_start,
748  unsigned address_limit,
749  unsigned next_block_start_address,
750  const address_mapt &amap,
751  bool allow_merge)
752 {
753  // Check the tree shape invariant:
754  assert(tree.branch.size()==tree.branch_addresses.size());
755 
756  // If there are no child blocks, return this.
757  if(tree.leaf)
758  return this_block;
759  assert(!tree.branch.empty());
760 
761  // Find child block starting > address_start:
762  const auto afterstart=
763  std::upper_bound(
764  tree.branch_addresses.begin(),
765  tree.branch_addresses.end(),
766  address_start);
767  assert(afterstart!=tree.branch_addresses.begin());
768  auto findstart=afterstart;
769  --findstart;
770  auto child_offset=
771  std::distance(tree.branch_addresses.begin(), findstart);
772 
773  // Find child block starting >= address_limit:
774  auto findlim=
775  std::lower_bound(
776  tree.branch_addresses.begin(),
777  tree.branch_addresses.end(),
778  address_limit);
779  unsigned findlim_block_start_address=
780  findlim==tree.branch_addresses.end() ?
781  next_block_start_address :
782  (*findlim);
783 
784  // If all children are in scope, return this.
785  if(findstart==tree.branch_addresses.begin() &&
786  findlim==tree.branch_addresses.end())
787  return this_block;
788 
789  // Find the child code_blockt where the queried range begins:
790  auto child_iter=this_block.operands().begin();
791  // Skip any top-of-block declarations;
792  // all other children are labelled subblocks.
793  while(child_iter!=this_block.operands().end() &&
794  to_code(*child_iter).get_statement()==ID_decl)
795  ++child_iter;
796  assert(child_iter!=this_block.operands().end());
797  std::advance(child_iter, child_offset);
798  assert(child_iter!=this_block.operands().end());
799  auto &child_label=to_code_label(to_code(*child_iter));
800  auto &child_block=to_code_block(child_label.code());
801 
802  bool single_child(afterstart==findlim);
803  if(single_child)
804  {
805  // Range wholly contained within a child block
807  tree.branch[child_offset],
808  child_block,
809  address_start,
810  address_limit,
811  findlim_block_start_address,
812  amap,
813  allow_merge);
814  }
815 
816  // Otherwise we're being asked for a range of subblocks, but not all of them.
817  // If it's legal to draw a new lexical scope around the requested subset,
818  // do so; otherwise just return this block.
819 
820  // This can be a new lexical scope if all incoming edges target the
821  // new block header, or come from within the suggested new block.
822 
823  // If modifying the block tree is forbidden, give up and return this:
824  if(!allow_merge)
825  return this_block;
826 
827  // Check for incoming control-flow edges targeting non-header
828  // blocks of the new proposed block range:
829  auto checkit=amap.find(*findstart);
830  assert(checkit!=amap.end());
831  ++checkit; // Skip the header, which can have incoming edges from outside.
832  for(;
833  checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
834  ++checkit)
835  {
836  for(auto p : checkit->second.predecessors)
837  {
838  if(p<(*findstart) || p>=findlim_block_start_address)
839  {
840  debug() << "Generating codet: "
841  << "warning: refusing to create lexical block spanning "
842  << (*findstart) << "-" << findlim_block_start_address
843  << " due to incoming edge " << p << " -> "
844  << checkit->first << eom;
845  return this_block;
846  }
847  }
848  }
849 
850  // All incoming edges are acceptable! Create a new block wrapping
851  // the relevant children. Borrow the header block's label, and redirect
852  // any block-internal edges to target the inner header block.
853 
854  const irep_idt child_label_name=child_label.get_label();
855  std::string new_label_str = id2string(child_label_name);
856  new_label_str+='$';
857  irep_idt new_label_irep(new_label_str);
858 
859  code_labelt newlabel(child_label_name, code_blockt());
860  code_blockt &newblock=to_code_block(newlabel.code());
861  auto nblocks=std::distance(findstart, findlim);
862  assert(nblocks>=2);
863  debug() << "Generating codet: combining "
864  << std::distance(findstart, findlim)
865  << " blocks for addresses " << (*findstart) << "-"
866  << findlim_block_start_address << eom;
867 
868  // Make a new block containing every child of interest:
869  auto &this_block_children=this_block.operands();
870  assert(tree.branch.size()==this_block_children.size());
871  for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
872  blockidx!=blocklim;
873  ++blockidx)
874  newblock.move_to_operands(this_block_children[blockidx]);
875 
876  // Relabel the inner header:
877  to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
878  // Relabel internal gotos:
879  replace_goto_target(newblock, child_label_name, new_label_irep);
880 
881  // Remove the now-empty sibling blocks:
882  auto delfirst=this_block_children.begin();
883  std::advance(delfirst, child_offset+1);
884  auto dellim=delfirst;
885  std::advance(dellim, nblocks-1);
886  this_block_children.erase(delfirst, dellim);
887  this_block_children[child_offset].swap(newlabel);
888 
889  // Perform the same transformation on the index tree:
890  block_tree_nodet newnode;
891  auto branchstart=tree.branch.begin();
892  std::advance(branchstart, child_offset);
893  auto branchlim=branchstart;
894  std::advance(branchlim, nblocks);
895  for(auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
896  newnode.branch.push_back(std::move(*branchiter));
897  ++branchstart;
898  tree.branch.erase(branchstart, branchlim);
899 
900  assert(tree.branch.size()==this_block_children.size());
901 
902  auto branchaddriter=tree.branch_addresses.begin();
903  std::advance(branchaddriter, child_offset);
904  auto branchaddrlim=branchaddriter;
905  std::advance(branchaddrlim, nblocks);
906  newnode.branch_addresses.insert(
907  newnode.branch_addresses.begin(),
908  branchaddriter,
909  branchaddrlim);
910 
911  ++branchaddriter;
912  tree.branch_addresses.erase(branchaddriter, branchaddrlim);
913 
914  tree.branch[child_offset]=std::move(newnode);
915 
916  assert(tree.branch.size()==tree.branch_addresses.size());
917 
918  return
921  to_code(this_block_children[child_offset])).code());
922 }
923 
925  unsigned pc,
926  const exprt &e,
927  std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
928 {
929  if(e.id()==ID_symbol)
930  {
931  const auto &symexpr=to_symbol_expr(e);
932  auto findit = result.insert(
933  {symexpr.get_identifier(), java_bytecode_convert_methodt::variablet()});
934  auto &var=findit.first->second;
935  if(findit.second)
936  {
937  var.symbol_expr=symexpr;
938  var.start_pc=pc;
939  var.length=1;
940  }
941  else
942  {
943  if(pc<var.start_pc)
944  {
945  var.length+=(var.start_pc-pc);
946  var.start_pc=pc;
947  }
948  else
949  {
950  var.length=std::max(var.length, (pc-var.start_pc)+1);
951  }
952  }
953  }
954  else
955  {
956  forall_operands(it, e)
957  gather_symbol_live_ranges(pc, *it, result);
958  }
959 }
960 
967  const irep_idt &classname)
968 {
969  auto findit = symbol_table.symbols.find(clinit_wrapper_name(classname));
970  if(findit == symbol_table.symbols.end())
971  return code_skipt();
972  else
973  {
975  ret.function() = findit->second.symbol_expr();
977  needed_lazy_methods->add_needed_method(findit->second.name);
978  return ret;
979  }
980 }
981 
982 static std::size_t get_bytecode_type_width(const typet &ty)
983 {
984  if(ty.id()==ID_pointer)
985  return 32;
986  return ty.get_size_t(ID_width);
987 }
988 
990  const methodt &method,
991  const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
992 {
993  const instructionst &instructions=method.instructions;
994 
995  // Run a worklist algorithm, assuming that the bytecode has not
996  // been tampered with. See "Leroy, X. (2003). Java bytecode
997  // verification: algorithms and formalizations. Journal of Automated
998  // Reasoning, 30(3-4), 235-269." for a more complete treatment.
999 
1000  // first pass: get targets and map addresses to instructions
1001 
1002  address_mapt address_map;
1003  std::set<unsigned> targets;
1004 
1005  std::vector<unsigned> jsr_ret_targets;
1006  std::vector<instructionst::const_iterator> ret_instructions;
1007 
1008  for(auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1009  {
1011  std::pair<address_mapt::iterator, bool> a_entry=
1012  address_map.insert(std::make_pair(i_it->address, ins));
1013  assert(a_entry.second);
1014  // addresses are strictly increasing, hence we must have inserted
1015  // a new maximal key
1016  assert(a_entry.first==--address_map.end());
1017 
1018  if(i_it->statement!="goto" &&
1019  i_it->statement!="return" &&
1020  !(i_it->statement==patternt("?return")) &&
1021  i_it->statement!="athrow" &&
1022  i_it->statement!="jsr" &&
1023  i_it->statement!="jsr_w" &&
1024  i_it->statement!="ret")
1025  {
1026  instructionst::const_iterator next=i_it;
1027  if(++next!=instructions.end())
1028  a_entry.first->second.successors.push_back(next->address);
1029  }
1030 
1031  if(i_it->statement=="athrow" ||
1032  i_it->statement=="putfield" ||
1033  i_it->statement=="getfield" ||
1034  i_it->statement=="checkcast" ||
1035  i_it->statement=="newarray" ||
1036  i_it->statement=="anewarray" ||
1037  i_it->statement=="idiv" ||
1038  i_it->statement=="ldiv" ||
1039  i_it->statement=="irem" ||
1040  i_it->statement=="lrem" ||
1041  i_it->statement==patternt("?astore") ||
1042  i_it->statement==patternt("?aload") ||
1043  i_it->statement=="invokestatic" ||
1044  i_it->statement=="invokevirtual" ||
1045  i_it->statement=="invokespecial" ||
1046  i_it->statement=="invokeinterface" ||
1047  (threading_support && (i_it->statement=="monitorenter" ||
1048  i_it->statement=="monitorexit")))
1049  {
1050  const std::vector<unsigned int> handler =
1051  try_catch_handler(i_it->address, method.exception_table);
1052  std::list<unsigned int> &successors = a_entry.first->second.successors;
1053  successors.insert(successors.end(), handler.begin(), handler.end());
1054  targets.insert(handler.begin(), handler.end());
1055  }
1056 
1057  if(i_it->statement=="goto" ||
1058  i_it->statement==patternt("if_?cmp??") ||
1059  i_it->statement==patternt("if??") ||
1060  i_it->statement=="ifnonnull" ||
1061  i_it->statement=="ifnull" ||
1062  i_it->statement=="jsr" ||
1063  i_it->statement=="jsr_w")
1064  {
1065  PRECONDITION(!i_it->args.empty());
1066 
1067  unsigned target;
1068  bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
1069  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
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  unsigned target;
1093  bool ret=to_unsigned_integer(to_constant_expr(arg), target);
1094  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
1095  targets.insert(target);
1096  a_entry.first->second.successors.push_back(target);
1097  }
1098  is_label=!is_label;
1099  }
1100  }
1101  else if(i_it->statement=="ret")
1102  {
1103  // Finish these later, once we've seen all jsr instructions.
1104  ret_instructions.push_back(i_it);
1105  }
1106  }
1107  draw_edges_from_ret_to_jsr(address_map, jsr_ret_targets, ret_instructions);
1108 
1109  for(const auto &address : address_map)
1110  {
1111  for(unsigned s : address.second.successors)
1112  {
1113  const auto a_it = address_map.find(s);
1114  CHECK_RETURN(a_it != address_map.end());
1115  a_it->second.predecessors.insert(address.first);
1116  }
1117  }
1118 
1119  // Clean the list of temporary variables created by a call to `tmp_variable`.
1120  // These are local variables in the goto function used to represent temporary
1121  // values of the JVM operand stack, newly allocated objects before the
1122  // constructor is called, ...
1123  tmp_vars.clear();
1124 
1125  // Now that the control flow graph is built, set up our local variables
1126  // (these require the graph to determine live ranges)
1127  setup_local_variables(method, address_map);
1128 
1129  std::set<unsigned> working_set;
1130 
1131  if(!instructions.empty())
1132  working_set.insert(instructions.front().address);
1133 
1134  while(!working_set.empty())
1135  {
1136  auto cur = working_set.begin();
1137  auto address_it = address_map.find(*cur);
1138  CHECK_RETURN(address_it != address_map.end());
1139  auto &instruction = address_it->second;
1140  unsigned cur_pc=*cur;
1141  working_set.erase(cur);
1142 
1143  if(instruction.done)
1144  continue;
1145  working_set.insert(
1146  instruction.successors.begin(), instruction.successors.end());
1147 
1148  instructionst::const_iterator i_it = instruction.source;
1149  stack.swap(instruction.stack);
1150  instruction.stack.clear();
1151  codet &c = instruction.code;
1152 
1153  assert(
1154  stack.empty() || instruction.predecessors.size() <= 1 ||
1155  has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
1156 
1157  irep_idt statement=i_it->statement;
1158  exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
1159  exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
1160 
1162 
1163  // deal with _idx suffixes
1164  if(statement.size()>=2 &&
1165  statement[statement.size()-2]=='_' &&
1166  isdigit(statement[statement.size()-1]))
1167  {
1168  arg0=
1169  from_integer(
1171  std::string(id2string(statement), statement.size()-1, 1)),
1172  java_int_type());
1173  statement=std::string(id2string(statement), 0, statement.size()-2);
1174  }
1175 
1176  typet catch_type;
1177 
1178  // Find catch blocks that begin here. For now we assume if more than
1179  // one catch targets the same bytecode then we must be indifferent to
1180  // its type and just call it a Throwable.
1181  auto it=method.exception_table.begin();
1182  for(; it!=method.exception_table.end(); ++it)
1183  {
1184  if(cur_pc==it->handler_pc)
1185  {
1186  if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt()))
1187  {
1188  catch_type=symbol_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  exprt r=op[0];
1292  if(r.type()!=method_return_type)
1294  c=code_returnt(r);
1295  }
1296  else if(statement==patternt("?astore"))
1297  {
1298  assert(op.size()==3 && results.empty());
1299  c = convert_astore(statement, op, i_it->source_location);
1300  }
1301  else if(statement==patternt("?store"))
1302  {
1303  // store value into some local variable
1304  PRECONDITION(op.size() == 1 && results.empty());
1305  c = convert_store(
1306  statement, arg0, op, i_it->address, i_it->source_location);
1307  }
1308  else if(statement==patternt("?aload"))
1309  {
1310  PRECONDITION(op.size() == 2 && results.size() == 1);
1311  results[0] = convert_aload(statement, op);
1312  }
1313  else if(statement==patternt("?load"))
1314  {
1315  // load a value from a local variable
1316  results[0]=
1317  variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED);
1318  }
1319  else if(statement=="ldc" || statement=="ldc_w" ||
1320  statement=="ldc2" || statement=="ldc2_w")
1321  {
1322  PRECONDITION(op.empty() && results.size() == 1);
1323 
1324  INVARIANT(
1325  arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
1326  "String and Class literals should have been lowered in "
1327  "generate_constant_global_variables");
1328 
1329  results[0] = arg0;
1330  }
1331  else if(statement=="goto" || statement=="goto_w")
1332  {
1333  PRECONDITION(op.empty() && results.empty());
1334  mp_integer number;
1335  bool ret=to_integer(to_constant_expr(arg0), number);
1336  INVARIANT(!ret, "goto argument should be an integer");
1337  code_gotot code_goto(label(integer2string(number)));
1338  c=code_goto;
1339  }
1340  else if(statement=="jsr" || statement=="jsr_w")
1341  {
1342  // As 'goto', except we must also push the subroutine return address:
1343  PRECONDITION(op.empty() && results.size() == 1);
1344  mp_integer number;
1345  bool ret=to_integer(to_constant_expr(arg0), number);
1346  INVARIANT(!ret, "jsr argument should be an integer");
1347  code_gotot code_goto(label(integer2string(number)));
1348  c=code_goto;
1349  results[0]=
1350  from_integer(
1351  std::next(i_it)->address,
1352  unsignedbv_typet(64));
1353  results[0].type()=pointer_type(void_typet());
1354  }
1355  else if(statement=="ret")
1356  {
1357  // Since we have a bounded target set, make life easier on our analyses
1358  // and write something like:
1359  // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
1360  PRECONDITION(op.empty() && results.empty());
1361  assert(!jsr_ret_targets.empty());
1362  c = convert_ret(
1363  jsr_ret_targets, arg0, i_it->source_location, i_it->address);
1364  }
1365  else if(statement=="iconst_m1")
1366  {
1367  assert(results.size()==1);
1368  results[0]=from_integer(-1, java_int_type());
1369  }
1370  else if(statement==patternt("?const"))
1371  {
1372  assert(results.size()==1);
1373  results = convert_const(statement, arg0, results);
1374  }
1375  else if(statement==patternt("?ipush"))
1376  {
1377  PRECONDITION(results.size()==1);
1379  arg0.id()==ID_constant,
1380  "ipush argument expected to be constant");
1381  results[0]=arg0;
1382  if(arg0.type()!=java_int_type())
1383  results[0].make_typecast(java_int_type());
1384  }
1385  else if(statement==patternt("if_?cmp??"))
1386  {
1387  PRECONDITION(op.size() == 2 && results.empty());
1388  mp_integer number;
1389  bool ret=to_integer(to_constant_expr(arg0), number);
1390  INVARIANT(!ret, "if_?cmp?? argument should be an integer");
1391  c = convert_if_cmp(
1392  address_map, statement, op, number, i_it->source_location);
1393  }
1394  else if(statement==patternt("if??"))
1395  {
1396  const irep_idt id=
1397  statement=="ifeq"?ID_equal:
1398  statement=="ifne"?ID_notequal:
1399  statement=="iflt"?ID_lt:
1400  statement=="ifge"?ID_ge:
1401  statement=="ifgt"?ID_gt:
1402  statement=="ifle"?ID_le:
1403  irep_idt();
1404 
1405  INVARIANT(!id.empty(), "unexpected bytecode-if");
1406  PRECONDITION(op.size() == 1 && results.empty());
1407  mp_integer number;
1408  bool ret=to_integer(to_constant_expr(arg0), number);
1409  INVARIANT(!ret, "if?? argument should be an integer");
1410  c = convert_if(address_map, op, id, number, i_it->source_location);
1411  }
1412  else if(statement==patternt("ifnonnull"))
1413  {
1414  PRECONDITION(op.size() == 1 && results.empty());
1415  mp_integer number;
1416  bool ret=to_integer(to_constant_expr(arg0), number);
1417  INVARIANT(!ret, "ifnonnull argument should be an integer");
1418  c = convert_ifnonull(address_map, op, number, i_it->source_location);
1419  }
1420  else if(statement==patternt("ifnull"))
1421  {
1422  PRECONDITION(op.size() == 1 && results.empty());
1423  mp_integer number;
1424  bool ret=to_integer(to_constant_expr(arg0), number);
1425  INVARIANT(!ret, "ifnull argument should be an integer");
1426  c = convert_ifnull(address_map, op, number, i_it->source_location);
1427  }
1428  else if(statement=="iinc")
1429  {
1430  c = convert_iinc(arg0, arg1, i_it->source_location, i_it->address);
1431  }
1432  else if(statement==patternt("?xor"))
1433  {
1434  PRECONDITION(op.size() == 2 && results.size() == 1);
1435  results[0]=bitxor_exprt(op[0], op[1]);
1436  }
1437  else if(statement==patternt("?or"))
1438  {
1439  PRECONDITION(op.size() == 2 && results.size() == 1);
1440  results[0]=bitor_exprt(op[0], op[1]);
1441  }
1442  else if(statement==patternt("?and"))
1443  {
1444  PRECONDITION(op.size() == 2 && results.size() == 1);
1445  results[0]=bitand_exprt(op[0], op[1]);
1446  }
1447  else if(statement==patternt("?shl"))
1448  {
1449  PRECONDITION(op.size() == 2 && results.size() == 1);
1450  results[0]=shl_exprt(op[0], op[1]);
1451  }
1452  else if(statement==patternt("?shr"))
1453  {
1454  PRECONDITION(op.size() == 2 && results.size() == 1);
1455  results[0]=ashr_exprt(op[0], op[1]);
1456  }
1457  else if(statement==patternt("?ushr"))
1458  {
1459  PRECONDITION(op.size() == 2 && results.size() == 1);
1460  results = convert_ushr(statement, op, results);
1461  }
1462  else if(statement==patternt("?add"))
1463  {
1464  PRECONDITION(op.size() == 2 && results.size() == 1);
1465  results[0]=plus_exprt(op[0], op[1]);
1466  }
1467  else if(statement==patternt("?sub"))
1468  {
1469  PRECONDITION(op.size() == 2 && results.size() == 1);
1470  results[0]=minus_exprt(op[0], op[1]);
1471  }
1472  else if(statement==patternt("?div"))
1473  {
1474  PRECONDITION(op.size() == 2 && results.size() == 1);
1475  results[0]=div_exprt(op[0], op[1]);
1476  }
1477  else if(statement==patternt("?mul"))
1478  {
1479  PRECONDITION(op.size() == 2 && results.size() == 1);
1480  results[0]=mult_exprt(op[0], op[1]);
1481  }
1482  else if(statement==patternt("?neg"))
1483  {
1484  PRECONDITION(op.size() == 1 && results.size() == 1);
1485  results[0]=unary_minus_exprt(op[0], op[0].type());
1486  }
1487  else if(statement==patternt("?rem"))
1488  {
1489  PRECONDITION(op.size() == 2 && results.size() == 1);
1490  if(statement=="frem" || statement=="drem")
1491  results[0]=rem_exprt(op[0], op[1]);
1492  else
1493  results[0]=mod_exprt(op[0], op[1]);
1494  }
1495  else if(statement==patternt("?cmp"))
1496  {
1497  PRECONDITION(op.size() == 2 && results.size() == 1);
1498  results = convert_cmp(op, results);
1499  }
1500  else if(statement==patternt("?cmp?"))
1501  {
1502  PRECONDITION(op.size() == 2 && results.size() == 1);
1503  results = convert_cmp2(statement, op, results);
1504  }
1505  else if(statement==patternt("?cmpl"))
1506  {
1507  PRECONDITION(op.size() == 2 && results.size() == 1);
1508  results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
1509  }
1510  else if(statement=="dup")
1511  {
1512  PRECONDITION(op.size() == 1 && results.size() == 2);
1513  results[0]=results[1]=op[0];
1514  }
1515  else if(statement=="dup_x1")
1516  {
1517  PRECONDITION(op.size() == 2 && results.size() == 3);
1518  results[0]=op[1];
1519  results[1]=op[0];
1520  results[2]=op[1];
1521  }
1522  else if(statement=="dup_x2")
1523  {
1524  PRECONDITION(op.size() == 3 && results.size() == 4);
1525  results[0]=op[2];
1526  results[1]=op[0];
1527  results[2]=op[1];
1528  results[3]=op[2];
1529  }
1530  // dup2* behaviour depends on the size of the operands on the
1531  // stack
1532  else if(statement=="dup2")
1533  {
1534  PRECONDITION(!stack.empty() && results.empty());
1535  convert_dup2(op, results);
1536  }
1537  else if(statement=="dup2_x1")
1538  {
1539  PRECONDITION(!stack.empty() && results.empty());
1540  convert_dup2_x1(op, results);
1541  }
1542  else if(statement=="dup2_x2")
1543  {
1544  PRECONDITION(!stack.empty() && results.empty());
1545  convert_dup2_x2(op, results);
1546  }
1547  else if(statement=="dconst")
1548  {
1549  PRECONDITION(op.empty() && results.size() == 1);
1550  }
1551  else if(statement=="fconst")
1552  {
1553  PRECONDITION(op.empty() && results.size() == 1);
1554  }
1555  else if(statement=="getfield")
1556  {
1557  PRECONDITION(op.size() == 1 && results.size() == 1);
1558  results[0]=java_bytecode_promotion(to_member(op[0], arg0));
1559  }
1560  else if(statement=="getstatic")
1561  {
1562  PRECONDITION(op.empty() && results.size() == 1);
1563  symbol_exprt symbol_expr(arg0.type());
1564  const auto &field_name=arg0.get_string(ID_component_name);
1565  const bool is_assertions_disabled_field=
1566  field_name.find("$assertionsDisabled")!=std::string::npos;
1567 
1568  symbol_expr.set_identifier(
1569  get_static_field(arg0.get_string(ID_class), field_name));
1570 
1571  INVARIANT(
1572  symbol_table.has_symbol(symbol_expr.get_identifier()),
1573  "getstatic symbol should have been created before method conversion");
1574 
1576  arg0, symbol_expr, is_assertions_disabled_field, c, results);
1577  }
1578  else if(statement=="putfield")
1579  {
1580  PRECONDITION(op.size() == 2 && results.empty());
1581  c = convert_putfield(arg0, op);
1582  }
1583  else if(statement=="putstatic")
1584  {
1585  PRECONDITION(op.size() == 1 && results.empty());
1586  symbol_exprt symbol_expr(arg0.type());
1587  const auto &field_name=arg0.get_string(ID_component_name);
1588  symbol_expr.set_identifier(
1589  get_static_field(arg0.get_string(ID_class), field_name));
1590 
1591  INVARIANT(
1592  symbol_table.has_symbol(symbol_expr.get_identifier()),
1593  "putstatic symbol should have been created before method conversion");
1594 
1595  c = convert_putstatic(i_it->source_location, arg0, op, symbol_expr);
1596  }
1597  else if(statement==patternt("?2?")) // i2c etc.
1598  {
1599  PRECONDITION(op.size() == 1 && results.size() == 1);
1600  typet type=java_type_from_char(statement[2]);
1601  results[0]=op[0];
1602  if(results[0].type()!=type)
1603  results[0].make_typecast(type);
1604  }
1605  else if(statement=="new")
1606  {
1607  // use temporary since the stack symbol might get duplicated
1608  PRECONDITION(op.empty() && results.size() == 1);
1609  convert_new(i_it->source_location, arg0, c, results);
1610  }
1611  else if(statement=="newarray" ||
1612  statement=="anewarray")
1613  {
1614  // the op is the array size
1615  PRECONDITION(op.size() == 1 && results.size() == 1);
1616  convert_newarray(i_it->source_location, statement, arg0, op, c, results);
1617  }
1618  else if(statement=="multianewarray")
1619  {
1620  // The first argument is the type, the second argument is the number of
1621  // dimensions. The size of each dimension is on the stack.
1622  mp_integer number;
1623  bool ret=to_integer(to_constant_expr(arg1), number);
1624  INVARIANT(!ret, "multianewarray argument should be an integer");
1625  std::size_t dimension=integer2size_t(number);
1626 
1627  op=pop(dimension);
1628  assert(results.size()==1);
1629  convert_multianewarray(i_it->source_location, arg0, op, c, results);
1630  }
1631  else if(statement=="arraylength")
1632  {
1633  PRECONDITION(op.size() == 1 && results.size() == 1);
1634 
1635  const typecast_exprt pointer(op[0], java_array_type(statement[0]));
1636 
1637  dereference_exprt array(pointer, pointer.type().subtype());
1638  assert(pointer.type().subtype().id()==ID_symbol);
1639  array.set(ID_java_member_access, true);
1640 
1641  const member_exprt length(array, "length", java_int_type());
1642 
1643  results[0]=length;
1644  }
1645  else if(statement=="tableswitch" ||
1646  statement=="lookupswitch")
1647  {
1648  PRECONDITION(op.size() == 1 && results.empty());
1649  c = convert_switch(address_map, op, i_it->args, i_it->source_location);
1650  }
1651  else if(statement=="pop" || statement=="pop2")
1652  {
1653  c = convert_pop(statement, op);
1654  }
1655  else if(statement=="instanceof")
1656  {
1657  PRECONDITION(op.size() == 1 && results.size() == 1);
1658 
1659  results[0]=
1660  binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
1661  }
1662  else if(statement == "monitorenter" || statement == "monitorexit")
1663  {
1664  c = convert_monitorenterexit(statement, op, i_it->source_location);
1665  }
1666  else if(statement=="swap")
1667  {
1668  PRECONDITION(op.size() == 2 && results.size() == 2);
1669  results[1]=op[0];
1670  results[0]=op[1];
1671  }
1672  else if(statement=="nop")
1673  {
1674  c=code_skipt();
1675  }
1676  else
1677  {
1678  c=codet(statement);
1679  c.operands()=op;
1680  }
1681 
1682  c = do_exception_handling(method, working_set, cur_pc, c);
1683 
1684  // Finally if this is the beginning of a catch block (already determined
1685  // before the big bytecode switch), insert the exception 'landing pad'
1686  // instruction before the actual instruction:
1687  if(catch_instruction!=codet())
1688  {
1689  c.make_block();
1690  c.operands().insert(c.operands().begin(), catch_instruction);
1691  }
1692 
1693  if(!i_it->source_location.get_line().empty())
1695 
1696  push(results);
1697 
1698  instruction.done = true;
1699  for(const unsigned address : instruction.successors)
1700  {
1701  address_mapt::iterator a_it2=address_map.find(address);
1702  CHECK_RETURN(a_it2 != address_map.end());
1703 
1704  // clear the stack if this is an exception handler
1705  for(const auto &exception_row : method.exception_table)
1706  {
1707  if(address==exception_row.handler_pc)
1708  {
1709  stack.clear();
1710  break;
1711  }
1712  }
1713 
1714  if(!stack.empty() && a_it2->second.predecessors.size()>1)
1715  {
1716  // copy into temporaries
1717  code_blockt more_code;
1718 
1719  // introduce temporaries when successor is seen for the first
1720  // time
1721  if(a_it2->second.stack.empty())
1722  {
1723  for(stackt::iterator s_it=stack.begin();
1724  s_it!=stack.end();
1725  ++s_it)
1726  {
1727  symbol_exprt lhs=tmp_variable("$stack", s_it->type());
1728  code_assignt a(lhs, *s_it);
1729  more_code.copy_to_operands(a);
1730 
1731  s_it->swap(lhs);
1732  }
1733  }
1734  else
1735  {
1736  INVARIANT(
1737  a_it2->second.stack.size() == stack.size(),
1738  "Stack sizes should be the same.");
1739  stackt::const_iterator os_it=a_it2->second.stack.begin();
1740  for(auto &expr : stack)
1741  {
1742  assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
1743  symbol_exprt lhs=to_symbol_expr(*os_it);
1744  code_assignt a(lhs, expr);
1745  more_code.copy_to_operands(a);
1746 
1747  expr.swap(lhs);
1748  ++os_it;
1749  }
1750  }
1751 
1752  if(results.empty())
1753  {
1754  more_code.copy_to_operands(c);
1755  c.swap(more_code);
1756  }
1757  else
1758  {
1759  c.make_block();
1760  auto &last_statement=to_code_block(c).find_last_statement();
1761  if(last_statement.get_statement()==ID_goto)
1762  {
1763  // Insert stack twiddling before branch:
1764  last_statement.make_block();
1765  last_statement.operands().insert(
1766  last_statement.operands().begin(),
1767  more_code.operands().begin(),
1768  more_code.operands().end());
1769  }
1770  else
1771  forall_operands(o_it, more_code)
1772  c.copy_to_operands(*o_it);
1773  }
1774  }
1775  a_it2->second.stack=stack;
1776  }
1777  }
1778 
1779  code_blockt code;
1780 
1781  // Add anonymous locals to the symtab:
1782  for(const auto &var : used_local_names)
1783  {
1784  symbolt new_symbol;
1785  new_symbol.name=var.get_identifier();
1786  new_symbol.type=var.type();
1787  new_symbol.base_name=var.get(ID_C_base_name);
1788  new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
1789  new_symbol.mode=ID_java;
1790  new_symbol.is_type=false;
1791  new_symbol.is_file_local=true;
1792  new_symbol.is_thread_local=true;
1793  new_symbol.is_lvalue=true;
1794  symbol_table.add(new_symbol);
1795  }
1796 
1797  // Try to recover block structure as indicated in the local variable table:
1798 
1799  // The block tree node mirrors the block structure of root_block,
1800  // indexing the Java PCs where each subblock starts and ends.
1801  block_tree_nodet root;
1802  code_blockt root_block;
1803 
1804  // First create a simple flat list of basic blocks. We'll add lexical nesting
1805  // constructs as variable live-ranges require next.
1806  bool start_new_block=true;
1807  bool has_seen_previous_address=false;
1808  unsigned previous_address=0;
1809  for(const auto &address_pair : address_map)
1810  {
1811  const unsigned address=address_pair.first;
1812  assert(address_pair.first==address_pair.second.source->address);
1813  const codet &c=address_pair.second.code;
1814 
1815  // Start a new lexical block if this is a branch target:
1816  if(!start_new_block)
1817  start_new_block=targets.find(address)!=targets.end();
1818  // Start a new lexical block if this is a control flow join
1819  // (e.g. due to exceptional control flow)
1820  if(!start_new_block)
1821  start_new_block=address_pair.second.predecessors.size()>1;
1822  // Start a new lexical block if we've just entered a try block
1823  if(!start_new_block && has_seen_previous_address)
1824  {
1825  for(const auto &exception_row : method.exception_table)
1826  if(exception_row.start_pc==previous_address)
1827  {
1828  start_new_block=true;
1829  break;
1830  }
1831  }
1832 
1833  if(start_new_block)
1834  {
1835  code_labelt newlabel(label(std::to_string(address)), code_blockt());
1836  root_block.move_to_operands(newlabel);
1837  root.branch.push_back(block_tree_nodet::get_leaf());
1838  assert((root.branch_addresses.empty() ||
1839  root.branch_addresses.back()<address) &&
1840  "Block addresses should be unique and increasing");
1841  root.branch_addresses.push_back(address);
1842  }
1843 
1844  if(c.get_statement()!=ID_skip)
1845  {
1846  auto &lastlabel=to_code_label(to_code(root_block.operands().back()));
1847  auto &add_to_block=to_code_block(lastlabel.code());
1848  add_to_block.add(c);
1849  }
1850  start_new_block=address_pair.second.successors.size()>1;
1851 
1852  previous_address=address;
1853  has_seen_previous_address=true;
1854  }
1855 
1856  // Find out where temporaries are used:
1857  std::map<irep_idt, variablet> temporary_variable_live_ranges;
1858  for(const auto &aentry : address_map)
1860  aentry.first,
1861  aentry.second.code,
1862  temporary_variable_live_ranges);
1863 
1864  std::vector<const variablet*> vars_to_process;
1865  for(const auto &vlist : variables)
1866  for(const auto &v : vlist)
1867  vars_to_process.push_back(&v);
1868 
1869  for(const auto &v : tmp_vars)
1870  vars_to_process.push_back(
1871  &temporary_variable_live_ranges.at(v.get_identifier()));
1872 
1873  for(const auto &v : used_local_names)
1874  vars_to_process.push_back(
1875  &temporary_variable_live_ranges.at(v.get_identifier()));
1876 
1877  for(const auto vp : vars_to_process)
1878  {
1879  const auto &v=*vp;
1880  if(v.is_parameter)
1881  continue;
1882  // Merge lexical scopes as far as possible to allow us to
1883  // declare these variable scopes faithfully.
1884  // Don't insert yet, as for the time being the blocks' only
1885  // operands must be other blocks.
1886  // The declarations will be inserted in the next pass instead.
1888  root,
1889  root_block,
1890  v.start_pc,
1891  v.start_pc+v.length,
1892  std::numeric_limits<unsigned>::max(),
1893  address_map);
1894  }
1895  for(const auto vp : vars_to_process)
1896  {
1897  const auto &v=*vp;
1898  if(v.is_parameter)
1899  continue;
1900  // Skip anonymous variables:
1901  if(v.symbol_expr.get_identifier().empty())
1902  continue;
1903  auto &block=get_block_for_pcrange(
1904  root,
1905  root_block,
1906  v.start_pc,
1907  v.start_pc+v.length,
1908  std::numeric_limits<unsigned>::max());
1909  code_declt d(v.symbol_expr);
1910  block.operands().insert(block.operands().begin(), d);
1911  }
1912 
1913  for(auto &block : root_block.operands())
1914  code.move_to_operands(block);
1915 
1916  return code;
1917 }
1918 
1920  const irep_idt &statement,
1921  const exprt::operandst &op)
1922 {
1923  // these are skips
1924  codet c = code_skipt();
1925 
1926  // pop2 removes two single-word items from the stack (e.g. two
1927  // integers, or an integer and an object reference) or one
1928  // two-word item (i.e. a double or a long).
1929  // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
1930  if(statement == "pop2" && get_bytecode_type_width(op[0].type()) == 32)
1931  pop(1);
1932  return c;
1933 }
1934 
1937  const exprt::operandst &op,
1939  const source_locationt &location)
1940 {
1941  // we turn into switch-case
1942  code_switcht code_switch;
1943  code_switch.add_source_location() = location;
1944  code_switch.value() = op[0];
1945  code_blockt code_block;
1946  code_block.add_source_location() = location;
1947 
1948  bool is_label = true;
1949  for(auto a_it = args.begin(); a_it != args.end();
1950  a_it++, is_label = !is_label)
1951  {
1952  if(is_label)
1953  {
1954  code_switch_caset code_case;
1955  code_case.add_source_location() = location;
1956 
1957  mp_integer number;
1958  bool ret = to_integer(to_constant_expr(*a_it), number);
1959  DATA_INVARIANT(!ret, "case label expected to be integer");
1960  // The switch case does not contain any code, it just branches via a GOTO
1961  // to the jump target of the tableswitch/lookupswitch case at
1962  // hand. Therefore we consider this code to belong to the source bytecode
1963  // instruction and not the target instruction.
1964  code_case.code() = code_gotot(label(integer2string(number)));
1965  code_case.code().add_source_location() = location;
1966 
1967  if(a_it == args.begin())
1968  code_case.set_default();
1969  else
1970  {
1971  auto prev = a_it;
1972  prev--;
1973  code_case.case_op() = *prev;
1974  if(code_case.case_op().type() != op[0].type())
1975  code_case.case_op().make_typecast(op[0].type());
1976  code_case.case_op().add_source_location() = location;
1977  }
1978 
1979  code_block.add(code_case);
1980  }
1981  }
1982 
1983  code_switch.body() = code_block;
1984  return code_switch;
1985 }
1986 
1988  const irep_idt &statement,
1989  const exprt::operandst &op,
1990  const source_locationt &source_location)
1991 {
1992  const irep_idt descriptor = (statement == "monitorenter") ?
1993  "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
1994  "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
1995 
1996  if(!threading_support || !symbol_table.has_symbol(descriptor))
1997  return code_skipt();
1998 
1999  // becomes a function call
2000  java_method_typet type(
2002  void_typet());
2003  code_function_callt call;
2004  call.function() = symbol_exprt(descriptor, type);
2005  call.lhs().make_nil();
2006  call.arguments().push_back(op[0]);
2007  call.add_source_location() = source_location;
2008  if(needed_lazy_methods && symbol_table.has_symbol(descriptor))
2009  needed_lazy_methods->add_needed_method(descriptor);
2010  return call;
2011 }
2012 
2014  exprt::operandst &op,
2015  exprt::operandst &results)
2016 {
2017  if(get_bytecode_type_width(stack.back().type()) == 32)
2018  op = pop(2);
2019  else
2020  op = pop(1);
2021 
2022  results.insert(results.end(), op.begin(), op.end());
2023  results.insert(results.end(), op.begin(), op.end());
2024 }
2025 
2027  exprt::operandst &op,
2028  exprt::operandst &results)
2029 {
2030  if(get_bytecode_type_width(stack.back().type()) == 32)
2031  op = pop(3);
2032  else
2033  op = pop(2);
2034 
2035  results.insert(results.end(), op.begin() + 1, op.end());
2036  results.insert(results.end(), op.begin(), op.end());
2037 }
2038 
2040  exprt::operandst &op,
2041  exprt::operandst &results)
2042 {
2043  if(get_bytecode_type_width(stack.back().type()) == 32)
2044  op = pop(2);
2045  else
2046  op = pop(1);
2047 
2048  exprt::operandst op2;
2049 
2050  if(get_bytecode_type_width(stack.back().type()) == 32)
2051  op2 = pop(2);
2052  else
2053  op2 = pop(1);
2054 
2055  results.insert(results.end(), op.begin(), op.end());
2056  results.insert(results.end(), op2.begin(), op2.end());
2057  results.insert(results.end(), op.begin(), op.end());
2058 }
2059 
2061  const irep_idt &statement,
2062  const exprt &arg0,
2063  exprt::operandst &results) const
2064 {
2065  const char type_char = statement[0];
2066  const bool is_double('d' == type_char);
2067  const bool is_float('f' == type_char);
2068 
2069  if(is_double || is_float)
2070  {
2071  const ieee_float_spect spec(
2074 
2075  ieee_floatt value(spec);
2076  if(arg0.type().id() != ID_floatbv)
2077  {
2078  mp_integer number;
2079  bool ret = to_integer(to_constant_expr(arg0), number);
2080  DATA_INVARIANT(!ret, "failed to convert constant");
2081  value.from_integer(number);
2082  }
2083  else
2084  value.from_expr(to_constant_expr(arg0));
2085 
2086  results[0] = value.to_expr();
2087  }
2088  else
2089  {
2090  mp_integer value;
2091  bool ret = to_integer(to_constant_expr(arg0), value);
2092  DATA_INVARIANT(!ret, "failed to convert constant");
2093  const typet type = java_type_from_char(statement[0]);
2094  results[0] = from_integer(value, type);
2095  }
2096  return results;
2097 }
2098 
2100  source_locationt location,
2101  const irep_idt &statement,
2102  exprt &arg0,
2103  codet &c,
2104  exprt::operandst &results)
2105 {
2106  const bool use_this(statement != "invokestatic");
2107  const bool is_virtual(
2108  statement == "invokevirtual" || statement == "invokeinterface");
2109 
2110  java_method_typet &method_type = to_java_method_type(arg0.type());
2111  java_method_typet::parameterst &parameters(method_type.parameters());
2112 
2113  if(use_this)
2114  {
2115  if(parameters.empty() || !parameters[0].get_this())
2116  {
2117  irep_idt classname = arg0.get(ID_C_class);
2118  typet thistype = symbol_typet(classname);
2119  // Note invokespecial is used for super-method calls as well as
2120  // constructors.
2121  if(statement == "invokespecial")
2122  {
2123  if(is_constructor(arg0.get(ID_identifier)))
2124  {
2126  needed_lazy_methods->add_needed_class(classname);
2127  method_type.set_is_constructor();
2128  }
2129  else
2130  method_type.set(ID_java_super_method_call, true);
2131  }
2132  reference_typet object_ref_type = java_reference_type(thistype);
2133  java_method_typet::parametert this_p(object_ref_type);
2134  this_p.set_this();
2135  this_p.set_base_name("this");
2136  parameters.insert(parameters.begin(), this_p);
2137  }
2138  }
2139 
2140  code_function_callt call;
2141  location.set_function(method_id);
2142 
2143  call.add_source_location() = location;
2144  call.arguments() = pop(parameters.size());
2145 
2146  // double-check a bit
2147  if(use_this)
2148  {
2149  const exprt &this_arg = call.arguments().front();
2150  INVARIANT(
2151  this_arg.type().id() == ID_pointer, "first argument must be a pointer");
2152  }
2153 
2154  // do some type adjustment for the arguments,
2155  // as Java promotes arguments
2156  // Also cast pointers since intermediate locals
2157  // can be void*.
2158 
2159  for(std::size_t i = 0; i < parameters.size(); i++)
2160  {
2161  const typet &type = parameters[i].type();
2162  if(
2163  type == java_boolean_type() || type == java_char_type() ||
2164  type == java_byte_type() || type == java_short_type() ||
2165  type.id() == ID_pointer)
2166  {
2167  assert(i < call.arguments().size());
2168  if(type != call.arguments()[i].type())
2169  call.arguments()[i].make_typecast(type);
2170  }
2171  }
2172 
2173  // do some type adjustment for return values
2174 
2175  const typet &return_type = method_type.return_type();
2176 
2177  if(return_type.id() != ID_empty)
2178  {
2179  // return types are promoted in Java
2180  call.lhs() = tmp_variable("return", return_type);
2181  exprt promoted = java_bytecode_promotion(call.lhs());
2182  results.resize(1);
2183  results[0] = promoted;
2184  }
2185 
2186  assert(arg0.id() == ID_virtual_function);
2187 
2188  // If we don't have a definition for the called symbol, and we won't
2189  // inherit a definition from a super-class, we create a new symbol and
2190  // insert it in the symbol table. The name and type of the method are
2191  // derived from the information we have in the call.
2192  // We fix the access attribute to ID_public, because of the following
2193  // reasons:
2194  // - We don't know the orignal access attribute and since the .class file
2195  // unavailable, we have no way to know.
2196  // - Whatever it was, we assume that the bytecode we are translating
2197  // compiles correctly, so such a method has to be accessible from this
2198  // method.
2199  // - We will never generate code that calls that method unless we
2200  // translate bytecode that calls that method. As a result we will never
2201  // generate code that may wrongly assume that such a method is
2202  // accessible if we assume that its access attribute is "more
2203  // accessible" than it actually is.
2204  irep_idt id = arg0.get(ID_identifier);
2205  if(
2206  symbol_table.symbols.find(id) == symbol_table.symbols.end() &&
2207  !(is_virtual &&
2208  is_method_inherited(arg0.get(ID_C_class), arg0.get(ID_component_name))))
2209  {
2210  symbolt symbol;
2211  symbol.name = id;
2212  symbol.base_name = arg0.get(ID_C_base_name);
2213  symbol.pretty_name = id2string(arg0.get(ID_C_class)).substr(6) + "." +
2214  id2string(symbol.base_name) + "()";
2215  symbol.type = arg0.type();
2216  symbol.type.set(ID_access, ID_public);
2217  symbol.value.make_nil();
2218  symbol.mode = ID_java;
2220  to_java_method_type(symbol.type), symbol.name, symbol_table);
2221 
2222  debug() << "Generating codet: new opaque symbol: method '" << symbol.name
2223  << "'" << eom;
2224  symbol_table.add(symbol);
2225  }
2226 
2227  if(is_virtual)
2228  {
2229  // dynamic binding
2230  assert(use_this);
2231  assert(!call.arguments().empty());
2232  call.function() = arg0;
2233  // Populate needed methods later,
2234  // once we know what object types can exist.
2235  }
2236  else
2237  {
2238  // static binding
2239  call.function() = symbol_exprt(arg0.get(ID_identifier), arg0.type());
2241  {
2242  needed_lazy_methods->add_needed_method(arg0.get(ID_identifier));
2243  // Calling a static method causes static initialization:
2244  needed_lazy_methods->add_needed_class(arg0.get(ID_C_class));
2245  }
2246  }
2247 
2248  call.function().add_source_location() = location;
2249 
2250  // Replacing call if it is a function of the Character library,
2251  // returning the same call otherwise
2253 
2254  if(!use_this)
2255  {
2256  codet clinit_call = get_clinit_call(arg0.get(ID_C_class));
2257  if(clinit_call.get_statement() != ID_skip)
2258  {
2259  code_blockt ret_block;
2260  ret_block.move_to_operands(clinit_call);
2261  ret_block.move_to_operands(c);
2262  c = std::move(ret_block);
2263  }
2264  }
2265 }
2266 
2268  source_locationt location,
2269  codet &c)
2270 {
2271  exprt operand = pop(1)[0];
2272  // we may need to adjust the type of the argument
2273  if(operand.type() != bool_typet())
2274  operand.make_typecast(bool_typet());
2275 
2276  c = code_assumet(operand);
2277  location.set_function(method_id);
2278  c.add_source_location() = location;
2279  return c;
2280 }
2281 
2283  const exprt &arg0,
2284  const exprt::operandst &op,
2285  codet &c,
2286  exprt::operandst &results) const
2287 {
2288  binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
2289  code_assertt assert_class(check);
2290  assert_class.add_source_location().set_comment("Dynamic cast check");
2291  assert_class.add_source_location().set_property_class("bad-dynamic-cast");
2292  // we add this assert such that we can recognise it
2293  // during the instrumentation phase
2294  c = std::move(assert_class);
2295  results[0] = op[0];
2296 }
2297 
2299  const source_locationt &location,
2300  const exprt::operandst &op,
2301  codet &c,
2302  exprt::operandst &results) const
2303 {
2304  if(
2307  "java::java.lang.AssertionError")
2308  {
2309  // we translate athrow into
2310  // ASSERT false;
2311  // ASSUME false:
2312  code_assertt assert_code;
2313  assert_code.assertion() = false_exprt();
2314  source_locationt assert_location = location; // copy
2315  assert_location.set_comment("assertion at " + location.as_string());
2316  assert_location.set("user-provided", true);
2317  assert_location.set_property_class(ID_assertion);
2318  assert_code.add_source_location() = assert_location;
2319 
2320  code_assumet assume_code;
2321  assume_code.assumption() = false_exprt();
2322  source_locationt assume_location = location; // copy
2323  assume_location.set("user-provided", true);
2324  assume_code.add_source_location() = assume_location;
2325 
2326  code_blockt ret_block;
2327  ret_block.move_to_operands(assert_code);
2328  ret_block.move_to_operands(assume_code);
2329  c = ret_block;
2330  }
2331  else
2332  {
2333  side_effect_expr_throwt throw_expr(irept(), typet(), location);
2334  throw_expr.copy_to_operands(op[0]);
2335  c = code_expressiont(throw_expr);
2336  }
2337  results[0] = op[0];
2338 }
2339 
2342  const std::set<unsigned int> &working_set,
2343  unsigned int cur_pc,
2344  codet &c)
2345 {
2346  std::vector<irep_idt> exception_ids;
2347  std::vector<irep_idt> handler_labels;
2348 
2349  // for each try-catch add a CATCH-PUSH instruction
2350  // each CATCH-PUSH records a list of all the handler labels
2351  // together with a list of all the exception ids
2352 
2353  // be aware of different try-catch blocks with the same starting pc
2354  std::size_t pos = 0;
2355  std::size_t end_pc = 0;
2356  while(pos < method.exception_table.size())
2357  {
2358  // check if this is the beginning of a try block
2359  for(; pos < method.exception_table.size(); ++pos)
2360  {
2361  // unexplored try-catch?
2362  if(cur_pc == method.exception_table[pos].start_pc && end_pc == 0)
2363  {
2364  end_pc = method.exception_table[pos].end_pc;
2365  }
2366 
2367  // currently explored try-catch?
2368  if(
2369  cur_pc == method.exception_table[pos].start_pc &&
2370  method.exception_table[pos].end_pc == end_pc)
2371  {
2372  exception_ids.push_back(
2373  method.exception_table[pos].catch_type.get_identifier());
2374  // record the exception handler in the CATCH-PUSH
2375  // instruction by generating a label corresponding to
2376  // the handler's pc
2377  handler_labels.push_back(
2378  label(std::to_string(method.exception_table[pos].handler_pc)));
2379  }
2380  else
2381  break;
2382  }
2383 
2384  // add the actual PUSH-CATCH instruction
2385  if(!exception_ids.empty())
2386  {
2387  code_push_catcht catch_push;
2388  INVARIANT(
2389  exception_ids.size() == handler_labels.size(),
2390  "Exception tags and handler labels should be 1-to-1");
2391  code_push_catcht::exception_listt &exception_list =
2392  catch_push.exception_list();
2393  for(size_t i = 0; i < exception_ids.size(); ++i)
2394  {
2395  exception_list.push_back(
2397  exception_ids[i], handler_labels[i]));
2398  }
2399 
2400  code_blockt try_block;
2401  try_block.move_to_operands(catch_push);
2402  try_block.move_to_operands(c);
2403  c = try_block;
2404  }
2405  else
2406  {
2407  // advance
2408  ++pos;
2409  }
2410 
2411  // reset
2412  end_pc = 0;
2413  exception_ids.clear();
2414  handler_labels.clear();
2415  }
2416 
2417  // next add the CATCH-POP instructions
2418  size_t start_pc = 0;
2419  // as the first try block may have start_pc 0, we
2420  // must track it separately
2421  bool first_handler = false;
2422  // check if this is the end of a try block
2423  for(const auto &exception_row : method.exception_table)
2424  {
2425  // add the CATCH-POP before the end of the try block
2426  if(
2427  cur_pc < exception_row.end_pc && !working_set.empty() &&
2428  *working_set.begin() == exception_row.end_pc)
2429  {
2430  // have we already added a CATCH-POP for the current try-catch?
2431  // (each row corresponds to a handler)
2432  if(exception_row.start_pc != start_pc || !first_handler)
2433  {
2434  if(!first_handler)
2435  first_handler = true;
2436  // remember the beginning of the try-catch so that we don't add
2437  // another CATCH-POP for the same try-catch
2438  start_pc = exception_row.start_pc;
2439  // add CATCH_POP instruction
2440  code_pop_catcht catch_pop;
2441  code_blockt end_try_block;
2442  end_try_block.move_to_operands(c);
2443  end_try_block.move_to_operands(catch_pop);
2444  c = end_try_block;
2445  }
2446  }
2447  }
2448  return c;
2449 }
2450 
2452  const source_locationt &location,
2453  const exprt &arg0,
2454  const exprt::operandst &op,
2455  codet &c,
2456  exprt::operandst &results)
2457 {
2458  PRECONDITION(!location.get_line().empty());
2459  const reference_typet ref_type = java_reference_type(arg0.type());
2460  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
2461  java_new_array.operands() = op;
2462 
2463  code_blockt create;
2464 
2465  if(max_array_length != 0)
2466  {
2468  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2469  code_assumet assume_le_max_size(le_max_size);
2470  create.move_to_operands(assume_le_max_size);
2471  }
2472 
2473  const exprt tmp = tmp_variable("newarray", ref_type);
2474  create.copy_to_operands(code_assignt(tmp, java_new_array));
2475  c = std::move(create);
2476  results[0] = tmp;
2477 }
2478 
2480  const source_locationt &location,
2481  const irep_idt &statement,
2482  const exprt &arg0,
2483  const exprt::operandst &op,
2484  codet &c,
2485  exprt::operandst &results)
2486 {
2487  char element_type;
2488 
2489  if(statement == "newarray")
2490  {
2491  irep_idt id = arg0.type().id();
2492 
2493  if(id == ID_bool)
2494  element_type = 'z';
2495  else if(id == ID_char)
2496  element_type = 'c';
2497  else if(id == ID_float)
2498  element_type = 'f';
2499  else if(id == ID_double)
2500  element_type = 'd';
2501  else if(id == ID_byte)
2502  element_type = 'b';
2503  else if(id == ID_short)
2504  element_type = 's';
2505  else if(id == ID_int)
2506  element_type = 'i';
2507  else if(id == ID_long)
2508  element_type = 'j';
2509  else
2510  element_type = '?';
2511  }
2512  else
2513  element_type = 'a';
2514 
2515  const reference_typet ref_type = java_array_type(element_type);
2516 
2517  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
2518  java_new_array.copy_to_operands(op[0]);
2519 
2520  c = code_blockt();
2521 
2522  if(max_array_length != 0)
2523  {
2525  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
2526  code_assumet assume_le_max_size(le_max_size);
2527  c.move_to_operands(assume_le_max_size);
2528  }
2529  const exprt tmp = tmp_variable("newarray", ref_type);
2530  c.copy_to_operands(code_assignt(tmp, java_new_array));
2531  results[0] = tmp;
2532 }
2533 
2535  const source_locationt &location,
2536  const exprt &arg0,
2537  codet &c,
2538  exprt::operandst &results)
2539 {
2540  const reference_typet ref_type = java_reference_type(arg0.type());
2541  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
2542 
2543  if(!location.get_line().empty())
2544  java_new_expr.add_source_location() = location;
2545 
2546  const exprt tmp = tmp_variable("new", ref_type);
2547  c = code_assignt(tmp, java_new_expr);
2548  c.add_source_location() = location;
2549  codet clinit_call =
2550  get_clinit_call(to_symbol_type(arg0.type()).get_identifier());
2551  if(clinit_call.get_statement() != ID_skip)
2552  {
2553  code_blockt ret_block;
2554  ret_block.move_to_operands(clinit_call);
2555  ret_block.move_to_operands(c);
2556  c = std::move(ret_block);
2557  }
2558  results[0] = tmp;
2559 }
2560 
2562  const source_locationt &location,
2563  const exprt &arg0,
2564  const exprt::operandst &op,
2565  const symbol_exprt &symbol_expr)
2566 {
2567  if(needed_lazy_methods && arg0.type().id() == ID_symbol)
2568  {
2569  needed_lazy_methods->add_needed_class(
2570  to_symbol_type(arg0.type()).get_identifier());
2571  }
2572 
2573  code_blockt block;
2574  block.add_source_location() = location;
2575 
2576  // Note this initializer call deliberately inits the class used to make
2577  // the reference, which may be a child of the class that actually defines
2578  // the field.
2579  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2580  if(clinit_call.get_statement() != ID_skip)
2581  block.move_to_operands(clinit_call);
2582 
2584  "stack_static_field",
2585  symbol_expr.type(),
2586  block,
2588  symbol_expr.get_identifier());
2589  block.copy_to_operands(code_assignt(symbol_expr, op[0]));
2590  return block;
2591 }
2592 
2594  const exprt &arg0,
2595  const exprt::operandst &op)
2596 {
2597  code_blockt block;
2599  "stack_field",
2600  op[1].type(),
2601  block,
2603  arg0.get(ID_component_name));
2604  block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
2605  return block;
2606 }
2607 
2609  const exprt &arg0,
2610  const symbol_exprt &symbol_expr,
2611  const bool is_assertions_disabled_field,
2612  codet &c,
2613  exprt::operandst &results)
2614 {
2616  {
2617  if(arg0.type().id() == ID_symbol)
2618  {
2619  needed_lazy_methods->add_needed_class(
2620  to_symbol_type(arg0.type()).get_identifier());
2621  }
2622  else if(arg0.type().id() == ID_pointer)
2623  {
2624  const auto &pointer_type = to_pointer_type(arg0.type());
2625  if(pointer_type.subtype().id() == ID_symbol)
2626  {
2627  needed_lazy_methods->add_needed_class(
2628  to_symbol_type(pointer_type.subtype()).get_identifier());
2629  }
2630  }
2631  else if(is_assertions_disabled_field)
2632  {
2633  needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
2634  }
2635  }
2636  results[0] = java_bytecode_promotion(symbol_expr);
2637 
2638  // Note this initializer call deliberately inits the class used to make
2639  // the reference, which may be a child of the class that actually defines
2640  // the field.
2641  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
2642  if(clinit_call.get_statement() != ID_skip)
2643  c = clinit_call;
2644  else if(is_assertions_disabled_field)
2645  {
2646  // set $assertionDisabled to false
2647  c = code_assignt(symbol_expr, false_exprt());
2648  }
2649 }
2650 
2652  const irep_idt &statement,
2653  const exprt::operandst &op,
2654  exprt::operandst &results) const
2655 {
2656  const int nan_value(statement[4] == 'l' ? -1 : 1);
2657  const typet result_type(java_int_type());
2658  const exprt nan_result(from_integer(nan_value, result_type));
2659 
2660  // (value1 == NaN || value2 == NaN) ?
2661  // nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0;
2662  // (value1 == NaN || value2 == NaN) ?
2663  // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0;
2664 
2665  isnan_exprt nan_op0(op[0]);
2666  isnan_exprt nan_op1(op[1]);
2667  exprt one = from_integer(1, result_type);
2668  exprt minus_one = from_integer(-1, result_type);
2669  results[0] = if_exprt(
2670  or_exprt(nan_op0, nan_op1),
2671  nan_result,
2672  if_exprt(
2673  ieee_float_equal_exprt(op[0], op[1]),
2674  from_integer(0, result_type),
2675  if_exprt(binary_relation_exprt(op[0], ID_lt, op[1]), minus_one, one)));
2676  return results;
2677 }
2678 
2680  const exprt::operandst &op,
2681  exprt::operandst &results) const
2682 { // The integer result on the stack is:
2683  // 0 if op[0] equals op[1]
2684  // -1 if op[0] is less than op[1]
2685  // 1 if op[0] is greater than op[1]
2686 
2687  const typet t = java_int_type();
2688  exprt one = from_integer(1, t);
2689  exprt minus_one = from_integer(-1, t);
2690 
2691  if_exprt greater =
2692  if_exprt(binary_relation_exprt(op[0], ID_gt, op[1]), one, minus_one);
2693 
2694  results[0] = if_exprt(
2695  binary_relation_exprt(op[0], ID_equal, op[1]), from_integer(0, t), greater);
2696  return results;
2697 }
2698 
2700  const irep_idt &statement,
2701  const exprt::operandst &op,
2702  exprt::operandst &results) const
2703 {
2704  const typet type = java_type_from_char(statement[0]);
2705 
2706  const std::size_t width = type.get_size_t(ID_width);
2707  typet target = unsignedbv_typet(width);
2708 
2709  exprt lhs = op[0];
2710  if(lhs.type() != target)
2711  lhs.make_typecast(target);
2712  exprt rhs = op[1];
2713  if(rhs.type() != target)
2714  rhs.make_typecast(target);
2715 
2716  results[0] = lshr_exprt(lhs, rhs);
2717  if(results[0].type() != op[0].type())
2718  results[0].make_typecast(op[0].type());
2719  return results;
2720 }
2721 
2723  const exprt &arg0,
2724  const exprt &arg1,
2725  const source_locationt &location,
2726  const unsigned address)
2727 {
2728  code_blockt block;
2729  block.add_source_location() = location;
2730  // search variable on stack
2731  const exprt &locvar = variable(arg0, 'i', address, NO_CAST);
2733  "stack_iinc",
2734  java_int_type(),
2735  block,
2737  to_symbol_expr(locvar).get_identifier());
2738 
2739  code_assignt code_assign;
2740  code_assign.lhs() = variable(arg0, 'i', address, NO_CAST);
2741  exprt arg1_int_type = arg1;
2742  if(arg1.type() != java_int_type())
2743  arg1_int_type.make_typecast(java_int_type());
2744  code_assign.rhs() =
2745  plus_exprt(variable(arg0, 'i', address, CAST_AS_NEEDED), arg1_int_type);
2746  block.copy_to_operands(code_assign);
2747  return block;
2748 }
2749 
2752  const exprt::operandst &op,
2753  const mp_integer &number,
2754  const source_locationt &location) const
2755 {
2756  code_ifthenelset code_branch;
2757  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
2758  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2759  code_branch.cond() = binary_relation_exprt(lhs, ID_equal, rhs);
2760  code_branch.then_case() = code_gotot(label(integer2string(number)));
2761  code_branch.then_case().add_source_location() =
2762  address_map.at(integer2unsigned(number)).source->source_location;
2763  code_branch.add_source_location() = location;
2764  return code_branch;
2765 }
2766 
2769  const exprt::operandst &op,
2770  const mp_integer &number,
2771  const source_locationt &location) const
2772 {
2773  code_ifthenelset code_branch;
2774  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
2775  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
2776  code_branch.cond() = binary_relation_exprt(lhs, ID_notequal, rhs);
2777  code_branch.then_case() = code_gotot(label(integer2string(number)));
2778  code_branch.then_case().add_source_location() =
2779  address_map.at(integer2unsigned(number)).source->source_location;
2780  code_branch.add_source_location() = location;
2781  return code_branch;
2782 }
2783 
2786  const exprt::operandst &op,
2787  const irep_idt &id,
2788  const mp_integer &number,
2789  const source_locationt &location) const
2790 {
2791  code_ifthenelset code_branch;
2792  code_branch.cond() =
2793  binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
2794  code_branch.cond().add_source_location() = location;
2796  code_branch.then_case() = code_gotot(label(integer2string(number)));
2797  code_branch.then_case().add_source_location() =
2798  address_map.at(integer2unsigned(number)).source->source_location;
2800  code_branch.add_source_location() = location;
2802  return code_branch;
2803 }
2804 
2807  const irep_idt &statement,
2808  const exprt::operandst &op,
2809  const mp_integer &number,
2810  const source_locationt &location) const
2811 {
2812  code_ifthenelset code_branch;
2813  const irep_idt cmp_op = get_if_cmp_operator(statement);
2814 
2815  binary_relation_exprt condition(op[0], cmp_op, op[1]);
2816 
2817  exprt &lhs(condition.lhs());
2818  exprt &rhs(condition.rhs());
2819  const typet &lhs_type(lhs.type());
2820  if(lhs_type != rhs.type())
2821  rhs = typecast_exprt(rhs, lhs_type);
2822 
2823  code_branch.cond() = condition;
2824  code_branch.cond().add_source_location() = location;
2825  code_branch.then_case() = code_gotot(label(integer2string(number)));
2826  code_branch.then_case().add_source_location() =
2827  address_map.at(integer2unsigned(number)).source->source_location;
2828  code_branch.add_source_location() = location;
2829 
2830  return code_branch;
2831 }
2832 
2834  const std::vector<unsigned int> &jsr_ret_targets,
2835  const exprt &arg0,
2836  const source_locationt &location,
2837  const unsigned address)
2838 {
2839  code_blockt c;
2840  auto retvar = variable(arg0, 'a', address, NO_CAST);
2841  for(size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2842  {
2843  irep_idt number = std::to_string(jsr_ret_targets[idx]);
2844  code_gotot g(label(number));
2845  g.add_source_location() = location;
2846  if(idx == idxlim - 1)
2847  c.move_to_operands(g);
2848  else
2849  {
2851  auto address_ptr =
2852  from_integer(jsr_ret_targets[idx], unsignedbv_typet(64));
2853  address_ptr.type() = pointer_type(void_typet());
2854  branch.cond() = equal_exprt(retvar, address_ptr);
2855  branch.cond().add_source_location() = location;
2856  branch.then_case() = g;
2857  branch.add_source_location() = location;
2859  }
2860  }
2861  return c;
2862 }
2863 
2865  const irep_idt &statement,
2866  const exprt::operandst &op) const
2867 {
2868  const char &type_char = statement[0];
2869  const typecast_exprt pointer(op[0], java_array_type(type_char));
2870 
2871  dereference_exprt deref(pointer, pointer.type().subtype());
2872  deref.set(ID_java_member_access, true);
2873 
2874  const member_exprt data_ptr(
2875  deref, "data", pointer_type(java_type_from_char(type_char)));
2876 
2877  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
2878  // tag it so it's easy to identify during instrumentation
2879  data_plus_offset.set(ID_java_array_access, true);
2880  const typet &element_type = data_ptr.type().subtype();
2881  const dereference_exprt element(data_plus_offset, element_type);
2882  return java_bytecode_promotion(element);
2883 }
2884 
2886  const irep_idt &statement,
2887  const exprt &arg0,
2888  const exprt::operandst &op,
2889  const unsigned address,
2890  const source_locationt &location)
2891 {
2892  const exprt var = variable(arg0, statement[0], address, NO_CAST);
2893  const irep_idt &var_name = to_symbol_expr(var).get_identifier();
2894 
2895  exprt toassign = op[0];
2896  if('a' == statement[0] && toassign.type() != var.type())
2897  toassign = typecast_exprt(toassign, var.type());
2898 
2899  code_blockt block;
2900 
2902  "stack_store",
2903  toassign.type(),
2904  block,
2906  var_name);
2907  code_assignt assign(var, toassign);
2908  assign.add_source_location() = location;
2909  block.move(assign);
2910  return block;
2911 }
2912 
2914  const irep_idt &statement,
2915  const exprt::operandst &op,
2916  const source_locationt &location)
2917 {
2918  const char type_char = statement[0];
2919  const typecast_exprt pointer(op[0], java_array_type(type_char));
2920 
2921  dereference_exprt deref(pointer, pointer.type().subtype());
2922  deref.set(ID_java_member_access, true);
2923 
2924  const member_exprt data_ptr(
2925  deref, "data", pointer_type(java_type_from_char(type_char)));
2926 
2927  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
2928  // tag it so it's easy to identify during instrumentation
2929  data_plus_offset.set(ID_java_array_access, true);
2930  const typet &element_type = data_ptr.type().subtype();
2931  const dereference_exprt element(data_plus_offset, element_type);
2932 
2933  code_blockt block;
2934  block.add_source_location() = location;
2935 
2937  "stack_astore", element_type, block, bytecode_write_typet::ARRAY_REF, "");
2938 
2939  code_assignt array_put(element, op[2]);
2940  array_put.add_source_location() = location;
2941  block.move(array_put);
2942  return block;
2943 }
2944 
2946  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
2947  const source_locationt &location,
2948  const exprt &arg0)
2949 {
2950  const java_method_typet &method_type = to_java_method_type(arg0.type());
2951 
2952  const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
2953  lambda_method_handles,
2954  method_type.get_int(ID_java_lambda_method_handle_index));
2955  if(lambda_method_symbol.has_value())
2956  debug() << "Converting invokedynamic for lambda: "
2957  << lambda_method_symbol.value().name << eom;
2958  else
2959  debug() << "Converting invokedynamic for lambda with unknown handle "
2960  "type"
2961  << eom;
2962 
2963  const java_method_typet::parameterst &parameters(method_type.parameters());
2964 
2965  pop(parameters.size());
2966 
2967  const typet &return_type = method_type.return_type();
2968 
2969  if(return_type.id() == ID_empty)
2970  return {};
2971 
2972  return zero_initializer(
2973  return_type, location, namespacet(symbol_table), get_message_handler());
2974 }
2975 
2978  const std::vector<unsigned int> &jsr_ret_targets,
2979  const std::vector<
2980  std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2981  &ret_instructions) const
2982 { // Draw edges from every `ret` to every `jsr` successor. Could do better with
2983  // flow analysis to distinguish multiple subroutines within the same function.
2984  for(const auto &retinst : ret_instructions)
2985  {
2986  auto &a_entry = address_map.at(retinst->address);
2987  a_entry.successors.insert(
2988  a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
2989  }
2990 }
2991 
2993  const unsigned int address,
2995  const
2996 {
2997  std::vector<unsigned> result;
2998  for(const auto &exception_row : exception_table)
2999  {
3000  if(address >= exception_row.start_pc && address < exception_row.end_pc)
3001  result.push_back(exception_row.handler_pc);
3002  }
3003  return result;
3004 }
3005 
3019  symbolt &method_symbol,
3021  &local_variable_table,
3022  symbol_table_baset &symbol_table)
3023 {
3024  // Obtain a std::vector of java_method_typet::parametert objects from the
3025  // (function) type of the symbol
3026  java_method_typet &method_type = to_java_method_type(method_symbol.type);
3027  java_method_typet::parameterst &parameters = method_type.parameters();
3028 
3029  // Find number of parameters
3030  unsigned slots_for_parameters = java_method_parameter_slots(method_type);
3031 
3032  // Find parameter names in the local variable table:
3033  typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3034  std::map<std::size_t, base_name_and_identifiert> param_names;
3035  for(const auto &v : local_variable_table)
3036  {
3037  if(v.index < slots_for_parameters)
3038  param_names.emplace(
3039  v.index,
3040  make_pair(
3041  v.name, id2string(method_symbol.name) + "::" + id2string(v.name)));
3042  }
3043 
3044  // Assign names to parameters
3045  std::size_t param_index = 0;
3046  for(auto &param : parameters)
3047  {
3048  irep_idt base_name, identifier;
3049 
3050  // Construct a sensible base name (base_name) and a fully qualified name
3051  // (identifier) for every parameter of the method under translation,
3052  // regardless of whether we have an LVT or not; and assign it to the
3053  // parameter object (which is stored in the type of the symbol, not in the
3054  // symbol table)
3055  if(param_index == 0 && param.get_this())
3056  {
3057  // my.package.ClassName.myMethodName:(II)I::this
3058  base_name = "this";
3059  identifier = id2string(method_symbol.name) + "::" + id2string(base_name);
3060  }
3061  else
3062  {
3063  auto param_name = param_names.find(param_index);
3064  if(param_name != param_names.end())
3065  {
3066  base_name = param_name->second.first;
3067  identifier = param_name->second.second;
3068  }
3069  else
3070  {
3071  // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local
3072  // variable slot where the parameter is stored and T is a character
3073  // indicating the type
3074  const typet &type = param.type();
3075  char suffix = java_char_from_type(type);
3076  base_name = "arg" + std::to_string(param_index) + suffix;
3077  identifier =
3078  id2string(method_symbol.name) + "::" + id2string(base_name);
3079  }
3080  }
3081  param.set_base_name(base_name);
3082  param.set_identifier(identifier);
3083 
3084  // Build a new symbol for the parameter and add it to the symbol table
3085  parameter_symbolt parameter_symbol;
3086  parameter_symbol.base_name = base_name;
3087  parameter_symbol.mode = ID_java;
3088  parameter_symbol.name = identifier;
3089  parameter_symbol.type = param.type();
3090  symbol_table.insert(parameter_symbol);
3091 
3092  param_index += java_local_variable_slots(param.type());
3093  }
3094 }
3095 
3097  const symbolt &class_symbol,
3098  const java_bytecode_parse_treet::methodt &method,
3099  symbol_table_baset &symbol_table,
3101  size_t max_array_length,
3102  bool throw_assertion_error,
3103  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
3104  java_string_library_preprocesst &string_preprocess,
3105  const class_hierarchyt &class_hierarchy,
3106  bool threading_support)
3107 
3108 {
3109  if(std::regex_match(
3110  id2string(class_symbol.name),
3111  std::regex(".*org\\.cprover\\.CProver.*")) &&
3112  cprover_methods_to_ignore.count(id2string(method.name)))
3113  {
3114  // Ignore these methods; fall back to the driver program's
3115  // stubbing behaviour.
3116  return;
3117  }
3118 
3120  symbol_table,
3122  max_array_length,
3123  throw_assertion_error,
3124  needed_lazy_methods,
3125  string_preprocess,
3126  class_hierarchy,
3127  threading_support);
3128 
3129  java_bytecode_convert_method(class_symbol, method);
3130 }
3131 
3138  const irep_idt &classname,
3139  const irep_idt &methodid) const
3140 {
3143  classname,
3144  methodid,
3145  symbol_table,
3147  false);
3148  return inherited_method.is_valid();
3149 }
3150 
3157  const irep_idt &class_identifier,
3158  const irep_idt &component_name) const
3159 {
3162  class_identifier,
3163  component_name,
3164  symbol_table,
3166  true);
3167 
3168  INVARIANT(
3169  inherited_method.is_valid(), "static field should be in symbol table");
3170 
3171  return inherited_method.get_full_component_identifier();
3172 }
3173 
3182  const std::string &tmp_var_prefix,
3183  const typet &tmp_var_type,
3184  code_blockt &block,
3185  const bytecode_write_typet write_type,
3186  const irep_idt &identifier)
3187 {
3188  const std::function<bool(
3189  const std::function<tvt(const exprt &expr)>, const exprt &expr)>
3190  entry_matches = [&entry_matches](
3191  const std::function<tvt(const exprt &expr)> predicate,
3192  const exprt &expr) {
3193  const tvt &tvres = predicate(expr);
3194  if(tvres.is_unknown())
3195  {
3196  return std::any_of(
3197  expr.operands().begin(),
3198  expr.operands().end(),
3199  [&predicate, &entry_matches](const exprt &expr) {
3200  return entry_matches(predicate, expr);
3201  });
3202  }
3203  else
3204  {
3205  return tvres.is_true();
3206  }
3207  };
3208 
3209  // Function that checks whether the expression accesses a member with the
3210  // given identifier name. These accesses are created in the case of `iinc`, or
3211  // non-array `?store` instructions.
3212  const std::function<tvt(const exprt &expr)> has_member_entry = [&identifier](
3213  const exprt &expr) {
3214  const auto member_expr = expr_try_dynamic_cast<member_exprt>(expr);
3215  return !member_expr ? tvt::unknown()
3216  : tvt(member_expr->get_component_name() == identifier);
3217  };
3218 
3219  // Function that checks whether the expression is a symbol with the given
3220  // identifier name. These accesses are created in the case of `putstatic` or
3221  // `putfield` instructions.
3222  const std::function<tvt(const exprt &expr)> is_symbol_entry =
3223  [&identifier](const exprt &expr) {
3224  const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
3225  return !symbol_expr ? tvt::unknown()
3226  : tvt(symbol_expr->get_identifier() == identifier);
3227  };
3228 
3229  // Function that checks whether the expression is a dereference
3230  // expression. These accesses are created in `?astore` array write
3231  // instructions.
3232  const std::function<tvt(const exprt &expr)> is_dereference_entry =
3233  [](const exprt &expr) {
3234  const auto dereference_expr =
3236  return !dereference_expr ? tvt::unknown() : tvt(true);
3237  };
3238 
3239  for(auto &stack_entry : stack)
3240  {
3241  bool replace = false;
3242  switch(write_type)
3243  {
3246  replace = entry_matches(is_symbol_entry, stack_entry);
3247  break;
3249  replace = entry_matches(is_dereference_entry, stack_entry);
3250  break;
3252  replace = entry_matches(has_member_entry, stack_entry);
3253  break;
3254  }
3255  if(replace)
3256  {
3257  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
3258  }
3259  }
3260 }
3261 
3264  const std::string &tmp_var_prefix,
3265  const typet &tmp_var_type,
3266  code_blockt &block,
3267  exprt &stack_entry)
3268 {
3269  const exprt tmp_var=
3270  tmp_variable(tmp_var_prefix, tmp_var_type);
3271  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
3272  stack_entry=tmp_var;
3273 }
The void type.
Definition: std_types.h:64
const irep_idt & get_statement() const
Definition: std_code.h:40
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
const codet & then_case() const
Definition: std_code.h:486
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1229
void set_function(const irep_idt &function)
void set_access(const irep_idt &access)
Definition: std_types.h:930
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1589
semantic type conversion
Definition: std_expr.h:2111
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 convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
A ‘switch’ instruction.
Definition: std_code.h:538
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert(const symbolt &class_symbol, const methodt &)
std::vector< parametert > parameterst
Definition: std_types.h:767
bool is_thread_local
Definition: symbol.h:67
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
codet convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< symbol_exprt > java_lambda_method_handlest
Definition: java_types.h:174
void set_label(const irep_idt &label)
Definition: std_code.h:1005
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:176
Remove function exceptional returns.
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Over-approximative uncaught exceptions analysis.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:161
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
boolean OR
Definition: std_expr.h:2391
typet java_boolean_type()
Definition: java_types.cpp:72
irep_idt method_id
Fully qualified name of the method under translation.
void set_property_class(const irep_idt &property_class)
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address ...
Control Flow Graph.
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
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...
static void gather_symbol_live_ranges(unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
const java_lambda_method_handlest & lambda_method_handles() const
Definition: java_types.h:176
irep_idt mode
Language mode.
Definition: symbol.h:52
const exprt & cond() const
Definition: std_code.h:476
codet & code()
Definition: std_code.h:1080
void from_expr(const constant_exprt &expr)
bool is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const
Returns true iff method methodid from class classname is a method inherited from a class (and not an ...
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address, const address_mapt &amap, bool allow_merge=true)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
void set_comment(const irep_idt &comment)
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
static irep_idt label(const irep_idt &address)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1544
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::string as_string() const
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.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
struct bytecode_infot const bytecode_info[]
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4518
literalt pos(literalt a)
Definition: literal.h:193
exprt value
Initial value of symbol.
Definition: symbol.h:37
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
The trinary if-then-else operator.
Definition: std_expr.h:3359
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
A ‘goto’ instruction.
Definition: std_code.h:803
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
An exception that is raised for unsupported class signature.
Definition: java_types.h:639
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1632
bool operator==(const irep_idt &what) const
codet convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address)
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::vector< unsigned int > try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
A constant literal expression.
Definition: std_expr.h:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
bool get_is_constructor() const
Definition: std_types.h:935
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
std::map< unsigned, converted_instructiont > address_mapt
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
codet convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
An expression statement.
Definition: std_code.h:1220
void set_default()
Definition: std_code.h:1065
A side effect that throws an exception.
Definition: std_code.h:1491
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const exprt & case_op() const
Definition: std_code.h:1070
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 & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
&#39;tree&#39; describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
Extract member of struct or union.
Definition: std_expr.h:3869
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:307
codet convert_putfield(const exprt &arg0, const exprt::operandst &op)
equality
Definition: std_expr.h:1354
irep_idt current_method
A copy of method_id :/.
Class Hierarchy.
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:94
void set_is_constructor()
Definition: std_types.h:940
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3986
Bit-wise OR.
Definition: std_expr.h:2583
typet java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof...
Definition: java_types.cpp:470
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
class code_blockt & make_block()
Definition: std_code.cpp:24
void add_throws_exceptions(irep_idt exception)
Definition: java_types.h:277
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
Given a string of the format &#39;?blah?&#39;, will return true when compared against a string that matches a...
argumentst & arguments()
Definition: std_code.h:890
const irep_idt & get_line() const
division (integer and real)
Definition: std_expr.h:1075
A reference into the symbol table.
Definition: std_types.h:110
A declaration of a local variable.
Definition: std_code.h:254
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:339
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:298
The NIL expression.
Definition: std_expr.h:4508
exprt & rhs()
Definition: std_code.h:214
The empty type.
Definition: std_types.h:54
codet & code()
Definition: std_code.h:1010
codet replace_character_call(code_function_callt call)
Operator to dereference a pointer.
Definition: std_expr.h:3282
void convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
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:189
nonstd::optional< T > optionalt
Definition: optional.h:35
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:837
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
codet convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location)
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
Left shift.
Definition: std_expr.h:2848
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)
A label for branch targets.
Definition: std_code.h:977
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
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)
Definition: java_types.cpp:977
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Base class for tree-like data structures with sharing.
Definition: irep.h:156
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
Definition: java_utils.cpp:425
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
typet java_byte_type()
Definition: java_types.cpp:52
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Definition: java_utils.cpp:29
size_t size() const
Definition: dstring.h:89
Logical right shift.
Definition: std_expr.h:2888
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:33
codet & find_last_statement()
Definition: std_code.h:131
codet get_clinit_call(const irep_idt &classname)
Each static access to classname should be prefixed with a check for necessary static init; this retur...
The unary minus expression.
Definition: std_expr.h:444
typet java_short_type()
Definition: java_types.cpp:47
const symbolst & symbols
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
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:4497
const codet & body() const
Definition: std_code.h:564
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:649
exprt::operandst pop(std::size_t n)
void java_bytecode_convert_method_lazy(const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler)
This creates a method symbol in the symtab, but doesn&#39;t actually perform method conversion just yet...
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
bool is_true() const
Definition: threeval.h:25
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
The reference type.
Definition: std_types.h:1492
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:404
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
const exprt & value() const
Definition: std_code.h:554
Bit-wise XOR.
Definition: std_expr.h:2644
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
message_handlert & get_message_handler()
Definition: message.h:153
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
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
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
mstreamt & result() const
Definition: message.h:312
const char * mnemonic
Definition: bytecode_info.h:46
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:104
exprt & function()
Definition: std_code.h:878
void convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
Base class for all expressions.
Definition: expr.h:42
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
Convert parsed annotations into the symbol table.
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void move(codet &code)
Definition: std_code.h:107
bool has_this() const
Definition: std_types.h:866
const exprt & assumption() const
Definition: std_code.h:371
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
Definition: expr.h:125
std::vector< local_variablet > local_variable_tablet
bool is_file_local
Definition: symbol.h:68
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
remainder of division
Definition: std_expr.h:1187
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
Create temporary variables if a write instruction can have undesired side- effects.
const std::string & get_string(const irep_namet &name) const
Definition: irep.h: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:508
void swap(irept &irep)
Definition: irep.h:303
void push(const exprt::operandst &o)
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
binary minus
Definition: std_expr.h:959
codet & do_exception_handling(const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c)
Skip.
Definition: std_code.h:179
An if-then-else.
Definition: std_code.h:466
Bit-wise AND.
Definition: std_expr.h:2704
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:208
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
A switch-case.
Definition: std_code.h:1045
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:32
mstreamt & debug() const
Definition: message.h:332
A statement in a programming language.
Definition: std_code.h:21
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
Return from a function.
Definition: std_code.h:923
unsigned slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
Arithmetic right shift.
Definition: std_expr.h:2868
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
bool is_type
Definition: symbol.h:63
codet convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
typet java_char_type()
Definition: java_types.cpp:57
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1031
JAVA Bytecode Language Conversion.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
An expression containing a side effect.
Definition: std_code.h:1271
Compute dominators for CFG of goto_function.
codet convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
operandst & operands()
Definition: expr.h:66
void push_back(const T &t)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in &#39;repl&#39; that target &#39;old_label&#39; and redirect them to &#39;new_label&#39;.
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
exception_listt & exception_list()
Definition: std_code.h:1600
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:73
void convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
codet convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
irep_idt get_full_component_identifier() const
Get the full name of this function.
codet convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
const typet & return_type() const
Definition: std_types.h:895
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:227
binary modulo
Definition: std_expr.h:1133
Assignment.
Definition: std_code.h:196
char java_char_from_type(const typet &type)
Definition: java_types.cpp:611
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...
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1663
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91
void branch(goto_modelt &goto_model, const irep_idt &id)
Definition: branch.cpp:19
const exprt & assertion() const
Definition: std_code.h:418
Produce code for simple implementation of String Java libraries.
code_blockt convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address)
codet convert_instructions(const methodt &, const java_class_typet::java_lambda_method_handlest &)
IEEE-floating-point equality.
Definition: std_expr.h:4198
bool is_lvalue
Definition: symbol.h:68