about summary refs log tree commit diff homepage
path: root/lib/Expr/Parser.cpp
AgeCommit message (Collapse)Author
2023-03-30Prevent fallthrough warningDaniel Schemmel
2020-07-01Separate constraint set and constraint managerMartin Nowack
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr ↵Cristian Cadar
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2018-06-29Fix the final -Wimplicit-fallthrough warningDaniel Schemmel
2016-05-24Fixed bug #375 in Kleaver's parserAndrea Mattavelli
2015-12-18Fix a leak detected by ASan in the KQuery parser where on destruction ofDan Liew
the ``ParserImpl`` it wouldn't free allocated ``Identifier``s
2015-12-18Fix memory leaks of ``Array`` objects detected by ASan.Dan Liew
Some of these leaks were introduced by the factory constructor for Array objects (f049ff3bc04daead8c3bb9f06e89e71e2054c82a) but a few others have been around for far longer. This leak was fixed by introducing a ``ArrayCache`` object which has two purposes * Retains ownership of all created ``Array`` objects and destroys them when the ``ArrayCache`` destructor is called. * Mimic the caching behaviour for symbolic arrays that was introduced by f049ff3bc04daead8c3bb9f06e89e71e2054c82a where arrays with the same name and size get "uniqued". The Executor now maintains a ``arrayCache`` member that it uses and passes by pointer to objects that need to construct ``Array`` objects (i.e. ``ObjectState``). This way when the Executor is destroyed all the ``Array`` objects get freed which seems like the right time to do this. For Kleaver the ``ParserImpl`` has a ``TheArrayCache`` member that is used for building ``Array`` objects. This means that the Parser must live as long as the built expressions will be used otherwise we will have a use after free. I'm not sure this is the right design choice. It might be better to transfer ownership of the ``Array`` objects to the root ``Decl`` returned by the parser.
2015-02-27Improved some comments and fixed some formatting issues in the Array factory ↵Cristian Cadar
patch.
2015-02-22Added factory method for Arrays + hid constructors from outside callsEric Rizzi
The way that Arrays were handled in the past led to the possibility of aliasing issues. This occured whenever a new branch discovered an array for the first time. Each branch would create a new instance of the same array without seeing if it had been created before. Therefore, should a new branch encounter the same state as some previous branch, the previous branch's solution wouldn't satisfy the new state since they didn't recognize they were referencing the same array. By creating an array factory that creates a single symbolic array, that problem is handled. Note: Concrete arrays should not be created by the factory method since their values are never shared between branches. The factory works by seeing if an array with a similar hash has been created before (the hash is based on the name and size of array). If there has been it then searches through all of the arrays with the same hash (stored in a vector) to see if there is one with an exact match. If there is one, the address of this previously created equivalent array is returned. Otherwise, the newly created array is unique, it is added to the map, and it's address is returned. This aliasing issue can be seen by comparing the output of the Dogfood/ImmutableSet.cpp test cases with and with out this commit. Both act correctly, but the number of queries making it to the solver in the previous version is much greater 244 vs 211. This is because the UBTree in the CexCachingSolver and the cache in the CachingSolver do not recognize queries whose solutions were previously calculated because it doesn't think the arrays in the two queries are the same. While this does not cause an error, it does mean that extra calls are made.
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2011-10-17Fix some -Wunused-variable warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@142310 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
version codes. This makes the preprocessor-based version tests more concise and less error prone. Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext and trunc were introduced in LLVM 2.9); now 2.9 passes "make test". git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Patch by arrowdodger ↵Cristian Cadar
(http://keeda.stanford.edu/pipermail/klee-dev/2011-April/000617.html) for compiling KLEE with the latest LLVM changes. Tested against LLVM 2.7 and 2.8. The AsmAddresses test fails in 2.8 unless assertions are explicitely enabled (--enable-assertions). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130065 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-05Applied patch submitted by Pongsin Poosankam that fixes a bug in theCristian Cadar
parser. Fixed bug in the parses. Patch reported by git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@81056 91177308-0d34-0410-b5e6-96231b3b80d8
2009-09-01Update for LLVM ostream changes.Daniel Dunbar
- Includes patch by Michael Stone! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@80665 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-11Removed the Nz macro.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75377 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Added support for bitwise not. Replacing "false == " with Not inCristian Cadar
the canonical form. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75239 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-10Replaced createNot() by createIsZero() and "Not" macro by "Nz". Cristian Cadar
Not will become bitwise not. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75224 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-26More large integer support.Daniel Dunbar
- Allow constructing a ConstantExpr from an APInt, too painful otherwise. - Parser support for large integers. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74278 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14The expansion for Read{MSB,LSB} needs to continue to use the folding methods,Daniel Dunbar
otherwise we build expressions that won't be matched later when we print them. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73347 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Use ExprBuilder for constructing expressions in the Parser.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73345 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-14Add ConstantExpr::{getLimitedValue,getZExtValue}.Daniel Dunbar
- For use in situations where the range of the constant is known to fit in a uint64 (or smaller), or the extra bits don't matter. - No (intended) functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73326 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09More constant Array support.Daniel Dunbar
- The are parsed, printed, and solved now. - Remove some members of ArrayDecl which are only duplicates of Array members. - KLEE still doesn't create these, but you can write them by hand. The EXE style constant array optimization for STP (turning the initial writes into asserts) is now only a stones throw away, but I need to leave something fun to do tomorrow. :) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73133 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove Array::object.Daniel Dunbar
- The sole remaining client was IVC, which is currently disabled for other correctness issues. I patched it to compile and left a FIXME that we will have to resolve this before we can reenable IVC. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73129 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove Array::id.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73128 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Switch Array* print-outs to use name instead of ID, and update a fewDaniel Dunbar
constructors I missed. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73127 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Add Array::name field, initialized but not used for anything yet.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73125 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Kill off UpdateList::isRooted flag.Daniel Dunbar
- The right way to handle this is by using constant arrays, where the semantics are easier to define and implement. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73124 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Fix a mistake in previous commit to turn asserts -> parse errors.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73046 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Diagnose some more syntax errors instead of crashing.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73032 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Implement array declarations.Daniel Dunbar
- Printing current prints all declarations, and we allow redefinition, since the printer doesn't know what has already been printed. - Names don't print right yet, since the Array* object doesn't have the name. - Various things are unsupported. o Array domain/range must be w32/w8. o Concrete initializers for arrays are unsupported. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73026 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Make sure to make up a valid VersionResult on failures.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73019 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Eliminate anonymous versions.Daniel Dunbar
- For now, this means the isRooted flag for arrays isn't propogated to the kquery language. We should figure out how to do this, but allow anonymous versions isn't the right way. Also, improved the error on invalid writes a bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73018 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-06Document the KQuery language.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72997 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support the extended query command syntax.Daniel Dunbar
- There are two optional lists following the constraints and the query expression. The first is a list of expressions to give values for and the second is a list of arrays to provide values for. - Update ExprPPrinter to accept extra arguments to print these arguments. - Add Parser support. - Add more ArrayDecl support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72938 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Turn an assert into a parse failure.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72935 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05llvm::Casting support for Kleaver AST nodes.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72931 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Start removing uses of Expr::isConstant.Daniel Dunbar
- These should use cast<>, isa<>, or dyn_cast<> as appropriate (or better yet, changed to use ref<ConstantExpr> when the type is known). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72857 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Change ConstantExpr::{alloc,create} to return a ref<ConstantExpr>Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72853 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Fixed a bug in Kleaver's parser: APInt does not allow "truncation" toCristian Cadar
the same width. Added a test case that was previously triggering an assert violation. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72850 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Added a couple of tests for ReadLSB/MSB. Changed kleaver to write to stdout.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72841 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-04Move isConstant from ref<> to Expr::Daniel Dunbar
- Ref.h is now freestanding. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72824 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-03Kill off specialized ref<> forwarding methods, in the interest of making it aDaniel Dunbar
more standard reference counting wrapper. - The only interesting changes here are in Ref.h, everything else is just updating foo.method to use foo->method instead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72777 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-02Use ConstantExpr::alloc instead of ref<Expr> directlyDaniel Dunbar
- The "constant optimization" embedded inside ref<Expr> is going away. - No functionality change. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72730 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-28Small changes to silence some gcc warnings.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72518 91177308-0d34-0410-b5e6-96231b3b80d8
2009-05-21Initial KLEE checkin.Daniel Dunbar
- Lots more tweaks, documentation, and web page content is needed, but this should compile & work on OS X & Linux. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8