Repository navigation
llvm2bpl report error when use smack generate boogie code #792
Description
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.
Activity
alexthomasv commentedon Feb 6, 2025
Did you ever figure this issue out?
shaobo-he commentedon Feb 23, 2025
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.
shaobo-he commentedon Jul 6, 2026
I reproduced this on the current local LLVM 14 build: the reduced example still crashes in
llvm2bplwhile generating Boogie.My current diagnosis is that this is caused by the devirtualization pass treating
__SMACK_value(...)as a possible target of the indirectmemset_funccall. Since__SMACK_valueis variadic with no fixed parameters and returns a pointer-like value, the existing target compatibility check is too permissive: it can match a non-variadic indirect call likevoid *(void *, int, size_t)and then build adevirtbouncebranch that directly calls__SMACK_value()with zero arguments. Later, SMACK special handling for__SMACK_valueasserts because it expects at least one annotation argument.A tempting broad fix is to reject variadic targets for non-variadic indirect call sites. However, that may be too strong if we want SMACK/LLVM IR handling to tolerate non-portable function-pointer casts or ABI-level dispatch patterns, even if many such calls are undefined at the C level when the called function type is incompatible.
So I think the more conservative fix is:
__SMACK_valueas non-real call targets for devirtualization.memset_funcshould includememset, but should not include a__SMACK_valuetarget branch.Would this direction be acceptable? If so, I can prepare a small PR with that targeted devirt filtering and the regression test.