Skip to content

Commit a7bbf53

Browse files
romainbrenguierromainbrenguier
committed
Extract do_exception_handling function
1 parent 0aa1c8e commit a7bbf53

File tree

2 files changed

+118
-103
lines changed

2 files changed

+118
-103
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp‎

Lines changed: 112 additions & 103 deletions
Original file line numberDiff line numberDiff line change
@@ -1961,109 +1961,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
19611961
c.operands()=op;
19621962
}
19631963

1964-
// next we do the exception handling
1965-
std::vector<irep_idt> exception_ids;
1966-
std::vector<irep_idt> handler_labels;
1967-
1968-
// for each try-catch add a CATCH-PUSH instruction
1969-
// each CATCH-PUSH records a list of all the handler labels
1970-
// together with a list of all the exception ids
1971-
1972-
// be aware of different try-catch blocks with the same starting pc
1973-
std::size_t pos=0;
1974-
std::size_t end_pc=0;
1975-
while(pos<method.exception_table.size())
1976-
{
1977-
// check if this is the beginning of a try block
1978-
for(; pos<method.exception_table.size(); ++pos)
1979-
{
1980-
// unexplored try-catch?
1981-
if(cur_pc==method.exception_table[pos].start_pc && end_pc==0)
1982-
{
1983-
end_pc=method.exception_table[pos].end_pc;
1984-
}
1985-
1986-
// currently explored try-catch?
1987-
if(cur_pc==method.exception_table[pos].start_pc &&
1988-
method.exception_table[pos].end_pc==end_pc)
1989-
{
1990-
exception_ids.push_back(
1991-
method.exception_table[pos].catch_type.get_identifier());
1992-
// record the exception handler in the CATCH-PUSH
1993-
// instruction by generating a label corresponding to
1994-
// the handler's pc
1995-
handler_labels.push_back(
1996-
label(std::to_string(method.exception_table[pos].handler_pc)));
1997-
}
1998-
else
1999-
break;
2000-
}
2001-
2002-
// add the actual PUSH-CATCH instruction
2003-
if(!exception_ids.empty())
2004-
{
2005-
code_push_catcht catch_push;
2006-
INVARIANT(
2007-
exception_ids.size()==handler_labels.size(),
2008-
"Exception tags and handler labels should be 1-to-1");
2009-
code_push_catcht::exception_listt &exception_list=
2010-
catch_push.exception_list();
2011-
for(size_t i=0; i<exception_ids.size(); ++i)
2012-
{
2013-
exception_list.push_back(
2014-
code_push_catcht::exception_list_entryt(
2015-
exception_ids[i],
2016-
handler_labels[i]));
2017-
}
2018-
2019-
code_blockt try_block;
2020-
try_block.move_to_operands(catch_push);
2021-
try_block.move_to_operands(c);
2022-
c=try_block;
2023-
}
2024-
else
2025-
{
2026-
// advance
2027-
++pos;
2028-
}
2029-
2030-
// reset
2031-
end_pc=0;
2032-
exception_ids.clear();
2033-
handler_labels.clear();
2034-
}
2035-
2036-
// next add the CATCH-POP instructions
2037-
size_t start_pc=0;
2038-
// as the first try block may have start_pc 0, we
2039-
// must track it separately
2040-
bool first_handler=false;
2041-
// check if this is the end of a try block
2042-
for(const auto &exception_row : method.exception_table)
2043-
{
2044-
// add the CATCH-POP before the end of the try block
2045-
if(cur_pc<exception_row.end_pc &&
2046-
!working_set.empty() &&
2047-
*working_set.begin()==exception_row.end_pc)
2048-
{
2049-
// have we already added a CATCH-POP for the current try-catch?
2050-
// (each row corresponds to a handler)
2051-
if(exception_row.start_pc!=start_pc || !first_handler)
2052-
{
2053-
if(!first_handler)
2054-
first_handler=true;
2055-
// remember the beginning of the try-catch so that we don't add
2056-
// another CATCH-POP for the same try-catch
2057-
start_pc=exception_row.start_pc;
2058-
// add CATCH_POP instruction
2059-
code_pop_catcht catch_pop;
2060-
code_blockt end_try_block;
2061-
end_try_block.move_to_operands(c);
2062-
end_try_block.move_to_operands(catch_pop);
2063-
c=end_try_block;
2064-
}
2065-
}
2066-
}
1964+
c = do_exception_handling(method, working_set, cur_pc, c);
20671965

20681966
// Finally if this is the beginning of a catch block (already determined
20691967
// before the big bytecode switch), insert the exception 'landing pad'
@@ -2300,6 +2198,117 @@ codet java_bytecode_convert_methodt::convert_instructions(
23002198
return code;
23012199
}
23022200

2201+
codet &java_bytecode_convert_methodt::do_exception_handling(
2202+
const java_bytecode_convert_methodt::methodt &method,
2203+
const std::set<unsigned int> &working_set,
2204+
unsigned int cur_pc,
2205+
codet &c)
2206+
{
2207+
std::vector<irep_idt> exception_ids;
2208+
std::vector<irep_idt> handler_labels;
2209+
2210+
// for each try-catch add a CATCH-PUSH instruction
2211+
// each CATCH-PUSH records a list of all the handler labels
2212+
// together with a list of all the exception ids
2213+
2214+
// be aware of different try-catch blocks with the same starting pc
2215+
std::size_t pos = 0;
2216+
std::size_t end_pc = 0;
2217+
while(pos < method.exception_table.size())
2218+
{
2219+
// check if this is the beginning of a try block
2220+
for(; pos < method.exception_table.size(); ++pos)
2221+
{
2222+
// unexplored try-catch?
2223+
if(cur_pc == method.exception_table[pos].start_pc && end_pc == 0)
2224+
{
2225+
end_pc = method.exception_table[pos].end_pc;
2226+
}
2227+
2228+
// currently explored try-catch?
2229+
if(
2230+
cur_pc == method.exception_table[pos].start_pc &&
2231+
method.exception_table[pos].end_pc == end_pc)
2232+
{
2233+
exception_ids.push_back(
2234+
method.exception_table[pos].catch_type.get_identifier());
2235+
// record the exception handler in the CATCH-PUSH
2236+
// instruction by generating a label corresponding to
2237+
// the handler's pc
2238+
handler_labels.push_back(
2239+
label(std::to_string(method.exception_table[pos].handler_pc)));
2240+
}
2241+
else
2242+
break;
2243+
}
2244+
2245+
// add the actual PUSH-CATCH instruction
2246+
if(!exception_ids.empty())
2247+
{
2248+
code_push_catcht catch_push;
2249+
INVARIANT(
2250+
exception_ids.size() == handler_labels.size(),
2251+
"Exception tags and handler labels should be 1-to-1");
2252+
code_push_catcht::exception_listt &exception_list =
2253+
catch_push.exception_list();
2254+
for(size_t i = 0; i < exception_ids.size(); ++i)
2255+
{
2256+
exception_list.push_back(
2257+
code_push_catcht::exception_list_entryt(
2258+
exception_ids[i], handler_labels[i]));
2259+
}
2260+
2261+
code_blockt try_block;
2262+
try_block.move_to_operands(catch_push);
2263+
try_block.move_to_operands(c);
2264+
c = try_block;
2265+
}
2266+
else
2267+
{
2268+
// advance
2269+
++pos;
2270+
}
2271+
2272+
// reset
2273+
end_pc = 0;
2274+
exception_ids.clear();
2275+
handler_labels.clear();
2276+
}
2277+
2278+
// next add the CATCH-POP instructions
2279+
size_t start_pc = 0;
2280+
// as the first try block may have start_pc 0, we
2281+
// must track it separately
2282+
bool first_handler = false;
2283+
// check if this is the end of a try block
2284+
for(const auto &exception_row : method.exception_table)
2285+
{
2286+
// add the CATCH-POP before the end of the try block
2287+
if(
2288+
cur_pc < exception_row.end_pc && !working_set.empty() &&
2289+
*working_set.begin() == exception_row.end_pc)
2290+
{
2291+
// have we already added a CATCH-POP for the current try-catch?
2292+
// (each row corresponds to a handler)
2293+
if(exception_row.start_pc != start_pc || !first_handler)
2294+
{
2295+
if(!first_handler)
2296+
first_handler = true;
2297+
// remember the beginning of the try-catch so that we don't add
2298+
// another CATCH-POP for the same try-catch
2299+
start_pc = exception_row.start_pc;
2300+
// add CATCH_POP instruction
2301+
code_pop_catcht catch_pop;
2302+
code_blockt end_try_block;
2303+
end_try_block.move_to_operands(c);
2304+
end_try_block.move_to_operands(catch_pop);
2305+
c = end_try_block;
2306+
}
2307+
}
2308+
}
2309+
return c;
2310+
}
2311+
23032312
codet java_bytecode_convert_methodt::convert_monitorenter(
23042313
const source_locationt &location,
23052314
const exprt::operandst &op) const

‎jbmc/src/java_bytecode/java_bytecode_convert_method_class.h‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -420,5 +420,11 @@ class java_bytecode_convert_methodt:public messaget
420420
codet convert_monitorenter(
421421
const source_locationt &location,
422422
const exprt::operandst &op) const;
423+
424+
codet &do_exception_handling(
425+
const methodt &method,
426+
const std::set<unsigned int> &working_set,
427+
unsigned int cur_pc,
428+
codet &c);
423429
};
424430
#endif

0 commit comments

Comments
 (0)