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,
658  merge_vars,
659  dominator_analysis,
660  status());
661  }
662 }
663 
671 static void walk_to_next_index(
672  local_variable_table_with_holest::iterator &it1,
673  local_variable_table_with_holest::iterator &it2,
674  local_variable_table_with_holest::iterator itend)
675 {
676  if(it2==itend)
677  {
678  it1=itend;
679  return;
680  }
681 
682  auto old_it2=it2;
683  auto index=it2->var.index;
684  while(it2!=itend && it2->var.index==index)
685  ++it2;
686  it1=old_it2;
687 }
688 
697  const address_mapt &amap,
698  const java_cfg_dominatorst &dominator_analysis)
699 {
700  // Sort table entries by local slot index:
701  std::sort(vars.begin(), vars.end(), lt_index);
702 
703  // For each block of entries using a particular index,
704  // try to combine them:
705  auto it1=vars.begin();
706  auto it2=it1;
707  auto itend=vars.end();
708  walk_to_next_index(it1, it2, itend);
709  for(; it1!=itend; walk_to_next_index(it1, it2, itend))
710  find_initializers_for_slot(it1, it2, amap, dominator_analysis);
711 }
712 
716 static void cleanup_var_table(
717  std::vector<local_variable_with_holest> &vars_with_holes)
718 {
719  size_t toremove=0;
720  for(size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
721  {
722  auto &v=vars_with_holes[i];
723  if(v.var.length==0)
724  {
725  // Move to end; consider the new element we've swapped in:
726  ++toremove;
727  if(i!=vars_with_holes.size()-toremove) // Already where it needs to be?
728  std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
729  --i; // May make i (size_t)-1, but it will immediately be
730  // re-incremented as the loop iterates.
731  }
732  }
733 
734  // Remove un-needed entries.
735  vars_with_holes.resize(vars_with_holes.size()-toremove);
736 }
737 
745  const methodt &m,
746  const address_mapt &amap)
747 {
748  // Compute CFG dominator tree
749  java_cfg_dominatorst dominator_analysis;
750  method_with_amapt dominator_args(m, amap);
751  dominator_analysis(dominator_args);
752 
753 #ifdef DEBUG
754  debug() << "jcm: setup-local-vars: m.is_static "
755  << m.is_static << " m.descriptor " << m.descriptor << eom;
756  debug() << "jcm: setup-local-vars: lv arg slots "
758  debug() << "jcm: setup-local-vars: lvt size "
759  << m.local_variable_table.size() << eom;
760 #endif
761 
762  // Find out which local variable table entries should be merged:
763  // Wrap each entry so we have a data structure to work during function calls,
764  // where we record live ranges with holes:
765  std::vector<local_variable_with_holest> vars_with_holes;
766  for(const auto &v : m.local_variable_table)
767  vars_with_holes.push_back({v, is_parameter(v), {}});
768 
769  // Merge variable records. See documentation of in
770  // `find_initializers_for_slot` for more details. If the strategy employed
771  // there fails with an exception, we just ignore the LVT for this method, no
772  // variable is generated in `this->variables[]` (because we return here and
773  // dont let the for loop below to execute), and as a result the method
774  // this->variable() will be forced to create new `anonlocal::` variables, as
775  // the only source of variable names for that method is `this->variables[]`.
776  try
777  {
778  find_initializers(vars_with_holes, amap, dominator_analysis);
779  }
780  catch(const char *message)
781  {
782  warning() << "Bytecode -> codet translation error: " << message << eom
783  << "This is probably due to an unexpected LVT, "
784  << "falling back to translation without LVT" << eom;
785  return;
786  }
787 
788  // Clean up removed records from the variable table:
789  cleanup_var_table(vars_with_holes);
790 
791  // Do the locals and parameters in the variable table, which is available when
792  // compiled with -g or for methods with many local variables in the latter
793  // case, different variables can have the same index, depending on the
794  // context.
795  //
796  // to calculate which variable to use, one uses the address of the instruction
797  // that uses the variable, the size of the instruction and the start_pc /
798  // length values in the local variable table
799  for(auto &v : vars_with_holes)
800  {
801  if(v.is_parameter)
802  continue;
803 
804 #ifdef DEBUG
805  debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index
806  << " name " << v.var.name << " v.var.descriptor '"
807  << v.var.descriptor << "' holes " << v.holes.size() << eom;
808 #endif
809 
810  const std::string &method_name = id2string(method_id);
811  const size_t method_name_end = method_name.rfind(":(");
812  const size_t class_name_end = method_name.rfind('.', method_name_end);
813  INVARIANT(
814  method_name_end != std::string::npos &&
815  class_name_end != std::string::npos,
816  "A method name has the format class `.` method `:(`signature`)`.");
817  const std::string class_name = method_name.substr(0, class_name_end);
818 
819  const typet t = v.var.signature.has_value()
821  v.var.descriptor, v.var.signature, class_name)
822  : *java_type_from_string(v.var.descriptor);
823 
824  std::ostringstream id_oss;
825  id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;
826  irep_idt identifier(id_oss.str());
827  symbol_exprt result(identifier, t);
828  result.set(ID_C_base_name, v.var.name);
829 
830  // Create a new local variable in the variables[] array, the result of
831  // merging multiple local variables with equal name (parameters excluded)
832  // into a single local variable with holes
833  variables[v.var.index].emplace_back(
834  result, v.var.start_pc, v.var.length, false, std::move(v.holes));
835 
836  // Register the local variable in the symbol table
837  symbolt new_symbol;
838  new_symbol.name=identifier;
839  new_symbol.type=t;
840  new_symbol.base_name=v.var.name;
841  new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
842  new_symbol.mode=ID_java;
843  new_symbol.is_type=false;
844  new_symbol.is_file_local=true;
845  new_symbol.is_thread_local=true;
846  new_symbol.is_lvalue=true;
847  symbol_table.add(new_symbol);
848  }
849 }
850 
859  size_t address,
860  variablest &var_list)
861 {
862  for(const variablet &var : var_list)
863  {
864  size_t start_pc=var.start_pc;
865  size_t length=var.length;
866  if(address>=start_pc && address<(start_pc+length))
867  {
868  bool found_hole=false;
869  for(auto &hole : var.holes)
870  if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
871  {
872  found_hole=true;
873  break;
874  }
875  if(found_hole)
876  continue;
877  return var;
878  }
879  }
880  // add unnamed local variable to end of list at this index
881  // with scope from 0 to SIZE_T_MAX
882  // as it is at the end of the vector, it will only be taken into account
883  // if no other variable is valid
884  var_list.emplace_back(
885  symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits<size_t>::max());
886  return var_list.back();
887 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:62
java_bytecode_convert_methodt::is_parameter
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...
Definition: java_bytecode_convert_method_class.h:215
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_convert_methodt::holet
Definition: java_bytecode_convert_method_class.h:106
java_bytecode_parse_treet::methodt::local_variablet::name
irep_idt name
Definition: java_bytecode_parse_tree.h:129
java_bytecode_convert_methodt::local_variable_with_holest::var
local_variablet var
Definition: java_bytecode_convert_method_class.h:113
is_predecessor_oft
Definition: java_local_variable_table.cpp:163
local_variable_with_holest
java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest
Definition: java_local_variable_table.cpp:132
java_bytecode_convert_methodt::method_id
irep_idt method_id
Fully qualified name of the method under translation.
Definition: java_bytecode_convert_method_class.h:88
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
arith_tools.h
get_common_dominator
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.
Definition: java_local_variable_table.cpp:449
java_bytecode_convert_methodt::setup_local_variables
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
Definition: java_local_variable_table.cpp:744
java_bytecode_convert_method_class.h
JAVA Bytecode Language Conversion.
typet
The type of an expression, extends irept.
Definition: type.h:29
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:86
java_cfg_dominatorst
java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
Definition: java_local_variable_table.cpp:138
lt_startpc
static bool lt_startpc(const local_variable_with_holest *a, const local_variable_with_holest *b)
Definition: java_local_variable_table.cpp:148
messaget::status
mstreamt & status() const
Definition: message.h:414
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
java_bytecode_parse_treet::methodt::local_variable_table
local_variable_tablet local_variable_table
Definition: java_bytecode_parse_tree.h:138
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::get_first_node
static java_bytecode_convert_methodt::method_offsett get_first_node(const method_with_amapt &args)
Definition: java_local_variable_table.cpp:111
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entryt
std::size_t entryt
Definition: java_local_variable_table.cpp:43
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:168
java_bytecode_convert_methodt::find_initializers
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.
Definition: java_local_variable_table.cpp:695
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition: java_bytecode_parse_tree.h:60
invariant.h
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:57
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::nodes_empty
static bool nodes_empty(const method_with_amapt &args)
Definition: java_local_variable_table.cpp:122
grapht< cfg_base_nodet< T, goto_programt::const_targett > >::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:181
populate_variable_address_map
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.
Definition: java_local_variable_table.cpp:259
java_bytecode_convert_methodt::local_variable_with_holest::holes
std::vector< holet > holes
Definition: java_bytecode_convert_method_class.h:115
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cleanup_var_table
static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)
See above.
Definition: java_local_variable_table.cpp:716
irep_idt
dstringt irep_idt
Definition: irep.h:32
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entry_mapt
std::map< java_bytecode_convert_methodt::method_offsett, java_bytecode_convert_methodt::method_offsett > entry_mapt
Definition: java_local_variable_table.cpp:42
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
java_bytecode_convert_methodt::variables
expanding_vectort< variablest > variables
Definition: java_bytecode_convert_method_class.h:167
lt_index
static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)
Definition: java_local_variable_table.cpp:142
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::method_with_amapt
java_bytecode_convert_methodt::method_with_amapt method_with_amapt
Definition: java_local_variable_table.cpp:39
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_type_from_string_with_exception
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
java_bytecode_parse_treet::membert::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:67
local_variable_table_with_holest
java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
Definition: java_local_variable_table.cpp:134
is_predecessor_oft::is_predecessor_oft
is_predecessor_oft(const predecessor_mapt &_order)
Definition: java_local_variable_table.cpp:166
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
string2int.h
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::operator()
void operator()(const method_with_amapt &args)
Definition: java_local_variable_table.cpp:48
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_bytecode_convert_methodt::variablet::start_pc
size_t start_pc
Definition: java_bytecode_convert_method_class.h:125
messaget::result
mstreamt & result() const
Definition: message.h:409
java_bytecode_parse_treet::membert::is_static
bool is_static
Definition: java_bytecode_parse_tree.h:70
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_bytecode_convert_methodt::method_offsett
uint16_t method_offsett
Definition: java_bytecode_convert_method_class.h:74
address_mapt
java_bytecode_convert_methodt::address_mapt address_mapt
Definition: java_local_variable_table.cpp:136
gather_transitive_predecessors
static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest * > &result)
See above.
Definition: java_local_variable_table.cpp:186
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
java_bytecode_convert_methodt::local_variable_table_with_holest
std::vector< local_variable_with_holest > local_variable_table_with_holest
Definition: java_bytecode_convert_method_class.h:119
java_bytecode_convert_methodt::find_variable_for_slot
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
Definition: java_local_variable_table.cpp:858
cfg_baset< T, const goto_programt, goto_programt::const_targett >::get_node_index
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
java_bytecode_convert_methodt::slots_for_parameters
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
Definition: java_bytecode_convert_method_class.h:102
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::procedure_local_cfg_baset
procedure_local_cfg_baset()
Definition: java_local_variable_table.cpp:46
java_bytecode_parse_treet::methodt::local_variablet::length
std::size_t length
Definition: java_bytecode_parse_tree.h:134
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::get_node
nodet & get_node(const java_bytecode_convert_methodt::method_offsett &instruction)
Definition: java_local_variable_table.cpp:100
java_bytecode_parse_treet::methodt::local_variablet::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:133
message_handlert
Definition: message.h:28
populate_predecessor_map
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...
Definition: java_local_variable_table.cpp:304
grapht< cfg_base_nodet< T, goto_programt::const_targett > >::add_edge
void add_edge(node_indext a, node_indext b)
Definition: graph.h:233
java_type_from_string
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
safe_string2unsigned
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:19
is_predecessor_oft::operator()
bool operator()(local_variable_with_holest *a, local_variable_with_holest *b) const
Definition: java_local_variable_table.cpp:168
java_bytecode_convert_methodt
Definition: java_bytecode_convert_method_class.h:33
cfg_baset< T, const goto_programt, goto_programt::const_targett >::entry_map
entry_mapt entry_map
Definition: cfg.h:152
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
cfg_baset< T, const goto_programt, goto_programt::const_targett >::nodet
base_grapht::nodet nodet
Definition: cfg.h:92
java_bytecode_convert_methodt::find_initializers_for_slot
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...
Definition: java_local_variable_table.cpp:598
merge_variable_table_entries
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.
Definition: java_local_variable_table.cpp:540
is_predecessor_oft::order
const predecessor_mapt & order
Definition: java_local_variable_table.cpp:164
is_store_to_slot
static bool is_store_to_slot(const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx)
See above.
Definition: java_local_variable_table.cpp:205
symbolt
Symbol table entry.
Definition: symbol.h:28
java_bytecode_convert_methodt::address_mapt
std::map< method_offsett, converted_instructiont > address_mapt
Definition: java_bytecode_convert_method_class.h:238
procedure_local_cfg_baset
Definition: cfg.h:295
symbolt::is_type
bool is_type
Definition: symbol.h:61
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::get_node
const nodet & get_node(const java_bytecode_convert_methodt::method_offsett &instruction) const
Definition: java_local_variable_table.cpp:104
populate_live_range_holes
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.
Definition: java_local_variable_table.cpp:508
cfg_base_nodet
Definition: cfg.h:28
maybe_add_hole
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.
Definition: java_local_variable_table.cpp:240
java_bytecode_convert_methodt::variablest
std::vector< variablet > variablest
Definition: java_bytecode_convert_method_class.h:166
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
messaget::debug
mstreamt & debug() const
Definition: message.h:429
java_bytecode_convert_methodt::local_variable_with_holest
Definition: java_bytecode_convert_method_class.h:112
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
java_types.h
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::entry_map
entry_mapt entry_map
Definition: java_local_variable_table.cpp:44
java_utils.h
messaget::warning
mstreamt & warning() const
Definition: message.h:404
predecessor_mapt
std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
Definition: java_local_variable_table.cpp:160
java_bytecode_convert_methodt::variablet
Definition: java_bytecode_convert_method_class.h:122
java_bytecode_parse_treet::methodt::local_variablet::index
std::size_t index
Definition: java_bytecode_parse_tree.h:132
walk_to_next_index
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.
Definition: java_local_variable_table.cpp:671
java_bytecode_convert_methodt::method_with_amapt
std::pair< const methodt &, const address_mapt & > method_with_amapt
Definition: java_bytecode_convert_method_class.h:239
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::nodet
base_grapht::nodet nodet
Definition: java_local_variable_table.cpp:38
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:48
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::get_node_index
java_bytecode_convert_methodt::method_offsett get_node_index(const java_bytecode_convert_methodt::method_offsett &instruction) const
Definition: java_local_variable_table.cpp:93
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::get_last_node
static java_bytecode_convert_methodt::method_offsett get_last_node(const method_with_amapt &args)
Definition: java_local_variable_table.cpp:117
java_bytecode_convert_methodt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_convert_method_class.h:77
validation_modet::INVARIANT
@ INVARIANT
holet
java_bytecode_convert_methodt::holet holet
Definition: java_local_variable_table.cpp:130
procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, java_bytecode_convert_methodt::method_offsett >::base_grapht
grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > base_grapht
Definition: java_local_variable_table.cpp:37
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:38
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939