Abstract Execution Fails to Trace Correct Allocation Size

[rycbar77]

'zext' Instruction

Abstract execution fails to trace the correct allocation size when encountering instructions like "zext". This leads to incorrect buffer size calculations, resulting in false alerts of buffer overflow.

Sample Code:

#include <string.h>
#include <stdio.h>
#include <stdlib.h>

int main() {
    unsigned char size = 255;
    char *p;
    p = (char *)malloc(size + 1);
    p[251] = 0;
    free(p);
}

Here is the compiled llvm ir.

define dso_local i32 @main() #0 {
entry:
  %conv = zext i8 -1 to i32
  %add = add nsw i32 %conv, 1
  %conv1 = sext i32 %add to i64
  %call = call noalias i8* @malloc(i64 noundef %conv1) #3
  %arrayidx = getelementptr inbounds i8, i8* %call, i64 251
  store i8 0, i8* %arrayidx, align 1
  call void @free(i8* noundef %call) #4
  ret i32 0
}

The expected allocation size should be 256, but the output says it's 0. This should not be a buffer overflow case.

Buffer overflow!! Accessing buffer range: [251, 251]
Allocated buffer size: 0
Position:    %arrayidx = getelementptr inbounds i8, i8* %call, i64 251 
The following is the value flow. [[
IntraICFGNode7 {fun: main}
GepStmt: [Var110 <-- Var106]
   %arrayidx = getelementptr inbounds i8, i8* %call, i64 251 , Offset: [251, 251]
]].
Alloc Site: AddrStmt: [Var106 <-- Var107]
   %call = call noalias i8* @malloc(i64 noundef %conv1) #3 

Branch Condition

I was wondering if abstract execution might be able to address this case and how. I'm doing some test like the code below, the allocation size depends on a. The output says there's no overflow here. Is it possible to trace both data flow and warn the overflow one and the condtions like a==0?

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

int main() {
  unsigned char size = 10;
  unsigned int a;
  scanf("%d", &a);
  char *p;

  if (a == 0) {
    p = (char *)malloc(size + 1);
  } else {
    p = (char *)malloc(size + 5);
  }

  p[13] = 0;
  free(p);
}

[yuleisui]

The first case looks to be an integer overflow. The maximum value of unsigned char is 255, plus one will be an undefined value hence reporting an overflow warning.

The second one depends on your algorithm. A path-sensitive AE could be something you want.

[rycbar77]

Thanks for your response. I think the first case is not integer overflow since the param of malloc has a type of i64. So the program
first do zext to extend i8 to i32, plus 1 to an i32 integer 255 won't cause overflow. To test it, i compile this program and debug it to see the actual memory layout.

0x60a8933e1290: 0x0000000000000000      0x0000000000000111
0x60a8933e12a0: 0x0000000000000000      0x0000000000000000
0x60a8933e12b0: 0x0000000000000000      0x0000000000000000
0x60a8933e12c0: 0x0000000000000000      0x0000000000000000
0x60a8933e12d0: 0x0000000000000000      0x0000000000000000
0x60a8933e12e0: 0x0000000000000000      0x0000000000000000
0x60a8933e12f0: 0x0000000000000000      0x0000000000000000
0x60a8933e1300: 0x0000000000000000      0x0000000000000000
0x60a8933e1310: 0x0000000000000000      0x0000000000000000
0x60a8933e1320: 0x0000000000000000      0x0000000000000000
0x60a8933e1330: 0x0000000000000000      0x0000000000000000
0x60a8933e1340: 0x0000000000000000      0x0000000000000000
0x60a8933e1350: 0x0000000000000000      0x0000000000000000
0x60a8933e1360: 0x0000000000000000      0x0000000000000000
0x60a8933e1370: 0x0000000000000000      0x0000000000000000
0x60a8933e1380: 0x0000000000000000      0x0000000000000000
0x60a8933e1390: 0x0000000000000000      0x0000000000000000
0x60a8933e13a0: 0x0000000000000000      0x0000000000020c61
0x60a8933e13b0: 0x0000000000000000      0x0000000000000000
0x60a8933e13c0: 0x0000000000000000      0x0000000000000000

As it shows above, the p heap chunk starts at 0x60a8933e1290 which has a size of 0x110 which is 0x100 plus header size. It indicates that the allocated size is acctually 255+1. There is no integer overflow here.

The second one is more like a question. Glad to know it is possible to solve this case. I'll try to learn how to implement a custom checker for this.