forked from zhangzhenghsy/SymBisect
-
Notifications
You must be signed in to change notification settings - Fork 0
/
NEWS
339 lines (305 loc) · 21.4 KB
/
NEWS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
KLEE 2.2, 7 December 2020
=========================
Incorporating changes from 4 March 2020 to 7 December 2020.
Maintainers during this time span: @ccadar and @MartinNowack
Documentation at http://klee.github.io/releases/docs/v2.2
== Major features ==
- Added support for C++ exceptions (@corrodedHash, @futile, @jbuening)
- Correctly copy variadic arguments with byval attribute (@ccadar)
- Modified the random path searcher to work on a subset of states (@kren1)
- Added state IDs to improve determinism (@251)
- Overhauled the (Travis CI) build scripts (@MartinNowack)
- Restructured header files (@ccadar)
== LLVM support ==
- Current recommended version is LLVM 9
- Added support for LLVM 11 (@lzaoral)
- We have decided to extend support for LLVM 3.8 to 5, but KLEE 2.2 will be the last version with support for LLVM <6
== Options, scripts and KLEE intrinsics added, changed or removed ==
- Changed --debug-print-instructions to also print state IDs (@251)
- Added -rng-initial-seed to set the seed for KLEE's random number generator (@251)
- Added klee_is_replay intrinsic which returns whether the code is being executed symbolically or in replay mode (@alastairreid)
- Added --compress-process-tree to remove intermediate nodes in the process tree when possible (@sebastianpoeplau)
- Added klee-zesti, a ZESTI-like wrapper (@kren1)
- Added --table-format=readable-csv/csv to klee-stats (@251)
== Other changes ==
- Fixed GlobalAlias initialization (@jbuening)
- Enforced fork/branch limits in branch() and fix double termination (@251)
- Enhanced POSIX runtime in the case where a symbolic file is given as an absolute path, i.e. /current/work/dir/A (@kren1)
- Named jobs in Travis CI for better visualization of results (@ccadar)
- Fixes and improvements in the statistics code including klee-stats (@251)
- Added a simple model for GET/SET_LK (@kren1)
- Fixed bug in the handling of vectorized code (@Warfley)
- Fixed bug in the handling of STP array names (@MartinNowack)
- Fixed bug in Z3Solver::getConstraintLog (@daniel-grumberg)
- Added support for reading strings from the middle of objects in readStringAtAddress (@mchalupa)
- Disabled asm lifting for memory fences with return values (@MartinNowack)
- Fixed bug when the search requires MD2U (@adrianherrera)
- Added support for fshr/fshl intrinsics (@alastairreid)
- Refactored the constraint manager (@MartinNowack)
- Changed DiscretePDF to use IDs instead of pointers to remove nondeterminism (@251)
- Added a more robust handling of unknown intrinsics: if an unknown intrinsic is encountered on a path, that path is terminated but the others can proceed (@alastairreid)
- Fixed PTree::remove to clean the tree properly (@sebastianpoeplau)
- Added support for multiple symbolic files to gen-bout (@kren1)
- Added a PR template, with a checklist documenting the most frequent issues we have encountered (@ccadar)
- Fixed the behaviour of klee-stats for broken or empty DBs (@251)
- Added support for klee_open_merge and klee_close_merge in replay (@ccadar)
- Fixed the handling of global variables while validating direct call targets (@MartinNowack)
- Fixed the handling of the fabs intrinsic (@dlaprell)
- Added support for the fneg instruction (@jbuening)
- Removed incompatibility between merging and the random path search (@251)
- Fixed the behaviour of klee-libc to call the functions in __cxa_atexit in reverse order (@tomsik68)
- Fixed the behaviour of bcmp in klee-libc (@alastairreid)
- Added support for multi-version bitcode libraries (@MartinNowack)
- Added support for several fortified functions, -D_FORTIFY_SOURCE (@ccadar)
- Modernize ref<> and isa<> nullptr checks (@jbuening)
- Switched CI from Travis CI to GitHub Actions (@MartinNowack, with thanks to @jordr)
- Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @adrianherrera, @alastairreid, @andrewvaughanj, @andronat, @arrowd, @ccadar, @dependabot, @i-ky, @jbuening, @jiseongg, @jordr, @kren1, @lahiri-phdworks, @MartinNowack, @yxliang01)
KLEE 2.1, 3 March 2020
=======================
Incorporating changes from 20 March 2019 to 3 March 2020.
Maintainers during this time span: @ccadar and @MartinNowack
Documentation at http://klee.github.io/releases/docs/v2.1
== Major features ==
- New container-based architecture for KLEE Web (@Denis-Gavrielov, @andronat)
- Changed the statistics framework to use SQL and improve klee-stats (@kren1, @251)
- Added Grafana visualisation to klee-stats (@gdish, @KennyMacheka, @kren1)
- Brought gen-random-bout up-to-date (@domainexpert)
- Fixed support for FreeBSD (@arrowd)
- Replaced signalling with synchronous checks for implementing timers (@251)
- Improved reference handling (ref<>) (@MartinNowack)
== LLVM support ==
- Added support for LLVM 9 and 10 (@jbuening)
- Removed support for LLVM <3.8 (@jbuening)
- KLEE 2.1 will be the last version with support for LLVM <6
== Options, scripts and KLEE intrinsics added, changed or removed ==
- Replaced intrinsic klee_alias_function("foo", "bar") with option -function-alias=foo:bar, which supports regular expressions (@jbuening, @SolalPirelli)
- Removed -max-instruction-time (@251)
- Added -timer-interval (default 1s) to specify the minimum interval to check timers (@251)
- Added nurs:rp searcher which uses non-uniform random search with 1/2^depth (@kren1)
- Replaced the behavior of the nurs:depth searcher to use NURS with depth (@kren1)
- klee-stats: new --grafana option (see above)
- klee-stats: new --to-csv option for converting statistics to the CSV format (@251)
- klee-stats: removed --sample-interval, --sort-by, --compare-by, --precision. These can be now simulated by querying the SQL database directly (@kren1)
- klee-replay: added --keep-replay-dir option to keep the replay directory (@ccadar)
== Other changes ==
- Added support for llvm.fabs (@futile)
- Added support for saturated arithmetic intrinsics (@mateon1)
- Added support for llvm.objectsize (@MartinNowack)
- Added support for llvm.is.constant (@arrowd)
- Fixed bugs in --optimize-array (@kren1)
- Removed statistics limit from istats (@MartinNowack)
- Refactored PTree (@251)
- Improved klee-replay and made it safe to run multiple instances in parallel (@ccadar)
- Check if read-only objects are marked as symbolic (@MartinNowack)
- Allow main() with 3 arguments (@ccadar)
- Improved the structure of the codebase (@ccadar)
- Improved KLEE's CI build scripts (@MartinNowack, @jbuening)
- Smaller refactorings, fixes and improvements, test cases, maintenance, comments, web version, website, etc. (@251, @arrowd, @benquike, @ccadar, @cyberwookiee, @danielschemmel, @Denis-Gavrielov, @dependabot, @domainexpert, @futile, @gdish, @JasonPap, @jbuening, @jirislaby, @KennyMacheka, @kren1, @MartinNowack, @qurben)
KLEE 2.0, 19 March 2019
========================
Incorporating changes from 22 July 2017 to 19 March 2019
Maintainers during this time span: @AndreaMattavelli, @ccadar, @delcypher, @MartinNowack
Documentation at http://klee.github.io/releases/docs/v2.0
== Major features ==
- Added support for KLEE array optimizations from ISSTA'17 paper "Accelerating Array Constraints in Symbolic Execution" (@AndreaMattavelli, @MartinNowack, @ccadar)
- Added support for LibC++ (--libcxx flag) (@corrodedHash, @futile, @MartinNowack)
- Added support for CVC4 and Yices2 via metaSMT (@hoangmle)
- Added better path merging functionality via klee_open_merge and klee_close_merge (@corrodedHash, @futile)
- Fixed support for vector instructions (@MartinNowack)
- Support for recent LLVM versions (see "LLVM support" below)
- New categorized --help menu, with LLVM options hidden by default (see "Options, scripts and intrinsics changed or removed" below)
== LLVM support ==
- Added support for LLVM 3.7 - 7.0 (@jirislaby)
- Added support for LLVM 8.0 (@MartinNowack)
- KLEE 2.0 will be the last release with support for LLVM 3.4 to 3.7
- Removed support for LLVM <3.4 (@MartinNowack)
== Options, scripts and intrinsics changed or removed ==
- Renamed several options (@ccadar)
* --environ to --env-file
* --no-output to --write-no-tests
* --red-zone-space to --redzone-size
* --run-in to --run-in-dir
* --seed-out to --seed-file
* --seed-out-dir to --seed-dir
* --stop-after-n-tests to --max-tests
* --use-cache to --use-branch-cache
* --use-construct-hash to --use-construct-hash-stp
* --warn-all-externals to --warn-all-external-symbols
- Replaced --no-externals and --allow-external-sym-calls with --external-calls (@ccadar)
- Added --libcxx option to enable LibC++ support (see "Major features" above)
- Added option --max-stack-frames to limit the number of stack frames used (@MartinNowack)
- Added --klee-call-optimisation option, which can be set to false to disable some optimizations that interact incorrectly with the checks injected by KLEE. See https://github.com/klee/klee/pull/1059 for more details (@MartinNowack)
- Added support for disabling --batch-instructions and --batch-time by setting them to zero (@ccadar)
- Removed option --disable-opt (@ccadar)
- Removed klee-gcc and klee-clang (@251, @MartinNowack)
- Removed support for klee_make_symbolic with two arguments (@ccadar)
- Allow NULL as name to klee_int, to create "unnamed" object (@251)
- New time API used in options (@251)
- Improved the output of ktest-tool and added an --extract option (@251)
- Categorized options in --help, improved help messages, and hid LLVM options by default (@ccadar)
== Other changes ==
- Updated build system to detect whether STP, Z3, metaSMT are available (@delcypher)
- Fixed test case counter: previously the number of test cases generated by KLEE was always incremented, even if a symbolic solution was not found (@andreamattavelli)
- Added checks for div/mod by zero and overshifts in constant expressions (@ccadar)
- Fixed a bug causing KLEE to generate files with no permissions bits set (@ccadar)
- Added clean_doxygen target and a global clean_all target to the build system (@delcypher)
- Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers (@andreamattavelli)
- Fixed assert in BFSSearcher that does not hold as part of interleaved searcher (@jbuening)
- Fixed huge allocation size constant (@davidtr1037)
- Added Codecov support (@andreamattavelli, @MartinNowack)
- Store cex cache stats and report them in klee-stats (@helicopter88)
- Fixed incorrectly incremented stats for dumped states (@251)
- Fixed bug where KLEE would not output test cases when --exit-on-error is enabled (@buszk)
- Added support for blockaddress and indirectbr instructions (@251)
- Implemented klee_prefer_cex() and klee_abort() for replay mode (@Lysxia)
- Fixed handling of errno when external functions are invoked (@MartinNowack)
- Fixed utimes() behavior for symbolic files when the second argument is NULL (@yxliang01)
- Improved handling of constant array in Z3 (@kren1)
- Improved the handling of external calls with symbolic data (@kren1)
- Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not (@ccadar)
- Improved ConstantExpr performance (@kren1)
- Improved linking and optimizations order (@MartinNowack)
- Enabled TCMalloc by default (@kren1)
- Disabled unit testing in default build (@AndreaMattavelli)
- Added resolve time to klee-stats --print-all (@251)
- Improved the startup sequence enabling the POSIX runtime (@MartinNowack)
- Added ASan and UBSan flags to lit (@251)
- Added support for handling multiple SIGSEGVs in external calls (@251)
- Added checks for correct usage of the POSIX mode (@ccadar)
- Added support for klee-replay on OSX (@251)
- Added lowering pass for atomic instructions (@erzett, @futile)
- Improved handling of metadata (@MartinNowack)
- Improved efficiency of div/mod and shift checks by skipping unnecessary checks (@MartinNowack)
- Added support for memalign (@corrodedHash)
- Enable C++14 support (@MartinNowack)
- Fixed issue with aliases that point to other aliases (@jbuening)
- Added workaround for the LLVM bug PR39177 (@jbuening)
- Updated dependency build system for KLEE (@MartinNowack)
- Fixed the Docker deployment for KLEE (@MartinNowack)
- Added support for compiling KLEE with MSan and UBSan's integer sanitizer (@MartinNowack)
- Fixed representation of ReadExpr's into equivalent arrays (@MartinNowack)
- Added support for debug information provided by newer LLVM versions (@MartinNowack)
- Added many KLEE-related publications (@251)
- Smaller refactorings, fixes and improvements, test cases, maintenance,
comments, web version, website, etc. (@andronat, @251, @andreamattavelli, @ccadar, @corrodedHash, @danielschemmel, @delcypher, @itbot08, @jasondavies, @jbuening, @jirislaby, @kren1, @Lysxia, @MartinNowack, @Mic92, @odeits-vidder, @SolalPirelli, @szeyiuchau, @Tipwheal, @yannicnoller)
KLEE 1.4.0, 21 July 2017
========================
(Incorporating changes from 4 November 2016 up to and including 21 July 2017)
Documentation at http://klee.github.io/releases/docs/v1.4.0/
This will be the last version supporting LLVM 2.9 and the autoconf build system.
- New CMake build system (@delcypher, @jirislaby)
- Added support for vectorized instructions (@delcypher)
- Fixed and documents BFS searcher behaviour (@MartinNowack, @ccadar)
- Renames .pc files to .kquery files (@holycrap872)
- Removed option --randomize-fork (@ccadar)
- Changed preferred permissions from 0622 to the more standard 0644 in the
POSIX model (@ccadar)
- New target name, "make systemtests", for running the system tests. This replaces "make test". Running the unit tests is still accomplished via "make unittests".
- Better support for MacOS (@andreamattavelli, @delcypher)
- Enabled support for ASan builds of KLEE (@delcypher)
- Support long long values in --stop-after-n-instructions for LLVM > 2.9
(@andreamattavelli)
- Teach KLEE to respect the requested memory alignment of globals and stack
variables when possible (@delcypher)
- Added new option --warnings-only-to-file which causes warnings to be written
to warnings.txt only (@ccadar)
- metaSMT improvements (@hoangmle)
- KLEE-web improvements (@andronat, @helicopter88)
- Fixed bug in the implementation of NotExpr (@delcypher)
- Fixed a bug leading to data loss when writing into files (@ccadar, @gladtbx)
- Some improvements and refactoring to the Expr library (@delcypher)
- Added missing constant folding opportunity when handling constant arrays
(@andreamattavelli, @delcypher)
- Teach klee::getDirectCallTarget() to resolve weak aliases (@delcypher)
- Fixed handling of internal forks (@gladtbx)
- Improved replay using libkleeRuntest (@delcypher)
- Added -debug-assignment-validating-solver feature to check the correctness
of generated assignments (@delcypher)
- Added -debug-z3-dump-queries, -debug-z3-validate-models and
-debug-z3-verbosity options useful for debugging the interaction with Z3
(@delcypher)
- Added geq/lt-llvm- configs in lit (@jirislaby)
- Work on supporting newer LLVM versions (@jirislaby)
- Fixed bug where stats would not be updated on early exit (@delcypher)
- Reworked the external dispatching mechanism (@delcypher)
- Added support for creating release documentation (@delcypher)
- Smaller refactorings, fixes and improvements, test cases, maintenance,
comments, website, etc. (@adrianherrera, @akshaynagpal, @AlexxNica,
@andreamattavelli, @bananaappletw, @bigelephant29, @bunseokbot, @ccadar,
@delcypher, @emlai, @hoangmle, @jirislaby, @kren1, @levex,
@Manouchehri, @MartinNowack, @mechtaev, @Mic92, @omeranson, @rtrembecky,
@thestr4ng3r, @tomek-kuchta)
KLEE 1.3.0, 30 November 2016
============================
(Incorporating changes from 1 April up to and including 3 November 2016)
* Improved determinism of KLEE, an essential feature for experiments involving KLEE (@MartinNowack)
* KLEE-web has been improved and refactored, and now available at http://klee.doc.ic.ac.uk/ (@giacomoguerci, @helicopter88, @andronat, @ccadar, based on work by @ains, @ben-chin, @ilovepjs, @JamesDavidCarr, Kaho Sato, Conrad Watt, @ccadar)
* Renamed --replay-out to --replay-ktest and --replay-out-dir to replay-ktest-dir (@delcypher)
* Split creation of symbolic files and stdin in two distinct options, documented at http://klee.github.io/docs/options/#symbolic-environment (@andreamattavelli)
* Support for logging queries before invoking the solver via --log-partial-queries-early, useful for debugging solver crashes (@MartinNowack)
* Added --stats-write-after-instructions and --istats-write-after-instructions to update each statistic after n steps (@MartinNowack)
* Added --compress-log and --debug-compress-instructions to gzip-compress logs (@MartinNowack)
* Added --exit-on-error-type option for stopping execution when certain error types are encountered (@jirislaby)
* Updated and improved metaSMT support and added TravisCI targets (@hoangmle)
* Added option --debug-crosscheck-core-solver to allow crosschecking of solvers (@delcypher)
* Explicitly made division total in STP (@ccadar)
* Extended support for assembler raising (@MartinNowack)
* Disabled --solver-optimize-divides, as the optimization is currently buggy (@ccadar)
* Improved --debug-print-instructions options with more logging options (@andreamattavelli)
* Improved stub for times() not to trigger a NULL dereference (@ccadar)
* Allow relocation of installed KLEE tree (@ShayDamir)
* Fixed bug in independent solver (@delcypher)
* Fixed alignement of varargs (@MartinNowack)
* Fixed variable shifting behavior with different sizes and generation of STP shift operations with variable amounts (@MartinNowack)
* Fixed handling of non-sized globals (@jirislaby)
* Fixed klee_get_obj_size() crash on 64-bit (@hutoTUM)
* Fixed bug in Kleaver's parser (@andreamattavelli)
* Refactorings, small fixes and improvements, test cases, maintenance and website: (@andreamattavelli, @ccadar, @delcypher, @domainexpert, @giacomoguerci, @hoangmle, @helicopter88, @jirislaby, @Justme0, @kren1, @MartinNowack, @mchalupa)
KLEE 1.2.0, 31 March 2016
=========================
* Added native support for Z3 (@delcypher)
* Made it possible to build KLEE without using STP and only MetaSMT (@delcypher)
* Added support for tcmalloc, which allows KLEE to better track memory consumption (@MartinNowack)
* Added support for lowering the ``llvm.objectsize`` intrinsic (@delcypher)
* Added soname for Runtest dynamic library (@MartinNowack)
* Added support to load libraries from command line (@omeranson)
* Added command line flag --silent-klee-assume to suppress errors due to infeasible assumptions (Valentin Wüstholz, @wuestholz)
* Changed code to print out arrays deterministically (@MartinNowack)
* Improved klee-clang script (@msoos)
* Added code to dump queries and assignments (@MartinNowack)
* Code cleanup and refactorings (@delcypher, @MartinNowack)
* Improvements to code infrastructure (@delcypher, @domainexpert, @MartinNowack, @mdimjasevic, @msoos)
* Fixed several memory leaks (@delcypher)
* Fixed a bug with how non-power of 2 values were written to memory (@kren1)
* Fixed valueIsOnlyCalled() used by MD2U (@yotann)
* Fixed SELinux signatures (@lszekeres)
* Fixed incorrect position of Not in Expr::Kind (@delcypher)
* Fixed wrong std::vector usage after reserve() call (@pollnossa)
* Improved documentation (@bananaappletw, @ccadar, @delcypher, @mdimjasevic, @Teemperor, @ward, @wuestholz)
KLEE 1.1.0, 13 November 2015
============================
* Made LLVM 3.4 and STP 2.1.0 the recommended versions for installing KLEE (Cristian Cadar, @ccadar; Dan Liew, @delcypher; Martin Nowack, @MartinNowack; Mate Soos, @msoos)
* Added instructions for using the Docker images (Dan Liew, @delcypher)
* Added NEWS file to keep track of changes for each release (Cristian Cadar, @ccadar)
* Added coverage information for the current KLEE codebase (Timotej Kapus, @kren1)
* Added -entry-point=FOO option, where FOO is the name of the function to use as the entry point for execution (Riccardo Schirone, @ret2libc)
* Switched STP to v2.1.0 (instead of the old r940) in TravisCI (Martin Nowack, @MartinNowack)
* Improved Dockerfiles to use specific dependency versions (Dan Liew, @delcypher)
* Bug fix: Fixed signed division by constant 1/-1 (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1)
* Bug fix: Generate SRrem expressions correctly (Martin Nowack, @MartinNowack, reported by Timotej Kapus, @kren1)
* Bug fix: Allowed the generation of initial values for queries with empty constraint set (Martin Nowack, @MartinNowack)
* Bug fix: Fixed assertion failure in getDirectCallTarget (Sean Bartell, @yotann)
* Bug fix/test improvement: Use a temporary directory instead of /tmp in futimesat test (Andrew Chi, @andrewchi)
* Various fixes and improvements to the website (Eric Rizzi, @holycrap872; Martin Nowack, @MartinNowack; Bheesham Persaud, @bheesham; Gu Zhengxiong, @NoviceLive; Cristian Cadar, @ccadar)
KLEE 1.0.0, 10 August 2015
==========================
# Recent changes (from 2015)
* Several performance improvements to the counterexample cache, including changing some default behaviour (Eric Rizzi, @holycrap872)
* Computing coverage of KLEE code in Travis CI (Timotej Kapus, @kren1)
* Added an option --readable-posix-inputs which is used to turn on/off the CEX preferences added in the POSIX model (Eric Rizzi, @holycrap872; Cristian Cadar, @ccadar)
* Lots of improvements to the build process (Dan Liew, @delcypher)
* Added klee-clang as alternative to klee-gcc (Martin Nowack, @MartinNowack)
* Added Dockerfile for building a KLEE Docker image (Dan Liew, @delcypher)
* Added a new option, --rewrite-equalities, which makes it possible to disable the optimisation that rewrites existing constraints when an equality with a constant is added (Cristian Cadar, @ccadar)
* Cleaner, more efficient timestamps (Emil Rakadjiev, @erakadjiev)
* Improved integer overflow detection (Luca Dariz, @luckyluke)