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

[Sumit Kumar]

Hi Dan,

On 29 April 2016 at 14:30, Dan Liew <dan at su-root.co.uk> wrote:

> 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.
>

I was talking about 'Z3SolverImpl::getConstraintLog(const Query &query)'
which is eventually called by Executor::getConstraintLog(...) when the
backend is 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).
>
>
Thanks for the suggestion. It has improved my understanding.



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(..)``?
>
>
I used Z3 C++ API. I created a new solver object and used this method:
"solver::add(z3::expr, z3::char*)"




> >>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.
>
Let's hope it catches up fast. Z3 C++ api will make things really easy to
understand and use.


> 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.
>

I could not understand the 3rd point. Can you please explain it a little
more. It would help me understand the working of KLEE better.

--
Thanks and Regards,
Sumit
-------------- next part --------------
HTML attachment scrubbed and removed