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

Jump to bottom

update to latest crucible + macaw #1209

Merged
merged 1 commit into from
Apr 23, 2021
Merged

update to latest crucible + macaw #1209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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/crucible
Open in desktop
Submodule crucible updated 56 files
+1 −1 .github/workflows/crux-mir-build.yml
+10 −4 crucible-llvm/src/Lang/Crucible/LLVM.hs
+12 −9 crucible-llvm/src/Lang/Crucible/LLVM/Errors/Poison.hs
+3 −2 crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+3 −2 crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
+1 −1 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+3 −4 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs
+3 −1 crucible-llvm/test/MemSetup.hs
+4 −1 crucible-llvm/test/Tests.hs
+124 −63 crux-llvm/src/Crux/LLVM/Simulate.hs
+6 −7 crux-mir/crux-mir.cabal
+2 −0 crux-mir/lib/crucible/lib.rs
+83 −0 crux-mir/lib/crucible/method_spec/mod.rs
+73 −0 crux-mir/lib/crucible/method_spec/raw.rs
+5 −5 crux-mir/src/Mir/Generate.hs
+332 −8 crux-mir/src/Mir/Intrinsics.hs
+61 −16 crux-mir/src/Mir/Language.hs
+3 −3 crux-mir/src/Mir/Mir.hs
+7 −3 crux-mir/src/Mir/Overrides.hs
+19 −0 crux-mir/src/Mir/Trans.hs
+25 −0 crux-mir/src/Mir/TransTy.hs
+1 −1 crux-mir/test/symb_eval/concretize/assert.good
+1 −1 crux-mir/test/symb_eval/crux/early_fail.good
+2 −2 crux-mir/test/symb_eval/crux/fail_return.good
+2 −2 crux-mir/test/symb_eval/crux/mixed_fail.good
+2 −2 crux-mir/test/symb_eval/crux/multi.good
+5 −5 crux-mir/test/symb_eval/crypto/bytes.good
+1 −1 crux-mir/test/symb_eval/overrides/override2.good
+1 −1 crux-mir/test/symb_eval/overrides/override5.good
+1 −1 crux-mir/test/symb_eval/sym_bytes/construct.good
+11 −2 crux/src/Crux.hs
+4 −2 uc-crux-llvm/README.md
+264 −320 uc-crux-llvm/src/UCCrux/LLVM/Classify.hs
+15 −25 uc-crux-llvm/src/UCCrux/LLVM/Classify/Poison.hs
+89 −56 uc-crux-llvm/src/UCCrux/LLVM/Classify/Types.hs
+168 −52 uc-crux-llvm/src/UCCrux/LLVM/Constraints.hs
+15 −6 uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
+73 −3 uc-crux-llvm/src/UCCrux/LLVM/Cursor.hs
+0 −188 uc-crux-llvm/src/UCCrux/LLVM/FullType/CrucibleType.hs
+466 −0 uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
+4 −0 uc-crux-llvm/src/UCCrux/LLVM/FullType/Type.hs
+11 −7 uc-crux-llvm/src/UCCrux/LLVM/Main.hs
+162 −32 uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+5 −3 uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs
+8 −6 uc-crux-llvm/src/UCCrux/LLVM/Run/Result.hs
+25 −10 uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+78 −13 uc-crux-llvm/src/UCCrux/LLVM/Setup.hs
+28 −0 uc-crux-llvm/src/UCCrux/LLVM/Setup/Monad.hs
+13 −12 uc-crux-llvm/src/UCCrux/LLVM/Stats.hs
+27 −14 uc-crux-llvm/test/Test.hs
+2 −0 uc-crux-llvm/test/programs/read_extern_global.c
+2 −0 uc-crux-llvm/test/programs/read_extern_global_sized_array.c
+2 −0 uc-crux-llvm/test/programs/read_extern_global_unsized_array.c
+2 −0 uc-crux-llvm/test/programs/read_null_global_pointer.c
+5 −0 uc-crux-llvm/test/programs/read_pointer_from_global_struct.c
+2 −0 uc-crux-llvm/uc-crux-llvm.cabal
2 changes: 1 addition & 1 deletion deps/macaw
Open in desktop
Submodule macaw updated 21 files
+3 −1 .gitignore
+3 −2 base/macaw-base.cabal
+81 −57 base/src/Data/Macaw/CFG/App.hs
+137 −140 base/src/Data/Macaw/Discovery.hs
+11 −3 base/src/Data/Macaw/Discovery/State.hs
+19 −8 base/src/Data/Macaw/Memory/ElfLoader.hs
+61 −0 base/src/Data/Macaw/Utils/IncComp.hs
+3 −11 base/src/Data/Macaw/Utils/Pretty.hs
+1 −1 deps/asl-translator
+1 −1 deps/crucible
+1 −1 deps/dismantle
+1 −1 deps/elf-edit
+1 −1 deps/flexdis86
+1 −1 deps/what4
+1 −1 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+6 −6 symbolic/src/Data/Macaw/Symbolic.hs
+14 −4 symbolic/src/Data/Macaw/Symbolic/Backend.hs
+1 −1 symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+4 −3 symbolic/src/Data/Macaw/Symbolic/Memory.hs
+4 −7 symbolic/src/Data/Macaw/Symbolic/Testing.hs
+3 −3 utils/compare-dwarfdump/README.md
4 changes: 2 additions & 2 deletions src/SAWScript/Crucible/LLVM/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -545,7 +545,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
}
Nothing -> mem0

let globals1 = Crucible.llvmGlobals (ccLLVMContext cc) mem
let globals1 = Crucible.llvmGlobals mvar mem

-- construct the initial state for verifications
opts <- getOptions
Expand Down Expand Up @@ -1353,7 +1353,7 @@ setupLLVMCrucibleContext pathSat lm action =
mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans)
=<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod

let globals = Crucible.llvmGlobals ctx mem
let globals = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem

let setupMem =
do -- register the callable override functions
Expand Down
3 changes: 2 additions & 1 deletion src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM
, pattern PtrRepr
, ppPtr
, projectLLVM_bv
, mkMemVar
) where

import Lang.Crucible.LLVM
Expand Down Expand Up @@ -171,7 +172,7 @@ import Lang.Crucible.LLVM.MemModel
(Mem, MemImpl, doResolveGlobal, storeRaw, storeConstRaw, mallocRaw, mallocConstRaw,
ppMem, packMemValue, unpackMemValue, buildDisjointRegionsAssertion,
doLoad, doStore, loadRaw, doPtrAddOffset, assertSafe, isZero, testEqual,
emptyMem, doMalloc,
emptyMem, doMalloc, mkMemVar,
LLVMVal(..),
LLVMPtr, HasPtrWidth, ptrToPtrVal, mkNullPointer, ptrIsNull, ppPtr, ptrEq,
pattern LLVMPointerRepr, LLVMPointerType,
Expand Down
4 changes: 3 additions & 1 deletion src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
import Control.Lens
import Control.Monad (when)
import Data.Functor.Compose (Compose(..))
import qualified Data.Text as Text
import Data.Type.Equality (TestEquality(..))
import qualified Prettyprinter as PPL
import qualified Text.LLVM.AST as L
Expand Down Expand Up @@ -254,7 +255,8 @@ loadLLVMModule file halloc =
Left err -> return (Left err)
Right llvm_mod ->
do let ?optLoopMerge = False
Some mtrans <- CL.translateModule halloc llvm_mod
memVar <- CL.mkMemVar (Text.pack "saw:llvm_memory") halloc
Some mtrans <- CL.translateModule halloc memVar llvm_mod
return (Right (Some (LLVMModule file llvm_mod mtrans)))

instance TestEquality LLVMModule where
Expand Down
12 changes: 2 additions & 10 deletions src/SAWScript/X86.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,6 @@ module SAWScript.X86

import Control.Lens (toListOf, folded, (^.))
import Control.Exception(Exception(..),throwIO)
import Control.Monad.ST (stToIO)
import Control.Monad.IO.Class(liftIO)

import qualified Data.BitVector.Sized as BV
Expand Down Expand Up @@ -201,7 +200,7 @@ proof fileReader archi file mbCry globs fun =
sym <- newSAWCoreBackend sc
let ?fileReader = fileReader
cenv <- loadCry sym mbCry
mvar <- mkMemVar halloc
mvar <- mkMemVar "saw_x86:llvm_memory" halloc
proofWithOptions Options
{ fileName = file
, function = fun
Expand Down Expand Up @@ -521,7 +520,7 @@ makeCFG ::
MemSegmentOff 64 ->
IO TheCFG
makeCFG opts elf name addr =
do (_,Some funInfo) <- stToIO $ analyzeFunction quiet addr UserRequest empty
do (_,Some funInfo) <- return $ analyzeFunction addr UserRequest empty
-- writeFile "MACAW.cfg" (show (pretty funInfo))
mkFunCFG x86 (allocator opts) cruxName posFn funInfo
where
Expand Down Expand Up @@ -610,13 +609,6 @@ x86 = x86_64MacawSymbolicFns
-- * not modified by interrupts


--------------------------------------------------------------------------------
-- Logging
quiet :: Applicative m => a -> m ()
quiet _ = pure ()



--------------------------------------------------------------------------------
-- Errors

Expand Down