Merge branch 'master' into yppe/propsSubset

GaloisInc · Mar 2, 2023 · f0db68b · f0db68b
2 parents b53bc1b + 9d66afc
commit f0db68b
Show file tree

Hide file tree

Showing 14 changed files with 1,267 additions and 219 deletions.
diff --git a/heapster-saw/heapster-saw.cabal b/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

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/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
 {-

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs b/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 ->