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

[Thuan Pham]

Hi felicia,
In order to get unsat core, you should assign names for the constraints as
shown in the example at http://rise4fun.com/Z3/smtc_core.  In our
implementation, we modified the ExprSMTLIBPrinter.cpp to annotate all
asserts with names. One more thing should be noticed is that, you should
have more than one assert in the query.
Regards,
Thuan

On Mon, Sep 28, 2015 at 12:18 PM, felicia <felicia at comp.nus.edu.sg> wrote:

> 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
>>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed