AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

Is this a false positive? #1042

Closed Ryuanxue closed 1 month ago

Ryuanxue commented 1 month ago

I am trying to use alive-tv. My src file and their IR are as follow:

int main(){
    int a=4;
  int  b=3;
  a=a+b;
}

define dso_local i32 @main() #0 !dbg !7 {
entry:
  %a = alloca i32, align 4
  %b = alloca i32, align 4
  store i32 4, i32* %a, align 4, !dbg !12
  store i32 3, i32* %b, align 4, !dbg !14
  %0 = load i32, i32* %a, align 4, !dbg !15
  %1 = load i32, i32* %b, align 4, !dbg !16
  %add = add nsw i32 %0, %1, !dbg !17
  store i32 %add, i32* %a, align 4, !dbg !18
  ret i32 0, !dbg !19
}

My tgt file and their IR are as fllow:

inline __attribute__((always_inline)) int main_sub(int *a,int *b)
{
return *a+b;
}
int main(){
    int a=4;
  int  b=3;
  a=main_sub(&a,&b);
}

define dso_local i32 @main() #0 !dbg !7 {
entry:
  %a.addr.i = alloca i32*, align 8
  %b.addr.i = alloca i32*, align 8
  %a = alloca i32, align 4
  %b = alloca i32, align 4
  store i32 4, i32* %a, align 4, !dbg !21
  store i32 3, i32* %b, align 4, !dbg !23
  store i32* %a, i32** %a.addr.i, align 8
  store i32* %b, i32** %b.addr.i, align 8
  %0 = load i32*, i32** %a.addr.i, align 8, !dbg !24
  %1 = load i32, i32* %0, align 4, !dbg !25
  %2 = load i32*, i32** %b.addr.i, align 8, !dbg !26
  %idx.ext.i = sext i32 %1 to i64, !dbg !27
  %add.ptr.i = getelementptr inbounds i32, i32* %2, i64 %idx.ext.i, !dbg !27
  %3 = ptrtoint i32* %add.ptr.i to i32, !dbg !25
  store i32 %3, i32* %a, align 4, !dbg !28
  ret i32 0, !dbg !29
}

I used the command alive-tv src.ll tgt.ll for verification, and the result was correct. However, I believe the result should be incorrect because the return a + b in the tgt.c file uses an address value. It should be changed to return a + *b to be correct. Is this a false positive?

nunoplopes commented 1 month ago

The result of the addition is not observable, so there's nothing to verify. In both cases, main() returns 0 and has no further side effects. You need to, e.g., print the value or call some external function.