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

[Thuan Pham]

Hi,
I have a quick check on the APIs of MetaSMTSolver in solver.cpp. I think
you may need to add one more method based on the computeTruth method.
Basically, instead of return the validity of the query, you return the
output of the solver (Z3 in this case) as a string. And hence, you can
parse the string to get the unsat core. However, the implementation for the
new method seems to be non-trivial. You may need to modify the Solver.cpp
and also some parts of the metaSMT library.

According to the code of Z3_Backend at
https://github.com/agra-uni-bremen/metaSMT/blob/development/src/metaSMT/backend/Z3_Backend.hpp,
if I understand correctly, the function "solve" (at line 197) will be
invoked. You may debug the function first and see how it works as well as
how you can modify it to get unsat core.

In terms of our work - Hercules, it is not open source yet.
Regards,
Thuan

On Tue, Sep 22, 2015 at 10:40 PM, felicia <felicia at comp.nus.edu.sg> wrote:

> 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