Hs dependency upgrade

.github/workflows/master.yml

@@ -8,7 +8,7 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  ghc_version: "9.6.5"
+  ghc_version: "9.8.4"
   stack_version: "2.15.1"
   hpack_version: '0.36'
 

.github/workflows/release.yml

@@ -5,7 +5,7 @@ on:
       - release
 
 env:
-  ghc_version: "9.6.5"
+  ghc_version: "9.8.4"
   stack_version: "2.15.1"
   hpack_version: '0.36'
 

.github/workflows/test.yml

@@ -10,7 +10,7 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  ghc_version: "9.6.5"
+  ghc_version: "9.8.4"
   stack_version: "2.15.1"
   hpack_version: '0.36'
 
@@ -118,6 +118,16 @@ jobs:
       - name: Test
         run: GC_DONT_GC=1 nix develop .#cabal --command bash -c "hpack ./booster && hpack dev-tools && cabal update && cabal build all && cabal test --enable-tests --test-show-details=direct kore-test unit-tests"
 
+      - name: 'DEBUG MacOS build error'
+        if: ${{ contains(matrix.os, 'macos') }}
+        run: |
+          ls result/bin
+          for file in result/bin/*; do
+              echo $file;
+              strings $file | grep -e "/nix/store"
+          done
+
+
   nix-integration:
     name: 'Nix / Integration'
     needs: formatting

.hlint.yaml

@@ -16,6 +16,13 @@
 # applied to Kore.Rewrite.SMT.Evaluator.evaluate.
 - ignore: {name: "Redundant evaluate"}
 
+# This warning should apply to Data.NonEmpty.unzip but is mistakenly
+# applied to Data.List.unzip
+- ignore: {name: "Avoid NonEmpty.unzip", within: [Booster.Pattern.Rewrite]}
+
+# This suggestion is invalid since ghc-9.8.4 decided to emit a warning about partial functions
+- ignore: {name: "Use head"}
+
 # Corporate style
 - ignore: {name: "Move brackets to avoid $" }
 - ignore: {name: "Use tuple-section"}
@@ -94,6 +101,10 @@
     name: "Redundant bracket"
     within:
       - Kore.Internal.TermLike.TermLike
+# decreases readability
+- ignore: {name: "Functor law"}
+- ignore: {name: "Move filter"}
+- ignore: {name: "Move mapMaybe"}
 
 
 # Haskell names match K names

booster/library/Booster/Builtin/LIST.hs

@@ -44,12 +44,12 @@ listGetHook [KList _ heads mbRest, intArg] =
                     if i < headLen
                         then pure $ Just $ heads !! i -- positive index in range
                         else -- headLen <= i
-                        case mbRest of
-                            Nothing ->
-                                -- index too large
-                                pure Nothing -- actually #Bottom
-                            Just _ ->
-                                pure Nothing
+                            case mbRest of
+                                Nothing ->
+                                    -- index too large
+                                    pure Nothing -- actually #Bottom
+                                Just _ ->
+                                    pure Nothing
                 | otherwise -> -- i < 0, negative index, consider rest
                     case mbRest of
                         Nothing

booster/library/Booster/JsonRpc.hs

@@ -27,7 +27,7 @@ import Data.Foldable
 import Data.List (singleton)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
-import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, isJust, listToMaybe, mapMaybe)
 import Data.Proxy qualified
 import Data.Sequence (Seq)
 import Data.Set qualified as Set
@@ -469,9 +469,9 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
         innerSorts = mapMaybe sortOfJson $ KoreJson.term t : subAndPred
         topLevelSort = case innerSorts of
             [] -> KoreJson.SortApp (KoreJson.Id "SortGeneratedTopCell") []
-            xs ->
-                if all (== head xs) (tail xs) -- we know xs is non-empty, hence `head` is safe here
-                    then KoreJson.SortApp (head xs).name []
+            x : xs ->
+                if all (== x) xs
+                    then KoreJson.SortApp x.name []
                     else KoreJson.SortApp (KoreJson.Id "SortGeneratedTopCell") []
      in t
             { KoreJson.term =
@@ -667,10 +667,10 @@ mkLogRewriteTrace
                                             { reason = "Uncertain about a condition in rule"
                                             , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes r)
                                             }
-                                    RewriteRemainderPredicate rs _ _ ->
+                                    RewriteRemainderPredicate rules _ _ ->
                                         Failure
                                             { reason = "Uncertain about the remainder after applying a rule"
-                                            , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes (head rs))
+                                            , _ruleId = fmap (getUniqueId . uniqueId . Definition.attributes) $ listToMaybe rules
                                             }
                                     DefinednessUnclear r _ undefReasons ->
                                         Failure

booster/library/Booster/LLVM/TH.hs

@@ -169,6 +169,7 @@ cTypeToHs = \case
             C.TyDouble -> ''Foreign.C.CDouble
             C.TyLDouble -> error "TyLDouble unsupported"
             C.TyFloatN _ _ -> error "TyFloatN unsupported"
+            C.TyBFloat16{} -> error "TyBFloat16 unsupported"
         C.TyComplex _floatType -> error "TyComplex unsupported"
         C.TyComp _compTypeRef -> error "TyComp unsupported"
         C.TyEnum _enumTypeRef -> error "TyEnum unsupported"

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -229,12 +229,13 @@ pushRecursion t = eqState $ do
 popRecursion :: LoggerMIO io => EquationT io ()
 popRecursion = do
     s <- getState
-    if null s.recursionStack
-        then do
+    case s.recursionStack of
+        [] -> do
             withContext CtxAbort $
                 logMessage ("Trying to pop an empty recursion stack" :: Text)
             throw $ InternalError "Trying to pop an empty recursion stack"
-        else eqState $ put s{recursionStack = tail s.recursionStack}
+        _hd : rest ->
+            eqState $ put s{recursionStack = rest}
 
 toCache :: LoggerMIO io => CacheTag -> Term -> Term -> EquationT io ()
 toCache LLVM orig result = eqState . modify $

booster/library/Booster/Pattern/Implies.hs

@@ -130,7 +130,6 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                         then -- we are being conservative here for now and returning an error.
                                         -- since we have already simplified the LHS, we may want to eventually return implise, but the condition
                                         -- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
-
                                             pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
                                                 "match remainder: "
                                                     <> renderDefault
@@ -155,7 +154,6 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                         (externaliseExistTerm existsR patR.term)
                                         subst
                                 else -- FIXME This is incomplete because patL.constraints are not assumed in the check.
-
                                     ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
                                         (Right newPreds, _) ->
                                             if all (== Predicate TrueBool) newPreds

booster/library/Booster/Pattern/Match.hs

@@ -399,7 +399,8 @@ matchSymbolAplications
                 then
                     failWith
                         (DifferentSymbols (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2))
-                else addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2)
+                else
+                    addIndeterminate (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2)
         | length args1 /= length args2 =
             failWith $
                 ArgLengthsDiffer (SymbolApplication symbol1 sorts1 args1) (SymbolApplication symbol2 sorts2 args2)

booster/library/Booster/SMT/Translate.hs

@@ -27,7 +27,7 @@ import Data.Char (isDigit)
 import Data.Coerce (coerce)
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Maybe (catMaybes, fromMaybe, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, listToMaybe, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text (Text, pack)
 import Prettyprinter (pretty)
@@ -205,11 +205,10 @@ equationToSMTLemma equation
                     | (t, v) <- Map.toList m
                     ]
             lemmaId =
-                head $
+                fromMaybe "Unknown location" . listToMaybe $
                     catMaybes
                         [ fmap Pretty.pretty equation.attributes.ruleLabel
                         , fmap Pretty.pretty equation.attributes.location
-                        , Just "Unknown location"
                         ]
         -- free variables (not created by abstraction during
         -- translation) are all-quantified on the outside

booster/library/Booster/Syntax/Json/Internalise.hs

@@ -488,7 +488,7 @@ mkSubstitution initialSubst =
                 Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst]
         equations =
             [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts]
-     in execState breakCycles (Map.map head substMap, equations)
+     in execState breakCycles (Map.map (!! 0) substMap, equations)
   where
     breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) ()
     breakCycles = do
@@ -734,8 +734,10 @@ isTermM pat = case pat of
     Syntax.KJNot{} -> pure False
     Syntax.KJAnd{patterns} -> do
         terms <- mapM isTermM patterns
-        when (length (nub terms) /= 1) $ throwE (InconsistentPattern pat)
-        pure $ head terms
+        case nub terms of
+            [] -> throwE (InconsistentPattern pat) -- empty and not allowed
+            [x] -> pure x
+            _more -> throwE (InconsistentPattern pat)
     Syntax.KJOr{} -> pure False
     Syntax.KJImplies{} -> pure False
     Syntax.KJIff{} -> pure False

booster/library/Booster/Syntax/ParsedKore/Internalise.hs

@@ -339,9 +339,11 @@ addModule
         things `mappedBy` getKey =
             let sorted :: [[a]]
                 sorted = groupBy ((==) `on` getKey) $ sortOn getKey things
-                (good, dups) = partition (null . tail) sorted
+                isGood [_] = True
+                isGood _ = False
+                (good, dups) = partition isGood sorted
              in ( Map.fromAscList [(getKey a, a) | [a] <- good]
-                , [(getKey $ head d, d) | d <- dups]
+                , [(getKey d', d) | d@(d' : _) <- dups]
                 )
 
         -- if two symbols have the same smtlib attribute, they get renamed
@@ -786,9 +788,9 @@ internaliseRulePattern partialDefinition ref maybeVars f t = do
     unless (null ceilConditions) $
         throwE $
             DefinitionPatternError ref CeilNotAllowed
-    unless (null unsupported) $
-        throwE $
-            DefinitionPatternError ref (NotSupported (head unsupported))
+    case unsupported of
+        [] -> pure ()
+        x : _ -> throwE $ DefinitionPatternError ref (NotSupported x)
     pure
         ( Util.modifyVariablesInT f term
         , map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution)
@@ -975,10 +977,9 @@ internaliseCeil partialDef left right sortVars attrs = do
             -- turn substitution-like predicates back into equations
             constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution
             unsupported = internalPs.unsupported
-        unless (null unsupported) $
-            throwE $
-                DefinitionPatternError (sourceRef attrs) $
-                    NotSupported (head unsupported)
+        case unsupported of
+            [] -> pure ()
+            x : _ -> throwE $ DefinitionPatternError (sourceRef attrs) $ NotSupported x
         pure $
             map (Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) . coerce) constraints
 
@@ -1013,9 +1014,11 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
     unless (null ceils) $
         throwE $
             DefinitionPatternError (sourceRef attrs) CeilNotAllowed
-    unless (null unsupported) $
-        throwE $
-            DefinitionPatternError (sourceRef attrs) (NotSupported (head unsupported))
+    case unsupported of
+        [] -> pure ()
+        x : _ ->
+            throwE $
+                DefinitionPatternError (sourceRef attrs) (NotSupported x)
     -- extract argument binders from predicates and inline in to LHS term
     argPairs <- mapM internaliseArg args
     let lhs =

booster/tools/booster/Proxy.hs

@@ -601,12 +601,11 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                             , nextStates = Nothing
                                             , logs = combineLogs $ res.logs : simplifiedStateLogs : logsOnly
                                             }
-                            | length filteredNexts == 1 -> do
+                            | [onlyNext] <- filteredNexts -> do
                                 -- all but one next states are bottom, execution should proceed
                                 -- Note that we've effectively made a rewrite step here, so we need to
                                 -- extract the rule-id information from the result we proceed with
-                                let onlyNext = head filteredNexts
-                                    rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId
+                                let rewriteRuleId = fromMaybe "UNKNOWN" onlyNext.ruleId
                                     proxyRewriteStepLogs
                                         | Just True <- logSettings.logSuccessfulRewrites =
                                             Just . (: []) $

booster/unit-tests/Test/Booster/Syntax/Json.hs

@@ -1,3 +1,6 @@
+-- no head/tail warnings
+{-# OPTIONS_GHC -Wno-x-partial #-}
+
 module Test.Booster.Syntax.Json (
     -- Tasty wrappers
     test_prettyPattern,

cabal.project

@@ -8,17 +8,10 @@ package *
   ghc-options: -fhide-source-paths -haddock
 
 package kore
-  ghc-options: -Wall -Werror
+  ghc-options: -Wall -Werror -Wno-x-partial
   profiling-detail: exported-functions
 
 source-repository-package
   type: git
-  location: https://github.com/goodlyrottenapple/tasty-test-reporter.git
-  tag: b704130545aa3925a8487bd3e92f1dd5ce0512e2
-
-source-repository-package
-  type: git
-  location: https://github.com/goodlyrottenapple/profiteur.git
-  tag: 7b30bbe6b2a6b72a5b4896f3a0eed5587a5bf465
-
-constraints: profiteur +embed-data-files
+  location: https://github.com/jberthold/tasty-test-reporter.git
+  tag: 3abbfa942553f0986393af44eda0cb69bcaba6ad