diff --git a/src/Data/Quant.hs b/src/Data/Quant.hs index 13897dcd..40e0ece4 100644 --- a/src/Data/Quant.hs +++ b/src/Data/Quant.hs @@ -64,6 +64,7 @@ module Data.Quant , pattern Single , viewQuantEach , pattern QuantEach + , AsSingle(..) ) where import Prelude hiding (map, traverse) @@ -287,38 +288,37 @@ instance (HasReprK k, forall x. Ord (f x)) => Ord (Quant (f :: k -> Type) tp) wh -- Defining which conversions are always possible class ToQuant f (t1 :: QuantK k) (t2 :: QuantK k) where - toQuant :: f t1 -> QuantRepr t2 -> f t2 + toQuant :: QuantRepr t2 -> f t1 -> f t2 -- Can take a universally quantified variant to any variant instance HasReprK k => ToQuant (Quant f) AllK (tp :: QuantK k) where - toQuant z@(QuantAll f) repr = case repr of + toQuant repr z@(QuantAll f) = case repr of QuantOneRepr baserepr -> QuantOne baserepr (TMF.apply f baserepr) QuantAllRepr -> QuantAll f QuantSomeRepr -> QuantSome z -- Can take any variant to an existentially quantified variant instance ToQuant (Quant f) (tp :: QuantK k) ExistsK where - toQuant z _ = case z of + toQuant _ z = case z of QuantSome{} -> z _ -> QuantSome z -- Can always take a variant to the same kind instance ToQuant f (OneK k1) (OneK k1) where - toQuant x _ = x - + toQuant _ x = x class ToMaybeQuant f (t1 :: QuantK k) (t2 :: QuantK k) where - toMaybeQuant :: f t1 -> QuantRepr t2 -> Maybe (f t2) + toMaybeQuant :: QuantRepr t2 -> f t1 -> Maybe (f t2) instance HasReprK k => ToMaybeQuant (Quant f) (tp1 :: QuantK k) (tp2 :: QuantK k) where - toMaybeQuant x repr = case (x, repr) of - (QuantAll{}, _) -> Just (toQuant x repr) - (_, QuantSomeRepr) -> Just (toQuant x repr) + toMaybeQuant repr x = case (x, repr) of + (QuantAll{}, _) -> Just (toQuant repr x) + (_, QuantSomeRepr) -> Just (toQuant repr x) (QuantOne baseX x', QuantOneRepr baseY) -> case testEquality baseX baseY of Just Refl -> Just $ QuantOne baseX x' -- by definition we can't convert between base types Nothing -> Nothing - (QuantSome x', _) -> toMaybeQuant x' repr + (QuantSome x', _) -> toMaybeQuant repr x' -- by definition a base type cannot be turned into a universal quantifier (QuantOne{}, QuantAllRepr) -> Nothing -- in general we could consider types that themselves have defined conversions between @@ -426,54 +426,54 @@ pattern Single repr x <- (quantAsOne -> Just (QuantAsOneProof repr x)) {-# COMPLETE All, QuantOne, QuantExists #-} {-# COMPLETE All, QuantOne, QuantSome #-} -newtype AsOneK (f :: QuantK k -> Type) (y :: k) where - AsOneK :: f (OneK y) -> AsOneK f y +newtype AsSingle (f :: QuantK k -> Type) (y :: k) where + AsSingle :: f (OneK y) -> AsSingle f y -deriving instance Eq (f (OneK x)) => Eq ((AsOneK f) x) -deriving instance Ord (f (OneK x)) => Ord ((AsOneK f) x) -deriving instance Show (f (OneK x)) => Show ((AsOneK f) x) +deriving instance Eq (f (OneK x)) => Eq ((AsSingle f) x) +deriving instance Ord (f (OneK x)) => Ord ((AsSingle f) x) +deriving instance Show (f (OneK x)) => Show ((AsSingle f) x) -instance TestEquality f => TestEquality (AsOneK f) where - testEquality (AsOneK x) (AsOneK y) = case testEquality x y of +instance TestEquality f => TestEquality (AsSingle f) where + testEquality (AsSingle x) (AsSingle y) = case testEquality x y of Just Refl -> Just Refl Nothing -> Nothing -instance OrdF f => OrdF (AsOneK f) where - compareF (AsOneK x) (AsOneK y) = case compareF x y of +instance OrdF f => OrdF (AsSingle f) where + compareF (AsSingle x) (AsSingle y) = case compareF x y of EQF -> EQF LTF -> LTF GTF -> GTF -instance forall f. ShowF f => ShowF (AsOneK f) where - showF (AsOneK x) = showF x +instance forall f. ShowF f => ShowF (AsSingle f) where + showF (AsSingle x) = showF x withShow _ (_ :: q tp) f = withShow (Proxy :: Proxy f) (Proxy :: Proxy (OneK tp)) f -type QuantEach (f :: QuantK k -> Type) = Quant (AsOneK f) AllK +type QuantEach (f :: QuantK k -> Type) = Quant (AsSingle f) AllK viewQuantEach :: HasReprK k => QuantEach f -> (forall (x :: k). ReprOf x -> f (OneK x)) -viewQuantEach (QuantAll f) = \r -> case TMF.apply f r of AsOneK x -> x +viewQuantEach (QuantAll f) = \r -> case TMF.apply f r of AsSingle x -> x -viewQuantEach' :: HasReprK k => Quant (AsOneK f) tp -> Maybe (Dict (IsExistsOr tp AllK), forall (x :: k). ReprOf x -> f (OneK x)) +viewQuantEach' :: HasReprK k => Quant (AsSingle f) tp -> Maybe (Dict (IsExistsOr tp AllK), forall (x :: k). ReprOf x -> f (OneK x)) viewQuantEach' q = case q of QuantOne{} -> Nothing - QuantAll f -> Just (Dict, \r -> case TMF.apply f r of AsOneK x -> x) + QuantAll f -> Just (Dict, \r -> case TMF.apply f r of AsSingle x -> x) QuantSome q' -> case viewQuantEach' q' of Just (Dict, g) -> Just (Dict, g) Nothing -> Nothing -pattern QuantEach :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall (x :: k). ReprOf x -> f (OneK x)) -> Quant (AsOneK f) tp +pattern QuantEach :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall (x :: k). ReprOf x -> f (OneK x)) -> Quant (AsSingle f) tp pattern QuantEach f <- (viewQuantEach' -> Just (Dict, f)) where - QuantEach f = existsOrCases @tp @AllK (QuantAny (QuantEach f)) (QuantAll (TMF.mapWithKey (\r _ -> AsOneK (f r)) (allReprs @k))) + QuantEach f = existsOrCases @tp @AllK (QuantAny (QuantEach f)) (QuantAll (TMF.mapWithKey (\r _ -> AsSingle (f r)) (allReprs @k))) {-# COMPLETE QuantEach, Single #-} -_testQuantEach :: forall {k} f tp. HasReprK k => Quant (AsOneK (f :: QuantK k -> Type)) tp -> () +_testQuantEach :: forall {k} f tp. HasReprK k => Quant (AsSingle (f :: QuantK k -> Type)) tp -> () _testQuantEach = \case QuantEach (_f :: forall (x :: k). ReprOf x -> f (OneK x)) -> () - Single (_repr :: ReprOf (x :: k)) (AsOneK (_x :: f (OneK x))) -> () + Single (_repr :: ReprOf (x :: k)) (AsSingle (_x :: f (OneK x))) -> () -_testQuantEach1 :: HasReprK k => Quant (AsOneK (f :: QuantK k -> Type)) AllK -> () +_testQuantEach1 :: HasReprK k => Quant (AsSingle (f :: QuantK k -> Type)) AllK -> () _testQuantEach1 = \case QuantEach (_f :: forall (x :: k). ReprOf x -> f (OneK x)) -> () -- complete match, since Single has an unsolvable constraint \ No newline at end of file diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index 26c81dc8..1181b76f 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -331,8 +331,8 @@ mkSingle bin a = PatchPairSingle bin a -- | Return the single 'tp' and which binary if the input is a singleton 'PatchPair'. -- 'asSingleton (toSingleton bin x) == (bin, x)' when 'x' contains an entry for 'bin' -- '(y,bin) <- asSingleton x; toSingleton bin y == x' when 'x' is a singleton -asSingleton :: PatchPairM m => PatchPair tp -> m (Pair PB.WhichBinaryRepr tp) -asSingleton (PatchPairSingle bin v) = return (Pair bin v) +asSingleton :: PatchPairM m => Qu.Quant tp qbin -> m (Pair PB.WhichBinaryRepr tp) +asSingleton (Qu.Single bin v) = return (Pair bin v) asSingleton _ = throwPairErr -- | Convert a 'PatchPair' into a singleton containing only diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index e8af885d..05d02a8c 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -157,6 +157,7 @@ import Data.Parameterized.Classes import Data.Set (Set) import qualified Data.Set as Set import Data.Word (Word32) +import qualified Data.Quant as Qu import qualified Lumberjack as LJ import Data.Parameterized (Some(..), Pair (..)) @@ -333,8 +334,10 @@ data WorkItem arch = (SingleNodeEntry arch PBi.Original) (SingleNodeEntry arch PBi.Patched) -- | Handle starting a split analysis from a diverging node. - | ProcessSplitCtor (Some (SingleNodeEntry arch)) - deriving (Eq, Ord) + | ProcessSplitCtor (Some (Qu.AsSingle (NodeEntry' arch))) + +deriving instance Eq (WorkItem arch) +deriving instance Ord (WorkItem arch) instance PA.ValidArch arch => Show (WorkItem arch) where show = \case @@ -362,8 +365,7 @@ pattern ProcessMerge:: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch pattern ProcessMerge sneO sneP <- (processMergeSinglePair -> Just (sneO, sneP)) pattern ProcessSplit :: SingleNodeEntry arch bin -> WorkItem arch -pattern ProcessSplit sne <- ProcessSplitCtor (Some sne) - +pattern ProcessSplit sne = ProcessSplitCtor (Some (Qu.AsSingle sne)) {-# COMPLETE ProcessNode, ProcessMergeAtExits, ProcessMergeAtEntry, ProcessSplit #-} {-# COMPLETE ProcessNode, ProcessMerge, ProcessSplit #-} @@ -436,7 +438,7 @@ data SyncData arch = -- | Defines exceptions for exits that would otherwise be considered sync points. -- In these cases, the single-sided analysis continues instead, with the intention -- that another sync point is encountered after additional instructions are executed - , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch))) + , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(Qu.AsSingle (NodeEntry' arch), PB.BlockTarget arch))) -- Exits from the corresponding desync node that start the single-sided analysis , _syncDesyncExits :: PPa.PatchPair (SetF (PB.BlockTarget arch)) } @@ -451,7 +453,9 @@ syncPointBin :: SyncPoint arch bin -> PBi.WhichBinaryRepr bin syncPointBin sp = singleEntryBin $ syncPointNode sp instance TestEquality (SyncPoint arch) where - testEquality e1 e2 = testEquality (syncPointNode e1) (syncPointNode e2) + testEquality e1 e2 = case testEquality (syncPointNode e1) (syncPointNode e2) of + Just Refl -> Just Refl + Nothing -> Nothing instance OrdF (SyncPoint arch) where compareF sp1 sp2 = lexCompareF (syncPointBin sp1) (syncPointBin sp2) $ @@ -595,7 +599,7 @@ mkProcessSplit sne = do GraphNode dp_ne <- return $ singleNodeDivergePoint sne sne_dp <- toSingleNodeEntry (singleEntryBin sne) dp_ne guard (sne_dp == sne) - return (ProcessSplitCtor (Some sne)) + return (ProcessSplit sne) workItemNode :: WorkItem arch -> GraphNode arch @@ -1271,9 +1275,9 @@ pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg -- FIXME: do we need to support mismatched node kinds here? combineNodes :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (GraphNode arch) combineNodes node1 node2 = do - let ndPair = PPa.mkPair (singleEntryBin node1) node1 node2 - nodeO <- PPa.get PBi.OriginalRepr ndPair - nodeP <- PPa.get PBi.PatchedRepr ndPair + let ndPair = PPa.mkPair (singleEntryBin node1) (Qu.AsSingle node1) (Qu.AsSingle node2) + Qu.AsSingle nodeO <- PPa.get PBi.OriginalRepr ndPair + Qu.AsSingle nodeP <- PPa.get PBi.PatchedRepr ndPair -- it only makes sense to combine nodes that share a divergence point, -- where that divergence point will be used as the calling context for the -- merged point @@ -1458,7 +1462,7 @@ isSyncExit :: isSyncExit sne blkt@(PB.BlockTarget{}) = do excepts <- getSingleNodeData syncExceptions sne syncs <- getSingleNodeData syncPoints sne - let isExcept = Set.member (TupleF2 sne blkt) excepts + let isExcept = Set.member (TupleF2 (Qu.AsSingle sne) blkt) excepts case isExcept of True -> return Nothing False -> isCutAddressFor sne (PB.targetRawPC blkt) >>= \case @@ -1528,7 +1532,7 @@ filterSyncExits priority (ProcessSplit sne) blktPairs = pgValid $ do return x filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of Nothing -> return blktPairs - Just (Some sne) -> do + Just (Some (Qu.AsSingle sne)) -> do let bin = singleEntryBin sne blkts <- mapM (PPa.get bin) blktPairs syncExits <- catMaybes <$> mapM (isSyncExit sne) blkts @@ -1543,14 +1547,14 @@ addReturnPointSync :: PPa.PatchPair (PB.BlockTarget arch) -> PairGraphM sym arch () addReturnPointSync priority ne blktPair = case asSingleNodeEntry ne of - Just (Some sne) -> do + Just (Some (Qu.AsSingle sne)) -> do let bin = singleEntryBin sne blkt <- PPa.get bin blktPair case PB.targetReturn blkt of Just ret -> do cuts <- getSingleNodeData syncCutAddresses sne excepts <- getSingleNodeData syncExceptions sne - let isExcept = Set.member (TupleF2 sne blkt) excepts + let isExcept = Set.member (TupleF2 (Qu.AsSingle sne) blkt) excepts case (not isExcept) && Set.member (PPa.WithBin (singleEntryBin sne) (PB.concreteAddress ret)) cuts of True -> do @@ -1600,7 +1604,7 @@ handleSingleSidedReturnTo :: NodeEntry arch -> PairGraphM sym arch () handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of - Just (Some sne) -> do + Just (Some (Qu.AsSingle sne)) -> do let bin = singleEntryBin sne let dp = singleNodeDivergePoint sne syncAddrs <- getSyncData syncCutAddresses bin dp diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index f54c33a2..51c3a614 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -16,10 +16,14 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE FlexibleContexts #-} module Pate.Verification.PairGraph.Node ( GraphNode , GraphNode'(..) + , NodeEntry' + , NodeReturn' , NodeEntry , NodeReturn , CallingContext @@ -62,6 +66,9 @@ module Pate.Verification.PairGraph.Node ( , singleNodeDivergence , toSingleNodeEntry , singleNodeAddr + , SingleNodeReturn + , SingleGraphNode + , pattern SingleNodeReturn ) where import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) @@ -83,6 +90,7 @@ import Control.Monad (guard) import Data.Parameterized.Classes import Pate.Panic import qualified Pate.Address as PAd +import Data.Kind (Type) -- | Nodes in the program graph consist either of a pair of -- program points (GraphNode), or a synthetic node representing @@ -112,18 +120,31 @@ instance PA.ValidArch arch => W4S.W4Serializable sym (GraphNode' arch bin) where instance PA.ValidArch arch => W4S.W4Serializable sym (NodeEntry' arch bin) where w4Serialize r = return $ JSON.toJSON r -data NodeContent arch e = - NodeContent { nodeContentCtx :: CallingContext arch, nodeContent :: e } - deriving (Eq, Ord) +data NodeContent arch (f :: PB.WhichBinary -> Type) (qbin :: QuantK PB.WhichBinary) = + NodeContent { nodeContentCtx :: CallingContext arch, nodeContent :: Quant f qbin } + +deriving instance (forall x. Eq (f x)) => Eq (NodeContent arch f qbin) +deriving instance (forall x. Ord (f x)) => Ord (NodeContent arch f qbin) + +instance (forall x. Eq (f x)) => TestEquality (NodeContent arch f) where + testEquality (NodeContent cctx1 x1) (NodeContent cctx2 x2) | cctx1 == cctx2, Just Refl <- testEquality x1 x2 = Just Refl + testEquality _ _ = Nothing + +instance (forall x. Ord (f x)) => OrdF (NodeContent arch f) where + compareF (NodeContent cctx1 x1) (NodeContent cctx2 x2) = lexCompareF x1 x2 $ fromOrdering (compare cctx1 cctx2) -type NodeEntry' arch (bin :: QuantK PB.WhichBinary) = NodeContent arch (Quant (PB.ConcreteBlock arch) bin) +type NodeEntry' arch = NodeContent arch (PB.ConcreteBlock arch) type NodeEntry arch = NodeEntry' arch ExistsK +instance Qu.ToQuant (Quant (PB.ConcreteBlock arch)) q q' => Qu.ToQuant (NodeEntry' arch) q q' where + toQuant f (NodeEntry cctx blks) = NodeEntry cctx (Qu.toQuant f blks) pattern NodeEntry :: CallingContext arch -> Quant (PB.ConcreteBlock arch) bin -> NodeEntry' arch bin pattern NodeEntry ctx bp = NodeContent ctx bp {-# COMPLETE NodeEntry #-} +nodeEntryRepr :: NodeEntry' arch qbin -> Qu.QuantRepr qbin +nodeEntryRepr ne = Qu.quantToRepr $ nodeBlocks ne nodeBlocks :: NodeEntry' arch bin -> Quant (PB.ConcreteBlock arch) bin nodeBlocks = nodeContent @@ -131,9 +152,12 @@ nodeBlocks = nodeContent graphNodeContext :: NodeEntry' arch bin -> CallingContext arch graphNodeContext = nodeContentCtx -type NodeReturn' arch bin = NodeContent arch (Quant (PB.FunctionEntry arch) bin) +type NodeReturn' arch = NodeContent arch (PB.FunctionEntry arch) type NodeReturn arch = NodeReturn' arch ExistsK +nodeReturnRepr :: NodeReturn' arch qbin -> Qu.QuantRepr qbin +nodeReturnRepr ne = Qu.quantToRepr $ nodeFuns ne + nodeFuns :: NodeReturn' arch bin -> Quant (PB.FunctionEntry arch) bin nodeFuns = nodeContent @@ -144,6 +168,9 @@ pattern NodeReturn :: CallingContext arch -> Quant (PB.FunctionEntry arch) bin - pattern NodeReturn ctx bp = NodeContent ctx bp {-# COMPLETE NodeReturn #-} +instance Qu.ToQuant (Quant (PB.FunctionEntry arch)) q q' => Qu.ToQuant (NodeReturn' arch) q q' where + toQuant f (NodeReturn cctx fns) = NodeReturn cctx (Qu.toQuant f fns) + graphNodeBlocks :: GraphNode' arch bin -> Quant (PB.ConcreteBlock arch) bin graphNodeBlocks (GraphNode ne) = nodeBlocks ne graphNodeBlocks (ReturnNode ret) = Qu.map PB.functionEntryToConcreteBlock (nodeFuns ret) @@ -404,49 +431,40 @@ instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "entryno -- | Equivalent to a 'NodeEntry' but necessarily a single-sided node. -- Converting a 'SingleNodeEntry' to a 'NodeEntry' is always defined, -- while converting a 'NodeEntry' to a 'SingleNodeEntry' is partial. -data SingleNodeEntry arch bin = - SingleNodeEntry - { singleEntryBin :: PB.WhichBinaryRepr bin - , _singleEntry :: NodeContent arch (PB.ConcreteBlock arch bin) - } -singleNodeAddr :: SingleNodeEntry arch bin -> PPa.WithBin (PAd.ConcreteAddress arch) bin -singleNodeAddr se = PPa.WithBin (singleEntryBin se) (PB.concreteAddress (singleNodeBlock se)) +type SingleNodeEntry arch bin = NodeEntry' arch (Qu.OneK bin) -mkSingleNodeEntry :: NodeEntry arch -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin -mkSingleNodeEntry node blk = SingleNodeEntry (PB.blockBinRepr blk) (NodeContent (graphNodeContext node) blk) +pattern SingleNodeEntry :: CallingContext arch -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin +pattern SingleNodeEntry cctx blk <- ((\l -> case l of NodeEntry cctx (Qu.Single _ blk) -> (cctx,blk)) -> (cctx,blk)) + where + SingleNodeEntry cctx blk = NodeEntry cctx (Qu.Single (PB.blockBinRepr blk) blk) -instance TestEquality (SingleNodeEntry arch) where - testEquality se1 se2 | EQF <- compareF se1 se2 = Just Refl - testEquality _ _ = Nothing +{-# COMPLETE SingleNodeEntry #-} -instance Eq (SingleNodeEntry arch bin) where - se1 == se2 = compare se1 se2 == EQ +singleEntryBin :: SingleNodeEntry arch bin -> PB.WhichBinaryRepr bin +singleEntryBin (nodeEntryRepr -> Qu.QuantOneRepr repr) = repr -instance Ord (SingleNodeEntry arch bin) where - compare (SingleNodeEntry _ se1) (SingleNodeEntry _ se2) = compare se1 se2 +singleNodeAddr :: SingleNodeEntry arch bin -> PPa.WithBin (PAd.ConcreteAddress arch) bin +singleNodeAddr se = PPa.WithBin (singleEntryBin se) (PB.concreteAddress (singleNodeBlock se)) -instance OrdF (SingleNodeEntry arch) where - compareF (SingleNodeEntry bin1 se1) (SingleNodeEntry bin2 se2) = - lexCompareF bin1 bin2 $ fromOrdering (compare se1 se2) +mkSingleNodeEntry :: NodeEntry' arch qbin -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin +mkSingleNodeEntry node blk = SingleNodeEntry (graphNodeContext node) blk -instance PA.ValidArch arch => Show (SingleNodeEntry arch bin) where - show e = show (singleToNodeEntry e) singleNodeDivergePoint :: SingleNodeEntry arch bin -> GraphNode arch -singleNodeDivergePoint (SingleNodeEntry _ (NodeContent cctx _)) = case divergePoint cctx of +singleNodeDivergePoint (NodeEntry cctx _) = case divergePoint cctx of Just dp -> dp Nothing -> panic Verifier "singleNodeDivergePoint" ["missing diverge point for SingleNodeEntry"] -asSingleNodeEntry :: PPa.PatchPairM m => NodeEntry arch -> m (Some (SingleNodeEntry arch)) -asSingleNodeEntry (NodeEntry cctx bPair) = do - Pair bin blk <- PPa.asSingleton bPair +asSingleNodeEntry :: PPa.PatchPairM m => NodeEntry' arch qbin -> m (Some (Qu.AsSingle (NodeEntry' arch))) +asSingleNodeEntry (NodeEntry cctx blks) = do + Pair _ blk <- PPa.asSingleton blks case divergePoint cctx of - Just{} -> return $ Some (SingleNodeEntry bin (NodeContent cctx blk)) + Just{} -> return $ Some (Qu.AsSingle $ SingleNodeEntry cctx blk) Nothing -> PPa.throwPairErr singleNodeBlock :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin -singleNodeBlock (SingleNodeEntry _ (NodeContent _ blk)) = blk +singleNodeBlock (SingleNodeEntry _ blk) = blk -- | Returns a 'SingleNodeEntry' for a given 'NodeEntry' if it has an entry -- for the given 'bin'. @@ -461,15 +479,14 @@ toSingleNodeEntry bin ne = do case toSingleNode bin ne of Just (NodeEntry cctx bPair) -> do blk <- PPa.get bin bPair - return $ SingleNodeEntry bin (NodeContent cctx blk) + return $ SingleNodeEntry cctx blk _ -> PPa.throwPairErr singleToNodeEntry :: SingleNodeEntry arch bin -> NodeEntry arch -singleToNodeEntry (SingleNodeEntry bin (NodeContent cctx v)) = - NodeEntry cctx (PPa.PatchPairSingle bin v) +singleToNodeEntry sne = Qu.toQuant Qu.QuantSomeRepr sne singleNodeDivergence :: SingleNodeEntry arch bin -> GraphNode arch -singleNodeDivergence (SingleNodeEntry _ (NodeContent cctx _)) = case divergePoint cctx of +singleNodeDivergence (SingleNodeEntry cctx _) = case divergePoint cctx of Just dp -> dp Nothing -> panic Verifier "singleNodeDivergence" ["Unexpected missing divergence point"] @@ -477,12 +494,10 @@ combineSingleEntries' :: SingleNodeEntry arch PB.Original -> SingleNodeEntry arch PB.Patched -> Maybe (NodeEntry arch) -combineSingleEntries' (SingleNodeEntry _ eO) (SingleNodeEntry _ eP) = do - GraphNode divergeO <- divergePoint $ nodeContentCtx eO - GraphNode divergeP <- divergePoint $ nodeContentCtx eP +combineSingleEntries' (SingleNodeEntry cctxO blksO) (SingleNodeEntry cctxP blksP) = do + GraphNode divergeO <- divergePoint $ cctxO + GraphNode divergeP <- divergePoint $ cctxP guard $ divergeO == divergeP - let blksO = nodeContent eO - let blksP = nodeContent eP return $ mkNodeEntry divergeO (PPa.PatchPair blksO blksP) -- | Create a combined two-sided 'NodeEntry' based on @@ -497,4 +512,13 @@ combineSingleEntries :: Maybe (NodeEntry arch) combineSingleEntries sne1 sne2 = case singleEntryBin sne1 of PB.OriginalRepr -> combineSingleEntries' sne1 sne2 - PB.PatchedRepr -> combineSingleEntries' sne2 sne1 \ No newline at end of file + PB.PatchedRepr -> combineSingleEntries' sne2 sne1 + +type SingleNodeReturn arch bin = NodeReturn' arch (Qu.OneK bin) + +pattern SingleNodeReturn :: CallingContext arch -> PB.FunctionEntry arch bin -> SingleNodeReturn arch bin +pattern SingleNodeReturn cctx fn <- ((\l -> case l of NodeReturn cctx (Qu.Single _ fn) -> (cctx,fn)) -> (cctx,fn)) + where + SingleNodeReturn cctx fn = NodeReturn cctx (Qu.Single (PB.functionBinRepr fn) fn) + +type SingleGraphNode arch bin = GraphNode' arch (Qu.OneK bin) \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 7bf5456a..d4f7daf4 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -60,6 +60,7 @@ import qualified Data.Parameterized.TraversableF as TF import qualified Data.Parameterized.TraversableFC as TFC import Data.Parameterized.Nonce import qualified Data.Parameterized.Context as Ctx +import qualified Data.Quant as Qu import qualified What4.Expr as W4 import qualified What4.Interface as W4 @@ -761,7 +762,7 @@ withWorkItem gr0 f = do let nd = workItemNode wi res <- subTraceLabel @"node" (printPriorityKind priority) nd $ atPriority priority Nothing $ do (mnext, gr2) <- case wi of - ProcessNode (GraphNode ne) | Just (Some sne) <- asSingleNodeEntry ne -> do + ProcessNode (GraphNode ne) | Just (Some (Qu.AsSingle sne)) <- asSingleNodeEntry ne -> do (evalPG gr1 $ isSyncNode sne) >>= \case True -> do gr2 <- execPG gr1 $ queueExitMerges (\pk -> mkPriority pk priority) (SyncAtStart sne)