Question about interface and constraint solving in klee

[Shiyu Dong]

Hi all,

I am working on klee and trying to integrate it with another solver (CVC4) to do some test. I found that klee communicates with STP by calling the c_interface.h. The good thing is that the solver I am using has the same interface (same name) and some of the inside functions have overlaps. I'm wondering if there is anythings other than the STPBuilder that I need to change in order to make this integration, because Daniel has mentioned that he did something so that klee can be separated from STP(http://www.mail-archive.com/klee-dev-AQ/***@public.gmane.org/msg00030.html).

Also, I know klee runs based on the .o file generated by llvm. So I want to ask in what language does klee represent the constraints and passing them to the solver? Is it in still in readable language such as SMT or CVC, or some lower level representation?

Last question about the big picture of klee, in order to have a better understanding about how klee deals with constraints, what part of the code should I pay more attention to?

Thanks in advance for helping me with these basic questions.

Best Regards,
Shiyu
--
Shiyu Dong
Graduate Student
Electrical & Computer Engineering
University of Texas at Austin
Tel: [phone]
E-mail: shiyud-***@public.gmane.org

[Cristian Cadar]

Hi Shiyu,

Post by Shiyu Dong
Daniel has mentioned that he did something so that klee can be

Yes, right now STP is not tightly integrated with KLEE anymore; a recent
patch by Hristina has removed a remaining dependency on STP arrays (see
http://llvm.org/viewvc/llvm-project?rev=166214&view=rev for details).
So integrating a new solver should be easy now.

Post by Shiyu Dong
So I want to ask in what language does klee represent the constraints
and passing them to the solver? Is it in still in readable language
such as SMT or CVC, or some lower level representation?

KLEE uses its own expression language internally (documented at
http://test.minormatter.com/~ddunbar/klee-doxygen/index.html and
http://klee.llvm.org/KQuery.html), and is constructing equivalent
STP expressions just before invoking STP.

Post by Shiyu Dong
Last question about the big picture of klee, in order to have a
better understanding about how klee deals with constraints, what
part of the code should I pay more attention to?

Look in lib/Expr and lib/Solver.


BTW, we currently have support for multiple constraint solvers
internally, and we might be able to make this extension available
relatively soon (email me directly for more details).

Best,
Cristian