36 Commits

Author SHA1 Message Date
Joe Ranweiler
973d2a9264
Add KLEE example 2018-02-25 10:27:47 -08:00
Joe Ranweiler
281c5117ed
Add example for DeepState_TakeOver() 2018-02-20 15:43:34 -08:00
Joe Ranweiler
12dc706534
Add crashing example tests 2018-02-14 12:06:26 -08:00
Joe Ranweiler
731876a7e6
Fix typo in example CMakeLists.txt 2018-02-10 16:09:36 -08:00
Peter Goodman
1aa468dabc Minor formatting changes. 2018-02-06 12:18:06 +08:00
Peter Goodman
d227cc7f34 Enabled PIC. 2018-01-22 21:19:54 -05:00
Peter Goodman
ee80baa0ea Minor fix. 2018-01-18 14:24:08 -05:00
Peter Goodman
2eaeb7480c Adding Google Flags-like command-line option parsing, though implemented in C, to the main executable. The code is ported from Granary2. 2018-01-07 16:25:31 -05:00
Peter Goodman
bdf9f97913 Fixed OneOf example. 2017-12-12 22:22:31 -05:00
Peter Goodman
ada078368f Removing testfs example, and moving it to pgoodman/testfs. 2017-12-12 22:09:31 -05:00
alex
dca3f7342e adding 2017-12-12 14:45:44 -08:00
alex
97162bdf13 missing comment 2017-12-12 12:26:02 -08:00
alex
acd4e025b6 Merge branch 'master' of https://github.com/trailofbits/deepstate 2017-12-12 12:24:44 -08:00
alex
5b35c46fba small edits 2017-12-12 12:24:09 -08:00
Peter Goodman
e9bd6dc177 Fixes one or two subtle issues. But the more interesting fix is that I implemented puts in terms of DeepState_Log. Calls to printf that had no format arguments are transformed by the compiler into calls to puts, but that wasn't being wrapped by DeepState, so it was appearing as though those log messages never actually happened. 2017-12-12 14:01:41 -05:00
alex
c65b0c7ba4 better version 2017-12-12 00:20:13 -08:00
alex
70090bd712 Version that works, test depth 2017-12-11 23:17:18 -08:00
Peter Goodman
669f6cf3f9 Made the OneOf example work. 2017-12-11 19:40:39 -05:00
alex
76ff9ec5b3 capture fixed 2017-12-11 14:56:48 -08:00
alex
26657954c7 OneOf example (failing) 2017-12-11 14:30:37 -08:00
Peter Goodman
8248bbdcbc Removed usage of old name, added in a Euler power of like primes example. When the pairwise ASSERT_NEs are absent, you get interesting results that show examples of integer overflows. 2017-12-10 20:08:08 -05:00
Peter Goodman
188d4517d8 Added prime polynomial example, new Pumping function to address scalability challenges with primality testing, and some improvements to the streaming interface, where if you don't stream in values, then the python side doesn't end up printing out some 'empty' stream infos. 2017-12-09 16:43:43 -05:00
Peter Goodman
3aaaf71b85 Added support for c++ test fixtures. 2017-12-08 23:58:59 -05:00
Artem Dinaburg
2157f67dac Add an example that modifies an existing C program for symbolic testing 2017-11-02 00:33:35 -04:00
Peter Goodman
bc208dbd4d Fixes issue where the angr script printed out the wrong symbol bytes. 2017-11-01 21:27:08 -04:00
Peter Goodman
4f914e4eee Fixes to stream formatting of doubles, they weren't being streamed before. Implemented the chk versions of printf and such, so that they all route through the logging interface as well. Implemented the concretization APIs. 2017-11-01 17:56:54 -04:00
Peter Goodman
d2bc82fc35 Renaming from McTest to DeepState. 2017-11-01 13:38:32 -04:00
Peter Goodman
f7f029965b Whatever I had before renaming. 2017-11-01 12:14:22 -04:00
Peter Goodman
a46e06b03b Refactored to split common code between Manticore and Angr out into common.py. Implemented the new deferred streaming stuff, it seems to work semi-well for this simple cases I've tested, but there's still work to do. The latest code has some remaining issues. Printing out the final input bytes in Angr shows the wrong thing, although what gets streamed out is right. This is visible when running mctest-angr examples/ArtihmeticProperties. With Manticore, the big issue is that it doesn't properly pickle smt expressions (or something to this effect), so I'm ending up with multiple definitions of the same stuff and that throws exceptions. This is tricky to deal with because the streaming of output needs to be able to save symbolic data. 2017-11-01 02:42:31 -04:00
Peter Goodman
3702bfcb81 Changed how the logging works to log to a static buffer, then the hooks pull info out from there. 2017-10-30 14:16:02 -04:00
Peter Goodman
e4f4cfe0db Kind of feature parity between Manticore and Angr on these tests. 2017-10-30 00:45:59 -04:00
Peter Goodman
e0f104aaef Adding logger support, and other things. 2017-10-29 18:54:41 -04:00
Peter Goodman
89da3e8e94 Made it so that tests can be run on their own, independent of a symbolic executor. This will open up libFuzzer support, and concrete execution of solved-for test case inputs. Removed all stuff related to sections. Made tests get registered via initializers. Working on exposing the API functions to be hooked by Manticore via a special system call with addres 0x41414141. Split the Angr version out into the mctest-angr binary, and going to try to make the mctest binary use Manticore. 2017-10-28 19:13:59 -04:00
Peter Goodman
0d336bd4d6 Fixed build errors for c++ test basics. Added a ForAll thingy to abstract around making symbols. Shortened section name lengths. Added a simple arithmetic properties test case. 2017-10-28 01:11:59 -04:00
Peter Goodman
76585f095b Improvements. Now hooking fewer functions, and instead making on big array symbolic. This will make it easier to run the inputs concretely (by eventually filling in the array with the concrete bytes), and will also make possible fuzzer integration (where the fuzzer mutates the bytes of the array) possible. 2017-10-28 00:09:33 -04:00
Peter Goodman
6249ec6208 Initial commit. 2017-10-27 16:34:58 -04:00