[klee-dev] Is possible to mark a function as uninterpreted function?

[Dan Liew]

Hi Javier,

On 14 December 2016 at 13:28, Javier Godoy <j.godoy277 at gmail.com> wrote:
> Hi!
>
> Is possible to mark a function as uninterpreted function in Klee?
>
> Example i need:
>
>
> foo(int a)
> {
>   if( boo(a) > 0)
>       return 0;
>   else
>       return 1;
> }
>
> boo(int x) //I want to mark this as uninterpreted
> {
>  ...
>  return x;
> }

You could sort of model an uninterpreted function by having `boo`
return a fresh symbolic variable for every value of x it hasn't seen
before and the same symbolic variable for the corresponding value of x
previously seen.

This isn't really the right way to solve the problem. The STP solver
doesn't support uninterpreted functions however Z3 does and now that
we have first class Z3 support in KLEE this something that could be
implemented.

So the right way of going about this would be to

1. Introduce something like a  `UFExprCall` expression and a
`UninterpretedFunction` type to KLEE's Expr language. KLEE's Expr
language is not typed so this might be a bit of challenge.
2. Teach the Z3Builder and other parts of KLEE's code how to handle
these new parts of KLEE's Expr language
3. Figure out a way to annotate functions in C such that KLEE at
runtime can construct the `UninterpretedFunction`s in the program. You
also need to make sure that the function cannot be inlined (there is
an LLVM function attribute that can do this) and that it has no body
(so it can't change any state).

This would be a lot of work but could be a valuable contribution to
KLEE because it would give us a new way model certain functions. E.g.
if we were executing `sin()` we could replace that with a `UF` if we
can statically prove that we never branch on the value that is
returned by `sin()`.

I do not have time to do this myself so if you are interested in this
feature you would have to implement it.

Dan.