[klee-dev] [KLEE] About the DATA TYPE of the memory pointed by the POINTERS

[Frank Busse]

Hi,


On Thu, 29 Apr 2021 23:25:13 +0800 (CST)
董弈伯 <mr.asp at sjtu.edu.cn> wrote:

>         Also, the output of Klee test is shown in different encoding
> methods (like 0xffff.., char, int ,unsigned), does that mean it
> didn't keep the type information?

Tests are written in KLEE's .ktest file format and currently we do not
store type information in there (basically just a name, length and a
byte vector for each symbolic input). Hence, ktest-tool has to "guess"
types and prints common ones.

>         It seems that KLEE treat pointer as a continuous memory
> piece, which means KLEE does not "look into" the types of the
> pointers? If so, why then?

Not sure what you're asking exactly. KLEE just interprets LLVM and when
a program needs to "look into" a type, it does so on the LLVM level.

Let's take a simple example with a struct:
https://godbolt.org/z/cPbKz9bo8
Here you can see how the values are stored and how KLEE would get the
value for member "a" via getelementptr. [1]


Kind regards,

Frank


[1] https://llvm.org/docs/LangRef.html#getelementptr-instruction