Невозможно использовать команды JBMC (Bounded Model Checker) для Java

Question

Я новичок в JBMC(ограниченная модель проверки). У нас есть требование выяснить возможности исключения RunTime, которое может возникнуть в Java-программе, без ее запуска. Мы искали некоторые абстрактные рамки интерпретации и обнаружили, что 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]); 
    } 

}

В приведенной выше программе мы получим ArrayIndexOutOfBoundException, когда цикл будет выполняться во время 6-й итерации. Но как предсказать это, используя JBMC? Мы нашли лист команд, который предоставляет подробную информацию о параметрах командной строки в JBMC, но мы не смогли найти комбинации команд и способы их использования. Есть ли какой-нибудь Java API или Документы, доступные для JBMC?

Пожалуйста, предложите!

Answer 1

В отличие от CBMC, JBMC не поддерживает все опции, перечисленные здесь. Вы можете заметить это, запустив jbmc --help, Если вы запускаете что-то вроде jbmc <class> --bounds-check вы получите "ошибку использования".

О вашем классе Java: JBMC работает на .jar или .class. Попробуйте сначала сгенерировать.class следующим образом:

javac SampleClass.java

затем запустите JBMC на SampleClass.class следующее:

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 в прошлом, и дополнительную документацию можно найти здесь и здесь, но очень мало документации доступно для jbmc.