llvm2bpl report error when use smack generate boogie code

[Luweicai]

The source code which will trigger bug is following:

#include <stddef.h>
#include "string.h"
#include "smack.h"

void public_in(smack_value_t); // a wrapper funciton used for position

static void * (* const volatile memset_func)( void *, int, size_t ) = memset; // the position will trigger the bug

void mbedtls_platform_zeroize( void *buf, size_t len )  // the function that call the trigger function
{
    if( len > 0 )
        memset_func( buf, 0, len );
}


// entry-point function
void et(int tt)
{   
  public_in(__SMACK_value(tt));

  struct
  {
    int X[4];
    int Y[4];
   } t;
  mbedtls_platform_zeroize( &t, sizeof( t ) );
}

I use the latest smack in main branch. Build it from source code with auto ./build.sh. The OS system is Ubuntu 20.04
The run smack command is smack -t --warn silent --verifier=boogie --entry-points et --unroll 1 --loop-limit 1 -bpl tt.bpl 1.c
The bug report is

SMACK program verifier version 2.8.0
llvm2bpl: /usr/lib/llvm-12/include/llvm/IR/InstrTypes.h:1324: llvm::Value *llvm::CallBase::getArgOperand(unsigned int) const: Assertion `i < getNumArgOperands() && "Out of bounds!"' failed.
Stack dump without symbol names (ensure you have llvm-symbolizer in your PATH or set the environment var `LLVM_SYMBOLIZER_PATH` to point to it):
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamEi+0x31)[0x7facaacb5871]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7facaacb3972]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(+0xd26f82)[0x7facaacb5f82]
/lib/x86_64-linux-gnu/libc.so.6(+0x43090)[0x7faca9a5c090]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xcb)[0x7faca9a5c00b]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x12b)[0x7faca9a3b859]
/lib/x86_64-linux-gnu/libc.so.6(+0x22729)[0x7faca9a3b729]
/lib/x86_64-linux-gnu/libc.so.6(+0x33fd6)[0x7faca9a4cfd6]
llvm2bpl[0x444fa5]
llvm2bpl[0x438775]
llvm2bpl[0x49e20b]
llvm2bpl[0x425d67]
llvm2bpl[0x425356]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x3a8)[0x7facaade9af8]
llvm2bpl[0x421990]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7faca9a3d083]
llvm2bpl[0x42050e]
PLEASE submit a bug report to https://bugs.llvm.org/ and include the crash backtrace.
Stack dump:
0.      Program arguments: llvm2bpl /home/luwei/b-fns5cjhv.bc -bpl tt.bpl -warn-type silent -sea-dsa=ci -colored-warnings -source-loc-syms -entry-points et -mem-mod-impls -llvm-assumes=none
1.      Running pass 'SMACK generator pass' on module '/home/luwei/b-fns5cjhv.bc'.
Traceback (most recent call last):
  File "/usr/local/bin/smack", line 13, in <module>
    smack.top.main()
  File "/usr/local/bin/../share/smack/top.py", line 999, in main
    frontend(args)
  File "/usr/local/bin/../share/smack/top.py", line 709, in frontend
    return link_bc_files(bitcodes, libs, args)
  File "/usr/local/bin/../share/smack/frontend.py", line 496, in link_bc_files
    llvm_to_bpl(args)
  File "/usr/local/bin/../share/smack/top.py", line 765, in llvm_to_bpl
    try_command(cmd, console=True)
  File "/usr/local/bin/../share/smack/utils.py", line 92, in try_command
    raise Exception(output)
Exception: llvm2bpl: /usr/lib/llvm-12/include/llvm/IR/InstrTypes.h:1324: llvm::Value *llvm::CallBase::getArgOperand(unsigned int) const: Assertion `i < getNumArgOperands() && "Out of bounds!"' failed.
Stack dump without symbol names (ensure you have llvm-symbolizer in your PATH or set the environment var `LLVM_SYMBOLIZER_PATH` to point to it):
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamEi+0x31)[0x7facaacb5871]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7facaacb3972]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(+0xd26f82)[0x7facaacb5f82]
/lib/x86_64-linux-gnu/libc.so.6(+0x43090)[0x7faca9a5c090]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xcb)[0x7faca9a5c00b]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x12b)[0x7faca9a3b859]
/lib/x86_64-linux-gnu/libc.so.6(+0x22729)[0x7faca9a3b729]
/lib/x86_64-linux-gnu/libc.so.6(+0x33fd6)[0x7faca9a4cfd6]
llvm2bpl[0x444fa5]
llvm2bpl[0x438775]
llvm2bpl[0x49e20b]
llvm2bpl[0x425d67]
llvm2bpl[0x425356]
/lib/x86_64-linux-gnu/libLLVM-12.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x3a8)[0x7facaade9af8]
llvm2bpl[0x421990]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7faca9a3d083]
llvm2bpl[0x42050e]
PLEASE submit a bug report to https://bugs.llvm.org/ and include the crash backtrace.
Stack dump:
0.      Program arguments: llvm2bpl /home/luwei/b-fns5cjhv.bc -bpl tt.bpl -warn-type silent -sea-dsa=ci -colored-warnings -source-loc-syms -entry-points et -mem-mod-impls -llvm-assumes=none
1.      Running pass 'SMACK generator pass' on module '/home/luwei/b-fns5cjhv.bc'.

Some research of this bug is:
The smack will transfor the function mbedtls_platform_zeroize into:

; Function Attrs: noinline nounwind uwtable
define internal void @mbedtls_platform_zeroize(i8* %0, i64 %1) #0 !dbg !43 {
  call void @llvm.dbg.value(metadata i8* %0, metadata !46, metadata !DIExpression()), !dbg !47, !verifier.code !48
  call void @llvm.dbg.value(metadata i64 %1, metadata !49, metadata !DIExpression()), !dbg !47, !verifier.code !48
  %3 = icmp ugt i64 %1, 0, !dbg !50, !verifier.code !48
  br i1 %3, label %4, label %7, !dbg !52, !verifier.code !48

4:                                                ; preds = %2
  %5 = load volatile i8* (i8*, i32, i64)*, i8* (i8*, i32, i64)** @memset_func, align 8, !dbg !53, !verifier.code !48
  %6 = call i8* @devirtbounce(i8* (i8*, i32, i64)* %5, i8* %0, i32 0, i64 %1)
  br label %7, !dbg !53, !verifier.code !48

7:                                                ; preds = %4, %2
  ret void, !dbg !54, !verifier.code !48
}

define internal i8* @devirtbounce(i8* (i8*, i32, i64)* %funcPtr, i8* %arg, i32 %arg1, i64 %arg2) {
entry:
  %0 = bitcast i8* (i8*, i32, i64)* %funcPtr to i8*
  br label %test.__SMACK_value

memset:                                           ; preds = %test.memset
  %1 = call i8* @memset(i8* %arg, i32 %arg1, i64 %arg2)
  ret i8* %1

__SMACK_value:                                    ; preds = %test.__SMACK_value
  %2 = call %struct.smack_value* (...) @__SMACK_value()
  ret %struct.smack_value* %2

fail:                                             ; preds = %test.memset
  unreachable

test.memset:                                      ; preds = %test.__SMACK_value
  %sc = icmp eq i8* bitcast (i8* (i8*, i32, i64)* @memset to i8*), %0
  br i1 %sc, label %memset, label %fail

test.__SMACK_value:                               ; preds = %entry
  %sc3 = icmp eq i8* bitcast (%struct.smack_value* (...)* @__SMACK_value to i8*), %0
  br i1 %sc3, label %__SMACK_value, label %test.memset
}

While in the function devirtbounce, the instruction %2 = call %struct.smack_value* (...) @__SMACK_value() will trigger the assert(CI.getNumArgOperands() > 0 && "Expected at least one argument."); error in the smack source code SmackRep.cpp.

[alexthomasv]

Did you ever figure this issue out?

[shaobo-he]

Unfortunately, all SMACK developers currently do not have time to work on it anymore. If this issue persists on the latest version of SMACK, then it's not sorted out.