about summary refs log tree commit diff homepage
path: root/lib/Expr
AgeCommit message (Collapse)Author
2014-12-13Add a few line breaks to make the code more readable inDan Liew
ExprSMTLIBPrinter
2014-12-13Clean up some ExprSMTLIBPrinter code by using llvm_unreachableDan Liew
2014-12-13Clean up a few comments in ExprSMTLIBPrinterDan Liew
2014-12-12Print nested let-abbreviations in ExprSMTLIBPrinterRaimondas Sasnauskas
This patch introduces nested let-abbreviations in the ExprSMTLIBPrinter to reduce the size of the SMTLIBv2 queries and the corresponding processing time (bugfix for #170). The current implementation of the let abbreviation mode does not consider expression intra-dependencies and prints all abbreviations in the same let scope. For a (simplified) example, it prints (assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) ). This is extremely inefficient if the expressions (and there many of these!) extensively reuse their subexpressions. Therefore, it's better to print the query with nested let-expressions by reusing existing expression bindings in the new let scope: (assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) ). This patch adds a new function ExprSMTLIBPrinter::scanBindingExprDeps() that scans bindings for expression dependencies. The result is a vector of new bindings (orderedBindings) that represents the expression dependency tree. When printing in the let-abbreviation mode, the new code starts with abbreviating expressions that have no dependencies and then gradually makes these new bindings available in the upcoming let-scopes where expressions with dependencies reuse them. The effect of nested let-abbreviations is comparable to :named abbreviations. However, the latter mode is not supported by the majority of the solvers.
2014-12-02Fix typoDan Liew
2014-12-02Add a comment explaining why the query expr is being negated.Dan Liew
2014-12-02The printing of constraints and the QueryExpr have been merged into aDan Liew
single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-05-29Fix headerMartin Nowack
2014-05-29Avoid non-explicit use of functions from std namespace in KLEEMartin Nowack
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.
2014-05-11Fix the logic in ExprSMTLIBPrinter::getSortPeter Collingbourne
This now corresponds to the sorts of the operations we emit, as far as I can tell. Read is one example of an operation that now works correctly (with 1-bit array ranges). It's also possible (but not very useful, and I don't think KLEE can produce it) for other operations such as Add to operate on 1-bit values, and this patch also fixes those.
2014-04-24Asserting that update lists have non-NULL roots within ReadExpr objects (updateHristina Palikareva
lists can have NULL roots, e.g. in MemoryObject instances with concrete contents, where root is allocated lazily only when the updates are required). Also checking whether array updates are typed correctly in UpdateList::extend() rather than in the constructor of UpdateNode (only for update lists with non-NULL roots).
2014-04-16Removing a few more hard-coded values for domains and ranges of Array objectsHristina Palikareva
2014-04-04Add the ability to control whether the pretty printer uses line breaksPeter Collingbourne
This change makes it possible to more reliably write unit tests which check that an expression is equivalent to an expected pretty printed string.
2014-04-02Modify the SMT-LIB printer to declare arrays in a deterministic ↵Peter Collingbourne
(alphabetical) order.
2014-03-09Use clang-format to reformat SMT-LIB printer in LLVM style.Peter Collingbourne
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-12-06Deprecate LLVM 2.8 and lowerMartin Nowack
2013-09-21Merge pull request #17 from MartinNowack/LLVM33Cristian Cadar
Make KLEE compile with LLVM 2.3.
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-27Port to LLVM 3.3Martin Nowack
Major changes are: - Switching to llvm-link to build archive files - Use GetMallocUsage instead of GetTotalMemoryUsage (be aware of bug in LLVM 3.3 http://llvm.org/bugs/show_bug.cgi?id=16847) - intrinsic library functions like memcpy/mov/set use weak linkage to be replaced by e.g. uclibc functions - rewrote linking with library - enhanced MemoryLimit test case to check if mallocs were successful
2013-07-11Bug fix by Jonathan Neuschäfer: "Without this patchCristian Cadar
NotExpr::computeHash() will have a local variable with the name "hashValue" and assign the newly computed hash to that instead of the member variable with the same name that should be set by the computeHash method of every Expr subclass." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186102 91177308-0d34-0410-b5e6-96231b3b80d8
2013-05-08Patch by Dan Liew: "Renamed ExprSMTLIBPrinter method mangleQuery() to ↵Cristian Cadar
negateQueryExpression() to make it clear what it does." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181445 91177308-0d34-0410-b5e6-96231b3b80d8
2012-11-05Fixed a bug in Array::computeHash()Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@167382 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Nice patch by Dan Liew that adds support for printing queries in theCristian Cadar
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Moved PrintContext class out of ExprPrinter.cpp soCristian Cadar
it can be used by other classes. It has also been improved so it can be used with the soon to be added ExprSMTLIBPrinter classes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166555 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: " Modified ConstantExpr::toString() to take anCristian Cadar
optional radix (base e.g. 2,10,16). This will be needed by the ExprSMTLIBPrinter that will soon be added." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166553 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-18Nice patch by Hristina Palikareva that removes the dependency on STPCristian Cadar
arrays from the Array and UpdateNode classes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166214 91177308-0d34-0410-b5e6-96231b3b80d8
2012-04-07Catch up with hashing changes.Peter Collingbourne
Patch by arrowdodger! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154237 91177308-0d34-0410-b5e6-96231b3b80d8
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-24Applied patch by Leandro Sales that makes Kleaver compatible with theCristian Cadar
recent changes to array names. Modified FastCexSolver.pc to catch this issue. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135896 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-06-09Patch from Martin Nowack for LLVM 2.9Cristian Cadar
(http://llvm.org/bugs/show_bug.cgi?id=9595) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132787 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Maintain an equivalence set during comparison operationsPeter Collingbourne
This results in a significant speedup of certain comparisons involving large partially shared expression trees. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131585 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Support for arbitrary sized types in ConstantExpr::fromMemoryPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131583 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
2010-07-15Fix a -Wbool-conversion warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108404 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix some const cast warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102867 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Add long double support, patch by David Ramos.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 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-08-01Add Expr::dumpDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77802 91177308-0d34-0410-b5e6-96231b3b80d8
2009-07-28Move Machine constants into Context object, initialized based on the targetDaniel Dunbar
data. - This is the first step towards having KLEE be fully target independent, its not particularly beautiful but its expedient. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77306 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-10Updated the Not operation for constants. Added extra test case for this.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75282 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-27Start move to using APFloat (support long double).Daniel Dunbar
- Incomplete, still have to move some conversion operations. - Also, there isn't support yet for copying long double values to native memory. - Still, should be a monotonic improvement and we are no longer faking long double support. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74363 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-23 01:24:31 +0000