jpf-symbc 踩坑记录

发表于 分类于 阅读次数： 本文字数： 890 阅读时长 ≈ 3 分钟

JPF

Analysis system for Java

Developed by NASA

jpf 可以用来:

  • software model checking (deadlock & race detection)
  • deep inspection (numeric analysis, invalid access)
  • test case generation (symbolic execution)

组件

Java 字节码解释器(虚拟机)

Listeners: To print results of symbolic analysis (path conditions, test vectors or test sequences); to influence the search

相关资源

安装和配置

安装配置文档竟在作者的 notion 笔记里面…

下面讲一下笔者的踩坑经验

  1. 克隆项目

jpf-core 和 jpf-symbc 放在同一个目录下面

jpf-core 要用这个版本 -> https://github.com/yannicnoller/jpf-core

1
2
3
.
├── jpf-core
└── jpf-symbc
  1. 编译项目

jpf-symbc 只支持 Java 8

切换到 Java 8

1
2
$ jabba install temulin@8
$ jabba use temulin@8

jpf-core 用 ant 编译

1
2
3
4
5
# in jpf-core
ant build

# (Optional) test
JUNIT_HOME=/usr/share/maven-repo/junit/junit/4.13.2/ ant test

jpf-symbc 用 ant 编译

1
2
3
4
5
# in jpf-symbc
ant build

# (Optional) test
JUNIT_HOME=/usr/share/maven-repo/junit/junit/4.13.2/ ant test
  1. 配置 ~/.jpf/site.properties

里面填写如下内容

1
2
3
jpf-core = ${user.home}/src/javapathfinder/jpf-core
jpf-symbc = ${user.home}/src/javapathfinder/jpf-symbc
extensions = ${jpf-core},${jpf-symbc}

其中对应修改两个项目的路径

  1. 测试下能否正常使用
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
# in jpf-symbc
$ java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar src/examples/demo/NumericExample.jpf
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 - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
demo.NumericExample.main()

====================================================== search started: 23-12-29 下午2:55
>0
<=0
Property Violated: PC is constraint # = 1
((a_1_SYMINT[15] + b_2_SYMINT[-13]) - 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(-50,17)  --> Return Value: --
demo.NumericExample.test(0,0)  --> Return Value: --
demo.NumericExample.test(15,-13)  --> "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>-50</td><td>17</td><td>Return Value: --</td></tr>
<tr><td>0</td><td>0</td><td>Return Value: --</td></tr>
<tr><td>15</td><td>-13</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=5,visited=0,backtracked=5,end=2
search:             maxDepth=3,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=2
heap:               new=371,released=20,maxLive=349,gcCycles=3
instructions:       3246
max memory:         709MB
loaded code:        classes=64,methods=1325

====================================================== search finished: 23-12-29 下午2:55

jpf-symbc 使用

对于每个要进行符号执行的程序, 需要编写一个 .jpf 文件, 然后调用 RunJPF.jar:

1
2
# in jpf-symbc
$ java -Xmx1024m -ea -jar ../jpf-core/build/RunJPF.jar src/examples/demo/NumericExample.jpf

#.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
66
; 测试的application类
target=x.y.TreeMapSimple

target.args=arg1,arg2

classpath=${jpf-symbc}/build/examples  ; path to your class example
sourcepath=${jpf-symbc}/build/examples  ; path to the source of your example

; 注册到jpf-core的listener
; 控制接下来做什么
; gov.nasa.jpf.listener.PreciseRaceDetector  竞争情况检查
; gov.nasa.jpf.listener.CoverageAnalyzer   分析覆盖率
; gov.nasa.jpf.listener.DeadlockAnalyzer   分析代码死锁
; gov.nasa.jpf.listener.MethodAnalyzer
; gov.nasa.jpf.symbc.SymbolicListener   输出 PC 和 JUnit test
; gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener  输出 JUnit test
; gov.nasa.jpf.symbc.GreenListener
listener=gov.nasa.jpf.symbc.SymbolicListener,gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener,gov.nasa.jpf.listener.PreciseRaceDetector,gov.nasa.jpf.listener.CoverageAnalyzer

; specify some search limit
search.depth_limit=15

;
coverage.include=dataflow.Billing
coverage.show_requirements=true

; 遇到exception的时候打印stack trace
; 和 PreciseRaceDetector 一起使用
; error trace snapshot
report.console.property_violation=error,trace

; 对于 random.nextInt 枚举随机数
cg.enumerate_random=true

; 和 MethodAnalyzer 一起使用
method.include=*Robot*


; 测试的目标方法, 多个函数用逗号分隔
; 函数参数用 (sym) 表示, 多个参数用 # 分隔
; 例如: triangle.Triangle.getType(sym#sym#sym)
symbolic.method=TreeMapSimple.containsKey(sym),TreeMapSimple.put(sym),TreeMapSimple.remove(sym)

; specify the decision procedure to use
; z3, z3inc, z3bitvector, z3bitvectorinc
; cvc3, cvc3bitvec, choco, iasolver
symbolic.dp=z3bitvector
symbolic.bvlength=64

; 各种类型的范围
symbolic.min_int=-100
symbolic.max_int=100
symbolic.min_double=-100.0
symbolic.max_double=100.0

; print some debug information
symbolic.debug=true

; handling symbolic arrays
symbolic.lazy=on
symbolic.arrays=true

; specify string analysis
symbolic.strings=true
symbolic.string_dp=ABC  ; or z3str
symbolic.string_dp_timeout_ms=3000

jpf 源码分析