about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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-09Use Array* to map objects instead of id.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73126 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-09Remove unnecessary include.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73123 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Set svn:ignore on lib/SMT/{Debug,Release}Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73122 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Quick hack to build SMT LLVM style.Daniel Dunbar
- I don't want to make proper bison/flex rules, and eventually I think we should just check in the generated files since we don't expect them to change, so for now just build the files in the src directory. Eventually we will want to disable these rules so that it works for people who don't have bison/flex. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73121 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove exception.h and parser_exception.hDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73111 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Kill off uses of C++ exceptions.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73110 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove lang.h again.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73109 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Get rid of Parser language member, we only use SMTLIB.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73108 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Revert r73105, I think I was too hasty in killing this.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73107 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Fix a compiler warningDaniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73106 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Remove lang.h, it is unused.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73105 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Made the SMTLIB parser compile. Commented out most of the grammar inCristian Cadar
smtlib.y. Made a temporary functional Makefile that compiles the lex/bison generated files. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73064 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08More changes needed to make the SMTLIB parser compile.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73063 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Removed ValidityChecker field from ParserTemp. Temporarily replacedCristian Cadar
Expr with void* to quickly get some compilable parser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73062 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Removed support for the PL and Lisp languages.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73060 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Added CVC3's parser for the SMT-LIB grammar. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73059 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Start implementing exact value propogation.Daniel Dunbar
- So far this just propogates obvious equalities and reads. For example, FastCexSolver can now prove that: -- array arr219[3] : w32 -> w8 = symbolic (query [(Eq 235 N0:(Read w8 0 arr219))] (Eq 235 N0)) -- is valid. Even though this is very basic, it is good enough to solve ~50% of the valid queries on pcresymtest-[34].pc (total reduction in # of queries is ~25%). Unfortunately, this only gives a 1-2% speedup, which is disappointing, but there is a lot more we can do. I'm a little surprised the speedup is so low, this may be an indicator that there are some other things going on, for example perhaps the STP expr construction cost for arrays is very high, and we inevitably will end up paying this unless we solve so many queries that some arrays never ever make it to STP. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73058 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Add some query logs in utils/data/Queries (for 3 and 4 byte pcregrep)Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73057 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Stub out infrastructure for propogating exact values & provingDaniel Dunbar
validity. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73055 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Add exact value contents to CexObjectData.Daniel Dunbar
- The exact contents are a conservative approximation for the values of each array location, to be used for proving valid queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73054 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Rename forceExprTo* to propogatePossible*Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73053 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08FastCexSolver: Lazily initialize object values and kill off ObjectFinder class.Daniel Dunbar
Also, explicitly manage the object data to avoid copy overhead. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73051 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Kill off Concat::is[248]ByteConcat, and fix FastCexSolver for this case.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73049 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Add klee::createDummySolver, the dummy solver always fails.Daniel Dunbar
- Useful as an alternative backend to STP for testing. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73048 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-08Cleanup FastCexSolver:Daniel Dunbar
- Make CexObjectData members private. - Use std::vector instead of allocating memory by hand. - Factor out method which does the propogation from the various Solver routines. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73047 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-08kleaver: Use raw_ostream, and print some stats.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73045 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Make sure that ExprEvaluator will fold constant expressions (klee never createsDaniel Dunbar
these, but the parser can). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73033 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-07Fix typo.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73031 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Make sure to include arrays to be evaluated in the set of used arrays.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73030 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-07Don't delete decls before parsing is complete.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73023 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-07Update test case.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73020 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-05Fixed a division by zero triggered by straight-line code in klee-stats.Cristian Cadar
Added an error message when no directories are given. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72966 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Moved PrintStats.py to tool/klee-stats/Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72964 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Support counter example queries (at least, the restricted set that weDaniel Dunbar
use). - Arrays don't have sizes yet, so we don't get initial values correctly. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72939 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-05Add Expr::is{Zero,True,False} methods.Daniel Dunbar
- These are too convenient to live without. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72937 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-05Don't evaluate queries if there were parse failures.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72934 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-05Add evaluation support to kleaver (now the default).Daniel Dunbar
- Currently only handles validity queries. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72933 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-05Set svn:ignore properties.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72925 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 18:00:09 +0000