refactor(ldfi2): introduce ormolu and nixpkgs-fmt and reformat all ld…

…fi2 files

shell.nix

@@ -28,12 +28,15 @@ pkgs.mkShell {
     haskellPackages.ghc
     haskellPackages.cabal-install
     haskellPackages.tasty-discover
-    haskellPackages.cabal-fmt       # For formatting .cabal files, example
-                                    # invocation: `cabal-fmt -i ldfi.cabal`.
+    haskellPackages.cabal-fmt # For formatting .cabal files, example
+                              # invocation: `cabal-fmt -i ldfi.cabal`.
     haskellPackages.stylish-haskell # For import statement formatting, can be
                                     # invoked from spacemacs via `, F`.
+    haskellPackages.ormolu # Haskell code formatting, to format all files in the
+                           # current directory: `ormolu --mode inplace $(find . -name '*.hs')`.
     z3
 
+    nixpkgs-fmt # Nix code formatting, example invocation: `nixpkgs-fmt default.nix`.
     git
     nix
     niv

src/ldfi2/Setup.hs

@@ -1,2 +1,3 @@
 import Distribution.Simple
+
 main = defaultMain

src/ldfi2/app/Main.hs

@@ -4,22 +4,21 @@
 module Main where
 
 import qualified Data.Text.IO as T
-import Options.Generic
-
 import qualified Ldfi
-import Ldfi.FailureSpec (FailureSpec(FailureSpec))
+import Ldfi.FailureSpec (FailureSpec (FailureSpec))
 import qualified Ldfi.GitHash as Git
 import Ldfi.Sat (z3Solver)
 import Ldfi.Storage
+import Options.Generic
 
 ------------------------------------------------------------------------
 
 data Config = Config
-  { testId              :: Maybe Int
-  , endOfFiniteFailures :: Maybe Int
-  , maxCrashes          :: Maybe Int
-  , endOfTime           :: Maybe Int
-  , version             :: Bool
+  { testId :: Maybe Int,
+    endOfFiniteFailures :: Maybe Int,
+    maxCrashes :: Maybe Int,
+    endOfTime :: Maybe Int,
+    version :: Bool
   }
   deriving (Generic, Show)
 
@@ -33,11 +32,9 @@ main = do
 go :: Config -> IO () -> IO ()
 go cfg help
   | version cfg = putStrLn Git.version
-  | otherwise   =
-      let
-        mFailSpec = makeFailureSpec (endOfFiniteFailures cfg) (maxCrashes cfg) (endOfTime cfg)
-      in
-        case (testId cfg, mFailSpec) of
+  | otherwise =
+    let mFailSpec = makeFailureSpec (endOfFiniteFailures cfg) (maxCrashes cfg) (endOfTime cfg)
+     in case (testId cfg, mFailSpec) of
           (Just tid, Just failSpec) -> do
             json <- Ldfi.run' sqliteStorage z3Solver tid failSpec
             T.putStrLn json

src/ldfi2/default.nix

@@ -2,20 +2,22 @@
 , compiler ? "ghc8103"
 }:
 let
-  inherit (import sources.gitignore {}) gitignoreSource;
+  inherit (import sources.gitignore { }) gitignoreSource;
   nixpkgs = import sources.nixpkgs {
     config = {
       allowUnfree = true;
-      packageOverrides = super: let pkgs = super.pkgs; in
+      packageOverrides = super:
+        let pkgs = super.pkgs; in
         {
           haskell = super.haskell // {
             packages = super.haskell.packages // {
               ${compiler} = super.haskell.packages.${compiler}.override {
                 overrides = self: super: {
-                  z3 = self.callCabal2nix "z3" (builtins.fetchGit {
-                    url = "[email protected]:stevana/haskell-z3";
-                    rev = "b984d0451969428f6fbc00d65f4d958c8998d05a";
-                  })
+                  z3 = self.callCabal2nix "z3"
+                    (builtins.fetchGit {
+                      url = "[email protected]:stevana/haskell-z3";
+                      rev = "b984d0451969428f6fbc00d65f4d958c8998d05a";
+                    })
                     { z3 = pkgs.z3; };
                 };
               };
@@ -24,14 +26,14 @@ let
         };
     };
   };
-  pkg = nixpkgs.pkgs.haskell.packages.${compiler}.callCabal2nix "ldfi" (./.) {};
-in pkg.overrideAttrs(attrs: {
+  pkg = nixpkgs.pkgs.haskell.packages.${compiler}.callCabal2nix "ldfi" (./.) { };
+in
+pkg.overrideAttrs (attrs: {
+  pname = "detsys-ldfi2";
+  src = gitignoreSource ./.;
   preBuild = ''
     export DETSYS_LDFI_VERSION="${nixpkgs.lib.commitIdFromGitRepo ./../../.git}"
   '';
-  src = gitignoreSource ./.;
   # this should probably check that attrs.checkInputs doesn't exist
   checkInputs = [ nixpkgs.pkgs.haskell.packages.${compiler}.tasty-discover ];
-  pname = "detsys-ldfi2";
-  checkPhase = "";
 })

src/ldfi2/shell.nix

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

src/ldfi2/src/Ldfi.hs

@@ -10,16 +10,16 @@ import qualified Data.Set as Set
 import Data.Text (Text)
 import qualified Data.Text as T
 import qualified GHC.Natural as Nat
-import Text.Read (readMaybe)
-
 import Ldfi.FailureSpec
 import Ldfi.Prop
 import Ldfi.Solver
 import Ldfi.Storage
 import Ldfi.Traces
 import Ldfi.Util
+import Text.Read (readMaybe)
 
 ------------------------------------------------------------------------
+
 -- * Lineage-driven fault injection
 
 data LDFIVar
@@ -31,39 +31,46 @@ type LDFIFormula = FormulaF LDFIVar
 
 lineage :: [Trace] -> LDFIFormula
 lineage ts =
-  Or [ makeVars t | t <- map (foldMap $ Set.singleton . EventVar) ts ]
+  Or [makeVars t | t <- map (foldMap $ Set.singleton . EventVar) ts]
 
 affects :: Fault -> Event -> Bool
 affects (Omission (s, r) ra) (Event s' _ r' ra') = s == s' && r == r' && ra == ra'
 affects (Crash n a) (Event s sa r ra) =
-    (n == s && a <= sa) || (n == r && a <= ra)
-   -- we should be able to be smarter if we knew when something was sent, then
-   -- we could also count for the sender..
+  (n == s && a <= sa) || (n == r && a <= 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 events failures = And
-  [ Var (EventVar event) :+ Or [ Var (FaultVar failure)
-                               | failure <- Set.toList failures
-                               , failure `affects` event]
-  | event <- Set.toList events
-  ]
+failureSemantic events failures =
+  And
+    [ Var (EventVar event)
+        :+ Or
+          [ Var (FaultVar failure)
+            | failure <- Set.toList failures,
+              failure `affects` event
+          ]
+      | event <- Set.toList events
+    ]
 
 -- 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 fs events faults
   | null crashes = TT
-  | otherwise    = And (AtMost crashVars (Nat.naturalToInt $ maxCrashes fs) : crashConditions)
+  | otherwise = And (AtMost crashVars (Nat.naturalToInt $ maxCrashes fs) : crashConditions)
   where
-    crashes = [ c | c@(Crash _ _) <- Set.toList faults ]
+    crashes = [c | c@(Crash _ _) <- Set.toList faults]
     crashVars = map FaultVar crashes
-    crashConditions = [ Var (FaultVar c) :-> Or [ Var (EventVar e)
-                                          | e@(Event s sa _ _) <- Set.toList events
-                                          , s == n && sa < t]
-                      | c@(Crash n t) <- crashes]
+    crashConditions =
+      [ Var (FaultVar c)
+          :-> Or
+            [ Var (EventVar e)
+              | e@(Event s sa _ _) <- Set.toList events,
+                s == n && sa < t
+            ]
+        | c@(Crash n t) <- crashes
+      ]
 
 -- enumerateAllFaults will generate the interesting faults that could affect the
 -- set of events. But since it is pointless to generate a fault that is later
@@ -83,42 +90,53 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events)
 
     possibleFailure :: Event -> Set Fault
     possibleFailure (Event s sa r ra)
-      | eff < ra  = Set.fromList [Crash s eff , Crash r eff]
+      | eff < ra = Set.fromList [Crash s eff, Crash r eff]
       | otherwise = Set.fromList [Omission (s, r) ra, Crash s sa, Crash r ra]
 
 -- ldfi will produce a formula that if solved will give you:
+
 -- * Which faults to introduce
+
 -- * Which events will break (though we are probably not interested in those)
+
 -- such that
+
 -- * 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 -> [Trace] -> FormulaF String
-ldfi fs ts = fmap show $ simplify $ And
-  [ failureSemantic allEvents allFaults
-  , failureSpecConstraint fs allEvents allFaults
-  , Neg (lineage ts)
-  ]
+ldfi fs ts =
+  fmap show $
+    simplify $
+      And
+        [ failureSemantic allEvents allFaults,
+          failureSpecConstraint fs allEvents allFaults,
+          Neg (lineage ts)
+        ]
   where
     allEvents = Set.unions (map Set.fromList ts)
     allFaults = enumerateAllFaults allEvents fs
 
 ------------------------------------------------------------------------
+
 -- * Main
 
 data Fault = Crash Node Time | Omission Edge Time
   deriving (Eq, Ord, Read, Show)
 
 makeFaults :: Solution -> [Fault]
-makeFaults NoSolution        = []
+makeFaults NoSolution = []
 makeFaults (Solution assign) =
   [ f
-  | (key, True) <- Map.toAscList assign
-  , Just (FaultVar f) <- pure $ readMaybe key
+    | (key, True) <- Map.toAscList assign,
+      Just (FaultVar f) <- pure $ readMaybe key
   ]
 
 marshalFaults :: [Fault] -> Text
-marshalFaults  fs = "{\"faults\":" <> marshalList (map marshalFault fs) <> "}"
+marshalFaults fs = "{\"faults\":" <> marshalList (map marshalFault fs) <> "}"
   where
     marshalList :: [Text] -> Text
     marshalList ts = "[" <> T.intercalate "," ts <> "]"
@@ -127,11 +145,13 @@ marshalFaults  fs = "{\"faults\":" <> marshalList (map marshalFault fs) <> "}"
     marshalFault (Crash from at) =
       "{\"kind\":\"crash\",\"from\":" <> T.pack (show from) <> ",\"at\":" <> T.pack (show at) <> "}"
     marshalFault (Omission (from, to) at) =
-      "{\"kind\":\"omission\",\"from\":" <> T.pack (show from) <> ",\"to\":" <> T.pack (show to) <>
-      ",\"at\":" <> T.pack (show at) <> "}"
+      "{\"kind\":\"omission\",\"from\":" <> T.pack (show from) <> ",\"to\":" <> T.pack (show to)
+        <> ",\"at\":"
+        <> T.pack (show at)
+        <> "}"
 
 run :: Monad m => Storage m -> Solver m -> TestId -> FailureSpec -> m [Fault]
-run Storage{load} Solver{solve} testId failureSpec = do
+run Storage {load} Solver {solve} testId failureSpec = do
   traces <- load testId
   sol <- solve (ldfi failureSpec traces)
   return (makeFaults sol)

src/ldfi2/src/Ldfi/FailureSpec.hs

@@ -1,15 +1,17 @@
 module Ldfi.FailureSpec where
 
-import Numeric.Natural
-
 import Ldfi.Traces (Time)
+import Numeric.Natural
 
 ------------------------------------------------------------------------
+
 -- * Failure specification
 
 data FailureSpec = FailureSpec
-  { endOfFiniteFailures :: Time    -- ^ When finite failures, i.e. omissions,
-                                   -- stop (a.k.a. EOF).
-  , maxCrashes          :: Natural -- ^ The maximum amount of crashes allowed.
-  , endOfTime           :: Time    -- ^ When the test stops (a.k.a. EOT).
+  { -- | When finite failures, i.e. omissions, stop (a.k.a. EOF).
+    endOfFiniteFailures :: Time,
+    -- | The maximum amount of crashes allowed.
+    maxCrashes :: Natural,
+    -- | When the test stops (a.k.a. EOT).
+    endOfTime :: Time
   }

src/ldfi2/src/Ldfi/GitHashImpl.hs

@@ -18,10 +18,10 @@ getVersionFromEnv = do
   getEnv "DETSYS_LDFI_VERSION"
     `catchIOError` \e ->
       if isDoesNotExistError e
-      then return "unknown"
-      else throwIO e
+        then return "unknown"
+        else throwIO e
 
 tGetGitInfo :: Q (TExp String)
 tGetGitInfo = do
-    s <- runIO getVersionFromEnv
-    liftTyped s
+  s <- runIO getVersionFromEnv
+  liftTyped s