Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

KLEE LLVM Execution Engine

klee.github.io

Post reply on HN
Print view View original

11–20 of 22 posts

Re: KLEE LLVM Execution Engine

#11

Post by TheNewAndy »

withzombies wrote: post #10
TheNewAndy wrote: post #3

Earlier quoted context omitted.

I use it - I am writing a subset-of-yaml parser, and I've littered the code with a bunch of abort()/assert() statements for things I don't think should be possible. Running klee over my code spits out ~100K test cases (I let it use any 10 byte YAML input), and so while I don't inspect the output of any of the cases - I do make sure that none of them crash. Similarly, if I make a change which I don't expect to change…

Have you checked out DeepState ( https://github.com/trailofbits/deepstate ), it's a symbolic unit testing framework that has an interface similar to google test.

I haven't - thanks.

Writing test harnesses specific to the different tools (so far, just AFL and KLEE) has not been particularly difficult - all of them fit easily on one screen. So I'm not sure that deepstate really brings much to the table for what I'm doing.

Re: KLEE LLVM Execution Engine

#13

Post by nickpsecurity »

mslate wrote: post #2

Anyone using this in practice?

You can find both interesting uses (esp extensions) and users on the page below:

http://klee.github.io/publications/

There's a large amount of work building on KLEE. Similarly, it builds on LLVM that has its own huge ecosystem. The potential of all that together is what interests me about it.

Re: KLEE LLVM Execution Engine

#15

Post by cryptonector »

modeless wrote: post #7
senatorobama wrote: post #4

What is CS 101 explanation for this project?

I found a blog post with a succinct explanation. > KLEE [runs] a program considering its input(or some other variables) to be symbols instead of concrete values like 100 or “cacho”. In very few words, a symbolic execution runs through the code propagating symbols and conditions; forking execution at symbol dependant branches and asking the companion SMT solver for path feasibility or counter-examples. https://feliam.…

Finally, a succint, pithy explanation.

This is great. Makes me want to use it.

Re: KLEE LLVM Execution Engine

#18

Post by cztomsik »

I wonder if we could somehow use the work done in prepack to generate similar tests for javascript.

BTW: I don't want to oversimplify it, but it basically just looks at each branch and generates data which would pass the branch, right?

Post reply on HN