[klee-dev] Steps required for adding expr

[Dan Liew]

Hi,

On 4 April 2016 at 16:22, Sumit Kumar <sumit686215 at gmail.com> wrote:
> Hi,
>
> I was reading Expr.h file when I came across this comment:
>
>         <b>Steps required for adding an expr</b>:
>          -# Add case to printKind
>          -# Add to ExprVisitor
>          -# Add to IVC (implied value concretization) if possible
>
> Can anyone please explain the above in anyway possible (brief / detail) ?

I have been adding a lot of new expressions to my fork of KLEE
recently so I can tell you what I've found to be the bare minimum.

1. Add class declaration and a corresponding ``Expr::Kind`` to
``Expr.h`` and implementation to ``Expr.cpp``. You might need to
provide an implementation of ``computeHash()``, ``create()`` and
``compareContents()`` depending on which existing class your derive
form. You will need to add your new Expr class to
``Expr::printKind()``.
2. Add support for your new Expr class to ExprVisitor.
3. Add support for your new Expr class to STPBuilder.cpp and/or
Z3Builder.cpp depending on which solver you care about it.

If you want to be able to print your constraints as SMT-LIBv2 you'll
need to add support for your new Expr class in ``ExprSMTLIBPrinter``.
Similarly you will need to put some extra work in to add support for
your new Expr class to the KQuery printer/parser.

Hope that helps,
Dan.