heapster-saw: LogEntry with names and structure

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

@@ -23,6 +23,7 @@ import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Reflection
 import Data.List.NonEmpty (NonEmpty(..))
+import Data.Functor.Constant
 import Data.ByteString
 import Numeric
 import Numeric.Natural
@@ -564,6 +565,15 @@ instance Liftable (KnownReprObj f a) where
 instance LiftableAny1 (KnownReprObj f) where
   mbLiftAny1 = mbLift
 
+instance Liftable a => LiftableAny1 (Constant a) where
+  mbLiftAny1 = mbLift
+
+instance Liftable a => Liftable (Constant a b) where
+  mbLift (mbMatch -> [nuMP| Data.Functor.Constant.Constant x |]) = Data.Functor.Constant.Constant (mbLift x)
+
+instance (Liftable a, Liftable b, Liftable c) => Liftable (a,b,c) where
+  mbLift (mbMatch -> [nuMP| (x,y,z) |]) = (mbLift x, mbLift y, mbLift z)
+
 -- FIXME: this change for issue #28 requires ClosableAny1 to be exported from
 -- Hobbits
 {-

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

@@ -11,6 +11,7 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PolyKinds #-}
 module Verifier.SAW.Heapster.IDESupport where
 
 import Control.Monad.Reader
@@ -51,7 +52,10 @@ import Verifier.SAW.Heapster.Implication
 import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.TypedCrucible
 import Verifier.SAW.Heapster.JSONExport(ppToJson)
-
+import Data.Aeson (Value)
+import Data.Type.RList (mapRAssign)
+import Data.Functor.Constant
+import Control.Monad.Writer
 
 -- | The entry point for dumping a Heapster environment to a file for IDE
 -- consumption.
@@ -65,6 +69,9 @@ type ExtractionM = ReaderT (PPInfo, ProgramLoc, String) (Writer [LogEntry])
 emit :: LogEntry -> ExtractionM ()
 emit entry = tell [entry]
 
+gather :: ExtractionM () -> ExtractionM [LogEntry]
+gather m = snd <$> listen m
+
 -- | A single entry in the IDE info dump log.  At a bare minimum, this must
 -- include a location and corresponding permission.  Once the basics are
 -- working, we can enrich the information we log.
@@ -74,26 +81,31 @@ data LogEntry
       , leEntryId :: LogEntryID
       , leCallers :: [LogEntryID]
       , leFunctionName :: String
-      , leExport :: Value
-      , lePermissions :: String
+      , lePermissions :: [(String, String, Value)]
       }
   | LogError
       { lerrLocation :: String
       , lerrError :: String
       , lerrFunctionName :: String
       }
+  | LogImpl
+      { limplLocation :: String
+      , limplExport :: Value
+      , limplFunctionName :: String
+      }
+
   deriving (Generic, Show)
 instance ToJSON LogEntry
 instance NuMatching LogEntry where
   nuMatchingProof = unsafeMbTypeRepr
 instance Liftable LogEntry where
   mbLift mb = case mbMatch mb of
-    [nuMP| LogEntry u v w x y z |] -> 
-      LogEntry (mbLift u) (mbLift v) (mbLift w) 
-               (mbLift x) (mbLift y) (mbLift z)
+    [nuMP| LogEntry v w x y z |] -> 
+      LogEntry (mbLift v) (mbLift w) (mbLift x) (mbLift y) (mbLift z)
     [nuMP| LogError x y z |] -> 
       LogError (mbLift x) (mbLift y) (mbLift z)
-
+    [nuMP| LogImpl x y z |] -> 
+      LogImpl (mbLift x) (mbLift y) (mbLift z)
 
 data LogEntryID = LogEntryID
   { leIdBlock :: Int
@@ -126,7 +138,15 @@ instance (PermCheckExtC ext)
     withLoc loc (mbExtractLogEntries (typedEntryBody te))
     let entryId = mkLogEntryID $ typedEntryID te
     let callers = callerIDs $ typedEntryCallers te
-    mbValPermEntries entryId callers (typedEntryPermsIn te)
+    (ppi, _, fname) <- ask
+    let loc' = snd (ppLoc loc)
+    let f :: 
+           (Pair (Constant String) ValuePerm) x ->
+           Constant (String, String, Value) x
+        f (Pair (Constant name) vp) = Constant (name, permPrettyString ppi vp, ppToJson ppi vp)
+    let inputs = mbLift
+               $ fmap (RL.toList . mapRAssign f . zipRAssign (typedEntryNames te)) (typedEntryPermsIn te)
+    tell [LogEntry loc' entryId callers fname inputs]
 
 mkLogEntryID :: TypedEntryID blocks args -> LogEntryID
 mkLogEntryID = uncurry LogEntryID . entryIDIndices
@@ -135,6 +155,12 @@ callerIDs :: [Some (TypedCallSite phase blocks tops args ghosts)] -> [LogEntryID
 callerIDs = map $ \(Some tcs) -> case typedCallSiteID tcs of 
     TypedCallSiteID tei _ _ _ -> mkLogEntryID tei
 
+data Pair f g x = Pair (f x) (g x)
+
+zipRAssign :: RL.RAssign f x -> RL.RAssign g x -> RL.RAssign (Pair f g) x
+zipRAssign RL.MNil RL.MNil = RL.MNil
+zipRAssign (xs RL.:>: x) (ys RL.:>: y) = zipRAssign xs ys RL.:>: Pair x y
+
 instance ExtractLogEntries (TypedStmtSeq ext blocks tops ret ps_in) where
   extractLogEntries (TypedImplStmt (AnnotPermImpl _str pimpl)) =
     -- fmap (setErrorMsg str) <$> extractLogEntries pimpl
@@ -155,7 +181,10 @@ instance ExtractLogEntries (PermImpl1 ps_in ps_outs) where
   extractLogEntries (Impl1_Fail err) =
     do (_, loc, fname) <- ask
        emit (LogError (snd (ppLoc loc)) (ppError err) fname)
-  extractLogEntries _ = pure ()
+    -- The error message is available further up the stack, so we just leave it
+  extractLogEntries impl =
+    do (ppi, loc, fname) <- ask
+       emit (LogImpl (snd (ppLoc loc)) (ppToJson ppi impl) fname)
 
 instance ExtractLogEntries
     (MbPermImpls (TypedStmtSeq ext blocks tops ret) ps_outs) where
@@ -186,30 +215,6 @@ mbExtractLogEntries mb_a =
   execWriter $ runReaderT (extractLogEntries x) 
                           (ppInfoAddExprNames "x" ns ppi, loc, fname)
 
--- TODO: The next two functions are a hack, and we should probably rethink how
--- this is architected a bit.  They don't fit into the type signature of
--- `ExtractLogEntries` currently because we push down the extra information
--- about the entrypoint IDs which we need wherever `LogEntry`s are created.
-
-mbValPermEntries 
-  :: LogEntryID 
-  -> [LogEntryID] 
-  -> Mb ctx (ValuePerms ctx) 
-  -> ExtractionM ()
-mbValPermEntries entryId callers mb_vp =
-  ReaderT $ \(ppi, loc, fname) ->
-  tell $ mbLift $ flip nuMultiWithElim1 mb_vp $ \ns vp ->
-  execWriter $ runReaderT (valPermEntries entryId callers vp) 
-                          (ppInfoAddExprNames "x" ns ppi, loc, fname)
-
-valPermEntries :: LogEntryID -> [LogEntryID] -> ValuePerms ctx -> ExtractionM ()
-valPermEntries entryId callers vps = do
-  (ppi, loc, fname) <- ask
-  let loc' = snd (ppLoc loc)
-  let strs = foldValuePerms (\xs vp -> 
-               (ppToJson ppi vp, permPrettyString ppi vp) : xs) [] vps
-  tell [LogEntry loc' entryId callers fname export str | (export, str) <- strs]
-
 typedStmtOutCtx :: TypedStmt ext rets ps_in ps_next -> CruCtx rets
 typedStmtOutCtx = error "FIXME: write typedStmtOutCtx"
 
@@ -218,13 +223,16 @@ withLoc loc = local (\(ppinfo, _, fname) -> (ppinfo, loc, fname))
 
 setErrorMsg :: String -> LogEntry -> LogEntry
 setErrorMsg msg le@LogError {} = le { lerrError = msg }
+setErrorMsg msg le@LogImpl {} =
+  LogError { lerrError = msg
+           , lerrLocation = limplLocation le
+           , lerrFunctionName = limplFunctionName le}
 setErrorMsg msg le@LogEntry {} =
   LogError { lerrError = msg
            , lerrLocation = leLocation le
            , lerrFunctionName = leFunctionName le
            }
 
-
 runWithLoc :: PPInfo -> [Some SomeTypedCFG] -> [LogEntry]
 runWithLoc ppi =
   concatMap (runWithLocHelper ppi)

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

@@ -82,6 +82,7 @@ import Verifier.SAW.Heapster.Permissions
 import Verifier.SAW.Heapster.Widening
 
 import Debug.Trace
+import Data.Type.RList (mapRAssign)
 
 
 ----------------------------------------------------------------------
@@ -339,7 +340,6 @@ instance Closable (TypedCallSiteID blocks args vars) where
 instance Liftable (TypedCallSiteID blocks args vars) where
   mbLift = unClosed . mbLift . fmap toClosed
 
-
 ----------------------------------------------------------------------
 -- * Typed Crucible Statements
 ----------------------------------------------------------------------
@@ -1175,6 +1175,8 @@ data TypedEntry phase ext blocks tops ret args ghosts =
     typedEntryCallers :: ![Some (TypedCallSite phase blocks tops args ghosts)],
     -- | The ghost variables for this entrypoint
     typedEntryGhosts :: !(CruCtx ghosts),
+    --
+    typedEntryNames :: !(TransData phase (RAssign (Constant String) ((tops :++: args) :++: ghosts))),
     -- | The input permissions for this entrypoint
     typedEntryPermsIn :: !(MbValuePerms ((tops :++: args) :++: ghosts)),
     -- | The output permissions for the function (cached locally)
@@ -1205,23 +1207,26 @@ completeTypedEntry ::
 completeTypedEntry (TypedEntry { .. })
   | Just body <- typedEntryBody
   , Just callers <- mapM (traverseF completeTypedCallSite) typedEntryCallers
-  = Just $ TypedEntry { typedEntryBody = body, typedEntryCallers = callers, .. }
+  , Just names <- typedEntryNames
+  = Just $ TypedEntry { typedEntryBody = body, typedEntryCallers = callers, typedEntryNames = names, .. }
 completeTypedEntry _ = Nothing
 
 -- | Build an entrypoint from a call site, using that call site's permissions as
 -- the entyrpoint input permissions
-singleCallSiteEntry :: TypedCallSiteID blocks args vars ->
-                       CruCtx tops -> CruCtx args -> TypeRepr ret ->
-                       MbValuePerms ((tops :++: args) :++: vars) ->
-                       MbValuePerms (tops :> ret) ->
-                       TypedEntry TCPhase ext blocks tops ret args vars
+singleCallSiteEntry ::
+  TypedCallSiteID blocks args vars ->
+  CruCtx tops -> CruCtx args -> TypeRepr ret ->
+  MbValuePerms ((tops :++: args) :++: vars) ->
+  MbValuePerms (tops :> ret) ->
+  TypedEntry TCPhase ext blocks tops ret args vars
 singleCallSiteEntry siteID tops args ret perms_in perms_out =
   TypedEntry
   {
     typedEntryID = callSiteDest siteID, typedEntryTops = tops,
     typedEntryArgs = args, typedEntryRet = ret,
     typedEntryCallers = [Some $ idTypedCallSite siteID tops args perms_in],
     typedEntryGhosts = callSiteVars siteID,
+    typedEntryNames = Nothing,
     typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out,
     typedEntryBody = Nothing
   }
@@ -1345,6 +1350,7 @@ emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out
         typedEntryID = TypedEntryID blockID 0, typedEntryTops = tops,
         typedEntryArgs = args, typedEntryRet = ret,
         typedEntryCallers = [], typedEntryGhosts = ghosts,
+        typedEntryNames = Nothing,
         typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out,
         typedEntryBody = Nothing }]
     names
@@ -3867,27 +3873,46 @@ tcBlockEntryBody ::
   Block ext cblocks ret args ->
   TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts ->
   TopPermCheckM ext cblocks blocks tops ret
-    (Mb ((tops :++: CtxToRList args) :++: ghosts)
+    (RAssign (Constant String) ((tops :++: CtxToRList args) :++: ghosts),
+     Mb ((tops :++: CtxToRList args) :++: ghosts)
       (TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts)))
 tcBlockEntryBody names blk entry@(TypedEntry {..}) =
-  runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
-  \tops_ns args_ns ghosts_ns perms ->
-  let ctx = mkCtxTrans (blockInputs blk) args_ns
-      ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in
-  stmtTraceM (\i ->
-               pretty "Type-checking block" <+> pretty (blockID blk) <>
-               comma <+> pretty "entrypoint" <+> pretty (entryIndex typedEntryID)
-               <> line <>
-               pretty "Input types:"
-               <> align (permPretty i $
-                         RL.map2 VarAndType ns $ cruCtxToTypes $
-                         typedEntryAllArgs entry)
-               <> line <>
-               pretty "Input perms:"
-               <> align (permPretty i perms)) >>>
-  stmtRecombinePerms >>>
-  tcEmitStmtSeq names ctx (blk ^. blockStmts)
+  do mbNs <- mkNs
+     stmts <- mkStmts
+     pure (mbLift mbNs,stmts)
+  where
+    mkNs =
+      runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
+      \tops_ns args_ns ghosts_ns _ ->
+      permGetPPInfo >>>= \ppi ->
+      let tops   = mapRAssign (Constant . show . permPretty ppi) tops_ns
+          args   = mapRAssign (Constant . show . permPretty ppi) args_ns
+          ghosts = mapRAssign (Constant . show . permPretty ppi) ghosts_ns
+          ns     = rappend (rappend tops args) ghosts
+      in traceShow ("ns", RL.toList ns) $ gmapRet (>> pure ns)
+
+    mkStmts =
+      runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
+      \tops_ns args_ns ghosts_ns perms ->
+      let ctx = mkCtxTrans (blockInputs blk) args_ns
+          ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in
+      stmtTraceM (\i ->
+                  pretty "Type-checking block" <+> pretty (blockID blk) <>
+                  comma <+> pretty "entrypoint" <+> pretty (entryIndex typedEntryID)
+                  <> line <>
+                  pretty "Input types:"
+                  <> align (permPretty i $
+                            RL.map2 VarAndType ns $ cruCtxToTypes $
+                            typedEntryAllArgs entry)
+                  <> line <>
+                  pretty "Input perms:"
+                  <> align (permPretty i perms)) >>>
+      stmtRecombinePerms >>>
+      tcEmitStmtSeq names ctx (blk ^. blockStmts)
 
+rappend :: RAssign f x -> RAssign f y -> RAssign f (x :++: y)
+rappend xs (ys :>: y) = rappend xs ys :>: y
+rappend xs MNil = xs
 
 -- | Prove that the permissions held at a call site from the given source
 -- entrypoint imply the supplied input permissions of the current entrypoint
@@ -3949,18 +3974,22 @@ visitCallSite (TypedEntry {..}) site@(TypedCallSite {..})
 
 -- | Widen the permissions held by all callers of an entrypoint to compute new,
 -- weaker input permissions that can hopefully be satisfied by them
-widenEntry :: PermCheckExtC ext =>
-              TypedEntry TCPhase ext blocks tops ret args ghosts ->
-              Some (TypedEntry TCPhase ext blocks tops ret args)
+widenEntry ::
+  forall ext blocks tops ret args ghosts.
+  PermCheckExtC ext =>
+  TypedEntry TCPhase ext blocks tops ret args ghosts ->
+  Some (TypedEntry TCPhase ext blocks tops ret args)
 widenEntry (TypedEntry {..}) =
   case foldl1' (widen typedEntryTops typedEntryArgs) $
        map (fmapF typedCallSiteArgVarPerms) typedEntryCallers of
-    Some (ArgVarPerms ghosts perms_in) ->
+    Some (ArgVarPerms (ghosts :: CruCtx x) perms_in) ->
       let callers =
-            map (fmapF (callSiteSetGhosts ghosts)) typedEntryCallers in
+            map (fmapF (callSiteSetGhosts ghosts)) typedEntryCallers
+      in
       Some $
       TypedEntry { typedEntryCallers = callers, typedEntryGhosts = ghosts,
-                   typedEntryPermsIn = perms_in, typedEntryBody = Nothing, .. }
+                   typedEntryPermsIn = perms_in, typedEntryBody = Nothing,
+                   typedEntryNames = Nothing, .. }
 
 -- | Visit an entrypoint, by first proving the required implications at each
 -- call site, meaning that the permissions held at the call site imply the input
@@ -4003,9 +4032,10 @@ visitEntry names can_widen blk entry =
       -- is no reason to re-type-check the body, so just update the callers
       return $ Some $ entry { typedEntryCallers = callers }
     else
-      do body <- maybe (tcBlockEntryBody names blk entry) return (typedEntryBody entry)
+      do (ns, body) <- maybe (tcBlockEntryBody names blk entry) return ((,) <$> typedEntryNames entry <*> typedEntryBody entry)
          return $ Some $ entry { typedEntryCallers = callers,
-                                 typedEntryBody = Just body }
+                                 typedEntryBody = Just body,
+                                 typedEntryNames = Just ns }
 
 
 -- | Visit a block by visiting all its entrypoints