Skip to content

Commit

Permalink
Adapt to GaloisInc/crucible#906
Browse files Browse the repository at this point in the history 
This bumps the `crucible` submodule to include GaloisInc/crucible#906. This
also bumps the `macaw` submodule to include GaloisInc/macaw#245, which adapts
`macaw-symbolic` to the `crucible` changes. The `crucible` changes require
adding some additional `?memOpts :: MemOptions` and `HasLLVMAnn Sym`
constraints to various functions in `saw-script`.
  • Loading branch information
@RyanGlScott
RyanGlScott committed Nov 23, 2021
1 parent 7e0db49 commit 0c4c622
Show file tree
Hide file tree
Showing 4 changed files with 30 additions and 8 deletions.
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 34 files
+2 −1 crucible-concurrency/src/Cruces/CrucesMain.hs
+16 −0 crucible-llvm/CHANGELOG.md
+1 −0 crucible-llvm/crucible-llvm.cabal
+49 −6 crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs
+16 −8 crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+42 −11 crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+12 −1 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+46 −3 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs
+82 −43 crucible-llvm/src/Lang/Crucible/LLVM/SymIO.hs
+6 −0 crucible-llvm/test/MemSetup.hs
+2 −1 crucible-llvm/test/TestMemory.hs
+289 −153 crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+3 −0 crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+6 −0 crux-llvm/CHANGELOG.md
+17 −1 crux-llvm/README.md
+1 −0 crux-llvm/crux-llvm.cabal
+17 −1 crux-llvm/src/Crux/LLVM/Config.hs
+4 −1 crux-llvm/src/Crux/LLVM/Simulate.hs
+54 −1 crux-llvm/svcomp/crux-llvm-svcomp-driver.sh
+8 −16 crux-llvm/svcomp/def-files/crux.py
+0 −4 crux-llvm/svcomp/def-files/crux.xml
+13 −0 crux-llvm/test-data/golden/T844-stable.c
+3 −0 crux-llvm/test-data/golden/T844-stable.config
+1 −0 crux-llvm/test-data/golden/T844-stable.good
+13 −0 crux-llvm/test-data/golden/T844-unstable.c
+3 −0 crux-llvm/test-data/golden/T844-unstable.config
+4 −0 crux-llvm/test-data/golden/T844-unstable.good
+4 −0 uc-crux-llvm/CHANGELOG.md
+5 −3 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+3 −2 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Unsound.hs
+2 −2 uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+8 −4 uc-crux-llvm/src/UCCrux/LLVM/Setup.hs
+4 −1 uc-crux-llvm/src/UCCrux/LLVM/Setup/Monad.hs
+1 −0 uc-crux-llvm/uc-crux-llvm.cabal
2 changes: 1 addition & 1 deletion deps/macaw
Submodule macaw updated 43 files
+20 −0 base/ChangeLog.md
+1 −1 base/src/Data/Macaw/Analysis/FunctionArgs.hs
+2 −2 base/src/Data/Macaw/Analysis/RegisterUse.hs
+3 −3 base/src/Data/Macaw/Architecture/Info.hs
+4 −7 base/src/Data/Macaw/CFG/AssignRhs.hs
+2 −2 base/src/Data/Macaw/CFG/Block.hs
+8 −1 base/src/Data/Macaw/CFG/Core.hs
+2 −0 base/src/Data/Macaw/Discovery/Classifier.hs
+2 −2 base/src/Data/Macaw/Discovery/ParsedContents.hs
+1 −1 deps/crucible
+1 −1 deps/llvm-pretty-bc-parser
+1 −1 deps/semmc
+1 −0 macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal
+41 −9 macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
+2 −0 macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs
+6 −0 macaw-aarch32-symbolic/tests/pass/Makefile
+24 −0 macaw-aarch32-symbolic/tests/pass/test-conditional-return.c
+ − macaw-aarch32-symbolic/tests/pass/test-conditional-return.opt.exe
+ − macaw-aarch32-symbolic/tests/pass/test-conditional-return.unopt.exe
+3 −0 macaw-aarch32-symbolic/tests/pass/util.h
+2 −0 macaw-aarch32/macaw-aarch32.cabal
+3 −2 macaw-aarch32/src/Data/Macaw/ARM.hs
+45 −12 macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
+22 −1 macaw-aarch32/src/Data/Macaw/ARM/Eval.hs
+135 −0 macaw-aarch32/src/Data/Macaw/ARM/Identify.hs
+15 −0 macaw-aarch32/src/Data/Macaw/ARM/Panic.hs
+43 −9 macaw-aarch32/tests/ARMTests.hs
+9 −2 macaw-aarch32/tests/TestMain.hs
+ − macaw-aarch32/tests/arm/test-conditional-return-a32.exe
+5 −0 macaw-aarch32/tests/arm/test-conditional-return-a32.mcw.expected
+13 −10 macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
+28 −13 macaw-ppc/src/Data/Macaw/PPC/Arch.hs
+1 −1 macaw-ppc/src/Data/Macaw/PPC/Eval.hs
+1 −0 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+23 −0 symbolic/ChangeLog.md
+6 −0 symbolic/src/Data/Macaw/Symbolic/Backend.hs
+14 −3 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+1 −0 symbolic/src/Data/Macaw/Symbolic/Memory.hs
+1 −1 x86/src/Data/Macaw/X86.hs
+17 −5 x86/src/Data/Macaw/X86/ArchTypes.hs
+1 −1 x86/src/Data/Macaw/X86/Generator.hs
+6 −2 x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+13 −7 x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
16 changes: 13 additions & 3 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -739,7 +739,10 @@ checkSpecReturnType cc mspec =
-- Returns a tuple of (arguments, preconditions, pointer values,
-- memory).
verifyPrestate ::
(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
( ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options ->
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
Expand Down Expand Up @@ -879,7 +882,11 @@ resolveArguments cc mem mspec env = mapM resolveArg [0..(nArgs-1)]
-- | For each "llvm_global_alloc" in the method specification, allocate and
-- register the appropriate memory.
setupGlobalAllocs :: forall arch.
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
MemImpl ->
Expand Down Expand Up @@ -1007,7 +1014,10 @@ assertEqualVals cc v1 v2 =

-- TODO(langston): combine with/move to executeAllocation
doAlloc ::
(Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
( ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
LLVMCrucibleContext arch ->
AllocIndex ->
LLVMAllocSpec ->
Expand Down
18 changes: 15 additions & 3 deletions src/SAWScript/Crucible/LLVM/Override.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -626,7 +626,11 @@ methodSpecHandler_prestate opts sc cc args cs =
-- and computing postcondition predicates.
methodSpecHandler_poststate ::
forall arch ret.
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options {- ^ output/verbosity options -} ->
SharedContext {- ^ context for constructing SAW terms -} ->
LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} ->
Expand Down Expand Up @@ -696,7 +700,11 @@ enforceCompleteSubstitution loc ss =


-- execute a pre/post condition
executeCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym)
executeCond :: ( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
)
=> Options
-> SharedContext
-> LLVMCrucibleContext arch
Expand Down Expand Up @@ -1609,7 +1617,11 @@ invalidateMutableAllocs opts sc cc cs = do
-- | Perform an allocation as indicated by an @llvm_alloc@ or
-- @llvm_fresh_pointer@ statement from the postcondition section.
executeAllocation ::
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
( ?lc :: Crucible.TypeContext
, ?memOpts :: Crucible.MemOptions
, Crucible.HasPtrWidth (Crucible.ArchWidth arch)
, Crucible.HasLLVMAnn Sym
) =>
Options ->
SharedContext ->
LLVMCrucibleContext arch ->
Expand Down

0 comments on commit 0c4c622

Please sign in to comment.