Skip to content

Commit 1146864

Browse files
smowtonsmowton
committed
Java object factory: take a message handler
1 parent 9f64afa commit 1146864

11 files changed

+87
-39
lines changed

‎jbmc/src/java_bytecode/convert_java_nondet.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,8 @@ static goto_programt get_gen_nondet_init_instructions(
5757
skip_classid,
5858
lifetimet::DYNAMIC,
5959
object_factory_parameters,
60-
update_in_placet::NO_UPDATE_IN_PLACE);
60+
update_in_placet::NO_UPDATE_IN_PLACE,
61+
message_handler);
6162

6263
goto_programt instructions;
6364
goto_convert(

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -869,7 +869,8 @@ bool java_bytecode_languaget::generate_support_functions(
869869
symbol_table,
870870
assume_inputs_non_null,
871871
object_factory_parameters,
872-
get_pointer_type_selector());
872+
get_pointer_type_selector(),
873+
get_message_handler());
873874
});
874875
}
875876

@@ -1068,22 +1069,25 @@ bool java_bytecode_languaget::convert_single_method(
10681069
symbol_table,
10691070
nondet_static,
10701071
object_factory_parameters,
1071-
get_pointer_type_selector());
1072+
get_pointer_type_selector(),
1073+
get_message_handler());
10721074
else
10731075
writable_symbol.value = get_clinit_wrapper_body(
10741076
function_id,
10751077
symbol_table,
10761078
nondet_static,
10771079
object_factory_parameters,
1078-
get_pointer_type_selector());
1080+
get_pointer_type_selector(),
1081+
get_message_handler());
10791082
break;
10801083
case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
10811084
writable_symbol.value =
10821085
stub_global_initializer_factory.get_stub_initializer_body(
10831086
function_id,
10841087
symbol_table,
10851088
object_factory_parameters,
1086-
get_pointer_type_selector());
1089+
get_pointer_type_selector(),
1090+
get_message_handler());
10871091
break;
10881092
}
10891093
// Notify lazy methods of static calls made from the newly generated

‎jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -258,7 +258,8 @@ static void java_static_lifetime_init(
258258
lifetimet::STATIC_GLOBAL,
259259
parameters,
260260
pointer_type_selector,
261-
update_in_placet::NO_UPDATE_IN_PLACE);
261+
update_in_placet::NO_UPDATE_IN_PLACE,
262+
message_handler);
262263
}
263264
else if(sym.value.is_not_nil())
264265
{
@@ -296,7 +297,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
296297
symbol_table_baset &symbol_table,
297298
bool assume_init_pointers_not_null,
298299
java_object_factory_parameterst object_factory_parameters,
299-
const select_pointer_typet &pointer_type_selector)
300+
const select_pointer_typet &pointer_type_selector,
301+
message_handlert &message_handler)
300302
{
301303
const java_method_typet::parameterst &parameters =
302304
to_java_method_type(function.type).parameters();
@@ -354,7 +356,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
354356
factory_parameters,
355357
lifetimet::AUTOMATIC_LOCAL,
356358
function.location,
357-
pointer_type_selector);
359+
pointer_type_selector,
360+
message_handler);
358361
}
359362
else
360363
{
@@ -400,7 +403,8 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
400403
factory_parameters,
401404
lifetimet::DYNAMIC,
402405
function.location,
403-
pointer_type_selector);
406+
pointer_type_selector,
407+
message_handler);
404408
init_code_for_type.add(
405409
code_assignt(
406410
result_symbol.symbol_expr(),

‎jbmc/src/java_bytecode/java_entry_point.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,7 @@ bool generate_java_start_function(
169169
/// \param pointer_type_selector: Means of selecting the type of value
170170
/// constructed for reference types which are initialised by the code
171171
/// returned.
172+
/// \param message_handler: log
172173
/// \returns A pairing of the code to initialise the arguments and a std::vector
173174
/// of the expressions for these arguments. The vector contains one element
174175
/// per parameter of \p function. The vector of expressions can be used as
@@ -182,6 +183,7 @@ std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
182183
symbol_table_baset &symbol_table,
183184
bool assume_init_pointers_not_null,
184185
java_object_factory_parameterst object_factory_parameters,
185-
const select_pointer_typet &pointer_type_selector);
186+
const select_pointer_typet &pointer_type_selector,
187+
message_handlert &message_handler);
186188

187189
#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H

‎jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 24 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,9 @@ class java_object_factoryt
5959

6060
allocate_objectst allocate_objects;
6161

62+
/// Log for reporting warnings and errors in object creation
63+
messaget log;
64+
6265
code_assignt get_null_assignment(
6366
const exprt &expr,
6467
const pointer_typet &ptr_type);
@@ -84,7 +87,8 @@ class java_object_factoryt
8487
const source_locationt &loc,
8588
const java_object_factory_parameterst _object_factory_parameters,
8689
symbol_table_baset &_symbol_table,
87-
const select_pointer_typet &pointer_type_selector)
90+
const select_pointer_typet &pointer_type_selector,
91+
message_handlert &log)
8892
: loc(loc),
8993
object_factory_parameters(_object_factory_parameters),
9094
symbol_table(_symbol_table),
@@ -94,7 +98,8 @@ class java_object_factoryt
9498
ID_java,
9599
loc,
96100
object_factory_parameters.function_id,
97-
symbol_table)
101+
symbol_table),
102+
log(log)
98103
{}
99104

100105
void gen_nondet_array_init(
@@ -1517,7 +1522,8 @@ exprt object_factory(
15171522
java_object_factory_parameterst parameters,
15181523
lifetimet lifetime,
15191524
const source_locationt &loc,
1520-
const select_pointer_typet &pointer_type_selector)
1525+
const select_pointer_typet &pointer_type_selector,
1526+
message_handlert &log)
15211527
{
15221528
irep_idt identifier=id2string(goto_functionst::entry_point())+
15231529
"::"+id2string(base_name);
@@ -1541,7 +1547,8 @@ exprt object_factory(
15411547
loc,
15421548
parameters,
15431549
symbol_table,
1544-
pointer_type_selector);
1550+
pointer_type_selector,
1551+
log);
15451552
code_blockt assignments;
15461553
state.gen_nondet_init(
15471554
assignments,
@@ -1594,6 +1601,7 @@ exprt object_factory(
15941601
/// MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_
15951602
/// and MUST_ cases.
15961603
/// MUST_UPDATE_IN_PLACE: reinitialize an existing object
1604+
/// \param log: used to report object construction warnings and failures
15971605
/// \return `init_code` gets an instruction sequence to initialize or
15981606
/// reinitialize `expr` and child objects it refers to. `symbol_table` is
15991607
/// modified with any new symbols created. This includes any necessary
@@ -1607,13 +1615,15 @@ void gen_nondet_init(
16071615
lifetimet lifetime,
16081616
const java_object_factory_parameterst &object_factory_parameters,
16091617
const select_pointer_typet &pointer_type_selector,
1610-
update_in_placet update_in_place)
1618+
update_in_placet update_in_place,
1619+
message_handlert &log)
16111620
{
16121621
java_object_factoryt state(
16131622
loc,
16141623
object_factory_parameters,
16151624
symbol_table,
1616-
pointer_type_selector);
1625+
pointer_type_selector,
1626+
log);
16171627
code_blockt assignments;
16181628
state.gen_nondet_init(
16191629
assignments,
@@ -1641,7 +1651,8 @@ exprt object_factory(
16411651
symbol_tablet &symbol_table,
16421652
const java_object_factory_parameterst &object_factory_parameters,
16431653
lifetimet lifetime,
1644-
const source_locationt &location)
1654+
const source_locationt &location,
1655+
message_handlert &log)
16451656
{
16461657
select_pointer_typet pointer_type_selector;
16471658
return object_factory(
@@ -1652,7 +1663,8 @@ exprt object_factory(
16521663
object_factory_parameters,
16531664
lifetime,
16541665
location,
1655-
pointer_type_selector);
1666+
pointer_type_selector,
1667+
log);
16561668
}
16571669

16581670
/// Call gen_nondet_init() above with a default (identity) pointer_type_selector
@@ -1664,7 +1676,8 @@ void gen_nondet_init(
16641676
bool skip_classid,
16651677
lifetimet lifetime,
16661678
const java_object_factory_parameterst &object_factory_parameters,
1667-
update_in_placet update_in_place)
1679+
update_in_placet update_in_place,
1680+
message_handlert &log)
16681681
{
16691682
select_pointer_typet pointer_type_selector;
16701683
gen_nondet_init(
@@ -1676,7 +1689,8 @@ void gen_nondet_init(
16761689
lifetime,
16771690
object_factory_parameters,
16781691
pointer_type_selector,
1679-
update_in_place);
1692+
update_in_place,
1693+
log);
16801694
}
16811695

16821696
/// Adds a call for the given method to the end of `assignments` if the method

‎jbmc/src/java_bytecode/java_object_factory.h

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,8 @@ exprt object_factory(
8787
java_object_factory_parameterst parameters,
8888
lifetimet lifetime,
8989
const source_locationt &location,
90-
const select_pointer_typet &pointer_type_selector);
90+
const select_pointer_typet &pointer_type_selector,
91+
message_handlert &log);
9192

9293
exprt object_factory(
9394
const typet &type,
@@ -96,7 +97,8 @@ exprt object_factory(
9697
symbol_tablet &symbol_table,
9798
const java_object_factory_parameterst &object_factory_parameters,
9899
lifetimet lifetime,
99-
const source_locationt &location);
100+
const source_locationt &location,
101+
message_handlert &log);
100102

101103
enum class update_in_placet
102104
{
@@ -114,7 +116,8 @@ void gen_nondet_init(
114116
lifetimet lifetime,
115117
const java_object_factory_parameterst &object_factory_parameters,
116118
const select_pointer_typet &pointer_type_selector,
117-
update_in_placet update_in_place);
119+
update_in_placet update_in_place,
120+
message_handlert &log);
118121

119122
void gen_nondet_init(
120123
const exprt &expr,
@@ -124,6 +127,7 @@ void gen_nondet_init(
124127
bool skip_classid,
125128
lifetimet lifetime,
126129
const java_object_factory_parameterst &object_factory_parameters,
127-
update_in_placet update_in_place);
130+
update_in_placet update_in_place,
131+
message_handlert &log);
128132

129133
#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H

‎jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -195,13 +195,15 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
195195
/// if nondet-static is true)
196196
/// \param pointer_type_selector: used to choose concrete types for abstract-
197197
/// typed globals and fields (only needed if nondet-static is true)
198+
/// \param message_handler: log
198199
static void clinit_wrapper_do_recursive_calls(
199200
symbol_table_baset &symbol_table,
200201
const irep_idt &class_name,
201202
code_blockt &init_body,
202203
const bool nondet_static,
203204
const java_object_factory_parameterst &object_factory_parameters,
204-
const select_pointer_typet &pointer_type_selector)
205+
const select_pointer_typet &pointer_type_selector,
206+
message_handlert &message_handler)
205207
{
206208
const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
207209
for(const auto &base : to_class_type(class_symbol.type).bases())
@@ -265,7 +267,8 @@ static void clinit_wrapper_do_recursive_calls(
265267
lifetimet::DYNAMIC,
266268
parameters,
267269
pointer_type_selector,
268-
update_in_placet::NO_UPDATE_IN_PLACE);
270+
update_in_placet::NO_UPDATE_IN_PLACE,
271+
message_handler);
269272
}
270273
}
271274
}
@@ -453,7 +456,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
453456
symbol_table_baset &symbol_table,
454457
const bool nondet_static,
455458
const java_object_factory_parameterst &object_factory_parameters,
456-
const select_pointer_typet &pointer_type_selector)
459+
const select_pointer_typet &pointer_type_selector,
460+
message_handlert &message_handler)
457461
{
458462
const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
459463
irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@@ -605,7 +609,8 @@ code_blockt get_thread_safe_clinit_wrapper_body(
605609
init_body,
606610
nondet_static,
607611
object_factory_parameters,
608-
pointer_type_selector);
612+
pointer_type_selector,
613+
message_handler);
609614
function_body.append(init_body);
610615
}
611616

@@ -643,7 +648,8 @@ code_ifthenelset get_clinit_wrapper_body(
643648
symbol_table_baset &symbol_table,
644649
const bool nondet_static,
645650
const java_object_factory_parameterst &object_factory_parameters,
646-
const select_pointer_typet &pointer_type_selector)
651+
const select_pointer_typet &pointer_type_selector,
652+
message_handlert &message_handler)
647653
{
648654
// Assume that class C extends class C' and implements interfaces
649655
// I1, ..., In. We now create the following function (possibly recursively
@@ -687,7 +693,8 @@ code_ifthenelset get_clinit_wrapper_body(
687693
init_body,
688694
nondet_static,
689695
object_factory_parameters,
690-
pointer_type_selector);
696+
pointer_type_selector,
697+
message_handler);
691698

692699
// the entire body of the function is an if-then-else
693700
return code_ifthenelset(std::move(check_already_run), std::move(init_body));
@@ -833,7 +840,8 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
833840
const irep_idt &function_id,
834841
symbol_table_baset &symbol_table,
835842
const java_object_factory_parameterst &object_factory_parameters,
836-
const select_pointer_typet &pointer_type_selector)
843+
const select_pointer_typet &pointer_type_selector,
844+
message_handlert &message_handler)
837845
{
838846
const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
839847
irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
@@ -875,7 +883,8 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
875883
lifetimet::DYNAMIC,
876884
parameters,
877885
pointer_type_selector,
878-
update_in_placet::NO_UPDATE_IN_PLACE);
886+
update_in_placet::NO_UPDATE_IN_PLACE,
887+
message_handler);
879888
}
880889

881890
return static_init_body;

‎jbmc/src/java_bytecode/java_static_initializers.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Chris Smowton, [email protected]
1515

1616
#include <unordered_set>
1717

18+
#include <util/message.h>
1819
#include <util/symbol_table.h>
1920
#include <util/std_code.h>
2021

@@ -32,14 +33,16 @@ code_blockt get_thread_safe_clinit_wrapper_body(
3233
symbol_table_baset &symbol_table,
3334
const bool nondet_static,
3435
const java_object_factory_parameterst &object_factory_parameters,
35-
const select_pointer_typet &pointer_type_selector);
36+
const select_pointer_typet &pointer_type_selector,
37+
message_handlert &message_handler);
3638

3739
code_ifthenelset get_clinit_wrapper_body(
3840
const irep_idt &function_id,
3941
symbol_table_baset &symbol_table,
4042
const bool nondet_static,
4143
const java_object_factory_parameterst &object_factory_parameters,
42-
const select_pointer_typet &pointer_type_selector);
44+
const select_pointer_typet &pointer_type_selector,
45+
message_handlert &message_handler);
4346

4447
class stub_global_initializer_factoryt
4548
{
@@ -57,7 +60,8 @@ class stub_global_initializer_factoryt
5760
const irep_idt &function_id,
5861
symbol_table_baset &symbol_table,
5962
const java_object_factory_parameterst &object_factory_parameters,
60-
const select_pointer_typet &pointer_type_selector);
63+
const select_pointer_typet &pointer_type_selector,
64+
message_handlert &message_handler);
6165
};
6266

6367
void create_stub_global_initializers(

0 commit comments

Comments
 (0)