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 < [email protected]> 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 <[email protected]> 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 <[email protected]> >>> 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 <[email protected]> >>>> 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 <[email protected]> >>>> Date: 22/09/2015 21:56 (GMT+08:00) >>>> To: felicia <[email protected]> >>>> Cc: [email protected] >>>> 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 <[email protected]> >>>> 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 >>>> [email protected] >>>> 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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
