Add bv{Zero,One} helpers, hlint config (#258)

Fixes #257. The HLint configuration only checks that these helpers are
used where appropriate. I used it to find places where they would be
useful. It may also serve as a template for downstream repos. I added
HLint checking to CI as well.

.github/workflows/lint.yml

@@ -0,0 +1,24 @@
+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 what4/
+          ../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'

what4/src/What4/Expr/App.hs

@@ -2114,7 +2114,7 @@ reduceApp sym unary a0 = do
         SR.SemiRingRealRepr ->
           maybe (realLit sym 1) return =<< WSum.prodEvalM (realMul sym) return pd
         SR.SemiRingBVRepr SR.BVArithRepr w ->
-          maybe (bvLit sym w (BV.one w)) return =<< WSum.prodEvalM (bvMul sym) return pd
+          maybe (bvOne sym w) return =<< WSum.prodEvalM (bvMul sym) return pd
         SR.SemiRingBVRepr SR.BVBitsRepr w ->
           maybe (bvLit sym w (BV.maxUnsigned w)) return =<< WSum.prodEvalM (bvAndBits sym) return pd
 
@@ -2136,7 +2136,7 @@ reduceApp sym unary a0 = do
 
     BVOrBits w bs ->
       case bvOrToList bs of
-        [] -> bvLit sym w (BV.zero w)
+        [] -> bvZero sym w
         (x:xs) -> foldM (bvOrBits sym) x xs
 
     BVTestBit i e -> testBitBV sym i e

what4/src/What4/Expr/Builder.hs

@@ -1340,7 +1340,7 @@ sbConcreteLookup sym arr0 mcidx idx
   , Ctx.Empty Ctx.:> idx0 <- idx
   , Ctx.Empty Ctx.:> update_idx0 <- update_idx = do
     diff <- bvSub sym idx0 update_idx0
-    is_diff_zero <- bvEq sym diff =<< bvLit sym (bvWidth diff) (BV.zero (bvWidth diff))
+    is_diff_zero <- bvEq sym diff =<< bvZero sym (bvWidth diff)
     case asConstantPred is_diff_zero of
       Just True -> return v
       Just False -> sbConcreteLookup sym arr mcidx idx
@@ -2647,7 +2647,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   bvFill sym w p
     | Just True  <- asConstantPred p = bvLit sym w (BV.maxUnsigned w)
-    | Just False <- asConstantPred p = bvLit sym w (BV.zero w)
+    | Just False <- asConstantPred p = bvZero sym w
     | otherwise = sbMakeExpr sym $ BVFill w p
 
   bvIte sym c x y
@@ -2781,7 +2781,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
    -- shift by more than word width returns 0
    | let (lo, _hi) = BVD.ubounds (exprAbsValue y)
    , lo >= intValue (bvWidth x)
-   = bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+   = bvZero sym (bvWidth x)
 
    | Just xv <- asBV x, Just n <- asBV y
    = bvLit sym (bvWidth x) (BV.shl (bvWidth x) xv (BV.asNatural n))
@@ -2797,7 +2797,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
    -- shift by more than word width returns 0
    | let (lo, _hi) = BVD.ubounds (exprAbsValue y)
    , lo >= intValue (bvWidth x)
-   = bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+   = bvZero sym (bvWidth x)
 
    | Just xv <- asBV x, Just n <- asBV y
    = bvLit sym (bvWidth x) $ BV.lshr (bvWidth x) xv (BV.asNatural n)
@@ -2957,7 +2957,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
       sbMakeExpr sym (BVSext w x)
 
   bvXorBits sym x y
-    | x == y = bvLit sym (bvWidth x) (BV.zero (bvWidth x))  -- special case: x `xor` x = 0
+    | x == y = bvZero sym (bvWidth x)  -- special case: x `xor` x = 0
     | otherwise
     = let sr = SR.SemiRingBVRepr SR.BVBitsRepr (bvWidth x)
        in semiRingAdd sym sr x y
@@ -3124,7 +3124,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
             ubv
     | otherwise = do
           let w = bvWidth x
-          zro <- bvLit sym w (BV.zero w)
+          zro <- bvZero sym w
           notPred sym =<< bvEq sym x zro
 
   bvUdiv = bvBinDivOp (const BV.uquot) BVUdiv
@@ -3455,7 +3455,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   predToBV sym p w
     | Just b <- asConstantPred p =
-        if b then bvLit sym w (BV.one w) else bvLit sym w (BV.zero w)
+        if b then bvOne sym w else bvZero sym w
     | otherwise =
        case testNatCases w (knownNat @1) of
          NatCaseEQ   -> sbMakeExpr sym (BVFill (knownNat @1) p)

what4/src/What4/Expr/MATLAB.hs

@@ -106,7 +106,7 @@ clampedIntMul :: (IsExprBuilder sym, 1 <= w)
 clampedIntMul sym x y = do
   let w = bvWidth x
   (hi,lo) <- signedWideMultiplyBV sym x y
-  zro    <- bvLit sym w (BV.zero w)
+  zro    <- bvZero sym w
   ones   <- maxUnsignedBV sym w
   ok_pos <- join $ andPred sym <$> (notPred sym =<< bvIsNeg sym lo)
                               <*> bvEq sym hi zro
@@ -178,7 +178,7 @@ clampedUIntSub sym x y = do
        sym
        no_underflow
        (bvSub sym x y) -- Perform subtraction if y >= x
-       (bvLit sym w (BV.zero w)) -- Otherwise return min int
+       (bvZero sym w) -- Otherwise return min int
 
 clampedUIntMul :: (IsExprBuilder sym, 1 <= w)
                => sym

what4/src/What4/Interface.hs

@@ -156,6 +156,10 @@ module What4.Interface
   , SymEncoder(..)
 
     -- * Utility combinators
+    -- ** Bitvector operations
+  , bvZero
+  , bvOne
+
     -- ** Boolean operations
   , backendPred
   , andAllOf
@@ -945,7 +949,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
 
   -- | Return true if bitvector is negative.
   bvIsNeg :: (1 <= w) => sym -> SymBV sym w -> IO (Pred sym)
-  bvIsNeg sym x = bvSlt sym x =<< bvLit sym (bvWidth x) (BV.zero (bvWidth x))
+  bvIsNeg sym x = bvSlt sym x =<< bvZero sym (bvWidth x)
 
   -- | If-then-else applied to bitvectors.
   bvIte :: (1 <= w)
@@ -1693,7 +1697,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
       -- Handle case where i < 0
       min_sym <- intLit sym 0
       is_lt <- intLt sym i min_sym
-      iteM bvIte sym is_lt (bvLit sym w (BV.zero w)) $ do
+      iteM bvIte sym is_lt (bvZero sym w) $ do
         -- Handle case where i > maxUnsigned w
         let max_val = maxUnsigned w
             max_val_bv = BV.maxUnsigned w
@@ -1743,7 +1747,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
   intToUInt :: (1 <= m, 1 <= n) => sym -> SymBV sym m -> NatRepr n -> IO (SymBV sym n)
   intToUInt sym e w = do
     p <- bvIsNeg sym e
-    iteM bvIte sym p (bvLit sym w (BV.zero w)) (uintSetWidth sym e w)
+    iteM bvIte sym p (bvZero sym w) (uintSetWidth sym e w)
 
   -- | Convert an unsigned bitvector to the nearest signed bitvector with
   -- the given width (clamp on overflow).
@@ -3027,7 +3031,7 @@ baseDefaultValue sym bt =
   case bt of
     BaseBoolRepr    -> return $! falsePred sym
     BaseIntegerRepr -> intLit sym 0
-    BaseBVRepr w    -> bvLit sym w (BV.zero w)
+    BaseBVRepr w    -> bvZero sym w
     BaseRealRepr    -> return $! realZero sym
     BaseFloatRepr fpp -> floatPZero sym fpp
     BaseComplexRepr -> mkComplexLit sym (0 :+ 0)
@@ -3294,3 +3298,17 @@ data Statistics
 zeroStatistics :: Statistics
 zeroStatistics = Statistics { statAllocs = 0
                             , statNonLinearOps = 0 }
+
+----------------------------------------------------------------------
+-- Bitvector utilities
+
+-- | An alias for 'minUnsignedBv'.
+--
+-- Useful in contexts where you want to convey the zero-ness of the value more
+-- than its minimality.
+bvZero :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
+bvZero = minUnsignedBV
+
+-- | A bitvector that is all zeroes except the LSB, which is one.
+bvOne :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
+bvOne sym w = bvLit sym w (BV.one w)

what4/test/ExprBuilderSMTLib2.hs

@@ -1068,7 +1068,7 @@ issue182Test sym solver = do
     let idx = Ctx.Empty Ctx.:> idxInt
     let arrLookup = arrayLookup sym arr idx
     elt <- arrLookup
-    bvZero <- bvLit sym w (BV.zero w)
+    bvZero <- bvZero sym w
     p <- bvEq sym elt bvZero
 
     checkSatisfiableWithModel solver "test" p $ \case
@@ -1133,7 +1133,7 @@ testUnsafeSetAbstractValue1 = testCase "test unsafeSetAbstractValue1" $
     e1A <- freshConstant sym (userSymbol' "x1") (BaseBVRepr w)
     let e1A' = unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e1A
     unsignedBVBounds e1A' @?= Just (2, 2)
-    e1B <- bvAdd sym e1A' =<< bvLit sym w (BV.one w)
+    e1B <- bvAdd sym e1A' =<< bvOne sym w
     case asBV e1B of
       Just bv -> bv @?= BV.mkBV w 3
       Nothing -> assertFailure $ unlines
@@ -1151,7 +1151,7 @@ testUnsafeSetAbstractValue2 = testCase "test unsafeSetAbstractValue2" $
     e2C <- bvAdd sym e2A e2B
     (_, e2C') <- annotateTerm sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C
     unsignedBVBounds e2C' @?= Just (2, 2)
-    e2D <- bvAdd sym e2C' =<< bvLit sym w (BV.one w)
+    e2D <- bvAdd sym e2C' =<< bvOne sym w
     case asBV e2D of
       Just bv -> bv @?= BV.mkBV w 3
       Nothing -> assertFailure $ unlines

what4/test/InvariantSynthesis.hs

@@ -75,8 +75,8 @@ bvProblem sym = do
   inv <- freshTotalUninterpFn sym (safeSymbol "inv") knownRepr knownRepr
   i <- freshConstant sym (safeSymbol "i") $ BaseBVRepr $ knownNat @64
   n <- freshConstant sym (safeSymbol "n") knownRepr
-  zero <- bvLit sym knownNat $ BV.zero knownNat
-  one <- bvLit sym knownNat $ BV.one knownNat
+  zero <- bvZero sym knownNat
+  one <- bvOne sym knownNat
   ult_1_n <- bvUlt sym one n
   inv_0_n <- applySymFn sym inv $ Empty :> zero :> n
   -- 1 < n ==> inv(0, n)