GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 14:27:51 +03:00
Code Issues Projects Releases Wiki Activity

update to bv-sized branch of what4 and other things

Browse Source
This commit is contained in:
Ben Selfridge 2020-05-24 23:02:56 -07:00
parent 162d7f0c2c
commit c079d5bf5e
24 changed files with 78 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitmodules vendored
View File

@ -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

2
base/macaw-base.cabal
View File

@ -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,

2
deps/asl-translator vendored

@ -1 +1 @@
Subproject commit 0c0f7ac37d4a72f59ac08b8281a23997b8f685b0
Subproject commit 01ed3683c76a3472f36912aaaa82f7631d0c5fd4

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit aca70a9b30a823579883e5b9ea1f81391b3e59fb
Subproject commit a9ff2089ac2e8f884dad05c8f5cecccb5ad148e8

2
deps/dismantle vendored

@ -1 +1 @@
Subproject commit 6c66dfaa131255383bd4cade0556beda00d57e90
Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9

2
deps/semmc vendored

@ -1 +1 @@
Subproject commit 67d66fbebd91db5aa773a0c4ff8e61be2382445c
Subproject commit 86f036b23a6ad91e5d92b590d16e0412a44318a5

2
deps/what4 vendored

@ -1 +1 @@
Subproject commit 3a12e48f9e066ce99d7c29c16f067235abbfec31
Subproject commit a8bdd561354d54fbbb8703cebe66e74a871acb8e

2
deps/what4-serialize vendored

@ -1 +1 @@
Subproject commit f6177603aff8f3fa663aece2f0b35046e9c4202d
Subproject commit c1e40e5d147eba202c08b3980139bda616f6af08

11
macaw-aarch32/src/Data/Macaw/ARM/Semantics/ThumbSemantics.hs
View File

@ -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
-- )

1
macaw-ppc/macaw-ppc.cabal
View File

@ -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,

7
macaw-ppc/src/Data/Macaw/PPC/Semantics/Base.hs
View File

@ -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.

1
macaw-semmc/macaw-semmc.cabal
View File

@ -38,6 +38,7 @@ library
dismantle-tablegen,
ansi-wl-pprint,
semmc,
bv-sized,
what4
hs-source-dirs: src
default-language: Haskell2010

13
macaw-semmc/src/Data/Macaw/SemMC/TH.hs
View File

@ -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)))

1
refinement/macaw-refinement.cabal
View File

@ -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

19
refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
View File

@ -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

3
symbolic/macaw-symbolic.cabal
View File

@ -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

5
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -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

5
symbolic/src/Data/Macaw/Symbolic/Bitcast.hs
View File

@ -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

16
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -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

8
symbolic/src/Data/Macaw/Symbolic/MemOps.hs
View File

@ -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

7
symbolic/src/Data/Macaw/Symbolic/MemTraceOps.hs
View File

@ -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

27
symbolic/src/Data/Macaw/Symbolic/Memory.hs
View File

@ -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

1
x86_symbolic/macaw-x86-symbolic.cabal
View File

@ -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,

9
x86_symbolic/src/Data/Macaw/X86/Crucible.hs
View File

@ -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 $