Skip to content

Commit fdc5b1e

Browse files
Add source location to code added by preprocessing
When the String preprocessing adds code to populate some functions, we should associate a code location to these instructions. Otherwise this could in particular lead to problem with coverage instrumentation which would not know what instruction to instrument, and may not instrument the function at all.
1 parent 0208218 commit fdc5b1e

File tree

2 files changed

+84
-60
lines changed

2 files changed

+84
-60
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 78 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -464,7 +464,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
464464
array_data.type(), "char_array", "char_array", loc, ID_java, symbol_table);
465465
symbol_exprt char_array=sym_char_array.symbol_expr();
466466
// char_array = array_pointer->data
467-
code.add(code_assignt(char_array, array_data));
467+
code.add(code_assignt(char_array, array_data), loc);
468468

469469
// string_expr is `{ rhs->length; string_array }`
470470
refined_string_exprt string_expr(
@@ -524,9 +524,9 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr(
524524
ID_java,
525525
symbol_table);
526526
symbol_exprt content_field = sym_content.symbol_expr();
527-
code.add(code_declt(content_field));
527+
code.add(code_declt(content_field), loc);
528528
refined_string_exprt str(length_field, content_field, refined_string_type);
529-
code.add(code_declt(length_field));
529+
code.add(code_declt(length_field), loc);
530530
return str;
531531
}
532532

@@ -545,7 +545,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
545545
const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
546546

547547
side_effect_expr_nondett nondet_length(str.length().type());
548-
code.add(code_assignt(str.length(), nondet_length));
548+
code.add(code_assignt(str.length(), nondet_length), loc);
549549

550550
exprt nondet_array_expr =
551551
make_nondet_infinite_char_array(symbol_table, loc, code);
@@ -559,7 +559,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
559559
add_array_to_length_association(
560560
nondet_array_expr, str.length(), symbol_table, loc, code);
561561

562-
code.add(code_assignt(str.content(), array_pointer));
562+
code.add(code_assignt(str.content(), array_pointer), loc);
563563

564564
return refined_string_exprt(str.length(), str.content());
565565
}
@@ -594,7 +594,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array(
594594
code_blockt &code)
595595
{
596596
exprt array=fresh_array(type, loc, symbol_table);
597-
code.add(code_declt(array));
597+
code.add(code_declt(array), loc);
598598
allocate_dynamic_object_with_decl(array, symbol_table, loc, code);
599599
return array;
600600
}
@@ -659,9 +659,9 @@ exprt make_nondet_infinite_char_array(
659659
ID_java,
660660
symbol_table);
661661
const symbol_exprt data_expr = data_sym.symbol_expr();
662-
code.add(code_declt(data_expr));
662+
code.add(code_declt(data_expr), loc);
663663
side_effect_expr_nondett nondet_data(data_expr.type());
664-
code.add(code_assignt(data_expr, nondet_data));
664+
code.add(code_assignt(data_expr, nondet_data), loc);
665665
return data_expr;
666666
}
667667

@@ -689,13 +689,14 @@ void add_pointer_to_array_association(
689689
ID_java,
690690
symbol_table);
691691
exprt return_expr = return_sym.symbol_expr();
692-
code.add(code_declt(return_expr));
692+
code.add(code_declt(return_expr), loc);
693693
code.add(
694694
code_assign_function_application(
695695
return_expr,
696696
ID_cprover_associate_array_to_pointer_func,
697697
{array, pointer},
698-
symbol_table));
698+
symbol_table),
699+
loc);
699700
}
700701

701702
/// Add a call to a primitive of the string solver, letting it know that
@@ -720,13 +721,14 @@ void add_array_to_length_association(
720721
ID_java,
721722
symbol_table);
722723
const exprt return_expr = return_sym.symbol_expr();
723-
code.add(code_declt(return_expr));
724+
code.add(code_declt(return_expr), loc);
724725
code.add(
725726
code_assign_function_application(
726727
return_expr,
727728
ID_cprover_associate_length_to_array_func,
728729
{array, length},
729-
symbol_table));
730+
symbol_table),
731+
loc);
730732
}
731733

732734
/// Add a call to a primitive of the string solver which ensures all characters
@@ -751,14 +753,15 @@ void add_character_set_constraint(
751753
symbolt &return_sym = get_fresh_aux_symbol(
752754
java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table);
753755
const exprt return_expr = return_sym.symbol_expr();
754-
code.add(code_declt(return_expr));
756+
code.add(code_declt(return_expr), loc);
755757
const constant_exprt char_set_expr(char_set, string_typet());
756758
code.add(
757759
code_assign_function_application(
758760
return_expr,
759761
ID_cprover_string_constrain_characters_func,
760762
{length, pointer, char_set_expr},
761-
symbol_table));
763+
symbol_table),
764+
loc);
762765
}
763766

764767
/// Create a refined_string_exprt `str` whose content and length are fresh
@@ -793,7 +796,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
793796
ID_java,
794797
symbol_table);
795798
const exprt return_code = return_code_sym.symbol_expr();
796-
code.add(code_declt(return_code));
799+
code.add(code_declt(return_code), loc);
797800

798801
const refined_string_exprt string_expr =
799802
make_nondet_string_expr(loc, symbol_table, code);
@@ -807,7 +810,8 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function(
807810
// return_code = <function_name>_data(args)
808811
code.add(
809812
code_assign_function_application(
810-
return_code, function_name, args, symbol_table));
813+
return_code, function_name, args, symbol_table),
814+
loc);
811815

812816
return string_expr;
813817
}
@@ -893,9 +897,9 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
893897
const exprt rhs_length = get_length(deref, symbol_table);
894898

895899
// Assignments
896-
code.add(code_assignt(lhs.length(), rhs_length));
900+
code.add(code_assignt(lhs.length(), rhs_length), loc);
897901
const exprt data_as_array = get_data(deref, symbol_table);
898-
code.add(code_assignt(lhs.content(), data_as_array));
902+
code.add(code_assignt(lhs.content(), data_as_array), loc);
899903
}
900904

901905
/// Create a string expression whose value is given by a literal
@@ -958,16 +962,21 @@ codet java_string_library_preprocesst::make_equals_function_code(
958962
const symbolt string_equals_sym = get_fresh_aux_symbol(
959963
java_boolean_type(), "string_equals", "str_eq", loc, ID_java, symbol_table);
960964
const symbol_exprt string_equals = string_equals_sym.symbol_expr();
961-
code.add(code_declt(string_equals));
962-
code.add(code_assignt(
963-
string_equals,
964-
make_function_application(
965-
ID_cprover_string_equal_func, args, type.return_type(), symbol_table)));
966-
967-
code.add(code_returnt(if_exprt(
968-
arg_is_string,
969-
string_equals,
970-
from_integer(false, java_boolean_type()))));
965+
code.add(code_declt(string_equals), loc);
966+
code.add(
967+
code_assignt(
968+
string_equals,
969+
make_function_application(
970+
ID_cprover_string_equal_func, args, type.return_type(), symbol_table)),
971+
loc);
972+
973+
code.add(
974+
code_returnt(
975+
if_exprt(
976+
arg_is_string,
977+
string_equals,
978+
from_integer(false, java_boolean_type()))),
979+
loc);
971980
return code;
972981
}
973982

@@ -1094,10 +1103,10 @@ codet java_string_library_preprocesst::make_float_to_string_code(
10941103
ife.else_case()=tmp_code;
10951104
tmp_code=ife;
10961105
}
1097-
code.add(tmp_code);
1106+
code.add(tmp_code, loc);
10981107

10991108
// Return str
1100-
code.add(code_returnt(str));
1109+
code.add(code_returnt(str), loc);
11011110
return code;
11021111
}
11031112

@@ -1144,8 +1153,8 @@ codet java_string_library_preprocesst::make_init_function_from_call(
11441153

11451154
// arg_this <- string_expr
11461155
code.add(
1147-
code_assign_string_expr_to_java_string(
1148-
arg_this, string_expr, symbol_table));
1156+
code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1157+
loc);
11491158

11501159
return code;
11511160
}
@@ -1168,10 +1177,11 @@ codet java_string_library_preprocesst::
11681177
code_typet::parameterst params=type.parameters();
11691178
PRECONDITION(!params.empty());
11701179
code_blockt code;
1171-
code.add(make_assign_function_from_call(
1172-
function_name, type, loc, symbol_table));
1180+
code.add(
1181+
make_assign_function_from_call(function_name, type, loc, symbol_table),
1182+
loc);
11731183
exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type());
1174-
code.add(code_returnt(arg_this));
1184+
code.add(code_returnt(arg_this), loc);
11751185
return code;
11761186
}
11771187

@@ -1288,14 +1298,14 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
12881298
dereference_exprt deref(
12891299
typecast_exprt(object, pointer_type), pointer_type.subtype());
12901300
member_exprt deref_value(deref, value_comp.get_name(), value_comp.type());
1291-
code.add(code_assignt(value, deref_value));
1301+
code.add(code_assignt(value, deref_value), loc);
12921302
return value;
12931303
}
12941304
}
12951305

12961306
warning() << object_type.get_identifier()
12971307
<< " not available to format function" << eom;
1298-
code.add(code_declt(value));
1308+
code.add(code_declt(value), loc);
12991309
return value;
13001310
}
13011311

@@ -1378,7 +1388,7 @@ exprt java_string_library_preprocesst::make_argument_for_format(
13781388
symbolt field_symbol=get_fresh_aux_symbol(
13791389
type, tmp_name, tmp_name, loc, ID_java, symbol_table);
13801390
field_expr=field_symbol.symbol_expr();
1381-
code.add(code_declt(field_expr));
1391+
code.add(code_declt(field_expr), loc);
13821392
}
13831393
else
13841394
field_expr = make_nondet_string_expr(loc, symbol_table, code);
@@ -1393,9 +1403,12 @@ exprt java_string_library_preprocesst::make_argument_for_format(
13931403
obj.type(), "tmp_format_obj", "tmp_format_obj", loc, ID_java, symbol_table);
13941404
symbol_exprt arg_i=object_symbol.symbol_expr();
13951405
allocate_dynamic_object_with_decl(arg_i, symbol_table, loc, code);
1396-
code.add(code_assignt(arg_i, obj));
1397-
code.add(code_assumet(not_exprt(equal_exprt(
1398-
arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))));
1406+
code.add(code_assignt(arg_i, obj), loc);
1407+
code.add(
1408+
code_assumet(
1409+
not_exprt(
1410+
equal_exprt(arg_i, null_pointer_exprt(to_pointer_type(arg_i.type()))))),
1411+
loc);
13991412

14001413
// if arg_i != null then [code_not_null]
14011414
code_ifthenelset code_avoid_null_arg;
@@ -1426,15 +1439,15 @@ exprt java_string_library_preprocesst::make_argument_for_format(
14261439
{
14271440
exprt value=get_primitive_value_of_object(
14281441
arg_i, name, loc, symbol_table, code_not_null);
1429-
code_not_null.add(code_assignt(field_expr, value));
1442+
code_not_null.add(code_assignt(field_expr, value), loc);
14301443
}
14311444
else
14321445
{
14331446
// TODO: date_time and hash_code not implemented
14341447
}
14351448
}
14361449

1437-
code.add(code_not_null);
1450+
code.add(code_not_null, loc);
14381451
return arg_i_struct;
14391452
}
14401453

@@ -1488,8 +1501,9 @@ codet java_string_library_preprocesst::make_string_format_code(
14881501
type.return_type(), loc, symbol_table, code);
14891502
code.add(
14901503
code_assign_string_expr_to_java_string(
1491-
java_string, string_expr, symbol_table));
1492-
code.add(code_returnt(java_string));
1504+
java_string, string_expr, symbol_table),
1505+
loc);
1506+
code.add(code_returnt(java_string), loc);
14931507
return code;
14941508
}
14951509

@@ -1523,7 +1537,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
15231537
symbolt class1_sym=get_fresh_aux_symbol(
15241538
class_type, "class_symbol", "class_symbol", loc, ID_java, symbol_table);
15251539
symbol_exprt class1=class1_sym.symbol_expr();
1526-
code.add(code_declt(class1));
1540+
code.add(code_declt(class1), loc);
15271541

15281542
// class_identifier is this->@class_identifier
15291543
member_exprt class_identifier(
@@ -1553,8 +1567,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
15531567
symbol_table.lookup_ref("java::java.lang.String").type);
15541568
exprt string1=allocate_fresh_string(string_ptr_type, loc, symbol_table, code);
15551569
code.add(
1556-
code_assign_string_expr_to_java_string(
1557-
string1, string_expr1, symbol_table));
1570+
code_assign_string_expr_to_java_string(string1, string_expr1, symbol_table),
1571+
loc);
15581572

15591573
// > class1 = Class.forName(string1)
15601574
code_function_callt fun_call;
@@ -1565,10 +1579,10 @@ codet java_string_library_preprocesst::make_object_get_class_code(
15651579
code_typet fun_type;
15661580
fun_type.return_type()=string1.type();
15671581
fun_call.function().type()=fun_type;
1568-
code.add(fun_call);
1582+
code.add(fun_call, loc);
15691583

15701584
// > return class1;
1571-
code.add(code_returnt(class1));
1585+
code.add(code_returnt(class1), loc);
15721586
return code;
15731587
}
15741588

@@ -1591,8 +1605,10 @@ codet java_string_library_preprocesst::make_function_from_call(
15911605
code_blockt code;
15921606
exprt::operandst args=process_parameters(
15931607
type.parameters(), loc, symbol_table, code);
1594-
code.add(code_return_function_application(
1595-
function_name, args, type.return_type(), symbol_table));
1608+
code.add(
1609+
code_return_function_application(
1610+
function_name, args, type.return_type(), symbol_table),
1611+
loc);
15961612
return code;
15971613
}
15981614

@@ -1629,10 +1645,11 @@ codet java_string_library_preprocesst::make_string_returning_function_from_call(
16291645
// Assign to string
16301646
exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
16311647
code.add(
1632-
code_assign_string_expr_to_java_string(str, string_expr, symbol_table));
1648+
code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1649+
loc);
16331650

16341651
// Return value
1635-
code.add(code_returnt(str));
1652+
code.add(code_returnt(str), loc);
16361653
return code;
16371654
}
16381655

@@ -1669,10 +1686,11 @@ codet java_string_library_preprocesst::make_copy_string_code(
16691686
// Allocate and assign the string
16701687
exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
16711688
code.add(
1672-
code_assign_string_expr_to_java_string(str, string_expr, symbol_table));
1689+
code_assign_string_expr_to_java_string(str, string_expr, symbol_table),
1690+
loc);
16731691

16741692
// Return value
1675-
code.add(code_returnt(str));
1693+
code.add(code_returnt(str), loc);
16761694
return code;
16771695
}
16781696

@@ -1707,8 +1725,8 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
17071725
// Assign string_expr to `this` object
17081726
symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
17091727
code.add(
1710-
code_assign_string_expr_to_java_string(
1711-
arg_this, string_expr, symbol_table));
1728+
code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1729+
loc);
17121730

17131731
return code;
17141732
}
@@ -1752,8 +1770,8 @@ codet java_string_library_preprocesst::make_init_from_array_code(
17521770
// Assign string_expr to `this` object
17531771
symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
17541772
code.add(
1755-
code_assign_string_expr_to_java_string(
1756-
arg_this, string_expr, symbol_table));
1773+
code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
1774+
loc);
17571775

17581776
return code;
17591777
}

src/util/std_code.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -108,6 +108,12 @@ class code_blockt:public codet
108108
copy_to_operands(code);
109109
}
110110

111+
void add(codet code, const source_locationt &loc)
112+
{
113+
code.add_source_location() = loc;
114+
add(code);
115+
}
116+
111117
void append(const code_blockt &extra_block);
112118

113119
// This is the closing '}' or 'END' at the end of a block

0 commit comments

Comments
 (0)