33 cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
45 const auto &method=args.first;
46 const auto &amap=args.second;
47 for(
const auto &inst : amap)
52 (*this)[entry_map[inst.first]].PC=inst.first;
55 for(
const auto &inst : amap)
57 for(
auto succ : inst.second.successors)
62 for(
const auto &table_entry : method.exception_table)
64 auto findit=amap.find(table_entry.start_pc);
67 "Exception table entry doesn't point to an instruction?");
68 for(; findit->first<table_entry.end_pc; ++findit)
74 if(succit==amap.end())
76 const auto &thisinst=findit->second;
77 if(thisinst.successors.size()==1 &&
78 thisinst.successors.back()==succit->first)
81 entry_map.at(findit->first),
91 return args.second.begin()->first;
97 return (--args.second.end())->first;
102 return args.second.empty();
137 std::set<local_variable_with_holest *> >
150 auto findit=
order.find(a);
151 if(findit==
order.end())
153 return findit->second.count(b)>0;
167 std::set<local_variable_with_holest*> &result)
169 if(!result.insert(start).second)
171 auto findit=predecessor_map.find(start);
172 if(findit==predecessor_map.end())
174 for(
const auto pred : findit->second)
188 if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)==
"store"))
191 unsigned storeslotidx;
192 if(inst.
args.size()==1)
195 const auto &arg=inst.
args[0];
202 prevstatement[6]==
'_' && prevstatement.size()==8,
203 "expected store instruction looks like store_0, store_1...");
204 std::string storeslot(1, prevstatement[7]);
206 isdigit(storeslot[0]),
207 "store_? instructions should end in a digit");
210 return storeslotidx==slotidx;
226 static_cast<java_bytecode_convert_methodt::method_offsett>(to - from)});
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)
241 for(
auto it=firstvar, itend=varlimit; it!=itend; ++it)
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);
246 for(
auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
250 INVARIANT(!live_variable_at_address[idx],
"Local variable table clash?");
251 live_variable_at_address[idx]=&*it;
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,
290 for(
auto it=firstvar, itend=varlimit; it!=itend; ++it)
296 it->var.index==firstvar->var.index,
297 "all entries are for the same local variable slot");
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
313 const auto end_pc = it->var.start_pc + it->var.length;
314 auto amapit=amap.find(end_pc);
316 amapit!=amap.begin(),
317 "current bytecode shall not be the first");
318 auto old_amapit=amapit;
320 if(old_amapit==amap.end())
323 end_pc>amapit->first,
324 "Instruction live range doesn't align to instruction boundary?");
332 auto new_start_pc = it->var.start_pc;
333 for(; amapit->first>=it->var.start_pc; --amapit)
335 for(
auto pred : amapit->second.predecessors)
343 (pred<live_variable_at_address.size() ?
344 live_variable_at_address[pred] :
360 auto inst_before_this=amapit;
362 inst_before_this!=amap.begin(),
363 "we shall not be on the first bytecode of the method");
365 if(amapit->first!=it->var.start_pc || inst_before_this->first!=pred)
370 msg.
warning() <<
"Local variable table: ignoring flow from " 371 <<
"out of range for " << it->var.name <<
' ' 372 << pred <<
" -> " << amapit->first
377 *(inst_before_this->second.source),
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";
393 if(pred_var->var.name!=it->var.name ||
394 pred_var->var.descriptor!=it->var.descriptor)
399 msg.
warning() <<
"Local variable table: ignoring flow from " 400 <<
"clashing variable for " 401 << it->var.name <<
' ' << pred <<
" -> " 407 predecessor_map[&*it].insert(pred_var);
414 it->var.length+=(it->var.start_pc-new_start_pc);
415 it->var.start_pc=new_start_pc;
427 const std::set<local_variable_with_holest *> &merge_vars,
433 std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
434 for(
auto v : merge_vars)
436 if(v->var.start_pc<first_pc)
437 first_pc=v->var.start_pc;
440 std::vector<java_bytecode_convert_methodt::method_offsett>
441 candidate_dominators;
442 for(
auto v : merge_vars)
444 const auto &dominator_nodeidx=
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);
452 std::sort(candidate_dominators.begin(), candidate_dominators.end());
457 for(
auto domit=candidate_dominators.rbegin(),
458 domitend=candidate_dominators.rend();
462 std::size_t repeats = 0;
464 while(domit!=domitend && *domit==dom)
469 assert(repeats<=merge_vars.size());
470 if(repeats==merge_vars.size())
474 throw "variable live ranges with no common dominator?";
487 const std::set<local_variable_with_holest *> &merge_vars,
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);
496 expanded_live_range_start,
497 sorted_by_startpc[0]->var.start_pc);
499 idx < sorted_by_startpc.size() - 1;
504 sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->
var.
length,
505 sorted_by_startpc[idx+1]->var.start_pc);
519 const std::set<local_variable_with_holest *> &merge_vars,
521 std::ostream &debug_out)
527 const auto found_dominator =
537 for(
auto v : merge_vars)
539 if(v->var.start_pc+v->var.length>last_pc)
540 last_pc=v->var.start_pc+v->var.length;
545 merge_into.
var.
length=last_pc-found_dominator;
548 debug_out <<
"Merged " << merge_vars.size() <<
" variables named " 549 << merge_into.
var.
name <<
"; new live range " 557 for(
auto &v : merge_vars)
576 local_variable_table_with_holest::iterator firstvar,
577 local_variable_table_with_holest::iterator varlimit,
584 std::vector<local_variable_with_holest *> live_variable_at_address;
594 live_variable_at_address,
603 for(
auto &kv : predecessor_map)
605 std::set<local_variable_with_holest *> closed_preds;
607 kv.second=std::move(closed_preds);
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);
616 std::sort(topsorted_vars.begin(), topsorted_vars.end(), comp);
619 for(
auto merge_into : topsorted_vars)
622 if(merge_into->var.length==0)
625 auto findit=predecessor_map.find(merge_into);
627 if(findit==predecessor_map.end())
630 const auto &merge_vars=findit->second;
631 INVARIANT(merge_vars.size()>=2,
"merging requires at least 2 variables");
649 local_variable_table_with_holest::iterator &it1,
650 local_variable_table_with_holest::iterator &it2,
651 local_variable_table_with_holest::iterator itend)
660 auto index=it2->var.index;
661 while(it2!=itend && it2->var.index==index)
678 std::sort(vars.begin(), vars.end(),
lt_index);
682 auto it1=vars.begin();
684 auto itend=vars.end();
694 std::vector<local_variable_with_holest> &vars_with_holes)
697 for(
size_t i=0; i<(vars_with_holes.size()-toremove); ++i)
699 auto &v=vars_with_holes[i];
704 if(i!=vars_with_holes.size()-toremove)
705 std::swap(v, vars_with_holes[vars_with_holes.size()-toremove]);
712 vars_with_holes.resize(vars_with_holes.size()-toremove);
728 dominator_analysis(dominator_args);
731 debug() <<
"jcm: setup-local-vars: m.is_static " 733 debug() <<
"jcm: setup-local-vars: lv arg slots " 735 debug() <<
"jcm: setup-local-vars: lvt size " 742 std::vector<local_variable_with_holest> vars_with_holes;
757 catch(
const char *message)
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;
776 for(
const auto &v : vars_with_holes)
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;
788 const size_t method_name_end = method_name.rfind(
":(");
789 const size_t class_name_end = method_name.rfind(
'.', method_name_end);
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);
796 const typet t = v.var.signature.has_value()
798 v.var.descriptor, v.var.signature, class_name)
801 std::ostringstream id_oss;
802 id_oss <<
method_id <<
"::" << v.var.start_pc <<
"::" << v.var.name;
805 result.set(ID_C_base_name, v.var.name);
811 auto &newv=
variables[v.var.index].back();
813 newv.start_pc=v.var.start_pc;
814 newv.length=v.var.length;
815 newv.holes=std::move(v.holes);
819 new_symbol.
name=identifier;
823 new_symbol.
mode=ID_java;
846 size_t length=var.length;
847 if(address>=start_pc && address<(start_pc+length))
849 bool found_hole=
false;
850 for(
auto &hole : var.holes)
851 if(address>=hole.start_pc && address<(hole.start_pc+hole.length))
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];
The type of an expression, extends irept.
irep_idt name
The unique identifier.
java_bytecode_convert_methodt::method_offsett get_last_node(const method_with_amapt &args) const
java_bytecode_convert_methodt::address_mapt address_mapt
A generic directed graph with a parametric node type.
static void gather_transitive_predecessors(local_variable_with_holest *start, const predecessor_mapt &predecessor_map, std::set< local_variable_with_holest * > &result)
See above.
JAVA Bytecode Language Conversion.
const std::string & id2string(const irep_idt &d)
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.
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 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.
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
procedure_local_cfg_baset()
irep_idt pretty_name
Language-specific display name.
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.
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...
expanding_vectort< variablest > variables
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 'invariant_violated_string'.
java_bytecode_convert_methodt::method_with_amapt method_with_amapt
mstreamt & warning() const
std::vector< local_variable_with_holest > local_variable_table_with_holest
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.
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.
std::vector< holet > holes
java_bytecode_convert_methodt::holet holet
bool nodes_empty(const method_with_amapt &args) const
std::map< local_variable_with_holest *, std::set< local_variable_with_holest * > > predecessor_mapt
#define PRECONDITION(CONDITION)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
java_bytecode_convert_methodt::local_variable_with_holest local_variable_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.
unsigned safe_string2unsigned(const std::string &str, int base)
java_bytecode_convert_methodt::java_cfg_dominatorst java_cfg_dominatorst
typet type
Type of symbol.
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()
static void cleanup_var_table(std::vector< local_variable_with_holest > &vars_with_holes)
See above.
std::vector< variablet > variablest
bool operator()(local_variable_with_holest *a, local_variable_with_holest *b) const
mstreamt & result() const
mstreamt & status() const
irep_idt base_name
Base (non-scoped) name.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
void add_edge(node_indext a, node_indext b)
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.
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...
symbol_table_baset & symbol_table
Expression to hold a symbol (variable)
static bool lt_index(const local_variable_with_holest &a, const local_variable_with_holest &b)
void operator()(const method_with_amapt &args)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
java_bytecode_convert_methodt::method_offsett get_first_node(const method_with_amapt &args) const
is_predecessor_oft(const predecessor_mapt &_order)
std::map< method_offsett, converted_instructiont > address_mapt
local_variable_tablet local_variable_table
java_bytecode_convert_methodt::local_variable_table_with_holest local_variable_table_with_holest
void push_back(const T &t)
const predecessor_mapt & order