diff --git a/src/ldfi/cabal.project b/src/ldfi/cabal.project index 0e80d1c1..fff85ef8 100644 --- a/src/ldfi/cabal.project +++ b/src/ldfi/cabal.project @@ -1,6 +1,6 @@ packages: . -with-compiler: ghc-8.10.3 +with-compiler: ghc-8.10.4 reject-unconstrained-dependencies: all diff --git a/src/ldfi/ldfi.cabal b/src/ldfi/ldfi.cabal index 8c24e934..ba4a2ad8 100644 --- a/src/ldfi/ldfi.cabal +++ b/src/ldfi/ldfi.cabal @@ -32,17 +32,19 @@ library -- GHC boot library dependencies: -- (https://gitlab.haskell.org/ghc/ghc/-/blob/master/packages) build-depends: - base >=4.14 && <4.15 + base >=4.14 && <4.15 , containers , filepath , mtl , template-haskell + , unordered-containers -- Other dependencies: build-depends: aeson , binary , bytestring + , hashable , QuickCheck , sqlite-simple , text diff --git a/src/ldfi/shell.nix b/src/ldfi/shell.nix index bc62c765..22a04e0b 100644 --- a/src/ldfi/shell.nix +++ b/src/ldfi/shell.nix @@ -1,5 +1,5 @@ { sources ? import ./../../nix/sources.nix -, compiler ? "ghc8103" +, compiler ? "ghc8104" }: (import ./default.nix { inherit sources compiler; }).env diff --git a/src/ldfi/src/Ldfi.hs b/src/ldfi/src/Ldfi.hs index 84c1cc46..50e8ddda 100644 --- a/src/ldfi/src/Ldfi.hs +++ b/src/ldfi/src/Ldfi.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-} @@ -6,12 +7,14 @@ module Ldfi where import qualified Data.Aeson as Aeson import qualified Data.ByteString.Lazy as BSL +import Data.Hashable (Hashable) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text.Encoding as TE +import GHC.Generics (Generic) import qualified GHC.Natural as Nat import Ldfi.FailureSpec import qualified Ldfi.Marshal.Faults as MF @@ -19,7 +22,6 @@ import Ldfi.Prop import Ldfi.Solver import Ldfi.Storage import Ldfi.Traces -import Text.Read (readMaybe) ------------------------------------------------------------------------ @@ -28,7 +30,9 @@ import Text.Read (readMaybe) data LDFIVar = EventVar Event | FaultVar Fault - deriving (Eq, Ord, Read, Show) + deriving (Eq, Ord, Read, Show, Generic) + +instance Hashable LDFIVar type LDFIFormula = FormulaF LDFIVar @@ -43,37 +47,45 @@ affects (Crash n a) (Event s sa r ra) = -- failureSemantic computes a formula s.t for each event either (xor) the event -- is true or one of the failures that affect it is true -failureSemantic :: Set Event -> Set Fault -> LDFIFormula +failureSemantic :: Set Event -> [Fault] -> LDFIFormula failureSemantic events faults = And - [ Var (EventVar event) - :+ Or - [ Var (FaultVar failure) - | failure <- Set.toList faults, - failure `affects` event - ] + [ f + (Var (EventVar event)) + [ Var (FaultVar failure) + | failure <- faults, + failure `affects` event + ] | event <- Set.toList events ] + where + f x [] = Neg x + f x [y] = x :+ y + f x xs = x :+ Or xs -- failureSpecConstraint is the formula that makes sure we are following the -- Failure Specification. Although we will never generate any faults that occur -- later than eff, so we don't have to check that here -failureSpecConstraint :: FailureSpec -> Set Event -> Set Fault -> LDFIFormula +failureSpecConstraint :: FailureSpec -> Set Event -> [Fault] -> LDFIFormula failureSpecConstraint fs events faults | null crashes = TT | otherwise = And (AtMost crashVars (Nat.naturalToInt $ maxCrashes fs) : crashConditions) where - crashes = [c | c@(Crash _ _) <- Set.toList faults] + crashes = [c | c@(Crash _ _) <- faults] crashVars = map FaultVar crashes + -- this seems to allocate quite a bit.. crashConditions = - [ Var (FaultVar c) - :-> Or - [ Var (EventVar e) - | e@(Event s sa _ _) <- Set.toList events, - s == n && sa < t - ] + [ f + (Var (FaultVar c)) + [ Var (EventVar e) + | e@(Event s sa _ _) <- Set.toList events, + s == n && sa < t + ] | c@(Crash n t) <- crashes ] + f x [] = Neg x + f x [y] = x :-> y + f x xs = x :-> Or xs -- `enumerateAllFaults` will generate the interesting faults that could affect -- the set of events. But since it is pointless to generate a fault that is @@ -103,38 +115,36 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events) -- * If we introduce faults the corresponding events are false (`failureSemantic`) -- * We don't intruduce faults that violates the failure spec (`failureSpecConstaint`) -- * The lineage graph from traces are not satisfied (`Neg lineage`) -ldfi :: FailureSpec -> Map RunId Trace -> Failures -> FormulaF String +ldfi :: FailureSpec -> Map RunId Trace -> Failures -> FormulaF LDFIVar ldfi failureSpec tracesByRuns failures = - fmap show $ - simplify $ - And $ - addLimit - [ failureSemantic allEvents allFaults, - failureSpecConstraint failureSpec allEvents allFaults, - Neg (lineage traces), - And - [ Neg $ And $ map (Var . FaultVar) faults - | faults <- fFaultsFromFailedRuns failures - ] + And $ + addLimit + [ failureSemantic allEvents allFaultsList, + failureSpecConstraint failureSpec allEvents allFaultsList, + Neg (lineage traces), + And + [ Neg $ And $ map (Var . FaultVar) faults + | faults <- fFaultsFromFailedRuns failures ] + ] where addLimit xs = case numberOfFaultLimit failureSpec of Nothing -> xs - Just l -> AtMost [FaultVar $ f | f <- Set.toList allFaults] l : xs + Just l -> AtMost [FaultVar $ f | f <- allFaultsList] l : xs traces = Map.elems tracesByRuns allEvents = Set.unions (map Set.fromList traces) allFaults = enumerateAllFaults allEvents failureSpec + allFaultsList = Set.toList allFaults ------------------------------------------------------------------------ -- * Main -makeFaults :: Solution -> [Fault] +makeFaults :: Solution LDFIVar -> [Fault] makeFaults NoSolution = [] makeFaults (Solution assign) = [ f - | (key, True) <- Map.toAscList assign, - Just (FaultVar f) <- pure $ readMaybe key + | (FaultVar f, True) <- Map.toAscList assign ] marshalFaults :: [Fault] -> Text @@ -144,12 +154,12 @@ marshalFaults = TE.decodeUtf8 . BSL.toStrict . Aeson.encode . MF.Faults . map co convert (Crash f a) = MF.Crash f a convert (Omission (f, t) a) = MF.Omission f t a -run :: Monad m => Storage m -> Solver m -> TestInformation -> FailureSpec -> m [Fault] +run :: Monad m => Storage m -> Solver LDFIVar m -> TestInformation -> FailureSpec -> m [Fault] run Storage {load, loadFailures} Solver {solve} testInformation failureSpec = do traces <- load testInformation failures <- loadFailures testInformation sol <- solve (ldfi failureSpec traces failures) return (makeFaults sol) -run' :: Monad m => Storage m -> Solver m -> TestInformation -> FailureSpec -> m Text +run' :: Monad m => Storage m -> Solver LDFIVar m -> TestInformation -> FailureSpec -> m Text run' storage solver testInformation failureSpec = fmap marshalFaults (run storage solver testInformation failureSpec) diff --git a/src/ldfi/src/Ldfi/Sat.hs b/src/ldfi/src/Ldfi/Sat.hs index 47351f25..26c21a06 100644 --- a/src/ldfi/src/Ldfi/Sat.hs +++ b/src/ldfi/src/Ldfi/Sat.hs @@ -1,8 +1,12 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} + module Ldfi.Sat where -import Data.Map (Map) +import Data.HashMap.Strict (HashMap) +import qualified Data.HashMap.Strict as HashMap +import Data.Hashable (Hashable) import qualified Data.Map as Map -import qualified Data.Set as Set import GHC.Stack (HasCallStack) import Ldfi.Prop import Ldfi.Solver @@ -12,28 +16,59 @@ import Z3.Monad hiding (Solver) -- * SAT formula -type Env = Map String AST +type VarConstraint k = (Ord k, Hashable k, Show k) + +type Env k = HashMap k AST -liftFun :: MonadZ3 z3 => Env -> Formula -> Formula -> (AST -> AST -> z3 AST) -> z3 AST +liftFun :: (VarConstraint k, MonadZ3 z3) => Env k -> FormulaF k -> FormulaF k -> (AST -> AST -> z3 AST) -> z3 (AST, Env k) liftFun env l r f = do - l' <- translate env l - r' <- translate env r - f l' r' + (l', env') <- translate' env l + (r', env'') <- translate' env' r + a <- f l' r' + pure (a, env'') + +mapMTs :: Monad m => (s -> a -> m (b, s)) -> s -> [a] -> m ([b], s) +mapMTs _ s [] = pure ([], s) +mapMTs f s (x : xs) = do + (y, s') <- f s x + (ys, s'') <- mapMTs f s' xs + pure (y : ys, s'') -translate :: MonadZ3 z3 => Env -> Formula -> z3 AST -translate env f0 = case f0 of +-- Should try to speed up +translateVar :: (VarConstraint k, MonadZ3 z3) => Env k -> k -> z3 (AST, Env k) +translateVar env v = case HashMap.lookup v env of + Nothing -> do + v' <- mkFreshBoolVar (show v) + pure (v', HashMap.insert v v' env) + Just v' -> pure (v', env) + +translate' :: (VarConstraint k, MonadZ3 z3) => Env k -> FormulaF k -> z3 (AST, Env k) +translate' env f0 = case f0 of l :&& r -> liftFun env l r (\l' r' -> mkAnd [l', r']) l :|| r -> liftFun env l r (\l' r' -> mkOr [l', r']) l :+ r -> liftFun env l r mkXor - And fs -> mkAnd =<< mapM (translate env) fs - Or fs -> mkOr =<< mapM (translate env) fs - Neg f -> mkNot =<< translate env f + And fs -> withEnv mkAnd =<< mapMTs translate' env fs + Or fs -> withEnv mkOr =<< mapMTs translate' env fs + Neg f -> withEnv mkNot =<< translate' env f l :<-> r -> liftFun env l r mkIff l :-> r -> liftFun env l r mkImplies - TT -> mkTrue - FF -> mkFalse - Var v -> return (env Map.! v) - AtMost vs i -> mkAtMost [env Map.! v | v <- vs] i + TT -> (,env) <$> mkTrue + FF -> (,env) <$> mkFalse + Var v -> translateVar env v + AtMost vs i -> do + (vs', env') <- mapMTs translateVar env vs + (,env') <$> mkAtMost vs' i + +withEnv :: Monad m => (a -> m b) -> (a, s) -> m (b, s) +withEnv m (x, env) = do + a <- m x + pure (a, env) + +translate :: (VarConstraint k, MonadZ3 z3) => FormulaF k -> z3 (AST, [k], [AST]) +translate f0 = do + (a, env) <- translate' HashMap.empty f0 + let xs = HashMap.toList env + return (a, map fst xs, map snd xs) oldSolve :: MonadZ3 z3 => z3 AST -> z3 Result oldSolve m = do @@ -42,20 +77,17 @@ oldSolve m = do (result, _mModel) <- getModel return result -z3Solve :: HasCallStack => Formula -> IO Solution +z3Solve :: (VarConstraint k, HasCallStack) => FormulaF k -> IO (Solution k) z3Solve f = do sols <- z3SolveAll (Just 1) f case sols of [] -> return NoSolution sol : _ -> return sol -z3SolveAll :: HasCallStack => Maybe Int -> Formula -> IO [Solution] +z3SolveAll :: (VarConstraint k, HasCallStack) => Maybe Int -> FormulaF k -> IO [Solution k] z3SolveAll limit f = do - let vs = Set.toList (getVars f) evalZ3 $ do - vs' <- mapM mkFreshBoolVar vs - let env = Map.fromList (zip vs vs') - a <- translate env f + (a, vs, vs') <- translate f assert a go 0 [] vs vs' where @@ -64,11 +96,12 @@ z3SolveAll limit f = do Nothing -> False Just k -> n >= k - go :: MonadZ3 z3 => Int -> [Solution] -> [String] -> [AST] -> z3 [Solution] + -- should vs be list? + go :: (VarConstraint k, MonadZ3 z3) => Int -> [Solution k] -> [k] -> [AST] -> z3 [Solution k] go n acc vs vs' | limitReached n = return (reverse acc) | otherwise = do - (result, mModel) <- getModel + (result, mModel) <- getModel -- this takes most time case result of Undef -> error "impossible" Unsat -> return (reverse acc) @@ -79,10 +112,11 @@ z3SolveAll limit f = do let bs = map (maybe (error "impossible") id) mbs bs' <- mapM - (\(ix, b) -> mkNot =<< mkEq (vs' !! ix) =<< mkBool b) - (zip [0 .. length bs - 1] bs) + (\(v', b) -> mkNot =<< mkEq v' =<< mkBool b) + (zip vs' bs) + -- we should have a comment why we need this assert assert =<< mkOr bs' go (succ n) (Solution (Map.fromList (zip vs bs)) : acc) vs vs' -z3Solver :: Solver IO +z3Solver :: VarConstraint k => Solver k IO z3Solver = Solver z3Solve diff --git a/src/ldfi/src/Ldfi/Solver.hs b/src/ldfi/src/Ldfi/Solver.hs index c6420674..e48ecdf3 100644 --- a/src/ldfi/src/Ldfi/Solver.hs +++ b/src/ldfi/src/Ldfi/Solver.hs @@ -7,8 +7,8 @@ import Ldfi.Prop -- * Solver -data Solution = NoSolution | Solution (Map String Bool) +data Solution key = NoSolution | Solution (Map key Bool) deriving (Show) -data Solver m = Solver - {solve :: Formula -> m Solution} +data Solver key m = Solver + {solve :: FormulaF key -> m (Solution key)} diff --git a/src/ldfi/src/Ldfi/Storage.hs b/src/ldfi/src/Ldfi/Storage.hs index e907fdf4..6d08fe99 100644 --- a/src/ldfi/src/Ldfi/Storage.hs +++ b/src/ldfi/src/Ldfi/Storage.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -7,6 +8,7 @@ import Control.Arrow (second) import Control.Exception import Data.Aeson (decode) import qualified Data.Binary.Builder as BB +import Data.Hashable (Hashable) import Data.List (groupBy, intercalate) import Data.Map (Map) import qualified Data.Map as Map @@ -16,6 +18,7 @@ import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.Encoding as TextE import Database.SQLite.Simple +import GHC.Generics (Generic) import qualified Ldfi.Marshal.Faults as MF import Ldfi.Traces import System.Environment @@ -29,7 +32,9 @@ type TestId = Int type RunId = Int data Fault = Crash Node Time | Omission Edge Time - deriving (Eq, Ord, Read, Show) + deriving (Eq, Ord, Read, Show, Generic) + +instance Hashable Fault data Failures = Failures { fFaultsFromFailedRuns :: [[Fault]], diff --git a/src/ldfi/src/Ldfi/Traces.hs b/src/ldfi/src/Ldfi/Traces.hs index 01d46568..ed4f58dd 100644 --- a/src/ldfi/src/Ldfi/Traces.hs +++ b/src/ldfi/src/Ldfi/Traces.hs @@ -1,7 +1,11 @@ +{-# LANGUAGE DeriveGeneric #-} + module Ldfi.Traces where +import Data.Hashable (Hashable) import Data.Set (Set) import qualified Data.Set as Set +import GHC.Generics (Generic) import GHC.Natural ------------------------------------------------------------------------ @@ -16,7 +20,9 @@ data Event = Event to :: Node, recv :: Time } - deriving (Eq, Ord, Read, Show) + deriving (Eq, Ord, Read, Show, Generic) + +instance Hashable Event type Node = String