From 99f8cb0bdf1db5877b6758faafc82348c1b8d6a1 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 11 Sep 2020 14:40:02 -0700 Subject: [PATCH 1/3] Update to use new `HasLLVMAnn` API, which requires an action for recording (or discarding) annotations rather than a map. --- deps/crucible | 2 +- refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs | 4 +--- refinement/tests/RefinementTests.hs | 4 +--- symbolic/src/Data/Macaw/Symbolic.hs | 3 +-- symbolic/src/Data/Macaw/Symbolic/Memory.hs | 3 +-- x86_symbolic/tests/Main.hs | 3 +-- 6 files changed, 6 insertions(+), 13 deletions(-) diff --git a/deps/crucible b/deps/crucible index 996db66c..f02bccfc 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 996db66ca35950439282fc5724278dc5490ecd55 +Subproject commit f02bccfc6d369e5bff0a1e5ac1aa7889f671bddb diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs index 6ec9e875..f0266931 100644 --- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs +++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs @@ -30,7 +30,6 @@ 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 import qualified Data.Macaw.CFG as M import qualified Data.Macaw.Discovery as M @@ -184,8 +183,7 @@ smtSolveTransfer ctx slice case some_cfg of C.SomeCFG cfg -> do let executionFeatures = [] - bbMapRef <- liftIO $ newIORef mempty - let ?badBehaviorMap = bbMapRef + let ?recordLLVMAnnotation = \_ _ -> pure () initialState <- initializeSimulator ctx sym archVals halloc cfg entryBlock -- Symbolically execute the relevant code in a fresh assumption diff --git a/refinement/tests/RefinementTests.hs b/refinement/tests/RefinementTests.hs index 813141f0..adfabb3e 100644 --- a/refinement/tests/RefinementTests.hs +++ b/refinement/tests/RefinementTests.hs @@ -42,7 +42,6 @@ module Main ( main ) where import Control.Monad ( when ) import qualified Data.Foldable as F -import Data.IORef import qualified Data.Macaw.BinaryLoader as MBL import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Discovery as MD @@ -283,9 +282,8 @@ mkSymbolicTest testinp = do printf "External resolutions of %s: %s\n" (show funcName) (show (MD.discoveredClassifyFailureResolutions dfi)) CCC.SomeCFG cfg <- MS.mkFunCFG archFns halloc funcName (posFn proxy) dfi regs <- MS.macawAssignToCrucM (mkReg archFns sym) (MS.crucGenRegAssignment archFns) + let ?recordLLVMAnnotation = \_ _ -> pure () -- FIXME: We probably need to pull endianness from somewhere else - bbMapRef <- newIORef mempty - 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 -> diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs index 14a68051..126f096e 100644 --- a/symbolic/src/Data/Macaw/Symbolic.hs +++ b/symbolic/src/Data/Macaw/Symbolic.hs @@ -1252,8 +1252,7 @@ runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH toMemPred g reg -- -- ^ The CFG to simulate -- -> IO () -- useCFG hdlAlloc sym MS.ArchVals { MS.withArchEval = withArchEval } initialRegs initialMem globalMap lfh cfg = do --- bbMapRef <- newIORef mempty --- let ?badBehaviorMap = bbMapRef +-- let ?recordLLVMAnnotation = \_ _ -> pure () -- withArchEval sym $ \archEvalFns -> do -- let rep = CFH.handleReturnType (CC.cfgHandle cfg) -- memModelVar <- CLM.mkMemVar hdlAlloc diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs index 7e2896fe..563f0af0 100644 --- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs +++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs @@ -81,8 +81,7 @@ -- -- ^ The CFG to simulate -- -> IO () -- useCFG hdlAlloc sym MS.ArchVals { MS.withArchEval = withArchEval } initialRegs mem lfh cfg = do --- bbMapRef <- newIORef mempty --- let ?badBehaviorMap = bbMapRef +-- let ?recordLLVMAnnotation = \_ _ -> pure () -- withArchEval sym $ \archEvalFns -> do -- let rep = CFH.handleReturnType (CC.cfgHandle cfg) -- memModelVar <- CLM.mkMemVar hdlAlloc diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs index b03045a3..f5733d27 100644 --- a/x86_symbolic/tests/Main.hs +++ b/x86_symbolic/tests/Main.hs @@ -117,8 +117,7 @@ main = do symFuns <- MX.newSymFuns sym - bbMapRef <- newIORef mempty - let ?badBehaviorMap = bbMapRef + let ?recordLLVMAnnotation = \_ _ -> pure () (initMem, memPtrTbl) <- MSM.newGlobalMemory (Proxy @MX.X86_64) sym LittleEndian MSM.ConcreteMutable mem let globalMap = MSM.mapRegionPointers memPtrTbl From e9b960c6d5449bd910c50b8840fa2a1c39f2cd1b Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 15 Sep 2020 16:24:24 -0700 Subject: [PATCH 2/3] Bump semmc submodule --- deps/semmc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/semmc b/deps/semmc index 08ff6f46..6c2ab1cf 160000 --- a/deps/semmc +++ b/deps/semmc @@ -1 +1 @@ -Subproject commit 08ff6f46c68b0166784779744860d11d9c919f1f +Subproject commit 6c2ab1cf012f1af293916c76c5d44bb1ab53c893 From 0baa499c2a85b51536d73d30d7e7e7fc95ab58f8 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 21 Nov 2019 22:28:03 -0800 Subject: [PATCH 3/3] Migrate from Travis to Github Actions --- .github/workflows/ci.yaml | 50 +++++++++ .gitignore | 10 +- .travis.yml | 30 ----- ...eze => cabal.project.dist.ghc-8.8.4.freeze | 105 ++++++++---------- cabal.project.werror | 8 ++ 5 files changed, 111 insertions(+), 92 deletions(-) create mode 100644 .github/workflows/ci.yaml delete mode 100644 .travis.yml rename cabal.project.dist.ghc883.freeze => cabal.project.dist.ghc-8.8.4.freeze (77%) create mode 100644 cabal.project.werror diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml new file mode 100644 index 00000000..ee65e6c5 --- /dev/null +++ b/.github/workflows/ci.yaml @@ -0,0 +1,50 @@ +name: CI +on: + push: + +jobs: + build: + runs-on: ubuntu-latest + strategy: + matrix: + name: [linux-8.8.4] + include: + - name: linux-8.8.4 + ghc-ver: 8.8.4 + # complete all jobs + fail-fast: false + steps: + - name: Checkout + uses: actions/checkout@v2 + with: + submodules: true + - name: Get GHC + run: | + sudo apt-get install --no-install-recommends -y cabal-install-3.2 ghc-${{ matrix.ghc-ver }} + echo "::add-path::/opt/cabal/bin" + echo "::add-path::/opt/ghc/${{ matrix.ghc-ver }}/bin" + - name: Cache + uses: actions/cache@v1 + with: + path: /home/runner/.cabal/store/ghc-${{ matrix.ghc-ver }} + # Prefer previous SHA hash if it is still cached + key: ${{ matrix.name }}-${{ github.sha }} + # otherwise just use most recent build. + restore-keys: ${{ matrix.name }} + - name: Link cabal project files + run: | + ln -s cabal.project.dist cabal.project + ln -s cabal.project.werror cabal.project.local + ln -s cabal.project.dist.ghc-${{ matrix.ghc-ver }}.freeze cabal.project.freeze + - name: Cabal update + run: cabal update + # Build macaw-base dependencies and crucible separately just so later + # steps are less verbose and major dependency failures are separate. + - name: Cabal dependencies + run: | + cabal build --only-dependencies macaw-base + cabal build crucible-llvm + - name: Cabal x86 tests + run: cabal test macaw-x86 macaw-x86-symbolic + - name: Cabal ASL tests + run: cabal test macaw-asl-tests diff --git a/.gitignore b/.gitignore index 0cee409a..b476bbb2 100644 --- a/.gitignore +++ b/.gitignore @@ -2,13 +2,13 @@ *~ *.hi cabal.project -dist/ -dist-newstyle/ +/dist/ +/dist-newstyle/ cabal.sandbox.config .cabal-sandbox -.stack-work/ -stack.yaml -TAGS +/TAGS .ghc.environment.* **/tests/samples/*.last-actual **/tests/samples/*.s +/cabal.project.local +/cabal.project.freeze diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index b9982388..00000000 --- a/.travis.yml +++ /dev/null @@ -1,30 +0,0 @@ -sudo: false - -language: haskell -cabal: 2.4 -ghc: - - 8.4.4 - - 8.6.5 - -git: - submodules: false # whether to recursively clone submodules - -cache: - directories: - - $HOME/.ghc - - $HOME/.cabal - -install: -# Changes ssh paths into http path, so that we can do a read-only clone of -# our submodules without worrying about ssh keys. -- sed -i 's/git@github.com:/https:\/\/github.com\//' .gitmodules -- git submodule update --init -- cabal v2-configure --project-file=cabal.project.dist --flags="+asl-lite" -- cabal v2-update --project-file=cabal.project.dist - -script: -# Here starts the actual work to be performed for the package under test; -# any command which exits with a non-zero exit code causes the build to fail. - # Build packages - - cabal v2-test --project-file=cabal.project.dist x86 x86_symbolic - - cabal v2-test --project-file=cabal.project.dist macaw-asl-tests diff --git a/cabal.project.dist.ghc883.freeze b/cabal.project.dist.ghc-8.8.4.freeze similarity index 77% rename from cabal.project.dist.ghc883.freeze rename to cabal.project.dist.ghc-8.8.4.freeze index 61b1b870..684c7f5d 100644 --- a/cabal.project.dist.ghc883.freeze +++ b/cabal.project.dist.ghc-8.8.4.freeze @@ -1,15 +1,16 @@ +active-repositories: hackage.haskell.org:merge constraints: any.BoundedChan ==1.0.3.0, any.Cabal ==3.0.1.0, any.HUnit ==1.6.0.0, - any.IntervalMap ==0.6.1.1, + any.IntervalMap ==0.6.1.2, any.Only ==0.1, - any.QuickCheck ==2.14, - QuickCheck +templatehaskell, + any.QuickCheck ==2.14.1, + QuickCheck -old-random +templatehaskell, any.SHA ==1.6.4.4, SHA -exe, any.StateVar ==1.2, any.adjunctions ==4.4, - any.ansi-terminal ==0.10.3, + any.ansi-terminal ==0.11, ansi-terminal -example, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, @@ -24,7 +25,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.base ==4.13.0.0, any.base-compat ==0.11.1, any.base-orphans ==0.8.2, - any.base16-bytestring ==0.1.1.6, + any.base16-bytestring ==1.0.0.0, any.bifunctors ==5.5.7, bifunctors +semigroups +tagged, any.bimap ==0.4.0, @@ -34,8 +35,8 @@ constraints: any.BoundedChan ==1.0.3.0, any.blaze-textual ==0.2.1.0, blaze-textual -developer -integer-simple +native, any.boomerang ==1.4.6, - any.bv-sized ==1.0.1, - any.bytestring ==0.10.10.0, + any.bv-sized ==1.0.2, + any.bytestring ==0.10.10.1, any.bytestring-builder ==0.10.8.2.0, bytestring-builder +bytestring_has_builder, any.cabal-doctest ==1.0.8, @@ -49,8 +50,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.colour ==2.3.5, any.comonad ==5.0.6, comonad +containers +distributive +test-doctests, - any.concurrent-output ==1.10.11, - any.constraints ==0.11.2, + any.constraints ==0.12, any.containers ==0.6.2.1, any.contravariant ==1.5.2, contravariant +semigroups +statevar +tagged, @@ -58,7 +58,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, any.deepseq ==1.4.4.0, - any.deriving-compat ==0.5.8, + any.deriving-compat ==0.5.9, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.direct-sqlite ==2.3.26, direct-sqlite +fulltextsearch +haveusleep +json1 -systemlib +urifilenames, @@ -67,14 +67,12 @@ constraints: any.BoundedChan ==1.0.3.0, any.distributive ==0.6.2, distributive +semigroups +tagged, any.doctest ==0.16.3, - any.dotgen ==0.4.2, + any.dotgen ==0.4.3, dotgen -devel, - any.erf ==2.0.0.0, any.exceptions ==0.10.4, exceptions +transformers-0-4, - any.extra ==1.7.1, - any.fail ==4.9.0.0, - any.fgl ==5.7.0.2, + any.extra ==1.7.8, + any.fgl ==5.7.0.3, fgl +containers042, any.fgl-visualize ==0.1.0.1, any.filemanip ==0.3.6.3, @@ -83,29 +81,27 @@ constraints: any.BoundedChan ==1.0.3.0, any.finite-typelits ==0.1.4.2, any.free ==5.1.3, any.generic-random ==1.3.0.1, - any.ghc ==8.8.3, - any.ghc-boot ==8.8.3, - any.ghc-boot-th ==8.8.3, - any.ghc-heap ==8.8.3, + any.ghc ==8.8.4, + any.ghc-boot ==8.8.4, + any.ghc-boot-th ==8.8.4, + any.ghc-heap ==8.8.4, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.5.3, - any.ghci ==8.8.3, + any.ghci ==8.8.4, any.gitrev ==1.3.1, any.haggle ==0.1.0.0, - any.happy ==1.19.12, - happy +small_base, + any.happy ==1.20.0, any.hashable ==1.3.0.0, hashable -examples +integer-gmp +sse2 -sse41, - any.hashtables ==1.2.3.4, + any.hashtables ==1.2.4.1, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskell-lexer ==1.1, - any.hedgehog ==1.0.2, any.hpc ==0.6.0.3, any.hsc2hs ==0.68.7, hsc2hs -in-ghc-tree, - any.hspec ==2.7.1, - any.hspec-core ==2.7.1, - any.hspec-discover ==2.7.1, + any.hspec ==2.7.4, + any.hspec-core ==2.7.4, + any.hspec-discover ==2.7.4, any.hspec-expectations ==0.8.2, any.ilist ==0.4.0.1, any.indexed-list-literals ==0.2.1.3, @@ -113,38 +109,36 @@ constraints: any.BoundedChan ==1.0.3.0, any.integer-logarithms ==1.0.3, integer-logarithms -check-bounds +integer-gmp, any.invariant ==0.5.3, - any.io-streams ==1.5.1.0, - io-streams -nointeractivetests, + any.io-streams ==1.5.2.0, + io-streams +network -nointeractivetests +zlib, any.itanium-abi ==0.1.1.1, any.json ==0.10, json +generic -mapdict +parsec +pretty +split-base, any.kan-extensions ==5.2, any.lens ==4.19.2, lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.lifted-async ==0.10.0.6, - any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.located-base ==0.1.1.1, - any.logict ==0.7.0.2, + any.logict ==0.7.0.3, any.lumberjack ==0.1.0.2, - any.math-functions ==0.3.4.0, + any.math-functions ==0.3.4.1, math-functions +system-erf +system-expm1, any.megaparsec ==7.0.5, megaparsec -dev, any.microlens ==0.4.11.2, any.microlens-th ==0.4.3.5, - any.mmorph ==1.1.3, - any.monad-control ==1.0.2.3, any.monad-primitive ==0.1, any.monadLib ==3.10, any.mtl ==2.2.2, any.mwc-random ==0.14.0.0, - any.network ==3.1.1.1, + any.network ==3.1.2.0, + network -devel, any.old-locale ==1.0.0.7, - any.optparse-applicative ==0.15.1.0, + any.optparse-applicative ==0.16.0.0, any.ordered-containers ==0.2.2, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, + any.parameterized-utils ==2.1.1, parameterized-utils +unsafe-operations, any.parsec ==3.1.14.0, any.parser-combinators ==1.2.1, @@ -152,26 +146,25 @@ constraints: any.BoundedChan ==1.0.3.0, any.pretty ==1.1.3.6, any.pretty-hex ==1.1, any.pretty-show ==1.10, - any.prettyprinter ==1.6.1, + any.prettyprinter ==1.6.2, prettyprinter -buildreadme, - any.prettyprinter-ansi-terminal ==1.1.1.2, - any.primitive ==0.7.0.1, - any.process ==1.6.8.0, + any.prettyprinter-ansi-terminal ==1.1.2, + any.primitive ==0.7.1.0, + any.process ==1.6.9.0, any.profunctors ==5.5.2, any.quickcheck-io ==0.2.0, - any.random ==1.1, + any.random ==1.2.0, any.ref-tf ==0.4.0.2, any.reflection ==2.1.6, reflection -slow +template-haskell, any.regex-base ==0.94.0.0, any.regex-tdfa ==1.3.1.0, regex-tdfa -force-o2, - any.resourcet ==1.2.4, any.rts ==1.0, any.s-cargot ==0.1.4.0, s-cargot -build-example, any.s-cargot-letbind ==0.2.3.0, - any.scheduler ==1.4.2.2, + any.scheduler ==1.4.2.3, any.scientific ==0.3.6.2, scientific -bytestring-builder -integer-simple, any.semigroupoids ==5.3.4, @@ -179,10 +172,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.semigroups ==0.19.1, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.setenv ==0.1.1.3, - any.smallcheck ==1.1.5, + any.smallcheck ==1.2.0, any.split ==0.2.3.4, - any.splitmix ==0.0.4, - splitmix -optimised-mixer +random, + any.splitmix ==0.1.0.1, + splitmix -optimised-mixer, any.sqlite-simple ==0.4.18.0, any.stm ==2.5.0.0, any.syb ==0.7.1, @@ -190,22 +183,20 @@ constraints: any.BoundedChan ==1.0.3.0, tagged +deepseq +transformers, any.tasty ==1.3.1, tasty +clock, - any.tasty-expected-failure ==0.11.1.2, - any.tasty-golden ==2.3.3.3, + any.tasty-expected-failure ==0.12.1, + any.tasty-golden ==2.3.4, tasty-golden -build-example, - any.tasty-hedgehog ==1.0.0.2, any.tasty-hspec ==1.1.5.1, any.tasty-hunit ==0.10.0.2, any.tasty-quickcheck ==0.10.1.1, any.tasty-smallcheck ==0.8.1, any.template-haskell ==2.15.0.0, any.temporary ==1.3, - any.terminal-size ==0.3.2.1, any.terminfo ==0.4.1.4, any.text ==1.2.4.0, any.tf-random ==0.5, any.th-abstraction ==0.3.2.0, - any.th-lift ==0.8.1, + any.th-lift ==0.8.2, any.time ==1.9.3, any.transformers ==0.5.6.2, any.transformers-base ==0.4.5.2, @@ -221,20 +212,20 @@ constraints: any.BoundedChan ==1.0.3.0, unix-compat -old-time, any.unliftio ==0.2.13, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.10.0, + any.unordered-containers ==0.2.12.0, unordered-containers -debug, any.utf8-string ==1.0.1.1, any.vector ==0.12.1.2, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-sized ==1.4.1.0, + any.vector-sized ==1.4.2, any.versions ==3.5.4, any.void ==0.7.3, void -safe, any.wcwidth ==0.0.2, wcwidth -cli +split-base, - any.wl-pprint-annotated ==0.1.0.1, any.xml ==1.3.14, any.zenc ==0.1.1, - any.zlib ==0.6.2.1, - zlib -non-blocking-ffi -pkg-config, + any.zlib ==0.6.2.2, + zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2020-09-29T15:11:45Z diff --git a/cabal.project.werror b/cabal.project.werror new file mode 100644 index 00000000..ce74578f --- /dev/null +++ b/cabal.project.werror @@ -0,0 +1,8 @@ +package macaw-base + ghc-options: -Werror +package macaw-symbolic + ghc-options: -Werror +package macaw-x86 + ghc-options: -Werror +package macaw-x86-xsymbolic + ghc-options: -Werror