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

Mon Sep 28 09:06:21 BST 2015

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