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

[Thuan Pham]

Thanks Sudipta for the explanation :) As I mentioned in my first reply, we
use Z3 as an external solver. We form the query, save it to a file and
invoke Z3 to get unsat core, Z3 works as a separate process.
Regards,
Thuan

On Mon, Sep 28, 2015 at 4:14 PM, Sudipta Chattopadhyay <
sudiptaonline at gmail.com> wrote:

> Sorry for coming in the middle of discussion, I was following this thread
> for some time now.
>
> I believe you can install Z3 as a standalone tool and pass the query as an
> input, meaning
> that you can invoke Z3 as a separate process. If I understand correctly,
> that's what Thuan
> meant.
>
> Regards,
> Sudipta
>
> On Mon, Sep 28, 2015 at 10:06 AM, felicia <felicia at comp.nus.edu.sg> wrote:
>
>> Hi Thuan,
>>
>> I just realized metaSMT does not related to the query produced by
>> ExprSMTLIBPrinter.cpp
>> The query passed to the z3 in metaSMT might share the same constraint
>> with query of ExprSMTLIBPrinter, but the overall query might be different.
>> ExprSMTLIBPrinter.cpp is actually for logging purpose and it is not
>> directly passed as a query input to the solver.
>>
>> But, based on your explanation, it seems like you are using query string
>> produced by ExprSMTLIBPrinter and passed it to the solver. How do you able
>> to pass the query string in the SMT format directly to the solver? are you
>> using Z3 code in the rise4fun website?
>>
>> Thank you.
>>
>> Best Regards,
>>
>>
>> On 2015-09-28 12:44, Thuan Pham wrote:
>>
>>> 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 [3].  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 [1] 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 [1] 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
>>>
>>>> [2]
>>>>
>>>> [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 [3] [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 [4] [1]
>>>>
>>>
>>>  Links:
>>>  ------
>>>  [1] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev [4]
>>>  [2] http://rise4fun.com/Z3/smtc_core [3]
>>>  [3]
>>>
>>>
>>> https://github.com/agra-uni-bremen/metaSMT/blob/development/src/metaSMT/backend/Z3_Backend.hpp
>>> [2]
>>>
>>>
>>>
>>> Links:
>>> ------
>>> [1] http://rise4fun.com/z3
>>> [2]
>>>
>>> https://github.com/agra-uni-bremen/metaSMT/blob/development/src/metaSMT/backend/Z3_Backend.hpp
>>> [3] http://rise4fun.com/Z3/smtc_core
>>> [4] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>>
>>
>>
>> _______________________________________________
>> 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