[klee-dev] how to add label to assert statements

[Dan Liew]

Hi,

On 29 April 2016 at 06:55, Sumit Kumar <sumit686215 at gmail.com> wrote:
> Hi Dan,
>
> Thanks for introducing the z3 support. It has been great help. It has saved
> me tons of work :).
> Please find below my answers to some of your queries:
>
>>Yes your previous e-mails were misleading because you said
> "getConstraintLog method in Executor.cpp is called with
> logFormat=STP".
>
> Well, not exactly, because I am explicitly calling the getConstraintLog(...)
> method with logFormat=STP option even when the backend is z3. Now since my
> backend solver is z3, it in turn calls getConstraintLog(....) method on the
> z3 core solver object using the TimingSolver Object:
>
>     char *log = solver->getConstraintLog(query); //in Executor.cpp inside
> function getConstraintLog when logFormat=STP

Okay so our naming is really bad here. I've opened an issue so we
don't forget to fix this

https://github.com/klee/klee/issues/382

>>If your aim is to get to constraints in the SMT-LIBv2 format then why are
>> you using ``getConstraintLog()`` which will use the core solver's natural
>> constraint language (for Z3 this happens to be SMT-LIBv2 but you don't have
>> fine the grained control you need)? Instead you should do what Thuan is
>> suggesting and modify the ExprSMTLIBPrinter to add labels if that is your
>> goal.
>
> I chose to use the getConstraintLog method instead of modifying
> ExprSMTLIBPrinter for these reasons:
> 1. getConstraintLog(..) exposes Z3 C api to me. It allows me to modify/use
> Z3 C api to get desired output.

``Executor::getConstraintLog()`` doesn't really expose the Z3 C API to
you. The method just gets the solver to emit the constraint log which
if you're using Z3 eventually calls Z3.

> 2. getConstraintLog(..) method returns me a string instead of printing the
> result.

The ExprSMTLIBPrinter doesn't have to "print the result". It just
writes to an ``llvm::raw_ostream``. That can be a file but you can
also use ``llvm::raw_string_ostream`` instead to write to a
std::string. You use the following method to set the output.

ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output).

Any if you have used ``logFormat=SMTLIB2`` with
``Executor::getConstraintLog()`` you would have got a string in
SMT-LIBv2 format.

> Also, although I started with printing labels to assert statements, I later
> realized that I didn't need to do that as I had access to z3 c/c++ api and
> could pass the labels to z3 directly.

I'm curious what Z3 C API function did you use to label the Z3_asts?

Was it ``Z3_solver_assert_and_track(..)``?

>>If you are already using Z3 as the solver backend why don't you use
> its C API to get the unsat core?
>
> I also realized the same sometime back :) . I have already done exactly what
> you have suggested. I am able to get the unsat core using the z3 c++ api.


> P.S: While working on this I realized that it would be a lot better if
> instead of using Z3 C api, C++ api was used as Z3 C++ api is much easier to
> use than Z3 C api. I wonder if it would be good to rewrite the Z3 Core
> Solver methods using Z3 C++ api.

I don't want to use Z3's C++ API for several reasons

1. The C++ API is built on top of the C API so everything the C++ API
can do the C API can also do.
2. The C++ API doesn't expose everything the C API does. This is
improving but the C API is where all newly exposed features will be
added first.
3. We need to control Z3's memory management for Z3_ast and Z3_sort
nodes manually. IIRC the C++ API doesn't let you do this.

Dan.