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 <[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 [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 [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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
