perf(ldfi): Increase performance of ldfi

Changes:
* Use Hashmap instead of `Map String AST` for remembering the Variables of z3.
Furthermore rather than being a map of the Show of the variable, we keep it as
LDFIVar.
* The SAT variables are generated on demand, rather than all up-front.
* Don't do a simplification (i.e call `simplify`) of the ldfi formuala.
* Don't recompute Set.toList when uneccesarry (the set of all faults were often
  used quite often, and when iterated it used Set.toList in different places).
* Remove an uneccessary use of `(!!)` in `z3SolveAll`.

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
 

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

src/ldfi/shell.nix

@@ -1,5 +1,5 @@
 { sources ? import ./../../nix/sources.nix
-, compiler ? "ghc8103"
+, compiler ? "ghc8104"
 }:
 
 (import ./default.nix { inherit sources compiler; }).env

src/ldfi/src/Ldfi.hs

@@ -1,25 +1,27 @@
 {-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 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
 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)

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

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

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