🐛 Trying to fix CI build failure that cannot be reproduced locally

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

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)

src/Grisette/Internal/SymPrim/Prim/Internal/Caches.hs

@@ -39,6 +39,7 @@ import Control.Concurrent
     putMVar,
     takeMVar,
   )
+import Control.DeepSeq (force)
 import Control.Monad (replicateM)
 import qualified Data.Array as A
 import Data.Atomics (atomicModifyIORefCAS, atomicModifyIORefCAS_)
@@ -50,7 +51,7 @@ import Data.Maybe (isJust)
 import qualified Data.Vector.Unboxed.Mutable as U
 import Data.Word (Word32)
 import GHC.Base (Any)
-import GHC.IO (unsafePerformIO)
+import GHC.IO (evaluate, unsafePerformIO)
 import GHC.Weak (Weak, deRefWeak)
 import Grisette.Internal.SymPrim.Prim.Internal.Utils
   ( WeakThreadId,
@@ -186,7 +187,8 @@ intern !bt = do
       CacheState nextBaseId sem s = getCache cache A.! (fromIntegral r)
   takeMVar sem
   current <- readIORef s
-  case HM.lookup dt current of
+  t <- evaluate $ HM.lookup dt current
+  case t of
     Nothing -> do
       i <- U.unsafeRead nextBaseId 0
       U.unsafeWrite nextBaseId 0 (i + 1)

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

test/Grisette/Core/Control/Monad/UnionTests.hs

@@ -161,7 +161,7 @@ unionTests =
                       Just ("u1c", mrgSingle $ Left "u1a", mrgSingle $ Right "u1b")
                 actual @?= expected
             ]
-        ],
+        ]{-,
       testGroup
         "Show"
         [ testCase "Merged" $ do
@@ -172,7 +172,7 @@ unionTests =
           testCase "Not merged" $ do
             let expected = "<If u1c u1a u1b>"
             show unionSimple1 @?= expected
-        ],
+        ]-},
       testGroup
         "PPrint"
         [ testCase "Merged" $ do

test/Grisette/Core/Data/Class/SymShiftTests.hs

@@ -161,35 +161,35 @@ symShiftTests :: Test
 symShiftTests =
   testGroup
     "SymShift"
-    [ concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word8),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word16),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word32),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word64),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 1)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 2)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 3)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 63)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 64)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 65)),
-      concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 128)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy Int8),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy Int16),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy Int32),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy Int64),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy Int),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 1)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 2)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 3)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 63)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 64)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 65)),
-      concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 128)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 1)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 2)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 3)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 63)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 64)),
+    [ -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word8),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word16),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word32),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word64),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy Word),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 1)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 2)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 3)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 63)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 64)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 65)),
+      -- concreteUnsignedTypeSymShiftTests (Proxy :: Proxy (WordN 128)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy Int8),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy Int16),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy Int32),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy Int64),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy Int),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 1)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 2)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 3)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 63)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 64)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 65)),
+      -- concreteSignedTypeSymShiftTests (Proxy :: Proxy (IntN 128)),
+      -- symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 1)),
+      -- symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 2)),
+      -- symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 3)),
+      -- symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 63)),
+      symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 64)){-,
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 65)),
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymWordN 128)),
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 1)),
@@ -198,5 +198,5 @@ symShiftTests =
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 63)),
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 64)),
       symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 65)),
-      symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 128))
+      symbolicTypeSymShiftTests (Proxy :: Proxy (SymIntN 128))-}
     ]

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)
     ]

test/Main.hs

@@ -79,53 +79,53 @@ import Test.Framework (Test, defaultMain, testGroup)
 main :: IO ()
 main = do
   defaultMain
-    [ coreTests,
-      irTests,
-      sbvTests,
-      libTests,
-      unifiedTests
+    [ coreTests--,
+      -- irTests,
+      -- sbvTests,
+      -- libTests,
+      -- unifiedTests
     ]
 
 coreTests :: Test
 coreTests =
   testGroup
     "Grisette.Core"
-    [ testGroup
-        "Control"
-        [ testGroup
-            "Monad"
-            [ unionTests
-            ],
-          exceptionTests
-        ],
+    [ -- testGroup
+      --   "Control"
+      --   [ testGroup
+      --       "Monad"
+      --       [ unionTests
+      --       ],
+      --     exceptionTests
+      --   ],
       testGroup
         "Data"
         [ testGroup
             "Class"
-            [ bitCastTests,
-              Grisette.Core.Data.Class.BoolTests.boolTests,
-              evalSymTests,
-              extractSymTests,
-              genSymTests,
-              pprintTests,
-              mergeableTests,
-              plainUnionTests,
-              safeDivTests,
-              safeLinearArithTests,
-              safeSymShiftTests,
-              safeSymRotateTests,
-              seqTests,
-              sordTests,
-              simpleMergeableTests,
-              substSymTests,
-              symFiniteBitsTests,
-              symRotateTests,
-              symShiftTests,
-              toConTests,
-              toSymTests,
-              tryMergeTests
-            ],
-          unionBaseTests
+            [ -- bitCastTests,
+              -- Grisette.Core.Data.Class.BoolTests.boolTests,
+              -- evalSymTests,
+              -- extractSymTests,
+              -- genSymTests,
+              -- pprintTests,
+              -- mergeableTests,
+              -- plainUnionTests,
+              -- safeDivTests,
+              -- safeLinearArithTests,
+              -- safeSymShiftTests,
+              -- safeSymRotateTests,
+              -- seqTests,
+              -- sordTests,
+              -- simpleMergeableTests,
+              -- substSymTests,
+              -- symFiniteBitsTests,
+              -- symRotateTests,
+              symShiftTests--,
+              -- toConTests,
+              -- toSymTests,
+              -- tryMergeTests
+            ]--,
+          -- unionBaseTests
         ]
     ]