java pathfinder + symbc 踩坑记

安装

jpf-core: https://github.com/javapathfinder/jpf-core

jpf-symbc: https://github.com/SymbolicPathFinder/jpf-symbc

我改了一下中间不能跑的intellij代码，也上传了idea的相关配置，路径需要根据自己的机器环境进行配置

https://github.com/w93163red/jpf-core

https://github.com/w93163red/jpf-symbc

记录一下配置java pathfinder 和 symbolic javapathfinder的过程。

jpf 是基于gradle的，symbolic 基于ant + eclipse。

但是我不用eclipse，所以记录一下配置过程，省的之后重新配的时候又重新踩坑。

配置环境: Windows 11 22H2 + WSL2 Ubuntu 22.04

剩下的步骤全部在linux下执行。

  1. 验证下java 版本，官方说明只支持java 1.8.

    1
    java -version

  2. 在$HOME 路径下创建.jpf， 并且配置上site.properties, 指明jpf-core 和 jpf-symbc 的路径

    1
    2
    3
    4
    # cat ~/.jpf/site.properties
    jpf-core = /home/ling/code/pathfinder/jpf-core
    jpf-symbc = /home/ling/code/pathfinder/jpf-symbc
    extensions = ${jpf-core},${jpf-symbc}

  3. 因为symb-c 依赖于jpf 编译后的产物，产物路径在jpf-core/build下

    1
    2
    cd jpf-core
    gradle build

    路径

  4. 然后intellij import jpf-symbc，在import成功过后，import jpf-core as modules
    https://www.jetbrains.com/help/idea/import-project-from-eclipse-page-1.html#import-project

intellij 导入项目

最后项目结构应该长这样：
项目结构

  1. 对于jpf-symbc 的project structure 配置成如下这样

jpf-core 配置截图1

jpf-core 配置截图2

jpf-symbc 配置截图1

jpf lib 配置截图

  1. 在jpf-symbc下项目路径下ant build 出jar包，然后在RunJPF 下跑这个项目

实际运行

坑还是很多的。需要一个一个修，symbc自己提供的example都跑不了……我吐了。

运行配置

在运行配置时，需要按照上图先跑ant build，把symbc build之后再运行jpf-core里面的main函数。

大概流程是：symbc会把自己的listener注册到jpf-core当中，jpf-core在跑到一些stage时候，会notify listener，发送对应的时间让各listener去做相应的处理，然后再返回回来。

w