@@ -975,10 +975,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
975975 std::vector<unsigned > jsr_ret_targets;
976976 std::vector<instructionst::const_iterator> ret_instructions;
977977
978- for (instructionst::const_iterator
979- i_it=instructions.begin ();
980- i_it!=instructions.end ();
981- i_it++)
978+ for (auto i_it = instructions.begin (); i_it != instructions.end (); i_it++)
982979 {
983980 converted_instructiont ins=converted_instructiont (i_it, code_skipt ());
984981 std::pair<address_mapt::iterator, bool > a_entry=
@@ -1018,18 +1015,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
10181015 i_it->statement ==" invokespecial" ||
10191016 i_it->statement ==" invokeinterface" )
10201017 {
1021- // find the corresponding try-catch blocks and add the handlers
1022- // to the targets
1023- for (const auto &exception_row : method.exception_table )
1024- {
1025- if (i_it->address >=exception_row.start_pc &&
1026- i_it->address <exception_row.end_pc )
1027- {
1028- a_entry.first ->second .successors .push_back (
1029- exception_row.handler_pc );
1030- targets.insert (exception_row.handler_pc );
1031- }
1032- }
1018+ add_try_catch_handler_to_target (method, targets, i_it, a_entry);
10331019 }
10341020
10351021 if (i_it->statement ==" goto" ||
@@ -1052,10 +1038,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
10521038 if (i_it->statement ==" jsr" ||
10531039 i_it->statement ==" jsr_w" )
10541040 {
1055- instructionst::const_iterator next=i_it+1 ;
1056- assert (
1057- next!=instructions.end () &&
1058- " jsr without valid return address?" );
1041+ auto next = i_it + 1 ;
1042+ DATA_INVARIANT (
1043+ next != instructions.end (), " jsr should have valid return address" );
10591044 targets.insert (next->address );
10601045 jsr_ret_targets.push_back (next->address );
10611046 }
@@ -1083,27 +1068,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
10831068 ret_instructions.push_back (i_it);
10841069 }
10851070 }
1086-
1087- // Draw edges from every `ret` to every `jsr` successor. Could do better with
1088- // flow analysis to distinguish multiple subroutines within the same function.
1089- for (const auto retinst : ret_instructions)
1090- {
1091- auto &a_entry=address_map.at (retinst->address );
1092- a_entry.successors .insert (
1093- a_entry.successors .end (),
1094- jsr_ret_targets.begin (),
1095- jsr_ret_targets.end ());
1096- }
1071+ draw_edges_from_ret_to_jsr (address_map, jsr_ret_targets, ret_instructions);
10971072
10981073 for (const auto &address : address_map)
10991074 {
11001075 for (unsigned s : address.second .successors )
1101- {
1102- address_mapt::iterator a_it=address_map.find (s);
1103- assert (a_it!=address_map.end ());
1104-
1105- a_it->second .predecessors .insert (address.first );
1106- }
1076+ address_map.at (s).predecessors .insert (address.first );
11071077 }
11081078
11091079 // Clean the list of temporary variables created by a call to `tmp_variable`.
@@ -1123,28 +1093,23 @@ codet java_bytecode_convert_methodt::convert_instructions(
11231093
11241094 while (!working_set.empty ())
11251095 {
1126- std::set<unsigned >::iterator cur=working_set.begin ();
1127- address_mapt::iterator a_it=address_map.find (*cur);
1128- CHECK_RETURN (a_it != address_map.end ());
1096+ auto cur = working_set.begin ();
1097+ auto a = address_map.at (*cur);
11291098 unsigned cur_pc=*cur;
11301099 working_set.erase (cur);
11311100
1132- if (a_it-> second .done )
1101+ if (a .done )
11331102 continue ;
1134- working_set
1135- .insert (a_it->second .successors .begin (), a_it->second .successors .end ());
1103+ working_set.insert (a.successors .begin (), a.successors .end ());
11361104
1137- instructionst::const_iterator i_it=a_it-> second .source ;
1138- stack.swap (a_it-> second .stack );
1139- a_it-> second .stack .clear ();
1140- codet &c=a_it-> second .code ;
1105+ instructionst::const_iterator i_it = a .source ;
1106+ stack.swap (a .stack );
1107+ a .stack .clear ();
1108+ codet &c = a .code ;
11411109
11421110 assert (
1143- stack.empty () ||
1144- a_it->second .predecessors .size ()<=1 ||
1145- has_prefix (
1146- stack.front ().get_string (ID_C_base_name),
1147- " $stack" ));
1111+ stack.empty () || a.predecessors .size () <= 1 ||
1112+ has_prefix (stack.front ().get_string (ID_C_base_name), " $stack" ));
11481113
11491114 irep_idt statement=i_it->statement ;
11501115 exprt arg0=i_it->args .size ()>=1 ?i_it->args [0 ]:nil_exprt ();
@@ -2145,8 +2110,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
21452110 if (clinit_call.get_statement ()!=ID_skip)
21462111 {
21472112 code_blockt ret_block;
2148- ret_block.move_to_operands (clinit_call);
2149- ret_block.move_to_operands (c);
2113+ ret_block.add (clinit_call);
2114+ ret_block.add (c);
21502115 c=std::move (ret_block);
21512116 }
21522117 results[0 ]=tmp;
@@ -2490,8 +2455,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
24902455
24912456 push (results);
24922457
2493- a_it-> second .done = true ;
2494- for (const unsigned address : a_it-> second .successors )
2458+ a .done = true ;
2459+ for (const unsigned address : a .successors )
24952460 {
24962461 address_mapt::iterator a_it2=address_map.find (address);
24972462 CHECK_RETURN (a_it2 != address_map.end ());
@@ -2711,6 +2676,45 @@ codet java_bytecode_convert_methodt::convert_instructions(
27112676 return code;
27122677}
27132678
2679+ void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr (
2680+ java_bytecode_convert_methodt::address_mapt &address_map,
2681+ std::vector<unsigned int > &jsr_ret_targets,
2682+ const std::vector<
2683+ std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2684+ &ret_instructions) const
2685+ { // Draw edges from every `ret` to every `jsr` successor. Could do better with
2686+ // flow analysis to distinguish multiple subroutines within the same function.
2687+ for (const auto retinst : ret_instructions)
2688+ {
2689+ auto &a_entry = address_map.at (retinst->address );
2690+ a_entry.successors .insert (
2691+ a_entry.successors .end (), jsr_ret_targets.begin (), jsr_ret_targets.end ());
2692+ }
2693+ }
2694+
2695+ void java_bytecode_convert_methodt::add_try_catch_handler_to_target (
2696+ const java_bytecode_convert_methodt::methodt &method,
2697+ std::set<unsigned int > &targets,
2698+ const std::vector<java_bytecode_parse_treet::instructiont>::const_iterator
2699+ &i_it,
2700+ const std::pair<
2701+ std::map<unsigned int ,
2702+ java_bytecode_convert_methodt::converted_instructiont>::iterator,
2703+ bool > &a_entry) const
2704+ { // find the corresponding try-catch blocks and add the handlers
2705+ // to the targets
2706+ for (const auto &exception_row : method.exception_table )
2707+ {
2708+ if (
2709+ i_it->address >= exception_row.start_pc &&
2710+ i_it->address < exception_row.end_pc )
2711+ {
2712+ a_entry.first ->second .successors .push_back (exception_row.handler_pc );
2713+ targets.insert (exception_row.handler_pc );
2714+ }
2715+ }
2716+ }
2717+
27142718// / This uses a cut-down version of the logic in
27152719// / java_bytecode_convert_methodt::convert to initialize symbols for the
27162720// / parameters and update the parameters in the type of method_symbol with
0 commit comments