Refactoring to support control sync rework

.github/workflows/main.yml

@@ -190,7 +190,7 @@ jobs:
     - name: Test
       if: runner.os == 'Linux'
       run: |
-        cabal test pkg:pate
+        cabal test pkg:pate --test-options="-t 1200s"
 
     - name: Docs
       run: cabal haddock pkg:pate

src/Data/Parameterized/PairF.hs

@@ -15,6 +15,7 @@ module Data.Parameterized.PairF
   ) where
 
 import           Data.Kind (Type)
+import Data.Parameterized.Classes
 
 data PairF tp1 tp2 k = PairF (tp1 k) (tp2 k)
 
@@ -26,6 +27,22 @@ type instance TupleF '(a,b,c,d) = PairF a (PairF b (PairF c d))
 pattern TupleF2 :: a k -> b k -> TupleF '(a,b) k
 pattern TupleF2 a b = PairF a b
 
+instance (TestEquality a, TestEquality b) => TestEquality (PairF a b) where
+  testEquality (PairF a1 b1) (PairF a2 b2) = 
+    case (testEquality a1 a2, testEquality b1 b2) of
+      (Just Refl, Just Refl) -> Just Refl
+      _ -> Nothing
+
+instance (OrdF a, OrdF b) => OrdF (PairF a b) where
+  compareF (PairF a1 b1) (PairF a2 b2) = 
+    lexCompareF a1 a2 $ compareF b1 b2
+
+instance (Eq (a tp), Eq (b tp)) => Eq ((PairF a b) tp) where
+  (PairF a1 b1) == (PairF a2 b2) = a1 == a2 && b1 == b2
+
+instance (Ord (a tp), Ord (b tp)) => Ord ((PairF a b) tp) where
+  compare (PairF a1 b1) (PairF a2 b2) = compare a1 a2 <> compare b1 b2
+
 {-# COMPLETE TupleF2 #-}
 
 pattern TupleF3 :: a k -> b k -> c k -> TupleF '(a,b,c) k

src/Data/Parameterized/SetF.hs

@@ -43,10 +43,14 @@ module Data.Parameterized.SetF
   , union
   , unions
   , null
+  , toSet
+  , fromSet
+  , map
   , ppSetF
   ) where
 
-import Prelude hiding (filter, null)
+import Prelude hiding (filter, null, map)
+import qualified Data.List as List
 import           Data.Parameterized.Classes
 import qualified Data.Foldable as Foldable
 
@@ -55,6 +59,7 @@ import           Prettyprinter ( (<+>) )
 
 import           Data.Set (Set)
 import qualified Data.Set as S
+import Unsafe.Coerce (unsafeCoerce)
 
 newtype AsOrd f tp where
   AsOrd :: { unAsOrd :: f tp } -> AsOrd f tp
@@ -91,13 +96,13 @@ insert e (SetF es) = SetF (S.insert (AsOrd e) es)
 toList ::
   SetF f tp ->
   [f tp]
-toList (SetF es) = map unAsOrd $ S.toList es
+toList (SetF es) = List.map unAsOrd $ S.toList es
 
 fromList ::
   OrdF f =>
   [f tp] ->
   SetF f tp
-fromList es = SetF $ S.fromList (map AsOrd es)
+fromList es = SetF $ S.fromList (List.map AsOrd es)
 
 member ::
   OrdF f =>
@@ -130,6 +135,25 @@ null ::
   SetF f tp -> Bool
 null (SetF es) = S.null es
 
+-- | Convert a 'SetF' to a 'Set', under the assumption
+--   that the 'OrdF' and 'Ord' instances are consistent.
+--   This uses coercion rather than re-building the set,
+--   which is sound given the above assumption.
+toSet ::
+  (OrdF f, Ord (f tp)) => SetF f tp -> Set (f tp)
+toSet (SetF s) = unsafeCoerce s
+
+-- | Convert a 'Set' to a 'SetF', under the assumption
+--   that the 'OrdF' and 'Ord' instances are consistent.
+--   This uses coercion rather than re-building the set,
+--   which is sound given the above assumption.
+fromSet :: (OrdF f, Ord (f tp)) => Set (f tp) -> SetF f tp
+fromSet s = SetF (unsafeCoerce s)
+
+map ::
+  (OrdF g) => (f tp -> g tp) -> SetF f tp -> SetF g tp
+map f (SetF s) = SetF (S.map (\(AsOrd v) -> AsOrd (f v)) s)  
+
 ppSetF ::
   (f tp -> PP.Doc a) ->
   SetF f tp ->

src/Data/RevMap.hs

@@ -1,4 +1,6 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-|
 Module           : Data.RevMap
 Copyright        : (c) Galois, Inc 2023
@@ -19,9 +21,10 @@ module Data.RevMap
   , alter
   , insertWith
   , findFirst
+  , filter
   ) where
 
-import Prelude hiding (lookup)
+import Prelude hiding (lookup, filter)
 
 import qualified Data.Set as Set
 import           Data.Set (Set)
@@ -76,6 +79,13 @@ delete a m@(RevMap a_to_b b_to_a) = case Map.lookup a a_to_b of
   Just b -> reverseAdjust b (Set.delete a) (RevMap (Map.delete a a_to_b) b_to_a)
   Nothing -> m
 
+filter :: forall a b. (a -> b -> Bool) -> RevMap a b -> RevMap a b
+filter f (RevMap a_to_b b_to_a) = 
+  RevMap (Map.filterWithKey f a_to_b) (Map.mapMaybeWithKey g b_to_a)
+  where
+    g :: b -> Set a -> Maybe (Set a)
+    g b as = let as' = Set.filter (\a -> f a b) as
+      in if Set.null as' then Nothing else Just as'
 
 alter :: (Ord a, Ord b) => (Maybe b -> Maybe b) -> a -> RevMap a b -> RevMap a b
 alter f a m@(RevMap a_to_b b_to_as) = case Map.lookup a a_to_b of

src/Pate/Binary.hs

@@ -29,8 +29,11 @@ module Pate.Binary
   , Patched
   , WhichBinaryRepr(..)
   , OtherBinary
+  , binCases
   , flipRepr
-  , short)
+  , short
+  , otherInvolutive
+  )
 where
 
 import           Data.Parameterized.WithRepr
@@ -50,16 +53,27 @@ data WhichBinaryRepr (bin :: WhichBinary) where
   OriginalRepr :: WhichBinaryRepr 'Original
   PatchedRepr :: WhichBinaryRepr 'Patched
 
-type family OtherBinary (bin :: WhichBinary) :: WhichBinary
+type family OtherBinary (bin :: WhichBinary) :: WhichBinary where
+  OtherBinary Original = Patched
+  OtherBinary Patched = Original
 
-type instance OtherBinary Original = Patched
-type instance OtherBinary Patched = Original
+otherInvolutive :: WhichBinaryRepr bin -> (OtherBinary (OtherBinary bin) :~: bin)
+otherInvolutive bin = case binCases bin (flipRepr bin) of
+  Left Refl -> Refl
+  Right Refl -> Refl
 
 flipRepr :: WhichBinaryRepr bin -> WhichBinaryRepr (OtherBinary bin)
 flipRepr = \case
   OriginalRepr -> PatchedRepr
   PatchedRepr -> OriginalRepr
 
+binCases :: WhichBinaryRepr bin1 -> WhichBinaryRepr bin2 -> Either (bin1 :~: bin2) ('(bin1, bin2) :~: '(OtherBinary bin2, OtherBinary bin1))
+binCases bin1 bin2 = case (bin1, bin2) of
+  (OriginalRepr, OriginalRepr) -> Left Refl
+  (OriginalRepr, PatchedRepr) -> Right Refl
+  (PatchedRepr, PatchedRepr) -> Left Refl
+  (PatchedRepr, OriginalRepr) -> Right Refl
+
 short :: WhichBinaryRepr bin -> String
 short OriginalRepr = "O"
 short PatchedRepr = "P"

src/Pate/Equivalence/Error.hs

@@ -166,10 +166,11 @@ data InnerEquivalenceError arch
   | UninterpretedInstruction
   | FailedToResolveAddress (MM.MemWord (MM.ArchAddrWidth arch))
   | forall tp. FailedToGroundExpr (SomeExpr tp)
-  | OrphanedSingletonAnalysis (PB.FunPair arch)
+  | OrphanedSinglesidedAnalysis (PB.FunPair arch)
   | RequiresInvalidPointerOps
   | PairGraphError PairGraphErr
   | forall e. X.Exception e => UnhandledException e
+  | IncompatibleSingletonNodes (PB.ConcreteBlock arch PBi.Original) (PB.ConcreteBlock arch PBi.Patched)
   | SolverError X.SomeException
 
 errShortName :: MS.SymArchConstraints arch => InnerEquivalenceError arch -> String
@@ -230,7 +231,7 @@ isRecoverable' e = case e of
   BlockHasNoExit{} -> True
   OrphanedFunctionReturns{} -> True
   CallReturnsToFunctionEntry{} -> True
-  OrphanedSingletonAnalysis{} -> True
+  OrphanedSinglesidedAnalysis{} -> True
   UnsatisfiableEquivalenceCondition{} -> True
   _ -> False
 

src/Pate/Monad/Environment.hs

@@ -134,6 +134,7 @@ data NodePriorityK =
   | PriorityDeferredPropagation
   | PriorityDomainRefresh
   | PriorityHandleReturn
+  | PriorityHandleMerge
   | PriorityMiscCleanup
   | PriorityDeferred
   deriving (Eq, Ord)
@@ -153,6 +154,7 @@ printPriorityKind (NodePriority pk _ _ ) = case pk of
   PriorityDeferredPropagation -> "Propagating Deferred Conditions"
   PriorityDomainRefresh -> "Re-checking Equivalence Domains"
   PriorityHandleReturn -> "Handling Function Return"
+  PriorityHandleMerge -> "Handling Control Flow Merge"
   PriorityMiscCleanup -> "Proof Cleanup"
   PriorityDeferred -> "Handling Deferred Decisions"
 

src/Pate/Monad/PairGraph.hs

@@ -6,10 +6,17 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE PolyKinds #-}
 
 -- EquivM operations on a PairGraph
 module Pate.Monad.PairGraph 
   ( withPG
+  , evalPG
   , withPG_
   , liftPG
   , catchPG
@@ -23,6 +30,9 @@ module Pate.Monad.PairGraph
   , considerDesyncEvent
   , addLazyAction
   , queuePendingNodes
+  , runPG
+  , execPG
+  , liftPartEqM_
   ) where
 
 import           Control.Monad.State.Strict
@@ -52,44 +62,93 @@ import qualified Pate.Equivalence.Condition as PEC
 import qualified Data.Macaw.CFG as MM
 import qualified Data.Map as Map
 import qualified Pate.Equivalence.Error as PEE
+import GHC.Stack (HasCallStack)
+import qualified Prettyprinter as PP
+
 
+instance IsTraceNode (k :: l) "pg_trace" where
+  type TraceNodeType k "pg_trace" = [String]
+  prettyNode () msgs = PP.vsep (map PP.viaShow msgs)
+  nodeTags = mkTags @k @"pg_trace" [Custom "debug"]
+
+emitPGTrace :: [String] -> EquivM sym arch ()
+emitPGTrace [] = return ()
+emitPGTrace l = emitTrace @"pg_trace" l
 
 withPG :: 
+  HasCallStack =>
   PairGraph sym arch -> 
   StateT (PairGraph sym arch) (EquivM_ sym arch) a ->
   EquivM sym arch (a, PairGraph sym arch)
 withPG pg f = runStateT f pg 
 
+evalPG :: 
+  HasCallStack =>
+  PairGraph sym arch -> 
+  PairGraphM sym arch a ->
+  EquivM sym arch a
+evalPG pg f = fst <$> (withPG pg $ liftPG f) 
+
+execPG :: HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM_ sym arch (PairGraph sym arch)
+execPG pg f = snd <$> runPG pg f
+
 withPG_ :: 
+  HasCallStack =>
   PairGraph sym arch -> 
   StateT (PairGraph sym arch) (EquivM_ sym arch) a ->
   EquivM sym arch (PairGraph sym arch)
 withPG_ pg f = execStateT f pg
 
-liftPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a
+liftPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a
 liftPG f = do
   pg <- get
-  case runPairGraphM pg f of
-    Left err -> lift $ throwHere $ PEE.PairGraphError err
-    Right (a,pg') -> do
-      put pg'
-      return a
+  env <- lift $ ask
+  withValidEnv env $ 
+    case runPairGraphMLog pg f of
+      (l, Left err) -> do
+        lift $ emitPGTrace l
+        lift $ throwHere $ PEE.PairGraphError err
+      (l, Right (a,pg')) -> do
+        lift $ emitPGTrace l
+        put pg'
+        return a
 
-catchPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a)
+runPG :: HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM_ sym arch (a, PairGraph sym arch)
+runPG pg f = withValid $ case runPairGraphMLog pg f of
+  (l, Left err) -> do
+    emitPGTrace l
+    throwHere $ PEE.PairGraphError err
+  (l, Right a) -> do
+    emitPGTrace l
+    return a
+
+catchPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a)
 catchPG f = do
   pg <- get
-  case runPairGraphM pg f of
-    Left{} -> return Nothing
-    Right (a,pg') -> do
-      put pg'
-      return $ Just a
+  env <- lift $ ask
+  withValidEnv env $ 
+    case runPairGraphMLog pg f of
+      (l, Left{}) -> (lift $ emitPGTrace l) >> return Nothing
+      (l, Right (a,pg')) -> do
+        lift $ emitPGTrace l
+        put pg'
+        return $ Just a
 
 liftEqM_ :: 
+  HasCallStack =>
   (PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch)) -> 
   StateT (PairGraph sym arch) (EquivM_ sym arch) ()
 liftEqM_ f = liftEqM $ \pg -> ((),) <$> (f pg)
 
+liftPartEqM_ :: 
+  (PairGraph sym arch -> EquivM_ sym arch (Maybe (PairGraph sym arch))) -> 
+  StateT (PairGraph sym arch) (EquivM_ sym arch) Bool
+liftPartEqM_ f = liftEqM $ \pg -> f pg >>= \case
+  Just pg' -> return (True, pg')
+  Nothing -> return (False, pg)
+
 liftEqM :: 
+  HasCallStack =>
   (PairGraph sym arch -> EquivM_ sym arch (a, PairGraph sym arch)) -> 
   StateT (PairGraph sym arch) (EquivM_ sym arch) a
 liftEqM f = do