Bump What4 submodule, use new bitvector helpers, hlint

.github/workflows/lint.yml

@@ -0,0 +1,34 @@
+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)

.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-mir/src/Mir/Intrinsics.hs

@@ -1476,7 +1476,7 @@ arrayZeroedIO ::
     NatRepr w ->
     IO (RegValue sym (SymbolicArrayType (idxs ::> idx) (BaseBVType w)))
 arrayZeroedIO sym idxs w = do
-    zero <- bvLit sym w (BV.zero w)
+    zero <- bvZero sym w
     constantArray sym idxs zero
 
 mirVector_uninitIO ::
@@ -1679,15 +1679,15 @@ mirRef_offsetWrapLeaf bak _tpr (MirReference root (Index_RefPath tpr path idx))
     return $ MirReference root $ Index_RefPath tpr path idx'
 mirRef_offsetWrapLeaf bak _ ref@(MirReference _ _) offset = do
     let sym = backendGetSym bak
-    isZero <- liftIO $ bvEq sym offset =<< bvLit sym knownNat (BV.zero knownNat)
+    isZero <- liftIO $ bvEq sym offset =<< bvZero sym knownNat
     leafAssert bak isZero $ Unsupported callStack $
         "pointer arithmetic outside arrays is not yet implemented"
     return ref
 mirRef_offsetWrapLeaf bak _ ref@(MirReference_Integer _ _) offset = do
     let sym = backendGetSym bak
     -- Offsetting by zero is a no-op, and is always allowed, even on invalid
     -- pointers.  In particular, this permits `(&[])[0..]`.
-    isZero <- liftIO $ bvEq sym offset =<< bvLit sym knownNat (BV.zero knownNat)
+    isZero <- liftIO $ bvEq sym offset =<< bvZero sym knownNat
     leafAssert bak isZero $ Unsupported callStack $
         "cannot perform pointer arithmetic on invalid pointer"
     return ref
@@ -1710,7 +1710,7 @@ mirRef_tryOffsetFromLeaf sym (MirReference root1 path1) (MirReference root2 path
         _ -> do
             pathEq <- refPathEq sym path1 path2
             similar <- liftIO $ andPred sym rootEq pathEq
-            liftIO $ mkPE similar <$> bvLit sym knownNat (BV.zero knownNat)
+            liftIO $ mkPE similar <$> bvZero sym knownNat
 mirRef_tryOffsetFromLeaf _ _ _ = do
     -- MirReference_Integer pointers are always disjoint from all MirReference
     -- pointers, so we report them as being in different objects.

crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs

@@ -216,7 +216,7 @@ wasmLoadInt bak off w mem =
      p <- mkPtr sym off
      pval <- G.readMem sym knownNat Nothing p (bitvectorType bs) noAlignment (wasmMemHeap mem)
      Partial.assertSafe bak pval >>= \case
-       LLVMValZero _ -> bvLit sym w (BV.zero w)
+       LLVMValZero _ -> bvZero sym w
        LLVMValInt _ v | Just Refl <- testEquality (bvWidth v) w -> pure v
        _ -> panic "wasmLoadInt" ["type mismatch"]
 

crucible/src/Lang/Crucible/Simulator/Evaluation.hs

@@ -792,8 +792,8 @@ evalApp bak itefns _logFn evalExt (evalSub :: forall tp. f tp -> IO (RegValue sy
       bvSlt sym x y
     BoolToBV w xe -> do
       x <- evalSub xe
-      one <- bvLit sym w (BV.one w)
-      zro <- bvLit sym w (BV.zero w)
+      one <- bvOne sym w
+      zro <- bvZero sym w
       bvIte sym x one zro
     BVNonzero _ xe -> do
       x <- evalSub xe