JBMC with Kotlin.

[jkbbwr]

Upfront want to say, I know its not the standard usecase but it seems that JBMC works great out the box with kotlin for most situations.

This is awesome thank you guys!

I did however find a strange behaviour.

When running this code via JBMC

package dev.kibb.kfx

fun main() {
    val s: String? = null
    s!!
}

When executed via the JVM normally it results in

Exception in thread "main" java.lang.NullPointerException
        at dev.kibb.kfx.MainKt.main(main.kt:5)
        at dev.kibb.kfx.MainKt.main(main.kt)

When executed via JBMC it seems to infinitely unroll some internal stacktrace function.

Summary Details:

CBMC version: 5.48.0 (cbmc-5.48.0-19-g9f9ee0788)
Operating system: Arch Linux - Linux devroot 5.15.12-arch1-1 #1 SMP PREEMPT Wed, 29 Dec 2021 12:04:56 +0000 x86_64 GNU/Linux
Exact command line resulting in the issue: ~/tmp/cbmc/build/bin/jbmc -jar build/libs/kfx-1.0-SNAPSHOT-all.jar --java-assume-inputs-non-null --trace
What behaviour did you expect: Verification to fail with a null pointer failure state.
What happened instead: Seems to be an infinite unwind in internal code.

Unwinding loop java::kotlin.jvm.internal.Intrinsics.sanitizeStackTrace:(Ljava/lang/Throwable;Ljava/lang/String;)Ljava/lang/Throwable;.0 iteration 692 file kotlin/jvm/internal/Intrinsics.java line 259 function java::kotlin.jvm.internal.Intrinsics.sanitizeStackTrace:(Ljava/lang/Throwable;Ljava/lang/String;)Ljava/lang/Throwable; bytecode-index 23 thread 0

[jkbbwr]

If a max unwind is set it does reach a conclusion but fails in the wrong location.

Violated property:
  file kotlin/jvm/internal/Intrinsics.java function kotlin.jvm.internal.Intrinsics.sanitizeStackTrace(java.lang.Throwable, java.lang.String) line 265 thread 0
  Dynamic cast check
  return_tmp3 != null && return_tmp3->@java.lang.Object.@class_identifier == "java::array[reference]" && ((struct java::array[reference] *)return_tmp3)->@array_dimensions == 1 && ((struct java::array[reference] *)return_tmp3)->@element_class_identifier == "java::java.lang.StackTraceElement"

[jkbbwr]

The sanitize stacktrace method called in the kotlin runtime is this

static <T extends Throwable> T sanitizeStackTrace(T throwable, String classNameToDrop) {
    StackTraceElement[] stackTrace = throwable.getStackTrace();
    int size = stackTrace.length;

    int lastIntrinsic = -1;
    for (int i = 0; i < size; i++) {
        if (classNameToDrop.equals(stackTrace[i].getClassName())) {
            lastIntrinsic = i;
        }
    }

    StackTraceElement[] newStackTrace = Arrays.copyOfRange(stackTrace, lastIntrinsic + 1, size);
    throwable.setStackTrace(newStackTrace);
    return throwable;
}

https://github.com/JetBrains/kotlin/blob/master/libraries/stdlib/jvm/runtime/kotlin/jvm/internal/Intrinsics.java#L265

[peterschrammel]

@jkbbwr, JBMC has several options to control how to deal with exceptions.
It treats explicitly thrown exceptions differently from runtime exceptions. That's admittedly quite confusing, and primarily has performance reasons.
By default, it just asserts on runtime exceptions at the place where they are thrown, whereas explicitly thrown exceptions are propagated as you'd expect and JBMC asserts that there is no uncaught exception, i.e. exception that escapes the entry point method. To make runtime exceptions propagate, use --throw-runtime-exceptions.

Further options are:

 --disable-uncaught-exception-check
                              ignore uncaught exceptions and errors
 --throw-assertion-error      throw java.lang.AssertionError on violated
                              assert statements instead of failing
                              at the location of the assert statement
 --throw-runtime-exceptions   make implicit runtime exceptions explicit
 --assert-no-exceptions-thrown
                              transform `throw` instructions into `assert FALSE`
                              followed by `assume FALSE`.

[jkbbwr]

Ill give that a go shortly, on a very different note, I tried throwing Kotlin Coroutines at it to see what would happen, and it failed (as expected)

Trying to load Java main class: dev.kibb.kfx.MainKt
Found Java main class: dev.kibb.kfx.MainKt
Converting
stub class symbol java::java.lang.Object already exists
--- begin invariant violation report ---
Invariant check failed
File: /home/jakob/tmp/cbmc/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp:462 function: create_parameter_names
Condition: variables[param_index].size() <= 1
Reason: should have at most one entry per index
Backtrace:
/home/jakob/tmp/cbmc/build/bin/jbmc(print_backtrace(std::ostream&)+0x4c) [0x56001f2520bc]
/home/jakob/tmp/cbmc/build/bin/jbmc(get_backtrace[abi:cxx11]()+0x165) [0x56001f252d45]
/home/jakob/tmp/cbmc/build/bin/jbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::typeinvariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>,std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x40)[0x56001ebd8530]
/home/jakob/tmp/cbmc/build/bin/jbmc(create_parameter_names(java_bytecode_parse_treet::methodt const&, dstringt const&, std::vector<code_typet::parametert, std::allocator<code_typet::parametert> >&, unsigned short const&)+0x12ce) [0x56001edf5b0e]
/home/jakob/tmp/cbmc/build/bin/jbmc(java_bytecode_convert_method_lazy(symbolt&, dstringt const&, java_bytecode_parse_treet::methodt const&, symbol_tablet&, message_handlert&)+0x4ac) [0x56001edf615c]
/home/jakob/tmp/cbmc/build/bin/jbmc(java_bytecode_convert_classt::convert(java_bytecode_parse_treet::classt const&, std::__cxx11::list<std::reference_wrapper<java_bytecode_parse_treet::classt const>, std::allocator<std::reference_wrapper<java_bytecode_parse_treet::classt const> > > const&)+0x207b) [0x56001ede849b]
/home/jakob/tmp/cbmc/build/bin/jbmc(java_bytecode_convert_classt::operator()(std::__cxx11::list<java_bytecode_parse_treet, std::allocator<java_bytecode_parse_treet> > const&)+0x153) [0x56001edee393]
/home/jakob/tmp/cbmc/build/bin/jbmc(java_bytecode_convert_class(std::__cxx11::list<java_bytecode_parse_treet, std::allocator<java_bytecode_parse_treet> > const&, symbol_tablet&, message_handlert&, unsigned long, method_bytecodet&, java_string_library_preprocesst&, std::unordered_set<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::hash<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::equal_to<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&)+0x36b) [0x56001ede902b]
/home/jakob/tmp/cbmc/build/bin/jbmc(java_bytecode_languaget::typecheck(symbol_tablet&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x20c) [0x56001ed0a1ac]
/home/jakob/tmp/cbmc/build/bin/jbmc(language_filest::typecheck(symbol_tablet&, bool)+0x71d) [0x56001f20686d]
/home/jakob/tmp/cbmc/build/bin/jbmc(lazy_goto_modelt::initialize(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, optionst const&)+0x664) [0x56001ed8e3c4]
/home/jakob/tmp/cbmc/build/bin/jbmc(jbmc_parse_optionst::get_goto_program(std::unique_ptr<abstract_goto_modelt, std::default_delete<abstract_goto_modelt> >&, optionst const&)+0x2ff) [0x56001ebdda9f]
/home/jakob/tmp/cbmc/build/bin/jbmc(jbmc_parse_optionst::doit()+0x733) [0x56001ebde8f3]
/home/jakob/tmp/cbmc/build/bin/jbmc(parse_options_baset::main()+0x8b) [0x56001ebd66fb]
/home/jakob/tmp/cbmc/build/bin/jbmc(main+0x35) [0x56001ebc9675]
/usr/lib/libc.so.6(__libc_start_main+0xd5) [0x7f45d7ed3b25]
/home/jakob/tmp/cbmc/build/bin/jbmc(_start+0x2e) [0x56001ebd7dee]

package dev.kibb.kfx

import kotlinx.coroutines.delay
import kotlinx.coroutines.runBlocking
import kotlin.time.Duration

suspend fun test() {
    delay(Duration.parse("10s"))
    println("Test done.")
    assert(1 == 2)
}


fun main() {
    runBlocking {
        test()
    }
}

I know its very out of scope for the JBMC group, but it was a passing curiosity.

[peterschrammel]

Thanks, @jkbbwr. It's certainly interesting to understand what is missing to provide Kotlin support.

[jkbbwr]

This isn't required for traditional kotlin support just for how kotlin coroutines work, they take the code and transform it into a re-entrant state machine at the bytecode level. Im super impressed with what it is already able to handle out of the box! 👍

[jkbbwr]

Also, in regards to the --throw-runtime-exceptions that triggers the unroll that I commented on earlier that fails with the violated property when given upper bounds

[JonasKlamroth]

I have a question regarding the --throw-runtime-exceptions option. As i understand it this option when provided treats runtime-exceptions as in a normal program flow java would do. However when testing this hypothesis it turns out that exceptions are still being treated as "unhandled" even if thats not the case. Consider the following minimal example:

public static void main(String args[]) {
    Object o = null;
    try {
      o.toString();
    } catch (RuntimeException e) {

    }
  }

JBMC detects an uncaught exception. Similarly with IndexOutOfBounds Exceptions. The only time i got an expected result was when catching NullPointerExceptions directly (instead of RuntimeException) but this doesnt work for IndexOutOfBounds exceptions. Is this the expected behavior and if so is there any way to avoid this?

run on JBMC version 5.64 on ubuntu 20.04