无法为 Java 使用 JBMC（有界模型检查器）命令

Posted 2023-03-31

【中文标题】无法为 Java 使用 JBMC（有界模型检查器）命令

【英文标题】：Unable to use JBMC (Bounded Model Checker) Commands for Java

【发布时间】：2019-11-02 05:55:30

【问题描述】：

我是JBMC(Bounded Model Checker) 的新手。我们需要找出在不运行Java程序的情况下可能发生在Java程序中的RunTime Exception的可能性。我们搜索了一些抽象的解释框架，发现 JBMC 在这种情况下会有所帮助。

例如：

public class SampleClass 

    public static void main(String[] args) 
     
        int ar[] = 1, 2, 3, 4, 5; 
        for (int i=0; i<=ar.length; i++) 
          System.out.println(ar[i]); 
     

在上面的程序中，当循环在第 6 次迭代中运行时，我们将得到 ArrayIndexOutOfBoundException。但是如何使用 JBMC 来预测呢？我们在 JBMC 中找到了提供Command line options 详细信息的命令表，但我们无法找到命令组合以及如何使用它。 JBMC 是否有可用的 Java API 或文档？

请推荐！！。

【参考方案1】：

与 CBMC 不同，JBMC 不支持here 列出的所有选项。 您可以通过运行jbmc --help 注意到这一点。如果你运行jbmc <class> --bounds-check 之类的东西，你会得到一个“使用错误”。

关于您的 java 类：jbmc 适用于 .jar 或 .class。 尝试先生成一个 .class，如下所示：

javac SampleClass.java

然后在SampleClass.class 上运行 jbmc，如下所示：

jbmc SampleClass.class --unwind N（尝试用不同的N值变得更有信心）

低于 N=6 的结果：

JBMC version 5.12 (cbmc-5.11-3477-gcd70727ed) 64-bit x86_64 linux
Parsing SampleClass.class

...

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
SampleClass.java function java::SampleClass.main:([Ljava/lang/String;)V
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.5] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.2] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.3] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.3] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.3] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.4] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.4] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.4] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.5] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.1] line 4 no uncaught exception: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.5] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-create-negative-size.1] line 4 Array size should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 4 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.1] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.1] line 4 Array index should be < length: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.2] line 4 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.6] line 5 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.7] line 6 Null pointer check: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-low.6] line 6 Array index should be >= 0: SUCCESS
[java::SampleClass.main:([Ljava/lang/String;)V.array-index-out-of-bounds-high.6] line 6 Array index should be < length: FAILURE
[java::SampleClass.main:([Ljava/lang/String;)V.null-pointer-exception.8] line 6 Null pointer check: SUCCESS

** 1 of 31 failed (2 iterations)
VERIFICATION FAILED

我希望这会有所帮助。 我也是jbmc的新手。我过去使用过 cbmc，可以找到更多文档 here 和 here，但很少有文档可用于 jbmc。

【讨论】：

谢谢 dall .. 我们找到了用户手册 (github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/…)。其中提供了有关 JBMC 的更多信息。

谢谢。我看了看，对我真的很有用。