-
Notifications
You must be signed in to change notification settings - Fork 7
/
NEWS
229 lines (208 loc) · 14.8 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
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)