Independent solver rework #85

dim8art · 2023-04-29T01:47:14Z

Summary:

Checklist:

The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
The PR is divided into a logical sequence of commits OR a single commit is sufficient.
There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
Each commit has a meaningful message documenting what it does.
All messages added to the codebase, all comments, as well as commit messages are spellchecked.
The code is commented OR not applicable/necessary.
The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
There are test cases for the code you added or modified OR no such test cases are required.

codecov-commenter · 2023-08-04T08:54:34Z

Codecov Report

Merging #85 (5555b3e) into main (9406351) will increase coverage by 0.22%.
The diff coverage is 83.20%.

❗ Current head 5555b3e differs from pull request most recent head 5937f8b. Consider uploading reports for the commit 5937f8b to get more accurate results

@@            Coverage Diff             @@
##             main      #85      +/-   ##
==========================================
+ Coverage   65.37%   65.60%   +0.22%     
==========================================
  Files         211      213       +2     
  Lines       28676    29018     +342     
  Branches     6374     6437      +63     
==========================================
+ Hits        18746    19036     +290     
- Misses       7442     7519      +77     
+ Partials     2488     2463      -25

Files Changed	Coverage Δ
include/klee/Expr/Constraints.h	`50.00% <ø> (ø)`
include/klee/Expr/Expr.h	`82.30% <0.00%> (-1.24%)`	⬇️
lib/Core/SeedInfo.cpp	`9.78% <0.00%> (-0.45%)`	⬇️
lib/Solver/CachingSolver.cpp	`66.31% <ø> (+1.91%)`	⬆️
lib/Solver/FastCexSolver.cpp	`30.39% <ø> (+0.05%)`	⬆️
lib/Solver/Solver.cpp	`41.04% <0.00%> (ø)`
lib/Solver/Z3Solver.cpp	`69.52% <ø> (+0.57%)`	⬆️
lib/Solver/QueryLoggingSolver.cpp	`62.80% <37.50%> (+0.38%)`	⬆️
lib/Expr/Assignment.cpp	`46.55% <41.17%> (+1.09%)`	⬆️
lib/Solver/AssignmentValidatingSolver.cpp	`30.23% <50.00%> (+1.01%)`	⬆️
... and 17 more

... and 9 files with indirect coverage changes

misonijnik · 2023-08-20T11:33:53Z

include/klee/Expr/Assignment.h

+                                  bool allowFreeValues) {
+  AssignmentEvaluator v(*this, allowFreeValues);
+  for (; begin != end; ++begin) {
+    if ((*begin)->getWidth() == Expr::Bool && !v.visit(*begin)->isTrue())


Please separate the logic for processing non-boolean expressions into a separate function

misonijnik · 2023-08-20T11:34:31Z

include/klee/ADT/OrderMaintenanceTrie.h

+
+#undef ITEMSIZE
+#undef ALPHA
+#endif


Put a new line

misonijnik · 2023-08-20T11:38:57Z

include/klee/ADT/ImmutableMap.h

+      if (*it1 != *it2)
+        return false;
+    }
+    return size() == b.size();


Swap the size equality condition with the element equality conditions for better performance

misonijnik · 2023-08-20T11:39:16Z

include/klee/ADT/ImmutableMap.h

+      if (*it1 > *it2)
+        return false;
+    }
+    return size() < b.size();


Same as above

misonijnik · 2023-08-20T11:39:29Z

include/klee/ADT/DisjointSetUnion.h

+  disjointSets_ty ds() const { return disjointSets; }
+};
+} // namespace klee
+#endif


Put a new line

misonijnik · 2023-08-20T11:42:31Z

include/klee/Expr/Assignment.h

@@ -27,45 +28,44 @@ using symcretes_ty = SymcreteOrderedSet;

 class Assignment {
 public:
-  typedef std::map<const Array *, SparseStorage<unsigned char>> bindings_ty;
+  using bindings_ty = ImmutableMap<const Array *, SparseStorage<unsigned char>>;


You can use PersistentMap instead of ImmutableMap, since the persistent version is a wrapper for convenience

misonijnik · 2023-08-20T11:43:32Z

include/klee/Expr/Expr.h

@@ -328,6 +328,13 @@ class Expr {
  // Given an array of new kids return a copy of the expression
  // but using those children.
  virtual ref<Expr> rebuild(ref<Expr> kids[/* getNumKids() */]) const = 0;
+  virtual ref<Expr> rebuild() const {


Is this the code used?

misonijnik · 2023-08-20T11:43:45Z

include/klee/Expr/IndependentConstraintSetUnion.h

+};
+} // namespace klee
+
+#endif


Put a new line

misonijnik · 2023-08-20T11:45:10Z

lib/Expr/IndependentConstraintSetUnion.cpp

+  icsu.reEvaluateConcretization(newConcretization);
+  return icsu.getConcretizedVersion();
+}
+} // namespace klee


Put a new line

misonijnik · 2023-08-20T11:47:37Z

lib/Solver/CexCachingSolver.cpp

@@ -132,7 +132,8 @@ struct isValidOrSatisfyingResponse {
  isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {}

  bool operator()(ref<SolverResponse> a) const {


Split keys in boolean keys and non-boolean keys and update the predicate accordingly

dim8art marked this pull request as draft April 29, 2023 01:48

dim8art force-pushed the IndependentSolverRework branch from e7ce3b1 to fde881f Compare May 4, 2023 02:47

dim8art force-pushed the IndependentSolverRework branch 2 times, most recently from 38fc182 to 5c1c074 Compare May 15, 2023 11:41

dim8art marked this pull request as ready for review May 15, 2023 11:50

misonijnik mentioned this pull request Jul 28, 2023

Reworking independent and concretizing solvers #103

Closed

8 tasks

dim8art force-pushed the IndependentSolverRework branch 5 times, most recently from cdb3b3b to 0d0fcc1 Compare August 4, 2023 08:02

dim8art force-pushed the IndependentSolverRework branch 2 times, most recently from eaf1337 to a26c72d Compare August 7, 2023 09:41

dim8art force-pushed the IndependentSolverRework branch 5 times, most recently from 0e8b5e3 to 1d4b9bd Compare August 19, 2023 12:21

misonijnik reviewed Aug 20, 2023

View reviewed changes

dim8art force-pushed the IndependentSolverRework branch from 1d4b9bd to 5937f8b Compare August 20, 2023 14:47

dim8art added 5 commits August 23, 2023 15:50

Add DisjointSetUnion

be33e6f

Rework IndependentSolver using persistent DSU

c35c9f1

Reworking ConcretizingSolver

d9ae5a3

Add persistency to Assignment

bdf29c8

Rework solver chain + small refactoring changes

e319a6f

dim8art force-pushed the IndependentSolverRework branch from 5937f8b to e319a6f Compare August 23, 2023 12:51

misonijnik merged commit f72486f into UnitTestBot:main Sep 14, 2023
20 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Independent solver rework #85

Independent solver rework #85

dim8art commented Apr 29, 2023

codecov-commenter commented Aug 4, 2023 •

edited

Loading

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

misonijnik Aug 20, 2023

		@@ -132,7 +132,8 @@ struct isValidOrSatisfyingResponse {
		isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {}

		bool operator()(ref<SolverResponse> a) const {

Independent solver rework #85

Independent solver rework #85

Conversation

dim8art commented Apr 29, 2023

Summary:

Checklist:

codecov-commenter commented Aug 4, 2023 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov-commenter commented Aug 4, 2023 •

edited

Loading