NEWS

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)