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

Tue Dec 27 06:43:03 GMT 2016

Hi Yude, 

Others would probably have a better idea, but I think replacing calls to libm functions may not cause (many) false positives. I agree this may reduce the number of tests for the same coverage.

You may also want to have a look at the paper

https://www.usenix.org/system/files/conference/usenixsecurity15/sec15-paper-ramos.pdf

seems to be a KLEE-based approach that introduces over approximations for the purpose of finding more bugs. 

Best, 
Andrew 

---- Yude Lin wrote ----

>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