UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

Stack access over-approximation #216

Open l-kent opened 4 months ago

l-kent commented 4 months ago

The analyses currently seem to overapproximate stack accesses that should be possible to distinguish.

The following is from the indirect_call/clang test .bir file. I've annotated it with the values for relevant variables given by the points-to analysis result at relevant points.

00000352:
00000356: R31 := R31 - 0x30
R31 == (stack_24(R31 + 40), stack_13(R31 + 16))
0000035c: #5 := R31 + 0x20
#5 == (stack_24(R31 + 40), stack_13(R31 + 16))
00000362: mem := mem with [#5, el]:u64 <- R29
00000368: mem := mem with [#5 + 8, el]:u64 <- R30
0000036e: R29 := R31 + 0x20
R29 == (stack_24(R31 + 40), stack_13(R31 + 16))
00000373: R8 := 0
0000037b: mem := mem with [R31 + 0xC, el]:u32 <- 31:0[R8]
00000382: mem := mem with [R29 - 4, el]:u32 <- 0
00000387: R8 := 0
0000038d: R8 := R8 + 0x754
00000395: mem := mem with [R31 + 0x10, el]:u64 <- R8
0000039a: R0 := 0
000003a0: R0 := R0 + 0x7DF
000003a5: R30 := 0x7A0
000003a7: call @printf with return %000003a9

000003a9:
000003ae: R8 := mem[R31 + 0x10, el]:u64
R8 == (stack_24(R31 + 40), stack_13(R31 + 16))
000003b3: R30 := 0x7A8
000003b6: call R8 with return %000003b8

000003b8:
000003bd: R0 := pad:64[mem[R31 + 0xC, el]:u32]
R0 == stack_6(R31 + 12)
000003c3: #6 := R31 + 0x20
#6 == (stack_24(R31 + 40), stack_13(R31 + 16))
000003c8: R29 := mem[#6, el]:u64
R29 == (stack_24(R31 + 40), stack_13(R31 + 16))
000003cd: R30 := mem[#6 + 8, el]:u64
R30 == (stack_24(R31 + 40), stack_13(R31 + 16))
000003d3: R31 := R31 + 0x30
000003d8: call R30 with noreturn

According to the analysis, stack_13 contains a pointer to 'greet', stack_24's contents is empty/unknown, and stack_6 contains the value 0bv32.

The analysis can't distinguish between accesses to stack_13 and stack_24, even though there shouldn't be any ambiguity. The analysis only resolves the indirect call to greet correctly at 000003b6 because it doesn't know what stack_24 points to and ignores it as a result.

This sort of issue is common across many different test cases.