DSA Stack Inconsistencies

[l-kent]

StackLocations are only created in two places and there are inconsistencies with the semantics of their parameters.

Here, StackLocation's size parameter refers to the maximum access size, with the offset being part of the regionIdentifier:

BASIL/src/main/scala/analysis/data_structure_analysis/Graph.scala

Line 116 in 7849e72

node.allocationRegions.add(StackLocation(s"Stack_${proc}_$offset", proc, byteSize))

Here, StackLocation's size parameter refers to the negative of the offset from R31:

BASIL/src/main/scala/analysis/data_structure_analysis/SymbolicAddressAnalysis.scala

Line 105 in 7849e72

Map(d -> IdEdge(), Left(SymbolicAddress(variable, StackLocation(s"Stack_${procedure.name}", procedure, -size), 0)) -> ConstEdge(TwoElementTop))

There are also inconsistencies with the way indirect stack accesses and negative offsets are handled. For example, in indirect_calls/functionpointer/clang:BAP

000003cf: R31 := R31 - 0x30
000003d5: #4 := R31 + 0x20
000003db: mem := mem with [#4, el]:u64 <- R29
000003e1: mem := mem with [#4 + 8, el]:u64 <- R30
000003e7: R29 := R31 + 0x20
000003ee: mem := mem with [R29 - 4, el]:u32 <- 0
000003f6: mem := mem with [R29 - 8, el]:u32 <- 31:0[R0]
000003fd: R8 := pad:64[mem[R29 - 8, el]:u32]

The access at %000003ee is to R31 + 0x1C (28) and the access at %000003f6 is to R31 + 0x18 (24) but the DSA produces nodes containing StackLocations with ids Stack_main_18446744073709551640 and Stack_main_18446744073709551644, which are off from the correct offsets by 2^64. This seems to be caused by not treating the negative BitVecLiterals correctly when adding them - either overflow was not taken into account or they were not converted into negative values.