about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2009-06-10(Missed save) Move Array construction out of MemoryObject into ObjectState.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73163 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Move Array construction out of MemoryObject into ObjectState.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73162 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Change ExecutionState::symbolics to include both the MemoryObject and theDaniel Dunbar
symbolic Array. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73161 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Use Arrays instead of MemoryObject where possible.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73160 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Fix a bug in the logging solver which was printing the expression in aDaniel Dunbar
getInitialValues query in the wrong place. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73159 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Added a temporary driver to test the parser.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73155 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-10Changed expression nodes to be ExprHandle (instead of ExprHandle*), andCristian Cadar
added a quick hack to change Bison unions to structs. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73154 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Use env instead of hard coding python path.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73142 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-09Do not compile SMT parser by default. Removed automatically generatedCristian Cadar
parser files: We really don't want SVN to keep track of changes in these files while working on the parser. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73132 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Made expression nodes int the SMT parser be pointers to ExprHandle.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73131 91177308-0d34-0410-b5e6-96231b3b80d8
2009-06-09Add initial support for constant Arrays.Daniel Dunbar
- This doesn't actually start using them, it just attempts to update all clients to do the right thing in the presence of them. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73130 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-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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 12:52:34 +0000