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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
