RV-Match now supports inline assembly

Posted on September 19, 2017 by Dwight Guth

Posted in K, News, RV-Match

RV-Match now supports execution of applications containing x86_64 inline assembly. If you have a program that contains inline assembly, you can compile it with kcc like any other C program and we will compile the functions containing inline assembly with gcc and execute them directly the same way we handle any other native code which we do not have C source for. As a result of this, the ability to detect undefined behavior in that function is eliminated, but it allows you to analyze complex applications which contain some code in inline assembly which you do not want to translate into C source.

As an example, consider the following Hello World program written using inline assembly:

#include <string.h>
#include <limits.h>

char* str = "Hello World!\n";

void hello(void) {
        char *s = str;
        long len = strlen(str);
        int ret = 0;

        __asm__("movq $1, %%rax \n\t"
                "movq $1, %%rdi \n\t"
                "movq %1, %%rsi \n\t"
                "movl %2, %%edx \n\t"
                : "=g"(ret)
                : "g"(s), "g" (len));


int main() {
  int x = INT_MAX;

When we compile and run this program with kcc, we get the following output:

Hello World!
 Signed integer overflow.
   at main(test.c:24:3)
  Undefined behavior (UB-CCV1).
   see C11 section 6.5:5 <a href="http://rvdoc.org/C11/6.5">http://rvdoc.org/C11/6.5</a>
   see C11 section J.2:1 item 36 <a href="http://rvdoc.org/C11/J.2">http://rvdoc.org/C11/J.2</a>
   see CERT-C section INT32-C <a href="http://rvdoc.org/CERT-C/INT32-C">http://rvdoc.org/CERT-C/INT32-C</a>

As you can see, we correctly print the Hello World string using the inline assembly, while also being capable of detecting the integer overflow in the main function.

Good luck hunting bugs with this new RV-Match feature!

company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog