checkpoint

heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs

@@ -8,7 +8,7 @@ module Verifier.SAW.Heapster.GenMonad (
   -- * Core definitions
   GenStateContT(..), (>>>=), (>>>),
   -- * Continuation operations
-  gcaptureCC, gmapRet, gabortM, gparallel, startBinding, gopenBinding,
+  gcaptureCC, gmapRet, gabortM, gparallel, startBinding, startBinding', gopenBinding, gopenBinding',
   -- * State operations
   gmodify,
   -- * Transformations
@@ -20,6 +20,7 @@ import Control.Monad.State ( ap, MonadState(get, put) )
 import Control.Monad.Trans.Class ( MonadTrans(lift) )
 import Control.Monad.Trans.Reader
 import Data.Proxy
+import Verifier.SAW.Heapster.NamedMb
 
 -- | The generalized state-continuation monad
 newtype GenStateContT s1 r1 s2 r2 m a = GenStateContT {
@@ -108,13 +109,30 @@ gopenBinding f_ret mb_a =
   f_ret $ flip nuMultiWithElim1 mb_a $ \names a ->
   k (names, a)
 
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+gopenBinding' ::
+  (Mb' ctx (m b1) -> m r2) ->
+  Mb' ctx b2 ->
+  GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
+gopenBinding' f_ret mb_a =
+  gcaptureCC \k ->
+  f_ret $ flip nuMultiWithElim1' mb_a $ \names a ->
+  k (names, a)
+
 -- | Name-binding in the generalized continuation monad (FIXME: explain)
 startBinding ::
   RAssign Proxy ctx ->
   (Mb ctx (m r1) -> m r2) ->
   GenStateContT s r1 s r2 m (RAssign Name ctx)
 startBinding tps f_ret = gcaptureCC (f_ret . nuMulti tps)
 
+-- | Name-binding in the generalized continuation monad (FIXME: explain)
+startBinding' ::
+  RAssign StringF ctx ->
+  (Mb' ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startBinding' tps f_ret = gcaptureCC (f_ret . nuMulti' tps)
+
 addReader :: GenStateContT s1 r1 s2 r2 m a -> GenStateContT s1 r1 s2 r2 (ReaderT e m) a
 addReader (GenStateContT m) =
   GenStateContT \s2 k ->

heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs

@@ -53,6 +53,7 @@ import Data.Functor.Constant
 import Control.Monad.Writer
 import Data.Binding.Hobbits.NameMap (NameMap)
 import qualified Data.Binding.Hobbits.NameMap as NameMap
+import Verifier.SAW.Heapster.NamedMb
 
 -- | The entry point for dumping a Heapster environment to a file for IDE
 -- consumption.
@@ -131,30 +132,30 @@ instance (PermCheckExtC ext)
     => ExtractLogEntries
          (TypedEntry TransPhase ext blocks tops ret args ghosts) where
   extractLogEntries te = do
-    let loc = mbLift $ fmap getFirstProgramLocTS (typedEntryBody te)
-    withLoc loc (mbExtractLogEntries (typedEntryBody te))
+    let loc = mbLift' $ fmap getFirstProgramLocTS (typedEntryBody te)
+    withLoc loc (mb'ExtractLogEntries (typedEntryBody te))
     let entryId = mkLogEntryID $ typedEntryID te
     let callers = callerIDs $ typedEntryCallers te
     (ppi, _, fname) <- ask
     let loc' = snd (ppLoc loc)
-
+    let debugNames = _mbNames (typedEntryBody te)
     let insertNames ::
           RL.RAssign Name (x :: RList CrucibleType) ->
-          RL.RAssign (Constant String) x ->
+          RL.RAssign StringF x ->
           NameMap (StringF :: CrucibleType -> *)->
           NameMap (StringF :: CrucibleType -> *)
         insertNames RL.MNil RL.MNil m = m
-        insertNames (ns RL.:>: n) (xs RL.:>: Constant name) m =
+        insertNames (ns RL.:>: n) (xs RL.:>: StringF name) m =
           insertNames ns xs (NameMap.insert n (StringF name) m)
         inputs = mbLift
                $ flip nuMultiWithElim1 (typedEntryPermsIn te)
                $ \ns body ->
-                 let ppi' = ppi { ppExprNames = insertNames ns (typedEntryNames te) (ppExprNames ppi) }
+                 let ppi' = ppi { ppExprNames = insertNames ns debugNames (ppExprNames ppi) }
                      f :: 
-                      (Pair (Constant String) ValuePerm) x ->
+                      (Pair StringF ValuePerm) x ->
                       Constant (String, String, Value) x
-                     f (Pair (Constant name) vp) = Constant (name, permPrettyString ppi' vp, ppToJson ppi' vp)
-                 in RL.toList (mapRAssign f (zipRAssign (typedEntryNames te) body))
+                     f (Pair (StringF name) vp) = Constant (name, permPrettyString ppi' vp, ppToJson ppi' vp)
+                 in RL.toList (mapRAssign f (zipRAssign debugNames body))
     tell [LogEntry loc' entryId callers fname inputs]
 
 mkLogEntryID :: TypedEntryID blocks args -> LogEntryID
@@ -175,7 +176,7 @@ instance ExtractLogEntries (TypedStmtSeq ext blocks tops ret ps_in) where
     -- fmap (setErrorMsg str) <$> extractLogEntries pimpl
     extractLogEntries pimpl
   extractLogEntries (TypedConsStmt loc _ _ rest) = do
-    withLoc loc $ mbExtractLogEntries rest
+    withLoc loc $ mb'ExtractLogEntries rest
   extractLogEntries (TypedTermStmt _ _) = pure ()
 
 instance ExtractLogEntries
@@ -197,8 +198,8 @@ instance ExtractLogEntries (PermImpl1 ps_in ps_outs) where
 
 instance ExtractLogEntries
     (MbPermImpls (TypedStmtSeq ext blocks tops ret) ps_outs) where
-  extractLogEntries (MbPermImpls_Cons _ mbpis pis) = do
-    mbExtractLogEntries pis
+  extractLogEntries (MbPermImpls_Cons ctx mbpis pis) = do
+    mbExtractLogEntries ctx pis
     extractLogEntries mbpis
   extractLogEntries MbPermImpls_Nil = pure ()
 
@@ -217,11 +218,19 @@ instance (PermCheckExtC ext)
       mapM_ (\(Some te) -> extractLogEntries te) $ _typedBlockEntries tb
 
 mbExtractLogEntries
-  :: ExtractLogEntries a => Mb (ctx :: RList CrucibleType) a -> ExtractionM ()
-mbExtractLogEntries mb_a =
+  :: ExtractLogEntries a => CruCtx ctx -> Mb (ctx :: RList CrucibleType) a -> ExtractionM ()
+mbExtractLogEntries ctx mb_a =
   ReaderT $ \(ppi, loc, fname) ->
   tell $ mbLift $ flip nuMultiWithElim1 mb_a $ \ns x ->
-  let ppi' = ppInfoAddExprNames "x" ns ppi in
+  let ppi' = ppInfoAddTypedExprNames ctx ns ppi in
+  execWriter $ runReaderT (extractLogEntries x) (ppi', loc, fname)
+
+mb'ExtractLogEntries
+  :: ExtractLogEntries a => Mb' (ctx :: RList CrucibleType) a -> ExtractionM ()
+mb'ExtractLogEntries mb_a =
+  ReaderT $ \(ppi, loc, fname) ->
+  tell $ mbLift $ flip nuMultiWithElim1 (_mbBinding mb_a) $ \ns x ->
+  let ppi' = ppInfoApplyAllocation ns (_mbNames mb_a) ppi in
   execWriter $ runReaderT (extractLogEntries x) (ppi', loc, fname)
 
 typedStmtOutCtx :: TypedStmt ext rets ps_in ps_next -> CruCtx rets
@@ -278,7 +287,7 @@ getFirstProgramLocBM block =
       -> Maybe ProgramLoc
     helper ste = case ste of
       Some TypedEntry { typedEntryBody = stmts } ->
-        Just $ mbLift $ fmap getFirstProgramLocTS stmts
+        Just $ mbLift' $ fmap getFirstProgramLocTS stmts
 
 -- | From the sequence, get the first program location we encounter, which
 -- should correspond to the permissions for the entry point we want to log

heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs

@@ -0,0 +1,77 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE TypeOperators #-}
+module Verifier.SAW.Heapster.NamedMb where
+
+import Data.Binding.Hobbits
+import Data.Binding.Hobbits.MonadBind
+import Data.Type.RList
+import Control.Lens
+
+newtype StringF a = StringF { unStringF :: String }
+
+type Binding' c = Mb' (RNil :> c)
+
+data Mb' ctx a = Mb'
+  { _mbNames :: RAssign StringF ctx
+  , _mbBinding :: Mb ctx a
+  }
+  deriving Functor
+
+mbBinding :: Lens (Mb' ctx a) (Mb' ctx b) (Mb ctx a) (Mb ctx b)
+mbBinding f x = Mb' (_mbNames x) <$> f (_mbBinding x)
+
+nuMulti' :: RAssign StringF ctx -> (RAssign Name ctx -> b) -> Mb' ctx b
+nuMulti' tps f = Mb'
+  { _mbNames = tps
+  , _mbBinding = nuMulti (mapRAssign (const Proxy) tps) f
+  }
+
+nuMultiWithElim1' :: (RAssign Name ctx -> arg -> b) -> Mb' ctx arg -> Mb' ctx b
+nuMultiWithElim1' k = over mbBinding (nuMultiWithElim1 k)
+
+
+strongMbM' :: MonadStrongBind m => Mb' ctx (m a) -> m (Mb' ctx a)
+strongMbM' = traverseOf mbBinding strongMbM
+
+mbM' :: (MonadBind m, NuMatching a) => Mb' ctx (m a) -> m (Mb' ctx a)
+mbM' = traverseOf mbBinding mbM
+
+mbSwap' :: RAssign Proxy ctx -> Mb' ctx' (Mb' ctx a) -> Mb' ctx (Mb' ctx' a)
+mbSwap' p (Mb' names' body') =
+    Mb'
+    { _mbNames = mbLift (_mbNames <$> body')
+    , _mbBinding = Mb' names' <$> mbSwap p (_mbBinding <$> body')
+    }
+
+mbSink :: RAssign Proxy ctx -> Mb ctx' (Mb' ctx a) -> Mb' ctx (Mb ctx' a)
+mbSink p m =
+    Mb'
+    { _mbNames = mbLift (_mbNames <$> m)
+    , _mbBinding = mbSwap p (_mbBinding <$> m)
+    }
+
+mbLift' :: Liftable a => Mb' ctx a -> a
+mbLift' = views mbBinding mbLift
+
+elimEmptyMb' :: Mb' RNil a -> a
+elimEmptyMb' = views mbBinding elimEmptyMb
+
+emptyMb' :: a -> Mb' RNil a
+emptyMb' = Mb' MNil . emptyMb
+
+mkNuMatching [t| forall a. StringF a |]
+instance NuMatchingAny1 StringF where
+    nuMatchingAny1Proof = nuMatchingProof
+
+instance Liftable (StringF a) where
+    mbLift (mbMatch -> [nuMP| StringF x |]) = StringF (mbLift x)
+
+instance LiftableAny1 StringF where
+    mbLiftAny1 = mbLift
+
+mkNuMatching [t| forall ctx a. NuMatching a => Mb' ctx a |]

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -79,6 +79,7 @@ import Lang.Crucible.LLVM.Bytes
 import Lang.Crucible.CFG.Core
 import Verifier.SAW.Term.Functor (Ident)
 import Verifier.SAW.OpenTerm
+import Verifier.SAW.Heapster.NamedMb
 
 import Verifier.SAW.Heapster.CruUtil
 
@@ -137,8 +138,6 @@ foldMapWithDefault comb def f l = foldr1WithDefault comb def $ map f l
 -- * Pretty-printing
 ----------------------------------------------------------------------
 
-newtype StringF a = StringF { unStringF :: String }
-
 -- | Convert a type to a base name for printing variables of that type
 typeBaseName :: TypeRepr a -> String
 typeBaseName UnitRepr = "u"
@@ -175,16 +174,24 @@ emptyPPInfo = PPInfo NameMap.empty Map.empty
 
 -- | Add an expression variable to a 'PPInfo' with the given base name
 ppInfoAddExprName :: String -> ExprVar a -> PPInfo -> PPInfo
-ppInfoAddExprName base _ _
+ppInfoAddExprName base x ppi =
+  let (ppi', str) = ppInfoAllocateName base ppi in
+  ppInfoApplyName x str ppi'
+
+ppInfoApplyName :: Name (x :: CrucibleType) -> String -> PPInfo -> PPInfo
+ppInfoApplyName x str ppi =
+  ppi { ppExprNames = NameMap.insert x (StringF str) (ppExprNames ppi) }
+
+ppInfoAllocateName :: String -> PPInfo -> (PPInfo, String)
+ppInfoAllocateName base _
   | length base == 0 || isDigit (last base) =
     error ("ppInfoAddExprName: invalid base name: " ++ base)
-ppInfoAddExprName base x (PPInfo { .. }) =
+ppInfoAllocateName base ppi =
   let (i',str) =
-        case Map.lookup base ppBaseNextInt of
+        case Map.lookup base (ppBaseNextInt ppi) of
           Just i -> (i+1, base ++ show i)
           Nothing -> (1, base) in
-  PPInfo { ppExprNames = NameMap.insert x (StringF str) ppExprNames,
-           ppBaseNextInt = Map.insert base i' ppBaseNextInt }
+  (ppi { ppBaseNextInt = Map.insert base i' (ppBaseNextInt ppi) }, str)
 
 -- | Add a sequence of variables to a 'PPInfo' with the given base name
 ppInfoAddExprNames :: String -> RAssign Name (tps :: RList CrucibleType) ->
@@ -193,12 +200,33 @@ ppInfoAddExprNames _ MNil info = info
 ppInfoAddExprNames base (ns :>: n) info =
   ppInfoAddExprNames base ns $ ppInfoAddExprName base n info
 
+-- |
+ppInfoAllocateExprNames ::
+  String {- ^ base name -} ->
+  RAssign pxy (tps :: RList CrucibleType) ->
+  PPInfo ->
+  (PPInfo, RAssign StringF tps)
+ppInfoAllocateExprNames _ MNil info = (info, MNil)
+ppInfoAllocateExprNames base (ns :>: _) ppi =
+  case ppInfoAllocateName base ppi of
+    (ppi1, str) ->
+      case ppInfoAllocateExprNames base ns ppi1 of
+        (ppi2, ns') -> (ppi2, ns' :>: StringF str)
+
 -- | Add a sequence of variables to a 'PPInfo' using their 'typeBaseName's
 ppInfoAddTypedExprNames :: CruCtx tps -> RAssign Name tps -> PPInfo -> PPInfo
 ppInfoAddTypedExprNames _ MNil info = info
 ppInfoAddTypedExprNames (CruCtxCons tps tp) (ns :>: n) info =
   ppInfoAddTypedExprNames tps ns $ ppInfoAddExprName (typeBaseName tp) n info
 
+ppInfoApplyAllocation ::
+  RAssign Name (tps :: RList CrucibleType) ->
+  RAssign StringF tps ->
+  PPInfo ->
+  PPInfo
+ppInfoApplyAllocation MNil MNil ppi = ppi
+ppInfoApplyAllocation (ns :>: n) (ss :>: StringF s) ppi =
+  ppInfoApplyAllocation ns ss (ppInfoApplyName n s ppi)
 
 type PermPPM = Reader PPInfo
 
@@ -313,15 +341,15 @@ instance PermPrettyF VarAndType where
 
 
 permPrettyExprMb :: PermPretty a =>
-                    (RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
-                    Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
+  (RAssign (Constant (Doc ann)) ctx -> PermPPM (Doc ann) -> PermPPM (Doc ann)) ->
+  Mb (ctx :: RList CrucibleType) a -> PermPPM (Doc ann)
 permPrettyExprMb f mb =
   fmap mbLift $ strongMbM $ flip nuMultiWithElim1 mb $ \ns a ->
-  local (ppInfoAddExprNames "z" ns) $
+  local (ppInfoAddExprNames "x" ns) $
   do docs <- traverseRAssign (\n -> Constant <$> permPrettyM n) ns
      f docs $ permPrettyM a
 
-instance PermPretty a => PermPretty (Mb (ctx :: RList CrucibleType) a) where
+instance (PermPretty a) => PermPretty (Mb (ctx :: RList CrucibleType) a) where
   permPrettyM =
     permPrettyExprMb $ \docs ppm ->
     (\pp -> PP.group (ppEncList True (RL.toList docs) <>
@@ -4932,6 +4960,23 @@ genSubstMb ::
   s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a)
 genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb))
 
+
+instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb' ctx a) m where
+   genSubst = genSubstMb' given
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb' RNil a) m where
+   genSubst = genSubstMb' RL.typeCtxProxies
+
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding' c a) m where
+   genSubst = genSubstMb' RL.typeCtxProxies
+
+genSubstMb' ::
+  Substable s a m =>
+  NuMatching a =>
+  RAssign Proxy ctx ->
+  s ctx' -> Mb ctx' (Mb' ctx a) -> m (Mb' ctx a)
+genSubstMb' p s mbmb = mbM' (fmap (genSubst s) (mbSink p mbmb))
+
 instance SubstVar s m => Substable s (Member ctx a) m where
   genSubst _ mb_memb = return $ mbLift mb_memb
 

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -77,6 +77,7 @@ import Verifier.SAW.Heapster.CruUtil
 import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.Implication
 import Verifier.SAW.Heapster.TypedCrucible
+import Verifier.SAW.Heapster.NamedMb
 
 import GHC.Stack
 import Debug.Trace
@@ -3798,7 +3799,7 @@ translateCallEntry nm entry_trans mb_tops_args mb_ghosts =
          -- If not, continue by translating entry, setting the variable
          -- permission map to empty (as in the beginning of a block)
          clearVarPermsM $ translate $
-         fmap (\s -> varSubst s $ typedEntryBody entry) mb_s
+         fmap (\s -> varSubst s $ _mbBinding $ typedEntryBody entry) mb_s
 
 
 instance PermCheckExtC ext =>
@@ -4084,7 +4085,7 @@ instance PermCheckExtC ext =>
   translate mb_x = case mbMatch mb_x of
     [nuMP| TypedImplStmt impl_seq |] -> translate impl_seq
     [nuMP| TypedConsStmt loc stmt pxys mb_seq |] ->
-      translateStmt (mbLift loc) stmt (translate $ mbCombine (mbLift pxys) mb_seq)
+      translateStmt (mbLift loc) stmt (translate $ mbCombine (mbLift pxys) (_mbBinding <$> mb_seq))
     [nuMP| TypedTermStmt _ term_stmt |] -> translate term_stmt
 
 instance PermCheckExtC ext =>
@@ -4214,7 +4215,7 @@ translateEntryBody mapTrans entry =
   lambdaPermCtx (typedEntryPermsIn entry) $ \pctx ->
   do retType <- translateEntryRetType entry
      impTransM (RL.members pctx) pctx mapTrans retType $ translate $
-       typedEntryBody entry
+       _mbBinding $ typedEntryBody entry
 
 -- | Translate all the entrypoints in a 'TypedBlockMap' that correspond to
 -- letrec-bound functions to SAW core functions as in 'translateEntryBody'