From 8bb0d17b366525458b45f50cde47b1c9ba0a05e3 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 1 Nov 2023 19:17:41 +0400 Subject: [PATCH 1/7] [feat] Add `OptimizeAggressive` option --- lib/Module/Optimize.cpp | 75 +++++++++++-------- ...r.3.ufo.UNBOUNDED.pals+Problem12_label00.c | 2 +- .../pals_floodmax.5.2.ufo.BOUNDED-10.pals.c | 2 +- .../2023-10-04-email_spec0_product16.cil.c | 2 +- ...ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c | 2 +- test/regression/2023-10-06-Dubois-015.c | 2 +- test/regression/2023-10-13-kbfiltr.i.cil-2.c | 2 +- test/regression/2023-10-16-CostasArray-17.c | 21 ++++-- 8 files changed, 64 insertions(+), 44 deletions(-) diff --git a/lib/Module/Optimize.cpp b/lib/Module/Optimize.cpp index cda430bd96..e087ed2208 100644 --- a/lib/Module/Optimize.cpp +++ b/lib/Module/Optimize.cpp @@ -79,6 +79,11 @@ static cl::opt DeleteDeadLoops("delete-dead-loops", cl::desc("Use LoopDeletionPass"), cl::init(true), cl::cat(klee::ModuleCat)); +static cl::opt + OptimizeAggressive("optimize-aggressive", + cl::desc("Use aggressive optimization passes"), + cl::init(true), cl::cat(klee::ModuleCat)); + // A utility function that adds a pass to the pass manager but will also add // a verifier pass after if we're supposed to verify. static inline void addPass(legacy::PassManager &PM, Pass *P) { @@ -149,43 +154,12 @@ static void AddStandardCompilePasses(legacy::PassManager &PM) { addPass(PM, createInstructionCombiningPass()); addPass(PM, createDeadStoreEliminationPass()); // Delete dead stores - addPass(PM, createAggressiveDCEPass()); // Delete dead instructions addPass(PM, createCFGSimplificationPass()); // Merge & remove BBs addPass(PM, createStripDeadPrototypesPass()); // Get rid of dead prototypes addPass(PM, createConstantMergePass()); // Merge dup global constants } -/// Optimize - Perform link time optimizations. This will run the scalar -/// optimizations, any loaded plugin-optimization modules, and then the -/// inter-procedural optimizations if applicable. -void Optimize(Module *M, llvm::ArrayRef preservedFunctions) { - - // Instantiate the pass manager to organize the passes. - legacy::PassManager Passes; - - // If we're verifying, start off with a verification pass. - if (VerifyEach) - Passes.add(createVerifierPass()); - - // DWD - Run the opt standard pass list as well. - AddStandardCompilePasses(Passes); - - // Now that composite has been compiled, scan through the module, looking - // for a main function. If main is defined, mark all other functions - // internal. - if (!DisableInternalize) { - auto PreserveFunctions = [=](const GlobalValue &GV) { - StringRef GVName = GV.getName(); - - for (const char *fun : preservedFunctions) - if (GVName.equals(fun)) - return true; - - return false; - }; - ModulePass *pass = createInternalizePass(PreserveFunctions); - addPass(Passes, pass); - } +static void AddNonStandardCompilePasses(legacy::PassManager &Passes) { // Propagate constants at call sites into the functions they call. This // opens opportunities for globalopt (and inlining) by substituting function @@ -257,6 +231,43 @@ void Optimize(Module *M, llvm::ArrayRef preservedFunctions) { addPass(Passes, createCFGSimplificationPass()); addPass(Passes, createAggressiveDCEPass()); addPass(Passes, createGlobalDCEPass()); +} + +/// Optimize - Perform link time optimizations. This will run the scalar +/// optimizations, any loaded plugin-optimization modules, and then the +/// inter-procedural optimizations if applicable. +void Optimize(Module *M, llvm::ArrayRef preservedFunctions) { + + // Instantiate the pass manager to organize the passes. + legacy::PassManager Passes; + + // If we're verifying, start off with a verification pass. + if (VerifyEach) + Passes.add(createVerifierPass()); + + // DWD - Run the opt standard pass list as well. + AddStandardCompilePasses(Passes); + + // Now that composite has been compiled, scan through the module, looking + // for a main function. If main is defined, mark all other functions + // internal. + if (!DisableInternalize) { + auto PreserveFunctions = [=](const GlobalValue &GV) { + StringRef GVName = GV.getName(); + + for (const char *fun : preservedFunctions) + if (GVName.equals(fun)) + return true; + + return false; + }; + ModulePass *pass = createInternalizePass(PreserveFunctions); + addPass(Passes, pass); + } + + if (OptimizeAggressive) { + AddNonStandardCompilePasses(Passes); + } // Run our queue of passes all at once now, efficiently. Passes.run(*M); diff --git a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index 7b90ea5b2d..0c49afc42e 100644 --- a/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,7 +1,7 @@ // REQUIRES: geq-llvm-14.0 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=true --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc // RUN: %klee-stats --print-columns 'BCov(%)' --table-format=csv %t.klee-out > %t.stats // RUN: FileCheck -input-file=%t.stats %s diff --git a/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c index 4dd74f1d3c..4341173c1d 100644 --- a/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c +++ b/test/Solver/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3-tree --max-solvers-approx-tree-inc=16 -max-memory=6008 --optimize --skip-not-lazy-initialized -output-source=false --output-stats=false --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error -dump-states-on-halt=true -exit-on-error-type=Assert --search=dfs -max-instructions=6000 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3-tree --max-solvers-approx-tree-inc=16 --optimize-aggressive=false --track-coverage=branches -max-memory=6008 --optimize --skip-not-lazy-initialized -output-source=false --output-stats=false --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error -dump-states-on-halt=true -exit-on-error-type=Assert --search=dfs -max-instructions=6000 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s // CHECK-VERDICT: KLEE: done: total instructions = 6000 #include "klee-test-comp.c" diff --git a/test/regression/2023-10-04-email_spec0_product16.cil.c b/test/regression/2023-10-04-email_spec0_product16.cil.c index e407b7bbb2..291d48229c 100644 --- a/test/regression/2023-10-04-email_spec0_product16.cil.c +++ b/test/regression/2023-10-04-email_spec0_product16.cil.c @@ -1,6 +1,6 @@ // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --istats-write-interval=90s --exit-on-error-type=Assert --search=dfs --max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --optimize-aggressive=false --track-coverage=branches --max-memory=6008 --optimize --skip-not-lazy-initialized --istats-write-interval=90s --exit-on-error-type=Assert --search=dfs --max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s // RUN find %t.klee-out -type f -name "*.assert.err" | sed 's/assert\.err/ktest/' | xargs %ktest-tool | FileCheck -check-prefix=CHECK-TEST %s // CHECK-TEST-NOT: object 20 diff --git a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index d08c61d74a..25d674dcb7 100644 --- a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -1,6 +1,6 @@ // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s #include "klee-test-comp.c" diff --git a/test/regression/2023-10-06-Dubois-015.c b/test/regression/2023-10-06-Dubois-015.c index fccb9acd93..c782d694b5 100644 --- a/test/regression/2023-10-06-Dubois-015.c +++ b/test/regression/2023-10-06-Dubois-015.c @@ -1,6 +1,6 @@ // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s #include "klee-test-comp.c" diff --git a/test/regression/2023-10-13-kbfiltr.i.cil-2.c b/test/regression/2023-10-13-kbfiltr.i.cil-2.c index 8a3d658124..d46b853526 100644 --- a/test/regression/2023-10-13-kbfiltr.i.cil-2.c +++ b/test/regression/2023-10-13-kbfiltr.i.cil-2.c @@ -1,7 +1,7 @@ // REQUIRES: geq-llvm-14.0 // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize=true --mock-all-externals --external-calls=all --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=true --emit-all-errors=true --search=bfs %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --mock-all-externals --external-calls=all --use-forked-solver=false --max-memory=6008 --skip-not-lazy-initialized --istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --write-kqueries --write-xml-tests --only-output-states-covering-new=true --dump-states-on-halt=true --emit-all-errors=true --search=bfs %t1.bc // RUN: test -f %t.klee-out/test000023_1.xml #include "klee-test-comp.c" diff --git a/test/regression/2023-10-16-CostasArray-17.c b/test/regression/2023-10-16-CostasArray-17.c index 0321c71828..ed1651a15d 100644 --- a/test/regression/2023-10-16-CostasArray-17.c +++ b/test/regression/2023-10-16-CostasArray-17.c @@ -1,12 +1,21 @@ // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc -// RUN: %klee-stats --print-columns 'ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats -// RUN: FileCheck -input-file=%t.stats %s +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc +// RUN: %klee-stats --print-columns ' Branches,ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck --input-file=%t.stats --check-prefix=CHECK-AGGRESSIVE %s -// Branch coverage 100%, and instruction coverage is very small: -// CHECK: ICov(%),BCov(%) -// CHECK-NEXT: {{(0\.[0-9][0-9])}},100.00 +// Branch coverage 100%, the number of branches is 1: +// CHECK-AGGRESSIVE: Branches,ICov(%),BCov(%) +// CHECK-AGGRESSIVE-NEXT: 1,{{(0\.[0-9][0-9])}},100.00 + +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=true --search=dfs %t1.bc +// RUN: %klee-stats --print-columns ' Branches,ICov(%),BCov(%)' --table-format=csv %t.klee-out > %t.stats +// RUN: FileCheck --input-file=%t.stats --check-prefix=CHECK-NOT-AGGRESSIVE %s + +// Branch coverage 50%, but the number of branches is 2: +// CHECK-NOT-AGGRESSIVE: Branches,ICov(%),BCov(%) +// CHECK-NOT-AGGRESSIVE-NEXT: 2,{{(0\.[0-9][0-9])}},50.00 #include "klee-test-comp.c" From 1aabb063f44bea8fdf9a7b96818cf4193c9240a9 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:15:39 +0400 Subject: [PATCH 2/7] [feat] Getting the performance/memory consumption balance in `DisjointSetUnion` --- include/klee/ADT/DisjointSetUnion.h | 48 ++++++++++--------- include/klee/ADT/Either.h | 23 ++++++++- .../klee/Expr/IndependentConstraintSetUnion.h | 4 +- include/klee/Expr/IndependentSet.h | 16 ++++++- include/klee/Expr/Symcrete.h | 2 + lib/Expr/IndependentConstraintSetUnion.cpp | 14 +++--- 6 files changed, 73 insertions(+), 34 deletions(-) diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h index b479ca0765..41c1a0296b 100644 --- a/include/klee/ADT/DisjointSetUnion.h +++ b/include/klee/ADT/DisjointSetUnion.h @@ -24,21 +24,29 @@ namespace klee { using ExprEitherSymcrete = either; template , + typename PRED = std::equal_to, typename CMP = std::less> class DisjointSetUnion { +public: + using internal_storage_ty = std::unordered_set; + using disjoint_sets_ty = + std::unordered_map, HASH, PRED>; + using iterator = typename internal_storage_ty::iterator; + protected: - PersistentMap parent; - PersistentSet roots; - PersistentMap rank; + std::unordered_map parent; + std::set roots; + std::unordered_map rank; - PersistentSet internalStorage; - PersistentMap, CMP> disjointSets; + std::unordered_set internalStorage; + std::unordered_map, HASH, PRED> disjointSets; ValueType find(const ValueType &v) { // findparent assert(parent.find(v) != parent.end()); if (v == parent.at(v)) return v; - parent.replace({v, find(parent.at(v))}); + parent.insert_or_assign(v, find(parent.at(v))); return parent.at(v); } @@ -60,15 +68,15 @@ class DisjointSetUnion { if (rank.at(a) < rank.at(b)) { std::swap(a, b); } - parent.replace({b, a}); + parent.insert_or_assign(b, a); if (rank.at(a) == rank.at(b)) { - rank.replace({a, rank.at(a) + 1}); + rank.insert_or_assign(a, rank.at(a) + 1); } - roots.remove(b); - disjointSets.replace( - {a, SetType::merge(disjointSets.at(a), disjointSets.at(b))}); - disjointSets.remove(b); + roots.erase(b); + disjointSets.insert_or_assign( + a, SetType::merge(disjointSets.at(a), disjointSets.at(b))); + disjointSets.erase(b); } bool areJoined(const ValueType &i, const ValueType &j) const { @@ -76,10 +84,6 @@ class DisjointSetUnion { } public: - using internalStorage_ty = PersistentSet; - using disjointSets_ty = ImmutableMap, CMP>; - using iterator = typename internalStorage_ty::iterator; - iterator begin() const { return internalStorage.begin(); } iterator end() const { return internalStorage.end(); } @@ -107,7 +111,7 @@ class DisjointSetUnion { disjointSets.insert({value, new SetType(value)}); internalStorage.insert(value); - internalStorage_ty oldRoots = roots; + std::set oldRoots = roots; for (ValueType v : oldRoots) { if (!areJoined(v, value) && SetType::intersects(disjointSets.at(find(v)), @@ -122,8 +126,8 @@ class DisjointSetUnion { } void add(const DisjointSetUnion &b) { - internalStorage_ty oldRoots = roots; - internalStorage_ty newRoots = b.roots; + std::set oldRoots = roots; + std::set newRoots = b.roots; for (auto it : b.parent) { parent.insert(it); } @@ -152,16 +156,16 @@ class DisjointSetUnion { DisjointSetUnion() {} - DisjointSetUnion(const internalStorage_ty &is) { + DisjointSetUnion(const internal_storage_ty &is) { for (ValueType v : is) { addValue(v); } } public: - internalStorage_ty is() const { return internalStorage; } + internal_storage_ty is() const { return internalStorage; } - disjointSets_ty ds() const { return disjointSets; } + disjoint_sets_ty ds() const { return disjointSets; } }; } // namespace klee diff --git a/include/klee/ADT/Either.h b/include/klee/ADT/Either.h index cc01bf761e..81b2d8e51c 100644 --- a/include/klee/ADT/Either.h +++ b/include/klee/ADT/Either.h @@ -32,6 +32,9 @@ template class either { /// @brief Required by klee::ref-managed objects class ReferenceCounter _refCount; + unsigned hashValue; + + static const unsigned MAGIC_HASH_CONSTANT = 39; public: using left = either_left; @@ -46,6 +49,8 @@ template class either { // virtual unsigned hash() = 0; virtual int compare(const either &b) = 0; virtual bool equals(const either &b) = 0; + + unsigned hash() const { return hashValue; } }; template class either_left : public either { @@ -56,8 +61,15 @@ template class either_left : public either { private: ref value_; + unsigned computeHash() { + unsigned res = (unsigned)getKind(); + res = (res * either::MAGIC_HASH_CONSTANT) + value_->hash(); + either::hashValue = res; + return either::hashValue; + } + public: - either_left(ref leftValue) : value_(leftValue){}; + either_left(ref leftValue) : value_(leftValue) { computeHash(); }; ref value() const { return value_; } operator ref const() { return value_; } @@ -100,8 +112,15 @@ template class either_right : public either { private: ref value_; + unsigned computeHash() { + unsigned res = (unsigned)getKind(); + res = (res * either::MAGIC_HASH_CONSTANT) + value_->hash(); + either::hashValue = res; + return either::hashValue; + } + public: - either_right(ref rightValue) : value_(rightValue){}; + either_right(ref rightValue) : value_(rightValue) { computeHash(); }; ref value() const { return value_; } operator ref const() { return value_; } diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h index 4ec9e11c5a..3d6eb0f14c 100644 --- a/include/klee/Expr/IndependentConstraintSetUnion.h +++ b/include/klee/Expr/IndependentConstraintSetUnion.h @@ -8,8 +8,8 @@ namespace klee { class IndependentConstraintSetUnion - : public DisjointSetUnion, - IndependentConstraintSet> { + : public DisjointSetUnion, IndependentConstraintSet, + ExprEitherSymcreteHash, ExprEitherSymcreteCmp> { public: Assignment concretization; diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index a0878ea6c2..c1c69f2f72 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -24,6 +24,19 @@ DISABLE_WARNING_POP namespace klee { using ExprEitherSymcrete = either; +struct ExprEitherSymcreteHash { + unsigned operator()(const ref &e) const { + return e->hash(); + } +}; + +struct ExprEitherSymcreteCmp { + bool operator()(const ref &a, + const ref &b) const { + return a == b; + } +}; + template class DenseSet { typedef std::set set_ty; set_ty s; @@ -87,7 +100,8 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, class IndependentConstraintSet { private: using InnerSetUnion = - DisjointSetUnion, IndependentConstraintSet>; + DisjointSetUnion, IndependentConstraintSet, + ExprEitherSymcreteHash, ExprEitherSymcreteCmp>; void initIndependentConstraintSet(ref e); void initIndependentConstraintSet(ref s); diff --git a/include/klee/Expr/Symcrete.h b/include/klee/Expr/Symcrete.h index 6646c4cf16..65b70b20f7 100644 --- a/include/klee/Expr/Symcrete.h +++ b/include/klee/Expr/Symcrete.h @@ -75,6 +75,8 @@ class Symcrete { return id < rhs.id ? -1 : 1; } + unsigned hash() { return id; } + bool operator<(const Symcrete &rhs) const { return compare(rhs) < 0; }; }; diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp index 01358e2623..0dcbf7154b 100644 --- a/lib/Expr/IndependentConstraintSetUnion.cpp +++ b/lib/Expr/IndependentConstraintSetUnion.cpp @@ -21,13 +21,13 @@ IndependentConstraintSetUnion::IndependentConstraintSetUnion( auto exprs = ics->exprs; for (ref e : exprs) { auto v = ref(new ExprEitherSymcrete::left(e)); - rank.replace({v, 0}); + rank.insert_or_assign(v, 0); internalStorage.insert(v); } for (ref s : ics->symcretes) { auto v = ref(new ExprEitherSymcrete::right(s)); - rank.replace({v, 0}); + rank.insert_or_assign(v, 0); internalStorage.insert(v); } @@ -37,11 +37,11 @@ IndependentConstraintSetUnion::IndependentConstraintSetUnion( auto &first = *(internalStorage.begin()); for (auto &e : internalStorage) { - parent.replace({e, first}); + parent.insert_or_assign(e, first); } - rank.replace({first, 1}); + rank.insert_or_assign(first, 1); roots.insert(first); - disjointSets.replace({first, ics}); + disjointSets.insert_or_assign(first, ics); concretization = ics->concretization; } @@ -57,7 +57,7 @@ void IndependentConstraintSetUnion::updateConcretization( ref ics = disjointSets.at(e); Assignment part = delta.part(ics->getSymcretes()); ics = ics->updateConcretization(part, concretizedExprs); - disjointSets.replace({e, ics}); + disjointSets.insert_or_assign(e, ics); } for (auto &it : delta.bindings) { concretization.bindings.replace({it.first, it.second}); @@ -70,7 +70,7 @@ void IndependentConstraintSetUnion::removeConcretization( ref ics = disjointSets.at(e); Assignment part = remove.part(ics->getSymcretes()); ics = ics->removeConcretization(part, concretizedExprs); - disjointSets.replace({e, ics}); + disjointSets.insert_or_assign(e, ics); } for (auto &it : remove.bindings) { concretization.bindings.remove(it.first); From 4721b35d6c65745cab9ac821888730e1beb70e58 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:17:59 +0400 Subject: [PATCH 3/7] [fix] Fix performance for unbalanced expressions --- include/klee/Expr/Expr.h | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index 4646b1a3c8..9937999e2e 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -753,7 +753,14 @@ class SelectExpr : public NonConstantExpr { static ref create(ref c, ref t, ref f); - Width getWidth() const { return trueExpr->getWidth(); } + Width getWidth() const { + if (trueExpr->height() < falseExpr->height()) { + return trueExpr->getWidth(); + } else { + return falseExpr->getWidth(); + } + } + Kind getKind() const { return Select; } unsigned getNumKids() const { return numKids; } @@ -1093,7 +1100,6 @@ FP_CAST_EXPR_CLASS(SIToFP) return createCachedExpr(res); \ } \ static ref create(const ref &l, const ref &r); \ - Width getWidth() const { return left->getWidth(); } \ Kind getKind() const { return _class_kind; } \ virtual ref rebuild(ref kids[]) const { \ return create(kids[0], kids[1]); \ @@ -1103,6 +1109,13 @@ FP_CAST_EXPR_CLASS(SIToFP) return E->getKind() == Expr::_class_kind; \ } \ static bool classof(const _class_kind##Expr *) { return true; } \ + Width getWidth() const { \ + if (left->height() < right->height()) { \ + return left->getWidth(); \ + } else { \ + return right->getWidth(); \ + } \ + } \ \ protected: \ virtual int compareContents(const Expr &b) const { \ @@ -1145,7 +1158,14 @@ ARITHMETIC_EXPR_CLASS(AShr) } \ static ref create(const ref &l, const ref &r, \ llvm::APFloat::roundingMode rm); \ - Width getWidth() const { return left->getWidth(); } \ + Width getWidth() const { \ + if (left->height() < right->height()) { \ + return left->getWidth(); \ + } else { \ + return right->getWidth(); \ + } \ + } \ + \ Kind getKind() const { return _class_kind; } \ virtual ref rebuild(ref kids[]) const { \ return create(kids[0], kids[1], roundingMode); \ From ba4db1b62661f16b971f4c3a312eeb1dc3a98b2d Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:27:08 +0400 Subject: [PATCH 4/7] [refactor] Separate `isStuck` and `isCycled`, `isStuck` is smarter now --- .../klee/{util => Utilities}/APFloatEval.h | 0 include/klee/Utilities/Math.h | 32 +++++++++++++++++++ lib/Core/ExecutionState.h | 9 +++++- lib/Core/Searcher.cpp | 21 +++--------- lib/Core/TargetManager.cpp | 2 +- lib/Expr/APFloatEval.cpp | 2 +- lib/Expr/Expr.cpp | 2 +- 7 files changed, 47 insertions(+), 21 deletions(-) rename include/klee/{util => Utilities}/APFloatEval.h (100%) create mode 100644 include/klee/Utilities/Math.h diff --git a/include/klee/util/APFloatEval.h b/include/klee/Utilities/APFloatEval.h similarity index 100% rename from include/klee/util/APFloatEval.h rename to include/klee/Utilities/APFloatEval.h diff --git a/include/klee/Utilities/Math.h b/include/klee/Utilities/Math.h new file mode 100644 index 0000000000..a7739cadc6 --- /dev/null +++ b/include/klee/Utilities/Math.h @@ -0,0 +1,32 @@ +//===-- Math.h --------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_MATH_H +#define KLEE_MATH_H + +#include + +namespace klee { +namespace util { +static unsigned int ulog2(unsigned int val) { + if (val == 0) + return UINT_MAX; + if (val == 1) + return 0; + unsigned int ret = 0; + while (val > 1) { + val >>= 1; + ret++; + } + return ret; +} +} // namespace util +} // namespace klee + +#endif /* KLEE_MATH_H */ diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index d10afb7072..58fb0f7881 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -29,6 +29,7 @@ #include "klee/Module/TargetHash.h" #include "klee/Solver/Solver.h" #include "klee/System/Time.h" +#include "klee/Utilities/Math.h" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH @@ -492,7 +493,7 @@ class ExecutionState { bool reachedTarget(ref target) const; static std::uint32_t getLastID() { return nextID - 1; }; - inline bool isStuck(unsigned long long bound) const { + inline bool isCycled(unsigned long long bound) const { if (bound == 0) return false; if (prevPC->inst->isTerminator() && stack.size() > 0) { @@ -508,6 +509,12 @@ class ExecutionState { return false; } + inline bool isStuck(unsigned long long bound) const { + if (depth == 1) + return false; + return isCycled(bound) && depth > klee::util::ulog2(bound); + } + bool isCoveredNew() const { return !coveredNew.empty() && coveredNew.back()->value; } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index ad73527320..7611b14c45 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -25,6 +25,7 @@ #include "klee/Statistics/Statistics.h" #include "klee/Support/ErrorHandling.h" #include "klee/System/Time.h" +#include "klee/Utilities/Math.h" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH @@ -136,21 +137,6 @@ void RandomSearcher::printName(llvm::raw_ostream &os) { /// -static unsigned int ulog2(unsigned int val) { - if (val == 0) - return UINT_MAX; - if (val == 1) - return 0; - unsigned int ret = 0; - while (val > 1) { - val >>= 1; - ret++; - } - return ret; -} - -/// - TargetedSearcher::~TargetedSearcher() {} bool TargetedSearcher::empty() { return states->empty(); } @@ -195,7 +181,8 @@ weight_type TargetedSearcher::getWeight(ExecutionState *es) { return weight; } auto distRes = distanceCalculator.getDistance(*es, target->getBlock()); - weight = ulog2(distRes.weight + es->steppedMemoryInstructions + 1); // [0, 32) + weight = klee::util::ulog2(distRes.weight + es->steppedMemoryInstructions + + 1); // [0, 32) if (!distRes.isInsideFunction) { weight += 32; // [32, 64) } @@ -667,7 +654,7 @@ class MaxCyclesMetric final : public IterativeDeepeningSearcher::Metric { explicit MaxCyclesMetric() : MaxCyclesMetric(1ULL){}; bool exceeds(const ExecutionState &state) const final { - return state.isStuck(maxCycles); + return state.isCycled(maxCycles); } void increaseLimit() final { maxCycles *= 2ULL; diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 9dcaedcd86..23ad1347e8 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -135,7 +135,7 @@ void TargetManager::updateReached(ExecutionState &state) { void TargetManager::updateTargets(ExecutionState &state) { if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { + if (targets(state).empty() && state.isCycled(MaxCyclesBeforeStuck)) { state.setTargeted(true); } if (isTargeted(state) && targets(state).empty()) { diff --git a/lib/Expr/APFloatEval.cpp b/lib/Expr/APFloatEval.cpp index a1f49b28f9..49ae758d1c 100644 --- a/lib/Expr/APFloatEval.cpp +++ b/lib/Expr/APFloatEval.cpp @@ -6,7 +6,7 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/APFloatEval.h" +#include "klee/Utilities/APFloatEval.h" #include "klee/Config/Version.h" #include "klee/Support/CompilerWarning.h" diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 4f26cb1aaa..ec1ecd9235 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -16,7 +16,7 @@ #include "klee/Support/ErrorHandling.h" #include "klee/Support/OptionCategories.h" #include "klee/Support/RoundingModeUtil.h" -#include "klee/util/APFloatEval.h" +#include "klee/Utilities/APFloatEval.h" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH From 112f71bdd46e1ecf89820651d1351e13a23d000c Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:53:46 +0400 Subject: [PATCH 5/7] [fix] Limit the cexPreferences size --- lib/Core/Executor.cpp | 46 ++++++++++++++++++++++++------------------- lib/Core/Searcher.cpp | 2 +- 2 files changed, 27 insertions(+), 21 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0cc740787b..46462e235b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -7151,26 +7151,32 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { // the preferred constraints. See test/Features/PreferCex.c for // an example) While this process can be very expensive, it can // also make understanding individual test cases much easier. - for (auto &pi : state.cexPreferences) { - bool mustBeTrue; - // Attempt to bound byte to constraints held in cexPreferences - bool success = - solver->mustBeTrue(extendedConstraints.cs(), Expr::createIsZero(pi), - mustBeTrue, state.queryMetaData); - // If it isn't possible to add the condition without making the entire - // list UNSAT, then just continue to the next condition - if (!success) - break; - // If the particular constraint operated on in this iteration through - // the loop isn't implied then add it to the list of constraints. - if (!mustBeTrue) { - Assignment concretization = computeConcretization( - extendedConstraints.cs(), pi, state.queryMetaData); - - if (!concretization.isEmpty()) { - extendedConstraints.addConstraint(pi, concretization); - } else { - extendedConstraints.addConstraint(pi, {}); + const size_t cexPreferencesBound = 16; + if (state.cexPreferences.size() > cexPreferencesBound) { + klee_warning_once(0, "skipping cex preffering (size of restrictons > %d).", + cexPreferencesBound); + } else { + for (auto &pi : state.cexPreferences) { + bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences + bool success = + solver->mustBeTrue(extendedConstraints.cs(), Expr::createIsZero(pi), + mustBeTrue, state.queryMetaData); + // If it isn't possible to add the condition without making the entire + // list UNSAT, then just continue to the next condition + if (!success) + break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. + if (!mustBeTrue) { + Assignment concretization = computeConcretization( + extendedConstraints.cs(), pi, state.queryMetaData); + + if (!concretization.isEmpty()) { + extendedConstraints.addConstraint(pi, concretization); + } else { + extendedConstraints.addConstraint(pi, {}); + } } } } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 7611b14c45..f2d91cfd79 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -714,7 +714,7 @@ void IterativeDeepeningSearcher::update(ExecutionState *current, } // no states left in underlying searcher: fill with paused states - if (baseSearcher->empty()) { + if (baseSearcher->empty() && !pausedStates.empty()) { metric->increaseLimit(); baseSearcher->update(nullptr, pausedStates, {}); pausedStates.clear(); From 8585d34bb5fd2c1086203bffe82e11327bab2f26 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:57:38 +0400 Subject: [PATCH 6/7] [fix] Remove unused field --- include/klee/Module/TargetHash.h | 5 ----- lib/Core/ExecutionState.cpp | 13 +++++-------- lib/Core/ExecutionState.h | 1 - lib/Core/TargetCalculator.h | 2 -- lib/Module/TargetHash.cpp | 5 ----- 5 files changed, 5 insertions(+), 21 deletions(-) diff --git a/include/klee/Module/TargetHash.h b/include/klee/Module/TargetHash.h index 2c2c2f81bd..1962ba906c 100644 --- a/include/klee/Module/TargetHash.h +++ b/include/klee/Module/TargetHash.h @@ -31,13 +31,8 @@ struct TargetCmp { bool operator()(const ref &a, const ref &b) const; }; -typedef std::pair Transition; typedef std::pair Branch; -struct TransitionHash { - std::size_t operator()(const Transition &p) const; -}; - struct BranchHash { std::size_t operator()(const Branch &p) const; }; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9b7667ee62..31d60372dd 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -160,11 +160,11 @@ ExecutionState::ExecutionState(const ExecutionState &state) : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC), stack(state.stack), stackBalance(state.stackBalance), incomingBBIndex(state.incomingBBIndex), depth(state.depth), - level(state.level), transitionLevel(state.transitionLevel), - addressSpace(state.addressSpace), constraints(state.constraints), - targetForest(state.targetForest), pathOS(state.pathOS), - symPathOS(state.symPathOS), coveredLines(state.coveredLines), - symbolics(state.symbolics), resolvedPointers(state.resolvedPointers), + level(state.level), addressSpace(state.addressSpace), + constraints(state.constraints), targetForest(state.targetForest), + pathOS(state.pathOS), symPathOS(state.symPathOS), + coveredLines(state.coveredLines), symbolics(state.symbolics), + resolvedPointers(state.resolvedPointers), cexPreferences(state.cexPreferences), arrayNames(state.arrayNames), steppedInstructions(state.steppedInstructions), steppedMemoryInstructions(state.steppedMemoryInstructions), @@ -448,9 +448,6 @@ void ExecutionState::increaseLevel() { stack.infoStack().back().multilevel.replace({srcbb, srcLevel + 1}); level.insert(prevPC->parent); } - if (srcbb != dstbb) { - transitionLevel.insert(std::make_pair(srcbb, dstbb)); - } } bool ExecutionState::isGEPExpr(ref expr) const { diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 58fb0f7881..5ebcf17a74 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -291,7 +291,6 @@ class ExecutionState { /// @brief Exploration level, i.e., number of times KLEE cycled for this state std::set level; - std::unordered_set transitionLevel; /// @brief Address space used by this state (e.g. Global and Heap) AddressSpace addressSpace; diff --git a/lib/Core/TargetCalculator.h b/lib/Core/TargetCalculator.h index cd96306524..f337b879fd 100644 --- a/lib/Core/TargetCalculator.h +++ b/lib/Core/TargetCalculator.h @@ -34,7 +34,6 @@ DISABLE_WARNING_POP namespace klee { class CodeGraphInfo; class ExecutionState; -struct TransitionHash; enum class TrackCoverageBy { None, Blocks, Branches, All }; @@ -44,7 +43,6 @@ class TargetCalculator { using StatesSet = std::unordered_set; typedef std::unordered_set VisitedBlocks; - typedef std::unordered_set VisitedTransitions; typedef std::unordered_set VisitedBranches; enum HistoryKind { Blocks, Transitions }; diff --git a/lib/Module/TargetHash.cpp b/lib/Module/TargetHash.cpp index 7f5b9be2eb..f7c3010689 100644 --- a/lib/Module/TargetHash.cpp +++ b/lib/Module/TargetHash.cpp @@ -22,11 +22,6 @@ bool TargetCmp::operator()(const ref &a, const ref &b) const { return a == b; } -std::size_t TransitionHash::operator()(const Transition &p) const { - return reinterpret_cast(p.first) * 31 + - reinterpret_cast(p.second); -} - std::size_t BranchHash::operator()(const Branch &p) const { return reinterpret_cast(p.first) * 31 + p.second; } From d1370f72f1eb5863b53a432dc8356013be82a04b Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Thu, 2 Nov 2023 05:58:52 +0400 Subject: [PATCH 7/7] [fix] Fix memory consumption `using path_ty = std::vector` -> `using path_ty = ImmutableList` --- include/klee/ADT/ImmutableList.h | 17 ++++++++ include/klee/Expr/Constraints.h | 3 +- include/klee/Expr/Path.h | 24 ++--------- lib/Core/ExecutionState.h | 2 +- lib/Expr/Constraints.cpp | 31 ++------------ lib/Expr/Path.cpp | 72 ++++---------------------------- 6 files changed, 35 insertions(+), 114 deletions(-) diff --git a/include/klee/ADT/ImmutableList.h b/include/klee/ADT/ImmutableList.h index 20cb225fd8..425036979e 100644 --- a/include/klee/ADT/ImmutableList.h +++ b/include/klee/ADT/ImmutableList.h @@ -10,6 +10,7 @@ #ifndef KLEE_IMMUTABLELIST_H #define KLEE_IMMUTABLELIST_H +#include #include #include @@ -96,6 +97,22 @@ template class ImmutableList { node->values.push_back(std::move(value)); } + void push_back(const T &value) { + if (!node) { + node = std::make_shared(); + } + node->values.push_back(value); + } + + bool empty() { return size() == 0; } + + const T &back() { + assert(node && "requiers not empty list"); + auto it = iterator(node.get()); + it.get = size() - 1; + return *it; + } + ImmutableList() : node(){}; ImmutableList(const ImmutableList &il) : node(std::make_shared(il)) {} diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index d6f47e3d94..75769b3fb4 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -12,6 +12,7 @@ #include "klee/ADT/Ref.h" +#include "klee/ADT/PersistentMap.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" @@ -91,7 +92,7 @@ class ConstraintSet { class PathConstraints { public: using ordered_constraints_ty = - std::map; + PersistentMap; void advancePath(KInstruction *ki); void advancePath(const Path &path); diff --git a/include/klee/Expr/Path.h b/include/klee/Expr/Path.h index 48bb63ec47..a556a00213 100644 --- a/include/klee/Expr/Path.h +++ b/include/klee/Expr/Path.h @@ -1,6 +1,8 @@ #ifndef KLEE_PATH_H #define KLEE_PATH_H +#include "klee/ADT/ImmutableList.h" + #include #include #include @@ -16,7 +18,7 @@ using stackframe_ty = std::pair; class Path { public: - using path_ty = std::vector; + using path_ty = ImmutableList; enum class TransitionKind { StepInto, StepOut, None }; struct PathIndex { @@ -38,23 +40,6 @@ class Path { void advance(KInstruction *ki); - friend bool operator==(const Path &lhs, const Path &rhs) { - return lhs.KBlocks == rhs.KBlocks && - lhs.firstInstruction == rhs.firstInstruction && - lhs.lastInstruction == rhs.lastInstruction; - } - friend bool operator!=(const Path &lhs, const Path &rhs) { - return !(lhs == rhs); - } - - friend bool operator<(const Path &lhs, const Path &rhs) { - return lhs.KBlocks < rhs.KBlocks || - (lhs.KBlocks == rhs.KBlocks && - (lhs.firstInstruction < rhs.firstInstruction || - (lhs.firstInstruction == rhs.firstInstruction && - lhs.lastInstruction < rhs.lastInstruction))); - } - unsigned KBlockSize() const; const path_ty &getBlocks() const; unsigned getFirstIndex() const; @@ -64,7 +49,6 @@ class Path { std::vector getStack(bool reversed) const; - std::vector> asFunctionRanges() const; std::string toString() const; static Path concat(const Path &l, const Path &r); @@ -73,7 +57,7 @@ class Path { Path() = default; - Path(unsigned firstInstruction, std::vector kblocks, + Path(unsigned firstInstruction, const path_ty &kblocks, unsigned lastInstruction) : KBlocks(kblocks), firstInstruction(firstInstruction), lastInstruction(lastInstruction) {} diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 5ebcf17a74..7ae7d692cb 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -290,7 +290,7 @@ class ExecutionState { std::uint32_t depth = 0; /// @brief Exploration level, i.e., number of times KLEE cycled for this state - std::set level; + PersistentSet level; /// @brief Address space used by this state (e.g. Global and Heap) AddressSpace addressSpace; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index ae00a3303c..d349c9d0b2 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -330,10 +330,6 @@ PathConstraints::orderedCS() const { void PathConstraints::advancePath(KInstruction *ki) { _path.advance(ki); } -void PathConstraints::advancePath(const Path &path) { - _path = Path::concat(_path, path); -} - ExprHashSet PathConstraints::addConstraint(ref e, const Assignment &delta, Path::PathIndex currIndex) { auto expr = Simplificator::simplifyExpr(constraints, e); @@ -352,7 +348,9 @@ ExprHashSet PathConstraints::addConstraint(ref e, const Assignment &delta, added.insert(expr); pathIndexes.insert({expr, currIndex}); _simplificationMap[expr].insert(expr); - orderedConstraints[currIndex].insert(expr); + auto indexConstraints = orderedConstraints[currIndex].second; + indexConstraints.insert(expr); + orderedConstraints.replace({currIndex, indexConstraints}); constraints.addConstraint(expr, delta); } } @@ -389,29 +387,6 @@ void PathConstraints::rewriteConcretization(const Assignment &a) { constraints.rewriteConcretization(a); } -PathConstraints PathConstraints::concat(const PathConstraints &l, - const PathConstraints &r) { - // TODO : How to handle symcretes and concretization? - PathConstraints path = l; - path._path = Path::concat(l._path, r._path); - auto offset = l._path.KBlockSize(); - for (const auto &i : r._original) { - path._original.insert(i); - auto index = r.pathIndexes.at(i); - index.block += offset; - path.pathIndexes.insert({i, index}); - path.orderedConstraints[index].insert(i); - } - for (const auto &i : r.constraints.cs()) { - path.constraints.addConstraint(i, {}); - if (r._simplificationMap.count(i)) { - path._simplificationMap.insert({i, r._simplificationMap.at(i)}); - } - } - // Run the simplificator on the newly constructed set? - return path; -} - Simplificator::ExprResult Simplificator::simplifyExpr(const constraints_ty &constraints, const ref &expr) { diff --git a/lib/Expr/Path.cpp b/lib/Expr/Path.cpp index e67abd51b4..829e73b374 100644 --- a/lib/Expr/Path.cpp +++ b/lib/Expr/Path.cpp @@ -39,67 +39,6 @@ Path::PathIndex Path::getCurrentIndex() const { return {KBlocks.size() - 1, lastInstruction}; } -std::vector Path::getStack(bool reversed) const { - std::vector stack; - for (unsigned i = 0; i < KBlocks.size(); i++) { - auto current = reversed ? KBlocks[KBlocks.size() - 1 - i] : KBlocks[i]; - // Previous for reversed is the next - KBlock *prev = nullptr; - if (i != 0) { - prev = reversed ? KBlocks[KBlocks.size() - i] : KBlocks[i - 1]; - } - if (i == 0) { - stack.push_back({nullptr, current->parent}); - continue; - } - if (reversed) { - auto kind = getTransitionKind(current, prev); - if (kind == TransitionKind::StepInto) { - if (!stack.empty()) { - stack.pop_back(); - } - } else if (kind == TransitionKind::StepOut) { - assert(isa(prev)); - stack.push_back({prev->getFirstInstruction(), current->parent}); - } - } else { - auto kind = getTransitionKind(prev, current); - if (kind == TransitionKind::StepInto) { - stack.push_back({prev->getFirstInstruction(), current->parent}); - } else if (kind == TransitionKind::StepOut) { - if (!stack.empty()) { - stack.pop_back(); - } - } - } - } - return stack; -} - -std::vector> -Path::asFunctionRanges() const { - assert(!KBlocks.empty()); - std::vector> ranges; - BlockRange range{0, 0}; - KFunction *function = KBlocks[0]->parent; - for (unsigned i = 1; i < KBlocks.size(); i++) { - if (getTransitionKind(KBlocks[i - 1], KBlocks[i]) == TransitionKind::None) { - if (i == KBlocks.size() - 1) { - range.last = i; - ranges.push_back({function, range}); - return ranges; - } else { - continue; - } - } - range.last = i - 1; - ranges.push_back({function, range}); - range.first = i; - function = KBlocks[i]->parent; - } - llvm_unreachable("asFunctionRanges reached the end of the for!"); -} - Path Path::concat(const Path &l, const Path &r) { Path path = l; for (auto block : r.KBlocks) { @@ -112,11 +51,16 @@ Path Path::concat(const Path &l, const Path &r) { std::string Path::toString() const { std::string blocks = ""; unsigned depth = 0; - for (unsigned i = 0; i < KBlocks.size(); i++) { - auto current = KBlocks[i]; + std::vector KBlocksVector; + KBlocksVector.reserve(KBlocks.size()); + for (auto kblock : KBlocks) { + KBlocksVector.push_back(kblock); + } + for (size_t i = 0; i < KBlocksVector.size(); i++) { + auto current = KBlocksVector[i]; KBlock *prev = nullptr; if (i != 0) { - prev = KBlocks[i - 1]; + prev = KBlocksVector[i - 1]; } auto kind = i == 0 ? TransitionKind::StepInto : getTransitionKind(prev, current);