From dbfedb22c6f1a2a2c532ed97a8b56a0a78842767 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Thu, 5 Sep 2024 05:05:39 -0700 Subject: [PATCH] :bug: Trying to fix CI build failure that cannot be reproduced locally --- src/Grisette/Internal/Backend/Solving.hs | 7 +++++-- src/Grisette/Internal/Backend/SymBiMap.hs | 10 +++++++++ .../Internal/SymPrim/Prim/Internal/Caches.hs | 11 ++++++---- .../Internal/SymPrim/Prim/Internal/Term.hs | 14 ++++++++++--- .../Internal/SymPrim/Prim/Internal/Utils.hs | 16 +++++++++++--- test/Grisette/SymPrim/Prim/ConcurrentTests.hs | 21 +++++++++++++++++-- test/Main.hs | 2 +- 7 files changed, 66 insertions(+), 15 deletions(-) diff --git a/src/Grisette/Internal/Backend/Solving.hs b/src/Grisette/Internal/Backend/Solving.hs index d584e22a..ddac27c8 100644 --- a/src/Grisette/Internal/Backend/Solving.hs +++ b/src/Grisette/Internal/Backend/Solving.hs @@ -844,7 +844,7 @@ parseModel :: SBVI.SMTModel -> SymBiMap -> PM.Model -parseModel _ (SBVI.SMTModel _ _ assoc origFuncs) mp = +parseModel _ model@(SBVI.SMTModel _ _ assoc origFuncs) mp = case preprocessUIFuncs origFuncs of Just funcs -> foldr goSingle emptyModel $ funcs ++ assocFuncs _ -> error "SBV Failed to parse model" @@ -858,4 +858,7 @@ parseModel _ (SBVI.SMTModel _ _ assoc origFuncs) mp = Nothing -> error $ "BUG: Please send a bug report. The model is not consistent with the " - <> "list of symbols that have been defined." + <> "list of symbols that have been defined. The map is " + <> show mp + <> ". The model is " + <> show model diff --git a/src/Grisette/Internal/Backend/SymBiMap.hs b/src/Grisette/Internal/Backend/SymBiMap.hs index aa3e0fb0..ae05cb5b 100644 --- a/src/Grisette/Internal/Backend/SymBiMap.hs +++ b/src/Grisette/Internal/Backend/SymBiMap.hs @@ -57,6 +57,16 @@ data SymBiMap = SymBiMap quantifiedSymbolNum :: Int } +instance Show SymBiMap where + show (SymBiMap t s f _) = + "SymBiMap { size: " + ++ show s + ++ ", toSBV: " + ++ show (M.keys t) + ++ ", fromSBV: " + ++ show (M.toList f) + ++ " }" + -- | Information about a quantified symbol. newtype QuantifiedSymbolInfo = QuantifiedSymbolInfo Int deriving (Generic, Ord, Eq, Show, Hashable, Lift, NFData) diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs index 6268ab45..9defc82c 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs @@ -33,7 +33,6 @@ where import Control.Concurrent ( MVar, ThreadId, - mkWeakThreadId, myThreadId, newMVar, putMVar, @@ -55,10 +54,11 @@ import GHC.Weak (Weak, deRefWeak) import Grisette.Internal.SymPrim.Prim.Internal.Utils ( WeakThreadId, WeakThreadIdRef, + mkWeakThreadIdRefWithFinalizer, myWeakThreadId, weakThreadId, ) -import System.Mem.Weak (addFinalizer, mkWeakPtr) +import System.Mem.Weak (mkWeakPtr) import Unsafe.Coerce (unsafeCoerce) -- | A unique identifier for a term. @@ -144,8 +144,11 @@ typeMemoizedCache tid = do return r1 Nothing -> do r1 <- mkCache - wtidRef <- mkWeakThreadId tid - addFinalizer tid $ atomicModifyIORefCAS_ termCacheCell $ HM.delete wtid + wtidRef <- + mkWeakThreadIdRefWithFinalizer tid $ + print ("finalize", wtid) + >> atomicModifyIORefCAS_ termCacheCell (HM.delete wtid) + >> print ("finalize0", wtid) r <- newIORef $ HM.singleton (typeRep (Proxy @a)) (unsafeCoerce r1) atomicModifyIORefCAS termCacheCell $ \m -> (HM.insert wtid (wtidRef, r) m, r1) diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs index 35224f00..46a9fcb5 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Term.hs @@ -88,6 +88,7 @@ module Grisette.Internal.SymPrim.Prim.Internal.Term FPRoundingBinaryOp (..), FloatingUnaryOp (..), Term (..), + toCurThread, identity, typeHashId, introSupportedPrimConstraint, @@ -2151,9 +2152,10 @@ instance (SupportedPrim t) => Eq (Term t) where if threadId a == threadId b then identity a == identity b else unsafePerformIO $ do - a' <- fullReconstructTerm a - b' <- fullReconstructTerm b - return $ identity a' == identity b' + tid <- myWeakThreadId + a' <- toCurThreadImpl tid a + b' <- toCurThreadImpl tid b + return $ a' == b' instance (SupportedPrim t) => Hashable (Term t) where hashWithSalt s t = hashWithSalt s $ baseHash t @@ -3497,6 +3499,12 @@ toCurThreadImpl tid t | termThreadId t == tid = return t toCurThreadImpl _ t = fullReconstructTerm t {-# INLINE toCurThreadImpl #-} +toCurThread :: forall t. Term t -> IO (Term t) +toCurThread t = do + tid <- myWeakThreadId + toCurThreadImpl tid t +{-# INLINE toCurThread #-} + -- | Construct and internalizing a 'ConTerm'. curThreadConTerm :: (SupportedPrim t) => t -> IO (Term t) curThreadConTerm t = intern $ UConTerm t diff --git a/src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs b/src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs index 08781909..7aad2b4e 100644 --- a/src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs +++ b/src/Grisette/Internal/SymPrim/Prim/Internal/Utils.hs @@ -7,6 +7,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE UnliftedFFITypes #-} {-# LANGUAGE ViewPatterns #-} @@ -30,17 +31,19 @@ module Grisette.Internal.SymPrim.Prim.Internal.Utils WeakThreadIdRef, myWeakThreadId, weakThreadRefAlive, + mkWeakThreadIdRefWithFinalizer, ) where #if MIN_VERSION_base(4,19,0) import GHC.Conc.Sync - ( ThreadId, + ( ThreadId(ThreadId), ThreadStatus (ThreadDied, ThreadFinished), fromThreadId, myThreadId, threadStatus, ) +import GHC.Exts (mkWeak#) #else import GHC.Conc ( ThreadId (ThreadId), @@ -48,7 +51,7 @@ import GHC.Conc myThreadId, threadStatus, ) -import GHC.Exts (Addr#, ThreadId#, unsafeCoerce#) +import GHC.Exts (Addr#, ThreadId#, unsafeCoerce#, mkWeak#) #if __GLASGOW_HASKELL__ >= 904 #elif __GLASGOW_HASKELL__ >= 900 import Foreign.C.Types (CLong (CLong)) @@ -58,7 +61,9 @@ import Foreign.C.Types (CInt (CInt)) #endif import Data.Typeable (cast) import Data.Word (Word64) -import System.Mem.Weak (Weak, deRefWeak) +import GHC.IO (IO (IO)) +import GHC.Weak (Weak (Weak)) +import System.Mem.Weak (deRefWeak) import Type.Reflection ( TypeRep, Typeable, @@ -158,3 +163,8 @@ weakThreadRefAlive wtid = do st <- threadStatus tid return $ st `notElem` [ThreadFinished, ThreadDied] {-# INLINE weakThreadRefAlive #-} + +mkWeakThreadIdRefWithFinalizer :: ThreadId -> IO () -> IO (Weak ThreadId) +mkWeakThreadIdRefWithFinalizer t@(ThreadId t#) (IO finalizer) = IO $ \s -> + case mkWeak# t# t finalizer s of + (# s1, w #) -> (# s1, Weak w #) diff --git a/test/Grisette/SymPrim/Prim/ConcurrentTests.hs b/test/Grisette/SymPrim/Prim/ConcurrentTests.hs index 7e8398bd..25ac2609 100644 --- a/test/Grisette/SymPrim/Prim/ConcurrentTests.hs +++ b/test/Grisette/SymPrim/Prim/ConcurrentTests.hs @@ -8,7 +8,7 @@ import Control.DeepSeq (force) import Control.Exception (evaluate) import Data.Hashable (Hashable (hash)) import Data.String (IsString (fromString)) -import Grisette (SymInteger (SymInteger)) +import Grisette (SymEq ((.==)), SymInteger (SymInteger), evalSymToCon, solve, z3) import Test.Framework (Test, testGroup) import Test.Framework.Providers.HUnit (testCase) import Test.HUnit ((@?=)) @@ -31,5 +31,22 @@ concurrentTests = putMVar bref p br <- takeMVar bref ar @?= br - hash ar @?= hash br + hash ar @?= hash br, + testCase "Eval" $ do + aref <- newEmptyMVar + bref <- newEmptyMVar + _ <- forkIO $ do + a <- evaluate $ force ("a" :: SymInteger) + putMVar aref a + _ <- forkIO $ do + b <- evaluate $ force ("b" :: SymInteger) + putMVar bref b + a@(SymInteger ta) <- takeMVar aref + b@(SymInteger tb) <- takeMVar bref + r <- solve z3 $ a .== b + print ta + print tb + case r of + Left err -> error $ show err + Right m -> evalSymToCon m a @?= (evalSymToCon m b :: Integer) ] diff --git a/test/Main.hs b/test/Main.hs index 7db95fdf..c0d67dd3 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -77,7 +77,7 @@ import Grisette.Unified.UnifiedConstructorTest (unifiedConstructorTest) import Test.Framework (Test, defaultMain, testGroup) main :: IO () -main = do +main = defaultMain [ coreTests, irTests,