diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 668b2c1e02b..a7ef1df5fdb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -714,9 +714,9 @@ void java_bytecode_convert_methodt::replace_goto_target( code_blockt &java_bytecode_convert_methodt::get_block_for_pcrange( block_tree_nodet &tree, code_blockt &this_block, - unsigned address_start, - unsigned address_limit, - unsigned next_block_start_address) + method_offsett address_start, + method_offsett address_limit, + method_offsett next_block_start_address) { address_mapt dummy; return get_or_create_block_for_pcrange( @@ -746,9 +746,9 @@ code_blockt &java_bytecode_convert_methodt::get_block_for_pcrange( code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( block_tree_nodet &tree, code_blockt &this_block, - unsigned address_start, - unsigned address_limit, - unsigned next_block_start_address, + method_offsett address_start, + method_offsett address_limit, + method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge) { @@ -778,10 +778,9 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( tree.branch_addresses.begin(), tree.branch_addresses.end(), address_limit); - unsigned findlim_block_start_address= - findlim==tree.branch_addresses.end() ? - next_block_start_address : - (*findlim); + const auto findlim_block_start_address = + findlim == tree.branch_addresses.end() ? next_block_start_address + : (*findlim); // If all children are in scope, return this. if(findstart==tree.branch_addresses.begin() && @@ -924,7 +923,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange( } static void gather_symbol_live_ranges( - unsigned pc, + java_bytecode_convert_methodt::method_offsett pc, const exprt &e, std::map &result) { @@ -1002,9 +1001,9 @@ codet java_bytecode_convert_methodt::convert_instructions( // first pass: get targets and map addresses to instructions address_mapt address_map; - std::set targets; + std::set targets; - std::vector jsr_ret_targets; + std::vector jsr_ret_targets; std::vector ret_instructions; for(auto i_it = instructions.begin(); i_it != instructions.end(); i_it++) @@ -1049,9 +1048,9 @@ codet java_bytecode_convert_methodt::convert_instructions( (threading_support && (i_it->statement=="monitorenter" || i_it->statement=="monitorexit"))) { - const std::vector handler = + const std::vector handler = try_catch_handler(i_it->address, method.exception_table); - std::list &successors = a_entry.first->second.successors; + std::list &successors = a_entry.first->second.successors; successors.insert(successors.end(), handler.begin(), handler.end()); targets.insert(handler.begin(), handler.end()); } @@ -1110,7 +1109,7 @@ codet java_bytecode_convert_methodt::convert_instructions( for(const auto &address : address_map) { - for(unsigned s : address.second.successors) + for(auto s : address.second.successors) { const auto a_it = address_map.find(s); CHECK_RETURN(a_it != address_map.end()); @@ -1128,7 +1127,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // (these require the graph to determine live ranges) setup_local_variables(method, address_map); - std::set working_set; + std::set working_set; if(!instructions.empty()) working_set.insert(instructions.front().address); @@ -1139,7 +1138,7 @@ codet java_bytecode_convert_methodt::convert_instructions( auto address_it = address_map.find(*cur); CHECK_RETURN(address_it != address_map.end()); auto &instruction = address_it->second; - unsigned cur_pc=*cur; + const method_offsett cur_pc = *cur; working_set.erase(cur); if(instruction.done) @@ -1698,7 +1697,7 @@ codet java_bytecode_convert_methodt::convert_instructions( push(results); instruction.done = true; - for(const unsigned address : instruction.successors) + for(const auto address : instruction.successors) { address_mapt::iterator a_it2=address_map.find(address); CHECK_RETURN(a_it2 != address_map.end()); @@ -1807,10 +1806,10 @@ codet java_bytecode_convert_methodt::convert_instructions( // constructs as variable live-ranges require next. bool start_new_block=true; bool has_seen_previous_address=false; - unsigned previous_address=0; + method_offsett previous_address = 0; for(const auto &address_pair : address_map) { - const unsigned address=address_pair.first; + const method_offsett address = address_pair.first; assert(address_pair.first==address_pair.second.source->address); const codet &c=address_pair.second.code; @@ -1890,8 +1889,8 @@ codet java_bytecode_convert_methodt::convert_instructions( root, root_block, v.start_pc, - v.start_pc+v.length, - std::numeric_limits::max(), + v.start_pc + v.length, + std::numeric_limits::max(), address_map); } for(const auto vp : vars_to_process) @@ -1902,12 +1901,12 @@ codet java_bytecode_convert_methodt::convert_instructions( // Skip anonymous variables: if(v.symbol_expr.get_identifier().empty()) continue; - auto &block=get_block_for_pcrange( + auto &block = get_block_for_pcrange( root, root_block, v.start_pc, - v.start_pc+v.length, - std::numeric_limits::max()); + v.start_pc + v.length, + std::numeric_limits::max()); code_declt d(v.symbol_expr); block.operands().insert(block.operands().begin(), d); } @@ -1963,7 +1962,9 @@ codet java_bytecode_convert_methodt::convert_switch( // to the jump target of the tableswitch/lookupswitch case at // hand. Therefore we consider this code to belong to the source bytecode // instruction and not the target instruction. - code_case.code() = code_gotot(label(integer2string(number))); + const method_offsett label_number = + numeric_cast_v(number); + code_case.code() = code_gotot(label(std::to_string(label_number))); code_case.code().add_source_location() = location; if(a_it == args.begin()) @@ -2338,8 +2339,8 @@ void java_bytecode_convert_methodt::convert_athrow( codet &java_bytecode_convert_methodt::do_exception_handling( const java_bytecode_convert_methodt::methodt &method, - const std::set &working_set, - unsigned int cur_pc, + const std::set &working_set, + method_offsett cur_pc, codet &c) { std::vector exception_ids; @@ -2350,8 +2351,8 @@ codet &java_bytecode_convert_methodt::do_exception_handling( // together with a list of all the exception ids // be aware of different try-catch blocks with the same starting pc - std::size_t pos = 0; - std::size_t end_pc = 0; + method_offsett pos = 0; + method_offsett end_pc = 0; while(pos < method.exception_table.size()) { // check if this is the beginning of a try block @@ -2722,7 +2723,7 @@ codet java_bytecode_convert_methodt::convert_iinc( const exprt &arg0, const exprt &arg1, const source_locationt &location, - const unsigned address) + const method_offsett address) { code_blockt block; block.add_source_location() = location; @@ -2756,9 +2757,10 @@ codet java_bytecode_convert_methodt::convert_ifnull( const typecast_exprt lhs(op[0], java_reference_type(empty_typet())); const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond() = binary_relation_exprt(lhs, ID_equal, rhs); - code_branch.then_case() = code_gotot(label(integer2string(number))); + const method_offsett label_number = numeric_cast_v(number); + code_branch.then_case() = code_gotot(label(std::to_string(label_number))); code_branch.then_case().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + address_map.at(label_number).source->source_location; code_branch.add_source_location() = location; return code_branch; } @@ -2773,9 +2775,10 @@ codet java_bytecode_convert_methodt::convert_ifnonull( const typecast_exprt lhs(op[0], java_reference_type(empty_typet())); const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); code_branch.cond() = binary_relation_exprt(lhs, ID_notequal, rhs); - code_branch.then_case() = code_gotot(label(integer2string(number))); + const method_offsett label_number = numeric_cast_v(number); + code_branch.then_case() = code_gotot(label(std::to_string(label_number))); code_branch.then_case().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + address_map.at(label_number).source->source_location; code_branch.add_source_location() = location; return code_branch; } @@ -2792,9 +2795,10 @@ codet java_bytecode_convert_methodt::convert_if( binary_relation_exprt(op[0], id, from_integer(0, op[0].type())); code_branch.cond().add_source_location() = location; code_branch.cond().add_source_location().set_function(method_id); - code_branch.then_case() = code_gotot(label(integer2string(number))); + const method_offsett label_number = numeric_cast_v(number); + code_branch.then_case() = code_gotot(label(std::to_string(label_number))); code_branch.then_case().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + address_map.at(label_number).source->source_location; code_branch.then_case().add_source_location().set_function(method_id); code_branch.add_source_location() = location; code_branch.add_source_location().set_function(method_id); @@ -2821,19 +2825,20 @@ codet java_bytecode_convert_methodt::convert_if_cmp( code_branch.cond() = condition; code_branch.cond().add_source_location() = location; - code_branch.then_case() = code_gotot(label(integer2string(number))); + const method_offsett label_number = numeric_cast_v(number); + code_branch.then_case() = code_gotot(label(std::to_string(label_number))); code_branch.then_case().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + address_map.at(label_number).source->source_location; code_branch.add_source_location() = location; return code_branch; } code_blockt java_bytecode_convert_methodt::convert_ret( - const std::vector &jsr_ret_targets, + const std::vector &jsr_ret_targets, const exprt &arg0, const source_locationt &location, - const unsigned address) + const method_offsett address) { code_blockt c; auto retvar = variable(arg0, 'a', address, NO_CAST); @@ -2885,7 +2890,7 @@ codet java_bytecode_convert_methodt::convert_store( const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, - const unsigned address, + const method_offsett address, const source_locationt &location) { const exprt var = variable(arg0, statement[0], address, NO_CAST); @@ -2974,7 +2979,7 @@ optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr( java_bytecode_convert_methodt::address_mapt &address_map, - const std::vector &jsr_ret_targets, + const std::vector &jsr_ret_targets, const std::vector< std::vector::const_iterator> &ret_instructions) const @@ -2988,12 +2993,13 @@ void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr( } } -std::vector java_bytecode_convert_methodt::try_catch_handler( - const unsigned int address, +std::vector +java_bytecode_convert_methodt::try_catch_handler( + const method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const { - std::vector result; + std::vector result; for(const auto &exception_row : exception_table) { if(address >= exception_row.start_pc && address < exception_row.end_pc) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 5fef054e04c..1fab903bc2e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -65,6 +65,8 @@ class java_bytecode_convert_methodt:public messaget convert(class_symbol, method); } + typedef uint16_t method_offsett; + protected: symbol_table_baset &symbol_table; const size_t max_array_length; @@ -89,13 +91,13 @@ class java_bytecode_convert_methodt:public messaget /// Number of local variable slots used by the JVM to pass parameters upon /// invocation of the method under translation. /// Initialized in `convert`. - unsigned slots_for_parameters; + method_offsett slots_for_parameters; public: struct holet { - unsigned start_pc; - unsigned length; + method_offsett start_pc; + method_offsett length; }; struct local_variable_with_holest @@ -191,17 +193,17 @@ class java_bytecode_convert_methodt:public messaget } instructionst::const_iterator source; - std::list successors; - std::set predecessors; + std::list successors; + std::set predecessors; codet code; stackt stack; bool done; }; public: - typedef std::map address_mapt; + typedef std::map address_mapt; typedef std::pair method_with_amapt; - typedef cfg_dominators_templatet + typedef cfg_dominators_templatet java_cfg_dominatorst; protected: @@ -221,7 +223,7 @@ class java_bytecode_convert_methodt:public messaget struct block_tree_nodet { bool leaf; - std::vector branch_addresses; + std::vector branch_addresses; std::vector branch; block_tree_nodet() : leaf(false) @@ -246,16 +248,16 @@ class java_bytecode_convert_methodt:public messaget code_blockt &get_block_for_pcrange( block_tree_nodet &tree, code_blockt &this_block, - unsigned address_start, - unsigned address_limit, - unsigned next_block_start_address); + method_offsett address_start, + method_offsett address_limit, + method_offsett next_block_start_address); code_blockt &get_or_create_block_for_pcrange( block_tree_nodet &tree, code_blockt &this_block, - unsigned address_start, - unsigned address_limit, - unsigned next_block_start_address, + method_offsett address_start, + method_offsett address_limit, + method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge = true); @@ -302,14 +304,14 @@ class java_bytecode_convert_methodt:public messaget code_blockt &, exprt &); - std::vector try_catch_handler( - unsigned int address, + std::vector try_catch_handler( + method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const; void draw_edges_from_ret_to_jsr( address_mapt &address_map, - const std::vector &jsr_ret_targets, + const std::vector &jsr_ret_targets, const std::vector< std::vector::const_iterator> &ret_instructions) const; @@ -328,17 +330,17 @@ class java_bytecode_convert_methodt:public messaget const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, - const unsigned address, + const method_offsett address, const source_locationt &location); exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const; code_blockt convert_ret( - const std::vector &jsr_ret_targets, + const std::vector &jsr_ret_targets, const exprt &arg0, const source_locationt &location, - const unsigned address); + const method_offsett address); codet convert_if_cmp( const java_bytecode_convert_methodt::address_mapt &address_map, @@ -370,7 +372,7 @@ class java_bytecode_convert_methodt:public messaget const exprt &arg0, const exprt &arg1, const source_locationt &location, - unsigned address); + method_offsett address); exprt::operandst &convert_ushr( const irep_idt &statement, @@ -423,8 +425,8 @@ class java_bytecode_convert_methodt:public messaget codet &do_exception_handling( const methodt &method, - const std::set &working_set, - unsigned int cur_pc, + const std::set &working_set, + method_offsett cur_pc, codet &c); void convert_athrow( diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 9d44666f636..8535bb0ade5 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -24,15 +24,18 @@ Author: Chris Smowton, chris.smowton@diffblue.com // 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 +template struct procedure_local_cfg_baset< T, java_bytecode_convert_methodt::method_with_amapt, - unsigned> : - public grapht > + java_bytecode_convert_methodt::method_offsett> + : public grapht< + cfg_base_nodet> { typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt; - typedef std::map entry_mapt; + typedef std::map + entry_mapt; entry_mapt entry_map; procedure_local_cfg_baset() {} @@ -82,12 +85,14 @@ struct procedure_local_cfg_baset< } } - unsigned get_first_node(const method_with_amapt &args) const + java_bytecode_convert_methodt::method_offsett + get_first_node(const method_with_amapt &args) const { return args.second.begin()->first; } - unsigned get_last_node(const method_with_amapt &args) const + java_bytecode_convert_methodt::method_offsett + get_last_node(const method_with_amapt &args) const { return (--args.second.end())->first; } @@ -212,12 +217,14 @@ static bool is_store_to_slot( /// \return Adds a hole to `var`, unless it would be of zero size. static void maybe_add_hole( local_variable_with_holest &var, - unsigned from, - unsigned to) + 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, to-from}); + var.holes.push_back( + {from, + static_cast(to - from)}); } /// See above @@ -237,9 +244,8 @@ static void populate_variable_address_map( 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(unsigned idx=it->var.start_pc, - idxlim=it->var.start_pc+it->var.length; - idx!=idxlim; + 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?"); @@ -303,7 +309,7 @@ static void populate_predecessor_map( #endif // Find the last instruction within the live range: - unsigned end_pc=it->var.start_pc+it->var.length; + const auto end_pc = it->var.start_pc + it->var.length; auto amapit=amap.find(end_pc); INVARIANT( amapit!=amap.begin(), @@ -322,7 +328,7 @@ static void populate_predecessor_map( // 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) - unsigned new_start_pc=it->var.start_pc; + auto new_start_pc = it->var.start_pc; for(; amapit->first>=it->var.start_pc; --amapit) { for(auto pred : amapit->second.predecessors) @@ -417,20 +423,22 @@ static void populate_predecessor_map( /// \return Returns the bytecode address of the closest common dominator of all /// given variable table entries. In the worst case the function entry point /// should always satisfy this criterion. -static unsigned get_common_dominator( - const std::set &merge_vars, +static java_bytecode_convert_methodt::method_offsett get_common_dominator( + const std::set &merge_vars, const java_cfg_dominatorst &dominator_analysis) { PRECONDITION(!merge_vars.empty()); - unsigned first_pc=UINT_MAX; + auto first_pc = + std::numeric_limits::max(); for(auto v : merge_vars) { if(v->var.start_pcvar.start_pc; } - std::vector candidate_dominators; + std::vector + candidate_dominators; for(auto v : merge_vars) { const auto &dominator_nodeidx= @@ -451,7 +459,7 @@ static unsigned get_common_dominator( domit!=domitend; /* Don't increment here */) { - unsigned repeats=0; + std::size_t repeats = 0; auto dom=*domit; while(domit!=domitend && *domit==dom) { @@ -477,7 +485,7 @@ static unsigned get_common_dominator( static void populate_live_range_holes( local_variable_with_holest &merge_into, const std::set &merge_vars, - unsigned expanded_live_range_start) + java_bytecode_convert_methodt::method_offsett expanded_live_range_start) { std::vector sorted_by_startpc( merge_vars.begin(), merge_vars.end()); @@ -487,7 +495,9 @@ static void populate_live_range_holes( merge_into, expanded_live_range_start, sorted_by_startpc[0]->var.start_pc); - for(std::size_t idx=0; idxvar.start_pc+v->var.length>last_pc)