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

@@ -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
 
 --------------------------------------------------------------------------------
 

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