[klee-dev] Metasmt using Z3 for getting unsat core

[felicia]

Hi,

Thank you very much for your answer. Hercules sounds interesting.  Is it open source?

I know KLEE produce an smt query. So, I think I could pass it to the z3 solver. But, I still not sure how the method get unsat core implementation in KLEE. For example in solver.cpp file there are methods like compute initial value and method to check the validity, so I would like to add get unsat core method in solver.cpp. Thank you.


Sent from Samsung Mobile

-------- Original message --------
From: Thuan Pham <thuanpv at comp.nus.edu.sg> 
Date: 22/09/2015  21:56  (GMT+08:00) 
To: felicia <felicia at comp.nus.edu.sg> 
Cc: klee-dev at imperial.ac.uk 
Subject: Re: [klee-dev] Metasmt using Z3 for getting unsat core 
 
Hi,
I haven't tried to work with Z3 through metasmt. However, in our previous work (Hercules: reproducing crashes in real-world application binaries), I implemented an interface function for S2E (which is built on top of KLEE and QEMU) to get unsat-core from Z3. What I did is to formulate a SMT LIB-v2 query, save it to a file and invoke Z3 (as an external process) to get unsat-core (if the query is unsat). An example of the query is here http://rise4fun.com/Z3/smtc_core.

If you want to get unsat-core from Z3 directly through metasmt interface, I think you just need to know the interface between KLEE and metasmt, formulate your query and send it through the interface.
Hope it helps,
Regards,
Thuan

On Tue, Sep 22, 2015 at 7:58 PM, felicia <felicia at comp.nus.edu.sg> wrote:
Hi,

I have installed metasmt and use Z3 as a solver. I actually need to implement code in KLEE
where Z3 solver able to produce unsat-core. I am currently still not sure how I implement it in KLEE.
I really appreciate if you can give suggestion about this.

Thank you very much.
Best Regards, 


Sent from Samsung Mobile

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


-------------- next part --------------
HTML attachment scrubbed and removed