Skip to content

Commit 31245ed

Browse files
tautschnigtautschnig
authored
Merge pull request #4474 from tautschnig/messaget-java_string_library-preprocesst
java_string_library_preprocesst isn't a messaget [blocks: #3800]
2 parents 77a0496 + 47e3c93 commit 31245ed

File tree

3 files changed

+82
-40
lines changed

3 files changed

+82
-40
lines changed

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1356,8 +1356,8 @@ bool java_bytecode_languaget::convert_single_method_code(
13561356
writable_symbol, cmb->get().method.local_variable_table, symbol_table);
13571357
}
13581358
// Populate body of the function with code generated by string preprocess
1359-
codet generated_code =
1360-
string_preprocess.code_for_function(writable_symbol, symbol_table);
1359+
codet generated_code = string_preprocess.code_for_function(
1360+
writable_symbol, symbol_table, get_message_handler());
13611361
// String solver can make calls to functions that haven't yet been seen.
13621362
// Add these to the needed_lazy_methods collection
13631363
notify_static_method_calls(generated_code, needed_lazy_methods);

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 61 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -908,13 +908,17 @@ java_string_library_preprocesst::string_literal_to_string_expr(
908908
/// \param loc: location in the program_invocation_name
909909
/// \param function_id: function the generated code will be added to
910910
/// \param symbol_table: symbol table
911+
/// \param message_handler: a message handler
911912
/// \return Code corresponding to the Java conversion of floats to strings.
912913
code_blockt java_string_library_preprocesst::make_float_to_string_code(
913914
const java_method_typet &type,
914915
const source_locationt &loc,
915916
const irep_idt &function_id,
916-
symbol_table_baset &symbol_table)
917+
symbol_table_baset &symbol_table,
918+
message_handlert &message_handler)
917919
{
920+
(void)message_handler;
921+
918922
// Getting the argument
919923
java_method_typet::parameterst params = type.parameters();
920924
PRECONDITION(params.size()==1);
@@ -1153,6 +1157,7 @@ code_blockt java_string_library_preprocesst::make_assign_function_from_call(
11531157
/// \param loc: location in the source
11541158
/// \param function_id: function the generated code will be added to
11551159
/// \param symbol_table: the symbol table
1160+
/// \param message_handler: a message handler
11561161
/// \return Code corresponding to
11571162
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
11581163
/// string_expr1 = substr(obj->@class_identifier, 6)
@@ -1162,7 +1167,8 @@ code_blockt java_string_library_preprocesst::make_class_identifier_code(
11621167
const java_method_typet &type,
11631168
const source_locationt &loc,
11641169
const irep_idt &function_id,
1165-
symbol_table_baset &symbol_table)
1170+
symbol_table_baset &symbol_table,
1171+
message_handlert &message_handler)
11661172
{
11671173
java_method_typet::parameterst params = type.parameters();
11681174
PRECONDITION(!params.empty());
@@ -1283,6 +1289,7 @@ java_string_library_preprocesst::make_string_returning_function_from_call(
12831289
/// \param loc: location in the source
12841290
/// \param function_id: function the generated code will be added to
12851291
/// \param symbol_table: symbol table
1292+
/// \param message_handler: a message handler
12861293
/// \return Code corresponding to:
12871294
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
12881295
/// string_expr = string_to_string_expr(arg0)
@@ -1295,8 +1302,11 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
12951302
const java_method_typet &type,
12961303
const source_locationt &loc,
12971304
const irep_idt &function_id,
1298-
symbol_table_baset &symbol_table)
1305+
symbol_table_baset &symbol_table,
1306+
message_handlert &message_handler)
12991307
{
1308+
(void)message_handler;
1309+
13001310
// Code for the output
13011311
code_blockt code;
13021312

@@ -1331,6 +1341,7 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
13311341
/// \param function_id: name of the function (used for variable naming) where
13321342
/// the generated code ends up.
13331343
/// \param symbol_table: symbol table
1344+
/// \param message_handler: a message handler
13341345
/// \return Code corresponding to:
13351346
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
13361347
/// string_expr = java_string_to_string_expr(arg1)
@@ -1341,8 +1352,11 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
13411352
const java_method_typet &type,
13421353
const source_locationt &loc,
13431354
const irep_idt &function_id,
1344-
symbol_table_baset &symbol_table)
1355+
symbol_table_baset &symbol_table,
1356+
message_handlert &message_handler)
13451357
{
1358+
(void)message_handler;
1359+
13461360
code_blockt copy_constructor_body;
13471361

13481362
// String expression that will hold the result
@@ -1372,6 +1386,7 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
13721386
/// \param loc: location in the source
13731387
/// \param function_id: unused
13741388
/// \param symbol_table: symbol table
1389+
/// \param message_handler: a message handler
13751390
/// \return Code corresponding to:
13761391
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
13771392
/// str_expr = java_string_to_string_expr(this)
@@ -1382,9 +1397,11 @@ code_returnt java_string_library_preprocesst::make_string_length_code(
13821397
const java_method_typet &type,
13831398
const source_locationt &loc,
13841399
const irep_idt &function_id,
1385-
symbol_table_baset &symbol_table)
1400+
symbol_table_baset &symbol_table,
1401+
message_handlert &message_handler)
13861402
{
13871403
(void)function_id;
1404+
(void)message_handler;
13881405

13891406
const java_method_typet::parameterst &params = type.parameters();
13901407
PRECONDITION(!params[0].get_identifier().empty());
@@ -1434,11 +1451,13 @@ void java_string_library_preprocesst::get_all_function_names(
14341451
/// code but for which no implementation is provided.
14351452
/// \param symbol: symbol of the function to provide code for
14361453
/// \param symbol_table: a symbol table
1454+
/// \param message_handler: a message handler
14371455
/// \return Code for the body of the String functions if they are part of the
14381456
/// supported String functions, nil_exprt otherwise.
14391457
codet java_string_library_preprocesst::code_for_function(
14401458
const symbolt &symbol,
1441-
symbol_table_baset &symbol_table)
1459+
symbol_table_baset &symbol_table,
1460+
message_handlert &message_handler)
14421461
{
14431462
const irep_idt &function_id = symbol.name;
14441463
const java_method_typet &type = to_java_method_type(symbol.type);
@@ -1471,7 +1490,7 @@ codet java_string_library_preprocesst::code_for_function(
14711490
INVARIANT(
14721491
it != conversion_table.end(), "Couldn't retrieve code for string method");
14731492

1474-
return it->second(type, loc, function_id, symbol_table);
1493+
return it->second(type, loc, function_id, symbol_table, message_handler);
14751494
}
14761495

14771496
/// Check whether a class name is known as a string type.
@@ -1599,7 +1618,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
15991618
std::placeholders::_1,
16001619
std::placeholders::_2,
16011620
std::placeholders::_3,
1602-
std::placeholders::_4);
1621+
std::placeholders::_4,
1622+
std::placeholders::_5);
16031623
cprover_equivalent_to_java_function
16041624
["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
16051625
ID_cprover_string_parse_int_func;
@@ -1621,15 +1641,17 @@ void java_string_library_preprocesst::initialize_conversion_table()
16211641
std::placeholders::_1,
16221642
std::placeholders::_2,
16231643
std::placeholders::_3,
1624-
std::placeholders::_4);
1644+
std::placeholders::_4,
1645+
std::placeholders::_5);
16251646
conversion_table
16261647
["java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
16271648
&java_string_library_preprocesst::make_copy_constructor_code,
16281649
this,
16291650
std::placeholders::_1,
16301651
std::placeholders::_2,
16311652
std::placeholders::_3,
1632-
std::placeholders::_4);
1653+
std::placeholders::_4,
1654+
std::placeholders::_5);
16331655
cprover_equivalent_to_java_constructor
16341656
["java::java.lang.String.<init>:()V"]=
16351657
ID_cprover_string_empty_string_func;
@@ -1683,7 +1705,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
16831705
std::placeholders::_1,
16841706
std::placeholders::_2,
16851707
std::placeholders::_3,
1686-
std::placeholders::_4);
1708+
std::placeholders::_4,
1709+
std::placeholders::_5);
16871710
cprover_equivalent_to_java_string_returning_function
16881711
["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
16891712
ID_cprover_string_replace_func;
@@ -1706,7 +1729,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17061729
std::placeholders::_1,
17071730
std::placeholders::_2,
17081731
std::placeholders::_3,
1709-
std::placeholders::_4);
1732+
std::placeholders::_4,
1733+
std::placeholders::_5);
17101734
cprover_equivalent_to_java_string_returning_function
17111735
["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
17121736
ID_cprover_string_to_upper_case_func;
@@ -1722,7 +1746,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17221746
std::placeholders::_1,
17231747
std::placeholders::_2,
17241748
std::placeholders::_3,
1725-
std::placeholders::_4);
1749+
std::placeholders::_4,
1750+
std::placeholders::_5);
17261751
conversion_table
17271752
["java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
17281753
std::bind(
@@ -1731,7 +1756,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17311756
std::placeholders::_1,
17321757
std::placeholders::_2,
17331758
std::placeholders::_3,
1734-
std::placeholders::_4);
1759+
std::placeholders::_4,
1760+
std::placeholders::_5);
17351761
cprover_equivalent_to_java_constructor
17361762
["java::java.lang.StringBuilder.<init>:()V"]=
17371763
ID_cprover_string_empty_string_func;
@@ -1773,7 +1799,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17731799
std::placeholders::_1,
17741800
std::placeholders::_2,
17751801
std::placeholders::_3,
1776-
std::placeholders::_4);
1802+
std::placeholders::_4,
1803+
std::placeholders::_5);
17771804
cprover_equivalent_to_java_string_returning_function
17781805
["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
17791806
ID_cprover_string_substring_func;
@@ -1787,7 +1814,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17871814
std::placeholders::_1,
17881815
std::placeholders::_2,
17891816
std::placeholders::_3,
1790-
std::placeholders::_4);
1817+
std::placeholders::_4,
1818+
std::placeholders::_5);
17911819

17921820
// StringBuffer library
17931821
conversion_table
@@ -1797,7 +1825,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
17971825
std::placeholders::_1,
17981826
std::placeholders::_2,
17991827
std::placeholders::_3,
1800-
std::placeholders::_4);
1828+
std::placeholders::_4,
1829+
std::placeholders::_5);
18011830
cprover_equivalent_to_java_constructor
18021831
["java::java.lang.StringBuffer.<init>:()V"]=
18031832
ID_cprover_string_empty_string_func;
@@ -1838,7 +1867,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
18381867
std::placeholders::_1,
18391868
std::placeholders::_2,
18401869
std::placeholders::_3,
1841-
std::placeholders::_4);
1870+
std::placeholders::_4,
1871+
std::placeholders::_5);
18421872

18431873
// CharSequence library
18441874
cprover_equivalent_to_java_function
@@ -1851,7 +1881,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
18511881
std::placeholders::_1,
18521882
std::placeholders::_2,
18531883
std::placeholders::_3,
1854-
std::placeholders::_4);
1884+
std::placeholders::_4,
1885+
std::placeholders::_5);
18551886
conversion_table
18561887
["java::java.lang.CharSequence.length:()I"]=
18571888
conversion_table["java::java.lang.String.length:()I"];
@@ -1860,13 +1891,15 @@ void java_string_library_preprocesst::initialize_conversion_table()
18601891
cprover_equivalent_to_java_string_returning_function
18611892
["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
18621893
ID_cprover_string_of_int_hex_func;
1863-
conversion_table["java::org.cprover.CProver.classIdentifier:("
1864-
"Ljava/lang/Object;)Ljava/lang/String;"] =
1865-
std::bind(
1866-
&java_string_library_preprocesst::make_class_identifier_code,
1867-
this,
1868-
std::placeholders::_1,
1869-
std::placeholders::_2,
1870-
std::placeholders::_3,
1871-
std::placeholders::_4);
1894+
conversion_table
1895+
["java::org.cprover.CProver.classIdentifier:("
1896+
"Ljava/lang/Object;)Ljava/lang/String;"] =
1897+
std::bind(
1898+
&java_string_library_preprocesst::make_class_identifier_code,
1899+
this,
1900+
std::placeholders::_1,
1901+
std::placeholders::_2,
1902+
std::placeholders::_3,
1903+
std::placeholders::_4,
1904+
std::placeholders::_5);
18721905
}

‎jbmc/src/java_bytecode/java_string_library_preprocess.h

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ Date: March 2017
1414
#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
1515
#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
1616

17-
#include <util/ui_message.h>
1817
#include <util/std_code.h>
1918
#include <util/symbol_table.h>
2019
#include <util/refined_string_type.h>
@@ -29,10 +28,12 @@ Date: March 2017
2928
#include "character_refine_preprocess.h"
3029
#include "java_types.h"
3130

31+
class message_handlert;
32+
3233
// Arbitrary limit of 10 arguments for the number of arguments to String.format
3334
#define MAX_FORMAT_ARGS 10
3435

35-
class java_string_library_preprocesst:public messaget
36+
class java_string_library_preprocesst
3637
{
3738
public:
3839
java_string_library_preprocesst()
@@ -48,8 +49,10 @@ class java_string_library_preprocesst:public messaget
4849
bool implements_function(const irep_idt &function_id) const;
4950
void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
5051

51-
codet
52-
code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table);
52+
codet code_for_function(
53+
const symbolt &symbol,
54+
symbol_table_baset &symbol_table,
55+
message_handlert &message_handler);
5356

5457
codet replace_character_call(code_function_callt call)
5558
{
@@ -102,7 +105,8 @@ class java_string_library_preprocesst:public messaget
102105
const java_method_typet &,
103106
const source_locationt &,
104107
const irep_idt &,
105-
symbol_table_baset &)>
108+
symbol_table_baset &,
109+
message_handlert &)>
106110
conversion_functiont;
107111

108112
typedef std::unordered_map<irep_idt, irep_idt> id_mapt;
@@ -149,31 +153,36 @@ class java_string_library_preprocesst:public messaget
149153
const java_method_typet &type,
150154
const source_locationt &loc,
151155
const irep_idt &function_id,
152-
symbol_table_baset &symbol_table);
156+
symbol_table_baset &symbol_table,
157+
message_handlert &message_handler);
153158

154159
code_blockt make_copy_string_code(
155160
const java_method_typet &type,
156161
const source_locationt &loc,
157162
const irep_idt &function_id,
158-
symbol_table_baset &symbol_table);
163+
symbol_table_baset &symbol_table,
164+
message_handlert &message_handler);
159165

160166
code_blockt make_copy_constructor_code(
161167
const java_method_typet &type,
162168
const source_locationt &loc,
163169
const irep_idt &function_id,
164-
symbol_table_baset &symbol_table);
170+
symbol_table_baset &symbol_table,
171+
message_handlert &message_handler);
165172

166173
code_returnt make_string_length_code(
167174
const java_method_typet &type,
168175
const source_locationt &loc,
169176
const irep_idt &function_id,
170-
symbol_table_baset &symbol_table);
177+
symbol_table_baset &symbol_table,
178+
message_handlert &message_handler);
171179

172180
code_blockt make_class_identifier_code(
173181
const java_method_typet &type,
174182
const source_locationt &loc,
175183
const irep_idt &function_id,
176-
symbol_table_baset &symbol_table);
184+
symbol_table_baset &symbol_table,
185+
message_handlert &message_handler);
177186

178187
// Helper functions
179188
exprt::operandst process_parameters(

0 commit comments

Comments
 (0)