From c079d5bf5e362935a59be6fb3967ecb013535a80 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Sun, 24 May 2020 23:02:56 -0700 Subject: [PATCH] update to bv-sized branch of what4 and other things --- .gitmodules | 3 --- base/macaw-base.cabal | 2 +- deps/asl-translator | 2 +- deps/crucible | 2 +- deps/dismantle | 2 +- deps/semmc | 2 +- deps/what4 | 2 +- deps/what4-serialize | 2 +- .../Macaw/ARM/Semantics/ThumbSemantics.hs | 11 -------- macaw-ppc/macaw-ppc.cabal | 1 + .../src/Data/Macaw/PPC/Semantics/Base.hs | 7 ++--- macaw-semmc/macaw-semmc.cabal | 1 + macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 13 ++++----- refinement/macaw-refinement.cabal | 1 + .../Macaw/Refinement/SymbolicExecution.hs | 19 ++++++------- symbolic/macaw-symbolic.cabal | 3 ++- symbolic/src/Data/Macaw/Symbolic.hs | 5 ++-- symbolic/src/Data/Macaw/Symbolic/Bitcast.hs | 5 ++-- symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 16 +++++------ symbolic/src/Data/Macaw/Symbolic/MemOps.hs | 8 +++--- .../src/Data/Macaw/Symbolic/MemTraceOps.hs | 7 ++--- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 27 +++++++++++-------- x86_symbolic/macaw-x86-symbolic.cabal | 1 + x86_symbolic/src/Data/Macaw/X86/Crucible.hs | 9 ++++--- 24 files changed, 78 insertions(+), 73 deletions(-) diff --git a/.gitmodules b/.gitmodules index b4886313..ece6c2a2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,9 +7,6 @@ [submodule "x86/tests/submodules/flexdis86"] path = deps/flexdis86 url = https://github.com/GaloisInc/flexdis86.git -[submodule "x86/tests/submodules/parameterized-utils"] - path = deps/parameterized-utils - url = https://github.com/GaloisInc/parameterized-utils.git [submodule "deps/crucible"] path = deps/crucible url = https://github.com/GaloisInc/crucible.git diff --git a/base/macaw-base.cabal b/base/macaw-base.cabal index 8dbeaf3a..1d6bf99f 100644 --- a/base/macaw-base.cabal +++ b/base/macaw-base.cabal @@ -39,7 +39,7 @@ library IntervalMap >= 0.5, lens >= 4.7, mtl, - parameterized-utils >= 2.0.0.0.104, + parameterized-utils >= 2.1.0 && < 2.2, template-haskell, text, vector, diff --git a/deps/asl-translator b/deps/asl-translator index 0c0f7ac3..01ed3683 160000 --- a/deps/asl-translator +++ b/deps/asl-translator @@ -1 +1 @@ -Subproject commit 0c0f7ac37d4a72f59ac08b8281a23997b8f685b0 +Subproject commit 01ed3683c76a3472f36912aaaa82f7631d0c5fd4 diff --git a/deps/crucible b/deps/crucible index aca70a9b..a9ff2089 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit aca70a9b30a823579883e5b9ea1f81391b3e59fb +Subproject commit a9ff2089ac2e8f884dad05c8f5cecccb5ad148e8 diff --git a/deps/dismantle b/deps/dismantle index 6c66dfaa..21c5d44d 160000 --- a/deps/dismantle +++ b/deps/dismantle @@ -1 +1 @@ -Subproject commit 6c66dfaa131255383bd4cade0556beda00d57e90 +Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9 diff --git a/deps/semmc b/deps/semmc index 67d66fbe..86f036b2 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 67d66fbebd91db5aa773a0c4ff8e61be2382445c +Subproject commit 86f036b23a6ad91e5d92b590d16e0412a44318a5 diff --git a/deps/what4 b/deps/what4 index 3a12e48f..a8bdd561 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 3a12e48f9e066ce99d7c29c16f067235abbfec31 +Subproject commit a8bdd561354d54fbbb8703cebe66e74a871acb8e diff --git a/deps/what4-serialize b/deps/what4-serialize index f6177603..c1e40e5d 160000 --- a/deps/what4-serialize +++ b/deps/what4-serialize @@ -1 +1 @@ -Subproject commit f6177603aff8f3fa663aece2f0b35046e9c4202d +Subproject commit c1e40e5d147eba202c08b3980139bda616f6af08 diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs index 345d30c3..294a00ad 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs @@ -29,14 +29,3 @@ execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32) -> Instruction -> Maybe (Generator ARMSem.AArch32 ids s ()) execInstruction = \_ _ -> Nothing - -- $(genExecInstruction (Proxy @ARMSem.AArch32) - -- (locToRegTH (Proxy @ARMSem.AArch32)) - -- armNonceAppEval - -- (armAppEvaluator MC.LittleEndian) - -- 't32InstructionMatcher - -- allT32Semantics - -- allT32OpcodeInfo - -- allDefinedFunctions - -- ([t| Operand |], [t| ARMSem.AArch32 |]) - -- MC.LittleEndian - -- ) diff --git a/macaw-ppc/macaw-ppc.cabal b/macaw-ppc/macaw-ppc.cabal index b7ae3746..ba01c95c 100644 --- a/macaw-ppc/macaw-ppc.cabal +++ b/macaw-ppc/macaw-ppc.cabal @@ -28,6 +28,7 @@ library Data.Macaw.PPC.Semantics.PPC32 Data.Macaw.PPC.Semantics.TH build-depends: base >=4.9 && <5, + bv-sized >= 1.0.0 && < 1.1, bytestring, containers, constraints, diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs index 8f4d823b..51b725f6 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs @@ -24,6 +24,7 @@ import qualified Data.Foldable as F import Data.Proxy import GHC.TypeLits +import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes import qualified What4.BaseTypes as S import qualified What4.Expr.BoolMap as BooM @@ -121,14 +122,14 @@ crucAppToExpr (S.SemiRingSum sm) = let smul mul e = do x <- sval mul y <- eltToExpr e AppExpr <$> do M.BVMul w <$> addExpr x <*> addExpr y - sval v = return $ ValueExpr $ M.BVValue w v + sval v = return $ ValueExpr $ M.BVValue w (BV.asUnsigned v) add x y = AppExpr <$> do M.BVAdd w <$> addExpr x <*> addExpr y in WSum.evalM add smul sval sm SR.SemiRingBVRepr SR.BVBitsRepr w -> let smul mul e = do x <- sval mul y <- eltToExpr e AppExpr <$> do M.BVAnd w <$> addExpr x <*> addExpr y - sval v = return $ ValueExpr $ M.BVValue w v + sval v = return $ ValueExpr $ M.BVValue w (BV.asUnsigned v) add x y = AppExpr <$> do M.BVXor w <$> addExpr x <*> addExpr y in WSum.evalM add smul sval sm _ -> error "unsupported SemiRingSum repr for macaw PPC base semantics" @@ -228,7 +229,7 @@ eltToExpr :: (M.ArchConstraints (SP.AnyPPC var), MSS.SimplifierExtension (SP.Any -> Generator (SP.AnyPPC var) ids s (Expr (SP.AnyPPC var) ids (FromCrucibleBaseType ctp)) eltToExpr (S.AppExpr appElt) = crucAppToExpr (S.appExprApp appElt) eltToExpr (S.SemiRingLiteral (SR.SemiRingBVRepr _ w) val _) = - return $ ValueExpr (M.BVValue w val) + return $ ValueExpr (M.BVValue w (BV.asUnsigned val)) eltToExpr _ = error "Unexpected expr type in eltToExpr" -- Add a Crucible element in the Generator monad. diff --git a/macaw-semmc/macaw-semmc.cabal b/macaw-semmc/macaw-semmc.cabal index a1bceae4..0049e2dd 100644 --- a/macaw-semmc/macaw-semmc.cabal +++ b/macaw-semmc/macaw-semmc.cabal @@ -38,6 +38,7 @@ library dismantle-tablegen, ansi-wl-pprint, semmc, + bv-sized, what4 hs-source-dirs: src default-language: Haskell2010 diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs index 08407995..8f20ca70 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs @@ -56,6 +56,7 @@ import Language.Haskell.TH import Language.Haskell.TH.Syntax import Text.Read ( readMaybe ) +import qualified Data.BitVector.Sized as BVS import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.HasRepr as HR @@ -711,7 +712,7 @@ addEltTH endianness interps elt = do bindExpr elt (return translatedExpr) S.SemiRingLiteral srTy val _ | (SR.SemiRingBVRepr _ w) <- srTy -> - bindExpr elt [| genBVValue $(natReprTH w) $(lift val) |] + bindExpr elt [| genBVValue $(natReprTH w) $(lift (BVS.asUnsigned val)) |] | otherwise -> liftQ [| error "SemiRingLiteral Elts are not supported" |] S.StringExpr {} -> liftQ [| error "StringExpr elts are not supported" |] S.BoolExpr b _loc -> bindExpr elt [| return (M.BoolValue $(lift b)) |] @@ -962,7 +963,7 @@ defaultAppEvaluator endianness elt interps = case elt of S.BVTestBit idx bv -> do bvValExp <- addEltTH endianness interps bv liftQ [| G.AppExpr <$> (M.BVTestBit <$> - G.addExpr (G.ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx))) <*> + G.addExpr (G.ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift (toInteger idx)))) <*> pure $(return bvValExp)) |] S.SemiRingSum sm -> @@ -972,10 +973,10 @@ defaultAppEvaluator endianness elt interps = case elt of liftQ [| return (G.AppExpr (M.BVMul $(natReprTH w) - (M.BVValue $(natReprTH w) $(lift mul)) + (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) $(return y))) |] - sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift v))) |] + sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)))) |] add x y = liftQ [| G.AppExpr <$> (M.BVAdd $(natReprTH w) <$> (G.addExpr =<< $(return x)) <*> (G.addExpr =<< $(return y))) @@ -986,10 +987,10 @@ defaultAppEvaluator endianness elt interps = case elt of liftQ [| return (G.AppExpr (M.BVAnd $(natReprTH w) - (M.BVValue $(natReprTH w) $(lift mul)) + (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) $(return y))) |] - sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift v))) |] + sval v = liftQ [| return (G.ValueExpr (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)))) |] add x y = liftQ [| G.AppExpr <$> (M.BVXor $(natReprTH w) <$> (G.addExpr =<< $(return x)) <*> (G.addExpr =<< $(return y))) diff --git a/refinement/macaw-refinement.cabal b/refinement/macaw-refinement.cabal index 40b300e0..74448ea4 100644 --- a/refinement/macaw-refinement.cabal +++ b/refinement/macaw-refinement.cabal @@ -48,6 +48,7 @@ source-repository head library build-depends: base >= 4 , ansi-wl-pprint + , bv-sized >= 1.0.0 , containers , crucible >= 0.4 , crucible-llvm diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs index 22313774..ee473693 100644 --- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs +++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs @@ -28,6 +28,7 @@ import Control.Lens ( (^.) ) import qualified Control.Monad.Catch as X import Control.Monad.IO.Class ( MonadIO, liftIO ) import qualified Control.Monad.IO.Unlift as MU +import qualified Data.BitVector.Sized as BV import qualified Data.Foldable as F import Data.IORef import qualified Data.Macaw.BinaryLoader as MBL @@ -278,7 +279,7 @@ initialRegisterState sym archVals globalMappingFn memory entryBlock spVal = do -- Build an IP value to populate the initial register state with let entryAddr = M.segoffAddr (M.pblockAddr entryBlock) ip_base <- liftIO $ W.natLit sym (fromIntegral (M.addrBase entryAddr)) - ip_off <- liftIO $ W.bvLit sym W.knownNat (M.memWordToUnsigned (M.addrOffset entryAddr)) + ip_off <- liftIO $ W.bvLit sym W.knownNat (BV.mkBV W.knownNat $ M.memWordToUnsigned (M.addrOffset entryAddr)) entryIPVal <- liftIO $ globalMappingFn sym memory ip_base ip_off -- liftIO $ printf "Entry initial state" @@ -325,7 +326,7 @@ addKnownRegValue sym archVals globalMappingFn memory regsStruct reg val = Just Refl -> do -- This is a value with the same width as a pointer. We attempt -- to translate it into a pointer using the global map if possible - off <- liftIO $ W.bvLit sym ptrWidthRepr singleBV + off <- liftIO $ W.bvLit sym ptrWidthRepr (BV.mkBV ptrWidthRepr singleBV) ptr <- liftIO $ globalMappingFn sym memory base off return (MS.updateReg archVals regsStruct reg ptr) Nothing -> @@ -333,7 +334,7 @@ addKnownRegValue sym archVals globalMappingFn memory regsStruct reg val = LLVM.LLVMPointerRepr nr -> do -- Otherwise, this is just a bitvector of a non-pointer size, -- so we just make it into a plain bitvector. - bvVal <- liftIO $ W.bvLit sym nr singleBV + bvVal <- liftIO $ W.bvLit sym nr (BV.mkBV nr singleBV) let ptr = LLVM.LLVMPointer base bvVal return (MS.updateReg archVals regsStruct reg ptr) _ -> return regsStruct @@ -377,8 +378,8 @@ genIPConstraint ctx sym ipVal = liftIO $ do genSegConstraint repr seg = do let low = MM.segmentOffset seg let high = low + MM.segmentSize seg - lo <- W.bvLit sym repr (fromIntegral low) - hi <- W.bvLit sym repr (fromIntegral high) + lo <- W.bvLit sym repr (BV.mkBV repr (toInteger low)) + hi <- W.bvLit sym repr (BV.mkBV repr (toInteger high)) lb <- W.bvUle sym lo ipVal ub <- W.bvUle sym ipVal hi W.andPred sym lb ub @@ -408,7 +409,7 @@ genModels proxy sym solver_proc assumptions expr count next_ground_val <- liftIO $ W.groundEval evalFn expr next_bv_val <- liftIO $ W.bvLit sym W.knownNat next_ground_val not_current_ground_val <- liftIO $ W.bvNe sym expr next_bv_val - LJ.writeLogM (RL.GeneratedModel @arch next_ground_val) + LJ.writeLogM (RL.GeneratedModel @arch (BV.asUnsigned next_ground_val)) more_ground_vals <- genModels proxy sym solver_proc (not_current_ground_val : assumptions) expr (count - 1) return $ next_ground_val : more_ground_vals _ -> return [] @@ -455,7 +456,7 @@ extractIPModels ctx sym solverProc initialAssumptions res_ip_base res_ip_off = d let resolveAddr off = M.resolveAbsoluteAddr (binaryMemory ctx) $ M.memWord $ fromIntegral $ M.memWordToUnsigned ip_base_mem_word + off - let resolved = mapMaybe resolveAddr ip_off_ground_vals + let resolved = mapMaybe resolveAddr (BV.asUnsigned <$> ip_off_ground_vals) unlift $ LJ.writeLogM (RL.ResolvedAddresses @arch resolved) case length resolved of 0 -> return NoModels @@ -517,8 +518,8 @@ initializeMemory _ sym mem = do let ?ptrWidth = W.knownNat let stackBytes = 2 * 1024 * 1024 stackArray <- liftIO $ W.freshConstant sym (W.safeSymbol "stack") C.knownRepr - stackSize <- liftIO $ W.bvLit sym ?ptrWidth stackBytes - stackSizex2 <- liftIO $ W.bvLit sym ?ptrWidth (2 * stackBytes) + stackSize <- liftIO $ W.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth stackBytes) + stackSizex2 <- liftIO $ W.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (2 * stackBytes)) (stackBasePtr, mem1) <- liftIO $ LLVM.doMalloc sym LLVM.StackAlloc LLVM.Mutable "stack_alloc" mem stackSizex2 LLVM.noAlignment mem2 <- liftIO $ LLVM.doArrayStore sym mem1 stackBasePtr LLVM.noAlignment stackArray stackSize initSPVal <- liftIO $ LLVM.ptrAdd sym C.knownRepr stackBasePtr stackSize diff --git a/symbolic/macaw-symbolic.cabal b/symbolic/macaw-symbolic.cabal index c665cc96..88bfd0d3 100644 --- a/symbolic/macaw-symbolic.cabal +++ b/symbolic/macaw-symbolic.cabal @@ -10,6 +10,7 @@ license-file: LICENSE library build-depends: base >= 4, + bv-sized >= 1.0.0, ansi-wl-pprint, containers, IntervalMap >= 0.6 && < 0.7, @@ -50,6 +51,6 @@ test-suite doctests hs-source-dirs: test main-is: doctest.hs ghc-options: -Wall -Wcompat -threaded - build-depends: base, doctest >= 0.10 && < 0.17 + build-depends: base, macaw-base, macaw-symbolic, doctest >= 0.10 && < 0.17 diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index c38cdd04..14a68051 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -123,6 +123,7 @@ import GHC.TypeLits import Control.Lens ((^.)) import Control.Monad import Control.Monad.IO.Class +import qualified Data.BitVector.Sized as BV import qualified Data.Foldable as F import qualified Data.Map.Strict as Map import Data.Maybe @@ -894,8 +895,8 @@ evalMacawExprExtension sym _iTypes _logFn f e0 = c <- f cv let w' = incNat w Just LeqProof <- pure $ testLeq (knownNat :: NatRepr 1) w' - one <- What4.Interface.bvLit sym w' 1 - zero <- What4.Interface.bvLit sym w' 0 + one <- What4.Interface.bvLit sym w' (BV.one w') + zero <- What4.Interface.bvLit sym w' (BV.zero w') cext <- baseTypeIte sym c one zero case op of Uadc -> do diff --git a/symbolic/src/Data/Macaw/Symbolic/Bitcast.hs b/symbolic/src/Data/Macaw/Symbolic/Bitcast.hs index b71a4d57..662d9b9c 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Bitcast.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Bitcast.hs @@ -10,6 +10,7 @@ module Data.Macaw.Symbolic.Bitcast ( import GHC.TypeLits import Control.Monad ( forM, when ) +import qualified Data.BitVector.Sized as BV import qualified Data.Foldable as F import qualified Data.Vector as V @@ -64,7 +65,7 @@ doBitcast sym x eqPr = let doPack :: (Integer,SymBV sym (n GHC.TypeLits.* w)) -> MM.LLVMPtr sym w -> IO (Integer, SymBV sym (n GHC.TypeLits.* w)) doPack (i,r) y = do extY <- bvZext sym outW =<< MM.projectLLVM_bv sym y - shiftAmt <- bvLit sym outW i + shiftAmt <- bvLit sym outW (BV.mkBV outW i) r' <- bvOrBits sym r =<< bvShl sym extY shiftAmt pure (i+1,r') (_,r) <- F.foldlM doPack (1,extH) rest @@ -75,7 +76,7 @@ doBitcast sym x eqPr = LeqProof <- pure $ plus1LeqDbl n w xbv <- MM.projectLLVM_bv sym x V.generateM (fromIntegral (natValue n)) $ \i -> do - shiftAmt <- bvLit sym inW (toInteger i) + shiftAmt <- bvLit sym inW (BV.mkBV inW (toInteger i)) MM.llvmPointer_bv sym =<< bvTrunc sym w =<< bvLshr sym xbv shiftAmt M.FromFloat f -> do Refl <- pure $ checkMacawFloatEq f diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index c7bf9b60..2b802e65 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs @@ -83,7 +83,7 @@ import Control.Lens hiding (Empty, (:>)) import Control.Monad.Except import qualified Control.Monad.Fail as MF import Control.Monad.State.Strict -import Data.Bits +import qualified Data.BitVector.Sized as BV import qualified Data.Foldable as F import qualified Data.Kind as K import qualified Data.Macaw.CFG as M @@ -850,7 +850,7 @@ addLemma x y = -- | Create a crucible value for a bitvector literal. bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids s (CR.Atom s (C.BVType w)) -bvLit w i = crucibleValue (C.BVLit w (i .&. maxUnsigned w)) +bvLit w i = crucibleValue (C.BVLit w (BV.mkBV w i)) bitOp2 :: (1 <= w) => NatRepr w @@ -954,8 +954,8 @@ appToCrucible app = do M.BVAdc w x y c -> do z <- appAtom =<< C.BVAdd w <$> v2c' w x <*> v2c' w y d <- appAtom =<< C.BaseIte (C.BaseBVRepr w) <$> v2c c - <*> appAtom (C.BVLit w 1) - <*> appAtom (C.BVLit w 0) + <*> appAtom (C.BVLit w (BV.one w)) + <*> appAtom (C.BVLit w (BV.zero w)) appBVAtom w (C.BVAdd w z d) M.BVSub w x y -> do @@ -969,8 +969,8 @@ appToCrucible app = do M.BVSbb w x y c -> do z <- appAtom =<< C.BVSub w <$> v2c' w x <*> v2c' w y d <- appAtom =<< C.BaseIte (C.BaseBVRepr w) <$> v2c c - <*> appAtom (C.BVLit w 1) - <*> appAtom (C.BVLit w 0) + <*> appAtom (C.BVLit w (BV.one w)) + <*> appAtom (C.BVLit w (BV.zero w)) appBVAtom w (C.BVSub w z d) @@ -1495,7 +1495,7 @@ addIPSwitch blockLabelMap targets macaw_ip = do let Just bvAddr = M.segoffAsAbsoluteAddr thenAddr -- Make a Crucible instruction sequence that compares the current IP -- against a possible target taken from the input list. - return ( [ CR.DefineAtom ptrBitsAtom $ CR.EvalApp $ C.BVLit width (toInteger bvAddr) + return ( [ CR.DefineAtom ptrBitsAtom $ CR.EvalApp $ C.BVLit width (BV.mkBV width (toInteger bvAddr)) , CR.DefineAtom ptrAtom $ CR.EvalApp $ C.ExtensionApp $ BitsToPtr width ptrBitsAtom , CR.DefineAtom eqAtom $ CR.EvalExt $ PtrEq widthRepr ipVal ptrAtom ] @@ -1574,7 +1574,7 @@ addSwitch blockLabelMap idx possibleAddrs = do let thnLbl = parsedBlockLabel blockLabelMap thnAddr return ( [ CR.DefineAtom thnIdxBitsAtom $ - CR.EvalApp $ C.BVLit width (toInteger thnIdx) + CR.EvalApp $ C.BVLit width (BV.mkBV width (toInteger thnIdx)) , CR.DefineAtom thnIdxAtom $ CR.EvalApp $ C.ExtensionApp $ BitsToPtr width thnIdxBitsAtom diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs index ecc0e838..474dbba8 100644 --- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs +++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs @@ -41,6 +41,7 @@ import Control.Monad (guard, when) import Data.Bits (testBit) import qualified Data.Vector as V +import qualified Data.BitVector.Sized as BV import Data.Parameterized (Some(..)) import qualified Data.Parameterized.Context as Ctx @@ -351,7 +352,8 @@ doGetGlobal st mvar globs addr = do let sym = st^.stateSymInterface mem <- getMem st mvar regionNum <- natLit sym (fromIntegral (M.addrBase addr)) - offset <- bvLit sym (M.addrWidthNatRepr (M.addrWidthRepr addr)) (M.memWordToUnsigned (M.addrOffset addr)) + let w = M.addrWidthNatRepr (M.addrWidthRepr addr) + offset <- bvLit sym w (BV.mkBV w (M.memWordToUnsigned (M.addrOffset addr))) ptr <- globs sym mem regionNum offset return (ptr, st) @@ -485,7 +487,7 @@ isAlignMask v = do 0 <- asNat (ptrBase v) let off = asBits v w = fromInteger (intValue (bvWidth off)) - k <- asUnsignedBV off + k <- BV.asUnsigned <$> asBV off let (zeros,ones) = break (testBit k) (take w [ 0 .. ]) guard (all (testBit k) ones) return (fromIntegral (length zeros)) @@ -514,7 +516,7 @@ doPtrAnd = ptrOp $ \sym _mem w xPtr xBits yPtr yBits x y -> Just LeqProof <- return (testLeq n nw) let mostBits = subNat nw n Just LeqProof <- return (testLeq (knownNat @1) mostBits) - most <- bvLit sym mostBits 0 + most <- bvLit sym mostBits (BV.zero mostBits) bts <- bvConcat sym most least diff --git a/symbolic/src/Data/Macaw/Symbolic/MemTraceOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemTraceOps.hs index edcde3a1..e6b99969 100644 --- a/symbolic/src/Data/Macaw/Symbolic/MemTraceOps.hs +++ b/symbolic/src/Data/Macaw/Symbolic/MemTraceOps.hs @@ -24,6 +24,7 @@ module Data.Macaw.Symbolic.MemTraceOps where import Control.Applicative import Control.Lens ((%~), (&), (^.)) import Control.Monad.State +import qualified Data.BitVector.Sized as BV import Data.List import Data.Sequence (Seq) import qualified Data.Sequence as Seq @@ -364,7 +365,7 @@ freshRegValue sym (LLVMPointer reg off) = go 0 where describe :: NatRepr w -> Integer -> [String] describe = case (asConcrete reg, asConcrete off) of (Just (ConcreteNat regVal), Just (ConcreteBV _ offVal)) -> \byteWidth n -> - ["read", show (natValue byteWidth), show regVal, "0x" ++ showHex (offVal + n) ""] + ["read", show (natValue byteWidth), show regVal, "0x" ++ showHex (BV.asUnsigned offVal + n) ""] _ -> \byteWidth _n -> ["read", show (natValue byteWidth), "symbolic_location"] doMemOpInternal :: forall sym ptrW ty. @@ -384,10 +385,10 @@ doMemOpInternal sym dir cond ptrWidth = go where where bitWidth = natMultiply (knownNat @8) byteWidth FloatMemRepr _infoRepr _endianness -> fail "reading floats not supported in doMemOpInternal" PackedVecMemRepr _countRepr recRepr -> addrWidthsArePositive ptrWidth $ do - elemSize <- liftIO $ bvLit sym ptrWidthNatRepr (memReprByteSize recRepr) + elemSize <- liftIO $ bvLit sym ptrWidthNatRepr (BV.mkBV ptrWidthNatRepr (memReprByteSize recRepr)) flip V.imapM_ regVal $ \i recRegVal -> do off' <- liftIO $ do - symbolicI <- bvLit sym ptrWidthNatRepr (toInteger i) + symbolicI <- bvLit sym ptrWidthNatRepr (BV.mkBV ptrWidthNatRepr (toInteger i)) dOff <- bvMul sym symbolicI elemSize bvAdd sym off dOff go (LLVMPointer reg off') recRegVal recRepr diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 49141b35..07578d55 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -114,6 +114,7 @@ import GHC.TypeLits import qualified Control.Lens as L import Control.Monad import Control.Monad.IO.Class ( MonadIO, liftIO ) +import qualified Data.BitVector.Sized as BV import qualified Data.ByteString as BS import qualified Data.Foldable as F import qualified Data.IntervalMap.Strict as IM @@ -253,9 +254,9 @@ populateMemory proxy sym mmc mem symArray0 = MC.RelocationRegion {} -> error $ "SymbolicRef SegmentRanges are not supported yet: " ++ show memChunk MC.BSSRegion sz -> - liftIO $ replicate (fromIntegral sz) <$> WI.bvLit sym PN.knownNat 0 + liftIO $ replicate (fromIntegral sz) <$> WI.bvLit sym PN.knownNat (BV.zero PN.knownNat) MC.ByteRegion bytes -> - liftIO $ mapM (WI.bvLit sym PN.knownNat . fromIntegral) $ BS.unpack bytes + liftIO $ mapM (WI.bvLit sym PN.knownNat . BV.word8) $ BS.unpack bytes populateSegmentChunk proxy sym mmc mem symArray seg addr concreteBytes allocs2 -- | If we want to treat the contents of this chunk of memory (the bytes at the @@ -356,7 +357,7 @@ populateSegmentChunk _ sym mmc mem symArray seg addr bytes ptrtable = do F.forM_ (zip [0.. size - 1] bytes) $ \(idx, byte) -> do let byteAddr = MC.incAddr (fromIntegral idx) addr let Just absByteAddr = MC.asAbsoluteAddr byteAddr - index_bv <- liftIO $ WI.bvLit sym (MC.memWidth mem) (fromIntegral absByteAddr) + index_bv <- liftIO $ WI.bvLit sym (MC.memWidth mem) (BV.mkBV (MC.memWidth mem) (toInteger absByteAddr)) eq_pred <- liftIO $ WI.bvEq sym byte =<< WI.arrayLookup sym symArray (Ctx.singleton index_bv) prog_loc <- liftIO $ WI.getCurrentProgramLoc sym let desc = "Byte@" ++ show byteAddr @@ -415,26 +416,30 @@ mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do | otherwise = case range of IM.IntervalCO lo hi -> do - lobv <- WI.bvLit sym (memRepr mpt) (fromIntegral lo) - hibv <- WI.bvLit sym (memRepr mpt) (fromIntegral hi) + let w = memRepr mpt + lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) + hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) lob <- WI.bvUlt sym lobv off hib <- WI.bvUle sym off hibv WI.andPred sym lob hib IM.ClosedInterval lo hi -> do - lobv <- WI.bvLit sym (memRepr mpt) (fromIntegral lo) - hibv <- WI.bvLit sym (memRepr mpt) (fromIntegral hi) + let w = memRepr mpt + lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) + hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) lob <- WI.bvUlt sym lobv off hib <- WI.bvUlt sym off hibv WI.andPred sym lob hib IM.OpenInterval lo hi -> do - lobv <- WI.bvLit sym (memRepr mpt) (fromIntegral lo) - hibv <- WI.bvLit sym (memRepr mpt) (fromIntegral hi) + let w = memRepr mpt + lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) + hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) lob <- WI.bvUle sym lobv off hib <- WI.bvUle sym off hibv WI.andPred sym lob hib IM.IntervalOC lo hi -> do - lobv <- WI.bvLit sym (memRepr mpt) (fromIntegral lo) - hibv <- WI.bvLit sym (memRepr mpt) (fromIntegral hi) + let w = memRepr mpt + lobv <- WI.bvLit sym w (BV.mkBV w (toInteger lo)) + hibv <- WI.bvLit sym w (BV.mkBV w (toInteger hi)) lob <- WI.bvUle sym lobv off hib <- WI.bvUlt sym off hibv WI.andPred sym lob hib diff --git a/x86_symbolic/macaw-x86-symbolic.cabal b/x86_symbolic/macaw-x86-symbolic.cabal index 417a1463..022d00d4 100644 --- a/x86_symbolic/macaw-x86-symbolic.cabal +++ b/x86_symbolic/macaw-x86-symbolic.cabal @@ -10,6 +10,7 @@ license-file: LICENSE library build-depends: base >= 4, ansi-wl-pprint, + bv-sized >= 1.0.0, crucible >= 0.4, crucible-llvm, flexdis86 >= 0.1.2, diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs index 94fbe5ab..c6c6fd81 100644 --- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs +++ b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs @@ -34,6 +34,7 @@ import Control.Lens ((^.)) import Control.Monad import Data.Bits hiding (xor) import Data.Kind ( Type ) +import qualified Data.BitVector.Sized as BV import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Context.Unsafe (empty,extend) import Data.Parameterized.NatRepr @@ -114,9 +115,9 @@ withConcreteCountAndDir state val_size wrapped_count _wrapped_dir func = do case asConcrete bv_count of Just (ConcreteBV _ count) -> do res_crux_state <- foldM func state - =<< mapM (\index -> bvLit sym knownNat $ index * val_byte_size) + =<< mapM (\index -> bvLit sym knownNat $ BV.mkBV knownNat $ index * val_byte_size) -- [0..((if dir then 1 else -1) * (count - 1))] - [0..(count - 1)] + [0..(BV.asUnsigned count - 1)] return ((), res_crux_state) Nothing -> error $ "Unsupported symbolic count in rep stmt: " @@ -513,7 +514,7 @@ getDenominator dw sym macawDenom = do let symi = symIface sym den <- getBitVal symi macawDenom -- Check denominator is not 0 - do let bvZ = app (BVLit dw 0) + do let bvZ = app (BVLit dw (BV.zero dw)) denNotZero <- evalApp sym $ Not (app (BVEq dw den bvZ)) let errMsg = "denominator not zero" assert symi denNotZero (C.AssertFailureSimError errMsg (errMsg ++ " in Data.Macaw.X86.Crucible.getDenominator")) @@ -761,7 +762,7 @@ evalApp :: forall sym t. IsSymInterface sym => evalApp sym = evalApp' sym (evalE sym) bv :: (KnownNat w, 1 <= w) => Int -> E sym (BVType w) -bv i = app (BVLit knownNat (fromIntegral i)) +bv i = app (BVLit knownNat (BV.mkBV knownNat (toInteger i))) bvTestBit :: (KnownNat w, 1 <= w) => E sym (BVType w) -> Int -> E sym BoolType bvTestBit e n = app $ BVNonzero knownNat $