From 888ae3b6193a29c5358331c789ba7949ae96d614 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <c.cadar@imperial.ac.uk>
Date: Thu, 20 Sep 2018 13:37:00 +0100
Subject: Refactored AddressSpace::resolve() by creating a new function
 AddressSpace::checkPointerInObject() that is called in both the forward and
 the backward searches.  This makes the code more modular and removes a large
 part of duplicated code and should also address the non-deterministic
 coverage in the resolve() function which affects Codecov reports.

---
 lib/Core/AddressSpace.h | 30 ++++++++++++++++++++----------
 1 file changed, 20 insertions(+), 10 deletions(-)

(limited to 'lib/Core/AddressSpace.h')

diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 10549e7a..fa814950 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -32,15 +32,26 @@ namespace klee {
   };
   
   typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
-  
+
   class AddressSpace {
   private:
     /// Epoch counter used to control ownership of objects.
     mutable unsigned cowKey;
 
     /// Unsupported, use copy constructor
-    AddressSpace &operator=(const AddressSpace&); 
-    
+    AddressSpace &operator=(const AddressSpace &);
+
+    /// Check if pointer `p` can point to the memory object in the
+    /// given object pair.  If so, add it to the given resolution list.
+    ///
+    /// \return 1 iff the resolution is incomplete (`maxResolutions`
+    /// is non-zero and it was reached, or a query timed out), 0 iff
+    /// the resolution is complete (`p` can only point to the given
+    /// memory object), and 2 otherwise.
+    int checkPointerInObject(ExecutionState &state, TimingSolver *solver,
+                             ref<Expr> p, const ObjectPair &op,
+                             ResolutionList &rl, unsigned maxResolutions) const;
+
   public:
     /// The MemoryObject -> ObjectState map that constitutes the
     /// address space.
@@ -51,7 +62,6 @@ namespace klee {
     /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
     MemoryMap objects;
     
-  public:
     AddressSpace() : cowKey(1) {}
     AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
     ~AddressSpace() {}
@@ -76,15 +86,15 @@ namespace klee {
                     ObjectPair &result,
                     bool &success);
 
-    /// Resolve address to a list of ObjectPairs it can point to. If
-    /// maxResolutions is non-zero then no more than that many pairs
-    /// will be returned. 
+    /// Resolve pointer `p` to a list of `ObjectPairs` it can point
+    /// to. If `maxResolutions` is non-zero then no more than that many
+    /// pairs will be returned.
     ///
-    /// \return true iff the resolution is incomplete (maxResolutions
-    /// is non-zero and the search terminated early, or a query timed out).
+    /// \return true iff the resolution is incomplete (`maxResolutions`
+    /// is non-zero and it was reached, or a query timed out).
     bool resolve(ExecutionState &state,
                  TimingSolver *solver,
-                 ref<Expr> address, 
+                 ref<Expr> p,
                  ResolutionList &rl, 
                  unsigned maxResolutions=0,
                  double timeout=0.);
-- 
cgit 1.4.1