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

[Yude Lin]

Hi Andrew,

Good from you too!

I've never thought about the problem in terms of non-determinism.
Yes, our work is related to using summaries, but I actually want to discuss
some thing more general here.

My understanding of KLEE is that it doesn't do over-approximation. It's
either
precise or when it makes concrete calls to libraries it's
under-approximating.
My question is is it a bad idea to consider over-approximation? Like in
this case
we are over-approximating what the boo function can do if we make it an
uninterpreted function.

By doing this I'm thinking KLEE will spend less time on that function call
and
focus more on other parts of the program. But the downside is it introduces
imprecision and false alarms. I wonder how KLEE devs/users view this
imprecision (as I'm quite new around here). Thanks!

Regards,
Yude

On Fri, Dec 23, 2016 at 8:11 PM, Andrew Santosa <asantosa1999 at gmail.com>
wrote:

> Hi Yude,
>
> Good to hear from you!
>
> I guess you are replacing function calls with their symbolic summary under
> the weakest semantics. (What I meant by weakest semantics here can even be
> nondeterministic, so this is more general than uninterpreted function: In
> your approach, sequence of f(5) calls can return different values, whereas
> this can not be the case if f was an uninterpreted function).
>
> Ok, so I admit this has the merit I previously did not think about, which
> is the use of function summary, either as uninterpreted function or
> using the weakest semantics. It may not improve the coverage in the caller,
> but it may reduce the number of paths traversed in achieving the same
> coverage (in the caller). I guess viewing it this way, the idea may beworth
> trying out after all, regardless of whether it's applied to libm or user
> functions.
>
> Best,
> Andrew
>
> Sent from my Sony Xperia™ smartphone
>
> ---- Andrew Santosa wrote ----
>
>
>
>
> On Friday, 23 December 2016, 14:37, Yude Lin <yudel at student.unimelb.edu.au>
> wrote:
>
>
> Hi Guys,
>
> For a function in the program source code, i.e., not a library function,
> do you think we have reasons to make it uninterpreted? My idea is that
> KLEE could generate a lot of states in some functions but they don't
> necessarily help with coverage. For example mathematical functions.
>
> I'm working on something similar to this. I currently make KLEE skip
> functions
> that we think are less efficient in increasing the coverage, so that KLEE
> can
> spend more time on those functions that are.
>
> Currently we make the return value of such function a fresh symbolic
> variable.
> Now it only works on functions with no side effect (more specifically,
> functions
> that don't take/return pointers or use globals).
>
> Regards,
> Yude
>
> On Sat, Dec 17, 2016 at 3:42 PM, Andrew Santosa <santosa_1999 at yahoo.com>
> wrote:
>
>
>
> libm functions such as sin() are 1) usually side-effect free and 2) on
> floating-point values, which are not typically used for control decision,
> so many of them can probably be shown statically to not affect branch
> decision.
>
>
> But let us think about the purpose of symbolicizing them:
>
> 1. Since they do not typically affect branch decision, symbolicizing them
>    is not needed to obtain better coverage.
> 2. Symbolicizing them may be needed for discovering floating-point errors,
>    but in that case we need to provide the real number semantics or some
>    auxiliary semantics specific to our purpose, to the libm functions and
>    not leaving them uninterpreted.
>
> Given the above, I am still unsure about the extent of the merit of
> implementing
> a support for uninterpreted functions, but I am probably missing something.
>
> Best,
> Andrew
>
>
>
> On Saturday, 17 December 2016, 2:09, Dan Liew <dan at su-root.co.uk> wrote:
> 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.
>
>
> ______________________________ _________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
> ______________________________ _________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>
>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed