Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to changes in GaloisInc/macaw#327 #1838

Merged
merged 2 commits into from
Mar 15, 2023
Merged

Adapt to changes in GaloisInc/macaw#327 #1838

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4fb3fd2
Bump elf-edit, macaw submodules
RyanGlScott Mar 10, 2023
e74a79a
Adapt to changes in GaloisInc/macaw#327
RyanGlScott Mar 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/elf-edit
Open in desktop
Submodule elf-edit updated 4 files
+3 −0 ChangeLog.md
+54 −23 src/Data/ElfEdit/Prim/HeaderInfo.hs
+13 −5 src/Data/ElfEdit/Prim/SymbolTable.hs
+22 −2 tests/Test.hs
2 changes: 1 addition & 1 deletion deps/macaw
Open in desktop
Submodule macaw updated 59 files
+32 −31 README.md
+9 −0 base/ChangeLog.md
+6 −0 base/macaw-base.cabal
+2 −2 base/src/Data/Macaw/CFG/App.hs
+4 −2 base/src/Data/Macaw/CFG/AssignRhs.hs
+3 −0 base/src/Data/Macaw/CFG/Core.hs
+36 −35 base/src/Data/Macaw/Memory/ElfLoader.hs
+342 −0 base/src/Data/Macaw/Memory/ElfLoader/DynamicDependencies.hs
+426 −0 base/src/Data/Macaw/Memory/ElfLoader/PLTStubs.hs
+2 −0 base/src/Data/Macaw/Types.hs
+1 −1 deps/asl-translator
+1 −1 deps/elf-edit
+1 −1 deps/semmc
+229 −0 doc/Design.md
+18 −12 macaw-aarch32-symbolic/tests/Main.hs
+22 −0 macaw-aarch32-symbolic/tests/pass/Makefile
+21 −0 macaw-aarch32-symbolic/tests/pass/movt.c
+ − macaw-aarch32-symbolic/tests/pass/movt.opt.exe
+ − macaw-aarch32-symbolic/tests/pass/movt.unopt.exe
+8 −0 macaw-aarch32-symbolic/tests/pass/so/fib.c
+1 −0 macaw-aarch32-symbolic/tests/pass/so/fib.h
+5 −0 macaw-aarch32-symbolic/tests/pass/so/getone.c
+1 −0 macaw-aarch32-symbolic/tests/pass/so/getone.h
+ − macaw-aarch32-symbolic/tests/pass/so/libfib.opt.so
+ − macaw-aarch32-symbolic/tests/pass/so/libfib.unopt.so
+ − macaw-aarch32-symbolic/tests/pass/so/libgetone.opt.so
+ − macaw-aarch32-symbolic/tests/pass/so/libgetone.unopt.so
+9 −0 macaw-aarch32-symbolic/tests/pass/so/so.c
+ − macaw-aarch32-symbolic/tests/pass/so/so.opt.exe
+ − macaw-aarch32-symbolic/tests/pass/so/so.unopt.exe
+11 −0 macaw-aarch32/src/Data/Macaw/ARM.hs
+12 −2 macaw-aarch32/src/Data/Macaw/ARM/Identify.hs
+26 −13 macaw-ppc-symbolic/tests/Main.hs
+6 −6 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+6 −2 refinement/tests/RefinementTests.hs
+61 −0 symbolic/ChangeLog.md
+6 −0 symbolic/macaw-symbolic.cabal
+132 −52 symbolic/src/Data/Macaw/Symbolic.hs
+221 −0 symbolic/src/Data/Macaw/Symbolic/Concretize.hs
+33 −3 symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+86 −235 symbolic/src/Data/Macaw/Symbolic/Memory.hs
+320 −0 symbolic/src/Data/Macaw/Symbolic/Memory/Common.hs
+894 −0 symbolic/src/Data/Macaw/Symbolic/Memory/Lazy.hs
+563 −56 symbolic/src/Data/Macaw/Symbolic/Testing.hs
+1 −0 x86/macaw-x86.cabal
+10 −0 x86/src/Data/Macaw/X86.hs
+15 −10 x86_symbolic/tests/Main.hs
+16 −0 x86_symbolic/tests/pass/Makefile
+8 −0 x86_symbolic/tests/pass/so/fib.c
+1 −0 x86_symbolic/tests/pass/so/fib.h
+5 −0 x86_symbolic/tests/pass/so/getone.c
+1 −0 x86_symbolic/tests/pass/so/getone.h
+ − x86_symbolic/tests/pass/so/libfib.opt.so
+ − x86_symbolic/tests/pass/so/libfib.unopt.so
+ − x86_symbolic/tests/pass/so/libgetone.opt.so
+ − x86_symbolic/tests/pass/so/libgetone.unopt.so
+9 −0 x86_symbolic/tests/pass/so/so.c
+ − x86_symbolic/tests/pass/so/so.opt.exe
+ − x86_symbolic/tests/pass/so/so.unopt.exe
15 changes: 10 additions & 5 deletions src/SAWScript/Crucible/LLVM/X86.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -475,13 +475,18 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
archEvalFns = Macaw.x86_64MacawEvalFn sfs Macaw.defaultMacawArchStmtExtensionOverride
lookupSyscall = Macaw.unsupportedSyscalls "saw-script"
noExtraValidityPred _ _ _ _ = return Nothing
mmConf = Macaw.MemModelConfig
{ Macaw.globalMemMap = mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase
, Macaw.lookupFunctionHandle = funcLookup
, Macaw.lookupSyscallHandle = lookupSyscall
, Macaw.mkGlobalPointerValidityAssertion = noExtraValidityPred
, Macaw.resolvePointer = pure
, Macaw.concreteImmutableGlobalRead = \_ _ -> pure Nothing
, Macaw.lazilyPopulateGlobalMem = \_ _ -> pure
}
defaultMacawExtensions_x86_64 =
Macaw.macawExtensions
archEvalFns mvar
(mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase)
funcLookup
lookupSyscall
noExtraValidityPred
archEvalFns mvar mmConf
sawMacawExtensions = defaultMacawExtensions_x86_64
{ C.extensionExec = \s0 st -> case s0 of
Macaw.PtrLt w x y -> doPtrCmp W4.bvUlt st mvar w x y
Expand Down
12 changes: 11 additions & 1 deletion src/SAWScript/X86.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ import Data.Macaw.Symbolic( ArchRegStruct
, GlobalMap
, MacawSimulatorState(..)
, macawExtensions
, MemModelConfig(..)
, unsupportedSyscalls
, defaultMacawArchStmtExtensionOverride
)
Expand Down Expand Up @@ -491,13 +492,22 @@ doSim opts elf sfs name (globs,overs) st checkPost =
let noExtraValidityPred _ _ _ _ = return Nothing
let archEvalFns = x86_64MacawEvalFn sfs defaultMacawArchStmtExtensionOverride
let lookupSyscall = unsupportedSyscalls "saw-script"
let mmConf = MemModelConfig
{ globalMemMap = globs
, lookupFunctionHandle = callHandler overs sym
, lookupSyscallHandle = lookupSyscall
, mkGlobalPointerValidityAssertion = noExtraValidityPred
, resolvePointer = pure
, concreteImmutableGlobalRead = \_ _ -> pure Nothing
, lazilyPopulateGlobalMem = \_ _ -> pure
}
let ctx :: SimContext (MacawSimulatorState Sym) Sym (MacawExt X86_64)
ctx = SimContext { _ctxBackend = backend opts
, ctxSolverProof = \a -> a
, ctxIntrinsicTypes = llvmIntrinsicTypes
, simHandleAllocator = allocator opts
, printHandle = stdout
, extensionImpl = macawExtensions archEvalFns mvar globs (callHandler overs sym) lookupSyscall noExtraValidityPred
, extensionImpl = macawExtensions archEvalFns mvar mmConf
, _functionBindings = FnBindings $
insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) emptyHandleMap
, _cruciblePersonality = MacawSimulatorState
Expand Down