33 cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
50 const auto &method=args.first;
51 const auto &amap=args.second;
52 for(
const auto &inst : amap)
57 (*this)[entry_map[inst.first]].PC=inst.first;
60 for(
const auto &inst : amap)
62 for(
auto succ : inst.second.successors)
67 for(
const auto &table_entry : method.exception_table)
69 auto findit=amap.find(table_entry.start_pc);
72 "Exception table entry doesn't point to an instruction?");
73 for(; findit->first<table_entry.end_pc; ++findit)
79 if(succit==amap.end())
81 const auto &thisinst=findit->second;
82 if(thisinst.successors.size()==1 &&
83 thisinst.successors.back()==succit->first)
86 entry_map.at(findit->first),
113 return args.second.begin()->first;
119 return (--args.second.end())->first;
124 return args.second.empty();
159 std::set<local_variable_with_holest *> >
172 auto findit=
order.find(a);
173 if(findit==
order.end())
175 return findit->second.count(b)>0;
189 std::set<local_variable_with_holest*> &result)
191 if(!result.insert(start).second)
193 auto findit=predecessor_map.find(start);
194 if(findit==predecessor_map.end())
196 for(
const auto pred : findit->second)
211 if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)==
"store"))
214 unsigned storeslotidx;
215 if(inst.
args.size()==1)
218 const auto &arg=inst.
args[0];
225 prevstatement[6]==
'_' && prevstatement.size()==8,
226 "expected store instruction looks like store_0, store_1...");
227 std::string storeslot(1, prevstatement[7]);
229 isdigit(storeslot[0]),
230 "store_? instructions should end in a digit");
233 return storeslotidx==slotidx;
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)
264 for(
auto it=firstvar, itend=varlimit; it!=itend; ++it)
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);
269 for(
auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
273 INVARIANT(!live_variable_at_address[idx],
"Local variable table clash?");
274 live_variable_at_address[idx]=&*it;
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,
313 for(
auto it=firstvar, itend=varlimit; it!=itend; ++it)
319 it->var.index==firstvar->var.index,
320 "all entries are for the same local variable slot");
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
336 const auto end_pc = it->var.start_pc + it->var.length;
337 auto amapit=amap.find(end_pc);
339 amapit!=amap.begin(),
340 "current bytecode shall not be the first");
341 auto old_amapit=amapit;
343 if(old_amapit==amap.end())
346 end_pc>amapit->first,
347 "Instruction live range doesn't align to instruction boundary?");
355 auto new_start_pc = it->var.start_pc;
356 for(; amapit->first>=it->var.start_pc; --amapit)
358 for(
auto pred : amapit->second.predecessors)
366 (pred<live_variable_at_address.size() ?
367 live_variable_at_address[pred] :
383 auto inst_before_this=amapit;
385 inst_before_this!=amap.begin(),
386 "we shall not be on the first bytecode of the method");
388 if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
393 msg.
warning() <<
"Local variable table: ignoring flow from "
394 <<
"out of range for " << it->var.name <<
' '
395 << pred <<
" -> " << amapit->first
400 *(inst_before_this->second.source),
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";
416 if(pred_var->var.name!=it->var.name ||
417 pred_var->var.descriptor!=it->var.descriptor)
422 msg.
warning() <<
"Local variable table: ignoring flow from "
423 <<
"clashing variable for "
424 << it->var.name <<
' ' << pred <<
" -> "
430 predecessor_map[&*it].insert(pred_var);
437 it->var.length+=(it->var.start_pc-new_start_pc);
438 it->var.start_pc=new_start_pc;
450 const std::set<local_variable_with_holest *> &merge_vars,
456 std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
457 for(
auto v : merge_vars)
459 if(v->var.start_pc<first_pc)
460 first_pc=v->var.start_pc;
463 std::vector<java_bytecode_convert_methodt::method_offsett>
464 candidate_dominators;
465 for(
auto v : merge_vars)
467 const auto &dominator_nodeidx=
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);
475 std::sort(candidate_dominators.begin(), candidate_dominators.end());
480 for(
auto domit=candidate_dominators.rbegin(),
481 domitend=candidate_dominators.rend();
485 std::size_t repeats = 0;
487 while(domit!=domitend && *domit==dom)
492 assert(repeats<=merge_vars.size());
493 if(repeats==merge_vars.size())
497 throw "variable live ranges with no common dominator?";
510 const std::set<local_variable_with_holest *> &merge_vars,
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);
519 expanded_live_range_start,
520 sorted_by_startpc[0]->var.start_pc);
522 idx < sorted_by_startpc.size() - 1;
527 sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->
var.
length,
528 sorted_by_startpc[idx+1]->var.start_pc);
542 const std::set<local_variable_with_holest *> &merge_vars,
544 std::ostream &debug_out)
550 const auto found_dominator =
560 for(
auto v : merge_vars)
562 if(v->var.start_pc+v->var.length>last_pc)
563 last_pc=v->var.start_pc+v->var.length;
568 merge_into.
var.
length=last_pc-found_dominator;
571 debug_out <<
"Merged " << merge_vars.size() <<
" variables named "
572 << merge_into.
var.
name <<
"; new live range "
580 for(
auto &v : merge_vars)
599 local_variable_table_with_holest::iterator firstvar,
600 local_variable_table_with_holest::iterator varlimit,
607 std::vector<local_variable_with_holest *> live_variable_at_address;
617 live_variable_at_address,
626 for(
auto &kv : predecessor_map)
628 std::set<local_variable_with_holest *> closed_preds;
630 kv.second=std::move(closed_preds);
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);
639 std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);
642 for(
auto merge_into : topsorted_vars)
645 if(merge_into->var.length==0)
648 auto findit=predecessor_map.find(merge_into);
650 if(findit==predecessor_map.end())
653 const auto &merge_vars=findit->second;
654 INVARIANT(merge_vars.size()>=2,
"merging requires at least 2 variables");
657 *merge_into, merge_vars, dominator_analysis,
log.
status());
669 local_variable_table_with_holest::iterator &it1,
670 local_variable_table_with_holest::iterator &it2,
671 local_variable_table_with_holest::iterator itend)
680 auto index=it2->var.index;
681 while(it2!=itend && it2->var.index==index)
698 std::sort(vars.begin(), vars.end(),
lt_index);
702 auto it1=vars.begin();
704 auto itend=vars.end();
714 std::vector<local_variable_with_holest> &vars_with_holes)
717 for(
size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
719 auto &v=vars_with_holes[i];
724 if(i!=vars_with_holes.size()-toremove)
725 std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
732 vars_with_holes.resize(vars_with_holes.size()-toremove);
748 dominator_analysis(dominator_args);
755 log.
debug() <<
"jcm: setup-local-vars: lvt size "
762 std::vector<local_variable_with_holest> vars_with_holes;
781 <<
"This is probably due to an unexpected LVT, "
782 <<
"falling back to translation without LVT" <<
messaget::eom;
797 for(
auto &v : vars_with_holes)
803 log.
debug() <<
"jcm: setup-local-vars: merged variable: idx " << v.var.index
804 <<
" name " << v.var.name <<
" v.var.descriptor '"
805 << v.var.descriptor <<
"' holes " << v.holes.size()
810 const size_t method_name_end = method_name.rfind(
":(");
811 const size_t class_name_end = method_name.rfind(
'.', method_name_end);
813 method_name_end != std::string::npos &&
814 class_name_end != std::string::npos,
815 "A method name has the format class `.` method `:(`signature`)`.");
816 const std::string class_name = method_name.substr(0, class_name_end);
818 const typet t = v.var.signature.has_value()
820 v.var.descriptor, v.var.signature, class_name)
823 std::ostringstream id_oss;
824 id_oss <<
method_id <<
"::" << v.var.start_pc <<
"::" << v.var.name;
827 result.
set(ID_C_base_name, v.var.name);
833 result, v.var.start_pc, v.var.length,
false, std::move(v.holes));
837 new_symbol.
name=identifier;
841 new_symbol.
mode=ID_java;
864 size_t length=var.length;
865 if(address>=start_pc && address<(start_pc+length))
867 bool found_hole=
false;
868 for(
auto &hole : var.holes)
869 if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
883 var_list.emplace_back(
885 return var_list.back();
struct bytecode_infot const bytecode_info[]
entryt & at(const goto_programt::const_targett &t)
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A generic directed graph with a parametric node type.
node_indext add_node(arguments &&... values)
void add_edge(node_indext a, node_indext b)
void set(const irep_namet &name, const irep_idt &value)
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
std::vector< variablet > variablest
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void find_initializers(local_variable_table_with_holest &vars, const address_mapt &amap, const java_cfg_dominatorst &doms)
See find_initializers_for_slot above for more detail.
std::vector< local_variable_with_holest > local_variable_table_with_holest
std::pair< const methodt &, const address_mapt & > method_with_amapt
void find_initializers_for_slot(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const address_mapt &amap, const java_cfg_dominatorst &doms)
Given a sequence of users of the same local variable slot, this figures out which ones are related by...
expanding_vectort< variablest > variables
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
std::map< method_offsett, converted_instructiont > address_mapt
symbol_table_baset & symbol_table
irep_idt method_id
Fully qualified name of the method under translation.
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
mstreamt & status() const
message_handlert & get_message_handler()
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
irep_idt mode
Language mode.
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
JAVA Bytecode Language Conversion.
static void maybe_add_hole(local_variable_with_holest &var, java_bytecode_convert_methodt::method_offsett from, java_bytecode_convert_methodt::method_offsett to)
See above.
std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)
java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
static void populate_variable_address_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, std::vector< local_variable_with_holest * > &live_variable_at_address)
See above.
static bool is_store_to_slot(const java_bytecode_convert_methodt::instructiont &inst, unsigned slotidx)
See above.
static void populate_predecessor_map(local_variable_table_with_holest::iterator firstvar, local_variable_table_with_holest::iterator varlimit, const std::vector< local_variable_with_holest * > &live_variable_at_address, const address_mapt &amap, predecessor_mapt &predecessor_map, message_handlert &msg_handler)
Populates the predecessor_map with a graph from local variable table entries to their predecessors (t...
static void populate_live_range_holes(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, java_bytecode_convert_methodt::method_offsett expanded_live_range_start)
See above.
static bool lt_startpc(const local_variable_with_holest *a, const local_variable_with_holest *b)
java_bytecode_convert_methodt::address_mapt address_mapt
java_bytecode_convert_methodt::holet holet
static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)
See above.
static java_bytecode_convert_methodt::method_offsett get_common_dominator(const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis)
Used to find out where to put a variable declaration that subsumes several variable live ranges.
java_bytecode_convert_methodt::local_variable_with_holest local_variable_with_holest
static void walk_to_next_index(local_variable_table_with_holest::iterator &it1, local_variable_table_with_holest::iterator &it2, local_variable_table_with_holest::iterator itend)
Walk a vector, a contiguous block of entries with equal slot index at a time.
static void merge_variable_table_entries(local_variable_with_holest &merge_into, const std::set< local_variable_with_holest * > &merge_vars, const java_cfg_dominatorst &dominator_analysis, std::ostream &debug_out)
See above.
java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest * > &result)
See above.
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
optionalt< typet > java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static const char * message(const statust &status)
Makes a status message string from a status.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
unsigned safe_string2unsigned(const std::string &str, int base)
bool operator()(local_variable_with_holest *a, local_variable_with_holest *b) const
is_predecessor_oft(const predecessor_mapt &_order)
const predecessor_mapt & order
std::vector< holet > holes
local_variable_tablet local_variable_table
procedure_local_cfg_baset()
java_bytecode_convert_methodt::method_with_amapt method_with_amapt
nodet & get_node(const java_bytecode_convert_methodt::method_offsett &instruction)
java_bytecode_convert_methodt::method_offsett get_node_index(const java_bytecode_convert_methodt::method_offsett &instruction) const
std::map< java_bytecode_convert_methodt::method_offsett, java_bytecode_convert_methodt::method_offsett > entry_mapt
static bool nodes_empty(const method_with_amapt &args)
const nodet & get_node(const java_bytecode_convert_methodt::method_offsett &instruction) const
static java_bytecode_convert_methodt::method_offsett get_first_node(const method_with_amapt &args)
grapht< cfg_base_nodet< T, java_bytecode_convert_methodt::method_offsett > > base_grapht
void operator()(const method_with_amapt &args)
static java_bytecode_convert_methodt::method_offsett get_last_node(const method_with_amapt &args)