From e92fb1630cafdf276d79f078c816d0f06ea35b28 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Mon, 24 Feb 2020 07:51:25 -0800
Subject: [PATCH 1/3] Support conditional memory write operations.

---
 .../src/Lang/Crucible/LLVM/MemModel.hs        | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
index 957a99ef6..3f7954079 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
@@ -159,6 +159,7 @@ module Lang.Crucible.LLVM.MemModel
   , G.SomeAlloc(..)
   , G.possibleAllocs
   , G.ppSomeAlloc
+  , doConditionalWriteOperation
 
     -- * PtrWidth (re-exports)
   , HasPtrWidth
@@ -1090,6 +1091,30 @@ storeRaw sym mem ptr valType alignment val = do
     assert sym p2 (err $ ptrMessage errMsg2 ptr valType)
     return mem{ memImplHeap = heap' }
 
+doConditionalWriteOperation
+  :: (IsSymInterface sym, HasPtrWidth wptr)
+  => sym
+  -> MemImpl sym
+  -> Pred sym
+  -> (MemImpl sym -> IO (MemImpl sym))
+  -> IO (MemImpl sym)
+doConditionalWriteOperation sym mem cond write_op = do
+  frame_id <- pushAssumptionFrame sym
+  loc <- getCurrentProgramLoc sym
+  addAssumption sym $ LabeledPred cond $
+    AssumptionReason loc "conditional memory write predicate"
+
+  let branched_heap = G.branchMem $ memImplHeap mem
+  mutated_heap <-
+    memImplHeap <$> write_op (mem { memImplHeap = branched_heap })
+  let merged_mem = mem
+        { memImplHeap = G.mergeMem cond mutated_heap branched_heap
+        }
+
+  _ <- popAssumptionFrame sym frame_id
+
+  return $! merged_mem
+
 -- | Store an LLVM value in memory if the condition is true, and
 -- otherwise leaves memory unchanged.
 --

From 82a26b4be110d3a5c4a0dc9bd25297e74b6c8ad9 Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Tue, 3 Mar 2020 17:51:28 -0800
Subject: [PATCH 2/3] Add helper to merge memory operations.

---
 .../src/Lang/Crucible/LLVM/MemModel.hs        | 22 ++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
index 3f7954079..37d9d57af 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
@@ -160,6 +160,7 @@ module Lang.Crucible.LLVM.MemModel
   , G.possibleAllocs
   , G.ppSomeAlloc
   , doConditionalWriteOperation
+  , mergeWriteOperations
 
     -- * PtrWidth (re-exports)
   , HasPtrWidth
@@ -1098,17 +1099,28 @@ doConditionalWriteOperation
   -> Pred sym
   -> (MemImpl sym -> IO (MemImpl sym))
   -> IO (MemImpl sym)
-doConditionalWriteOperation sym mem cond write_op = do
+doConditionalWriteOperation sym mem cond write_op =
+  mergeWriteOperations sym mem cond write_op return
+
+mergeWriteOperations
+  :: (IsSymInterface sym, HasPtrWidth wptr)
+  => sym
+  -> MemImpl sym
+  -> Pred sym
+  -> (MemImpl sym -> IO (MemImpl sym))
+  -> (MemImpl sym -> IO (MemImpl sym))
+  -> IO (MemImpl sym)
+mergeWriteOperations sym mem cond true_write_op false_write_op = do
   frame_id <- pushAssumptionFrame sym
   loc <- getCurrentProgramLoc sym
   addAssumption sym $ LabeledPred cond $
     AssumptionReason loc "conditional memory write predicate"
 
-  let branched_heap = G.branchMem $ memImplHeap mem
-  mutated_heap <-
-    memImplHeap <$> write_op (mem { memImplHeap = branched_heap })
+  let branched_mem = mem { memImplHeap = G.branchMem $ memImplHeap mem }
+  true_mutated_heap <- memImplHeap <$> true_write_op branched_mem
+  false_mutated_heap <- memImplHeap <$> false_write_op branched_mem
   let merged_mem = mem
-        { memImplHeap = G.mergeMem cond mutated_heap branched_heap
+        { memImplHeap = G.mergeMem cond true_mutated_heap false_mutated_heap
         }
 
   _ <- popAssumptionFrame sym frame_id

From ee4c2940e6987a212fc1d6942e40581b690619dc Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Mon, 9 Mar 2020 17:02:29 -0700
Subject: [PATCH 3/3] Address comments.

---
 .../src/Lang/Crucible/LLVM/MemModel.hs        | 41 ++++++++++++-------
 1 file changed, 27 insertions(+), 14 deletions(-)

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
index 37d9d57af..0bbc815ed 100644
--- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
@@ -1092,40 +1092,53 @@ storeRaw sym mem ptr valType alignment val = do
     assert sym p2 (err $ ptrMessage errMsg2 ptr valType)
     return mem{ memImplHeap = heap' }
 
+-- | Perform a memory write operation if the condition is true,
+-- do not change the memory otherwise.
+--
+-- Asserts that the write operation is valid when cond is true.
 doConditionalWriteOperation
   :: (IsSymInterface sym, HasPtrWidth wptr)
   => sym
   -> MemImpl sym
-  -> Pred sym
-  -> (MemImpl sym -> IO (MemImpl sym))
+  -> Pred sym {- ^ write condition -}
+  -> (MemImpl sym -> IO (MemImpl sym)) {- ^ memory write operation -}
   -> IO (MemImpl sym)
 doConditionalWriteOperation sym mem cond write_op =
   mergeWriteOperations sym mem cond write_op return
 
+-- | Merge memory write operations on condition: if the condition is true,
+-- perform the true branch write operation, otherwise perform the false branch
+-- write operation.
+--
+-- Asserts that the true branch write operation is valid when cond is true, and
+-- that the false branch write operation is valid when cond is not true.
 mergeWriteOperations
   :: (IsSymInterface sym, HasPtrWidth wptr)
   => sym
   -> MemImpl sym
-  -> Pred sym
-  -> (MemImpl sym -> IO (MemImpl sym))
-  -> (MemImpl sym -> IO (MemImpl sym))
+  -> Pred sym {- ^ merge condition -}
+  -> (MemImpl sym -> IO (MemImpl sym)) {- ^ true branch memory write operation -}
+  -> (MemImpl sym -> IO (MemImpl sym)) {- ^ false branch memory write operation -}
   -> IO (MemImpl sym)
 mergeWriteOperations sym mem cond true_write_op false_write_op = do
-  frame_id <- pushAssumptionFrame sym
+  let branched_mem = mem { memImplHeap = G.branchMem $ memImplHeap mem }
   loc <- getCurrentProgramLoc sym
+
+  true_frame_id <- pushAssumptionFrame sym
   addAssumption sym $ LabeledPred cond $
     AssumptionReason loc "conditional memory write predicate"
-
-  let branched_mem = mem { memImplHeap = G.branchMem $ memImplHeap mem }
   true_mutated_heap <- memImplHeap <$> true_write_op branched_mem
-  false_mutated_heap <- memImplHeap <$> false_write_op branched_mem
-  let merged_mem = mem
-        { memImplHeap = G.mergeMem cond true_mutated_heap false_mutated_heap
-        }
+  _ <- popAssumptionFrame sym true_frame_id
 
-  _ <- popAssumptionFrame sym frame_id
+  false_frame_id <- pushAssumptionFrame sym
+  not_cond <- notPred sym cond
+  addAssumption sym $ LabeledPred not_cond $
+    AssumptionReason loc "conditional memory write predicate"
+  false_mutated_heap <- memImplHeap <$> false_write_op branched_mem
+  _ <- popAssumptionFrame sym false_frame_id
 
-  return $! merged_mem
+  return $!
+    mem { memImplHeap = G.mergeMem cond true_mutated_heap false_mutated_heap }
 
 -- | Store an LLVM value in memory if the condition is true, and
 -- otherwise leaves memory unchanged.