Skip to content

Commit 119e88b

Browse files
romainbrenguierromainbrenguier
committed
Pass location around for nondet initialization
1 parent 50660db commit 119e88b

File tree

2 files changed

+71
-51
lines changed

2 files changed

+71
-51
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -812,8 +812,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
812812
code_declt declare_cloned(local_symexpr);
813813
clone_body.move_to_operands(declare_cloned);
814814

815+
source_locationt location;
816+
location.set_function(local_name);
815817
side_effect_exprt java_new_array(
816-
ID_java_new_array, java_reference_type(symbol_type), source_locationt());
818+
ID_java_new_array, java_reference_type(symbol_type), location);
817819
dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
818820
dereference_exprt new_array(local_symexpr, symbol_type);
819821
member_exprt old_length(
@@ -859,7 +861,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
859861
copy_loop.cond()=
860862
binary_relation_exprt(index_symexpr, ID_lt, old_length);
861863

862-
side_effect_exprt inc(ID_assign, typet(), source_locationt());
864+
side_effect_exprt inc(ID_assign, typet(), location);
863865
inc.operands().resize(2);
864866
inc.op0()=index_symexpr;
865867
inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));

‎jbmc/src/java_bytecode/java_object_factory.cpp‎

Lines changed: 67 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -69,13 +69,15 @@ class java_object_factoryt
6969
const typet &target_type,
7070
allocation_typet alloc_type,
7171
size_t depth,
72-
update_in_placet update_in_place);
72+
update_in_placet update_in_place,
73+
const source_locationt &location);
7374

7475
void allocate_nondet_length_array(
7576
code_blockt &assignments,
7677
const exprt &lhs,
7778
const exprt &max_length_expr,
78-
const typet &element_type);
79+
const typet &element_type,
80+
const source_locationt &location);
7981

8082
public:
8183
java_object_factoryt(
@@ -102,7 +104,8 @@ class java_object_factoryt
102104
code_blockt &assignments,
103105
const exprt &expr,
104106
size_t depth,
105-
update_in_placet);
107+
update_in_placet,
108+
const source_locationt &location);
106109

107110
void gen_nondet_init(
108111
code_blockt &assignments,
@@ -114,7 +117,8 @@ class java_object_factoryt
114117
bool override_,
115118
const typet &override_type,
116119
size_t depth,
117-
update_in_placet);
120+
update_in_placet,
121+
const source_locationt &location);
118122

119123
private:
120124
void gen_nondet_pointer_init(
@@ -123,7 +127,8 @@ class java_object_factoryt
123127
allocation_typet alloc_type,
124128
const pointer_typet &pointer_type,
125129
size_t depth,
126-
const update_in_placet &update_in_place);
130+
const update_in_placet &update_in_place,
131+
const source_locationt &location);
127132

128133
void gen_nondet_struct_init(
129134
code_blockt &assignments,
@@ -134,13 +139,15 @@ class java_object_factoryt
134139
allocation_typet alloc_type,
135140
const struct_typet &struct_type,
136141
size_t depth,
137-
const update_in_placet &update_in_place);
142+
const update_in_placet &update_in_place,
143+
const source_locationt &location);
138144

139145
symbol_exprt gen_nondet_subtype_pointer_init(
140146
code_blockt &assignments,
141147
allocation_typet alloc_type,
142148
const pointer_typet &substitute_pointer_type,
143-
size_t depth);
149+
size_t depth,
150+
const source_locationt &location);
144151
};
145152

146153
/// Generates code for allocating a dynamic object. This is used in
@@ -372,7 +379,8 @@ void java_object_factoryt::gen_pointer_target_init(
372379
const typet &target_type,
373380
allocation_typet alloc_type,
374381
size_t depth,
375-
update_in_placet update_in_place)
382+
update_in_placet update_in_place,
383+
const source_locationt &location)
376384
{
377385
PRECONDITION(expr.type().id()==ID_pointer);
378386
PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
@@ -383,10 +391,7 @@ void java_object_factoryt::gen_pointer_target_init(
383391
"java::array["))
384392
{
385393
gen_nondet_array_init(
386-
assignments,
387-
expr,
388-
depth+1,
389-
update_in_place);
394+
assignments, expr, depth + 1, update_in_place, location);
390395
}
391396
else
392397
{
@@ -426,14 +431,15 @@ void java_object_factoryt::gen_pointer_target_init(
426431
gen_nondet_init(
427432
assignments,
428433
init_expr,
429-
false, // is_sub
430-
"", // class_identifier
431-
false, // skip_classid
434+
false, // is_sub
435+
"", // class_identifier
436+
false, // skip_classid
432437
alloc_type,
433-
false, // override
434-
typet(), // override type immaterial
435-
depth+1,
436-
update_in_place);
438+
false,
439+
typet(),
440+
depth + 1,
441+
update_in_place,
442+
location);
437443
}
438444
}
439445

@@ -688,7 +694,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
688694
allocation_typet alloc_type,
689695
const pointer_typet &pointer_type,
690696
size_t depth,
691-
const update_in_placet &update_in_place)
697+
const update_in_placet &update_in_place,
698+
const source_locationt &location)
692699
{
693700
PRECONDITION(expr.type().id()==ID_pointer);
694701
const pointer_typet &replacement_pointer_type =
@@ -710,7 +717,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
710717
replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
711718

712719
const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
713-
assignments, alloc_type, replacement_pointer_type, depth);
720+
assignments, alloc_type, replacement_pointer_type, depth, location);
714721

715722
// Having created a pointer to object of type replacement_pointer_type
716723
// we now assign it back to the original pointer with a cast
@@ -772,7 +779,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
772779
subtype,
773780
alloc_type,
774781
depth,
775-
update_in_placet::MUST_UPDATE_IN_PLACE);
782+
update_in_placet::MUST_UPDATE_IN_PLACE,
783+
location);
776784
}
777785

778786
// if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
@@ -794,7 +802,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
794802
subtype,
795803
alloc_type,
796804
depth,
797-
update_in_placet::NO_UPDATE_IN_PLACE);
805+
update_in_placet::NO_UPDATE_IN_PLACE,
806+
location);
798807

799808
auto set_null_inst=get_null_assignment(expr, pointer_type);
800809

@@ -829,8 +838,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
829838
// tmp$<temporary_counter>>
830839
// }
831840
code_ifthenelset null_check;
832-
null_check.cond() =
833-
side_effect_expr_nondett(bool_typet(), expr.source_location());
841+
null_check.cond() = side_effect_expr_nondett(bool_typet(), location);
834842
null_check.then_case()=set_null_inst;
835843
null_check.else_case()=non_null_inst;
836844

@@ -886,7 +894,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
886894
code_blockt &assignments,
887895
allocation_typet alloc_type,
888896
const pointer_typet &replacement_pointer,
889-
size_t depth)
897+
size_t depth,
898+
const source_locationt &location)
890899
{
891900
symbolt new_symbol = get_fresh_aux_symbol(
892901
replacement_pointer,
@@ -900,14 +909,15 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
900909
gen_nondet_init(
901910
assignments,
902911
new_symbol.symbol_expr(),
903-
false, // is_sub
904-
"", // class_identifier
905-
false, // skip_classid
912+
false, // is_sub
913+
"", // class_identifier
914+
false, // skip_classid
906915
alloc_type,
907916
false, // override
908917
typet(), // override_type
909918
depth,
910-
update_in_placet::NO_UPDATE_IN_PLACE);
919+
update_in_placet::NO_UPDATE_IN_PLACE,
920+
location);
911921

912922
return new_symbol.symbol_expr();
913923
}
@@ -950,7 +960,8 @@ void java_object_factoryt::gen_nondet_struct_init(
950960
allocation_typet alloc_type,
951961
const struct_typet &struct_type,
952962
size_t depth,
953-
const update_in_placet &update_in_place)
963+
const update_in_placet &update_in_place,
964+
const source_locationt &location)
954965
{
955966
PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
956967
PRECONDITION(struct_type.id()==ID_struct);
@@ -1052,12 +1063,13 @@ void java_object_factoryt::gen_nondet_struct_init(
10521063
me,
10531064
_is_sub,
10541065
class_identifier,
1055-
false, // skip_classid
1066+
false, // skip_classid
10561067
alloc_type,
10571068
false, // override
10581069
typet(), // override_type
10591070
depth,
1060-
substruct_in_place);
1071+
substruct_in_place,
1072+
location);
10611073
}
10621074
}
10631075

@@ -1125,7 +1137,8 @@ void java_object_factoryt::gen_nondet_init(
11251137
bool override_,
11261138
const typet &override_type,
11271139
size_t depth,
1128-
update_in_placet update_in_place)
1140+
update_in_placet update_in_place,
1141+
const source_locationt &location)
11291142
{
11301143
const typet &type=
11311144
override_ ? ns.follow(override_type) : ns.follow(expr.type());
@@ -1150,7 +1163,8 @@ void java_object_factoryt::gen_nondet_init(
11501163
alloc_type,
11511164
pointer_type,
11521165
depth,
1153-
update_in_place);
1166+
update_in_place,
1167+
location);
11541168
}
11551169
else if(type.id()==ID_struct)
11561170
{
@@ -1179,7 +1193,8 @@ void java_object_factoryt::gen_nondet_init(
11791193
alloc_type,
11801194
struct_type,
11811195
depth,
1182-
update_in_place);
1196+
update_in_place,
1197+
location);
11831198
}
11841199
else
11851200
{
@@ -1211,7 +1226,8 @@ void java_object_factoryt::allocate_nondet_length_array(
12111226
code_blockt &assignments,
12121227
const exprt &lhs,
12131228
const exprt &max_length_expr,
1214-
const typet &element_type)
1229+
const typet &element_type,
1230+
const source_locationt &location)
12151231
{
12161232
symbolt &length_sym = get_fresh_aux_symbol(
12171233
java_int_type(),
@@ -1234,7 +1250,8 @@ void java_object_factoryt::allocate_nondet_length_array(
12341250
false, // override
12351251
typet(), // override type is immaterial
12361252
0, // depth is immaterial, always non-null
1237-
update_in_placet::NO_UPDATE_IN_PLACE);
1253+
update_in_placet::NO_UPDATE_IN_PLACE,
1254+
location);
12381255

12391256
// Insert assumptions to bound its length:
12401257
binary_relation_exprt
@@ -1265,7 +1282,8 @@ void java_object_factoryt::gen_nondet_array_init(
12651282
code_blockt &assignments,
12661283
const exprt &expr,
12671284
size_t depth,
1268-
update_in_placet update_in_place)
1285+
update_in_placet update_in_place,
1286+
const source_locationt &location)
12691287
{
12701288
PRECONDITION(expr.type().id()==ID_pointer);
12711289
PRECONDITION(expr.type().subtype().id()==ID_symbol);
@@ -1284,10 +1302,7 @@ void java_object_factoryt::gen_nondet_array_init(
12841302
if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
12851303
{
12861304
allocate_nondet_length_array(
1287-
assignments,
1288-
expr,
1289-
max_length_expr,
1290-
element_type);
1305+
assignments, expr, max_length_expr, element_type, location);
12911306
}
12921307

12931308
// Otherwise we're updating the array in place, and use the
@@ -1377,15 +1392,16 @@ void java_object_factoryt::gen_nondet_array_init(
13771392
gen_nondet_init(
13781393
assignments,
13791394
arraycellref,
1380-
false, // is_sub
1395+
false, // is_sub
13811396
irep_idt(), // class_identifier
1382-
false, // skip_classid
1397+
false, // skip_classid
13831398
// These are variable in number, so use dynamic allocator:
13841399
allocation_typet::DYNAMIC,
1385-
true, // override
1400+
true, // override
13861401
element_type,
13871402
depth,
1388-
child_update_in_place);
1403+
child_update_in_place,
1404+
location);
13891405

13901406
exprt java_one=from_integer(1, java_int_type());
13911407
code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
@@ -1476,7 +1492,8 @@ exprt object_factory(
14761492
false, // override
14771493
typet(), // override_type is immaterial
14781494
1, // initial depth
1479-
update_in_placet::NO_UPDATE_IN_PLACE);
1495+
update_in_placet::NO_UPDATE_IN_PLACE,
1496+
loc);
14801497

14811498
declare_created_symbols(symbols_created, loc, init_code);
14821499

@@ -1549,7 +1566,8 @@ void gen_nondet_init(
15491566
false, // override
15501567
typet(), // override_type is immaterial
15511568
1, // initial depth
1552-
update_in_place);
1569+
update_in_place,
1570+
loc);
15531571

15541572
declare_created_symbols(symbols_created, loc, init_code);
15551573

0 commit comments

Comments
 (0)