diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs index 4f69afc39..26ed28926 100644 --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -595,8 +595,8 @@ genCProg cfg fn proto (Result pinfo kindInfo _tvals _ovals cgs topInps (_, preCo where static = if location == -1 then text "static" else empty location = maximum (-1 : map getNodeId elts) - getNodeId s@(SV _ (NodeId (_, n))) | isConst s = -1 - | True = n + getNodeId s@(SV _ (NodeId (_, _, n))) | isConst s = -1 + | True = n genAsgn :: (SV, SBVExpr) -> (Int, Doc) genAsgn (sv, n) = (getNodeId sv, ppExpr cfg consts n (declSV typeWidth sv) (declSVNoConst typeWidth sv) P.<> semi) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 79d8b2f48..12dd7e9ab 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -75,13 +75,15 @@ import Control.Monad.Trans.Maybe (MaybeT) import Control.Monad.Writer.Strict (MonadWriter) import Data.Char (isAlpha, isAlphaNum, toLower) import Data.IORef (IORef, newIORef, readIORef) -import Data.List (intercalate, sortBy, isPrefixOf, isSuffixOf) +import Data.List (intercalate, sortBy, isPrefixOf, isSuffixOf, nub) import Data.Maybe (fromMaybe, mapMaybe) import Data.String (IsString(fromString)) import Data.Kind (Type) import Data.Time (getCurrentTime, UTCTime) +import Data.Int (Int64) + import GHC.Stack import GHC.Generics (Generic) @@ -91,14 +93,16 @@ import qualified Control.Monad.Writer.Lazy as LW import qualified Control.Monad.Writer.Strict as SW import qualified Data.IORef as R (modifyIORef') import qualified Data.Generics as G (Data(..)) +import qualified Data.Generics.Uniplate.Data as G import qualified Data.IntMap.Strict as IMap (IntMap, empty, toAscList, lookup, insertWith) -import qualified Data.Map.Strict as Map (Map, empty, toList, lookup, insert, size) +import qualified Data.Map.Strict as Map (Map, empty, toList, lookup, insert, size, elems) import qualified Data.Set as Set (Set, empty, toList, insert, member) import qualified Data.Foldable as F (toList) import qualified Data.Sequence as S (Seq, empty, (|>), (<|), lookup, elemIndexL) import qualified Data.Text as T import System.Mem.StableName +import System.Random import Data.SBV.Core.Kind import Data.SBV.Core.Concrete @@ -112,13 +116,30 @@ import Data.SBV.Control.Types import Control.Monad.Fail as Fail #endif +-- | Context identifier. 0 is reserved global context +newtype SBVContext = SBVContext Int64 deriving (Eq, Ord, G.Data, Show) + +-- | Global context +globalSBVContext :: SBVContext +globalSBVContext = SBVContext 0 + +-- | Generate context. We make sure it isn't 0, i.e., the global context +-- The "hope" here is that each time we call this we get a different context number. +-- A random number doesn't necessarily have to do that, but I think the pseudo-generator +-- has a large enough period for this to go through OK. +genSBVContext :: IO SBVContext +genSBVContext = do ctx <- SBVContext <$> randomIO + if ctx == globalSBVContext -- unlikely, but possible + then genSBVContext + else pure ctx + -- | A symbolic node id -newtype NodeId = NodeId { getId :: (Int, Int) } -- Lambda-level, and node-id +newtype NodeId = NodeId { getId :: (SBVContext, Int, Int) } -- Lambda-level, and node-id deriving (Ord, G.Data) -- Equality is pair-wise, except we accommodate for negative node-id; which is reserved for true/false instance Eq NodeId where - NodeId n1@(_, i) == NodeId n2@(_, j) + NodeId n1@(_, _, i) == NodeId n2@(_, _, j) | i < 0 && j < 0 = i == j | True @@ -140,10 +161,10 @@ instance HasKind SV where kindOf (SV k _) = k instance Show SV where - show (SV _ (NodeId (l, n))) = case n of - -2 -> "false" - -1 -> "true" - _ -> prefix ++ 's' : show n + show (SV _ (NodeId (_, l, n))) = case n of + -2 -> "false" + -1 -> "true" + _ -> prefix ++ 's' : show n where prefix = case l of 0 -> "" _ -> 'l' : show l ++ "_" @@ -164,11 +185,11 @@ forceSVArg (SV k n) = k `seq` n `seq` return () -- | Constant False as an 'SV'. Note that this value always occupies slot -2 and level 0. falseSV :: SV -falseSV = SV KBool $ NodeId (0, -2) +falseSV = SV KBool $ NodeId (globalSBVContext, 0, -2) -- | Constant True as an 'SV'. Note that this value always occupies slot -1 and level 0. trueSV :: SV -trueSV = SV KBool $ NodeId (0, -1) +trueSV = SV KBool $ NodeId (globalSBVContext, 0, -1) -- | Symbolic operations data Op = Plus @@ -622,7 +643,7 @@ instance Show Op where ] -- | Quantifiers: forall or exists. Note that we allow arbitrary nestings. -data Quantifier = ALL | EX deriving Eq +data Quantifier = ALL | EX deriving (Eq, G.Data) -- | Show instance for 'Quantifier' instance Show Quantifier where @@ -680,7 +701,7 @@ type Name = T.Text -- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names data NamedSymVar = NamedSymVar !SV !Name - deriving (Show, Generic) + deriving (Show, Generic, G.Data) -- | For comparison purposes, we simply use the SV and ignore the name instance Eq NamedSymVar where @@ -829,6 +850,7 @@ instance NFData a => NFData (Objective a) where -- | A result can either produce something at the top or as a lambda/constraint. Distinguish by inputs data ResultInp = ResultTopInps ([NamedSymVar], [NamedSymVar]) -- user inputs -- trackers | ResultLamInps [(Quantifier, NamedSymVar)] -- for constraints, we can have quantifiers + deriving G.Data instance NFData ResultInp where rnf (ResultTopInps xs) = rnf xs @@ -949,6 +971,7 @@ instance Show Result where data ArrayContext = ArrayFree (Either (Maybe SV) String) -- ^ A new array, the contents are initialized with the given value, if any, or the custom lambda given | ArrayMutate ArrayIndex SV SV -- ^ An array created by mutating another array at a given cell | ArrayMerge SV ArrayIndex ArrayIndex -- ^ An array created by symbolically merging two other arrays + deriving G.Data instance Show ArrayContext where show (ArrayFree (Left Nothing)) = " initialized with random elements" @@ -1142,13 +1165,13 @@ lookupInput f sv ns | l == 0 = res | True = Nothing -- l != 0, a lambda var, so we ignore where - (l, i) = getId (swNodeId sv) - svs = fmap f ns - res = case S.lookup i ns of -- Nothing on negative Int or Int > length seq - Nothing -> secondLookup - x@(Just e) -> if sv == f e then x else secondLookup - -- we try the fast lookup first, if the node ids don't match then - -- we use the more expensive O (n) to find the index and the elem + (_, l, i) = getId (swNodeId sv) + svs = fmap f ns + res = case S.lookup i ns of -- Nothing on negative Int or Int > length seq + Nothing -> secondLookup + x@(Just e) -> if sv == f e then x else secondLookup + -- we try the fast lookup first, if the node ids don't match then + -- we use the more expensive O (n) to find the index and the elem secondLookup = S.elemIndexL sv svs >>= flip S.lookup ns -- | A defined function/value @@ -1186,7 +1209,8 @@ instance NFData SMTDef where rnf (SMTLam fk frees params body) = rnf fk `seq` rnf frees `seq` rnf params `seq` rnf body -- | The state of the symbolic interpreter -data State = State { pathCond :: SVal -- ^ kind KBool +data State = State { sbvContext :: SBVContext + , pathCond :: SVal -- ^ kind KBool , stCfg :: SMTConfig , startTime :: UTCTime , rProgInfo :: IORef ProgInfo @@ -1436,7 +1460,7 @@ lambdaVar = quantVar ALL newSV :: State -> Kind -> IO NamedSymVar newSV st k = do ctr <- incrementInternalCounter st ll <- readIORef (rLambdaLevel st) - let sv = SV k (NodeId (ll, ctr)) + let sv = SV k (NodeId (sbvContext st, ll, ctr)) registerKind st k return $ NamedSymVar sv $ T.pack (show sv) {-# INLINE newSV #-} @@ -1553,12 +1577,27 @@ newExpr st k app = do -- as an example. Just sv | kindOf sv == k -> return sv _ -> do (NamedSymVar sv _) <- newSV st k + checkConsistent sv e let append (SBVPgm xs) = SBVPgm (xs S.|> (sv, e)) modifyState st spgm append $ modifyIncState st rNewAsgns append modifyState st rexprMap (Map.insert e sv) (return ()) return sv {-# INLINE newExpr #-} +-- | In rare cases, we can get a context mismatch; so make sure the expression is well-formed. +-- This isn't a full solution, but handles the common case (hopefully!) +checkConsistent :: SV -> SBVExpr -> IO () +checkConsistent lhs (SBVApp _ args) = mapM_ check args + where SV _ (NodeId (lhsContext, lambdaLevel, lhsId)) = lhs + check (SV _ (NodeId (rhsContext, ll, ni))) + | lhsContext `compatible` rhsContext && lambdaLevel >= ll && (lambdaLevel /= ll || lhsId > ni) + = pure () + | True + = contextMismatchError lhsContext rhsContext (Just (lambdaLevel, lhsId)) (Just (ll, ni)) + + compatible c1 c2 = c1 == c2 || c1 == globalSBVContext || c2 == globalSBVContext +{-# INLINE checkConsistent #-} + -- | Convert a symbolic value to an internal SV svToSV :: State -> SVal -> IO SV svToSV st (SVal _ (Left c)) = newConst st c @@ -1711,7 +1750,12 @@ svMkSymVarGen isTracker varContext k mbNm st = do let nm = fromMaybe (T.unpack internalName) mbNm nsv = toNamedSV' sv nm - cv = case [v | (nsv', v) <- env, nsv == nsv'] of + -- Ignore the context equivalence check here. When validating, we are in a different + -- context; so they won't match + same (NamedSymVar (SV _ (NodeId (_, ll1, li1))) _) + (NamedSymVar (SV _ (NodeId (_, ll2, li2))) _) = (ll1, li1) == (ll2, li2) + + cv = case [v | (nsv', v) <- env, nsv `same` nsv'] of [] -> if isTracker then -- The sole purpose of a tracker variable is to send the optimization -- directive to the solver, so we can name "expressions" that are minimized @@ -1813,7 +1857,9 @@ mkNewState cfg currentRunMode = liftIO $ do asserts <- newIORef [] istate <- newIORef =<< newIncState qstate <- newIORef Nothing - pure $ State { runMode = rm + ctx <- genSBVContext + pure $ State { sbvContext = ctx + , runMode = rm , stCfg = cfg , startTime = currTime , rProgInfo = progInfo @@ -1854,6 +1900,25 @@ runSymbolic cfg currentRunMode comp = do st <- mkNewState cfg currentRunMode runSymbolicInState st comp +-- | Catch the catastrophic case of context mismatch +contextMismatchError :: SBVContext -> SBVContext -> Maybe (Int, Int) -> Maybe (Int, Int) -> a +contextMismatchError ctx1 ctx2 level1 level2 = error $ unlines $ prefix ++ rest + where prefix | ctx1 /= ctx2 = [ "Data.SBV: Mismatched contexts detected." + , "***" + , "*** Current context: " ++ show ctx1 + , "*** Mixed with : " ++ show ctx2 + ] + | True = [ "Data.SBV: Mismatched levels detected in the same context." + , "***" + , "*** Refers to: " ++ show level1 + , "*** And also : " ++ show level2 + ] + rest = [ "***" + , "*** This happens if you call a proof-function (prove/sat) etc." + , "*** while another one is in execution. Avoid such nested calls." + , "*** See https://github.com/LeventErkok/sbv/issues/71 for examples." + ] + -- | Run a symbolic computation in a given state runSymbolicInState :: MonadIO m => State -> SymbolicT m a -> m (a, Result) runSymbolicInState st (SymbolicT c) = do @@ -1862,6 +1927,27 @@ runSymbolicInState st (SymbolicT c) = do r <- runReaderT c st res <- liftIO $ extractSymbolicSimulationState st + -- Check that the state wasn't clobbered in any way + let check ctx | ctx == sbvContext st || ctx == globalSBVContext + = pure () + | True + = contextMismatchError (sbvContext st) ctx Nothing Nothing + + -- Collect parts of the state that has an SV in it. unfortunately we can't just do G.universeBi res, because + -- the CV component contains a BigFloat, which doesn't have a Data instance. (And the library doesn't export + -- all the constructors, so we can't do a deriving instance. Sigh.) + mapM_ check $ nub [ctx | NodeId (ctx, _, _) <- G.universeBi $ [s | (_, _, s) <- resObservables res] + ++ G.universeBi (resParams res) + ++ Map.elems (fst (resConsts res)) + ++ map fst (snd (resConsts res)) + ++ G.universeBi (resTables res) + ++ G.universeBi (resArrays res) + ++ G.universeBi (pgmAssignments (resAsgns res)) + ++ G.universeBi (resConstraints res) + ++ [s | (_, _, s) <- resAssertions res] + ++ resOutputs res + ] + -- Clean-up after ourselves qs <- liftIO $ readIORef $ rQueryState st case qs of diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs index b0ccfc49e..6f740b759 100644 --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -70,7 +70,8 @@ inSubState inState comp = do -- don't really impact anything. comp State { -- These are not IORefs; so we share by copying the value; changes won't be copied back - pathCond = share pathCond + sbvContext = share sbvContext + , pathCond = share pathCond , startTime = share startTime -- These are shared IORef's; and is shared, so they will be copied back to the parent state @@ -298,7 +299,10 @@ toLambda curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgnsSeq} walk (cur@(SV _ nd, _) : rest) remaining = map (mkTable . snd) ready ++ [mkLet cur] ++ walk rest notReady - where (ready, notReady) = partition (\(need, _) -> need < getId nd) remaining + where (ready, notReady) = partition (\(need, _) -> need < getLLI nd) remaining + + getLLI :: NodeId -> (Int, Int) + getLLI (NodeId (_, l, i)) = (l, i) -- if we have just one definition returning it, simplify simpleBody :: [(SV, String)] -> SV -> Maybe String @@ -331,7 +335,7 @@ toLambda curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgnsSeq} (tableMap, constTables, nonConstTablesUnindexed) = constructTables rm consts tbls -- Index each non-const table with the largest index of SV it needs - nonConstTables = [ (maximum ((0, 0) : [getId n | SV _ n <- elts]), nct) + nonConstTables = [ (maximum ((0, 0) : [getLLI n | SV _ n <- elts]), nct) | nct@((_, elts), _) <- nonConstTablesUnindexed] lambdaTable :: String -> Kind -> Kind -> [SV] -> String