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

[董弈伯]

Dear KLEE Colleagues:

        Hi there!

        I hope this email finds you well. I'm a bachelor student from Shanghai JiaoTong University, and was recently quite interested in symbolic execution. And, as you are guess, KLEE caught my eye at my first glance! As a symbolic execution engine, KLEE did execellent work——Its high coverage and efficiency really surprised me.

        Attracted by KLEE, I went to read the original paper (three times!), and tried all the tutorials from the github.io website, I also tried to write my own "weird cases", sure KLEE found all the "hidden bugs".

        And when I got more interested, I started to read the sourrce code. And as I recrusively read it, a question rose in my mind:

        In the executor::run function ,KLEE called `executeInstruction(state, ki);` to 'simulate' the execution.
        And during the simulation, KLEE destructed the "Instruction" into several cases and do the analysis.
        However, I don't find KLEE use the information of the Types of Pointers?

        I'm not quite sure with this, as this is my first try recursively diving in source code of such a magnificent project.

        I first guessed maybe the LLVM dumps all the information when generating IR (I thought ,maybe it only generated the hexical address?) And I went to read the LLVM documents and tried to use `llvm-dis` to transform the .bc file into .ll file. Then I found that actually all the types of pointers are strictly marked, and cannot convert from one to another casually (I found a 'bitcast' instruction when trying to convert a struct pointer to void pointer).

         I found some more information about "well-formed". That is to say, not all the behaviors accepted by the parser is well-formed, like the type of return value may not match. I guessed it was because I had always been using Clang as the compiler frontend, which may differ when using other frontends?

        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?

        In a word, my question is:
        
        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?

         I'd really appreciate it if you could shed some light on this topic. Thanks much! ;-)

Yours sincerely

                Asp
                A student from SJTU