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 {
40 
42 
43  void operator()(const method_with_amapt &args)
44  {
45  const auto &method=args.first;
46  const auto &amap=args.second;
47  for(const auto &inst : amap)
48  {
49  // Map instruction PCs onto node indices:
50  entry_map[inst.first]=this->add_node();
51  // Map back:
52  (*this)[entry_map[inst.first]].PC=inst.first;
53  }
54  // Add edges declared in the address map:
55  for(const auto &inst : amap)
56  {
57  for(auto succ : inst.second.successors)
58  this->add_edge(entry_map.at(inst.first), entry_map.at(succ));
59  }
60  // Next, add edges declared in the exception table, which
61  // don't figure in the address map successors/predecessors as yet:
62  for(const auto &table_entry : method.exception_table)
63  {
64  auto findit=amap.find(table_entry.start_pc);
65  INVARIANT(
66  findit!=amap.end(),
67  "Exception table entry doesn't point to an instruction?");
68  for(; findit->first<table_entry.end_pc; ++findit)
69  {
70  // For now just assume any non-branch
71  // instruction could potentially throw.
72  auto succit=findit;
73  ++succit;
74  if(succit==amap.end())
75  continue;
76  const auto &thisinst=findit->second;
77  if(thisinst.successors.size()==1 &&
78  thisinst.successors.back()==succit->first)
79  {
80  this->add_edge(
81  entry_map.at(findit->first),
82  entry_map.at(table_entry.handler_pc));
83  }
84  }
85  }
86  }
87 
89  get_first_node(const method_with_amapt &args) const
90  {
91  return args.second.begin()->first;
92  }
93 
95  get_last_node(const method_with_amapt &args) const
96  {
97  return (--args.second.end())->first;
98  }
99 
100  bool nodes_empty(const method_with_amapt &args) const
101  {
102  return args.second.empty();
103  }
104 };
105 
106 // Grab some class typedefs for brevity:
117 
118 // Comparators for local variables:
119 
120 static bool lt_index(
123 {
124  return a.var.index<b.var.index;
125 }
126 static bool lt_startpc(
129 {
130  return a->var.start_pc<b->var.start_pc;
131 }
132 
133 // The predecessor map, and a top-sorting comparator:
134 
135 typedef std::map<
137  std::set<local_variable_with_holest *> >
139 
141 {
143 
144  explicit is_predecessor_oft(const predecessor_mapt &_order) : order(_order) {}
145 
149  {
150  auto findit=order.find(a);
151  if(findit==order.end())
152  return false;
153  return findit->second.count(b)>0;
154  }
155 };
156 
157 // Helper routines for the find-initializers code below:
158 
166  const predecessor_mapt &predecessor_map,
167  std::set<local_variable_with_holest*> &result)
168 {
169  if(!result.insert(start).second)
170  return;
171  auto findit=predecessor_map.find(start);
172  if(findit==predecessor_map.end())
173  return;
174  for(const auto pred : findit->second)
175  gather_transitive_predecessors(pred, predecessor_map, result);
176 }
177 
183 static bool is_store_to_slot(
185  unsigned slotidx)
186 {
187  const std::string prevstatement=id2string(inst.statement);
188  if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
189  return false;
190 
191  unsigned storeslotidx;
192  if(inst.args.size()==1)
193  {
194  // Store with an argument:
195  const auto &arg=inst.args[0];
196  storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
197  }
198  else
199  {
200  // Store shorthands, like "store_0", "store_1"
201  INVARIANT(
202  prevstatement[6]=='_' && prevstatement.size()==8,
203  "expected store instruction looks like store_0, store_1...");
204  std::string storeslot(1, prevstatement[7]);
205  INVARIANT(
206  isdigit(storeslot[0]),
207  "store_? instructions should end in a digit");
208  storeslotidx=safe_string2unsigned(storeslot);
209  }
210  return storeslotidx==slotidx;
211 }
212 
217 static void maybe_add_hole(
221 {
222  PRECONDITION(to>=from);
223  if(to!=from)
224  var.holes.push_back(
225  {from,
226  static_cast<java_bytecode_convert_methodt::method_offsett>(to - from)});
227 }
228 
237  local_variable_table_with_holest::iterator firstvar,
238  local_variable_table_with_holest::iterator varlimit,
239  std::vector<local_variable_with_holest *> &live_variable_at_address)
240 {
241  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
242  {
243  if(it->var.start_pc+it->var.length>live_variable_at_address.size())
244  live_variable_at_address.resize(it->var.start_pc+it->var.length);
245 
246  for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
247  idx != idxlim;
248  ++idx)
249  {
250  INVARIANT(!live_variable_at_address[idx], "Local variable table clash?");
251  live_variable_at_address[idx]=&*it;
252  }
253  }
254 }
255 
273 // live at that address
282  local_variable_table_with_holest::iterator firstvar,
283  local_variable_table_with_holest::iterator varlimit,
284  const std::vector<local_variable_with_holest *> &live_variable_at_address,
285  const address_mapt &amap,
286  predecessor_mapt &predecessor_map,
287  message_handlert &msg_handler)
288 {
289  messaget msg(msg_handler);
290  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
291  {
292  // All entries of the "local_variable_table_with_holest" processed in this
293  // function concern the same Java Local Variable Table slot/register. This
294  // is because "find_initializers()" has already sorted them.
295  INVARIANT(
296  it->var.index==firstvar->var.index,
297  "all entries are for the same local variable slot");
298 
299  // Parameters are irrelevant to us and shouldn't be changed. This is because
300  // they cannot have live predecessor ranges: they are initialized by the JVM
301  // and no other live variable range can flow into them.
302  if(it->is_parameter)
303  continue;
304 
305 #ifdef DEBUG
306  msg.debug() << "jcm: ppm: processing var idx " << it->var.index
307  << " name '" << it->var.name << "' start-pc "
308  << it->var.start_pc << " len " << it->var.length
309  << "; holes " << it->holes.size() << messaget::eom;
310 #endif
311 
312  // Find the last instruction within the live range:
313  const auto end_pc = it->var.start_pc + it->var.length;
314  auto amapit=amap.find(end_pc);
315  INVARIANT(
316  amapit!=amap.begin(),
317  "current bytecode shall not be the first");
318  auto old_amapit=amapit;
319  --amapit;
320  if(old_amapit==amap.end())
321  {
322  INVARIANT(
323  end_pc>amapit->first,
324  "Instruction live range doesn't align to instruction boundary?");
325  }
326 
327  // Find vartable entries that flow into this one. For unknown reasons this
328  // loop iterates backwards, walking back from the last bytecode in the live
329  // range of variable it to the first one. For each value of the iterator
330  // "amapit" we search for instructions that jump into amapit's address
331  // (predecessors)
332  auto new_start_pc = it->var.start_pc;
333  for(; amapit->first>=it->var.start_pc; --amapit)
334  {
335  for(auto pred : amapit->second.predecessors)
336  {
337  // pred is the address (byecode offset) of a instruction that jumps into
338  // amapit. Compute now a pointer to the variable-with-holes whose index
339  // equals that of amapit and which was alive on instruction pred, or a
340  // null pointer if no such variable exists (e.g., because no live range
341  // covers that instruction)
342  auto pred_var=
343  (pred<live_variable_at_address.size() ?
344  live_variable_at_address[pred] :
345  nullptr);
346 
347  // Three cases are now possible:
348  // 1. The predecessor instruction is in the same live range: nothing to
349  // do.
350  if(pred_var==&*it)
351  {
352  continue;
353  }
354  // 2. The predecessor instruction is in no live range among those for
355  // variable slot it->var.index
356  else if(!pred_var)
357  {
358  // Check if this is an initializer, and if so expand the live range
359  // to include it, but don't check its predecessors:
360  auto inst_before_this=amapit;
361  INVARIANT(
362  inst_before_this!=amap.begin(),
363  "we shall not be on the first bytecode of the method");
364  --inst_before_this;
365  if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
366  {
367  // These sorts of infeasible edges can occur because jsr
368  // handling is presently vague (any subroutine is assumed to
369  // be able to return to any callsite)
370  msg.warning() << "Local variable table: ignoring flow from "
371  << "out of range for " << it->var.name << ' '
372  << pred << " -> " << amapit->first
373  << messaget::eom;
374  continue;
375  }
376  if(!is_store_to_slot(
377  *(inst_before_this->second.source),
378  it->var.index))
379  {
380  msg.warning() << "Local variable table: didn't find initializing "
381  << "store for predecessor of bytecode at address "
382  << amapit->first << " ("
383  << amapit->second.predecessors.size()
384  << " predecessors)" << msg.eom;
385  throw "local variable table: unexpected live ranges";
386  }
387  new_start_pc=pred;
388  }
389  // 3. Predecessor instruction is a different range associated to the
390  // same variable slot
391  else
392  {
393  if(pred_var->var.name!=it->var.name ||
394  pred_var->var.descriptor!=it->var.descriptor)
395  {
396  // These sorts of infeasible edges can occur because
397  // jsr handling is presently vague (any subroutine is
398  // assumed to be able to return to any callsite)
399  msg.warning() << "Local variable table: ignoring flow from "
400  << "clashing variable for "
401  << it->var.name << ' ' << pred << " -> "
402  << amapit->first << messaget::eom;
403  continue;
404  }
405  // OK, this is a flow from a similar but
406  // distinct entry in the local var table.
407  predecessor_map[&*it].insert(pred_var);
408  }
409  }
410  }
411 
412  // If a simple pre-block initializer was found,
413  // add it to the live range now:
414  it->var.length+=(it->var.start_pc-new_start_pc);
415  it->var.start_pc=new_start_pc;
416  }
417 }
418 
427  const std::set<local_variable_with_holest *> &merge_vars,
428  const java_cfg_dominatorst &dominator_analysis)
429 {
430  PRECONDITION(!merge_vars.empty());
431 
432  auto first_pc =
433  std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
434  for(auto v : merge_vars)
435  {
436  if(v->var.start_pc<first_pc)
437  first_pc=v->var.start_pc;
438  }
439 
440  std::vector<java_bytecode_convert_methodt::method_offsett>
441  candidate_dominators;
442  for(auto v : merge_vars)
443  {
444  const auto &dominator_nodeidx=
445  dominator_analysis.cfg.entry_map.at(v->var.start_pc);
446  const auto &this_var_doms=
447  dominator_analysis.cfg[dominator_nodeidx].dominators;
448  for(const auto this_var_dom : this_var_doms)
449  if(this_var_dom<=first_pc)
450  candidate_dominators.push_back(this_var_dom);
451  }
452  std::sort(candidate_dominators.begin(), candidate_dominators.end());
453 
454  // Working from the back, simply find the first PC
455  // that occurs merge_vars.size() times and therefore
456  // dominates all vars we seek to merge:
457  for(auto domit=candidate_dominators.rbegin(),
458  domitend=candidate_dominators.rend();
459  domit!=domitend;
460  /* Don't increment here */)
461  {
462  std::size_t repeats = 0;
463  auto dom=*domit;
464  while(domit!=domitend && *domit==dom)
465  {
466  ++domit;
467  ++repeats;
468  }
469  assert(repeats<=merge_vars.size());
470  if(repeats==merge_vars.size())
471  return dom;
472  }
473 
474  throw "variable live ranges with no common dominator?";
475 }
476 
486  local_variable_with_holest &merge_into,
487  const std::set<local_variable_with_holest *> &merge_vars,
488  java_bytecode_convert_methodt::method_offsett expanded_live_range_start)
489 {
490  std::vector<local_variable_with_holest *> sorted_by_startpc(
491  merge_vars.begin(), merge_vars.end());
492  std::sort(sorted_by_startpc.begin(), sorted_by_startpc.end(), lt_startpc);
493 
495  merge_into,
496  expanded_live_range_start,
497  sorted_by_startpc[0]->var.start_pc);
499  idx < sorted_by_startpc.size() - 1;
500  ++idx)
501  {
503  merge_into,
504  sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->var.length,
505  sorted_by_startpc[idx+1]->var.start_pc);
506  }
507 }
508 
518  local_variable_with_holest &merge_into,
519  const std::set<local_variable_with_holest *> &merge_vars,
520  const java_cfg_dominatorst &dominator_analysis,
521  std::ostream &debug_out)
522 {
523  // Because we need a lexically-scoped declaration,
524  // we must have the merged variable
525  // enter scope both in a block that dominates all entries, and which
526  // precedes them in program order.
527  const auto found_dominator =
528  get_common_dominator(merge_vars, dominator_analysis);
529 
530  // Populate the holes in the live range
531  // (addresses where the new variable will be in scope,
532  // but references to this stack slot should not resolve to it
533  // as it was not visible in the original local variable table)
534  populate_live_range_holes(merge_into, merge_vars, found_dominator);
535 
537  for(auto v : merge_vars)
538  {
539  if(v->var.start_pc+v->var.length>last_pc)
540  last_pc=v->var.start_pc+v->var.length;
541  }
542 
543  // Apply the changes:
544  merge_into.var.start_pc=found_dominator;
545  merge_into.var.length=last_pc-found_dominator;
546 
547 #ifdef DEBUG
548  debug_out << "Merged " << merge_vars.size() << " variables named "
549  << merge_into.var.name << "; new live range "
550  << merge_into.var.start_pc << '-'
551  << merge_into.var.start_pc + merge_into.var.length << '\n';
552 #else
553  (void)debug_out; // unused parameter
554 #endif
555 
556  // Nuke the now-subsumed var-table entries:
557  for(auto &v : merge_vars)
558  if(v!=&merge_into)
559  v->var.length=0;
560 }
561 
576  local_variable_table_with_holest::iterator firstvar,
577  local_variable_table_with_holest::iterator varlimit,
578  const address_mapt &amap,
579  const java_cfg_dominatorst &dominator_analysis)
580 {
581  // Build a simple map from instruction PC to the variable
582  // live in this slot at that PC, and a map from each variable
583  // to variables that flow into it:
584  std::vector<local_variable_with_holest *> live_variable_at_address;
585  populate_variable_address_map(firstvar, varlimit, live_variable_at_address);
586 
587  // Now find variables that flow together by
588  // walking backwards to find initializers
589  // or branches from other live ranges:
590  predecessor_mapt predecessor_map;
592  firstvar,
593  varlimit,
594  live_variable_at_address,
595  amap,
596  predecessor_map,
598 
599  // OK, we've established the flows all seem sensible.
600  // Now merge vartable entries according to the predecessor_map:
601 
602  // Take the transitive closure of the predecessor map:
603  for(auto &kv : predecessor_map)
604  {
605  std::set<local_variable_with_holest *> closed_preds;
606  gather_transitive_predecessors(kv.first, predecessor_map, closed_preds);
607  kv.second=std::move(closed_preds);
608  }
609 
610  // Top-sort so that we get the bottom variables first:
611  is_predecessor_oft comp(predecessor_map);
612  std::vector<local_variable_with_holest *> topsorted_vars;
613  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
614  topsorted_vars.push_back(&*it);
615 
616  std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);
617 
618  // Now merge the entries:
619  for(auto merge_into : topsorted_vars)
620  {
621  // Already merged into another variable?
622  if(merge_into->var.length==0)
623  continue;
624 
625  auto findit=predecessor_map.find(merge_into);
626  // Nothing to do?
627  if(findit==predecessor_map.end())
628  continue;
629 
630  const auto &merge_vars=findit->second;
631  INVARIANT(merge_vars.size()>=2, "merging requires at least 2 variables");
632 
634  *merge_into,
635  merge_vars,
636  dominator_analysis,
637  status());
638  }
639 }
640 
648 static void walk_to_next_index(
649  local_variable_table_with_holest::iterator &it1,
650  local_variable_table_with_holest::iterator &it2,
651  local_variable_table_with_holest::iterator itend)
652 {
653  if(it2==itend)
654  {
655  it1=itend;
656  return;
657  }
658 
659  auto old_it2=it2;
660  auto index=it2->var.index;
661  while(it2!=itend && it2->var.index==index)
662  ++it2;
663  it1=old_it2;
664 }
665 
674  const address_mapt &amap,
675  const java_cfg_dominatorst &dominator_analysis)
676 {
677  // Sort table entries by local slot index:
678  std::sort(vars.begin(), vars.end(), lt_index);
679 
680  // For each block of entries using a particular index,
681  // try to combine them:
682  auto it1=vars.begin();
683  auto it2=it1;
684  auto itend=vars.end();
685  walk_to_next_index(it1, it2, itend);
686  for(; it1!=itend; walk_to_next_index(it1, it2, itend))
687  find_initializers_for_slot(it1, it2, amap, dominator_analysis);
688 }
689 
693 static void cleanup_var_table(
694  std::vector<local_variable_with_holest> &vars_with_holes)
695 {
696  size_t toremove=0;
697  for(size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
698  {
699  auto &v=vars_with_holes[i];
700  if(v.var.length==0)
701  {
702  // Move to end; consider the new element we've swapped in:
703  ++toremove;
704  if(i!=vars_with_holes.size()-toremove) // Already where it needs to be?
705  std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
706  --i; // May make i (size_t)-1, but it will immediately be
707  // re-incremented as the loop iterates.
708  }
709  }
710 
711  // Remove un-needed entries.
712  vars_with_holes.resize(vars_with_holes.size()-toremove);
713 }
714 
722  const methodt &m,
723  const address_mapt &amap)
724 {
725  // Compute CFG dominator tree
726  java_cfg_dominatorst dominator_analysis;
727  method_with_amapt dominator_args(m, amap);
728  dominator_analysis(dominator_args);
729 
730 #ifdef DEBUG
731  debug() << "jcm: setup-local-vars: m.is_static "
732  << m.is_static << " m.descriptor " << m.descriptor << eom;
733  debug() << "jcm: setup-local-vars: lv arg slots "
735  debug() << "jcm: setup-local-vars: lvt size "
736  << m.local_variable_table.size() << eom;
737 #endif
738 
739  // Find out which local variable table entries should be merged:
740  // Wrap each entry so we have a data structure to work during function calls,
741  // where we record live ranges with holes:
742  std::vector<local_variable_with_holest> vars_with_holes;
743  for(const auto &v : m.local_variable_table)
744  vars_with_holes.push_back({v, is_parameter(v), {}});
745 
746  // Merge variable records. See documentation of in
747  // `find_initializers_for_slot` for more details. If the strategy employed
748  // there fails with an exception, we just ignore the LVT for this method, no
749  // variable is generated in `this->variables[]` (because we return here and
750  // dont let the for loop below to execute), and as a result the method
751  // this->variable() will be forced to create new `anonlocal::` variables, as
752  // the only source of variable names for that method is `this->variables[]`.
753  try
754  {
755  find_initializers(vars_with_holes, amap, dominator_analysis);
756  }
757  catch(const char *message)
758  {
759  warning() << "Bytecode -> codet translation error: " << message << eom
760  << "This is probably due to an unexpected LVT, "
761  << "falling back to translation without LVT" << eom;
762  return;
763  }
764 
765  // Clean up removed records from the variable table:
766  cleanup_var_table(vars_with_holes);
767 
768  // Do the locals and parameters in the variable table, which is available when
769  // compiled with -g or for methods with many local variables in the latter
770  // case, different variables can have the same index, depending on the
771  // context.
772  //
773  // to calculate which variable to use, one uses the address of the instruction
774  // that uses the variable, the size of the instruction and the start_pc /
775  // length values in the local variable table
776  for(const auto &v : vars_with_holes)
777  {
778  if(v.is_parameter)
779  continue;
780 
781 #ifdef DEBUG
782  debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index
783  << " name " << v.var.name << " v.var.descriptor '"
784  << v.var.descriptor << "' holes " << v.holes.size() << eom;
785 #endif
786 
787  const std::string &method_name = id2string(method_id);
788  const size_t method_name_end = method_name.rfind(":(");
789  const size_t class_name_end = method_name.rfind('.', method_name_end);
790  INVARIANT(
791  method_name_end != std::string::npos &&
792  class_name_end != std::string::npos,
793  "A method name has the format class `.` method `:(`signature`)`.");
794  const std::string class_name = method_name.substr(0, class_name_end);
795 
796  const typet t = v.var.signature.has_value()
798  v.var.descriptor, v.var.signature, class_name)
799  : java_type_from_string(v.var.descriptor);
800 
801  std::ostringstream id_oss;
802  id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;
803  irep_idt identifier(id_oss.str());
804  symbol_exprt result(identifier, t);
805  result.set(ID_C_base_name, v.var.name);
806 
807  // Create a new local variable in the variables[] array, the result of
808  // merging multiple local variables with equal name (parameters excluded)
809  // into a single local variable with holes
810  variables[v.var.index].push_back(variablet());
811  auto &newv=variables[v.var.index].back();
812  newv.symbol_expr=result;
813  newv.start_pc=v.var.start_pc;
814  newv.length=v.var.length;
815  newv.holes=std::move(v.holes);
816 
817  // Register the local variable in the symbol table
818  symbolt new_symbol;
819  new_symbol.name=identifier;
820  new_symbol.type=t;
821  new_symbol.base_name=v.var.name;
822  new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
823  new_symbol.mode=ID_java;
824  new_symbol.is_type=false;
825  new_symbol.is_file_local=true;
826  new_symbol.is_thread_local=true;
827  new_symbol.is_lvalue=true;
828  symbol_table.add(new_symbol);
829  }
830 }
831 
840  size_t address,
841  variablest &var_list)
842 {
843  for(const variablet &var : var_list)
844  {
845  size_t start_pc=var.start_pc;
846  size_t length=var.length;
847  if(address>=start_pc && address<(start_pc+length))
848  {
849  bool found_hole=false;
850  for(auto &hole : var.holes)
851  if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
852  {
853  found_hole=true;
854  break;
855  }
856  if(found_hole)
857  continue;
858  return var;
859  }
860  }
861  // add unnamed local variable to end of list at this index
862  // with scope from 0 to SIZE_T_MAX
863  // as it is at the end of the vector, it will only be taken into account
864  // if no other variable is valid
865  size_t list_length=var_list.size();
866  var_list.resize(list_length+1);
867  var_list[list_length].start_pc=0;
868  var_list[list_length].length=std::numeric_limits<size_t>::max();
869  return var_list[list_length];
870 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
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::address_mapt address_mapt
A generic directed graph with a parametric node type.
Definition: graph.h:167
JAVA Bytecode Language Conversion.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:65
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::pair< const methodt &, const address_mapt & > method_with_amapt
irep_idt method_id
Fully qualified name of the method under translation.
std::map< java_bytecode_convert_methodt::method_offsett, java_bytecode_convert_methodt::method_offsett > entry_mapt
irep_idt mode
Language mode.
Definition: symbol.h:49
entry_mapt entry_map
Definition: cfg.h:106
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
Symbol table entry.
Definition: symbol.h:27
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...
static bool is_store_to_slot(const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx)
See above.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
mstreamt & warning() const
Definition: message.h:391
std::vector< local_variable_with_holest > local_variable_table_with_holest
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...
typet java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof...
Definition: java_types.cpp:492
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.
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.
java_bytecode_convert_methodt::holet holet
static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest *> &result)
See above.
std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
static bool lt_startpc(const local_variable_with_holest *a, const local_variable_with_holest *b)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
Definition: java_types.h:705
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.
java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest
static eomt eom
Definition: message.h:284
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:54
java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
typet type
Type of symbol.
Definition: symbol.h:31
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
message_handlert & get_message_handler()
Definition: message.h:174
static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)
See above.
bool operator()(local_variable_with_holest *a, local_variable_with_holest *b) const
mstreamt & result() const
Definition: message.h:396
mstreamt & status() const
Definition: message.h:401
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
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.
void add_edge(node_indext a, node_indext b)
Definition: graph.h:232
bool is_file_local
Definition: symbol.h:66
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...
Expression to hold a symbol (variable)
Definition: std_expr.h:143
static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
is_predecessor_oft(const predecessor_mapt &_order)
mstreamt & debug() const
Definition: message.h:416
std::map< method_offsett, converted_instructiont > address_mapt
bool is_type
Definition: symbol.h:61
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...
java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
void push_back(const T &t)
bool is_lvalue
Definition: symbol.h:66
const predecessor_mapt & order