Skip to content

Commit b5a205a

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #425 from mgudemann/clean_pr_java_front_end
Basic java front end improvements
2 parents aa99900 + a0e251f commit b5a205a

35 files changed

+1731
-523
lines changed

‎regression/cbmc-java/NullPointer1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer1.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer1.java line 16$
6+
^ file NullPointer1.java line 16 function java::NullPointer1.main:(\[Ljava/lang/String;)V$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎regression/cbmc-java/NullPointer2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer2.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer2.java line 9$
6+
^ file NullPointer2.java line 9 function java::NullPointer2.main:(\[Ljava/lang/String;)V$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎regression/cbmc-java/NullPointer3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer3.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer3.java line 5$
6+
^ file NullPointer3.java line 5 function java::NullPointer3.main:(\[Ljava/lang/String;)V bytecode_index 1$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎regression/cbmc-java/NullPointer4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ NullPointer4.class
33
--pointer-check --stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
6-
^ file NullPointer4.java line 6$
6+
^ file NullPointer4.java line 6 function java::NullPointer4.main:(\[Ljava/lang/String;)V$
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎src/cegis/refactor/constraint/constraint_factory.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ void create_or_redirect_entry(symbol_tablet &st, goto_functionst &gf)
4141
if (fmap.end() == it)
4242
{
4343
config.main=CONSTRAINT_CALLER;
44-
assert(!java_entry_point(st, ID_empty, msg));
44+
assert(!java_entry_point(st, ID_empty, msg, false, 0));
4545
goto_convert(CPROVER_INIT, st, gf, msg);
4646
goto_convert(goto_functionst::entry_point(), st, gf, msg);
4747
} else

‎src/java_bytecode/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ SRC = java_bytecode_language.cpp java_bytecode_parse_tree.cpp \
55
java_bytecode_typecheck_type.cpp java_bytecode_internal_additions.cpp \
66
java_root_class.cpp java_bytecode_parser.cpp bytecode_info.cpp \
77
java_class_loader.cpp jar_file.cpp java_object_factory.cpp \
8-
java_bytecode_convert_method.cpp java_local_variable_table.cpp
8+
java_bytecode_convert_method.cpp java_local_variable_table.cpp \
9+
java_pointer_casts.cpp java_utils.cpp
910

1011
INCLUDES= -I ..
1112

‎src/java_bytecode/expr2java.cpp

+51-47
Original file line numberDiff line numberDiff line change
@@ -15,45 +15,12 @@ Author: Daniel Kroening, [email protected]
1515
#include <util/arith_tools.h>
1616

1717
#include <ansi-c/c_qualifiers.h>
18+
#include <ansi-c/c_misc.h>
1819
#include <ansi-c/expr2c_class.h>
1920

2021
#include "java_types.h"
2122
#include "expr2java.h"
2223

23-
class expr2javat:public expr2ct
24-
{
25-
public:
26-
expr2javat(const namespacet &_ns):expr2ct(_ns) { }
27-
28-
std::string convert(const exprt &src) override
29-
{
30-
return expr2ct::convert(src);
31-
}
32-
33-
std::string convert(const typet &src) override
34-
{
35-
return expr2ct::convert(src);
36-
}
37-
38-
protected:
39-
std::string convert(const exprt &src, unsigned &precedence) override;
40-
std::string convert_java_this(const exprt &src, unsigned precedence);
41-
std::string convert_java_instanceof(const exprt &src, unsigned precedence);
42-
std::string convert_java_new(const exprt &src, unsigned precedence);
43-
std::string convert_code_java_delete(const exprt &src, unsigned precedence);
44-
std::string convert_struct(const exprt &src, unsigned &precedence) override;
45-
std::string convert_code(const codet &src, unsigned indent) override;
46-
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
47-
std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
48-
49-
std::string convert_rec(
50-
const typet &src,
51-
const c_qualifierst &qualifiers,
52-
const std::string &declarator) override;
53-
54-
typedef std::unordered_set<std::string, string_hash> id_sett;
55-
};
56-
5724
/*******************************************************************\
5825
5926
Function: expr2javat::convert_code_function_call
@@ -83,7 +50,6 @@ std::string expr2javat::convert_code_function_call(
8350
unsigned p;
8451
std::string lhs_str=convert(src.lhs(), p);
8552

86-
// TODO: ggf. Klammern je nach p
8753
dest+=lhs_str;
8854
dest+='=';
8955
}
@@ -124,8 +90,10 @@ std::string expr2javat::convert_code_function_call(
12490
unsigned p;
12591
std::string arg_str=convert(*it, p);
12692

127-
if(first) first=false; else dest+=", ";
128-
// TODO: ggf. Klammern je nach p
93+
if(first)
94+
first=false;
95+
else
96+
dest+=", ";
12997
dest+=arg_str;
13098
}
13199
}
@@ -244,15 +212,16 @@ std::string expr2javat::convert_constant(
244212
else if(src.type()==java_char_type())
245213
{
246214
std::string dest;
247-
dest.reserve(10);
215+
dest.reserve(char_representation_length);
248216

249217
mp_integer int_value;
250-
to_integer(src, int_value);
218+
if(!to_integer(src, int_value))
219+
assert(false);
251220

252-
dest+='\'';
221+
dest+="(char)'";
253222

254223
if(int_value>=' ' && int_value<127)
255-
dest+=(char)(int_value.to_long());
224+
dest+=static_cast<char>(int_value.to_long());
256225
else
257226
{
258227
std::string hex=integer2string(int_value, 16);
@@ -265,6 +234,26 @@ std::string expr2javat::convert_constant(
265234
dest+='\'';
266235
return dest;
267236
}
237+
else if(src.type()==java_byte_type())
238+
{
239+
// No byte-literals in Java, so just cast:
240+
mp_integer int_value;
241+
if(!to_integer(src, int_value))
242+
assert(false);
243+
std::string dest="(byte)";
244+
dest+=integer2string(int_value);
245+
return dest;
246+
}
247+
else if(src.type()==java_short_type())
248+
{
249+
// No short-literals in Java, so just cast:
250+
mp_integer int_value;
251+
if(!to_integer(src, int_value))
252+
assert(false);
253+
std::string dest="(short)";
254+
dest+=integer2string(int_value);
255+
return dest;
256+
}
268257
else if(src.type()==java_long_type())
269258
{
270259
// long integer literals must have 'L' at the end
@@ -319,7 +308,7 @@ std::string expr2javat::convert_rec(
319308
else if(src==java_double_type())
320309
return q+"double"+d;
321310
else if(src==java_boolean_type())
322-
return q+"bool"+d;
311+
return q+"boolean"+d;
323312
else if(src==java_byte_type())
324313
return q+"byte"+d;
325314
else if(src.id()==ID_code)
@@ -348,7 +337,8 @@ std::string expr2javat::convert_rec(
348337

349338
if(code_type.has_ellipsis())
350339
{
351-
if(!parameters.empty()) dest+=", ";
340+
if(!parameters.empty())
341+
dest+=", ";
352342
dest+="...";
353343
}
354344

@@ -491,9 +481,10 @@ std::string expr2javat::convert(
491481
const exprt &src,
492482
unsigned &precedence)
493483
{
484+
const typet &type=ns.follow(src.type());
494485
if(src.id()=="java-this")
495486
return convert_java_this(src, precedence=15);
496-
if(src.id()=="java_instanceof")
487+
if(src.id()==ID_java_instanceof)
497488
return convert_java_instanceof(src, precedence=15);
498489
else if(src.id()==ID_side_effect &&
499490
(src.get(ID_statement)==ID_java_new ||
@@ -509,9 +500,22 @@ std::string expr2javat::convert(
509500
else if(src.id()=="pod_constructor")
510501
return "pod_constructor";
511502
else if(src.id()==ID_virtual_function)
512-
return convert_function(src, "VIRTUAL_FUNCTION", precedence=16);
503+
{
504+
return "VIRTUAL_FUNCTION(" +
505+
id2string(src.get(ID_C_class)) +
506+
"." +
507+
id2string(src.get(ID_component_name)) +
508+
")";
509+
}
513510
else if(src.id()==ID_java_string_literal)
514-
return '"'+id2string(src.get(ID_value))+'"'; // Todo: add escaping as needed
511+
return '"'+MetaString(src.get_string(ID_value))+'"';
512+
else if(src.id()==ID_constant && (type.id()==ID_bool || type.id()==ID_c_bool))
513+
{
514+
if(src.is_true())
515+
return "true";
516+
else
517+
return "false";
518+
}
515519
else
516520
return expr2ct::convert(src, precedence);
517521
}
@@ -536,7 +540,7 @@ std::string expr2javat::convert_code(
536540

537541
if(statement==ID_java_new ||
538542
statement==ID_java_new_array)
539-
return convert_java_new(src,indent);
543+
return convert_java_new(src, indent);
540544

541545
if(statement==ID_function_call)
542546
return convert_code_function_call(to_code_function_call(src), indent);

‎src/java_bytecode/expr2java.h

+45-4
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,51 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H
1111

1212
#include <string>
13-
14-
class exprt;
15-
class namespacet;
16-
class typet;
13+
#include <ansi-c/expr2c_class.h>
14+
15+
class expr2javat:public expr2ct
16+
{
17+
public:
18+
explicit expr2javat(const namespacet &_ns):expr2ct(_ns) { }
19+
20+
virtual std::string convert(const exprt &src)
21+
{
22+
return expr2ct::convert(src);
23+
}
24+
25+
virtual std::string convert(const typet &src)
26+
{
27+
return expr2ct::convert(src);
28+
}
29+
30+
protected:
31+
virtual std::string convert(const exprt &src, unsigned &precedence);
32+
virtual std::string convert_java_this(const exprt &src, unsigned precedence);
33+
virtual std::string convert_java_instanceof(
34+
const exprt &src,
35+
unsigned precedence);
36+
virtual std::string convert_java_new(const exprt &src, unsigned precedence);
37+
virtual std::string convert_code_java_delete(
38+
const exprt &src,
39+
unsigned precedence);
40+
virtual std::string convert_struct(const exprt &src, unsigned &precedence);
41+
virtual std::string convert_code(const codet &src, unsigned indent);
42+
virtual std::string convert_constant(
43+
const constant_exprt &src,
44+
unsigned &precedence);
45+
virtual std::string convert_code_function_call(
46+
const code_function_callt &src,
47+
unsigned indent);
48+
49+
virtual std::string convert_rec(
50+
const typet &src,
51+
const c_qualifierst &qualifiers,
52+
const std::string &declarator);
53+
54+
// length of string representation of Java Char
55+
// representation is '\u0000'
56+
const std::size_t char_representation_length=8;
57+
};
1758

1859
std::string expr2java(const exprt &expr, const namespacet &ns);
1960
std::string type2java(const typet &type, const namespacet &ns);

0 commit comments

Comments
 (0)