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"
19 #include "java_types.h"
20 
21 #include <util/arith_tools.h>
22 #include <util/c_types.h>
23 #include <util/ieee_float.h>
24 #include <util/invariant.h>
25 #include <util/namespace.h>
26 #include <util/prefix.h>
27 #include <util/simplify_expr.h>
28 #include <util/std_expr.h>
29 #include <util/string2int.h>
30 
32 
33 #include <goto-programs/cfg.h>
35 
36 #include <limits>
37 #include <algorithm>
38 #include <functional>
39 #include <unordered_set>
40 
41 class patternt
42 {
43 public:
44  explicit patternt(const char *_p):p(_p)
45  {
46  }
47 
48  // match with '?'
49  bool operator==(const irep_idt &what) const
50  {
51  for(std::size_t i=0; i<what.size(); i++)
52  if(p[i]==0)
53  return false;
54  else if(p[i]!='?' && p[i]!=what[i])
55  return false;
56 
57  return p[what.size()]==0;
58  }
59 
60 protected:
61  const char *p;
62 };
63 
64 static bool operator==(const irep_idt &what, const patternt &pattern)
65 {
66  return pattern==what;
67 }
68 
69 const size_t SLOTS_PER_INTEGER(1u);
70 const size_t INTEGER_WIDTH(64u);
71 static size_t count_slots(
72  const size_t value,
73  const code_typet::parametert &param)
74 {
75  const std::size_t width(param.type().get_unsigned_int(ID_width));
76  return value+SLOTS_PER_INTEGER+width/INTEGER_WIDTH;
77 }
78 
79 static size_t get_variable_slots(const code_typet::parametert &param)
80 {
81  return count_slots(0, param);
82 }
83 
85 {
86  const auto to_strip_str=id2string(to_strip);
87  assert(has_prefix(to_strip_str, "java::"));
88  return to_strip_str.substr(6, std::string::npos);
89 }
90 
91 // name contains <init> or <clinit>
93  const class_typet::methodt &method)
94 {
95  const std::string &name(id2string(method.get_name()));
96  const std::string::size_type &npos(std::string::npos);
97  return npos!=name.find("<init>") || npos!=name.find("<clinit>");
98 }
99 
101 {
102  if(stack.size()<n)
103  {
104  error() << "malformed bytecode (pop too high)" << eom;
105  throw 0;
106  }
107 
108  exprt::operandst operands;
109  operands.resize(n);
110  for(std::size_t i=0; i<n; i++)
111  operands[i]=stack[stack.size()-n+i];
112 
113  stack.resize(stack.size()-n);
114  return operands;
115 }
116 
119 {
120  std::size_t residue_size=std::min(n, stack.size());
121 
122  stack.resize(stack.size()-residue_size);
123 }
124 
126 {
127  stack.resize(stack.size()+o.size());
128 
129  for(std::size_t i=0; i<o.size(); i++)
130  stack[stack.size()-o.size()+i]=o[i];
131 }
132 
133 // JVM program locations
135 {
136  return "pc"+id2string(address);
137 }
138 
140  const std::string &prefix,
141  const typet &type)
142 {
143  irep_idt base_name=prefix+"_tmp"+std::to_string(tmp_vars.size());
144  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
145 
146  auxiliary_symbolt tmp_symbol;
147  tmp_symbol.base_name=base_name;
148  tmp_symbol.is_static_lifetime=false;
149  tmp_symbol.mode=ID_java;
150  tmp_symbol.name=identifier;
151  tmp_symbol.type=type;
152  symbol_table.add(tmp_symbol);
153 
154  symbol_exprt result(identifier, type);
155  result.set(ID_C_base_name, base_name);
156  tmp_vars.push_back(result);
157 
158  return result;
159 }
160 
162  const exprt &arg,
163  char type_char,
164  size_t address,
166 {
167  mp_integer number;
168  bool ret=to_integer(to_constant_expr(arg), number);
169  CHECK_RETURN(!ret);
170 
171  std::size_t number_int=integer2size_t(number);
172  typet t=java_type_from_char(type_char);
173  variablest &var_list=variables[number_int];
174 
175  // search variable in list for correct frame / address if necessary
176  const variablet &var=
177  find_variable_for_slot(address, var_list);
178 
179  if(var.symbol_expr.get_identifier().empty())
180  {
181  // an unnamed local variable
182  irep_idt base_name="anonlocal::"+std::to_string(number_int)+type_char;
183  irep_idt identifier=id2string(current_method)+"::"+id2string(base_name);
184 
185  symbol_exprt result(identifier, t);
186  result.set(ID_C_base_name, base_name);
187  used_local_names.insert(result);
188  return result;
189  }
190  else
191  {
193  if(do_cast==CAST_AS_NEEDED && t!=result.type())
195  return result;
196  }
197 }
198 
208  const symbolt &class_symbol,
209  const irep_idt &method_identifier,
211  symbol_tablet &symbol_table)
212 {
213  symbolt method_symbol;
214  typet member_type=java_type_from_string(m.signature);
215 
216  method_symbol.name=method_identifier;
217  method_symbol.base_name=m.base_name;
218  method_symbol.mode=ID_java;
219  method_symbol.location=m.source_location;
220  method_symbol.location.set_function(method_identifier);
221  if(m.is_public)
222  member_type.set(ID_access, ID_public);
223  else if(m.is_protected)
224  member_type.set(ID_access, ID_protected);
225  else if(m.is_private)
226  member_type.set(ID_access, ID_private);
227  else
228  member_type.set(ID_access, ID_default);
229 
230  if(method_symbol.base_name=="<init>")
231  {
232  method_symbol.pretty_name=
233  id2string(class_symbol.pretty_name)+"."+
234  id2string(class_symbol.base_name)+"()";
235  member_type.set(ID_constructor, true);
236  }
237  else
238  method_symbol.pretty_name=
239  id2string(class_symbol.pretty_name)+"."+
240  id2string(m.base_name)+"()";
241 
242  // do we need to add 'this' as a parameter?
243  if(!m.is_static)
244  {
245  code_typet &code_type=to_code_type(member_type);
246  code_typet::parameterst &parameters=code_type.parameters();
247  code_typet::parametert this_p;
248  const reference_typet object_ref_type=
249  java_reference_type(symbol_typet(class_symbol.name));
250  this_p.type()=object_ref_type;
251  this_p.set_this();
252  parameters.insert(parameters.begin(), this_p);
253  }
254 
255  method_symbol.type=member_type;
256  symbol_table.add(method_symbol);
257 }
258 
260  const symbolt &class_symbol,
261  const methodt &m)
262 {
263  const irep_idt method_identifier=
264  id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
265  method_id=method_identifier;
266 
267  const auto &old_sym=symbol_table.lookup(method_identifier);
268 
269  typet member_type=old_sym.type;
270  code_typet &code_type=to_code_type(member_type);
271  method_return_type=code_type.return_type();
272  code_typet::parameterst &parameters=code_type.parameters();
273 
274  variables.clear();
275 
276  // find parameter names in the local variable table:
277  for(const auto &v : m.local_variable_table)
278  {
279  if(v.start_pc!=0) // Local?
280  continue;
281 
282  typet t=java_type_from_string(v.signature);
283  std::ostringstream id_oss;
284  id_oss << method_id << "::" << v.name;
285  irep_idt identifier(id_oss.str());
286  symbol_exprt result(identifier, t);
287  result.set(ID_C_base_name, v.name);
288 
289  variables[v.index].push_back(variablet());
290  auto &newv=variables[v.index].back();
291  newv.symbol_expr=result;
292  newv.start_pc=v.start_pc;
293  newv.length=v.length;
294  }
295 
296  // set up variables array
297  std::size_t param_index=0;
298  for(const auto &param : parameters)
299  {
300  variables[param_index].resize(1);
301  param_index+=get_variable_slots(param);
302  }
303 
304  // assign names to parameters
305  param_index=0;
306  for(auto &param : parameters)
307  {
308  irep_idt base_name, identifier;
309 
310  if(param_index==0 && param.get_this())
311  {
312  base_name="this";
313  identifier=id2string(method_identifier)+"::"+id2string(base_name);
314  param.set_base_name(base_name);
315  param.set_identifier(identifier);
316  }
317  else
318  {
319  // in the variable table?
320  base_name=variables[param_index][0].symbol_expr.get(ID_C_base_name);
321  identifier=variables[param_index][0].symbol_expr.get(ID_identifier);
322 
323  if(base_name.empty())
324  {
325  const typet &type=param.type();
326  char suffix=java_char_from_type(type);
327  base_name="arg"+std::to_string(param_index)+suffix;
328  identifier=id2string(method_identifier)+"::"+id2string(base_name);
329  }
330 
331  param.set_base_name(base_name);
332  param.set_identifier(identifier);
333  }
334 
335  // add to symbol table
336  parameter_symbolt parameter_symbol;
337  parameter_symbol.base_name=base_name;
338  parameter_symbol.mode=ID_java;
339  parameter_symbol.name=identifier;
340  parameter_symbol.type=param.type();
341  symbol_table.add(parameter_symbol);
342 
343  // add as a JVM variable
344  std::size_t slots=get_variable_slots(param);
345  variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
346  variables[param_index][0].is_parameter=true;
347  variables[param_index][0].start_pc=0;
348  variables[param_index][0].length=std::numeric_limits<size_t>::max();
349  variables[param_index][0].is_parameter=true;
350  param_index+=slots;
351  assert(param_index>0);
352  }
353 
354  const bool is_virtual=!m.is_static && !m.is_final;
355 
356  #if 0
357  class_type.methods().push_back(class_typet::methodt());
358  class_typet::methodt &method=class_type.methods().back();
359  #else
360  class_typet::methodt method;
361  #endif
362 
363  method.set_base_name(m.base_name);
364  method.set_name(method_identifier);
365 
366  method.set(ID_abstract, m.is_abstract);
367  method.set(ID_is_virtual, is_virtual);
368 
369  if(is_constructor(method))
370  method.set(ID_constructor, true);
371 
372  method.type()=member_type;
373 
374  // we add the symbol for the method
375 
376  symbolt method_symbol;
377 
378  method_symbol.name=method.get_name();
379  method_symbol.base_name=method.get_base_name();
380  method_symbol.mode=ID_java;
381  method_symbol.location=m.source_location;
382  method_symbol.location.set_function(method_identifier);
383 
384  if(method.get_base_name()=="<init>")
385  method_symbol.pretty_name=id2string(class_symbol.pretty_name)+"."+
386  id2string(class_symbol.base_name)+"()";
387  else
388  method_symbol.pretty_name=id2string(class_symbol.pretty_name)+"."+
389  id2string(method.get_base_name())+"()";
390 
391  method_symbol.type=member_type;
392  if(is_constructor(method))
393  method_symbol.type.set(ID_constructor, true);
394  current_method=method_symbol.name;
395  method_has_this=code_type.has_this();
396 
397  tmp_vars.clear();
398  if((!m.is_abstract) && (!m.is_native))
399  method_symbol.value=convert_instructions(m, code_type);
400 
401  // Replace the existing stub symbol with the real deal:
402  const auto s_it=symbol_table.symbols.find(method.get_name());
403  assert(s_it!=symbol_table.symbols.end());
404  symbol_table.symbols.erase(s_it);
405 
406  symbol_table.add(method_symbol);
407 }
408 
410  const irep_idt &statement)
411 {
412  for(const bytecode_infot *p=bytecode_info; p->mnemonic!=nullptr; p++)
413  if(statement==p->mnemonic)
414  return *p;
415 
416  error() << "failed to find bytecode mnemonic `"
417  << statement << '\'' << eom;
418  throw 0;
419 }
420 
422 {
423  if(stmt==patternt("if_?cmplt"))
424  return ID_lt;
425  if(stmt==patternt("if_?cmple"))
426  return ID_le;
427  if(stmt==patternt("if_?cmpgt"))
428  return ID_gt;
429  if(stmt==patternt("if_?cmpge"))
430  return ID_ge;
431  if(stmt==patternt("if_?cmpeq"))
432  return ID_equal;
433  if(stmt==patternt("if_?cmpne"))
434  return ID_notequal;
435 
436  throw "unhandled java comparison instruction";
437 }
438 
439 static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
440 {
441  symbol_typet class_type(fieldref.get(ID_class));
442 
443  exprt pointer2=
444  typecast_exprt(pointer, java_reference_type(class_type));
445 
446  const dereference_exprt obj_deref(pointer2, class_type);
447 
448  return member_exprt(
449  obj_deref,
450  fieldref.get(ID_component_name),
451  fieldref.type());
452 }
453 
455  const exprt &arraystruct,
456  const exprt &idx,
457  const source_locationt &original_sloc)
458 {
460  binary_relation_exprt gezero(idx, ID_ge, intzero);
461  const member_exprt length_field(arraystruct, "length", java_int_type());
462  binary_relation_exprt ltlength(idx, ID_lt, length_field);
463  code_blockt bounds_checks;
464 
465  bounds_checks.add(code_assertt(gezero));
466  bounds_checks.operands().back().add_source_location()=original_sloc;
467  bounds_checks.operands().back().add_source_location()
468  .set_comment("Array index < 0");
469  bounds_checks.operands().back().add_source_location()
470  .set_property_class("array-index-out-of-bounds-low");
471  bounds_checks.add(code_assertt(ltlength));
472 
473  bounds_checks.operands().back().add_source_location()=original_sloc;
474  bounds_checks.operands().back().add_source_location()
475  .set_comment("Array index >= length");
476  bounds_checks.operands().back().add_source_location()
477  .set_property_class("array-index-out-of-bounds-high");
478 
479  // TODO make this throw ArrayIndexOutOfBoundsException instead of asserting.
480  return bounds_checks;
481 }
482 
490  codet &repl,
491  const irep_idt &old_label,
492  const irep_idt &new_label)
493 {
494  const auto &stmt=repl.get_statement();
495  if(stmt==ID_goto)
496  {
497  auto &g=to_code_goto(repl);
498  if(g.get_destination()==old_label)
499  g.set_destination(new_label);
500  }
501  else
502  {
503  for(auto &op : repl.operands())
504  if(op.id()==ID_code)
505  replace_goto_target(to_code(op), old_label, new_label);
506  }
507 }
508 
524  block_tree_nodet &tree,
525  code_blockt &this_block,
526  unsigned address_start,
527  unsigned address_limit,
528  unsigned next_block_start_address)
529 {
530  address_mapt dummy;
532  tree,
533  this_block,
534  address_start,
535  address_limit,
536  next_block_start_address,
537  dummy,
538  false);
539 }
540 
556  block_tree_nodet &tree,
557  code_blockt &this_block,
558  unsigned address_start,
559  unsigned address_limit,
560  unsigned next_block_start_address,
561  const address_mapt &amap,
562  bool allow_merge)
563 {
564  // Check the tree shape invariant:
565  assert(tree.branch.size()==tree.branch_addresses.size());
566 
567  // If there are no child blocks, return this.
568  if(tree.leaf)
569  return this_block;
570  assert(!tree.branch.empty());
571 
572  // Find child block starting > address_start:
573  const auto afterstart=
574  std::upper_bound(
575  tree.branch_addresses.begin(),
576  tree.branch_addresses.end(),
577  address_start);
578  assert(afterstart!=tree.branch_addresses.begin());
579  auto findstart=afterstart;
580  --findstart;
581  auto child_offset=
582  std::distance(tree.branch_addresses.begin(), findstart);
583 
584  // Find child block starting >= address_limit:
585  auto findlim=
586  std::lower_bound(
587  tree.branch_addresses.begin(),
588  tree.branch_addresses.end(),
589  address_limit);
590  unsigned findlim_block_start_address=
591  findlim==tree.branch_addresses.end() ?
592  next_block_start_address :
593  (*findlim);
594 
595  // If all children are in scope, return this.
596  if(findstart==tree.branch_addresses.begin() &&
597  findlim==tree.branch_addresses.end())
598  return this_block;
599 
600  // Find the child code_blockt where the queried range begins:
601  auto child_iter=this_block.operands().begin();
602  // Skip any top-of-block declarations;
603  // all other children are labelled subblocks.
604  while(child_iter!=this_block.operands().end() &&
605  to_code(*child_iter).get_statement()==ID_decl)
606  ++child_iter;
607  assert(child_iter!=this_block.operands().end());
608  std::advance(child_iter, child_offset);
609  assert(child_iter!=this_block.operands().end());
610  auto &child_label=to_code_label(to_code(*child_iter));
611  auto &child_block=to_code_block(child_label.code());
612 
613  bool single_child(afterstart==findlim);
614  if(single_child)
615  {
616  // Range wholly contained within a child block
618  tree.branch[child_offset],
619  child_block,
620  address_start,
621  address_limit,
622  findlim_block_start_address,
623  amap,
624  allow_merge);
625  }
626 
627  // Otherwise we're being asked for a range of subblocks, but not all of them.
628  // If it's legal to draw a new lexical scope around the requested subset,
629  // do so; otherwise just return this block.
630 
631  // This can be a new lexical scope if all incoming edges target the
632  // new block header, or come from within the suggested new block.
633 
634  // If modifying the block tree is forbidden, give up and return this:
635  if(!allow_merge)
636  return this_block;
637 
638  // Check for incoming control-flow edges targeting non-header
639  // blocks of the new proposed block range:
640  auto checkit=amap.find(*findstart);
641  assert(checkit!=amap.end());
642  ++checkit; // Skip the header, which can have incoming edges from outside.
643  for(;
644  checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
645  ++checkit)
646  {
647  for(auto p : checkit->second.predecessors)
648  {
649  if(p<(*findstart) || p>=findlim_block_start_address)
650  {
651  debug() << "Warning: refusing to create lexical block spanning "
652  << (*findstart) << "-" << findlim_block_start_address
653  << " due to incoming edge " << p << " -> "
654  << checkit->first << eom;
655  return this_block;
656  }
657  }
658  }
659 
660  // All incoming edges are acceptable! Create a new block wrapping
661  // the relevant children. Borrow the header block's label, and redirect
662  // any block-internal edges to target the inner header block.
663 
664  const irep_idt child_label_name=child_label.get_label();
665  std::string new_label_str=as_string(child_label_name);
666  new_label_str+='$';
667  irep_idt new_label_irep(new_label_str);
668 
669  code_labelt newlabel(child_label_name, code_blockt());
670  code_blockt &newblock=to_code_block(newlabel.code());
671  auto nblocks=std::distance(findstart, findlim);
672  assert(nblocks>=2);
673  debug() << "Combining " << std::distance(findstart, findlim)
674  << " blocks for addresses " << (*findstart) << "-"
675  << findlim_block_start_address << eom;
676 
677  // Make a new block containing every child of interest:
678  auto &this_block_children=this_block.operands();
679  assert(tree.branch.size()==this_block_children.size());
680  for(auto blockidx=child_offset, blocklim=child_offset+nblocks;
681  blockidx!=blocklim;
682  ++blockidx)
683  newblock.move_to_operands(this_block_children[blockidx]);
684 
685  // Relabel the inner header:
686  to_code_label(to_code(newblock.operands()[0])).set_label(new_label_irep);
687  // Relabel internal gotos:
688  replace_goto_target(newblock, child_label_name, new_label_irep);
689 
690  // Remove the now-empty sibling blocks:
691  auto delfirst=this_block_children.begin();
692  std::advance(delfirst, child_offset+1);
693  auto dellim=delfirst;
694  std::advance(dellim, nblocks-1);
695  this_block_children.erase(delfirst, dellim);
696  this_block_children[child_offset].swap(newlabel);
697 
698  // Perform the same transformation on the index tree:
699  block_tree_nodet newnode;
700  auto branchstart=tree.branch.begin();
701  std::advance(branchstart, child_offset);
702  auto branchlim=branchstart;
703  std::advance(branchlim, nblocks);
704  for(auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
705  newnode.branch.push_back(std::move(*branchiter));
706  ++branchstart;
707  tree.branch.erase(branchstart, branchlim);
708 
709  assert(tree.branch.size()==this_block_children.size());
710 
711  auto branchaddriter=tree.branch_addresses.begin();
712  std::advance(branchaddriter, child_offset);
713  auto branchaddrlim=branchaddriter;
714  std::advance(branchaddrlim, nblocks);
715  newnode.branch_addresses.insert(
716  newnode.branch_addresses.begin(),
717  branchaddriter,
718  branchaddrlim);
719 
720  ++branchaddriter;
721  tree.branch_addresses.erase(branchaddriter, branchaddrlim);
722 
723  tree.branch[child_offset]=std::move(newnode);
724 
725  assert(tree.branch.size()==tree.branch_addresses.size());
726 
727  return
730  to_code(this_block_children[child_offset])).code());
731 }
732 
734  unsigned pc,
735  const exprt &e,
736  std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
737 {
738  if(e.id()==ID_symbol)
739  {
740  const auto &symexpr=to_symbol_expr(e);
741  auto findit=
742  result.insert({ // NOLINT(whitespace/braces)
743  symexpr.get_identifier(),
745  auto &var=findit.first->second;
746  if(findit.second)
747  {
748  var.symbol_expr=symexpr;
749  var.start_pc=pc;
750  var.length=1;
751  }
752  else
753  {
754  if(pc<var.start_pc)
755  {
756  var.length+=(var.start_pc-pc);
757  var.start_pc=pc;
758  }
759  else
760  {
761  var.length=std::max(var.length, (pc-var.start_pc)+1);
762  }
763  }
764  }
765  else
766  {
767  forall_operands(it, e)
768  gather_symbol_live_ranges(pc, *it, result);
769  }
770 }
771 
772 static unsigned get_bytecode_type_width(const typet &ty)
773 {
774  if(ty.id()==ID_pointer)
775  return 32;
776  return ty.get_unsigned_int(ID_width);
777 }
778 
780  const methodt &method,
781  const code_typet &method_type)
782 {
783  const instructionst &instructions=method.instructions;
784 
785  // Run a worklist algorithm, assuming that the bytecode has not
786  // been tampered with. See "Leroy, X. (2003). Java bytecode
787  // verification: algorithms and formalizations. Journal of Automated
788  // Reasoning, 30(3-4), 235-269." for a more complete treatment.
789 
790  // first pass: get targets and map addresses to instructions
791 
792  address_mapt address_map;
793  std::set<unsigned> targets;
794 
795  std::vector<unsigned> jsr_ret_targets;
796  std::vector<instructionst::const_iterator> ret_instructions;
797 
798  for(instructionst::const_iterator
799  i_it=instructions.begin();
800  i_it!=instructions.end();
801  i_it++)
802  {
804  std::pair<address_mapt::iterator, bool> a_entry=
805  address_map.insert(std::make_pair(i_it->address, ins));
806  assert(a_entry.second);
807  // addresses are strictly increasing, hence we must have inserted
808  // a new maximal key
809  assert(a_entry.first==--address_map.end());
810 
811  if(i_it->statement!="goto" &&
812  i_it->statement!="return" &&
813  !(i_it->statement==patternt("?return")) &&
814  i_it->statement!="athrow" &&
815  i_it->statement!="jsr" &&
816  i_it->statement!="jsr_w" &&
817  i_it->statement!="ret")
818  {
819  instructionst::const_iterator next=i_it;
820  if(++next!=instructions.end())
821  a_entry.first->second.successors.push_back(next->address);
822  }
823 
824  if(i_it->statement=="athrow" ||
825  i_it->statement=="invokestatic" ||
826  i_it->statement=="invokevirtual" ||
827  i_it->statement=="invokespecial" ||
828  i_it->statement=="invokeinterface")
829  {
830  // find the corresponding try-catch blocks and add the handlers
831  // to the targets
832  for(const auto &exception_row : method.exception_table)
833  {
834  if(i_it->address>=exception_row.start_pc &&
835  i_it->address<exception_row.end_pc)
836  {
837  a_entry.first->second.successors.push_back(
838  exception_row.handler_pc);
839  targets.insert(exception_row.handler_pc);
840  }
841  }
842  }
843 
844  if(i_it->statement=="goto" ||
845  i_it->statement==patternt("if_?cmp??") ||
846  i_it->statement==patternt("if??") ||
847  i_it->statement=="ifnonnull" ||
848  i_it->statement=="ifnull" ||
849  i_it->statement=="jsr" ||
850  i_it->statement=="jsr_w")
851  {
852  assert(!i_it->args.empty());
853 
854  unsigned target;
855  bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
856  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
857  targets.insert(target);
858 
859  a_entry.first->second.successors.push_back(target);
860 
861  if(i_it->statement=="jsr" ||
862  i_it->statement=="jsr_w")
863  {
864  instructionst::const_iterator next=i_it+1;
865  assert(
866  next!=instructions.end() &&
867  "jsr without valid return address?");
868  targets.insert(next->address);
869  jsr_ret_targets.push_back(next->address);
870  }
871  }
872  else if(i_it->statement=="tableswitch" ||
873  i_it->statement=="lookupswitch")
874  {
875  bool is_label=true;
876  for(const auto &arg : i_it->args)
877  {
878  if(is_label)
879  {
880  unsigned target;
881  bool ret=to_unsigned_integer(to_constant_expr(arg), target);
882  DATA_INVARIANT(!ret, "target expected to be unsigned integer");
883  targets.insert(target);
884  a_entry.first->second.successors.push_back(target);
885  }
886  is_label=!is_label;
887  }
888  }
889  else if(i_it->statement=="ret")
890  {
891  // Finish these later, once we've seen all jsr instructions.
892  ret_instructions.push_back(i_it);
893  }
894  }
895 
896  // Draw edges from every `ret` to every `jsr` successor. Could do better with
897  // flow analysis to distinguish multiple subroutines within the same function.
898  for(const auto retinst : ret_instructions)
899  {
900  auto &a_entry=address_map.at(retinst->address);
901  a_entry.successors.insert(
902  a_entry.successors.end(),
903  jsr_ret_targets.begin(),
904  jsr_ret_targets.end());
905  }
906 
907  for(const auto &address : address_map)
908  {
909  for(unsigned s : address.second.successors)
910  {
911  address_mapt::iterator a_it=address_map.find(s);
912  assert(a_it!=address_map.end());
913 
914  a_it->second.predecessors.insert(address.first);
915  }
916  }
917 
918  // Now that the control flow graph is built, set up our local variables
919  // (these require the graph to determine live ranges)
920  setup_local_variables(method, address_map);
921 
922  std::set<unsigned> working_set;
923 
924  if(!instructions.empty())
925  working_set.insert(instructions.front().address);
926 
927  while(!working_set.empty())
928  {
929  std::set<unsigned>::iterator cur=working_set.begin();
930  address_mapt::iterator a_it=address_map.find(*cur);
931  assert(a_it!=address_map.end());
932  unsigned cur_pc=*cur;
933  working_set.erase(cur);
934 
935  if(a_it->second.done)
936  continue;
937  working_set
938  .insert(a_it->second.successors.begin(), a_it->second.successors.end());
939 
940  instructionst::const_iterator i_it=a_it->second.source;
941  stack.swap(a_it->second.stack);
942  a_it->second.stack.clear();
943  codet &c=a_it->second.code;
944 
945  assert(
946  stack.empty() ||
947  a_it->second.predecessors.size()<=1 ||
948  has_prefix(
949  stack.front().get_string(ID_C_base_name),
950  "$stack"));
951 
952  irep_idt statement=i_it->statement;
953  exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
954  exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
955 
957 
958  // deal with _idx suffixes
959  if(statement.size()>=2 &&
960  statement[statement.size()-2]=='_' &&
961  isdigit(statement[statement.size()-1]))
962  {
963  arg0=
964  from_integer(
966  std::string(id2string(statement), statement.size()-1, 1)),
967  java_int_type());
968  statement=std::string(id2string(statement), 0, statement.size()-2);
969  }
970 
971  // we throw away the first statement in an exception handler
972  // as we don't know if a function call had a normal or exceptional return
973  auto it=method.exception_table.begin();
974  for(; it!=method.exception_table.end(); ++it)
975  {
976  if(cur_pc==it->handler_pc)
977  {
978  exprt exc_var=variable(
979  arg0, statement[0],
980  i_it->address,
981  NO_CAST);
982 
983  // throw away the operands
985 
986  // add a CATCH-PUSH signaling a handler
987  side_effect_expr_catcht catch_handler_expr;
988  // pack the exception variable so that it can be used
989  // later for instrumentation
990  catch_handler_expr.get_sub().resize(1);
991  catch_handler_expr.get_sub()[0]=exc_var;
992 
993  code_expressiont catch_handler(catch_handler_expr);
994  code_labelt newlabel(label(std::to_string(cur_pc)),
995  code_blockt());
996 
997  code_blockt label_block=to_code_block(newlabel.code());
998  code_blockt handler_block;
999  handler_block.move_to_operands(c);
1000  handler_block.move_to_operands(catch_handler);
1001  handler_block.move_to_operands(label_block);
1002  c=handler_block;
1003  break;
1004  }
1005  }
1006 
1007  if(it!=method.exception_table.end())
1008  {
1009  // go straight to the next statement
1010  continue;
1011  }
1012 
1014  exprt::operandst results;
1015  results.resize(bytecode_info.push, nil_exprt());
1016 
1017  if(statement=="aconst_null")
1018  {
1019  assert(results.size()==1);
1021  }
1022  else if(statement=="athrow")
1023  {
1024  assert(op.size()==1 && results.size()==1);
1025  code_blockt block;
1026  // TODO throw NullPointerException instead
1027  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
1028  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
1029  const exprt not_equal_null(
1030  binary_relation_exprt(lhs, ID_notequal, rhs));
1031  code_assertt check(not_equal_null);
1032  check.add_source_location()
1033  .set_comment("Throw null");
1034  check.add_source_location()
1035  .set_property_class("null-pointer-exception");
1036  block.move_to_operands(check);
1037 
1038  side_effect_expr_throwt throw_expr;
1039  throw_expr.add_source_location()=i_it->source_location;
1040  throw_expr.copy_to_operands(op[0]);
1041  c=code_expressiont(throw_expr);
1042  results[0]=op[0];
1043 
1044  block.move_to_operands(c);
1045  c=block;
1046  }
1047  else if(statement=="checkcast")
1048  {
1049  // checkcast throws an exception in case a cast of object
1050  // on stack to given type fails.
1051  // The stack isn't modified.
1052  // TODO: convert assertions to exceptions.
1053  assert(op.size()==1 && results.size()==1);
1054  binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
1055  c=code_assertt(check);
1056  c.add_source_location().set_comment("Dynamic cast check");
1057  c.add_source_location().set_property_class("bad-dynamic-cast");
1058 
1059  results[0]=op[0];
1060  }
1061  else if(statement=="invokedynamic")
1062  {
1063  // not used in Java
1064  code_typet &code_type=to_code_type(arg0.type());
1065  const code_typet::parameterst &parameters(code_type.parameters());
1066 
1067  pop(parameters.size());
1068 
1069  const typet &return_type=code_type.return_type();
1070 
1071  if(return_type.id()!=ID_empty)
1072  {
1073  results.resize(1);
1074  results[0]=
1076  return_type,
1077  i_it->source_location,
1080  }
1081  }
1082  else if(statement=="invokeinterface" ||
1083  statement=="invokespecial" ||
1084  statement=="invokevirtual" ||
1085  statement=="invokestatic")
1086  {
1087  const bool use_this(statement!="invokestatic");
1088  const bool is_virtual(
1089  statement=="invokevirtual" || statement=="invokeinterface");
1090 
1091  code_typet &code_type=to_code_type(arg0.type());
1092  code_typet::parameterst &parameters(code_type.parameters());
1093 
1094  if(use_this)
1095  {
1096  if(parameters.empty() || !parameters[0].get_this())
1097  {
1098  irep_idt classname=arg0.get(ID_C_class);
1099  typet thistype=symbol_typet(classname);
1100  // Note invokespecial is used for super-method calls as well as
1101  // constructors.
1102  if(statement=="invokespecial")
1103  {
1104  if(as_string(arg0.get(ID_identifier))
1105  .find("<init>")!=std::string::npos)
1106  {
1107  if(lazy_methods)
1108  lazy_methods->add_needed_class(classname);
1109  code_type.set(ID_constructor, true);
1110  }
1111  else
1112  code_type.set(ID_java_super_method_call, true);
1113  }
1114  reference_typet object_ref_type=java_reference_type(thistype);
1115  code_typet::parametert this_p(object_ref_type);
1116  this_p.set_this();
1117  this_p.set_base_name("this");
1118  parameters.insert(parameters.begin(), this_p);
1119  }
1120  }
1121 
1122  code_function_callt call;
1123  source_locationt loc=i_it->source_location;
1124  loc.set_function(method_id);
1125 
1126  call.add_source_location()=loc;
1127  call.arguments()=pop(parameters.size());
1128 
1129  // double-check a bit
1130  if(use_this)
1131  {
1132  const exprt &this_arg=call.arguments().front();
1133  assert(this_arg.type().id()==ID_pointer);
1134  }
1135 
1136  // do some type adjustment for the arguments,
1137  // as Java promotes arguments
1138  // Also cast pointers since intermediate locals
1139  // can be void*.
1140 
1141  for(std::size_t i=0; i<parameters.size(); i++)
1142  {
1143  const typet &type=parameters[i].type();
1144  if(type==java_boolean_type() ||
1145  type==java_char_type() ||
1146  type==java_byte_type() ||
1147  type==java_short_type() ||
1148  type.id()==ID_pointer)
1149  {
1150  assert(i<call.arguments().size());
1151  if(type!=call.arguments()[i].type())
1152  call.arguments()[i].make_typecast(type);
1153  }
1154  }
1155 
1156  // do some type adjustment for return values
1157 
1158  const typet &return_type=code_type.return_type();
1159 
1160  if(return_type.id()!=ID_empty)
1161  {
1162  // return types are promoted in Java
1163  call.lhs()=tmp_variable("return", return_type);
1164  exprt promoted=java_bytecode_promotion(call.lhs());
1165  results.resize(1);
1166  results[0]=promoted;
1167  }
1168 
1169  assert(arg0.id()==ID_virtual_function);
1170 
1171  // does the function symbol exist?
1172  irep_idt id=arg0.get(ID_identifier);
1173 
1174  if(symbol_table.symbols.find(id)==symbol_table.symbols.end())
1175  {
1176  // no, create stub
1177  symbolt symbol;
1178  symbol.name=id;
1179  symbol.base_name=arg0.get(ID_C_base_name);
1180  symbol.type=arg0.type();
1181  symbol.value.make_nil();
1182  symbol.mode=ID_java;
1183  symbol_table.add(symbol);
1184  }
1185 
1186  if(is_virtual)
1187  {
1188  // dynamic binding
1189  assert(use_this);
1190  assert(!call.arguments().empty());
1191  call.function()=arg0;
1192  // Populate needed methods later,
1193  // once we know what object types can exist.
1194  }
1195  else
1196  {
1197  // static binding
1198  call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type());
1199  if(lazy_methods)
1200  lazy_methods->add_needed_method(arg0.get(ID_identifier));
1201  }
1202 
1203  call.function().add_source_location()=loc;
1204 
1205  // Replacing call if it is a function of the Character library,
1206  // returning the same call otherwise
1208  }
1209  else if(statement=="return")
1210  {
1211  assert(op.empty() && results.empty());
1212  c=code_returnt();
1213  }
1214  else if(statement==patternt("?return"))
1215  {
1216  // Return types are promoted in java, so this might need
1217  // conversion.
1218  assert(op.size()==1 && results.empty());
1219  exprt r=op[0];
1220  if(r.type()!=method_return_type)
1222  c=code_returnt(r);
1223  }
1224  else if(statement==patternt("?astore"))
1225  {
1226  assert(op.size()==3 && results.empty());
1227 
1228  char type_char=statement[0];
1229 
1230  exprt pointer=
1231  typecast_exprt(op[0], java_array_type(type_char));
1232 
1233  const dereference_exprt deref(pointer, pointer.type().subtype());
1234 
1235  const member_exprt data_ptr(
1236  deref,
1237  "data",
1238  pointer_type(java_type_from_char(type_char)));
1239 
1240  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
1241  typet element_type=data_ptr.type().subtype();
1242  const dereference_exprt element(data_plus_offset, element_type);
1243 
1244  code_blockt block;
1245  block.add_source_location()=i_it->source_location;
1246 
1248  "stack_astore",
1249  element_type,
1250  block,
1252  "");
1253 
1254  codet bounds_check=
1255  get_array_bounds_check(deref, op[1], i_it->source_location);
1256  bounds_check.add_source_location()=i_it->source_location;
1257  block.move_to_operands(bounds_check);
1258  code_assignt array_put(element, op[2]);
1259  array_put.add_source_location()=i_it->source_location;
1260  block.move_to_operands(array_put);
1261  c=block;
1262  }
1263  else if(statement==patternt("?store"))
1264  {
1265  // store value into some local variable
1266  assert(op.size()==1 && results.empty());
1267 
1268  exprt var=
1269  variable(arg0, statement[0], i_it->address, NO_CAST);
1270  const irep_idt &var_name=to_symbol_expr(var).get_identifier();
1271 
1272  exprt toassign=op[0];
1273  if('a'==statement[0] && toassign.type()!=var.type())
1274  toassign=typecast_exprt(toassign, var.type());
1275 
1276  code_blockt block;
1277 
1279  "stack_store",
1280  toassign.type(),
1281  block,
1283  var_name);
1284  code_assignt assign(var, toassign);
1285  assign.add_source_location()=i_it->source_location;
1286  block.copy_to_operands(assign);
1287  c=block;
1288  }
1289  else if(statement==patternt("?aload"))
1290  {
1291  assert(op.size()==2 && results.size()==1);
1292 
1293  char type_char=statement[0];
1294 
1295  exprt pointer=
1296  typecast_exprt(op[0], java_array_type(type_char));
1297 
1298  const dereference_exprt deref(pointer, pointer.type().subtype());
1299 
1300  const member_exprt data_ptr(
1301  deref,
1302  "data",
1303  pointer_type(java_type_from_char(type_char)));
1304 
1305  plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
1306  typet element_type=data_ptr.type().subtype();
1307  dereference_exprt element(data_plus_offset, element_type);
1308 
1309  c=get_array_bounds_check(deref, op[1], i_it->source_location);
1310  c.add_source_location()=i_it->source_location;
1311  results[0]=java_bytecode_promotion(element);
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  assert(op.empty() && results.size()==1);
1323 
1324  // 1) Pushing a String causes a reference to a java.lang.String object
1325  // to be constructed and pushed onto the operand stack.
1326 
1327  // 2) Pushing an int or a float causes a primitive value to be pushed
1328  // onto the stack.
1329 
1330  // 3) Pushing a Class constant causes a reference to a java.lang.Class
1331  // to be pushed onto the operand stack
1332 
1333  if(arg0.id()==ID_java_string_literal)
1334  {
1335  // these need to be references to java.lang.String
1336  results[0]=arg0;
1337  symbol_typet string_type("java::java.lang.String");
1338  results[0].type()=java_reference_type(string_type);
1339  }
1340  else if(arg0.id()==ID_type)
1341  {
1342  irep_idt class_id=arg0.type().get(ID_identifier);
1343  symbol_typet java_lang_Class("java::java.lang.Class");
1344  symbol_exprt symbol_expr(
1345  id2string(class_id)+"@class_model",
1346  java_lang_Class);
1347  address_of_exprt address_of_expr(symbol_expr);
1348  results[0]=address_of_expr;
1349  }
1350  else if(arg0.id()==ID_constant)
1351  {
1352  results[0]=arg0;
1353  }
1354  else
1355  {
1356  error() << "unexpected ldc argument" << eom;
1357  throw 0;
1358  }
1359  }
1360  else if(statement=="goto" || statement=="goto_w")
1361  {
1362  assert(op.empty() && results.empty());
1363  mp_integer number;
1364  bool ret=to_integer(to_constant_expr(arg0), number);
1365  INVARIANT(!ret, "goto argument should be an integer");
1366  code_gotot code_goto(label(integer2string(number)));
1367  c=code_goto;
1368  }
1369  else if(statement=="jsr" || statement=="jsr_w")
1370  {
1371  // As 'goto', except we must also push the subroutine return address:
1372  assert(op.empty() && results.size()==1);
1373  mp_integer number;
1374  bool ret=to_integer(to_constant_expr(arg0), number);
1375  INVARIANT(!ret, "jsr argument should be an integer");
1376  code_gotot code_goto(label(integer2string(number)));
1377  c=code_goto;
1378  results[0]=
1379  from_integer(
1380  std::next(i_it)->address,
1381  unsignedbv_typet(64));
1382  results[0].type()=pointer_typet(void_typet(), 64);
1383  }
1384  else if(statement=="ret")
1385  {
1386  // Since we have a bounded target set, make life easier on our analyses
1387  // and write something like:
1388  // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
1389  assert(op.empty() && results.empty());
1390  c=code_blockt();
1391  auto retvar=variable(arg0, 'a', i_it->address, NO_CAST);
1392  assert(!jsr_ret_targets.empty());
1393  for(size_t idx=0, idxlim=jsr_ret_targets.size(); idx!=idxlim; ++idx)
1394  {
1395  irep_idt number=std::to_string(jsr_ret_targets[idx]);
1396  code_gotot g(label(number));
1397  g.add_source_location()=i_it->source_location;
1398  if(idx==idxlim-1)
1399  c.move_to_operands(g);
1400  else
1401  {
1403  auto address_ptr=
1404  from_integer(
1405  jsr_ret_targets[idx],
1406  unsignedbv_typet(64));
1407  address_ptr.type()=pointer_typet(void_typet(), 64);
1408  branch.cond()=equal_exprt(retvar, address_ptr);
1409  branch.cond().add_source_location()=i_it->source_location;
1410  branch.then_case()=g;
1411  branch.add_source_location()=i_it->source_location;
1412  c.move_to_operands(branch);
1413  }
1414  }
1415  }
1416  else if(statement=="iconst_m1")
1417  {
1418  assert(results.size()==1);
1419  results[0]=from_integer(-1, java_int_type());
1420  }
1421  else if(statement==patternt("?const"))
1422  {
1423  assert(results.size()==1);
1424 
1425  const char type_char=statement[0];
1426  const bool is_double('d'==type_char);
1427  const bool is_float('f'==type_char);
1428 
1429  if(is_double || is_float)
1430  {
1431  const ieee_float_spect spec(
1434 
1435  ieee_floatt value(spec);
1436  if(arg0.type().id()!=ID_floatbv)
1437  {
1438  mp_integer number;
1439  bool ret=to_integer(to_constant_expr(arg0), number);
1440  DATA_INVARIANT(!ret, "failed to convert constant");
1441  value.from_integer(number);
1442  }
1443  else
1444  value.from_expr(to_constant_expr(arg0));
1445 
1446  results[0]=value.to_expr();
1447  }
1448  else
1449  {
1450  mp_integer value;
1451  bool ret=to_integer(to_constant_expr(arg0), value);
1452  DATA_INVARIANT(!ret, "failed to convert constant");
1453  const typet type=java_type_from_char(statement[0]);
1454  results[0]=from_integer(value, type);
1455  }
1456  }
1457  else if(statement==patternt("?ipush"))
1458  {
1459  PRECONDITION(results.size()==1);
1461  arg0.id()==ID_constant,
1462  "ipush argument expected to be constant");
1463  results[0]=arg0;
1464  if(arg0.type()!=java_int_type())
1465  results[0].make_typecast(java_int_type());
1466  }
1467  else if(statement==patternt("if_?cmp??"))
1468  {
1469  assert(op.size()==2 && results.empty());
1470  mp_integer number;
1471  bool ret=to_integer(to_constant_expr(arg0), number);
1472  INVARIANT(!ret, "if_?cmp?? argument should be an integer");
1473 
1474  code_ifthenelset code_branch;
1475  const irep_idt cmp_op=get_if_cmp_operator(statement);
1476 
1477  binary_relation_exprt condition(op[0], cmp_op, op[1]);
1478 
1479  exprt &lhs(condition.lhs());
1480  exprt &rhs(condition.rhs());
1481  const typet &lhs_type(lhs.type());
1482  if(lhs_type!=rhs.type())
1483  rhs=typecast_exprt(rhs, lhs_type);
1484 
1485  code_branch.cond()=condition;
1486  code_branch.cond().add_source_location()=i_it->source_location;
1487  code_branch.then_case()=code_gotot(label(integer2string(number)));
1488  code_branch.then_case().add_source_location()=i_it->source_location;
1489  code_branch.add_source_location()=i_it->source_location;
1490 
1491  c=code_branch;
1492  }
1493  else if(statement==patternt("if??"))
1494  {
1495  const irep_idt id=
1496  statement=="ifeq"?ID_equal:
1497  statement=="ifne"?ID_notequal:
1498  statement=="iflt"?ID_lt:
1499  statement=="ifge"?ID_ge:
1500  statement=="ifgt"?ID_gt:
1501  statement=="ifle"?ID_le:
1502  (assert(false), "");
1503 
1504  assert(op.size()==1 && results.empty());
1505  mp_integer number;
1506  bool ret=to_integer(to_constant_expr(arg0), number);
1507  INVARIANT(!ret, "if?? argument should be an integer");
1508 
1509  code_ifthenelset code_branch;
1510  code_branch.cond()=
1511  binary_relation_exprt(op[0], id, from_integer(0, op[0].type()));
1512  code_branch.cond().add_source_location()=i_it->source_location;
1514  code_branch.then_case()=code_gotot(label(integer2string(number)));
1515  code_branch.then_case().add_source_location()=i_it->source_location;
1517  code_branch.add_source_location()=i_it->source_location;
1519 
1520  c=code_branch;
1521  }
1522  else if(statement==patternt("ifnonnull"))
1523  {
1524  assert(op.size()==1 && results.empty());
1525  mp_integer number;
1526  bool ret=to_integer(to_constant_expr(arg0), number);
1527  INVARIANT(!ret, "ifnonnull argument should be an integer");
1528  code_ifthenelset code_branch;
1529  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
1530  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
1531  code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
1532  code_branch.then_case()=code_gotot(label(integer2string(number)));
1533  code_branch.then_case().add_source_location()=i_it->source_location;
1534  code_branch.add_source_location()=i_it->source_location;
1535 
1536  c=code_branch;
1537  }
1538  else if(statement==patternt("ifnull"))
1539  {
1540  assert(op.size()==1 && results.empty());
1541  mp_integer number;
1542  bool ret=to_integer(to_constant_expr(arg0), number);
1543  INVARIANT(!ret, "ifnull argument should be an integer");
1544  code_ifthenelset code_branch;
1545  const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
1546  const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
1547  code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
1548  code_branch.then_case()=code_gotot(label(integer2string(number)));
1549  code_branch.then_case().add_source_location()=i_it->source_location;
1550  code_branch.add_source_location()=i_it->source_location;
1551 
1552  c=code_branch;
1553  }
1554  else if(statement=="iinc")
1555  {
1556  code_blockt block;
1557  block.add_source_location()=i_it->source_location;
1558  // search variable on stack
1559  const exprt &locvar=variable(arg0, 'i', i_it->address, NO_CAST);
1561  "stack_iinc",
1562  java_int_type(),
1563  block,
1565  to_symbol_expr(locvar).get_identifier());
1566 
1567  code_assignt code_assign;
1568  code_assign.lhs()=
1569  variable(arg0, 'i', i_it->address, NO_CAST);
1570  exprt arg1_int_type=arg1;
1571  if(arg1.type()!=java_int_type())
1572  arg1_int_type.make_typecast(java_int_type());
1573  code_assign.rhs()=plus_exprt(
1574  variable(arg0, 'i', i_it->address, CAST_AS_NEEDED),
1575  arg1_int_type);
1576  block.copy_to_operands(code_assign);
1577  c=block;
1578  }
1579  else if(statement==patternt("?xor"))
1580  {
1581  assert(op.size()==2 && results.size()==1);
1582  results[0]=bitxor_exprt(op[0], op[1]);
1583  }
1584  else if(statement==patternt("?or"))
1585  {
1586  assert(op.size()==2 && results.size()==1);
1587  results[0]=bitor_exprt(op[0], op[1]);
1588  }
1589  else if(statement==patternt("?and"))
1590  {
1591  assert(op.size()==2 && results.size()==1);
1592  results[0]=bitand_exprt(op[0], op[1]);
1593  }
1594  else if(statement==patternt("?shl"))
1595  {
1596  assert(op.size()==2 && results.size()==1);
1597  results[0]=shl_exprt(op[0], op[1]);
1598  }
1599  else if(statement==patternt("?shr"))
1600  {
1601  assert(op.size()==2 && results.size()==1);
1602  results[0]=ashr_exprt(op[0], op[1]);
1603  }
1604  else if(statement==patternt("?ushr"))
1605  {
1606  assert(op.size()==2 && results.size()==1);
1607  const typet type=java_type_from_char(statement[0]);
1608 
1609  const std::size_t width=type.get_size_t(ID_width);
1610  typet target=unsignedbv_typet(width);
1611 
1612  exprt lhs=op[0];
1613  if(lhs.type()!=target)
1614  lhs.make_typecast(target);
1615  exprt rhs=op[1];
1616  if(rhs.type()!=target)
1617  rhs.make_typecast(target);
1618 
1619  results[0]=lshr_exprt(lhs, rhs);
1620  if(results[0].type()!=op[0].type())
1621  results[0].make_typecast(op[0].type());
1622  }
1623  else if(statement==patternt("?add"))
1624  {
1625  assert(op.size()==2 && results.size()==1);
1626  results[0]=plus_exprt(op[0], op[1]);
1627  }
1628  else if(statement==patternt("?sub"))
1629  {
1630  assert(op.size()==2 && results.size()==1);
1631  results[0]=minus_exprt(op[0], op[1]);
1632  }
1633  else if(statement==patternt("?div"))
1634  {
1635  assert(op.size()==2 && results.size()==1);
1636  results[0]=div_exprt(op[0], op[1]);
1637  }
1638  else if(statement==patternt("?mul"))
1639  {
1640  assert(op.size()==2 && results.size()==1);
1641  results[0]=mult_exprt(op[0], op[1]);
1642  }
1643  else if(statement==patternt("?neg"))
1644  {
1645  assert(op.size()==1 && results.size()==1);
1646  results[0]=unary_minus_exprt(op[0], op[0].type());
1647  }
1648  else if(statement==patternt("?rem"))
1649  {
1650  assert(op.size()==2 && results.size()==1);
1651  if(statement=="frem" || statement=="drem")
1652  results[0]=rem_exprt(op[0], op[1]);
1653  else
1654  results[0]=mod_exprt(op[0], op[1]);
1655  }
1656  else if(statement==patternt("?cmp"))
1657  {
1658  assert(op.size()==2 && results.size()==1);
1659 
1660  // The integer result on the stack is:
1661  // 0 if op[0] equals op[1]
1662  // -1 if op[0] is less than op[1]
1663  // 1 if op[0] is greater than op[1]
1664 
1665  const typet t=java_int_type();
1666  exprt one=from_integer(1, t);
1667  exprt minus_one=from_integer(-1, t);
1668 
1669  if_exprt greater=if_exprt(
1670  binary_relation_exprt(op[0], ID_gt, op[1]),
1671  one,
1672  minus_one);
1673 
1674  results[0]=
1675  if_exprt(
1676  binary_relation_exprt(op[0], ID_equal, op[1]),
1677  from_integer(0, t),
1678  greater);
1679  }
1680  else if(statement==patternt("?cmp?"))
1681  {
1682  assert(op.size()==2 && results.size()==1);
1683  const floatbv_typet type(
1684  to_floatbv_type(java_type_from_char(statement[0])));
1685  const ieee_float_spect spec(type);
1686  const ieee_floatt nan(ieee_floatt::NaN(spec));
1687  const constant_exprt nan_expr(nan.to_expr());
1688  const int nan_value(statement[4]=='l' ? -1 : 1);
1689  const typet result_type(java_int_type());
1690  const exprt nan_result(from_integer(nan_value, result_type));
1691 
1692  // (value1 == NaN || value2 == NaN) ?
1693  // nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0;
1694  // (value1 == NaN || value2 == NaN) ?
1695  // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0;
1696 
1697  exprt nan_op0=ieee_float_equal_exprt(nan_expr, op[0]);
1698  exprt nan_op1=ieee_float_equal_exprt(nan_expr, op[1]);
1699  exprt one=from_integer(1, result_type);
1700  exprt minus_one=from_integer(-1, result_type);
1701  results[0]=
1702  if_exprt(
1703  or_exprt(nan_op0, nan_op1),
1704  nan_result,
1705  if_exprt(
1706  ieee_float_equal_exprt(op[0], op[1]),
1707  from_integer(0, result_type),
1708  if_exprt(
1709  binary_relation_exprt(op[0], ID_lt, op[1]),
1710  minus_one,
1711  one)));
1712  }
1713  else if(statement==patternt("?cmpl"))
1714  {
1715  assert(op.size()==2 && results.size()==1);
1716  results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
1717  }
1718  else if(statement=="dup")
1719  {
1720  assert(op.size()==1 && results.size()==2);
1721  results[0]=results[1]=op[0];
1722  }
1723  else if(statement=="dup_x1")
1724  {
1725  assert(op.size()==2 && results.size()==3);
1726  results[0]=op[1];
1727  results[1]=op[0];
1728  results[2]=op[1];
1729  }
1730  else if(statement=="dup_x2")
1731  {
1732  assert(op.size()==3 && results.size()==4);
1733  results[0]=op[2];
1734  results[1]=op[0];
1735  results[2]=op[1];
1736  results[3]=op[2];
1737  }
1738  // dup2* behaviour depends on the size of the operands on the
1739  // stack
1740  else if(statement=="dup2")
1741  {
1742  assert(!stack.empty() && results.empty());
1743 
1744  if(get_bytecode_type_width(stack.back().type())==32)
1745  op=pop(2);
1746  else
1747  op=pop(1);
1748 
1749  results.insert(results.end(), op.begin(), op.end());
1750  results.insert(results.end(), op.begin(), op.end());
1751  }
1752  else if(statement=="dup2_x1")
1753  {
1754  assert(!stack.empty() && results.empty());
1755 
1756  if(get_bytecode_type_width(stack.back().type())==32)
1757  op=pop(3);
1758  else
1759  op=pop(2);
1760 
1761  results.insert(results.end(), op.begin()+1, op.end());
1762  results.insert(results.end(), op.begin(), op.end());
1763  }
1764  else if(statement=="dup2_x2")
1765  {
1766  assert(!stack.empty() && results.empty());
1767 
1768  if(get_bytecode_type_width(stack.back().type())==32)
1769  op=pop(2);
1770  else
1771  op=pop(1);
1772 
1773  assert(!stack.empty());
1774  exprt::operandst op2;
1775 
1776  if(get_bytecode_type_width(stack.back().type())==32)
1777  op2=pop(2);
1778  else
1779  op2=pop(1);
1780 
1781  results.insert(results.end(), op.begin(), op.end());
1782  results.insert(results.end(), op2.begin(), op2.end());
1783  results.insert(results.end(), op.begin(), op.end());
1784  }
1785  else if(statement=="dconst")
1786  {
1787  assert(op.empty() && results.size()==1);
1788  }
1789  else if(statement=="fconst")
1790  {
1791  assert(op.empty() && results.size()==1);
1792  }
1793  else if(statement=="getfield")
1794  {
1795  assert(op.size()==1 && results.size()==1);
1796  results[0]=java_bytecode_promotion(to_member(op[0], arg0));
1797  }
1798  else if(statement=="getstatic")
1799  {
1800  assert(op.empty() && results.size()==1);
1801  symbol_exprt symbol_expr(arg0.type());
1802  const auto &field_name=arg0.get_string(ID_component_name);
1803  symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
1804  if(lazy_methods && arg0.type().id()==ID_symbol)
1805  {
1807  to_symbol_type(arg0.type()).get_identifier());
1808  }
1809  results[0]=java_bytecode_promotion(symbol_expr);
1810 
1811  // set $assertionDisabled to false
1812  if(field_name.find("$assertionsDisabled")!=std::string::npos)
1813  c=code_assignt(symbol_expr, false_exprt());
1814  }
1815  else if(statement=="putfield")
1816  {
1817  assert(op.size()==2 && results.empty());
1818  code_blockt block;
1820  "stack_field",
1821  op[1].type(),
1822  block,
1824  arg0.get(ID_component_name));
1825  block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
1826  c=block;
1827  }
1828  else if(statement=="putstatic")
1829  {
1830  assert(op.size()==1 && results.empty());
1831  symbol_exprt symbol_expr(arg0.type());
1832  const auto &field_name=arg0.get_string(ID_component_name);
1833  symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name);
1834  if(lazy_methods && arg0.type().id()==ID_symbol)
1835  {
1837  to_symbol_type(arg0.type()).get_identifier());
1838  }
1839  code_blockt block;
1840  block.add_source_location()=i_it->source_location;
1841 
1843  "stack_static_field",
1844  symbol_expr.type(),
1845  block,
1847  symbol_expr.get_identifier());
1848  block.copy_to_operands(code_assignt(symbol_expr, op[0]));
1849  c=block;
1850  }
1851  else if(statement==patternt("?2?")) // i2c etc.
1852  {
1853  assert(op.size()==1 && results.size()==1);
1854  typet type=java_type_from_char(statement[2]);
1855  results[0]=op[0];
1856  if(results[0].type()!=type)
1857  results[0].make_typecast(type);
1858  }
1859  else if(statement=="new")
1860  {
1861  // use temporary since the stack symbol might get duplicated
1862  assert(op.empty() && results.size()==1);
1863  const reference_typet ref_type=java_reference_type(arg0.type());
1864  exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type);
1865 
1866  if(!i_it->source_location.get_line().empty())
1867  java_new_expr.add_source_location()=i_it->source_location;
1868 
1869  const exprt tmp=tmp_variable("new", ref_type);
1870  c=code_assignt(tmp, java_new_expr);
1871  c.add_source_location()=i_it->source_location;
1872  results[0]=tmp;
1873  }
1874  else if(statement=="newarray" ||
1875  statement=="anewarray")
1876  {
1877  // the op is the array size
1878  assert(op.size()==1 && results.size()==1);
1879 
1880  char element_type;
1881 
1882  if(statement=="newarray")
1883  {
1884  irep_idt id=arg0.type().id();
1885 
1886  if(id==ID_bool)
1887  element_type='z';
1888  else if(id==ID_char)
1889  element_type='c';
1890  else if(id==ID_float)
1891  element_type='f';
1892  else if(id==ID_double)
1893  element_type='d';
1894  else if(id==ID_byte)
1895  element_type='b';
1896  else if(id==ID_short)
1897  element_type='s';
1898  else if(id==ID_int)
1899  element_type='i';
1900  else if(id==ID_long)
1901  element_type='j';
1902  else
1903  element_type='?';
1904  }
1905  else
1906  element_type='a';
1907 
1908  const reference_typet ref_type=
1909  java_array_type(element_type);
1910 
1911  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
1912  java_new_array.copy_to_operands(op[0]);
1913 
1914  if(!i_it->source_location.get_line().empty())
1915  java_new_array.add_source_location()=i_it->source_location;
1916 
1917  c=code_blockt();
1918  // TODO make this throw NegativeArrayIndexException instead.
1920  binary_relation_exprt gezero(op[0], ID_ge, intzero);
1921  code_assertt check(gezero);
1922  check.add_source_location().set_comment("Array size < 0");
1923  check.add_source_location()
1924  .set_property_class("array-create-negative-size");
1925  c.move_to_operands(check);
1926 
1927  if(max_array_length!=0)
1928  {
1929  constant_exprt size_limit=
1931  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
1932  code_assumet assume_le_max_size(le_max_size);
1933  c.move_to_operands(assume_le_max_size);
1934  }
1935  const exprt tmp=tmp_variable("newarray", ref_type);
1936  c.copy_to_operands(code_assignt(tmp, java_new_array));
1937  results[0]=tmp;
1938  }
1939  else if(statement=="multianewarray")
1940  {
1941  // The first argument is the type, the second argument is the number of
1942  // dimensions. The size of each dimension is on the stack.
1943  mp_integer number;
1944  bool ret=to_integer(to_constant_expr(arg1), number);
1945  INVARIANT(!ret, "multianewarray argument should be an integer");
1946  std::size_t dimension=integer2size_t(number);
1947 
1948  op=pop(dimension);
1949  assert(results.size()==1);
1950 
1951  const reference_typet ref_type=
1952  java_reference_type(arg0.type());
1953 
1954  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
1955  java_new_array.operands()=op;
1956 
1957  if(!i_it->source_location.get_line().empty())
1958  java_new_array.add_source_location()=i_it->source_location;
1959 
1960  code_blockt checkandcreate;
1961  // TODO make this throw NegativeArrayIndexException instead.
1963  binary_relation_exprt gezero(op[0], ID_ge, intzero);
1964  code_assertt check(gezero);
1965  check.add_source_location().set_comment("Array size < 0");
1966  check.add_source_location()
1967  .set_property_class("array-create-negative-size");
1968  checkandcreate.move_to_operands(check);
1969 
1970  if(max_array_length!=0)
1971  {
1972  constant_exprt size_limit=
1974  binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
1975  code_assumet assume_le_max_size(le_max_size);
1976  checkandcreate.move_to_operands(assume_le_max_size);
1977  }
1978 
1979  const exprt tmp=tmp_variable("newarray", ref_type);
1980  c=code_assignt(tmp, java_new_array);
1981  results[0]=tmp;
1982  }
1983  else if(statement=="arraylength")
1984  {
1985  assert(op.size()==1 && results.size()==1);
1986 
1987  exprt pointer=
1988  typecast_exprt(op[0], java_array_type(statement[0]));
1989 
1990  const dereference_exprt array(pointer, pointer.type().subtype());
1991  assert(pointer.type().subtype().id()==ID_symbol);
1992 
1993  const member_exprt length(array, "length", java_int_type());
1994 
1995  results[0]=length;
1996  }
1997  else if(statement=="tableswitch" ||
1998  statement=="lookupswitch")
1999  {
2000  assert(op.size()==1 && results.empty());
2001 
2002  // we turn into switch-case
2003  code_switcht code_switch;
2004  code_switch.add_source_location()=i_it->source_location;
2005  code_switch.value()=op[0];
2006  code_blockt code_block;
2007  code_block.add_source_location()=i_it->source_location;
2008 
2009  bool is_label=true;
2010  for(instructiont::argst::const_iterator
2011  a_it=i_it->args.begin();
2012  a_it!=i_it->args.end();
2013  a_it++, is_label=!is_label)
2014  {
2015  if(is_label)
2016  {
2017  code_switch_caset code_case;
2018  code_case.add_source_location()=i_it->source_location;
2019 
2020  mp_integer number;
2021  bool ret=to_integer(to_constant_expr(*a_it), number);
2022  DATA_INVARIANT(!ret, "case label expected to be integer");
2023  code_case.code()=code_gotot(label(integer2string(number)));
2024  code_case.code().add_source_location()=i_it->source_location;
2025 
2026  if(a_it==i_it->args.begin())
2027  code_case.set_default();
2028  else
2029  {
2030  instructiont::argst::const_iterator prev=a_it;
2031  prev--;
2032  code_case.case_op()=*prev;
2033  if(code_case.case_op().type()!=op[0].type())
2034  code_case.case_op().make_typecast(op[0].type());
2035  code_case.case_op().add_source_location()=i_it->source_location;
2036  }
2037 
2038  code_block.add(code_case);
2039  }
2040  }
2041 
2042  code_switch.body()=code_block;
2043  c=code_switch;
2044  }
2045  else if(statement=="pop" || statement=="pop2")
2046  {
2047  // these are skips
2048  c=code_skipt();
2049 
2050  // pop2 removes two single-word items from the stack (e.g. two
2051  // integers, or an integer and an object reference) or one
2052  // two-word item (i.e. a double or a long).
2053  // http://cs.au.dk/~mis/dOvs/jvmspec/ref-pop2.html
2054  if(statement=="pop2" &&
2055  get_bytecode_type_width(op[0].type())==32)
2056  pop(1);
2057  }
2058  else if(statement=="instanceof")
2059  {
2060  assert(op.size()==1 && results.size()==1);
2061 
2062  results[0]=
2063  binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
2064  }
2065  else if(statement=="monitorenter")
2066  {
2067  // becomes a function call
2068  code_typet type;
2069  type.return_type()=void_typet();
2070  type.parameters().resize(1);
2071  type.parameters()[0].type()=java_reference_type(void_typet());
2072  code_function_callt call;
2073  call.function()=symbol_exprt("java::monitorenter", type);
2074  call.lhs().make_nil();
2075  call.arguments().push_back(op[0]);
2076  call.add_source_location()=i_it->source_location;
2077  c=call;
2078  }
2079  else if(statement=="monitorexit")
2080  {
2081  // becomes a function call
2082  code_typet type;
2083  type.return_type()=void_typet();
2084  type.parameters().resize(1);
2085  type.parameters()[0].type()=java_reference_type(void_typet());
2086  code_function_callt call;
2087  call.function()=symbol_exprt("java::monitorexit", type);
2088  call.lhs().make_nil();
2089  call.arguments().push_back(op[0]);
2090  call.add_source_location()=i_it->source_location;
2091  c=call;
2092  }
2093  else
2094  {
2095  c=codet(statement);
2096  c.operands()=op;
2097  }
2098 
2099  // next we do the exception handling
2100  std::vector<irep_idt> exception_ids;
2101  std::vector<irep_idt> handler_labels;
2102 
2103  // for each try-catch add a CATCH-PUSH instruction
2104  // each CATCH-PUSH records a list of all the handler labels
2105  // together with a list of all the exception ids
2106 
2107  // be aware of different try-catch blocks with the same starting pc
2108  std::size_t pos=0;
2109  std::size_t end_pc=0;
2110  while(pos<method.exception_table.size())
2111  {
2112  // check if this is the beginning of a try block
2113  for(; pos<method.exception_table.size(); ++pos)
2114  {
2115  // unexplored try-catch?
2116  if(cur_pc==method.exception_table[pos].start_pc && end_pc==0)
2117  {
2118  end_pc=method.exception_table[pos].end_pc;
2119  }
2120 
2121  // currently explored try-catch?
2122  if(cur_pc==method.exception_table[pos].start_pc &&
2123  method.exception_table[pos].end_pc==end_pc)
2124  {
2125  exception_ids.push_back(
2126  method.exception_table[pos].catch_type.get_identifier());
2127  // record the exception handler in the CATCH-PUSH
2128  // instruction by generating a label corresponding to
2129  // the handler's pc
2130  handler_labels.push_back(
2131  label(std::to_string(method.exception_table[pos].handler_pc)));
2132  }
2133  else
2134  break;
2135  }
2136 
2137  // add the actual PUSH-CATCH instruction
2138  if(!exception_ids.empty())
2139  {
2140  // add the exception ids
2141  side_effect_expr_catcht catch_push_expr;
2142  irept result(ID_exception_list);
2143  result.get_sub().resize(exception_ids.size());
2144  for(size_t i=0; i<exception_ids.size(); ++i)
2145  result.get_sub()[i].id(exception_ids[i]);
2146  catch_push_expr.set(ID_exception_list, result);
2147 
2148  // add the labels corresponding to the handlers
2149  irept labels(ID_label);
2150  labels.get_sub().resize(handler_labels.size());
2151  for(size_t i=0; i<handler_labels.size(); ++i)
2152  labels.get_sub()[i].id(handler_labels[i]);
2153  catch_push_expr.set(ID_label, labels);
2154 
2155  code_blockt try_block;
2156  code_expressiont catch_push(catch_push_expr);
2157  try_block.move_to_operands(catch_push);
2158  try_block.move_to_operands(c);
2159  c=try_block;
2160  }
2161  else
2162  {
2163  // advance
2164  ++pos;
2165  }
2166 
2167  // reset
2168  end_pc=0;
2169  exception_ids.clear();
2170  handler_labels.clear();
2171  }
2172 
2173  // next add the CATCH-POP instructions
2174  size_t start_pc=0;
2175  // as the first try block may have start_pc 0, we
2176  // must track it separately
2177  bool first_handler=false;
2178  // check if this is the end of a try block
2179  for(const auto &exception_row : method.exception_table)
2180  {
2181  // add the CATCH-POP before the end of the try block
2182  if(cur_pc<exception_row.end_pc &&
2183  !working_set.empty() &&
2184  *working_set.begin()==exception_row.end_pc)
2185  {
2186  // have we already added a CATCH-POP for the current try-catch?
2187  // (each row corresponds to a handler)
2188  if(exception_row.start_pc!=start_pc || !first_handler)
2189  {
2190  if(!first_handler)
2191  first_handler=true;
2192  // remember the beginning of the try-catch so that we don't add
2193  // another CATCH-POP for the same try-catch
2194  start_pc=exception_row.start_pc;
2195  // add CATCH_POP instruction
2196  side_effect_expr_catcht catch_pop_expr;
2197  code_blockt end_try_block;
2198  code_expressiont catch_pop(catch_pop_expr);
2199  catch_pop.set(ID_exception_list, get_nil_irep());
2200  catch_pop.set(ID_label, get_nil_irep());
2201  end_try_block.move_to_operands(c);
2202  end_try_block.move_to_operands(catch_pop);
2203  c=end_try_block;
2204  }
2205  }
2206  }
2207 
2208  if(!i_it->source_location.get_line().empty())
2209  c.add_source_location()=i_it->source_location;
2210 
2211  push(results);
2212 
2213  a_it->second.done=true;
2214  for(const unsigned address : a_it->second.successors)
2215  {
2216  address_mapt::iterator a_it2=address_map.find(address);
2217  assert(a_it2!=address_map.end());
2218 
2219  // we don't worry about exception handlers as we don't load the
2220  // operands from the stack anyway -- we keep explicit global
2221  // exception variables
2222  for(const auto &exception_row : method.exception_table)
2223  {
2224  if(address==exception_row.handler_pc)
2225  {
2226  stack.clear();
2227  break;
2228  }
2229  }
2230 
2231  if(!stack.empty() && a_it2->second.predecessors.size()>1)
2232  {
2233  // copy into temporaries
2234  code_blockt more_code;
2235 
2236  // introduce temporaries when successor is seen for the first
2237  // time
2238  if(a_it2->second.stack.empty())
2239  {
2240  for(stackt::iterator s_it=stack.begin();
2241  s_it!=stack.end();
2242  ++s_it)
2243  {
2244  symbol_exprt lhs=tmp_variable("$stack", s_it->type());
2245  code_assignt a(lhs, *s_it);
2246  more_code.copy_to_operands(a);
2247 
2248  s_it->swap(lhs);
2249  }
2250  }
2251  else
2252  {
2253  assert(a_it2->second.stack.size()==stack.size());
2254  stackt::const_iterator os_it=a_it2->second.stack.begin();
2255  for(auto &expr : stack)
2256  {
2257  assert(has_prefix(os_it->get_string(ID_C_base_name), "$stack"));
2258  symbol_exprt lhs=to_symbol_expr(*os_it);
2259  code_assignt a(lhs, expr);
2260  more_code.copy_to_operands(a);
2261 
2262  expr.swap(lhs);
2263  ++os_it;
2264  }
2265  }
2266 
2267  if(results.empty())
2268  {
2269  more_code.copy_to_operands(c);
2270  c.swap(more_code);
2271  }
2272  else
2273  {
2274  c.make_block();
2275  auto &last_statement=to_code_block(c).find_last_statement();
2276  if(last_statement.get_statement()==ID_goto)
2277  {
2278  // Insert stack twiddling before branch:
2279  last_statement.make_block();
2280  last_statement.operands().insert(
2281  last_statement.operands().begin(),
2282  more_code.operands().begin(),
2283  more_code.operands().end());
2284  }
2285  else
2286  forall_operands(o_it, more_code)
2287  c.copy_to_operands(*o_it);
2288  }
2289  }
2290 
2291  a_it2->second.stack=stack;
2292  }
2293  }
2294 
2295  code_blockt code;
2296 
2297  // Add anonymous locals to the symtab:
2298  for(const auto &var : used_local_names)
2299  {
2300  symbolt new_symbol;
2301  new_symbol.name=var.get_identifier();
2302  new_symbol.type=var.type();
2303  new_symbol.base_name=var.get(ID_C_base_name);
2304  new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier());
2305  new_symbol.mode=ID_java;
2306  new_symbol.is_type=false;
2307  new_symbol.is_file_local=true;
2308  new_symbol.is_thread_local=true;
2309  new_symbol.is_lvalue=true;
2310  symbol_table.add(new_symbol);
2311  }
2312 
2313  // Try to recover block structure as indicated in the local variable table:
2314 
2315  // The block tree node mirrors the block structure of root_block,
2316  // indexing the Java PCs where each subblock starts and ends.
2317  block_tree_nodet root;
2318  code_blockt root_block;
2319 
2320  // First create a simple flat list of basic blocks. We'll add lexical nesting
2321  // constructs as variable live-ranges require next.
2322  bool start_new_block=true;
2323  bool has_seen_previous_address=false;
2324  unsigned previous_address=0;
2325  for(const auto &address_pair : address_map)
2326  {
2327  const unsigned address=address_pair.first;
2328  assert(address_pair.first==address_pair.second.source->address);
2329  const codet &c=address_pair.second.code;
2330 
2331  // Start a new lexical block if this is a branch target:
2332  if(!start_new_block)
2333  start_new_block=targets.find(address)!=targets.end();
2334  // Start a new lexical block if this is a control flow join
2335  // (e.g. due to exceptional control flow)
2336  if(!start_new_block)
2337  start_new_block=address_pair.second.predecessors.size()>1;
2338  // Start a new lexical block if we've just entered a try block
2339  if(!start_new_block && has_seen_previous_address)
2340  {
2341  for(const auto &exception_row : method.exception_table)
2342  if(exception_row.start_pc==previous_address)
2343  {
2344  start_new_block=true;
2345  break;
2346  }
2347  }
2348 
2349  if(start_new_block)
2350  {
2351  code_labelt newlabel(label(std::to_string(address)), code_blockt());
2352  root_block.move_to_operands(newlabel);
2353  root.branch.push_back(block_tree_nodet::get_leaf());
2354  assert((root.branch_addresses.empty() ||
2355  root.branch_addresses.back()<address) &&
2356  "Block addresses should be unique and increasing");
2357  root.branch_addresses.push_back(address);
2358  }
2359 
2360  if(c.get_statement()!=ID_skip)
2361  {
2362  auto &lastlabel=to_code_label(to_code(root_block.operands().back()));
2363  auto &add_to_block=to_code_block(lastlabel.code());
2364  add_to_block.add(c);
2365  }
2366  start_new_block=address_pair.second.successors.size()>1;
2367 
2368  previous_address=address;
2369  has_seen_previous_address=true;
2370  }
2371 
2372  // Find out where temporaries are used:
2373  std::map<irep_idt, variablet> temporary_variable_live_ranges;
2374  for(const auto &aentry : address_map)
2376  aentry.first,
2377  aentry.second.code,
2378  temporary_variable_live_ranges);
2379 
2380  std::vector<const variablet*> vars_to_process;
2381  for(const auto &vlist : variables)
2382  for(const auto &v : vlist)
2383  vars_to_process.push_back(&v);
2384 
2385  for(const auto &v : tmp_vars)
2386  vars_to_process.push_back(
2387  &temporary_variable_live_ranges.at(v.get_identifier()));
2388 
2389  for(const auto &v : used_local_names)
2390  vars_to_process.push_back(
2391  &temporary_variable_live_ranges.at(v.get_identifier()));
2392 
2393  for(const auto vp : vars_to_process)
2394  {
2395  const auto &v=*vp;
2396  if(v.is_parameter)
2397  continue;
2398  // Merge lexical scopes as far as possible to allow us to
2399  // declare these variable scopes faithfully.
2400  // Don't insert yet, as for the time being the blocks' only
2401  // operands must be other blocks.
2402  // The declarations will be inserted in the next pass instead.
2404  root,
2405  root_block,
2406  v.start_pc,
2407  v.start_pc+v.length,
2408  std::numeric_limits<unsigned>::max(),
2409  address_map);
2410  }
2411  for(const auto vp : vars_to_process)
2412  {
2413  const auto &v=*vp;
2414  if(v.is_parameter)
2415  continue;
2416  // Skip anonymous variables:
2417  if(v.symbol_expr.get_identifier().empty())
2418  continue;
2419  auto &block=get_block_for_pcrange(
2420  root,
2421  root_block,
2422  v.start_pc,
2423  v.start_pc+v.length,
2424  std::numeric_limits<unsigned>::max());
2425  code_declt d(v.symbol_expr);
2426  block.operands().insert(block.operands().begin(), d);
2427  }
2428 
2429  for(auto &block : root_block.operands())
2430  code.move_to_operands(block);
2431 
2432  return code;
2433 }
2434 
2436  const symbolt &class_symbol,
2437  const java_bytecode_parse_treet::methodt &method,
2438  symbol_tablet &symbol_table,
2439  message_handlert &message_handler,
2440  size_t max_array_length,
2441  safe_pointer<ci_lazy_methodst> lazy_methods,
2442  const character_refine_preprocesst &character_refine)
2443 {
2445  symbol_table,
2446  message_handler,
2447  max_array_length,
2448  lazy_methods,
2449  character_refine);
2450 
2451  java_bytecode_convert_method(class_symbol, method);
2452 }
2453 
2457  const std::string &tmp_var_prefix,
2458  const typet &tmp_var_type,
2459  code_blockt &block,
2460  const bytecode_write_typet write_type,
2461  const irep_idt &identifier)
2462 {
2463  for(auto &stack_entry : stack)
2464  {
2465  // remove typecasts if existing
2466  while(stack_entry.id()==ID_typecast)
2467  stack_entry=to_typecast_expr(stack_entry).op();
2468 
2469  // variables or static fields and symbol -> save symbols with same id
2470  if((write_type==bytecode_write_typet::VARIABLE ||
2471  write_type==bytecode_write_typet::STATIC_FIELD) &&
2472  stack_entry.id()==ID_symbol)
2473  {
2474  const symbol_exprt &var=to_symbol_expr(stack_entry);
2475  if(var.get_identifier()==identifier)
2476  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
2477  }
2478 
2479  // array reference and dereference -> save all references on the stack
2480  else if(write_type==bytecode_write_typet::ARRAY_REF &&
2481  stack_entry.id()==ID_dereference)
2482  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
2483 
2484  // field and member access -> compare component name
2485  else if(write_type==bytecode_write_typet::FIELD &&
2486  stack_entry.id()==ID_member)
2487  {
2488  const irep_idt &entry_id=
2489  to_member_expr(stack_entry).get_component_name();
2490  if(entry_id==identifier)
2491  create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
2492  }
2493  }
2494 }
2495 
2498  const std::string &tmp_var_prefix,
2499  const typet &tmp_var_type,
2500  code_blockt &block,
2501  exprt &stack_entry)
2502 {
2503  const exprt tmp_var=
2504  tmp_variable(tmp_var_prefix, tmp_var_type);
2505  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
2506  stack_entry=tmp_var;
2507 }
#define loc()
The void type.
Definition: std_types.h:63
const irept & get_nil_irep()
Definition: irep.cpp:56
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
const irep_idt & get_statement() const
Definition: std_code.h:37
A side effect that pushes/pops a catch handler.
Definition: std_code.h:1130
const irep_idt & get_name() const
Definition: std_types.h:179
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const codet & then_case() const
Definition: std_code.h:370
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
mstreamt & result()
Definition: message.h:233
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)
This creates a method symbol in the symtab, but doesn&#39;t actually perform method conversion just yet...
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
void set_function(const irep_idt &function)
semantic type conversion
Definition: std_expr.h:1725
static int8_t r
Definition: irep_hash.h:59
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
JAVA Bytecode Language Conversion.
A ‘switch’ instruction.
Definition: std_code.h:412
Base type of functions.
Definition: std_types.h:734
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert(const symbolt &class_symbol, const methodt &)
bool is_thread_local
Definition: symbol.h:70
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void set_label(const irep_idt &label)
Definition: std_code.h:787
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:163
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
boolean OR
Definition: std_expr.h:1968
typet java_boolean_type()
Definition: java_types.cpp:59
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:186
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)
Control Flow Graph.
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
static void gather_symbol_live_ranges(unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
irep_idt mode
Language mode.
Definition: symbol.h:55
const exprt & cond() const
Definition: std_code.h:360
codet & code()
Definition: std_code.h:851
void from_expr(const constant_exprt &expr)
safe_pointer< ci_lazy_methodst > 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:67
typet java_int_type()
Definition: java_types.cpp:19
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:194
void set_comment(const irep_idt &comment)
void set_name(const irep_idt &name)
Definition: std_types.h:184
irep_idt label(const irep_idt &address)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
struct bytecode_infot const bytecode_info[]
The null pointer constant.
Definition: std_expr.h:3774
literalt pos(literalt a)
Definition: literal.h:193
std::vector< parametert > parameterst
Definition: std_types.h:829
exprt value
Initial value of symbol.
Definition: symbol.h:40
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initialisers_for_slot above for more detail.
The trinary if-then-else operator.
Definition: std_expr.h:2771
character_refine_preprocesst character_preprocess
A ‘goto’ instruction.
Definition: std_code.h:613
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
bool operator==(const irep_idt &what) const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
std::map< unsigned, converted_instructiont > address_mapt
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:77
exprt & op()
Definition: std_expr.h:1739
An expression statement.
Definition: std_code.h:957
expanding_vectort< variablest > variables
void set_default()
Definition: std_code.h:836
A side effect that throws an exception.
Definition: std_code.h:1100
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
bool is_static_lifetime
Definition: symbol.h:70
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:202
const exprt & case_op() const
Definition: std_code.h:841
subt & get_sub()
Definition: irep.h:245
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 ...
static irep_idt strip_java_namespace_prefix(const irep_idt to_strip)
void set_base_name(const irep_idt &name)
Definition: std_types.h:777
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
Extract member of struct or union.
Definition: std_expr.h:3214
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
equality
Definition: std_expr.h:1082
const irep_idt & get_base_name() const
Definition: std_types.h:189
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition: arith_tools.cpp:95
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
const irep_idt & id() const
Definition: irep.h:189
bool is_constructor(const class_typet::methodt &method)
exprt & lhs()
Definition: std_code.h:157
Bit-wise OR.
Definition: std_expr.h:2087
void add(const codet &code)
Definition: std_code.h:81
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
typet java_type_from_string(const std::string &src)
Definition: java_types.cpp:152
class code_blockt & make_block()
Definition: std_code.cpp:24
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
division (integer and real)
Definition: std_expr.h:854
A reference into the symbol table.
Definition: std_types.h:109
A declaration of a local variable.
Definition: std_code.h:192
The NIL expression.
Definition: std_expr.h:3764
The pointer type.
Definition: std_types.h:1343
exprt & rhs()
Definition: std_code.h:162
The empty type.
Definition: std_types.h:53
codet & code()
Definition: std_code.h:792
Operator to dereference a pointer.
Definition: std_expr.h:2701
typet java_type_from_char(char t)
Definition: java_types.cpp:111
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:636
API to expression classes.
patternt(const char *_p)
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
TO_BE_DOCUMENTED.
Definition: namespace.h:62
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible, returns the same code otherwise.
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
Left shift.
Definition: std_expr.h:2301
A label for branch targets.
Definition: std_code.h:760
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
static unsigned get_bytecode_type_width(const typet &ty)
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
typet java_byte_type()
Definition: java_types.cpp:39
size_t size() const
Definition: dstring.h:77
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Logical right shift.
Definition: std_expr.h:2341
codet & find_last_statement()
Definition: std_code.h:94
Operator to return the address of an object.
Definition: std_expr.h:2593
The unary minus expression.
Definition: std_expr.h:346
typet java_short_type()
Definition: java_types.cpp:34
The boolean constant false.
Definition: std_expr.h:3753
exprt::operandst pop(std::size_t n)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
binary multiplication
Definition: std_expr.h:806
The reference type.
Definition: std_types.h:1394
void branch(symbol_tablet &symbol_table, goto_functionst &goto_functions, const irep_idt &id)
Definition: branch.cpp:19
An assertion.
Definition: std_code.h:312
An assumption.
Definition: std_code.h:274
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
codet convert_instructions(const methodt &, const code_typet &)
Bit-wise XOR.
Definition: std_expr.h:2134
static size_t count_slots(const size_t value, const code_typet::parametert &param)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
static size_t get_variable_slots(const code_typet::parametert &param)
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
const char * mnemonic
Definition: bytecode_info.h:46
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
bool has_this() const
Definition: std_types.h:808
irep_idt get_component_name() const
Definition: std_expr.h:3249
bool is_file_local
Definition: symbol.h:71
remainder of division
Definition: std_expr.h:946
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
create temporary variables if a write instruction can have undesired side- effects ...
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
void from_integer(const mp_integer &i)
Definition: ieee_float.cpp:508
void swap(irept &irep)
Definition: irep.h:231
const size_t SLOTS_PER_INTEGER(1u)
mstreamt & error()
Definition: message.h:223
void push(const exprt::operandst &o)
unsigned int get_unsigned_int(const irep_namet &name) const
Definition: irep.cpp:250
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
binary minus
Definition: std_expr.h:758
Skip.
Definition: std_code.h:134
Bit-wise AND.
Definition: std_expr.h:2180
An if-then-else.
Definition: std_code.h:350
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:130
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
A switch-case.
Definition: std_code.h:817
A statement in a programming language.
Definition: std_code.h:19
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:546
Return from a function.
Definition: std_code.h:714
Arithmetic right shift.
Definition: std_expr.h:2321
const size_t INTEGER_WIDTH(64u)
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
bool is_type
Definition: symbol.h:66
typet java_char_type()
Definition: java_types.cpp:44
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
JAVA Bytecode Language Conversion.
const typet & subtype() const
Definition: type.h:31
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:252
An expression containing a side effect.
Definition: std_code.h:997
Compute dominators for CFG of goto_function.
operandst & operands()
Definition: expr.h:70
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;.
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:90
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
const typet & return_type() const
Definition: std_types.h:831
binary modulo
Definition: std_expr.h:902
Assignment.
Definition: std_code.h:144
char java_char_from_type(const typet &type)
Definition: java_types.cpp:252
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
codet get_array_bounds_check(const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc)
IEEE-floating-point equality.
Definition: std_expr.h:3497
bool is_lvalue
Definition: symbol.h:71