Bump What4 submodule, use new bitvector helpers, hlint

.github/workflows/lint.yml

@@ -0,0 +1,36 @@
+name: lint
+on:
+  push:
+    branches: [master, "release-**"]
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  lint:
+    runs-on: ubuntu-22.04
+    name: lint
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: false
+
+      - shell: bash
+        run: |
+          curl --location -o hlint.tar.gz \
+            https://github.com/ndmitchell/hlint/releases/download/v3.8/hlint-3.8-x86_64-linux.tar.gz
+          tar xvf hlint.tar.gz
+
+          (cd crucible/; ../hlint-3.8/hlint src test)
+          (cd crucible-cli/; ../hlint-3.8/hlint src test)
+          (cd crucible-concurrency/; ../hlint-3.8/hlint src test)
+          (cd crucible-go/; ../hlint-3.8/hlint src tests)
+          (cd crucible-jvm/; ../hlint-3.8/hlint src tests)
+          (cd crucible-llvm-cli/; ../hlint-3.8/hlint src test)
+          (cd crucible-llvm-syntax/; ../hlint-3.8/hlint src test)
+          (cd crucible-mir/; ../hlint-3.8/hlint src)
+          (cd crucible-saw/; ../hlint-3.8/hlint src)
+          (cd crucible-symio/; ../hlint-3.8/hlint src tests)
+          (cd crucible-syntax/; ../hlint-3.8/hlint src test)
+          (cd crucible-wasm/; ../hlint-3.8/hlint src test)
+          (cd crux-llvm/; ../hlint-3.8/hlint src test)
+          (cd crux-mir/; ../hlint-3.8/hlint src test)

.hlint.yaml

@@ -1,75 +1,14 @@
-# HLint configuration file
-# https://github.com/ndmitchell/hlint
-##########################
+# HLint's default suggestions are opinionated, so we disable all of them by
+# default and enable just a small subset we can agree on.
 
-- modules:
-  - {name: [Data.Set, Data.HashSet], as: Set} # if you import Data.Set qualified, it must be as 'Set'
-  - {name: [Data.List], as: List}
-  - {name: [Data.Sequence], as: Seq}
+- ignore: {}  # ignore all
 
-# Add custom hints for this project
-#
-# Will suggest replacing "wibbleMany [myvar]" with "wibbleOne myvar"
-# - error: {lhs: "wibbleMany [x]", rhs: wibbleOne x}
+- error:
+    name: Use bvZero
+    lhs: "What4.Interface.bvLit sym w (Data.BitVector.Sized.zero w)"
+    rhs: 'What4.Interface.bvZero sym w'
 
-# We should use "panic", not "error".
-# - error:
-#     lhs: "error x"
-#     rhs: 'panic "nameOfFunction" [x, "more lines of details"]'
-
-# TODO: specialize these to the modules they are needed
-- ignore: {name: 'Use :'}
-- ignore: {name: Avoid lambda using `infix`}
-- ignore: {name: Avoid lambda}
-- ignore: {name: Avoid restricted qualification}
-- ignore: {name: Eta reduce}
-- ignore: {name: Functor law}
-- ignore: {name: Move brackets to avoid $}
-- ignore: {name: Parse error}
-- ignore: {name: Reduce duplication}
-- ignore: {name: Redundant $}
-- ignore: {name: Redundant ==}
-- ignore: {name: Redundant bracket}
-- ignore: {name: Redundant case}
-- ignore: {name: Redundant do}
-- ignore: {name: Redundant flip}
-- ignore: {name: Redundant guard}
-- ignore: {name: Redundant lambda}
-- ignore: {name: Redundant return}
-- ignore: {name: Unused LANGUAGE pragma}
-- ignore: {name: Use $>}
-- ignore: {name: Use &&}
-- ignore: {name: Use ++}
-- ignore: {name: Use .}
-- ignore: {name: Use <$>}
-- ignore: {name: Use <=<}
-- ignore: {name: Use =<<}
-- ignore: {name: Use ==}
-- ignore: {name: Use >=>}
-- ignore: {name: Use String}
-- ignore: {name: Use asks}
-- ignore: {name: Use camelCase}
-- ignore: {name: Use const}
-- ignore: {name: Use fewer imports}
-- ignore: {name: Use fmap}
-- ignore: {name: Use forM_}
-- ignore: {name: Use fromMaybe, within: [Lang.Crucible.Analysis.Shape, Lang.Crucible.JVM.Class, Lang.Crucible.JVM.Translation.Class]}
-- ignore: {name: Use record patterns, within: [Lang.Crucible.Simulator.EvalStmt, Lang.Crucible.Simulator.Profiling, Lang.Crucible.CFG.Core]}
-- ignore: {name: Use guards}
-- ignore: {name: Use hPrint}
-- ignore: {name: Use if}
-- ignore: {name: Use isNothing}
-- ignore: {name: Use lambda-case}
-- ignore: {name: Use list comprehension}
-- ignore: {name: Use maybe}
-- ignore: {name: Use newtype instead of data}
-- ignore: {name: Use record patterns}
-- ignore: {name: Use otherwise}
-- ignore: {name: Use section}
-- ignore: {name: Use sortOn}
-- ignore: {name: Use tuple-section}
-- ignore: {name: Use uncurry}
-- ignore: {name: Use unless}
-- ignore: {name: Use unwords}
-- ignore: {name: Use void}
-- ignore: {name: Use when}
+- error:
+    name: Use bvOne
+    lhs: "What4.Interface.bvLit sym w (Data.BitVector.Sized.one w)"
+    rhs: 'What4.Interface.bvOne sym w'

crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs

@@ -699,7 +699,7 @@ isArray_override =
                       let sym = backendGetSym bak
                       let reg :: W4.PartExpr (W4.Pred sym) (C.MuxTree sym (RefCell JVMObjectType))
                           reg = C.unRV (Ctx.last args)
-                      bvFalse <- liftIO $ return $ W4.bvLit sym knownRepr (BV.zero knownRepr)
+                      bvFalse <- liftIO $ return $ W4.bvZero sym knownRepr
 {-
                       let k :: RefCell JVMObjectType -> IO (W4.SymBV sym 32)
                           k = undefined

crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs

@@ -505,15 +505,15 @@ zeroValue :: IsSymInterface sym => sym -> J.Type -> IO (C.RegValue sym JVMValueT
 zeroValue sym ty =
   case ty of
     J.ArrayType _ -> C.injectVariant sym knownRepr tagR <$> return W4.Unassigned
-    J.BooleanType -> C.injectVariant sym knownRepr tagI <$> W4.bvLit sym w32 (BV.zero w32)
-    J.ByteType    -> C.injectVariant sym knownRepr tagI <$> W4.bvLit sym w32 (BV.zero w32)
-    J.CharType    -> C.injectVariant sym knownRepr tagI <$> W4.bvLit sym w32 (BV.zero w32)
+    J.BooleanType -> C.injectVariant sym knownRepr tagI <$> W4.bvZero sym w32
+    J.ByteType    -> C.injectVariant sym knownRepr tagI <$> W4.bvZero sym w32
+    J.CharType    -> C.injectVariant sym knownRepr tagI <$> W4.bvZero sym w32
     J.ClassType _ -> C.injectVariant sym knownRepr tagR <$> return W4.Unassigned
     J.DoubleType  -> C.injectVariant sym knownRepr tagD <$> W4.iFloatPZero sym DoubleFloatRepr
     J.FloatType   -> C.injectVariant sym knownRepr tagF <$> W4.iFloatPZero sym SingleFloatRepr
-    J.IntType     -> C.injectVariant sym knownRepr tagI <$> W4.bvLit sym w32 (BV.zero w32)
-    J.LongType    -> C.injectVariant sym knownRepr tagL <$> W4.bvLit sym w64 (BV.zero w64)
-    J.ShortType   -> C.injectVariant sym knownRepr tagI <$> W4.bvLit sym w32 (BV.zero w32)
+    J.IntType     -> C.injectVariant sym knownRepr tagI <$> W4.bvZero sym w32
+    J.LongType    -> C.injectVariant sym knownRepr tagL <$> W4.bvZero sym w64
+    J.ShortType   -> C.injectVariant sym knownRepr tagI <$> W4.bvZero sym w32
 
 -- (currently unused)
 -- Way to run initialization code before simulation starts

crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs

@@ -259,7 +259,7 @@ registerFunPtr ::
   IO (LLVMPtr sym wptr, MemImpl sym)
 registerFunPtr bak mem displayName nm aliases = do
   let sym = backendGetSym bak
-  z <- bvLit sym ?ptrWidth (BV.zero ?ptrWidth)
+  z <- bvZero sym ?ptrWidth
   (ptr, mem') <- doMalloc bak G.GlobalAlloc G.Immutable displayName mem z noAlignment
   return $ (ptr, registerGlobal mem' (nm:aliases) ptr)
 

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

@@ -1396,7 +1396,7 @@ callObjectsize _mvar w
       -- through compilation for us to see, that means the compiler could not
       -- determine the value.
       t <- bvIsNonzero sym flag
-      z <- bvLit sym w (BV.zero w)
+      z <- bvZero sym w
       n <- bvNotBits sym z -- NB: -1 is the boolean negation of zero
       bvIte sym t z n
 
@@ -1716,16 +1716,16 @@ callIsFpclass ::
 callIsFpclass regOp@(regValue -> op) (regValue -> test) = do
   sym <- getSymInterface
   let w1 = knownNat @1
-  bvOne  <- liftIO $ bvLit sym w1 (BV.one w1)
-  bvZero <- liftIO $ bvLit sym w1 (BV.zero w1)
+  bv1 <- liftIO $ bvZero sym w1
+  bv0 <- liftIO $ bvOne sym w1
 
   let negative bit = liftIO $ do
         isNeg <- iFloatIsNeg @_ @fi sym op
-        liftIO $ bvIte sym isNeg bit bvZero
+        liftIO $ bvIte sym isNeg bit bv0
 
   let positive bit = liftIO $ do
         isPos <- iFloatIsPos @_ @fi sym op
-        liftIO $ bvIte sym isPos bit bvZero
+        liftIO $ bvIte sym isPos bit bv0
 
   let negAndPos doCheck = liftIO $ do
         check <- doCheck
@@ -1735,19 +1735,19 @@ callIsFpclass regOp@(regValue -> op) (regValue -> test) = do
 
   let callIsInf x = do
         isInf <- iFloatIsInf @_ @fi sym x
-        bvIte sym isInf bvOne bvZero
+        bvIte sym isInf bv1 bv0
 
   let callIsNormal x = do
         isNorm <- iFloatIsNorm @_ @fi sym x
-        bvIte sym isNorm bvOne bvZero
+        bvIte sym isNorm bv1 bv0
 
   let callIsSubnormal x = do
         isSubnorm <- iFloatIsSubnorm @_ @fi sym x
-        bvIte sym isSubnorm bvOne bvZero
+        bvIte sym isSubnorm bv1 bv0
 
   let callIsZero x = do
         is0 <- iFloatIsZero @_ @fi sym x
-        bvIte sym is0 bvOne bvZero
+        bvIte sym is0 bv1 bv0
 
   isNan <- Libc.callIsnan w1 regOp
   (isInfN, isInfP) <- negAndPos $ callIsInf op
@@ -1758,9 +1758,9 @@ callIsFpclass regOp@(regValue -> op) (regValue -> test) = do
   foldM
     (\bits (bitNum, check) -> liftIO $ do
         isBitSet <- liftIO $ testBitBV sym bitNum test
-        newBit <- liftIO $ bvIte sym isBitSet check bvZero
+        newBit <- liftIO $ bvIte sym isBitSet check bv0
         liftIO $ bvOrBits sym newBit bits)
-    bvZero
+    bv0
     [ (0, isNan)      -- Signaling NaN
     , (1, isNan)      -- Quiet NaN
     , (2, isInfN)     -- Negative infinity

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

@@ -192,7 +192,7 @@ llvmMemcpyOverride =
   [llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]
   (\memOps args ->
        do sym <- getSymInterface
-          volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)
+          volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat
           Ctx.uncurryAssignment (callMemcpy memOps)
                                 (args :> volatile)
           return $ regValue $ args^._1 -- return first argument
@@ -213,7 +213,7 @@ llvmMemcpyChkOverride =
   (\memOps args ->
       do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3)
          sym <- getSymInterface
-         volatile <- liftIO $ RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat)
+         volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat
          Ctx.uncurryAssignment (callMemcpy memOps)
                                (args' :> volatile)
          return $ regValue $ args^._1 -- return first argument
@@ -231,7 +231,7 @@ llvmMemmoveOverride =
   [llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]
   (\memOps args ->
       do sym <- getSymInterface
-         volatile <- liftIO (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat))
+         volatile <- liftIO (RegEntry knownRepr <$> bvZero sym knownNat)
          Ctx.uncurryAssignment (callMemmove memOps)
                                (args :> volatile)
          return $ regValue $ args^._1 -- return first argument
@@ -253,7 +253,7 @@ llvmMemsetOverride =
          val <- liftIO (RegEntry knownRepr <$> bvTrunc sym (knownNat @8) (regValue (args^._2)))
          let len = args^._3
          volatile <- liftIO
-            (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat))
+            (RegEntry knownRepr <$> bvZero sym knownNat)
          callMemset memOps dest val len volatile
          return (regValue dest)
     )
@@ -275,7 +275,7 @@ llvmMemsetChkOverride =
               (RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2)))
          let len = args^._3
          volatile <- liftIO
-            (RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat))
+            (RegEntry knownRepr <$> bvZero sym knownNat)
          callMemset memOps dest val len volatile
          return (regValue dest)
     )
@@ -462,7 +462,7 @@ callPosixMemalign mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz)
                   let displayString = "<posix_memaign> " ++ show loc
                   (p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a
                   mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p)
-                  z <- bvLit sym knownNat (BV.zero knownNat)
+                  z <- bvZero sym knownNat
                   return (z, mem'')
 
 callMalloc
@@ -647,7 +647,7 @@ callExit ec =
   ovrWithBackend $ \bak -> liftIO $ do
     let sym = backendGetSym bak
     when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
-      do cond <- bvEq sym (regValue ec) =<< bvLit sym knownNat (BV.zero knownNat)
+      do cond <- bvEq sym (regValue ec) =<< bvZero sym knownNat
          -- If the argument is non-zero, throw an assertion failure. Otherwise,
          -- simply stop the current thread of execution.
          assert bak cond "Call to exit() with non-zero argument"
@@ -1036,11 +1036,11 @@ callIsinf w (regValue -> x) = do
     isPos <- iFloatIsPos @_ @fi sym x
     isInfN <- andPred sym isInf isNeg
     isInfP <- andPred sym isInf isPos
-    bvOne    <- bvLit sym w (BV.one w)
-    bvNegOne <- bvNeg sym bvOne
-    bvZero   <- bvLit sym w (BV.zero w)
-    res0 <- bvIte sym isInfP bvOne bvZero
-    bvIte sym isInfN bvNegOne res0
+    bv1 <- bvOne sym w
+    bvNeg1 <- bvNeg sym bv1
+    bv0 <- bvZero sym w
+    res0 <- bvIte sym isInfP bv1 bv0
+    bvIte sym isInfN bvNeg1 res0
 
 callIsnan ::
   forall fi w p sym ext r args ret.
@@ -1052,11 +1052,11 @@ callIsnan w (regValue -> x) = do
   sym <- getSymInterface
   liftIO $ do
     isnan  <- iFloatIsNaN @_ @fi sym x
-    bvOne  <- bvLit sym w (BV.one w)
-    bvZero <- bvLit sym w (BV.zero w)
+    bv1 <- bvOne sym w
+    bv0 <- bvZero sym w
     -- isnan() is allowed to return any nonzero value if the argument is NaN, and
     -- out of all the possible nonzero values, `1` is certainly one of them.
-    bvIte sym isnan bvOne bvZero
+    bvIte sym isnan bv1 bv0
 
 callSqrt ::
   forall fi p sym ext r args ret.
@@ -1831,7 +1831,7 @@ cxa_atexitOverride =
   [llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |]
   (\_ _args -> do
     sym <- getSymInterface
-    liftIO $ bvLit sym knownNat (BV.zero knownNat))
+    liftIO $ bvZero sym knownNat)
 
 ----------------------------------------------------------------------------