Heapster ide info (#1821)

* add basic IDE logging, start error cleanup

* clean up additional implication errors

* add structure to stmt fail in line with impl fail

* redesign error message types, pipe through to log

* fix default heapster environments missing ioref

* carry more information through on most common implication error

* remove Some from error constructor

* Export valueperms in full json detail

* Avoid generating orphan ToJSON instances and using Given

* refine jsonexport instances

* Document JSONExport

* Remove need for passing undefined

* JSONExport support for PermImpls

* export entrypoint and caller ID information

* cleanup imports, 80 char columns

* heapster: export function name for IDE

* heapster-saw: LogEntry with names and structure

* Incorporate names from bindings in JsonExport

* Update PPInfo while exporting

* checkpoint

* Use types to generate names for pretty permissions where possible

* WIP: fixing errors introduced by the merge.

* got SAW to compile after the latest merge of master

* Updtate deps

* bumping the cryptol submodule to match master

* moved nuMatching and Liftable instances to the top of the file in NamedMb.hs, to help with GHC 9 support

* GHC 9 fixes

* renamed the Mb' datatype to the more accessible name NamedMb, and changed the names of all of its operationsto use 'Named' as a suffix instead of just using a prime

---------

Co-authored-by: Karl Smeltzer <[email protected]>
Co-authored-by: Eric Mertens <[email protected]>
Co-authored-by: Eddy Westbrook <[email protected]>

heapster-saw/heapster-saw.cabal

@@ -38,20 +38,26 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
-    extra,
+    aeson ^>= 1.5,
+    th-abstraction,
+    template-haskell,
+    extra
   hs-source-dirs: src
   build-tool-depends:
     alex:alex,
     happy:happy,
   exposed-modules:
     Verifier.SAW.Heapster.CruUtil
     Verifier.SAW.Heapster.GenMonad
+    Verifier.SAW.Heapster.IDESupport
     Verifier.SAW.Heapster.HintExtract
     Verifier.SAW.Heapster.Implication
     Verifier.SAW.Heapster.IRTTranslation
     Verifier.SAW.Heapster.Lexer
     Verifier.SAW.Heapster.LLVMGlobalConst
     Verifier.SAW.Heapster.Located
+    Verifier.SAW.Heapster.NamedMb
+    Verifier.SAW.Heapster.JSONExport
     Verifier.SAW.Heapster.ParsedCtx
     Verifier.SAW.Heapster.Parser
     Verifier.SAW.Heapster.Permissions

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

@@ -25,6 +25,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
@@ -570,6 +571,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/GenMonad.hs

@@ -8,17 +8,20 @@ module Verifier.SAW.Heapster.GenMonad (
   -- * Core definitions
   GenStateContT(..), (>>>=), (>>>),
   -- * Continuation operations
-  gcaptureCC, gmapRet, gabortM, gparallel, gopenBinding,
+  gcaptureCC, gmapRet, gabortM, gparallel, startBinding,
+  startNamedBinding, gopenBinding, gopenNamedBinding,
   -- * State operations
   gmodify,
   -- * Transformations
   addReader,
   ) where
 
-import Data.Binding.Hobbits ( nuMultiWithElim1, Mb, Name, RAssign )
+import Data.Binding.Hobbits ( nuMulti, nuMultiWithElim1, Mb, Name, RAssign )
 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 {
@@ -107,6 +110,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)
+gopenNamedBinding ::
+  (NamedMb ctx (m b1) -> m r2) ->
+  NamedMb ctx b2 ->
+  GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
+gopenNamedBinding f_ret mb_a =
+  gcaptureCC \k ->
+  f_ret $ flip nuMultiWithElim1Named 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)
+startNamedBinding ::
+  RAssign StringF ctx ->
+  (NamedMb ctx (m r1) -> m r2) ->
+  GenStateContT s r1 s r2 m (RAssign Name ctx)
+startNamedBinding tps f_ret = gcaptureCC (f_ret . nuMultiNamed tps)
+
 addReader :: GenStateContT s1 r1 s2 r2 m a -> GenStateContT s1 r1 s2 r2 (ReaderT e m) a
 addReader (GenStateContT m) =
   GenStateContT \s2 k ->