Symbolic (Java) PathFinder
SPF 是能够在 Java 字节码上进行符号执行的一个工具，它通过对字节码进行非标准解释执行（non-standard interpretation），支持对包含基本类型参数（如int、long、double、boolean等）的方法进行符号执行，并进一步支持符号化字符串（symbolic strings）、数组及用户自定义数据结构。SPF 是一个 JPF(Java PathFinder) 的扩展
安装和配置
实验环境和版本信息
- 选择 SPF 的 gradle build 和 Java 11 的版本（gradle-build-java-11 分支）
- 操作系统：Windows Subsystem for Linux - archlinux (2.4.13)
- openjdk version “11.0.26” 2025-01-21
- OpenJDK Runtime Environment (build 11.0.26+4)
- OpenJDK 64-Bit Server VM (build 11.0.26+4, mixed mode)
- Gradle: 8.13
安装
参考：https://github.com/SymbolicPathFinder/jpf-symbc/blob/gradle-build-java-11/README.md
1
2
3
4
5
6
| # 需要包含 jpf-core 子模块
git clone -b gradle-build-java-11 --recurse-submodules git@github.com:SymbolicPathFinder/jpf-symbc.git SPF
cd SPF
# build
gradle :jpf-core:buildJars
gradle :jpf-symbc:buildJars
|
跑一个简单的例子：
1
2
| cd jpf-symbc
java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar ./src/examples/demo/NumericExample.jpf
|
输出如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
| symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 052390b95ebe2bca062c31e6c1e52a6f13d68d5f) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
demo.NumericExample.main()
====================================================== search started: 4/10/25, 10:05 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Property Violated: PC is constraint # = 1
((a_1_SYMINT[-2147483648] + b_2_SYMINT[-2147483646]) - CONST_2) == CONST_0
Property Violated: result is "java.lang.ArithmeticException: div by 0..."
****************************
====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: div by 0
at demo.NumericExample.test(NumericExample.java:26)
at demo.NumericExample.main(NumericExample.java:34)
====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at demo.NumericExample.test(NumericExample.java:26)
at demo.NumericExample.main(NumericExample.java:34)
====================================================== Method Summaries
Inputs: a_1_SYMINT,b_2_SYMINT
demo.NumericExample.test(-2147483648,-2147483646) --> "java.lang.ArithmeticException: div by 0..."
====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for demo.NumericExample.test (Path Coverage) </h1>
<table border=1>
<tr><td>a_1_SYMINT</td><td>b_2_SYMINT</td><td>RETURN</td></tr>
<tr><td>-2147483648</td><td>-2147483646</td><td>"java.lang.ArithmeticException: div by 0..."</td></tr>
</table>
====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: div by 0 at demo.N..."
====================================================== statistics
elapsed time: 00:00:00
states: new=3,visited=0,backtracked=3,end=0
search: maxDepth=2,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1
heap: new=517,released=15,maxLive=0,gcCycles=1
instructions: 9176
max memory: 124MB
loaded code: classes=85,methods=1784
====================================================== search finished: 4/10/25, 10:05 AM
|
简单使用
在 ${jpf-symbc}/src/example 目录下有很多例子，可以从中研究一下 .jpf 配置文件的内容，如何处理不同的情况和需求。
jpf-symbc 的配置文件的一些内容
- classpath 和 sourcepath 需要指定要进行测试的类的源码路径和编译后的 .class 文件的路径
- symbolic.bp 配置使用的约束求解器，例如：
symbolic.bp=z3, symbolic_bp=no_solver - listener 配置监听器并在最终输出哪些内容，选择哪一个 listener，
listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener 会输出生成的测试代码等，listener = .symbc.SymbolicListener 会输出生成的测试用例等
自己编写一些 example 进行测试
在 examples/ 下新建文件夹 mytests，自己写用例进行测试:
examples/mytests/NonLinerEquation.java:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
| package mytests;
public class NonLinerEquation {
public static int test (int a, int b, int c) {
if (a > 100)
return 200;
int x = a * b + c;
int y = a + b * c;
int z = a * c + b;
if (x > 0) {
if (y > 0) {
if (z > 0) {
return 3;
} else {
return -1;
}
}
else {
return -2;
}
} else {
return 0;
}
}
public static void main(String[] args) {
int a =gov.nasa.jpf.symbc.Debug.makeSymbolicInteger("a");
int b =gov.nasa.jpf.symbc.Debug.makeSymbolicInteger("b");
int c =gov.nasa.jpf.symbc.Debug.makeSymbolicInteger("c");
int result = test(a, b, c);
System.out.println("Result: " + result);
}
}
|
examples/mytests/NonLinerEquation.jpf:
1
2
3
4
5
6
7
8
9
| target=mytests.NonLinerEquation
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples
symbolic.method = mytests.NonLinerEquation.test(sym#sym#sym)
# symbolic.min_int=-100
# symbolic.max_int=100
symbolic.dp=z3
listener = gov.nasa.jpf.symbc.SymbolicListener
# listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
|
在运行中，出现 java.lang.UnsatisfiedLinkError: no libz3java in java.library.path error，这是由于 Z3 求解器需要另外安装，通过 sudo pacman -S z3 安装之后解决。
最终输出如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
| symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 052390b95ebe2bca062c31e6c1e52a6f13d68d5f) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
mytests.NonLinerEquation.main()
====================================================== search started: 4/10/25, 10:47 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Result: 200
Result: 1
Result: -1
Result: 10
Result: 0
====================================================== Method Summaries
Inputs: a_1_SYMINT,b_2_SYMINT,c_3_SYMINT
mytests.NonLinerEquation.test(101,-9223372036854775808(don't care),-9223372036854775808(don't care)) --> Return Value: 200
mytests.NonLinerEquation.test(1,1,0) --> Return Value: 1
mytests.NonLinerEquation.test(4,1,-3) --> Return Value: -1
mytests.NonLinerEquation.test(0,0,1) --> Return Value: 10
mytests.NonLinerEquation.test(0,0,0) --> Return Value: 0
====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for mytests.NonLinerEquation.test (Path Coverage) </h1>
<table border=1>
<tr><td>a_1_SYMINT</td><td>b_2_SYMINT</td><td>c_3_SYMINT</td><td>RETURN</td></tr>
<tr><td>101</td><td>-9223372036854775808(don't care)</td><td>-9223372036854775808(don't care)</td><td>Return Value: 200</td></tr>
<tr><td>1</td><td>1</td><td>0</td><td>Return Value: 1</td></tr>
<tr><td>4</td><td>1</td><td>-3</td><td>Return Value: -1</td></tr>
<tr><td>0</td><td>0</td><td>1</td><td>Return Value: 10</td></tr>
<tr><td>0</td><td>0</td><td>0</td><td>Return Value: 0</td></tr>
</table>
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=9,visited=0,backtracked=9,end=5
search: maxDepth=5,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=4
heap: new=650,released=105,maxLive=505,gcCycles=6
instructions: 11535
max memory: 124MB
loaded code: classes=87,methods=2345
====================================================== search finished: 4/10/25, 10:47 AM
|
打印 Path Condition (PC)
利用 Debug.printPC() 可以打印不同路径的条件：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
| package mytests;
import gov.nasa.jpf.symbc.Debug;
public class CollectConstraints {
public static void test(int x, int y) {
int z = x + y;
if (z != 0) {
if (x > 0) {
System.out.println("Visiting the branch x > 0");
} else {
System.out.println("Visiting the branch y < 0");
}
} else {
System.out.println("Visiting the branch z == 0");
}
Debug.printPC("PC ");
}
// The test driver
public static void main(String[] args) {
int x = 2;
int y = 3;
// x = Debug.addSymbolicInt(x, "sym_x");
// y = Debug.addSymbolicInt(y, "sym_y");
test(x, y);
}
}
|
1
2
3
4
5
6
7
8
9
10
11
12
| target=mytests.CollectConstraints
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples
symbolic.method = mytests.CollectConstraints.test(sym#sym)
symbolic.dp=z3
symbolic.optimizechoices=false
#symbolic.debug=true
# listener = .symbc.SymbolicListener
listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
|
进行分析，输出为：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
| symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 052390b95ebe2bca062c31e6c1e52a6f13d68d5f) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
mytests.CollectConstraints.main()
====================================================== search started: 4/14/25, 10:04 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Visiting the branch x > 0
PC constraint # = 2
x_1_SYMINT > CONST_0 &&
(y_2_SYMINT + x_1_SYMINT) != CONST_0
Visiting the branch y < 0
PC constraint # = 2
x_1_SYMINT <= CONST_0 &&
(y_2_SYMINT + x_1_SYMINT) != CONST_0
Visiting the branch z == 0
PC constraint # = 1
(y_2_SYMINT + x_1_SYMINT) == CONST_0
====================================================== Method Sequences
[test(1,-2)]
[test(0,-1)]
[test(0,0)]
====================================================== JUnit 4.0 test class
import static org.junit.Assert.*;
import org.junit.Before;
import org.junit.Test;
public class mytests_CollectConstraintsTest {
private mytests.CollectConstraints mytests_collectconstraints;
@Before
public void setUp() throws Exception {
mytests_collectconstraints = new mytests.CollectConstraints();
}
@Test
public void test0() {
mytests_collectconstraints.test(1,-2);
}
@Test
public void test1() {
mytests_collectconstraints.test(0,-1);
}
@Test
public void test2() {
mytests_collectconstraints.test(0,0);
}
}
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=6,visited=0,backtracked=6,end=3
search: maxDepth=4,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=3
heap: new=522,released=42,maxLive=486,gcCycles=4
instructions: 9255
max memory: 124MB
loaded code: classes=82,methods=1800
====================================================== search finished: 4/14/25, 10:04 AM
|
Assume
利用 Debug.assume()，可以指定条件进行分析：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
| package mytests;
import gov.nasa.jpf.symbc.Debug;
public class CollectConstraints {
public static void test(int x, int y) {
int z = x + y;
Debug.assume(z != 0);
if (z != 0) {
if (x > 0) {
System.out.println("Visiting the branch x > 0");
} else {
System.out.println("Visiting the branch y < 0");
}
} else {
System.out.println("Visiting the branch z == 0");
}
Debug.printPC("PC ");
}
// The test driver
public static void main(String[] args) {
int x = 2;
int y = 3;
// x = Debug.addSymbolicInt(x, "sym_x");
// y = Debug.addSymbolicInt(y, "sym_y");
test(x, y);
}
}
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
| symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 052390b95ebe2bca062c31e6c1e52a6f13d68d5f) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
mytests.CollectConstraints.main()
====================================================== search started: 4/14/25, 10:07 AM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Visiting the branch x > 0
PC constraint # = 2
x_1_SYMINT > CONST_0 &&
(y_2_SYMINT + x_1_SYMINT) != CONST_0
Visiting the branch y < 0
PC constraint # = 2
x_1_SYMINT <= CONST_0 &&
(y_2_SYMINT + x_1_SYMINT) != CONST_0
====================================================== Method Summaries
Inputs: x_1_SYMINT,y_2_SYMINT
mytests.CollectConstraints.test(1,-2) --> Return Value: --
mytests.CollectConstraints.test(-1,0) --> Return Value: --
====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for mytests.CollectConstraints.test (Path Coverage) </h1>
<table border=1>
<tr><td>x_1_SYMINT</td><td>y_2_SYMINT</td><td>RETURN</td></tr>
<tr><td>1</td><td>-2</td><td>Return Value: --</td></tr>
<tr><td>-1</td><td>0</td><td>Return Value: --</td></tr>
</table>
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=7,visited=0,backtracked=7,end=2
search: maxDepth=4,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=3
heap: new=515,released=33,maxLive=489,gcCycles=4
instructions: 9244
max memory: 124MB
loaded code: classes=82,methods=1800
====================================================== search finished: 4/14/25, 10:07 AM
|
引入其他 Java 库进行测试
需要在 gradle 的配置文件中添加依赖，要注意的是，main 源码包以外的源码包（比如example）的依赖添加需要指定源码包：
1
2
3
4
5
6
7
| dependencies {
......
examplesImplementation 'net.time4j:time4j-base:5.9.4'
......
}
|
编写对应的测试驱动类：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
| package mytests;
import gov.nasa.jpf.symbc.Debug;
import net.time4j.base.MathUtils;
public class TestTime4J {
public static void test(long num) {
MathUtils.safeCast(num);
Debug.printPC("PC ");
}
public static void main(String[] args) {
long num = 0;
test(num);
}
}
|
为了方便，把 gradle 下载的 time4j 的 jar 包复制到了项目目录下，并且在 jpf 配置文件中指明 classpath, sourcepath
1
2
3
4
5
6
7
8
9
10
11
12
13
| target=mytests.TestTime4J
classpath=${jpf-symbc}/build/examples:\
${jpf-symbc}/lib-to-be-tested/time4j-base-5.9.4.jar
sourcepath=${jpf-symbc}/src/examples:\
${jpf-symbc}/lib-to-be-tested/sources/time4j-base-5.9.4-sources.jar
symbolic.method = mytests.TestTime4J.test(sym)
symbolic.dp=z3
symbolic.optimizechoices=false
#symbolic.debug=true
listener = .symbc.SymbolicListener
|
输出如下：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
| symbolic.min_int=-2147483648
symbolic.min_long=-9223372036854775808
symbolic.min_short=-32768
symbolic.min_byte=-128
symbolic.min_char=0
symbolic.max_int=2147483647
symbolic.max_long=9223372036854775807
symbolic.max_short=32767
symbolic.max_byte=127
symbolic.max_char=65535
symbolic.min_double=4.9E-324
symbolic.max_double=1.7976931348623157E308
JavaPathfinder core system v8.0 (rev 052390b95ebe2bca062c31e6c1e52a6f13d68d5f) - (C) 2005-2014 United States Government. All rights reserved.
====================================================== system under test
mytests.TestTime4J.main()
====================================================== search started: 4/14/25, 5:49 PM
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
PC constraint # = 2
num_1_SYMINT < CONST_2147483647 &&
num_1_SYMINT < CONST_-2147483648
PC constraint # = 2
num_1_SYMINT < CONST_2147483647 &&
CONST_-2147483648 == num_1_SYMINT
PC constraint # = 2
num_1_SYMINT < CONST_2147483647 &&
num_1_SYMINT > CONST_-2147483648
PC constraint # = 2
CONST_2147483647 == num_1_SYMINT &&
num_1_SYMINT > CONST_-2147483648
PC constraint # = 2
num_1_SYMINT > CONST_2147483647 &&
num_1_SYMINT > CONST_-2147483648
====================================================== Method Summaries
Inputs: num_1_SYMINT
mytests.TestTime4J.test(-2147483649l) --> Return Value: --
mytests.TestTime4J.test(-2147483648l) --> Return Value: --
mytests.TestTime4J.test(0l) --> Return Value: --
mytests.TestTime4J.test(2147483647l) --> Return Value: --
mytests.TestTime4J.test(2147483648l) --> Return Value: --
====================================================== Method Summaries (HTML)
<h1>Test Cases Generated by Symbolic JavaPath Finder for mytests.TestTime4J.test (Path Coverage) </h1>
<table border=1>
<tr><td>num_1_SYMINT</td><td>RETURN</td></tr>
<tr><td>-2147483649</td><td>Return Value: --</td></tr>
<tr><td>-2147483648</td><td>Return Value: --</td></tr>
<tr><td>0</td><td>Return Value: --</td></tr>
<tr><td>2147483647</td><td>Return Value: --</td></tr>
<tr><td>2147483648</td><td>Return Value: --</td></tr>
</table>
====================================================== results
no errors detected
====================================================== statistics
elapsed time: 00:00:00
states: new=13,visited=0,backtracked=13,end=5
search: maxDepth=3,constraints=0
choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=4
heap: new=529,released=60,maxLive=489,gcCycles=6
instructions: 9313
max memory: 124MB
loaded code: classes=83,methods=1814
====================================================== search finished: 4/14/25, 5:49 PM
|
不过，为了方便，选择利用 gradle 来进行这个复制 jar 包的过程，在 build.gradle 中添加 task：
1
2
3
4
| task copyJars(type: Copy) {
from configurations.examplesImplementation
into "$buildDir/libs/jars"
}
|
不过，运行 task gradle spf-symbc:copyJars 之后报错：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
| FAILURE: Build failed with an exception.
* What went wrong:
Could not determine the dependencies of task ':jpf-symbc:copyJars'.
> Resolving dependency configuration 'examplesImplementation' is not allowed as it is defined as 'canBeResolved=false'.
Instead, a resolvable ('canBeResolved=true') dependency configuration that extends 'examplesImplementation' should be resolved.
* Try:
> Run with --stacktrace option to get the stack trace.
> Run with --info or --debug option to get more log output.
> Get more help at https://help.gradle.org.
Deprecated Gradle features were used in this build, making it incompatible with Gradle 9.0.
You can use '--warning-mode all' to show the individual deprecation warnings and determine if they come from your own scripts or plugins.
For more on this, please refer to https://docs.gradle.org/8.13/userguide/command_line_interface.html#sec:command_line_warnings in the Gradle documentation.
BUILD FAILED in 1s
|
需要创建一个可解析的配置并且继承 examplesImplementation, 在 build.gradle 中添加:
1
2
3
4
5
6
7
| configurations {
resolvableExamplesImplementation {
canBeResolved = true // 允许解析
canBeConsumed = false // 禁止被其他项目消费
extendsFrom examplesImplementation // 继承原配置
}
}
|
这样，运行 task gradle spf-symbc:copyJars 之后 gradle 就会自动将 jar 包复制到项目目录中的指定位置，不用再手动复制，在 jpf 配置文件中指定 jar 包位置等的时候会更加方便。