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
