Merge pull request #450 from GaloisInc/issue-448

Issue 448

pate.cabal

@@ -114,6 +114,7 @@ library
                        Pate.Verification.DemandDiscovery,
                        Pate.Verification.Domain,
                        Pate.Verification.ExternalCall,
+                       Pate.Verification.FnBindings,
                        Pate.Verification.InlineCallee,
                        Pate.Verification.MemoryLog,
                        Pate.Verification.Override,

src/Data/Parameterized/SetF.hs

@@ -47,12 +47,14 @@ module Data.Parameterized.SetF
   , fromSet
   , map
   , ppSetF
+  , asSet
   ) where
 
 import Prelude hiding (filter, null, map)
 import qualified Data.List as List
 import           Data.Parameterized.Classes
 import qualified Data.Foldable as Foldable
+import qualified Control.Lens as L
 
 import qualified Prettyprinter as PP
 import           Prettyprinter ( (<+>) )
@@ -150,6 +152,11 @@ toSet (SetF s) = unsafeCoerce s
 fromSet :: (OrdF f, Ord (f tp)) => Set (f tp) -> SetF f tp
 fromSet s = SetF (unsafeCoerce s)
 
+asSet ::
+  (OrdF f, Ord (f tp)) =>
+  L.Lens' (SetF f tp) (Set (f tp))
+asSet f sf = fmap fromSet (f (toSet sf))
+
 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)  

src/Data/Parameterized/TotalMapF.hs

@@ -32,6 +32,7 @@ module Data.Parameterized.TotalMapF
     , zip
     , mapWithKey
     , traverseWithKey
+    , toList
   ) where
 
 import           Prelude hiding ( zip )

src/Pate/AssumptionSet.hs

@@ -138,6 +138,11 @@ instance OrdF (W4.SymExpr sym) => PEM.ExprMappable sym (AssumptionSet sym) where
         return $ MapF.singleton k' v'
     return $ mkAssumptionSet sym ps' (foldr (mergeExprSetFMap (Proxy @sym)) MapF.empty bs')
 
+instance PEM.ExprFoldable sym (AssumptionSet sym) where
+  foldExpr sym f (AssumptionSet ps bs) acc =
+    PEM.withSymExprFoldable @W4.BaseBoolType sym $
+      PEM.foldExpr sym f ps acc >>= PEM.foldExpr sym f bs
+
 instance forall sym. W4S.SerializableExprs sym => W4S.W4Serializable sym (AssumptionSet sym) where
   w4Serialize (AssumptionSet ps bs) | SetF.null ps, MapF.null bs = W4S.w4Serialize True
   w4Serialize (AssumptionSet ps bs) | [p] <- SetF.toList ps, MapF.null bs = W4S.w4SerializeF p
@@ -166,6 +171,11 @@ data NamedAsms sym (nm :: Symbol) =
 instance W4S.SerializableExprs sym => W4S.W4Serializable sym (NamedAsms sym nm) where
   w4Serialize (NamedAsms asm) = W4S.w4Serialize asm
 
+instance PEM.ExprFoldable sym (NamedAsms sym nm) where
+  foldExpr sym f (NamedAsms asm) acc = PEM.foldExpr sym f asm acc
+
+instance PEM.ExprFoldableF sym (NamedAsms sym)
+
 instance PEM.ExprMappable sym (NamedAsms sym nm) where
   mapExpr sym f (NamedAsms asm) = NamedAsms <$> PEM.mapExpr sym f asm
 

src/Pate/Equivalence/Condition.hs

@@ -148,6 +148,13 @@ instance PEM.ExprMappable sym (EquivalenceCondition sym arch v) where
     <*> PEM.mapExpr sym f c
     <*> PEM.mapExpr sym f d
 
+instance PEM.ExprFoldableF sym (MM.ArchReg arch) => PEM.ExprFoldable sym (EquivalenceCondition sym arch v) where
+  foldExpr sym f (EquivalenceCondition a b c d) acc =
+        PEM.foldExpr sym f a acc
+    >>= PEM.foldExpr sym f b
+    >>= PEM.foldExpr sym f c
+    >>= PEM.foldExpr sym f d
+
 instance PS.Scoped (EquivalenceCondition sym arch) where
   unsafeCoerceScope (EquivalenceCondition a b c d) = EquivalenceCondition a (PS.unsafeCoerceScope b) c d
 
@@ -234,6 +241,10 @@ instance PS.Scoped (RegisterCondition sym arch) where
 instance PEM.ExprMappable sym (RegisterCondition sym arch v) where
   mapExpr sym f (RegisterCondition cond) = RegisterCondition <$> MM.traverseRegsWith (\_ -> PEM.mapExpr sym f) cond
 
+instance PEM.ExprFoldableF sym (MM.ArchReg arch) => PEM.ExprFoldable sym (RegisterCondition sym arch v) where
+  foldExpr sym f (RegisterCondition cond) = PEM.foldExpr sym f (MM.regStateMap cond)
+
+
 trueRegCond ::
   W4.IsSymExprBuilder sym =>
   PA.ValidArch arch =>

src/Pate/ExprMappable.hs

@@ -30,6 +30,7 @@ module Pate.ExprMappable (
   , withExprFoldable
   , ExprFoldableFC
   , ExprFoldableIO(..)
+  , withSymExprFoldable
   , SkipTransformation(..)
   , ToExprMappable(..)
   , SymExprMappable(..)
@@ -70,6 +71,7 @@ import qualified Lang.Crucible.Utils.MuxTree as MT
 import           Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.TraversableF as TF
+import qualified Data.Parameterized.TraversableFC as TFC
 import Data.Text
 import Control.Monad (forM, foldM)
 import Data.Kind (Type)
@@ -414,6 +416,9 @@ withExprFoldable ::
   (ExprFoldable sym (f tp) => a) -> a
 withExprFoldable f = withExprFoldable_ (Proxy @sym) (Proxy @f) (Proxy @tp) f
 
+instance forall sym f. ExprFoldableF sym f => ExprFoldable sym (Some f) where
+  foldExpr sym f (Some (a :: f tp)) b = withExprFoldable @sym @f @tp $ foldExpr sym f a b
+
 class (forall sym. ExprFoldableF sym f) => ExprFoldableFC f where
 
 instance (Ord f, ExprMappable sym f) => ExprMappable sym (MT.MuxTree sym f) where
@@ -456,15 +461,37 @@ instance ExprFoldable sym f => ExprFoldable sym (Maybe f) where
   foldExpr sym f (Just e) b0 = foldExpr sym f e b0
   foldExpr _ _ Nothing b0 = return b0
 
-instance (ExprFoldable sym f) => ExprFoldable sym (MT.MuxTree sym f) where
-  foldExpr sym f mt b0 | SymExprFoldable aEF <- symExprFoldable sym = aEF @WI.BaseBoolType $ foldExpr sym f (MT.viewMuxTree mt) b0
+instance forall sym f. (ExprFoldable sym f) => ExprFoldable sym (MT.MuxTree sym f) where
+  foldExpr sym f mt b0 | SymExprFoldable aEF <- symExprFoldable sym =
+    aEF $ withExprFoldable @sym @(WI.SymExpr sym) @WI.BaseBoolType $ foldExpr sym f (MT.viewMuxTree mt) b0
+
+instance forall sym f ctx. ExprFoldableF sym f => ExprFoldable sym (Ctx.Assignment f ctx) where
+  foldExpr sym f asn b0 = TFC.foldrMFC (\(a :: f x) b -> withExprFoldable @sym @f @x $ foldExpr sym f a b) b0 asn
+
+instance forall sym f k. (ExprFoldable sym f) => ExprFoldable sym (WPM.PredMap sym f k) where
+  foldExpr sym f pm b = withSymExprFoldable @WI.BaseBoolType sym $
+    WPM.foldMWithKey pm (\k v b_ -> foldExpr sym f k b_ >>= foldExpr sym f v) b
+
+instance ExprFoldable sym f => ExprFoldable sym ((Const f) tp)  where
+  foldExpr sym f (Const e) b = foldExpr sym f e b
+
+instance ExprFoldable sym f => ExprFoldableF sym (Const f)
+
+instance ExprFoldable sym (f tp) => ExprFoldable sym (SetF.SetF f tp) where
+  foldExpr sym f s b = foldExpr sym f (SetF.toList s) b
+
+instance forall sym f. ExprFoldableF sym f => ExprFoldableF sym (SetF.SetF f) where
+  withExprFoldable_ psym _pf ptp f =
+     withExprFoldable_ psym (Proxy @f) ptp f
 
 newtype ToExprFoldable sym tp = ToExprFoldable { unEF :: WI.SymExpr sym tp }
 
 instance ExprFoldable sym (ToExprFoldable sym tp) where
   foldExpr _sym f (ToExprFoldable e) b = f e b
 
-newtype SymExprFoldable sym f = SymExprFoldable (forall tp a. ((ExprFoldable sym (f tp)) => a) -> a)
+instance ExprFoldableF sym (ToExprFoldable sym)
+
+newtype SymExprFoldable sym f = SymExprFoldable (forall a. ((ExprFoldableF sym f) => a) -> a)
 
 -- Same approach for 'symExprMappable' to create ExprFoldable instances for SymExpr
 symExprFoldable ::
@@ -474,4 +501,10 @@ symExprFoldable ::
 symExprFoldable _sym =
   unsafeCoerce r
   where r :: SymExprFoldable sym (ToExprFoldable sym)
-        r = SymExprFoldable (\a -> a)
+        r = SymExprFoldable (\a -> a)
+
+withSymExprFoldable ::
+  forall tp sym a.
+  sym ->
+  ((ExprFoldableF sym (WI.SymExpr sym), ExprFoldable sym (WI.SymExpr sym tp)) => a) -> a
+withSymExprFoldable sym f | SymExprFoldable aEF <- symExprFoldable sym = aEF $ withExprFoldable @sym @(WI.SymExpr sym) @tp f

src/Pate/Location.hs

@@ -287,6 +287,9 @@ instance Ord (SomeLocation sym arch) where
             LTF -> LT
             GTF -> GT
 
+instance forall sym arch. PEM.ExprMappable sym (SomeLocation sym arch) where
+  mapExpr sym f (SomeLocation l) = SomeLocation <$> PEM.mapExpr sym f l
+
 instance (W4.IsSymExprBuilder sym, MM.RegisterInfo (MM.ArchReg arch)) => IsTraceNode '(sym :: DK.Type,arch :: DK.Type) "loc" where
   type TraceNodeType '(sym,arch) "loc" = SomeLocation sym arch
   prettyNode () (SomeLocation l) = PP.pretty (showLoc l) PP.<> ":" PP.<+> PP.pretty l

src/Pate/MemCell.hs

@@ -180,6 +180,12 @@ instance PEM.ExprMappable sym (MemCell sym arch w) where
     ptr' <- WEH.mapExprPtr sym f ptr
     return $ MemCell ptr' w end
 
+instance PEM.ExprFoldable sym (MemCell sym arch w) where
+  foldExpr _sym f (MemCell (CLM.LLVMPointer reg off) _w _end) b =
+    f (WI.natToIntegerPure reg) b >>= f off
+
+instance PEM.ExprFoldableF sym (MemCell sym arch)
+
 ppCell :: (WI.IsExprBuilder sym) => MemCell sym arch w -> PP.Doc a
 ppCell cell =
   let CLM.LLVMPointer reg off = cellPtr cell

src/Pate/Monad.hs

@@ -613,8 +613,7 @@ withSimSpec ::
   EquivM sym arch (SimSpec sym arch g)
 withSimSpec blocks spec f = withSym $ \sym -> do
   spec_fresh <- withFreshVars blocks $ \vars -> liftIO $ bindSpec sym vars spec
-  forSpec spec_fresh $ \scope body ->
-    withAssumptionSet (scopeAsm scope) (f scope body)
+  forSpec spec_fresh $ \scope body -> (f scope body)
 
 lookupArgumentNamesSingle
   :: PBi.WhichBinaryRepr bin
@@ -654,14 +653,13 @@ currentAsm = CMR.asks envCurrentFrame
 
 withFreshScope ::
   forall sym arch f.
-  Scoped f =>
   PB.BlockPair arch ->
-  (forall v. SimScope sym arch v -> EquivM sym arch (f v)) ->
-  EquivM sym arch (SimSpec sym arch f)
+  (forall v. SimScope sym arch v -> EquivM sym arch f) ->
+  EquivM sym arch f
 withFreshScope bPair f = do
   dummy_spec <- withFreshVars @sym @arch @(WithScope ()) bPair $ \_ -> do
-    return (mempty, WithScope ())
-  forSpec dummy_spec $ \scope _ -> f scope
+    return (WithScope ())
+  fmap (\x -> viewSpecBody x unWS) $ forSpec dummy_spec $ \scope _ -> WithScope <$> f scope
 
 -- | Create a new 'SimSpec' by evaluating the given function under a fresh set
 -- of bound variables. The returned 'AssumptionSet' is set as the assumption
@@ -670,7 +668,7 @@ withFreshVars ::
   forall sym arch f.
   Scoped f =>
   PB.BlockPair arch ->
-  (forall v. (SimVars sym arch v PBi.Original, SimVars sym arch v PBi.Patched) -> EquivM sym arch (AssumptionSet sym,(f v))) ->
+  (forall v. (SimVars sym arch v PBi.Original, SimVars sym arch v PBi.Patched) -> EquivM sym arch (f v)) ->
   EquivM sym arch (SimSpec sym arch f)
 withFreshVars blocks f = do
   argNames <- lookupArgumentNames blocks

src/Pate/Monad/PairGraph.hs

@@ -33,6 +33,7 @@ module Pate.Monad.PairGraph
   , runPG
   , execPG
   , liftPartEqM_
+  , lookupFnBindings
   ) where
 
 import           Control.Monad.State.Strict
@@ -42,8 +43,10 @@ import           Control.Monad (foldM, forM_)
 import qualified Control.Monad.IO.Unlift as IO
 import           Data.Functor.Const
 import           Data.Maybe (fromMaybe)
+import           Control.Lens ( (&), (.~), (^.), (%~) )
 
 import qualified Data.Parameterized.TraversableF as TF
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Some
 
 import           SemMC.Formula.Env (SomeSome(..))
@@ -65,6 +68,10 @@ import qualified Pate.Equivalence.Error as PEE
 import GHC.Stack (HasCallStack)
 import qualified Prettyprinter as PP
 import qualified What4.Interface as W4
+import qualified Pate.Verification.FnBindings as PFn
+import qualified What4.Concrete as W4
+import qualified Data.Quant as Qu
+
 
 instance IsTraceNode (k :: l) "pg_trace" where
   type TraceNodeType k "pg_trace" = [String]
@@ -201,14 +208,11 @@ initialDomainSpec ::
   GraphNode arch ->
   EquivM sym arch (PAD.AbstractDomainSpec sym arch)
 initialDomainSpec (GraphNodeEntry blocks) = withTracing @"function_name" "initialDomainSpec" $ 
-  withFreshVars blocks $ \_vars -> do
-    dom <- initialDomain
-    return (mempty, dom)
+  withFreshVars blocks $ \_vars -> initialDomain
 initialDomainSpec (GraphNodeReturn fPair) = withTracing @"function_name" "initialDomainSpec" $ do
   let blocks = PPa.map PB.functionEntryToConcreteBlock fPair
-  withFreshVars blocks $ \_vars -> do
-    dom <- initialDomain
-    return (mempty, dom)
+  withFreshVars blocks $ \_vars -> initialDomain
+
 
 getScopedCondition ::
   PS.SimScope sym arch v ->
@@ -218,7 +222,7 @@ getScopedCondition ::
   EquivM sym arch (PEC.EquivalenceCondition sym arch v)
 getScopedCondition scope pg nd condK = withSym $ \sym -> case getCondition pg nd condK of
   Just condSpec -> do
-    (_, eqCond) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) condSpec
+    eqCond <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) condSpec
     return eqCond
   Nothing -> return $ PEC.universal sym
 
@@ -324,3 +328,14 @@ runPendingActions lens edge result pg0 = do
   case didchange of
     True -> return $ Just pg1
     False -> return Nothing
+
+lookupFnBindings ::
+  PS.SimScope sym arch v ->
+  SingleGraphNode arch bin ->
+  PairGraph sym arch ->
+  EquivM sym arch (Maybe (PFn.FnBindings sym bin v))
+lookupFnBindings scope sne pg = withSym $ \sym -> case MapF.lookup (Qu.AsSingle sne) (pg ^. (syncData dp . syncBindings)) of
+  Just (PS.AbsT bindsSpec) -> Just <$> (IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) bindsSpec)
+  Nothing -> return Nothing
+  where
+    dp = singleNodeDivergePoint sne