From 4df70ac2d2c027ae0219e0987787cb96a84e4051 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 5 Jun 2019 09:13:04 -0700
Subject: [PATCH] Add a SAWscript position to calls to Crucible's malloc (#479)

* Add a SAWscript position to calls to Crucible's malloc

So when users get a Crucible memory dump, they can tell that this allocation
was made in a SAW override, rather than in their C/LLVM code

* Add a SAWscript position to calls to Crucible's malloc

* Show Positions instead of ProgramLocs
---
 src/SAWScript/CrucibleBuiltins.hs | 27 ++++++++++++++++-----------
 src/SAWScript/CrucibleOverride.hs |  4 +++-
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs
index 7335b50c75..ad43ac4705 100644
--- a/src/SAWScript/CrucibleBuiltins.hs
+++ b/src/SAWScript/CrucibleBuiltins.hs
@@ -576,19 +576,29 @@ assertEqualVals cc v1 v2 =
 
 --------------------------------------------------------------------------------
 
--- | Allocate space on the LLVM heap to store a value of the given
--- type. Returns the pointer to the allocated memory.
-doAlloc ::
+doAllocWithMutability ::
   (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  Crucible.Mutability        ->
   CrucibleContext arch       ->
   (W4.ProgramLoc, Crucible.MemType) ->
   StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
-doAlloc cc (_loc,tp) = StateT $ \mem ->
+doAllocWithMutability mut cc (loc, tp) = StateT $ \mem ->
   do let sym = cc^.ccBackend
      let dl = Crucible.llvmDataLayout ?lc
      sz <- W4.bvLit sym Crucible.PtrWidth (Crucible.bytesToInteger (Crucible.memTypeSize dl tp))
      let alignment = Crucible.maxAlignment dl -- Use the maximum alignment required for any primitive type (FIXME?)
-     Crucible.mallocRaw sym mem sz alignment
+     let l = show (W4.plSourceLoc loc)
+     liftIO $
+       Crucible.doMalloc sym Crucible.HeapAlloc Crucible.Mutable l mem sz alignment
+
+-- | Allocate space on the LLVM heap to store a value of the given
+-- type. Returns the pointer to the allocated memory.
+doAlloc ::
+  (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
+  CrucibleContext arch       ->
+  (W4.ProgramLoc, Crucible.MemType) ->
+  StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
+doAlloc = doAllocWithMutability Crucible.Mutable
 
 -- | Allocate read-only space on the LLVM heap to store a value of the
 -- given type. Returns the pointer to the allocated memory.
@@ -597,12 +607,7 @@ doAllocConst ::
   CrucibleContext arch       ->
   (W4.ProgramLoc, Crucible.MemType) ->
   StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
-doAllocConst cc (_loc,tp) = StateT $ \mem ->
-  do let sym = cc^.ccBackend
-     let dl = Crucible.llvmDataLayout ?lc
-     sz <- W4.bvLit sym Crucible.PtrWidth (Crucible.bytesToInteger (Crucible.memTypeSize dl tp))
-     let alignment = Crucible.maxAlignment dl -- Use the maximum alignment required for any primitive type (FIXME?)
-     Crucible.mallocConstRaw sym mem sz alignment
+doAllocConst = doAllocWithMutability Crucible.Immutable
 
 --------------------------------------------------------------------------------
 
diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs
index 1b51f23d5f..6b0d400021 100644
--- a/src/SAWScript/CrucibleOverride.hs
+++ b/src/SAWScript/CrucibleOverride.hs
@@ -1368,7 +1368,9 @@ executeAllocation opts cc (var, (loc, memTy)) =
      mem <- readGlobal memVar
      sz <- liftIO $ W4.bvLit sym Crucible.PtrWidth (Crucible.bytesToInteger w)
      let alignment = Crucible.noAlignment -- default to byte alignment (FIXME)
-     (ptr, mem') <- liftIO (Crucible.mallocRaw sym mem sz alignment)
+     let l = show (W4.plSourceLoc loc) ++ " (Poststate)"
+     (ptr, mem') <- liftIO $
+       Crucible.doMalloc sym Crucible.HeapAlloc Crucible.Mutable l mem sz alignment
      writeGlobal memVar mem'
      assignVar cc loc var ptr