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 <[email protected]> >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 <[email protected]> >> 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 <[email protected]> >> 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 <[email protected]> wrote: >> Hi Javier, >> >> On 14 December 2016 at 13:28, Javier Godoy <[email protected]> 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 >> [email protected] >> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev >> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> >> >> ______________________________ _________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/ mailman/listinfo/klee-dev >> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> >> >> >> >>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
