From bac4c239b3f857efb8426cecbeec550ec252bf58 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Sat, 9 Dec 2023 11:42:56 -0500
Subject: [PATCH] Generalize lazy memory model using HasMacawLazySimulatorState

This introduces a `HasMacawLazySimulatorState` data type, which provides a
"classy lens" for accessing a `MacawLazySimulatorState` within some Crucible
personality type. It also generalizes the lazy `macaw-symbolic` memory model in
`Data.Macaw.Symbolic.Memory.Lazy` to be polymorphic over
`HasMacawLazySimulatorState` instances. The upside is that it is now possible
to use the lazy memory model at other personality types besides just
`MacawLazySimulatorState`, making it much easier to extend the memory model.

Because there is a `HasMacawLazySimulatorState` instance for
`MacawLazySimulatorState`, existing code that uses `MacawLazySimulatorState`
should continue to compile without changes.

Fixes #357.
---
 symbolic/src/Data/Macaw/Symbolic.hs           |  1 +
 symbolic/src/Data/Macaw/Symbolic/MemOps.hs    | 25 ++++++++++++++++---
 .../src/Data/Macaw/Symbolic/Memory/Lazy.hs    |  9 ++++---
 3 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs
index bdd8e76d..89ba0d44 100644
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@@ -133,6 +133,7 @@ module Data.Macaw.Symbolic
   , MO.MacawSimulatorState(..)
   , MO.MacawLazySimulatorState(..)
   , MO.emptyMacawLazySimulatorState
+  , MO.HasMacawLazySimulatorState(..)
   , MO.populatedMemChunks
   , MkGlobalPointerValidityAssertion
   , MemModelConfig(..)
diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
index cdcfd829..5a95eba9 100644
--- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# Language DataKinds #-}
 {-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language FunctionalDependencies #-}
 {-# Language TypeOperators #-}
 {-# Language TypeFamilies #-}
 {-# Language ImplicitParams #-}
@@ -37,6 +39,7 @@ module Data.Macaw.Symbolic.MemOps
   , MacawSimulatorState(..)
   , MacawLazySimulatorState(..)
   , emptyMacawLazySimulatorState
+  , HasMacawLazySimulatorState(..)
   , populatedMemChunks
   , LookupFunctionHandle(..)
   , LookupSyscallHandle(..)
@@ -379,11 +382,25 @@ emptyMacawLazySimulatorState = MacawLazySimulatorState
   { _populatedMemChunks = IS.empty
   }
 
+-- | A class for Crucible personality types @p@ which contain a
+-- 'MacawLazySimulatorState'. The lazy memory model in
+-- "Data.Macaw.Symbolic.Memory" is polymorphic over 'HasMacawLazySimulatorState'
+-- instances so that downstream @macaw-symbolic@ users can supply their own
+-- personality types that extend 'MacawLazySimulatorState' further.
+-- See @Note [Lazy memory model]@ in "Data.Macaw.Symbolic.Memory.Lazy".
+class HasMacawLazySimulatorState p sym w | p -> sym w where
+  macawLazySimulatorState :: Lens' p (MacawLazySimulatorState sym w)
+instance HasMacawLazySimulatorState (MacawLazySimulatorState sym w) sym w where
+  macawLazySimulatorState = id
+
 -- | A `Lens'` for '_populatedMemChunks'.
-populatedMemChunks :: Lens' (MacawLazySimulatorState sym w)
-                            (IS.IntervalSet (IMI.Interval (M.MemWord w)))
-populatedMemChunks = lens _populatedMemChunks
-                          (\s v -> s { _populatedMemChunks = v })
+populatedMemChunks ::
+     HasMacawLazySimulatorState p sym w
+  => Lens' p (IS.IntervalSet (IMI.Interval (M.MemWord w)))
+populatedMemChunks =
+    macawLazySimulatorState
+  . lens _populatedMemChunks
+         (\s v -> s { _populatedMemChunks = v })
 
 type Regs sym arch = Ctx.Assignment (C.RegValue' sym)
                                     (MacawCrucibleRegTypes arch)
diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs b/symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs
index 29e6a95c..80c35b47 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs
@@ -100,8 +100,8 @@ import qualified Data.Macaw.Symbolic.Memory.Common as MSMC
 -- Note some key differences between this function and the @memModelConfig@
 -- function in "Data.Macaw.Symbolic.Memory":
 --
--- * This function requires the personality type to be
---   'MS.MacawLazySimulatorState', as it must track which sections of global
+-- * This function requires the personality type to be an instance of
+--   'MS.HasMacawLazySimulatorState', as it must track which sections of global
 --   memory have already been populated in the simulator state.
 --
 -- * This function requires an 'CBO.OnlineBackend' to make use of an online
@@ -112,6 +112,7 @@ memModelConfig ::
      , sym ~ WE.ExprBuilder scope st fs
      , bak ~ CBO.OnlineBackend solver scope st fs
      , WPO.OnlineSolver solver
+     , MS.HasMacawLazySimulatorState p sym w
      , MC.MemWidth w
      , 1 <= w
      , 16 <= w
@@ -120,7 +121,7 @@ memModelConfig ::
      )
   => bak
   -> MemPtrTable sym w
-  -> MS.MemModelConfig (MS.MacawLazySimulatorState sym w) sym arch CL.Mem
+  -> MS.MemModelConfig p sym arch CL.Mem
 memModelConfig bak mpt =
   MS.MemModelConfig
     { MS.globalMemMap = mapRegionPointers mpt
@@ -660,7 +661,7 @@ lazilyPopulateGlobalMemArr ::
   forall sym bak w t st fs p ext.
   ( CB.IsSymBackend sym bak
   , sym ~ WEB.ExprBuilder t st fs
-  , p ~ MS.MacawLazySimulatorState sym w
+  , MS.HasMacawLazySimulatorState p sym w
   , MC.MemWidth w
   ) =>
   bak ->