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

[felicia]

Hi,

Thank you very much for checking on the API.
I agree with your suggestion, so my implementation in the function 
"solve", would be
checking the sat result first and if I find the result was unsat, I will 
call the function get unsat core which is provided by the 
Z3_Backend.hpp.
However, it seems the unsat core always return empty. I have printed the 
SMT Query, and it looks like this:

(set-logic QF_AUFBV )
(declare-fun p1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun p2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat  (select  p2 (_ bv3 32) ) (concat  (select  
p2 (_ bv2 32) ) (concat  (select  p2 (_ bv1 32) ) (select  p2 (_ bv0 32) 
) ) ) ) ) (?B2 (concat  (select  p1 (_ bv3 32) ) (concat  (select  p1 (_ 
bv2 32) ) (concat  (select  p1 (_ bv1 32) ) (select  p1 (_ bv0 32) ) ) ) 
) ) ) (=  true (=  (bvadd  (_ bv2 32) (bvmul  ?B2 ?B2 ) ) (bvmul  ?B1 
?B1 ) ) ) ) )
(check-sat)

and then I checked on rise4fun.com/z3 by adding the option (set-option 
:produce-unsat-cores true) and also put (get-unsat-core). So it become 
like this:
(set-option :produce-unsat-cores true) ; enable generation of unsat 
cores
(set-logic QF_AUFBV )
(declare-fun p1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun p2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (let ( (?B1 (concat  (select  p2 (_ bv3 32) ) (concat  (select  
p2 (_ bv2 32) ) (concat  (select  p2 (_ bv1 32) ) (select  p2 (_ bv0 32) 
) ) ) ) ) (?B2 (concat  (select  p1 (_ bv3 32) ) (concat  (select  p1 (_ 
bv2 32) ) (concat  (select  p1 (_ bv1 32) ) (select  p1 (_ bv0 32) ) ) ) 
) ) ) (=  true (=  (bvadd  (_ bv2 32) (bvmul  ?B2 ?B2 ) ) (bvmul  ?B1 
?B1 ) ) ) ) )
(check-sat)
(get-unsat-core)

Function unsat core in the rise4fun.com/z3 is also return empty for this 
particular query. The smt query produced by KLEE might not sufficient to 
produce unsat core, although the result of the formula is unsat. I hope 
you could give further suggestion for me about this.

Thank you very much.

Best Regards,


On 2015-09-24 00:04, Thuan Pham wrote:
> 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
> [3], 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 [2].
>> 
>> 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 [1]
> 
> 
> 
> Links:
> ------
> [1] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> [2] http://rise4fun.com/Z3/smtc_core
> [3]
> https://github.com/agra-uni-bremen/metaSMT/blob/development/src/metaSMT/backend/Z3_Backend.hpp