Skip to content

Commit d68708f

Browse files
author
svorenova
authored
Merge pull request #2658 from svorenova/bugfix_tg4365
[TG-2755] Add nondet-static option to JBMC and fix it for static initializers
2 parents 6749aaf + e37d051 commit d68708f

15 files changed

+446
-19
lines changed

‎jbmc/regression/jbmc/nondet-static/My$PInner.class‎

422 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/nondet-static/My$PSInner.class‎

1.45 KB
Binary file not shown.

‎jbmc/regression/jbmc/nondet-static/My$PrInner.class‎

415 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/nondet-static/My$PrSInner.class‎

1.4 KB
Binary file not shown.

‎jbmc/regression/jbmc/nondet-static/My.class‎

2.94 KB
Binary file not shown.

‎jbmc/regression/jbmc/nondet-static/My.java‎

Lines changed: 238 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
public class My {
2+
public static int val() { return 3; }
3+
4+
public static int p1;
5+
public static int p2 = 1;
6+
public static int p3;
7+
static { p3 = 2; }
8+
public static int p4 = val();
9+
public static Integer p5 = new Integer(5);
10+
11+
public static final int pf1 = 1;
12+
public static final int pf2;
13+
static { pf2 = 2; }
14+
public static final int pf3 = val();
15+
public static final Integer pf4 = new Integer(4);
16+
17+
private static int pr1;
18+
private static int pr2 = 1;
19+
private static int pr3;
20+
static { pr3 = 2; }
21+
private static int pr4 = val();
22+
private static Integer pr5 = new Integer(5);
23+
24+
private static final int prf1 = 1;
25+
private static final int prf2;
26+
static { prf2 = 2; }
27+
private static final int prf3 = val();
28+
private static final Integer prf4 = new Integer(4);
29+
30+
// for inner classes, the missing cases of the above fields do not compile
31+
public class PInner {
32+
public static final int pf1 = 1;
33+
34+
private static final int prf1 = 1;
35+
}
36+
37+
public static class PSInner {
38+
public static int p1;
39+
public static int p2 = 1;
40+
public static int p3;
41+
static { p3 = 2; }
42+
public static int p4 = val();
43+
public static Integer p5 = new Integer(5);
44+
45+
public static final int pf1 = 1;
46+
public static final int pf2;
47+
static { pf2 = 2; }
48+
public static final int pf3 = val();
49+
public static final Integer pf4 = new Integer(4);
50+
51+
private static int pr1;
52+
private static int pr2 = 1;
53+
private static int pr3;
54+
static { pr3 = 2; }
55+
private static int pr4 = val();
56+
private static Integer pr5 = new Integer(5);
57+
58+
private static final int prf1 = 1;
59+
private static final int prf2;
60+
static { prf2 = 2; }
61+
private static final int prf3 = val();
62+
private static final Integer prf4 = new Integer(4);
63+
}
64+
65+
private class PrInner {
66+
public static final int pf1 = 1;
67+
68+
private static final int prf1 = 1;
69+
}
70+
71+
private static class PrSInner {
72+
public static int p1;
73+
public static int p2 = 1;
74+
public static int p3;
75+
static { p3 = 2; }
76+
public static int p4 = val();
77+
public static Integer p5 = new Integer(5);
78+
79+
public static final int pf1 = 1;
80+
public static final int pf2;
81+
static { pf2 = 2; }
82+
public static final int pf3 = val();
83+
public static final Integer pf4 = new Integer(4);
84+
85+
private static int pr1;
86+
private static int pr2 = 1;
87+
private static int pr3;
88+
static { pr3 = 2; }
89+
private static int pr4 = val();
90+
private static Integer pr5 = new Integer(5);
91+
92+
private static final int prf1 = 1;
93+
private static final int prf2;
94+
static { prf2 = 2; }
95+
private static final int prf3 = val();
96+
private static final Integer prf4 = new Integer(4);
97+
}
98+
99+
public int field;
100+
public My(int i) {
101+
String s = "bla";
102+
field = i;
103+
if (p1 != 0)
104+
field = 108; // this line can only be covered with nondet-static
105+
if (p2 != 1)
106+
field = 108; // this line can only be covered with nondet-static
107+
if (p3 != 2)
108+
field = 108; // this line can only be covered with nondet-static
109+
if (p4 != 3)
110+
field = 108; // this line can only be covered with nondet-static
111+
if (!p5.equals(5))
112+
field = 108; // this line can only be covered with nondet-static
113+
114+
if (pf1 != 1)
115+
field = 108; // this line cannot be covered even with nondet-static
116+
if (pf2 != 2)
117+
field = 108; // this line cannot be covered even with nondet-static
118+
if (pf3 != 3)
119+
field = 108; // this line cannot be covered even with nondet-static
120+
if (!pf4.equals(4))
121+
field = 108; // this line cannot be covered even with nondet-static
122+
123+
if (pr1 != 0)
124+
field = 108; // this line can only be covered with nondet-static
125+
if (pr2 != 1)
126+
field = 108; // this line can only be covered with nondet-static
127+
if (pr3 != 2)
128+
field = 108; // this line can only be covered with nondet-static
129+
if (pr4 != 3)
130+
field = 108; // this line can only be covered with nondet-static
131+
if (!pr5.equals(5))
132+
field = 108; // this line can only be covered with nondet-static
133+
134+
if (prf1 != 1)
135+
field = 108; // this line cannot be covered even with nondet-static
136+
if (prf2 != 2)
137+
field = 108; // this line cannot be covered even with nondet-static
138+
if (prf3 != 3)
139+
field = 108; // this line cannot be covered even with nondet-static
140+
if (!prf4.equals(4))
141+
field = 108; // this line cannot be covered even with nondet-static
142+
143+
if (PInner.pf1 != 1)
144+
field = 108; // this line cannot be covered even with nondet-static
145+
146+
if (PInner.prf1 != 1)
147+
field = 108; // this line cannot be covered even with nondet-static
148+
149+
if (PSInner.p1 != 0)
150+
field = 108; // this line can only be covered with nondet-static
151+
if (PSInner.p2 != 1)
152+
field = 108; // this line can only be covered with nondet-static
153+
if (PSInner.p3 != 2)
154+
field = 108; // this line can only be covered with nondet-static
155+
if (PSInner.p4 != 3)
156+
field = 108; // this line can only be covered with nondet-static
157+
if (!PSInner.p5.equals(5))
158+
field = 108; // this line can only be covered with nondet-static
159+
160+
if (PSInner.pf1 != 1)
161+
field = 108; // this line cannot be covered even with nondet-static
162+
if (PSInner.pf2 != 2)
163+
field = 108; // this line cannot be covered even with nondet-static
164+
if (PSInner.pf3 != 3)
165+
field = 108; // this line cannot be covered even with nondet-static
166+
if (!PSInner.pf4.equals(4))
167+
field = 108; // this line cannot be covered even with nondet-static
168+
169+
if (PSInner.pr1 != 0)
170+
field = 108; // this line can only be covered with nondet-static
171+
if (PSInner.pr2 != 1)
172+
field = 108; // this line can only be covered with nondet-static
173+
if (PSInner.pr3 != 2)
174+
field = 108; // this line can only be covered with nondet-static
175+
if (PSInner.pr4 != 3)
176+
field = 108; // this line can only be covered with nondet-static
177+
if (!PSInner.pr5.equals(5))
178+
field = 108; // this line can only be covered with nondet-static
179+
180+
if (PSInner.prf1 != 1)
181+
field = 108; // this line cannot be covered even with nondet-static
182+
if (PSInner.prf2 != 2)
183+
field = 108; // this line cannot be covered even with nondet-static
184+
if (PSInner.prf3 != 3)
185+
field = 108; // this line cannot be covered even with nondet-static
186+
if (!PSInner.prf4.equals(4))
187+
field = 108; // this line cannot be covered even with nondet-static
188+
189+
if (PrInner.pf1 != 1)
190+
field = 108; // this line cannot be covered even with nondet-static
191+
192+
if (PrInner.prf1 != 1)
193+
field = 108; // this line cannot be covered even with nondet-static
194+
195+
if (PrSInner.p1 != 0)
196+
field = 108; // this line can only be covered with nondet-static
197+
if (PrSInner.p2 != 1)
198+
field = 108; // this line can only be covered with nondet-static
199+
if (PrSInner.p3 != 2)
200+
field = 108; // this line can only be covered with nondet-static
201+
if (PrSInner.p4 != 3)
202+
field = 108; // this line can only be covered with nondet-static
203+
if (!PrSInner.p5.equals(5))
204+
field = 108; // this line can only be covered with nondet-static
205+
206+
if (PrSInner.pf1 != 1)
207+
field = 108; // this line cannot be covered even with nondet-static
208+
if (PrSInner.pf2 != 2)
209+
field = 108; // this line cannot be covered even with nondet-static
210+
if (PrSInner.pf3 != 3)
211+
field = 108; // this line cannot be covered even with nondet-static
212+
if (!PrSInner.pf4.equals(4))
213+
field = 108; // this line cannot be covered even with nondet-static
214+
215+
if (PrSInner.pr1 != 0)
216+
field = 108; // this line can only be covered with nondet-static
217+
if (PrSInner.pr2 != 1)
218+
field = 108; // this line can only be covered with nondet-static
219+
if (PrSInner.pr3 != 2)
220+
field = 108; // this line can only be covered with nondet-static
221+
if (PrSInner.pr4 != 3)
222+
field = 108; // this line can only be covered with nondet-static
223+
if (!PrSInner.pr5.equals(5))
224+
field = 108; // this line can only be covered with nondet-static
225+
226+
if (PrSInner.prf1 != 1)
227+
field = 108; // this line cannot be covered even with nondet-static
228+
if (PrSInner.prf2 != 2)
229+
field = 108; // this line cannot be covered even with nondet-static
230+
if (PrSInner.prf3 != 3)
231+
field = 108; // this line cannot be covered even with nondet-static
232+
if (!PSInner.prf4.equals(4))
233+
field = 108; // this line cannot be covered even with nondet-static
234+
235+
if (s != "bla")
236+
field = 108; // this line cannot be covered even with nondet-static
237+
}
238+
}

‎jbmc/regression/jbmc/nondet-static/test.desc‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
CORE symex-driven-lazy-loading-expected-failure
2+
My.class
3+
--function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
7+
file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
8+
file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
9+
file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
10+
file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
11+
file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
12+
file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
13+
file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
14+
file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
15+
file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
16+
file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
17+
file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
18+
file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
19+
file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
20+
file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
21+
file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
22+
file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
23+
file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
24+
file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
25+
file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
26+
file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
27+
file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
28+
file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
29+
file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
30+
file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
31+
file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
32+
file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
33+
file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
34+
file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
35+
file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
36+
file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
37+
file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
38+
file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
39+
file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
40+
file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
41+
file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
42+
file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
43+
file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
44+
file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
45+
file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
46+
file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
47+
file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
48+
file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
49+
file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
50+
file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
51+
file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
52+
file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
53+
file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
54+
file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
55+
--
56+
file My\.java line 115 function java::My\.\<init\>:\(I\)V
57+
file My\.java line 135 function java::My\.\<init\>:\(I\)V
58+
file My\.java line 144 function java::My\.\<init\>:\(I\)V
59+
file My\.java line 147 function java::My\.\<init\>:\(I\)V
60+
file My\.java line 161 function java::My\.\<init\>:\(I\)V
61+
file My\.java line 181 function java::My\.\<init\>:\(I\)V
62+
file My\.java line 190 function java::My\.\<init\>:\(I\)V
63+
file My\.java line 193 function java::My\.\<init\>:\(I\)V
64+
file My\.java line 207 function java::My\.\<init\>:\(I\)V
65+
file My\.java line 227 function java::My\.\<init\>:\(I\)V
66+
--
67+
This tests nondet-static option
68+
69+
This fails under symex-driven lazy loading because nondet-static cannot be used
70+
with it

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -645,6 +645,8 @@ void java_bytecode_convert_classt::convert(
645645
// link matches the method used by java_bytecode_convert_method::convert
646646
// for methods.
647647
new_symbol.type.set(ID_C_class, class_symbol.name);
648+
new_symbol.type.set(ID_C_field, f.name);
649+
new_symbol.type.set(ID_C_constant, f.is_final);
648650
new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
649651
"."+id2string(f.name);
650652
new_symbol.mode=ID_java;

‎jbmc/src/java_bytecode/java_bytecode_language.cpp‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
157157
else
158158
java_cp_include_files=".*";
159159

160+
nondet_static = cmd.isset("nondet-static");
161+
160162
language_options_initialized=true;
161163
}
162164

@@ -1039,9 +1041,18 @@ bool java_bytecode_languaget::convert_single_method(
10391041
case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
10401042
if(threading_support)
10411043
symbol.value = get_thread_safe_clinit_wrapper_body(
1042-
function_id, symbol_table);
1044+
function_id,
1045+
symbol_table,
1046+
nondet_static,
1047+
object_factory_parameters,
1048+
get_pointer_type_selector());
10431049
else
1044-
symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
1050+
symbol.value = get_clinit_wrapper_body(
1051+
function_id,
1052+
symbol_table,
1053+
nondet_static,
1054+
object_factory_parameters,
1055+
get_pointer_type_selector());
10451056
break;
10461057
case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
10471058
symbol.value =

‎jbmc/src/java_bytecode/java_bytecode_language.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,7 @@ class java_bytecode_languaget:public languaget
193193
bool throw_assertion_error;
194194
java_string_library_preprocesst string_preprocess;
195195
std::string java_cp_include_files;
196+
bool nondet_static;
196197

197198
// list of classes to force load even without reference from the entry point
198199
std::vector<irep_idt> java_load_classes;

0 commit comments

Comments
 (0)