@@ -975,10 +975,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
975
975
std::vector<unsigned > jsr_ret_targets;
976
976
std::vector<instructionst::const_iterator> ret_instructions;
977
977
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++)
982
979
{
983
980
converted_instructiont ins=converted_instructiont (i_it, code_skipt ());
984
981
std::pair<address_mapt::iterator, bool > a_entry=
@@ -1018,18 +1015,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1018
1015
i_it->statement ==" invokespecial" ||
1019
1016
i_it->statement ==" invokeinterface" )
1020
1017
{
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);
1033
1019
}
1034
1020
1035
1021
if (i_it->statement ==" goto" ||
@@ -1052,10 +1038,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
1052
1038
if (i_it->statement ==" jsr" ||
1053
1039
i_it->statement ==" jsr_w" )
1054
1040
{
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" );
1059
1044
targets.insert (next->address );
1060
1045
jsr_ret_targets.push_back (next->address );
1061
1046
}
@@ -1083,27 +1068,12 @@ codet java_bytecode_convert_methodt::convert_instructions(
1083
1068
ret_instructions.push_back (i_it);
1084
1069
}
1085
1070
}
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);
1097
1072
1098
1073
for (const auto &address : address_map)
1099
1074
{
1100
1075
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 );
1107
1077
}
1108
1078
1109
1079
// Clean the list of temporary variables created by a call to `tmp_variable`.
@@ -1123,28 +1093,23 @@ codet java_bytecode_convert_methodt::convert_instructions(
1123
1093
1124
1094
while (!working_set.empty ())
1125
1095
{
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);
1129
1098
unsigned cur_pc=*cur;
1130
1099
working_set.erase (cur);
1131
1100
1132
- if (a_it-> second .done )
1101
+ if (a .done )
1133
1102
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 ());
1136
1104
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 ;
1141
1109
1142
1110
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" ));
1148
1113
1149
1114
irep_idt statement=i_it->statement ;
1150
1115
exprt arg0=i_it->args .size ()>=1 ?i_it->args [0 ]:nil_exprt ();
@@ -2145,8 +2110,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
2145
2110
if (clinit_call.get_statement ()!=ID_skip)
2146
2111
{
2147
2112
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);
2150
2115
c=std::move (ret_block);
2151
2116
}
2152
2117
results[0 ]=tmp;
@@ -2490,8 +2455,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
2490
2455
2491
2456
push (results);
2492
2457
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 )
2495
2460
{
2496
2461
address_mapt::iterator a_it2=address_map.find (address);
2497
2462
CHECK_RETURN (a_it2 != address_map.end ());
@@ -2711,6 +2676,45 @@ codet java_bytecode_convert_methodt::convert_instructions(
2711
2676
return code;
2712
2677
}
2713
2678
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
+
2714
2718
// / This uses a cut-down version of the logic in
2715
2719
// / java_bytecode_convert_methodt::convert to initialize symbols for the
2716
2720
// / parameters and update the parameters in the type of method_symbol with
0 commit comments