GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-02 10:54:04 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #157 from GaloisInc/llvm_annotations_upd

Browse Source 
Update for addition of badBehaviorMap implicit for LLVM annotations.
This commit is contained in:
Kevin Quick 2020-08-11 11:08:57 -07:00 committed by GitHub
commit 4713bc91c7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 13 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
deps/asl-translator vendored

@ -1 +1 @@
Subproject commit d0bac677e038a54f47af0467e68c4aab95a32d64 Subproject commit a71409d4168fe7db912e85c9c53af550751a6adf

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit 5cb47b4f77299b54b0ead3f93f25dc24447c80f3 Subproject commit 996db66ca35950439282fc5724278dc5490ecd55

2
deps/dismantle vendored

@ -1 +1 @@
Subproject commit 1f61d7259228bbfb51053e7c990fac6d9228e154 Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9

2
deps/semmc vendored

@ -1 +1 @@
Subproject commit 990ce7ab63dd67cf0f23876d5d4d93da507ec11e Subproject commit 08ff6f46c68b0166784779744860d11d9c919f1f

2
deps/what4 vendored

@ -1 +1 @@
Subproject commit f9a8f950e7c66f0f04312ce3983a42f3facd576e Subproject commit b66527eda1274d4f9d539d8c2956d9fe215c4aa2

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

@ -508,6 +508,7 @@ initializeMemory :: forall arch sym m proxy
. ( MS.SymArchConstraints arch . ( MS.SymArchConstraints arch
, 16 <= M.ArchAddrWidth arch , 16 <= M.ArchAddrWidth arch
, CB.IsSymInterface sym , CB.IsSymInterface sym
, LLVM.HasLLVMAnn sym
, MonadIO m , MonadIO m
) )
=> proxy arch => proxy arch

4
refinement/tests/RefinementTests.hs
View File

@ -284,10 +284,10 @@ mkSymbolicTest testinp = do
CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi
regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns) regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns)
-- FIXME: We probably need to pull endianness from somewhere else -- FIXME: We probably need to pull endianness from somewhere else
(initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem
let globalMap = MSM.mapRegionPointers memPtrTbl
bbMapRef <- newIORef mempty bbMapRef <- newIORef mempty
let ?badBehaviorMap = bbMapRef let ?badBehaviorMap = bbMapRef
(initMem, memPtrTbl) <- MSM.newGlobalMemory proxy sym CLD.LittleEndian MSM.ConcreteMutable mem
let globalMap = MSM.mapRegionPointers memPtrTbl
let lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> let lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs ->
error "Could not find function handle" error "Could not find function handle"
let validityCheck _ _ _ _ = return Nothing let validityCheck _ _ _ _ = return Nothing

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

@ -196,6 +196,7 @@ newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch
, KnownNat (MC.ArchAddrWidth arch) , KnownNat (MC.ArchAddrWidth arch)
, CB.IsSymInterface sym , CB.IsSymInterface sym
, Ord (WI.SymExpr sym WI.BaseNatType) , Ord (WI.SymExpr sym WI.BaseNatType)
, CL.HasLLVMAnn sym
, MonadIO m , MonadIO m
) )
=> proxy arch => proxy arch
@ -479,6 +480,7 @@ mkGlobalPointerValidityPred mpt = \sym puse mcond ptr -> do
mapRegionPointers :: ( MC.MemWidth w mapRegionPointers :: ( MC.MemWidth w
, 16 <= w , 16 <= w
, CB.IsSymInterface sym , CB.IsSymInterface sym
, CL.HasLLVMAnn sym
) )
=> MemPtrTable sym w => MemPtrTable sym w
-> MS.GlobalMap sym CL.Mem w -> MS.GlobalMap sym CL.Mem w

6
x86_symbolic/tests/Main.hs
View File

@ -117,12 +117,12 @@ main = do
symFuns <- MX.newSymFuns sym symFuns <- MX.newSymFuns sym
(initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem
let globalMap = MSM.mapRegionPointers memPtrTbl
bbMapRef <- newIORef mempty bbMapRef <- newIORef mempty
let ?badBehaviorMap = bbMapRef let ?badBehaviorMap = bbMapRef
(initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem
let globalMap = MSM.mapRegionPointers memPtrTbl
let lookupFn :: MS.LookupFunctionHandle sym MX.X86_64 let lookupFn :: MS.LookupFunctionHandle sym MX.X86_64
lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> do lookupFn = MS.LookupFunctionHandle $ \_s _mem _regs -> do
fail "Could not find function handle." fail "Could not find function handle."