diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml new file mode 100644 index 00000000..4d6015dc --- /dev/null +++ b/.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 diff --git a/.hlint.yaml b/.hlint.yaml index 9aca7096..db24bf8b 100644 --- a/.hlint.yaml +++ b/.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' diff --git a/what4/src/What4/Expr/App.hs b/what4/src/What4/Expr/App.hs index 7ec2a132..f4943f33 100644 --- a/what4/src/What4/Expr/App.hs +++ b/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 diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 3bc99057..bff5fadc 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/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) diff --git a/what4/src/What4/Expr/MATLAB.hs b/what4/src/What4/Expr/MATLAB.hs index 586462f2..50e55988 100644 --- a/what4/src/What4/Expr/MATLAB.hs +++ b/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 diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs index cbe41e46..9b3a5299 100644 --- a/what4/src/What4/Interface.hs +++ b/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) diff --git a/what4/test/ExprBuilderSMTLib2.hs b/what4/test/ExprBuilderSMTLib2.hs index c5e5f3ce..3c24496f 100644 --- a/what4/test/ExprBuilderSMTLib2.hs +++ b/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 diff --git a/what4/test/InvariantSynthesis.hs b/what4/test/InvariantSynthesis.hs index 3d6991a2..2b96c106 100644 --- a/what4/test/InvariantSynthesis.hs +++ b/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)