abcBridge 0.11 → 0.12

raw patch · 10 files changed

+231/−111 lines, 10 filesdep +randomdep +tf-randomdep +unixdep ~aigdep ~basedep ~tasty-quickchecksetup-changednew-component:exe:find-segfaultPVP ok

version bump matches the API change (PVP)

Dependencies added: random, tf-random, unix

Dependency ranges changed: aig, base, tasty-quickcheck

API changes (from Hackage documentation)

Files

• Setup.hs +12/−34
• abc-build/galois-abcBridge.version +1/−1
• abcBridge.cabal +46/−31
• scripts/build-abc.sh +0/−1
• src/Data/ABC/AIG.hs +18/−17
• src/Data/ABC/GIA.hs +39/−15
• src/Data/ABC/Internal/ABC.chs +1/−1
• src/Data/ABC/Internal/ABCGlobal.chs +9/−5
• src/Data/ABC/Internal/GIA.chs +9/−6
• tests/find-segfault.hs +96/−0

@@ -9,6 +9,7 @@         updatePackageDescription, FlagAssignment(..), FlagName(..)) import Distribution.Verbosity (verbose, Verbosity(..)) import Distribution.System (OS(..), Arch(..), Platform (..), buildOS, buildPlatform)+import qualified Distribution.Simple.Utils import Data.Version( Version, showVersion ) import System.Directory import System.FilePath@@ -29,21 +30,22 @@ -- Finally, we must also include some information about where do find the libabc.a -- and libabc.dll files. ----- The way we have to do this is sort of nasty, but implementing the "readDesc" user--- hook doesn't seem to work the way I expect, so we have to modify the package description--- "in flight" inside each of the various hooks.+-- We do this by modifying the configure hook so it modifies the package description+-- read from disk before returing the local build info that is used by other cabal actions.+-- However, we also have to modify the sDistHook because it reads from the package description+-- file directly rather than using the one from the confHook.  The 'clean' action likewise reads+-- the description file directly, but it causes no problems to use the unmodified package+-- description for the clean action, so we do not modify that hook.  main = defaultMainWithHooks simpleUserHooks-    { postConf = \a f pkg_desc lbi -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    postConf simpleUserHooks a f pkg_desc' lbi--    ,  confHook = \(gpkg_desc, hbi) f -> do+    {  confHook = \(gpkg_desc, hbi) f -> do                     let v = fromFlag $ configVerbosity f                     let fs = configConfigurationsFlags f                     setupAbc v (packageDescription gpkg_desc)                     buildAbc v fs-                    confHook simpleUserHooks (gpkg_desc, hbi) f+                    lbi <- confHook simpleUserHooks (gpkg_desc, hbi) f+                    pkg_desc' <- abcPkgDesc (localPkgDescr lbi)+                    return lbi{ localPkgDescr = pkg_desc' }      , sDistHook = \pkg_desc lbi h f -> do                     let v = fromFlag $ sDistVerbosity f@@ -51,31 +53,6 @@                     pkg_desc' <- abcPkgDesc pkg_desc                     sDistHook simpleUserHooks pkg_desc' lbi h f -    , buildHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    buildHook simpleUserHooks pkg_desc' lbi h f-    , haddockHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    haddockHook simpleUserHooks pkg_desc' lbi h f-    , copyHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    copyHook simpleUserHooks pkg_desc' lbi h f-    , instHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    instHook simpleUserHooks pkg_desc' lbi h f-    , regHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    regHook simpleUserHooks pkg_desc' lbi h f-    , unregHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    unregHook simpleUserHooks pkg_desc' lbi h f-    , hscolourHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    hscolourHook simpleUserHooks pkg_desc' lbi h f-    , testHook = \pkg_desc lbi h f -> do-                    pkg_desc' <- abcPkgDesc pkg_desc-                    testHook simpleUserHooks pkg_desc' lbi h f-     , postCopy = postCopyAbc     , postInst = postInstAbc     }@@ -109,6 +86,7 @@ -- If necessary, fetch the ABC sources and prepare for building setupAbc :: Verbosity -> PackageDescription -> IO () setupAbc verbosity pkg_desc = do+    putStrLn $ unwords ["Cabal library version:", showVersion Distribution.Simple.Utils.cabalVersion]     let version = pkgVersion $ package $ pkg_desc     let packageVersion = "PACKAGE_VERSION"     env <- getEnvironment

@@ -1,1 +1,1 @@-0.11+0.12

@@ -1,5 +1,5 @@ Name:               abcBridge-Version:            0.11+Version:            0.12 Synopsis:           Bindings for ABC, A System for Sequential                     Synthesis and Verification Description:        Bindings for ABC focused on creating And-Inverter@@ -9,10 +9,10 @@ License-file:       LICENSE Author:             Galois Inc. Maintainer:         jhendrix@galois.com-Copyright:          (c) 2010-2014 Galois Inc.+Copyright:          (c) 2010-2015 Galois Inc. Category:           Data build-type:         Custom-cabal-Version:      >= 1.10+cabal-Version:      >= 1.18  extra-source-files:   include/*.h@@ -20,15 +20,14 @@   scripts/*.sh   tests/eijk.S298.S.aig +flag enable-extra-tests+  Description: Enable building the long-test and find-segfault utility progams+  Default: False+ flag enable-pthreads   Description: Turn on multithreading   Default: True --- Ugh. Temporary fix to make Hackage happy.---flag enable-hpc---  Description: Collect HPC coverage information.---  Default: False- source-repository head   type: git   location: https://github.com/GaloisInc/abcBridge.git@@ -61,7 +60,8 @@                         FlexibleContexts,                         MultiParamTypeClasses,                         EmptyDataDecls-  Ghc-options:          -Wall  -auto-all -caf-all -fno-ignore-asserts+  Ghc-options:          -Wall -fno-ignore-asserts+  -- Ghc-prof-options:     -auto-all -caf-all   -- -U__BLOCKS__ to work around https://github.com/haskell/c2hs/issues/29   Cc-options:           -U__BLOCKS__ -U__has_attribute -w @@ -84,10 +84,10 @@   }   Include-dirs:         include -  +   Build-depends:     base >= 4,-    aig,+    aig >= 0.2.1,     containers,     directory,     vector@@ -99,28 +99,15 @@                         cbits/abcBridgeGiaDup.c                         cbits/pthread_stubs.c -  -- Ugh. Temporary fix to make Hackage happy.-  --if flag(enable-hpc)-  --  ghc-options: -fhpc -hpcdir .hpc-- test-suite abc-test   type: exitcode-stdio-1.0   hs-source-dirs: tests    ghc-options: -Wall-  ghc-prof-options: -fprof-auto -O2--  -- Ugh. Temporary fix to make Hackage happy.-  --if flag(enable-hpc)-  --  ghc-options: -fhpc+  -- ghc-prof-options: -fprof-auto    default-Language: Haskell98 -  -- Ugh. Temporary fix to make Hackage happy.-  --if flag(enable-hpc)-  --  ghc-options: -fhpc-   other-modules:     Tests.Basic     Tests.Operations@@ -137,19 +124,47 @@     tasty,     tasty-ant-xml,     tasty-hunit,-    tasty-quickcheck,+    tasty-quickcheck >= 0.8.1,     QuickCheck >= 2.7  +Executable find-segfault+  hs-source-dirs: tests+  ghc-options: -Wall++  default-Language: Haskell2010++  main-is:+    find-segfault.hs++  if !flag(enable-extra-tests)+     buildable: False+  else+     buildable: True+     build-depends:+       base == 4.*,+       abcBridge,+       aig,+       directory,+       vector,+       random,+       tf-random,+       unix >= 2.7,+       tasty,+       tasty-hunit,+       tasty-quickcheck,+       QuickCheck >= 2.7+++ Executable long-test   hs-source-dirs: tests -  ghc-options: -Wall-  ghc-prof-options: -fprof-auto -O2+  if !flag(enable-extra-tests)+     buildable: False -  -- Ugh. Temporary fix to make Hackage happy.-  --if flag(enable-hpc)-  --  ghc-options: -fhpc+  ghc-options: -Wall+  -- ghc-prof-options: -fprof-auto    default-Language: Haskell98 

@@ -44,4 +44,3 @@  cd abc-build make -j4 ARCHFLAGS="-DABC_LIB $A" REMOVE_DRECTVE="$REMOVE_CMD" READLINE=0 PTHREADS="$PTHREADS" libabc.a $S-

@@ -272,11 +272,12 @@       ioWriteAiger p path True False False    checkSat g l = do-    withNetworkPtr (AIG.Network g [l]) $ \p -> do-      alloca $ \pp -> do-        poke pp =<< abcNtkDup p-        flip finally (abcNtkDelete =<< peek pp) $ do-        checkSat' pp+    withNetworkPtr (AIG.Network g [l]) $ \p ->+      alloca $ \pp ->+        bracket_+          (poke pp =<< abcNtkDup p)+          (abcNtkDelete =<< peek pp)+          (checkSat' pp)    abstractEvaluateAIG = memoFoldAIG @@ -288,9 +289,10 @@     withNetworkPtr x $ \xp -> do     withNetworkPtr y $ \yp -> do       alloca $ \pp -> do-        flip finally (abcNtkDelete =<< peek pp) $ do-          poke pp =<< abcNtkMiter xp yp False 0 False False-          AIG.toVerifyResult <$> checkSat' pp+        bracket_+          (poke pp =<< abcNtkMiter xp yp False 0 False False)+          (abcNtkDelete =<< peek pp)+          (AIG.toVerifyResult <$> checkSat' pp)    evaluator g inputs_l = do     withAIGPtr g $ \ntk -> do@@ -327,7 +329,7 @@           r1 <- evaluateFn v . Lit =<< abcObjLit1 o           VM.write v i (r0 && r1)       -- Return evaluation function.-      pureEvaluateFn <$> V.freeze v+      pureEvaluateFn g <$> V.freeze v  forI_ :: Monad m => Int -> (Int -> m ()) -> m () forI_ = go 0@@ -335,8 +337,8 @@                  | otherwise = return ()  {-# NOINLINE pureEvaluateFn #-}-pureEvaluateFn :: V.Vector Bool -> Lit s -> Bool-pureEvaluateFn v (Lit l) = Unsafe.unsafePerformIO $ do+pureEvaluateFn :: AIG s -> V.Vector Bool -> Lit s -> Bool+pureEvaluateFn g v (Lit l) = Unsafe.unsafePerformIO $ withAIGPtr g $ \_ -> do   let c = abcObjIsComplement l   let o = abcObjRegular l   i <- fromIntegral <$> abcObjId o@@ -367,17 +369,16 @@                -> (Abc_Ntk_t -> IO a)                -> IO a withNetworkPtr (AIG.Network x o) m = do-  withAIGPtr x $ \p -> do-  flip finally (deletePos p) $ do-    mapM_ (addPo p) o-    m p+  withAIGPtr x $ \p ->+    bracket_+      (mapM_ (addPo p) o)+      (deletePos p)+      (m p)  addPo :: Abc_Ntk_t -> Lit s -> IO () addPo p (Lit ptr) = do   po <- abcNtkCreateObj p AbcObjPo   abcObjAddFanin po ptr--  checkIsConstant :: Abc_Ntk_t -> IO (Maybe Bool) checkIsConstant p = do

@@ -40,6 +40,7 @@     , litView       -- * File IO     , readAiger+    , writeAigerWithLatches     , writeCNF       -- * QBF     , check_exists_forall@@ -93,6 +94,7 @@ -- | An and-invertor graph network in GIA form. newtype GIA s = GIA { _giaPtr :: ForeignPtr Gia_Man_t_ } +-- | Represent a literal. newtype Lit s = L { _unLit :: GiaLit }   deriving (Eq, Storable, Ord) @@ -119,7 +121,7 @@     fail $ "Data.ABC.GIA.readAiger: file does not exist"   let skipStrash = False   bracketOnError (giaAigerRead path skipStrash False) giaManStop $ \p -> do-    rn <- giaManRegNum p+    rn <- getGiaManRegNum p     when (rn /= 0) $ fail "Networks do not yet support latches."      cov <- giaManCos p@@ -153,6 +155,27 @@   compareLit x y = compare x y   showLit x = show (unGiaLit (_unLit x)) +-- | Write an AIGER file with the given number of latches.+-- If the number of latches is denoted by "n", then the last n inputs and last n outputs+-- are treated as the latch input and outputs respectively.  The other inputs and outputs+-- represent primary inputs and outputs.+writeAigerWithLatches :: FilePath+                      -> AIG.Network Lit GIA+                      -> Int -- ^ Number of latches.+                      -> IO ()+writeAigerWithLatches path ntk latchCount =+  withNetworkPtr ntk $ \p -> do+    flip finally (setGiaManRegNum p 0) $ do+      ci_num <- giaManCiNum p+      let co_num = AIG.networkOutputCount ntk+      when (latchCount < 0) $ fail "Latch count must be positive."+      when (fromIntegral latchCount > ci_num) $ do+        fail "Latch count exceeds number of inputs."+      when (latchCount > co_num) $ do+        fail "Latch count exceeds number of outputs."+      setGiaManRegNum p (fromIntegral latchCount)+      giaAigerWrite p path False False+ instance AIG.IsAIG Lit GIA where    newGraph _ = newGIA@@ -184,9 +207,10 @@     giaNetworkAsAIGMan (AIG.Network ntk [l]) $ \pMan -> do     -- Allocate a pointer to an ABC network.     alloca $ \pp -> do-      flip finally (abcNtkDelete =<< peek pp) $ do-        poke pp =<< abcNtkFromAigPhase pMan-        AIG.checkSat' pp+      bracket_+        (poke pp =<< abcNtkFromAigPhase pMan)+        (abcNtkDelete =<< peek pp)+        (AIG.checkSat' pp)    cec gx gy = do     withNetworkPtr gx $ \x -> do@@ -249,6 +273,7 @@     -- return the outputs     pureEvaluateFn <$> V.freeze vec +-- | Evaluate a literal on an assignment. pureEvaluateFn :: V.Vector Bool -> Lit s -> Bool pureEvaluateFn v (L l) = assert inRange (c /= (v V.! i))   where i = fromIntegral $ unGiaVar $ giaLitVar l@@ -263,7 +288,6 @@ --withNetworkPtr = withNetworkPtr_Copy  - -- This is a safer method for implementing withNetworkPtr; it copies the -- entire graph before adding the required COs and disposes of the copied -- graph afterwards.  Obviously, this has substantial memory usage implications.@@ -272,7 +296,7 @@   withGIAPtr ntk $ \p -> do      ncos <- vecIntSize =<< giaManCos p      assert( ncos == 0 ) $ do-     bracket (giaManDupNormalize p) giaManStop +     bracket (giaManDupNormalize p) giaManStop          (\p' -> mapM_ (\(L o) -> giaManAppendCo p' o) out >> m p')  @@ -303,8 +327,8 @@           -- clear the objects for reuse           forN_ (fromIntegral ncos) $ \i -> do              var <- vecIntEntry cov (fromIntegral i)-             -- Assert that all the objects we are clearing are above the old object count; that is,-             -- they must have been allocated when we shoved in the new COs.+             -- Assert that all the objects we are clearing are above the old object count;+             -- that is, they must have been allocated when we shoved in the new COs.              assert (var >= orig_oc) $ do              -- clear the memory assocaited with the GIA object              clearGiaObj =<< giaManObj p (GiaVar var)@@ -316,13 +340,13 @@           writeAt giaManNObjs p orig_oc      -- Run computation, then reset.-    flip finally reset $ do+    bracket_       -- Add combinational outputs.-      mapM_ (\(L o) -> giaManAppendCo p o) out-+      (mapM_ (\(L o) -> giaManAppendCo p o) out)+      -- reset the graph afterwards+      reset       -- Run computation.-      m p-+      (m p)  -- | Run a computation with an AIG man created from a GIA netowrk. giaNetworkAsAIGMan :: AIG.Network Lit GIA@@ -358,7 +382,6 @@         return t   r <- newIORef Map.empty   let objTerm o = do-        --putStrLn $ "objTerm " ++ show o         m0 <- readIORef r         case Map.lookup o m0 of           Just t -> return t@@ -444,6 +467,7 @@       ci <- aigManCi pMan (fromIntegral i)       ((vars SV.!) . fromIntegral) `fmap` (aigObjId ci) +data PartialSatResult -- | Check a formula of the form Ex.Ay p(x,y)@. -- This function takes a network where input variables are used to -- represent both the existentially and the universally quantified variables.@@ -459,7 +483,7 @@                     -> [Bool]                        -- ^ Initial value to use in search for universal variables.                        -- (should equal number of universal variables.).-                    -> Int+                    -> CInt                        -- ^ Number of iterations to try solver.                     -> IO (Either String AIG.SatResult) check_exists_forall ntk exists_cnt prop init_assign iter_cnt = do

@@ -405,6 +405,6 @@ {#fun AbcBridge_NtkQbf as abcNtkQbf     { id `Abc_Ntk_t' -- Network     , `Int' -- Number of parameters-    , `Int' -- Maximum number of iterations.+    , id `CInt' -- Maximum number of iterations.     , id `Vec_Int_t' -- Vector for storing result.     } -> `Int' #}

@@ -28,6 +28,7 @@ #include "abc_global.h" #include "abcbridge.h" +import Data.Word import Control.Applicative import Control.Exception (assert) import Foreign@@ -77,14 +78,17 @@     nRegs   <- fromIntegral <$> {#get Abc_Cex_t->nRegs #} p     nPis    <- fromIntegral <$> {#get Abc_Cex_t->nPis #} p     nBits   <- fromIntegral <$> {#get Abc_Cex_t->nBits #} p++    let size = 32 -- this is what the assume in the code!+     -- read out the data (it's a big bit field, so we'll     -- convert it into a flat [Bool] before slicing and dicing);     -- there might be a little extra left over-    ws <- peekArray (nBits `divUp` (sizeOf (undefined :: CUInt)))-                    (castPtr (plusPtr p {#sizeof Abc_Cex_t#}) :: Ptr CUInt)-                    :: IO [CUInt]-    let size = 32 -- this is what the assume in the code!-        bits = concatMap (\x -> map (testBit x) [0..size-1]) ws :: [Bool]+    ws <- peekArray (nBits `divUp` size)+                    (castPtr (plusPtr p {#sizeof Abc_Cex_t#}) :: Ptr Word32)+                    :: IO [Word32]++    let bits = concatMap (\x -> map (testBit x) [0..size-1]) ws :: [Bool]         -- slice it up         (regs, flatInputs) = splitAt nRegs bits         inputs = chunksOf nPis ((take ((iFrame + 1) * nPis)) flatInputs)

@@ -51,7 +51,8 @@     , giaManPiNum     , giaManPoNum     , giaManAndNum-    , giaManRegNum+    , getGiaManRegNum+    , setGiaManRegNum      , giaManCiVar     , giaManCoVar@@ -299,7 +300,6 @@ giaManCexComb :: Gia_Man_t -> IO Abc_Cex_t giaManCexComb = {#get Gia_Man_t->pCexComb #} - giaManNObjs :: Field Gia_Man_t CInt giaManNObjs = fieldFromOffset {#offsetof Gia_Man_t->nObjs #} @@ -327,14 +327,17 @@ giaManCoNum :: Gia_Man_t -> IO CInt giaManCoNum = vecIntSize <=< giaManCos -giaManRegNum :: Gia_Man_t -> IO CInt-giaManRegNum = {#get Gia_Man_t->nRegs #}+getGiaManRegNum :: Gia_Man_t -> IO CInt+getGiaManRegNum = {#get Gia_Man_t->nRegs #} +setGiaManRegNum :: Gia_Man_t -> CInt -> IO ()+setGiaManRegNum = {#set Gia_Man_t->nRegs #}+ giaManPiNum :: Gia_Man_t -> IO CInt-giaManPiNum m = (-) <$> giaManCiNum m <*> giaManRegNum m+giaManPiNum m = (-) <$> giaManCiNum m <*> getGiaManRegNum m  giaManPoNum :: Gia_Man_t -> IO CInt-giaManPoNum m = (-) <$> giaManCoNum m <*> giaManRegNum m+giaManPoNum m = (-) <$> giaManCoNum m <*> getGiaManRegNum m  giaManAndNum :: Gia_Man_t -> IO CInt giaManAndNum m = fn <$> giaManObjNum m <*> giaManCiNum m <*> giaManCoNum m

@@ -0,0 +1,96 @@+module Main where++import Test.Tasty+import Test.Tasty.Ingredients+import Test.Tasty.QuickCheck++import qualified Data.ABC as ABC++import Tests.Basic+import Tests.Operations+import Tests.QBF++import System.Environment+import System.Posix.Process+import System.Posix.IO+import System.Posix.Files++import System.Random+import System.Random.TF+import System.Random.TF.Init++import Test.QuickCheck.Random++{-+This utility runs the test suite in a separate process with differently-chosen random seeds.+It continually runs the test suite until the child process exits on a signal.  We are trying to+track down an infrequently-occuring segfault.  The idea is to find a random seed that tickles+the error so we can run it in a repeatable way.+-}++------------------------------------------------------------------------+-- Runner+------------------------------------------------------------------------++main :: IO ()+main = do+  args <- getArgs+  case args of+    [strSize, strNum] -> do+       let testsize = read strSize+       let numtests = read strNum+       gen <- initTFGen+       searchForSegfault gen testsize numtests+    [strSize, strNum, strSeed] -> do+       let testsize = read strSize+       let numtests = read strNum+       let seed = read strSeed+       withArgs [] (runTests seed testsize numtests)+    _ -> error "incorrect arguments"++searchForSegfault :: TFGen -> Int -> Int -> IO ()+searchForSegfault gen testsize numtests = do+  let (seed,gen') = next gen+  putStrLn $ unwords ["Running test with seed: ", show seed, "and size:", show testsize,"and number",show numtests]+  pid <- forkProcess (forkTests seed testsize numtests)+  putStrLn $ unwords ["child forked", show pid]+  st <- getProcessStatus True False pid+  print st+  case st of+     Nothing -> error "process status not avaliable?"+     Just (Exited cd) -> do+           putStrLn $ unwords ["Normal Exit", show cd]+           searchForSegfault gen' testsize numtests+     Just (Terminated sig _coreDumped) -> do+           putStrLn $ unwords ["Terminated by signal:", show sig]+     Just (Stopped sig) -> do+           putStrLn $ unwords ["Stopped by signal:", show sig]++forkTests :: Int -> Int -> Int -> IO ()+forkTests seed sz num = do+  fd <- openFd "child.output" WriteOnly (Just stdFileMode) defaultFileFlags{ trunc = True }+  _ <- dupTo fd stdOutput+  withArgs [] (runTests seed sz num)++runTests :: Int -> Int -> Int -> IO ()+runTests seed sz num = do+  ABC.initialize+  putStrLn $ unwords ["running tests in child process..."]+  defaultMainWithIngredients ingrs+      ( localOption (QuickCheckReplay (Just (mkQCGen seed, sz)))+      $ localOption (QuickCheckTests num)+      $ tests+      )++ingrs :: [Ingredient]+ingrs = defaultIngredients++tests :: TestTree+tests =+    testGroup "ABC Bridge"+    [ testGroup "AIG basic" $ basic_tests ABC.aigNetwork+    , testGroup "AIG operations" $ op_tests ABC.aigNetwork+    , testGroup "GIA basic" $ basic_tests ABC.giaNetwork+    , testGroup "GIA operations" $ op_tests ABC.giaNetwork+    , testGroup "GIA QBF tests" $ qbf_tests+    ]