cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
lift_clinit_calls.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Static initializer call lifting
4
5
Author: Diffblue Ltd.
6
7
\*******************************************************************/
8
10
11
#include "
lift_clinit_calls.h
"
12
13
#include <
java_bytecode/java_static_initializers.h
>
14
15
#include <
goto-programs/goto_instruction_code.h
>
16
17
#include <
util/expr_iterator.h
>
18
19
#include <algorithm>
20
21
codet
lift_clinit_calls
(
codet
input)
22
{
23
// 1. Gather any clinit calls present in `input`:
24
std::vector<symbol_exprt> clinit_wrappers_called;
25
26
for
(
auto
it = input.
depth_begin
(), itend = input.
depth_end
(); it != itend;
27
++it)
28
{
29
if
(
const
auto
code =
expr_try_dynamic_cast<codet>
(*it))
30
{
31
if
(code->get_statement() == ID_function_call)
32
{
33
if
(
34
const
auto
callee =
expr_try_dynamic_cast<symbol_exprt>
(
35
to_code_function_call
(*code).
function
()))
36
{
37
if
(
is_clinit_wrapper_function
(callee->get_identifier()))
38
{
39
clinit_wrappers_called.push_back(*callee);
40
// Replace call with skip:
41
it.mutate() =
code_skipt
();
42
}
43
}
44
}
45
}
46
}
47
48
if
(clinit_wrappers_called.empty())
49
return
input;
50
51
// 2. Unique, such that each clinit method is only called once:
52
std::sort(clinit_wrappers_called.begin(), clinit_wrappers_called.end());
53
auto
delete_after =
54
std::unique(clinit_wrappers_called.begin(), clinit_wrappers_called.end());
55
clinit_wrappers_called.erase(delete_after, clinit_wrappers_called.end());
56
57
// 3. Lift static init calls to top of function:
58
code_blockt
result;
59
for
(
const
auto
&callee : clinit_wrappers_called)
60
{
61
code_function_callt
new_call(callee);
62
// Nuke the source location, now that the call doesn't really relate to any
63
// one particular line:
64
new_call.
function
().
drop_source_location
();
65
result.
add
(new_call);
66
}
67
68
result.
add
(std::move(input));
69
70
return
std::move(result);
71
}
code_blockt
A codet representing sequential composition of program statements.
Definition
std_code.h:130
code_blockt::add
void add(const codet &code)
Definition
std_code.h:168
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition
goto_instruction_code.h:271
code_function_callt::function
exprt & function()
Definition
goto_instruction_code.h:306
code_skipt
A codet representing a skip statement.
Definition
std_code.h:322
codet
Data structure for representing an arbitrary statement in a program.
Definition
std_code_base.h:29
exprt::depth_end
depth_iteratort depth_end()
Definition
expr.cpp:170
exprt::depth_begin
depth_iteratort depth_begin()
Definition
expr.cpp:168
exprt::drop_source_location
void drop_source_location()
Definition
expr.h:246
expr_try_dynamic_cast
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition
expr_cast.h:81
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
goto_instruction_code.h
to_code_function_call
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
Definition
goto_instruction_code.h:384
is_clinit_wrapper_function
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
Definition
java_static_initializers.cpp:86
java_static_initializers.h
lift_clinit_calls
codet lift_clinit_calls(codet input)
file Static initializer call lifting
Definition
lift_clinit_calls.cpp:21
lift_clinit_calls.h
jbmc
src
java_bytecode
lift_clinit_calls.cpp
Generated by
1.17.0