questions on translate LLVM language 'store <4 x i32>' to bpl

[muyaview]

take below simple C codes for example:

#include "smack.h"
#include <stdlib.h>

int g_val[10];
void init()
{
    g_val[0] = 0;
    g_val[1] = 1;
    g_val[2] = 2;
    g_val[3] = 3;
    
    __SMACK_code("call {:cexpr \"g_val[1] at place 1()\"} boogie_si_record_i32(@);", g_val[1]);
    return ;
}

int main()
{
    init();
    __SMACK_code("call {:cexpr \"g_val[1] at place 2()\"} boogie_si_record_i32(@);", g_val[1]);

    g_val[10] = 0; //make a buffer overflow, in order to print out the traces
    return 0;
}

Verify the codes using below cmd:

smack --clang-options="-g -O2" --memory-safety --entry-points main -bpl test.bpl -ll test.ll test.c

With the optimization option 'O2', the assignments of g_val[0] to g_val[3] are translated to LLVM language by clang as below:

store <4 x i32> <i32 0, i32 1, i32 2, i32 3>, <4 x i32>* bitcast ([10 x i32]* @g_val to <4 x i32>*), align 4, !dbg !40, !tbaa !43, !verifier.code !47

In the next step, the LLVM statements are translated to boogie codes as bit vector statements. See below:

$M.0 := $store.vec.4xi32.i8($M.0, g_val, mk.vec.4xi32(0, 1, 2, 3));

Seems $store.vec.4xi32.i8 is handled incorrect in normal model(without --bit-precise). The results of this verification is:

    /usr/local/share/smack/lib/smack.c(1421,3): Trace: Thread=1  ()
    /usr/local/share/smack/lib/smack.c(1424,3): Trace: Thread=1  ()
    /usr/local/share/smack/lib/smack.c(1426,1): Trace: Thread=1  ()
    test.c(7,14): Trace: Thread=1  (RETURN from __SMACK_init_func_memory_model , RETURN from $initialize )
    test.c(7,14): Trace: Thread=1  ()
    test.c(7,14): Trace: Thread=1  (smack:entry:main = -12437)
    test.c(7,14): Trace: Thread=1  ()
    test.c(7,14): Trace: Thread=1  (CALL __SMACK_check_memory_safety)
    test.c(7,14): Trace: Thread=1  (RETURN from __SMACK_check_memory_safety )
    test.c(7,14): Trace: Thread=1  ()
    test.c(12,5): Trace: Thread=1  ()
    test.c(12,5): Trace: Thread=1  (g_val[1] at place 1() = 1)
    test.c(12,5): Trace: Thread=1  ()
    test.c(12,5): Trace: Thread=1  (CALL __SMACK_check_memory_safety)
    test.c(12,5): Trace: Thread=1  (RETURN from __SMACK_check_memory_safety )
    test.c(19,86): Trace: Thread=1  ()
    test.c(19,5): Trace: Thread=1  ()
    test.c(19,5): Trace: Thread=1  (g_val[1] at place 2() = 17)
    test.c(19,5): Trace: Thread=1  ()
    test.c(19,5): Trace: Thread=1  (CALL __SMACK_check_memory_safety)
    test.c(19,5): Trace: Thread=1  (ASSERTION FAILS assert {:valid_deref} $Alloc[$base(p)];
    test.c(19,5): Trace: Thread=1  (Done)

Value of g_val[1] in place 2 was changed to 17 unreasonable. However if the parameter --bit-precise is added , the results could be as expected. So I think if $store.vec.4xi32.i8 can't be handled in normal model, if it is possible to print a warning? Or can we fix this issue?

[shaobo-he]

Hello @muyaview,

It appears the spurious counterexample is not a result of the --bit-precise flag. The real reason is that SMACK models the operation store.vec.4xbv32.bv8 using unintepreted functions. So, I'm curious about why you mentioned the results could be as expected if the --bit-precise flag is enabled.

That being said, we should definitely warn the users of this unsoundness. I'll push a fix soon. In the meanwhile, I doubt if a type-safe memory access of vector variables works fine. @michael-emmi, am I right?

Shaobo

[muyaview]

Hi @shaobo-he ,

Thanks for your clarification. Apart from warning this unsoundness, if it is possible to fix this to handle the operation correctly?

[shaobo-he]

Hi @shaobo-he ,

Thanks for your clarification. Apart from warning this unsoundness, if it is possible to fix this to handle the operation correctly?

I'm not sure. @michael-emmi implemented this bit so he probably has the definite answer for your question.

[zvonimir]

@shaobo-he : Why are you saying "unsoundness"? We are over-approximating here, and hence this can only be incompleteness, meaning SMACK might report spurious bugs but not miss bugs. Yes?

@muyaview : Any particular reason you are trying to verify programs under -O2 optimization level? Typically we always use -O0 with SMACK since in the case the generated LLVM IR code is more amenable to verification.

[muyaview]

Hi @zvonimir , The codes we are verifying are compiled with -O2 level and ran in production. I want to keep the llvm bitcodes and bpl codes which I verified identical with production totally. So I put them under -O2 level.