cprover
java_local_variable_table.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java local variable table processing
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include "java_types.h"
15 #include "java_utils.h"
16 
17 #include <util/arith_tools.h>
18 #include <util/invariant.h>
19 #include <util/string2int.h>
20 
21 #include <climits>
22 #include <iostream>
23 
24 // Specialise the CFG representation to work over Java instead of GOTO programs.
25 // This must be done at global scope due to template resolution rules.
26 
27 template <class T>
29  T,
32  : public grapht<
33  cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
34 {
35  typedef grapht<
38  typedef typename base_grapht::nodet nodet;
43  typedef std::size_t entryt;
45 
47 
48  void operator()(const method_with_amapt &args)
49  {
50  const auto &method=args.first;
51  const auto &amap=args.second;
52  for(const auto &inst : amap)
53  {
54  // Map instruction PCs onto node indices:
55  entry_map[inst.first]=this->add_node();
56  // Map back:
57  (*this)[entry_map[inst.first]].PC=inst.first;
58  }
59  // Add edges declared in the address map:
60  for(const auto &inst : amap)
61  {
62  for(auto succ : inst.second.successors)
63  this->add_edge(entry_map.at(inst.first), entry_map.at(succ));
64  }
65  // Next, add edges declared in the exception table, which
66  // don't figure in the address map successors/predecessors as yet:
67  for(const auto &table_entry : method.exception_table)
68  {
69  auto findit=amap.find(table_entry.start_pc);
70  INVARIANT(
71  findit!=amap.end(),
72  "Exception table entry doesn't point to an instruction?");
73  for(; findit->first<table_entry.end_pc; ++findit)
74  {
75  // For now just assume any non-branch
76  // instruction could potentially throw.
77  auto succit=findit;
78  ++succit;
79  if(succit==amap.end())
80  continue;
81  const auto &thisinst=findit->second;
82  if(thisinst.successors.size()==1 &&
83  thisinst.successors.back()==succit->first)
84  {
85  this->add_edge(
86  entry_map.at(findit->first),
87  entry_map.at(table_entry.handler_pc));
88  }
89  }
90  }
91  }
92 
94  const java_bytecode_convert_methodt::method_offsett &instruction) const
95  {
96  return entry_map.at(instruction);
97  }
98 
99  nodet &
101  {
102  return (*this)[get_node_index(instruction)];
103  }
104  const nodet &get_node(
105  const java_bytecode_convert_methodt::method_offsett &instruction) const
106  {
107  return (*this)[get_node_index(instruction)];
108  }
109 
112  {
113  return args.second.begin()->first;
114  }
115 
118  {
119  return (--args.second.end())->first;
120  }
121 
122  static bool nodes_empty(const method_with_amapt &args)
123  {
124  return args.second.empty();
125  }
126 };
127 
128 // Grab some class typedefs for brevity:
139 
140 // Comparators for local variables:
141 
142 static bool lt_index(
145 {
146  return a.var.index<b.var.index;
147 }
148 static bool lt_startpc(
151 {
152  return a->var.start_pc<b->var.start_pc;
153 }
154 
155 // The predecessor map, and a top-sorting comparator:
156 
157 typedef std::map<
159  std::set<local_variable_with_holest *> >
161 
163 {
165 
166  explicit is_predecessor_oft(const predecessor_mapt &_order) : order(_order) {}
167 
171  {
172  auto findit=order.find(a);
173  if(findit==order.end())
174  return false;
175  return findit->second.count(b)>0;
176  }
177 };
178 
179 // Helper routines for the find-initializers code below:
180 
188  const predecessor_mapt &predecessor_map,
189  std::set<local_variable_with_holest*> &result)
190 {
191  if(!result.insert(start).second)
192  return;
193  auto findit=predecessor_map.find(start);
194  if(findit==predecessor_map.end())
195  return;
196  for(const auto pred : findit->second)
197  gather_transitive_predecessors(pred, predecessor_map, result);
198 }
199 
205 static bool is_store_to_slot(
207  unsigned slotidx)
208 {
209  const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic;
210 
211  if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
212  return false;
213 
214  unsigned storeslotidx;
215  if(inst.args.size()==1)
216  {
217  // Store with an argument:
218  const auto &arg=inst.args[0];
219  storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
220  }
221  else
222  {
223  // Store shorthands, like "store_0", "store_1"
224  INVARIANT(
225  prevstatement[6]=='_' && prevstatement.size()==8,
226  "expected store instruction looks like store_0, store_1...");
227  std::string storeslot(1, prevstatement[7]);
228  INVARIANT(
229  isdigit(storeslot[0]),
230  "store_? instructions should end in a digit");
231  storeslotidx=safe_string2unsigned(storeslot);
232  }
233  return storeslotidx==slotidx;
234 }
235 
240 static void maybe_add_hole(
244 {
245  PRECONDITION(to>=from);
246  if(to!=from)
247  var.holes.push_back(
248  {from,
249  static_cast<java_bytecode_convert_methodt::method_offsett>(to - from)});
250 }
251 
260  local_variable_table_with_holest::iterator firstvar,
261  local_variable_table_with_holest::iterator varlimit,
262  std::vector<local_variable_with_holest *> &live_variable_at_address)
263 {
264  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
265  {
266  if(it->var.start_pc+it->var.length>live_variable_at_address.size())
267  live_variable_at_address.resize(it->var.start_pc+it->var.length);
268 
269  for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
270  idx != idxlim;
271  ++idx)
272  {
273  INVARIANT(!live_variable_at_address[idx], "Local variable table clash?");
274  live_variable_at_address[idx]=&*it;
275  }
276  }
277 }
278 
305  local_variable_table_with_holest::iterator firstvar,
306  local_variable_table_with_holest::iterator varlimit,
307  const std::vector<local_variable_with_holest *> &live_variable_at_address,
308  const address_mapt &amap,
309  predecessor_mapt &predecessor_map,
310  message_handlert &msg_handler)
311 {
312  messaget msg(msg_handler);
313  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
314  {
315  // All entries of the "local_variable_table_with_holest" processed in this
316  // function concern the same Java Local Variable Table slot/register. This
317  // is because "find_initializers()" has already sorted them.
318  INVARIANT(
319  it->var.index==firstvar->var.index,
320  "all entries are for the same local variable slot");
321 
322  // Parameters are irrelevant to us and shouldn't be changed. This is because
323  // they cannot have live predecessor ranges: they are initialized by the JVM
324  // and no other live variable range can flow into them.
325  if(it->is_parameter)
326  continue;
327 
328 #ifdef DEBUG
329  msg.debug() << "jcm: ppm: processing var idx " << it->var.index
330  << " name '" << it->var.name << "' start-pc "
331  << it->var.start_pc << " len " << it->var.length
332  << "; holes " << it->holes.size() << messaget::eom;
333 #endif
334 
335  // Find the last instruction within the live range:
336  const auto end_pc = it->var.start_pc + it->var.length;
337  auto amapit=amap.find(end_pc);
338  INVARIANT(
339  amapit!=amap.begin(),
340  "current bytecode shall not be the first");
341  auto old_amapit=amapit;
342  --amapit;
343  if(old_amapit==amap.end())
344  {
345  INVARIANT(
346  end_pc>amapit->first,
347  "Instruction live range doesn't align to instruction boundary?");
348  }
349 
350  // Find vartable entries that flow into this one. For unknown reasons this
351  // loop iterates backwards, walking back from the last bytecode in the live
352  // range of variable it to the first one. For each value of the iterator
353  // "amapit" we search for instructions that jump into amapit's address
354  // (predecessors)
355  auto new_start_pc = it->var.start_pc;
356  for(; amapit->first>=it->var.start_pc; --amapit)
357  {
358  for(auto pred : amapit->second.predecessors)
359  {
360  // pred is the address (byecode offset) of a instruction that jumps into
361  // amapit. Compute now a pointer to the variable-with-holes whose index
362  // equals that of amapit and which was alive on instruction pred, or a
363  // null pointer if no such variable exists (e.g., because no live range
364  // covers that instruction)
365  auto pred_var=
366  (pred<live_variable_at_address.size() ?
367  live_variable_at_address[pred] :
368  nullptr);
369 
370  // Three cases are now possible:
371  // 1. The predecessor instruction is in the same live range: nothing to
372  // do.
373  if(pred_var==&*it)
374  {
375  continue;
376  }
377  // 2. The predecessor instruction is in no live range among those for
378  // variable slot it->var.index
379  else if(!pred_var)
380  {
381  // Check if this is an initializer, and if so expand the live range
382  // to include it, but don't check its predecessors:
383  auto inst_before_this=amapit;
384  INVARIANT(
385  inst_before_this!=amap.begin(),
386  "we shall not be on the first bytecode of the method");
387  --inst_before_this;
388  if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
389  {
390  // These sorts of infeasible edges can occur because jsr
391  // handling is presently vague (any subroutine is assumed to
392  // be able to return to any callsite)
393  msg.warning() << "Local variable table: ignoring flow from "
394  << "out of range for " << it->var.name << ' '
395  << pred << " -> " << amapit->first
396  << messaget::eom;
397  continue;
398  }
399  if(!is_store_to_slot(
400  *(inst_before_this->second.source),
401  it->var.index))
402  {
403  msg.warning() << "Local variable table: didn't find initializing "
404  << "store for predecessor of bytecode at address "
405  << amapit->first << " ("
406  << amapit->second.predecessors.size()
407  << " predecessors)" << msg.eom;
408  throw "local variable table: unexpected live ranges";
409  }
410  new_start_pc=pred;
411  }
412  // 3. Predecessor instruction is a different range associated to the
413  // same variable slot
414  else
415  {
416  if(pred_var->var.name!=it->var.name ||
417  pred_var->var.descriptor!=it->var.descriptor)
418  {
419  // These sorts of infeasible edges can occur because
420  // jsr handling is presently vague (any subroutine is
421  // assumed to be able to return to any callsite)
422  msg.warning() << "Local variable table: ignoring flow from "
423  << "clashing variable for "
424  << it->var.name << ' ' << pred << " -> "
425  << amapit->first << messaget::eom;
426  continue;
427  }
428  // OK, this is a flow from a similar but
429  // distinct entry in the local var table.
430  predecessor_map[&*it].insert(pred_var);
431  }
432  }
433  }
434 
435  // If a simple pre-block initializer was found,
436  // add it to the live range now:
437  it->var.length+=(it->var.start_pc-new_start_pc);
438  it->var.start_pc=new_start_pc;
439  }
440 }
441 
450  const std::set<local_variable_with_holest *> &merge_vars,
451  const java_cfg_dominatorst &dominator_analysis)
452 {
453  PRECONDITION(!merge_vars.empty());
454 
455  auto first_pc =
456  std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
457  for(auto v : merge_vars)
458  {
459  if(v->var.start_pc<first_pc)
460  first_pc=v->var.start_pc;
461  }
462 
463  std::vector<java_bytecode_convert_methodt::method_offsett>
464  candidate_dominators;
465  for(auto v : merge_vars)
466  {
467  const auto &dominator_nodeidx=
468  dominator_analysis.cfg.entry_map.at(v->var.start_pc);
469  const auto &this_var_doms=
470  dominator_analysis.cfg[dominator_nodeidx].dominators;
471  for(const auto this_var_dom : this_var_doms)
472  if(this_var_dom<=first_pc)
473  candidate_dominators.push_back(this_var_dom);
474  }
475  std::sort(candidate_dominators.begin(), candidate_dominators.end());
476 
477  // Working from the back, simply find the first PC
478  // that occurs merge_vars.size() times and therefore
479  // dominates all vars we seek to merge:
480  for(auto domit=candidate_dominators.rbegin(),
481  domitend=candidate_dominators.rend();
482  domit!=domitend;
483  /* Don't increment here */)
484  {
485  std::size_t repeats = 0;
486  auto dom=*domit;
487  while(domit!=domitend && *domit==dom)
488  {
489  ++domit;
490  ++repeats;
491  }
492  assert(repeats<=merge_vars.size());
493  if(repeats==merge_vars.size())
494  return dom;
495  }
496 
497  throw "variable live ranges with no common dominator?";
498 }
499 
509  local_variable_with_holest &merge_into,
510  const std::set<local_variable_with_holest *> &merge_vars,
511  java_bytecode_convert_methodt::method_offsett expanded_live_range_start)
512 {
513  std::vector<local_variable_with_holest *> sorted_by_startpc(
514  merge_vars.begin(), merge_vars.end());
515  std::sort(sorted_by_startpc.begin(), sorted_by_startpc.end(), lt_startpc);
516 
518  merge_into,
519  expanded_live_range_start,
520  sorted_by_startpc[0]->var.start_pc);
522  idx < sorted_by_startpc.size() - 1;
523  ++idx)
524  {
526  merge_into,
527  sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->var.length,
528  sorted_by_startpc[idx+1]->var.start_pc);
529  }
530 }
531 
541  local_variable_with_holest &merge_into,
542  const std::set<local_variable_with_holest *> &merge_vars,
543  const java_cfg_dominatorst &dominator_analysis,
544  std::ostream &debug_out)
545 {
546  // Because we need a lexically-scoped declaration,
547  // we must have the merged variable
548  // enter scope both in a block that dominates all entries, and which
549  // precedes them in program order.
550  const auto found_dominator =
551  get_common_dominator(merge_vars, dominator_analysis);
552 
553  // Populate the holes in the live range
554  // (addresses where the new variable will be in scope,
555  // but references to this stack slot should not resolve to it
556  // as it was not visible in the original local variable table)
557  populate_live_range_holes(merge_into, merge_vars, found_dominator);
558 
560  for(auto v : merge_vars)
561  {
562  if(v->var.start_pc+v->var.length>last_pc)
563  last_pc=v->var.start_pc+v->var.length;
564  }
565 
566  // Apply the changes:
567  merge_into.var.start_pc=found_dominator;
568  merge_into.var.length=last_pc-found_dominator;
569 
570 #ifdef DEBUG
571  debug_out << "Merged " << merge_vars.size() << " variables named "
572  << merge_into.var.name << "; new live range "
573  << merge_into.var.start_pc << '-'
574  << merge_into.var.start_pc + merge_into.var.length << '\n';
575 #else
576  (void)debug_out; // unused parameter
577 #endif
578 
579  // Nuke the now-subsumed var-table entries:
580  for(auto &v : merge_vars)
581  if(v!=&merge_into)
582  v->var.length=0;
583 }
584 
599  local_variable_table_with_holest::iterator firstvar,
600  local_variable_table_with_holest::iterator varlimit,
601  const address_mapt &amap,
602  const java_cfg_dominatorst &dominator_analysis)
603 {
604  // Build a simple map from instruction PC to the variable
605  // live in this slot at that PC, and a map from each variable
606  // to variables that flow into it:
607  std::vector<local_variable_with_holest *> live_variable_at_address;
608  populate_variable_address_map(firstvar, varlimit, live_variable_at_address);
609 
610  // Now find variables that flow together by
611  // walking backwards to find initializers
612  // or branches from other live ranges:
613  predecessor_mapt predecessor_map;
615  firstvar,
616  varlimit,
617  live_variable_at_address,
618  amap,
619  predecessor_map,
621 
622  // OK, we've established the flows all seem sensible.
623  // Now merge vartable entries according to the predecessor_map:
624 
625  // Take the transitive closure of the predecessor map:
626  for(auto &kv : predecessor_map)
627  {
628  std::set<local_variable_with_holest *> closed_preds;
629  gather_transitive_predecessors(kv.first, predecessor_map, closed_preds);
630  kv.second=std::move(closed_preds);
631  }
632 
633  // Top-sort so that we get the bottom variables first:
634  is_predecessor_oft comp(predecessor_map);
635  std::vector<local_variable_with_holest *> topsorted_vars;
636  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
637  topsorted_vars.push_back(&*it);
638 
639  std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);
640 
641  // Now merge the entries:
642  for(auto merge_into : topsorted_vars)
643  {
644  // Already merged into another variable?
645  if(merge_into->var.length==0)
646  continue;
647 
648  auto findit=predecessor_map.find(merge_into);
649  // Nothing to do?
650  if(findit==predecessor_map.end())
651  continue;
652 
653  const auto &merge_vars=findit->second;
654  INVARIANT(merge_vars.size()>=2, "merging requires at least 2 variables");
655 
657  *merge_into, merge_vars, dominator_analysis, log.status());
658  }
659 }
660 
668 static void walk_to_next_index(
669  local_variable_table_with_holest::iterator &it1,
670  local_variable_table_with_holest::iterator &it2,
671  local_variable_table_with_holest::iterator itend)
672 {
673  if(it2==itend)
674  {
675  it1=itend;
676  return;
677  }
678 
679  auto old_it2=it2;
680  auto index=it2->var.index;
681  while(it2!=itend && it2->var.index==index)
682  ++it2;
683  it1=old_it2;
684 }
685 
694  const address_mapt &amap,
695  const java_cfg_dominatorst &dominator_analysis)
696 {
697  // Sort table entries by local slot index:
698  std::sort(vars.begin(), vars.end(), lt_index);
699 
700  // For each block of entries using a particular index,
701  // try to combine them:
702  auto it1=vars.begin();
703  auto it2=it1;
704  auto itend=vars.end();
705  walk_to_next_index(it1, it2, itend);
706  for(; it1!=itend; walk_to_next_index(it1, it2, itend))
707  find_initializers_for_slot(it1, it2, amap, dominator_analysis);
708 }
709 
713 static void cleanup_var_table(
714  std::vector<local_variable_with_holest> &vars_with_holes)
715 {
716  size_t toremove=0;
717  for(size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
718  {
719  auto &v=vars_with_holes[i];
720  if(v.var.length==0)
721  {
722  // Move to end; consider the new element we've swapped in:
723  ++toremove;
724  if(i!=vars_with_holes.size()-toremove) // Already where it needs to be?
725  std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
726  --i; // May make i (size_t)-1, but it will immediately be
727  // re-incremented as the loop iterates.
728  }
729  }
730 
731  // Remove un-needed entries.
732  vars_with_holes.resize(vars_with_holes.size()-toremove);
733 }
734 
742  const methodt &m,
743  const address_mapt &amap)
744 {
745  // Compute CFG dominator tree
746  java_cfg_dominatorst dominator_analysis;
747  method_with_amapt dominator_args(m, amap);
748  dominator_analysis(dominator_args);
749 
750 #ifdef DEBUG
751  log.debug() << "jcm: setup-local-vars: m.is_static " << m.is_static
752  << " m.descriptor " << m.descriptor << messaget::eom;
753  log.debug() << "jcm: setup-local-vars: lv arg slots " << slots_for_parameters
754  << messaget::eom;
755  log.debug() << "jcm: setup-local-vars: lvt size "
756  << m.local_variable_table.size() << messaget::eom;
757 #endif
758 
759  // Find out which local variable table entries should be merged:
760  // Wrap each entry so we have a data structure to work during function calls,
761  // where we record live ranges with holes:
762  std::vector<local_variable_with_holest> vars_with_holes;
763  for(const auto &v : m.local_variable_table)
764  vars_with_holes.push_back({v, is_parameter(v), {}});
765 
766  // Merge variable records. See documentation of in
767  // `find_initializers_for_slot` for more details. If the strategy employed
768  // there fails with an exception, we just ignore the LVT for this method, no
769  // variable is generated in `this->variables[]` (because we return here and
770  // dont let the for loop below to execute), and as a result the method
771  // this->variable() will be forced to create new `anonlocal::` variables, as
772  // the only source of variable names for that method is `this->variables[]`.
773  try
774  {
775  find_initializers(vars_with_holes, amap, dominator_analysis);
776  }
777  catch(const char *message)
778  {
779  log.warning() << "Bytecode -> codet translation error: " << message
780  << messaget::eom
781  << "This is probably due to an unexpected LVT, "
782  << "falling back to translation without LVT" << messaget::eom;
783  return;
784  }
785 
786  // Clean up removed records from the variable table:
787  cleanup_var_table(vars_with_holes);
788 
789  // Do the locals and parameters in the variable table, which is available when
790  // compiled with -g or for methods with many local variables in the latter
791  // case, different variables can have the same index, depending on the
792  // context.
793  //
794  // to calculate which variable to use, one uses the address of the instruction
795  // that uses the variable, the size of the instruction and the start_pc /
796  // length values in the local variable table
797  for(auto &v : vars_with_holes)
798  {
799  if(v.is_parameter)
800  continue;
801 
802 #ifdef DEBUG
803  log.debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index
804  << " name " << v.var.name << " v.var.descriptor '"
805  << v.var.descriptor << "' holes " << v.holes.size()
806  << messaget::eom;
807 #endif
808 
809  const std::string &method_name = id2string(method_id);
810  const size_t method_name_end = method_name.rfind(":(");
811  const size_t class_name_end = method_name.rfind('.', method_name_end);
812  INVARIANT(
813  method_name_end != std::string::npos &&
814  class_name_end != std::string::npos,
815  "A method name has the format class `.` method `:(`signature`)`.");
816  const std::string class_name = method_name.substr(0, class_name_end);
817 
818  const typet t = v.var.signature.has_value()
820  v.var.descriptor, v.var.signature, class_name)
821  : *java_type_from_string(v.var.descriptor);
822 
823  std::ostringstream id_oss;
824  id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;
825  irep_idt identifier(id_oss.str());
826  symbol_exprt result(identifier, t);
827  result.set(ID_C_base_name, v.var.name);
828 
829  // Create a new local variable in the variables[] array, the result of
830  // merging multiple local variables with equal name (parameters excluded)
831  // into a single local variable with holes
832  variables[v.var.index].emplace_back(
833  result, v.var.start_pc, v.var.length, false, std::move(v.holes));
834 
835  // Register the local variable in the symbol table
836  symbolt new_symbol;
837  new_symbol.name=identifier;
838  new_symbol.type=t;
839  new_symbol.base_name=v.var.name;
840  new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
841  new_symbol.mode=ID_java;
842  new_symbol.is_type=false;
843  new_symbol.is_file_local=true;
844  new_symbol.is_thread_local=true;
845  new_symbol.is_lvalue=true;
846  symbol_table.add(new_symbol);
847  }
848 }
849 
858  size_t address,
859  variablest &var_list)
860 {
861  for(const variablet &var : var_list)
862  {
863  size_t start_pc=var.start_pc;
864  size_t length=var.length;
865  if(address>=start_pc && address<(start_pc+length))
866  {
867  bool found_hole=false;
868  for(auto &hole : var.holes)
869  if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
870  {
871  found_hole=true;
872  break;
873  }
874  if(found_hole)
875  continue;
876  return var;
877  }
878  }
879  // add unnamed local variable to end of list at this index
880  // with scope from 0 to SIZE_T_MAX
881  // as it is at the end of the vector, it will only be taken into account
882  // if no other variable is valid
883  var_list.emplace_back(
884  symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits<size_t>::max());
885  return var_list.back();
886 }
struct bytecode_infot const bytecode_info[]
entryt & at(const goto_programt::const_targett &t)
Definition: cfg.h:137
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A generic directed graph with a parametric node type.
Definition: graph.h:167
node_indext add_node(arguments &&... values)
Definition: graph.h:180
void add_edge(node_indext a, node_indext b)
Definition: graph.h:232
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void find_initializers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
See find_initializers_for_slot above for more detail.
std::vector< local_variable_with_holest > local_variable_table_with_holest
std::pair< const methodt &, const address_mapt & > method_with_amapt
void find_initializers_for_slot(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)
Given a sequence of users of the same local variable slot, this figures out which ones are related by...
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< method_offsett, converted_instructiont > address_mapt
irep_idt method_id
Fully qualified name of the method under translation.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
mstreamt & status() const
Definition: message.h:414
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
Expression to hold a symbol (variable)
Definition: std_expr.h:81
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
bool is_thread_local
Definition: symbol.h:65
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:28
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
JAVA Bytecode Language Conversion.
static void maybe_add_hole(local_variable_with_holest &var, java_bytecode_convert_methodt::method_offsett from, java_bytecode_convert_methodt::method_offsett to)
See above.
std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)
java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
static void populate_variable_address_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, std::vector< local_variable_with_holest * > &live_variable_at_address)
See above.
static bool is_store_to_slot(const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx)
See above.
static void populate_predecessor_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const std::vector< local_variable_with_holest * > &live_variable_at_address, const address_mapt &amap, predecessor_mapt &predecessor_map, message_handlert &msg_handler)
Populates the predecessor_map with a graph from local variable table entries to their predecessors (t...
static void populate_live_range_holes(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, java_bytecode_convert_methodt::method_offsett expanded_live_range_start)
See above.
static bool lt_startpc(const local_variable_with_holest *a, const local_variable_with_holest *b)
java_bytecode_convert_methodt::address_mapt address_mapt
java_bytecode_convert_methodt::holet holet
static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)
See above.
static java_bytecode_convert_methodt::method_offsett get_common_dominator(const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis)
Used to find out where to put a variable declaration that subsumes several variable live ranges.
java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest
static void walk_to_next_index(local_variable_table_with_holest::iterator &it1, local_variable_table_with_holest::iterator &it2, local_variable_table_with_holest::iterator itend)
Walk a vector, a contiguous block of entries with equal slot index at a time.
static void merge_variable_table_entries(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis, std::ostream &debug_out)
See above.
java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest * > &result)
See above.
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
Definition: java_types.cpp:560
optionalt< 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:1141
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
static const char * message(const statust &status)
Makes a status message string from a status.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:19
const char * mnemonic
Definition: bytecode_info.h:46
bool operator()(local_variable_with_holest *a, local_variable_with_holest *b) const
is_predecessor_oft(const predecessor_mapt &_order)
const predecessor_mapt & order
java_bytecode_convert_methodt::method_offsett get_node_index(const java_bytecode_convert_methodt::method_offsett &instruction) const
std::map< java_bytecode_convert_methodt::method_offsett, java_bytecode_convert_methodt::method_offsett > entry_mapt