Merge pull request #255 from GaloisInc/ghc-9.8

Allow building with GHC 9.8

.github/workflows/gen_matrix.pl

@@ -94,6 +94,7 @@
 
 version(ubuntu, "ubuntu-latest").
 
+version(ghc, "9.8.1").
 version(ghc, "9.6.2").
 version(ghc, "9.4.4").
 version(ghc, "9.2.2").

.github/workflows/test.yml

@@ -105,6 +105,7 @@ jobs:
             9.2.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;;
             9.4.4) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
             9.6.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
+            9.8.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.11 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

what4-abc/what4-abc.cabal

@@ -17,7 +17,7 @@ Description:
 
 library
   build-depends:
-    base >= 4.7 && < 4.19,
+    base >= 4.7 && < 4.20,
     aig,
     abcBridge >= 0.11,
     bv-sized >= 1.0.0,

what4-blt/what4-blt.cabal

@@ -26,7 +26,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
-    base >= 4.7 && < 4.19,
+    base >= 4.7 && < 4.20,
     blt >= 0.12.1,
     containers,
     what4 >= 0.4,

what4-transition-system/what4-transition-system.cabal

@@ -13,7 +13,7 @@ build-type:    Simple
 common dependencies
   build-depends:
     , ansi-wl-pprint       ^>=0.6
-    , base                 >=4.12 && <4.19
+    , base                 >=4.12 && <4.20
     , bytestring
     , containers           ^>=0.6
     , io-streams

what4/src/What4/Protocol/SMTLib2.hs

@@ -112,6 +112,7 @@ import           Data.Foldable
 import           Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import           Data.IORef
+import qualified Data.List as List
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Monoid
@@ -152,6 +153,7 @@ import qualified What4.Config as CFG
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import qualified What4.Interface as I
+import           What4.Panic
 import           What4.ProblemFeatures
 import           What4.Protocol.Online
 import           What4.Protocol.ReadDecimal
@@ -1191,11 +1193,31 @@ parseExpr sym sexp = case sexp of
           liftIO $ Some <$> I.bvSelect sym j_repr n_repr arg_expr
         _ -> throwError ""
   SApp ((SAtom operator) : operands) -> case HashMap.lookup operator (opTable @sym) of
+    -- Sometimes, binary operators can be applied to more than two operands,
+    -- e.g., (+ 1 2 3 4). We want to uniformly represent binary operators such
+    -- that they are always applied to two operands, so this case converts the
+    -- expression above to:
+    --
+    -- - (+ (+ (+ 1 2) 3) 4) (if + is left-associative)
+    -- - (+ 1 (+ 2 (+ 3 4))) (if + is right-associative)
+    --
+    -- We then call `parseExpr` and recurse, which will reach one of the cases
+    -- below.
     Just op
-      | Just assoc <- opAssoc op
-      , length operands > 2 -> case assoc of
-        LeftAssoc -> parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) (head operands) (tail operands)
-        RightAssoc -> parseExpr sym $ foldr' (\arg acc -> SApp [SAtom operator, arg, acc]) (last operands) (init operands)
+      | Just LeftAssoc <- opAssoc op
+      , op1:op2:op3:ops <- operands ->
+          parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) op1 (op2:op3:ops)
+
+        -- For right-associative operators, we could alternatively call
+        -- init/last on the list of operands and call foldr on the results. The
+        -- downside, however, is that init/last are partial functions. To avoid
+        -- this partiality, we instead match on `reverse operands` and call
+        -- foldl on the results (with the order of acc/arg swapped). This
+        -- achieves the same end result and maintains the same asymptotic
+        -- complexity as using init/tail.
+      | Just RightAssoc <- opAssoc op
+      , op1:op2:op3:ops <- List.reverse operands ->
+          parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, arg, acc]) op1 (op2:op3:ops)
     Just (Op1 arg_types fn) -> do
       args <- mapM (parseExpr sym) operands
       exprAssignment arg_types args >>= \case
@@ -1236,6 +1258,7 @@ parseExpr sym sexp = case sexp of
                                        (show n)
     _ -> throwError ""
   _ -> throwError ""
+
 -- | Verify a list of arguments has a single argument and
 -- return it, else raise an error.
 readOneArg ::
@@ -1360,8 +1383,10 @@ instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where
           AckUnsat   -> Just $ Unsat ()
           AckUnknown -> Just Unknown
           _ -> Nothing
-    in getLimitedSolverResponse "sat result" satRsp s
-       (head $ reverse $ checkCommands p)
+        cmd = case reverse $ checkCommands p of
+                cmd':_ -> cmd'
+                []     -> panic "smtSatResult" ["Empty list of checkCommands"]
+    in getLimitedSolverResponse "sat result" satRsp s cmd
 
   smtUnsatAssumptionsResult p s =
     let unsatAssumpRsp = \case

what4/test/AdapterTest.hs

@@ -34,6 +34,7 @@ import           Data.Parameterized.Some
 import           What4.Config
 import           What4.Expr
 import           What4.Interface
+import           What4.Panic
 import           What4.Protocol.SMTLib2.Response ( strictSMTParsing )
 import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) )
 import           What4.Protocol.VerilogWriter
@@ -224,6 +225,11 @@ mkConfigTests adapters =
       in fmap mkPCTest adaptrs
 
     deprecatedConfigTests adaptrs =
+      let firstAdapter adptrs =
+            case adptrs of
+              adptr:_ -> adptr
+              [] -> panic "deprecatedConfigTests" ["Empty list of adapters"]
+      in
       [
 
         testCaseSteps "deprecated default_solver is equivalent to solver.default" $
@@ -258,7 +264,7 @@ mkConfigTests adapters =
 
           step "Update the value via regular (text identification)"
           res2 <- try $ setUnicodeOpt settera $
-                  pack $ solver_adapter_name $ head adaptrs
+                  pack $ solver_adapter_name $ firstAdapter adaptrs
           case res2 of
             Right warns -> fmap show warns @?= []
             Left (SomeException e) -> assertFailure $ show e
@@ -283,7 +289,7 @@ mkConfigTests adapters =
 
           step "Reset to original value"
           res4 <- try $ setOpt settera' $
-                  pack $ solver_adapter_name $ head adaptrs
+                  pack $ solver_adapter_name $ firstAdapter adaptrs
           case res4 of
             Right warns -> fmap show warns @?= []
             Left (SomeException e) -> assertFailure $ show e

what4/test/ConfigTest.hs

@@ -471,10 +471,12 @@ testHelp =
     withChecklist "builtins" $ do
       cfg <- initialConfig 0 []
       help <- configHelp "" cfg
+      let nonEmptyOr :: (a -> b) -> b -> [a] -> b
+          nonEmptyOr f = foldr (\h _ -> f h)
       help `checkValues`
         (Empty
         :> Val "num" length 1
-        :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True
+        :> Val "verbosity" (nonEmptyOr (L.isInfixOf "verbosity =" . show) False) True
         )
 
 

what4/test/ProbeSolvers.hs

@@ -27,7 +27,9 @@ getSolverVersion (SolverName solver) =
       if r == ExitSuccess
       then let ol = lines o in
              return $ Right $ SolverVersion
-             $ if null ol then (solver <> " v??") else head ol
+             $ case ol of
+                 [] -> solver <> " v??"
+                 olh:_ -> olh
       else return $ Left $ solver <> " version error: " <> show r <> " /;/ " <> e
     Left (err :: SomeException) -> return $ Left $ solver <> " invocation error: " <> show err