java_local_variable_table.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java local variable table processing
 
Author: Chris Smowton, chris.smowton@diffblue.com
 
\*******************************************************************/
 
 
#include "java_bytecode_convert_method_class.h"
 
#include "java_types.h"
 
#include <util/arith_tools.h>
#include <util/invariant.h>
#include <util/string2int.h>
#include <util/symbol_table.h>
 
#include <iostream>
 
// Specialise the CFG representation to work over Java instead of GOTO programs.
// This must be done at global scope due to template resolution rules.
 
template <class T>
struct procedure_local_cfg_baset<
  T,
  java_bytecode_convert_methodt::method_with_amapt,
  java_bytecode_convert_methodt::method_offsett>
  : public grapht<
      cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
{
  typedef grapht<
    cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
    base_grapht;
  typedef typename base_grapht::nodet nodet;
  typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt;
  typedef std::map<java_bytecode_convert_methodt::method_offsett,
                   java_bytecode_convert_methodt::method_offsett>
    entry_mapt;
  typedef std::size_t entryt;
  entry_mapt entry_map;
 
  procedure_local_cfg_baset() {}
 
  void operator()(const method_with_amapt &args)
  {
    const auto &method=args.first;
    const auto &amap=args.second;
    for(const auto &inst : amap)
    {
      // Map instruction PCs onto node indices:
      entry_map[inst.first]=this->add_node();
      // Map back:
      (*this)[entry_map[inst.first]].PC=inst.first;
    }
    // Add edges declared in the address map:
    for(const auto &inst : amap)
    {
      for(auto succ : inst.second.successors)
        this->add_edge(entry_map.at(inst.first), entry_map.at(succ));
    }
    // Next, add edges declared in the exception table, which
    // don't figure in the address map successors/predecessors as yet:
    for(const auto &table_entry : method.exception_table)
    {
      auto findit=amap.find(table_entry.start_pc);
      INVARIANT(
        findit!=amap.end(),
        "Exception table entry doesn't point to an instruction?");
      for(; findit->first<table_entry.end_pc; ++findit)
      {
        // For now just assume any non-branch
        // instruction could potentially throw.
        auto succit=findit;
        ++succit;
        if(succit==amap.end())
          continue;
        const auto &thisinst=findit->second;
        if(thisinst.successors.size()==1 &&
           thisinst.successors.back()==succit->first)
        {
          this->add_edge(
            entry_map.at(findit->first),
            entry_map.at(table_entry.handler_pc));
        }
      }
    }
  }
 
  java_bytecode_convert_methodt::method_offsett get_node_index(
    const java_bytecode_convert_methodt::method_offsett &instruction) const
  {
    return entry_map.at(instruction);
  }
 
  nodet &
  get_node(const java_bytecode_convert_methodt::method_offsett &instruction)
  {
    return (*this)[get_node_index(instruction)];
  }
  const nodet &get_node(
    const java_bytecode_convert_methodt::method_offsett &instruction) const
  {
    return (*this)[get_node_index(instruction)];
  }
 
  static java_bytecode_convert_methodt::method_offsett
  get_first_node(const method_with_amapt &args)
  {
    return args.second.begin()->first;
  }
 
  static java_bytecode_convert_methodt::method_offsett
  get_last_node(const method_with_amapt &args)
  {
    return (--args.second.end())->first;
  }
 
  static bool nodes_empty(const method_with_amapt &args)
  {
    return args.second.empty();
  }
};
 
// Grab some class typedefs for brevity:
typedef java_bytecode_convert_methodt::holet
  holet;
typedef java_bytecode_convert_methodt::local_variable_with_holest
  local_variable_with_holest;
typedef java_bytecode_convert_methodt::local_variable_table_with_holest
  local_variable_table_with_holest;
typedef java_bytecode_convert_methodt::address_mapt
  address_mapt;
typedef java_bytecode_convert_methodt::java_cfg_dominatorst
  java_cfg_dominatorst;
 
// Comparators for local variables:
 
static bool lt_index(
  const local_variable_with_holest &a,
  const local_variable_with_holest &b)
{
  return a.var.index<b.var.index;
}
static bool lt_startpc(
  const local_variable_with_holest *a,
  const local_variable_with_holest *b)
{
  return a->var.start_pc<b->var.start_pc;
}
 
// The predecessor map, and a top-sorting comparator:
 
typedef std::map<
  local_variable_with_holest *,
  std::set<local_variable_with_holest *> >
  predecessor_mapt;
 
struct is_predecessor_oft
{
  const predecessor_mapt &order;
 
  explicit is_predecessor_oft(const predecessor_mapt &_order) : order(_order) {}
 
  bool operator()(
    local_variable_with_holest *a,
    local_variable_with_holest *b) const
  {
    auto findit=order.find(a);
    if(findit==order.end())
      return false;
    return findit->second.count(b)>0;
  }
};
 
// Helper routines for the find-initializers code below:
 
static void gather_transitive_predecessors(
  local_variable_with_holest *start,
  const predecessor_mapt &predecessor_map,
  std::set<local_variable_with_holest*> &result)
{
  if(!result.insert(start).second)
    return;
  auto findit=predecessor_map.find(start);
  if(findit==predecessor_map.end())
    return;
  for(const auto pred : findit->second)
    gather_transitive_predecessors(pred, predecessor_map, result);
}
 
static bool is_store_to_slot(
  const java_bytecode_convert_methodt::instructiont &inst,
  unsigned slotidx)
{
  const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic;
 
  if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
    return false;
 
  unsigned storeslotidx;
  if(inst.args.size()==1)
  {
    // Store with an argument:
    const auto &arg=inst.args[0];
    storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
  }
  else
  {
    // Store shorthands, like "store_0", "store_1"
    INVARIANT(
      prevstatement[6]=='_' && prevstatement.size()==8,
      "expected store instruction looks like store_0, store_1...");
    std::string storeslot(1, prevstatement[7]);
    INVARIANT(
      isdigit(storeslot[0]),
      "store_? instructions should end in a digit");
    storeslotidx=safe_string2unsigned(storeslot);
  }
  return storeslotidx==slotidx;
}
 
static void maybe_add_hole(
  local_variable_with_holest &var,
  java_bytecode_convert_methodt::method_offsett from,
  java_bytecode_convert_methodt::method_offsett to)
{
  PRECONDITION(to>=from);
  if(to!=from)
    var.holes.push_back(
      {from,
       static_cast<java_bytecode_convert_methodt::method_offsett>(to - from)});
}
 
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)
{
  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
  {
    if(it->var.start_pc+it->var.length>live_variable_at_address.size())
      live_variable_at_address.resize(it->var.start_pc+it->var.length);
 
    for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
        idx != idxlim;
        ++idx)
    {
      INVARIANT(!live_variable_at_address[idx], "Local variable table clash?");
      live_variable_at_address[idx]=&*it;
    }
  }
}
 
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)
{
  messaget msg(msg_handler);
  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
  {
    // All entries of the "local_variable_table_with_holest" processed in this
    // function concern the same Java Local Variable Table slot/register. This
    // is because "find_initializers()" has already sorted them.
    INVARIANT(
      it->var.index==firstvar->var.index,
      "all entries are for the same local variable slot");
 
    // Parameters are irrelevant to us and shouldn't be changed. This is because
    // they cannot have live predecessor ranges: they are initialized by the JVM
    // and no other live variable range can flow into them.
    if(it->is_parameter)
      continue;
 
#ifdef DEBUG
    msg.debug() << "jcm: ppm: processing var idx " << it->var.index
                << " name '" << it->var.name << "' start-pc "
                << it->var.start_pc << " len " << it->var.length
                << "; holes " << it->holes.size() << messaget::eom;
#endif
 
    // Find the last instruction within the live range:
    const auto end_pc = it->var.start_pc + it->var.length;
    auto amapit=amap.find(end_pc);
    INVARIANT(
      amapit!=amap.begin(),
      "current bytecode shall not be the first");
    auto old_amapit=amapit;
    --amapit;
    if(old_amapit==amap.end())
    {
      INVARIANT(
        end_pc>amapit->first,
        "Instruction live range doesn't align to instruction boundary?");
    }
 
    // Find vartable entries that flow into this one. For unknown reasons this
    // loop iterates backwards, walking back from the last bytecode in the live
    // range of variable it to the first one. For each value of the iterator
    // "amapit" we search for instructions that jump into amapit's address
    // (predecessors)
    auto new_start_pc = it->var.start_pc;
    for(; amapit->first>=it->var.start_pc; --amapit)
    {
      for(auto pred : amapit->second.predecessors)
      {
        // pred is the address (byecode offset) of a instruction that jumps into
        // amapit. Compute now a pointer to the variable-with-holes whose index
        // equals that of amapit and which was alive on instruction pred, or a
        // null pointer if no such variable exists (e.g., because no live range
        // covers that instruction)
        auto pred_var=
          (pred<live_variable_at_address.size() ?
           live_variable_at_address[pred] :
           nullptr);
 
        // Three cases are now possible:
        // 1. The predecessor instruction is in the same live range: nothing to
        // do.
        if(pred_var==&*it)
        {
          continue;
        }
        // 2. The predecessor instruction is in no live range among those for
        // variable slot it->var.index
        else if(!pred_var)
        {
          // Check if this is an initializer, and if so expand the live range
          // to include it, but don't check its predecessors:
          auto inst_before_this=amapit;
          INVARIANT(
            inst_before_this!=amap.begin(),
            "we shall not be on the first bytecode of the method");
          --inst_before_this;
          if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
          {
            // These sorts of infeasible edges can occur because jsr
            // handling is presently vague (any subroutine is assumed to
            // be able to return to any callsite)
            msg.warning() << "Local variable table: ignoring flow from "
                          << "out of range for " << it->var.name << ' '
                          << pred << " -> " << amapit->first
                          << messaget::eom;
            continue;
          }
          if(!is_store_to_slot(
               *(inst_before_this->second.source),
               it->var.index))
          {
            msg.warning() << "Local variable table: didn't find initializing "
                          << "store for predecessor of bytecode at address "
                          << amapit->first << " ("
                          << amapit->second.predecessors.size()
                          << " predecessors)" << msg.eom;
            throw "local variable table: unexpected live ranges";
          }
          new_start_pc=pred;
        }
        // 3. Predecessor instruction is a different range associated to the
        // same variable slot
        else
        {
          if(pred_var->var.name!=it->var.name ||
             pred_var->var.descriptor!=it->var.descriptor)
          {
            // These sorts of infeasible edges can occur because
            // jsr handling is presently vague (any subroutine is
            // assumed to be able to return to any callsite)
            msg.warning() << "Local variable table: ignoring flow from "
                          << "clashing variable for "
                          << it->var.name << ' ' << pred << " -> "
                          << amapit->first << messaget::eom;
            continue;
          }
          // OK, this is a flow from a similar but
          // distinct entry in the local var table.
          predecessor_map[&*it].insert(pred_var);
        }
      }
    }
 
    // If a simple pre-block initializer was found,
    // add it to the live range now:
    it->var.length+=(it->var.start_pc-new_start_pc);
    it->var.start_pc=new_start_pc;
  }
}
 
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)
{
  PRECONDITION(!merge_vars.empty());
 
  auto first_pc =
    std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
  for(auto v : merge_vars)
  {
    if(v->var.start_pc<first_pc)
      first_pc=v->var.start_pc;
  }
 
  std::vector<java_bytecode_convert_methodt::method_offsett>
    candidate_dominators;
  for(auto v : merge_vars)
  {
    const auto &dominator_nodeidx=
      dominator_analysis.cfg.entry_map.at(v->var.start_pc);
    const auto &this_var_doms=
      dominator_analysis.cfg[dominator_nodeidx].dominators;
    for(const auto this_var_dom : this_var_doms)
      if(this_var_dom<=first_pc)
        candidate_dominators.push_back(this_var_dom);
  }
  std::sort(candidate_dominators.begin(), candidate_dominators.end());
 
  // Working from the back, simply find the first PC
  // that occurs merge_vars.size() times and therefore
  // dominates all vars we seek to merge:
  for(auto domit=candidate_dominators.rbegin(),
        domitend=candidate_dominators.rend();
      domit!=domitend;
      /* Don't increment here */)
  {
    std::size_t repeats = 0;
    auto dom=*domit;
    while(domit!=domitend && *domit==dom)
    {
      ++domit;
      ++repeats;
    }
    assert(repeats<=merge_vars.size());
    if(repeats==merge_vars.size())
      return dom;
  }
 
  throw "variable live ranges with no common dominator?";
}
 
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)
{
  std::vector<local_variable_with_holest *> sorted_by_startpc(
    merge_vars.begin(), merge_vars.end());
  std::sort(sorted_by_startpc.begin(), sorted_by_startpc.end(), lt_startpc);
 
  PRECONDITION(!sorted_by_startpc.empty());
  maybe_add_hole(
    merge_into,
    expanded_live_range_start,
    sorted_by_startpc[0]->var.start_pc);
  for(auto it = std::next(sorted_by_startpc.begin());
      it != sorted_by_startpc.end();
      ++it)
  {
    auto &local_var = (*std::prev(it))->var;
    maybe_add_hole(
      merge_into, local_var.start_pc + local_var.length, (*it)->var.start_pc);
  }
}
 
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)
{
  // Because we need a lexically-scoped declaration,
  // we must have the merged variable
  // enter scope both in a block that dominates all entries, and which
  // precedes them in program order.
  const auto found_dominator =
    get_common_dominator(merge_vars, dominator_analysis);
 
  // Populate the holes in the live range
  // (addresses where the new variable will be in scope,
  // but references to this stack slot should not resolve to it
  // as it was not visible in the original local variable table)
  populate_live_range_holes(merge_into, merge_vars, found_dominator);
 
  java_bytecode_convert_methodt::method_offsett last_pc = 0;
  for(auto v : merge_vars)
  {
    if(v->var.start_pc+v->var.length>last_pc)
      last_pc=v->var.start_pc+v->var.length;
  }
 
  // Apply the changes:
  merge_into.var.start_pc=found_dominator;
  merge_into.var.length=last_pc-found_dominator;
 
#ifdef DEBUG
  debug_out << "Merged " << merge_vars.size() << " variables named "
            << merge_into.var.name << "; new live range "
            << merge_into.var.start_pc << '-'
            << merge_into.var.start_pc + merge_into.var.length << '\n';
#else
  (void)debug_out; // unused parameter
#endif
 
  // Nuke the now-subsumed var-table entries:
  for(auto &v : merge_vars)
    if(v!=&merge_into)
      v->var.length=0;
}
 
void java_bytecode_convert_methodt::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 &dominator_analysis)
{
  // Build a simple map from instruction PC to the variable
  // live in this slot at that PC, and a map from each variable
  // to variables that flow into it:
  std::vector<local_variable_with_holest *> live_variable_at_address;
  populate_variable_address_map(firstvar, varlimit, live_variable_at_address);
 
  // Now find variables that flow together by
  // walking backwards to find initializers
  // or branches from other live ranges:
  predecessor_mapt predecessor_map;
  populate_predecessor_map(
    firstvar,
    varlimit,
    live_variable_at_address,
    amap,
    predecessor_map,
    log.get_message_handler());
 
  // OK, we've established the flows all seem sensible.
  // Now merge vartable entries according to the predecessor_map:
 
  // Take the transitive closure of the predecessor map:
  for(auto &kv : predecessor_map)
  {
    std::set<local_variable_with_holest *> closed_preds;
    gather_transitive_predecessors(kv.first, predecessor_map, closed_preds);
    kv.second=std::move(closed_preds);
  }
 
  // Top-sort so that we get the bottom variables first:
  is_predecessor_oft comp(predecessor_map);
  std::vector<local_variable_with_holest *> topsorted_vars;
  for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
    topsorted_vars.push_back(&*it);
 
  std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);
 
  // Now merge the entries:
  for(auto merge_into : topsorted_vars)
  {
    // Already merged into another variable?
    if(merge_into->var.length==0)
      continue;
 
    auto findit=predecessor_map.find(merge_into);
    // Nothing to do?
    if(findit==predecessor_map.end())
      continue;
 
    const auto &merge_vars=findit->second;
    INVARIANT(merge_vars.size()>=2, "merging requires at least 2 variables");
 
    merge_variable_table_entries(
      *merge_into, merge_vars, dominator_analysis, log.status());
  }
}
 
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)
{
  if(it2==itend)
  {
    it1=itend;
    return;
  }
 
  auto old_it2=it2;
  auto index=it2->var.index;
  while(it2!=itend && it2->var.index==index)
    ++it2;
  it1=old_it2;
}
 
void java_bytecode_convert_methodt::find_initializers(
  local_variable_table_with_holest &vars,
  const address_mapt &amap,
  const java_cfg_dominatorst &dominator_analysis)
{
  // Sort table entries by local slot index:
  std::sort(vars.begin(), vars.end(), lt_index);
 
  // For each block of entries using a particular index,
  // try to combine them:
  auto it1=vars.begin();
  auto it2=it1;
  auto itend=vars.end();
  walk_to_next_index(it1, it2, itend);
  for(; it1!=itend; walk_to_next_index(it1, it2, itend))
    find_initializers_for_slot(it1, it2, amap, dominator_analysis);
}
 
static void cleanup_var_table(
  std::vector<local_variable_with_holest> &vars_with_holes)
{
  size_t toremove=0;
  for(size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
  {
    auto &v=vars_with_holes[i];
    if(v.var.length==0)
    {
      // Move to end; consider the new element we've swapped in:
      ++toremove;
      if(i!=vars_with_holes.size()-toremove) // Already where it needs to be?
        std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
      --i; // May make i (size_t)-1, but it will immediately be
           // re-incremented as the loop iterates.
    }
  }
 
  // Remove un-needed entries.
  vars_with_holes.resize(vars_with_holes.size()-toremove);
}
 
void java_bytecode_convert_methodt::setup_local_variables(
  const methodt &m,
  const address_mapt &amap)
{
  // Compute CFG dominator tree
  java_cfg_dominatorst dominator_analysis;
  method_with_amapt dominator_args(m, amap);
  dominator_analysis(dominator_args);
 
#ifdef DEBUG
  log.debug() << "jcm: setup-local-vars: m.is_static " << m.is_static
              << " m.descriptor " << m.descriptor << messaget::eom;
  log.debug() << "jcm: setup-local-vars: lv arg slots " << slots_for_parameters
              << messaget::eom;
  log.debug() << "jcm: setup-local-vars: lvt size "
              << m.local_variable_table.size() << messaget::eom;
#endif
 
  // Find out which local variable table entries should be merged:
  // Wrap each entry so we have a data structure to work during function calls,
  // where we record live ranges with holes:
  std::vector<local_variable_with_holest> vars_with_holes;
  for(const auto &v : m.local_variable_table)
    vars_with_holes.push_back({v, is_parameter(v), {}});
 
  // Merge variable records. See documentation of in
  // `find_initializers_for_slot` for more details. If the strategy employed
  // there fails with an exception, we just ignore the LVT for this method, no
  // variable is generated in `this->variables[]` (because we return here and
  // dont let the for loop below to execute), and as a result the method
  // this->variable() will be forced to create new `anonlocal::` variables, as
  // the only source of variable names for that method is `this->variables[]`.
  try
  {
    find_initializers(vars_with_holes, amap, dominator_analysis);
  }
  catch(const char *message)
  {
    log.warning() << "Bytecode -> codet translation error: " << message
                  << messaget::eom
                  << "This is probably due to an unexpected LVT, "
                  << "falling back to translation without LVT" << messaget::eom;
    return;
  }
 
  // Clean up removed records from the variable table:
  cleanup_var_table(vars_with_holes);
 
  // Do the locals and parameters in the variable table, which is available when
  // compiled with -g or for methods with many local variables in the latter
  // case, different variables can have the same index, depending on the
  // context.
  //
  // to calculate which variable to use, one uses the address of the instruction
  // that uses the variable, the size of the instruction and the start_pc /
  // length values in the local variable table
  for(auto &v : vars_with_holes)
  {
    if(v.is_parameter)
      continue;
 
#ifdef DEBUG
    log.debug() << "jcm: setup-local-vars: merged variable: idx " << v.var.index
                << " name " << v.var.name << " v.var.descriptor '"
                << v.var.descriptor << "' holes " << v.holes.size()
                << messaget::eom;
#endif
 
    const std::string &method_name = id2string(method_id);
    const size_t method_name_end = method_name.rfind(":(");
    const size_t class_name_end = method_name.rfind('.', method_name_end);
    INVARIANT(
      method_name_end != std::string::npos &&
        class_name_end != std::string::npos,
      "A method name has the format class `.` method `:(`signature`)`.");
    const std::string class_name = method_name.substr(0, class_name_end);
 
    const typet t = v.var.signature.has_value()
                      ? *java_type_from_string_with_exception(
                          v.var.descriptor, v.var.signature, class_name)
                      : *java_type_from_string(v.var.descriptor);
 
    std::ostringstream id_oss;
    id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;
    irep_idt identifier(id_oss.str());
    symbol_exprt result(identifier, t);
    result.set(ID_C_base_name, v.var.name);
 
    // Create a new local variable in the variables[] array, the result of
    // merging multiple local variables with equal name (parameters excluded)
    // into a single local variable with holes
    variables[v.var.index].emplace_back(
      result, v.var.start_pc, v.var.length, false, std::move(v.holes));
 
    // Register the local variable in the symbol table
    symbolt new_symbol;
    new_symbol.name=identifier;
    new_symbol.type=t;
    new_symbol.base_name=v.var.name;
    new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
    new_symbol.mode=ID_java;
    new_symbol.is_type=false;
    new_symbol.is_file_local=true;
    new_symbol.is_thread_local=true;
    new_symbol.is_lvalue=true;
    symbol_table.add(new_symbol);
  }
}
 
const java_bytecode_convert_methodt::variablet &
java_bytecode_convert_methodt::find_variable_for_slot(
  size_t address,
  variablest &var_list)
{
  for(const variablet &var : var_list)
  {
    size_t start_pc=var.start_pc;
    size_t length=var.length;
    if(address>=start_pc && address<(start_pc+length))
    {
      bool found_hole=false;
      for(auto &hole : var.holes)
        if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
        {
          found_hole=true;
          break;
        }
      if(found_hole)
        continue;
      return var;
    }
  }
  // add unnamed local variable to end of list at this index
  // with scope from 0 to SIZE_T_MAX
  // as it is at the end of the vector, it will only be taken into account
  // if no other variable is valid
  var_list.emplace_back(
    symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits<size_t>::max());
  return var_list.back();
}