diff --git a/CHANGES.md b/CHANGES.md index e3d7b56f8d..e4518b8e1e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -99,7 +99,7 @@ see the `mir_*` commands documented in the [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). -* Support LLVM versions up to 14. +* Support LLVM versions up to 16. # Version 0.9 diff --git a/README.md b/README.md index 6d78db2fec..5f967bbde8 100644 --- a/README.md +++ b/README.md @@ -72,7 +72,7 @@ SAW can analyze LLVM programs (usually derived from C, but potentially for other languages). The only tool strictly required for this is a compiler that can generate LLVM bitcode, such as `clang`. However, having the full LLVM tool suite available can be useful. We have tested -SAW with LLVM and `clang` versions from 3.5 to 14.0, as well as the +SAW with LLVM and `clang` versions from 3.5 to 16.0, as well as the version of `clang` bundled with Apple Xcode. We welcome bug reports on any failure to parse bitcode from LLVM versions in that range. diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 3818a165ee..7f3965322a 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -18,8 +18,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -154,7 +153,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.6.1, any.ghci ==8.10.7, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -178,9 +176,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -220,7 +219,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -230,7 +229,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.1.2.2, @@ -242,7 +241,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -252,8 +251,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -297,17 +294,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -318,8 +314,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -331,11 +325,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -344,7 +338,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.4.1, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -418,4 +411,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z diff --git a/cabal.GHC-9.2.7.config b/cabal.GHC-9.2.7.config index 81c75892c2..d2e57716d1 100644 --- a/cabal.GHC-9.2.7.config +++ b/cabal.GHC-9.2.7.config @@ -18,8 +18,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -155,7 +154,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.8.0, any.ghci ==9.2.7, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -179,9 +177,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -221,7 +220,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -231,7 +230,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.2.0.1, @@ -243,7 +242,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -253,8 +252,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -298,17 +295,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -319,8 +315,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -332,11 +326,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.18.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -345,7 +339,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.5.0, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -419,4 +412,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z diff --git a/cabal.GHC-9.4.4.config b/cabal.GHC-9.4.4.config index 241bb28fce..5063584852 100644 --- a/cabal.GHC-9.4.4.config +++ b/cabal.GHC-9.4.4.config @@ -19,8 +19,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.adjunctions ==4.4.2, any.aeson ==2.1.2.1, aeson -cffi +ordered-keymap, - any.aeson-typescript ==0.5.0.0, - any.alex ==3.2.7.3, + any.alex ==3.2.7.4, any.ansi-terminal ==0.11.5, ansi-terminal -example, any.ansi-terminal-types ==0.11.5, @@ -119,7 +118,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.doctest ==0.20.1, any.dotgen ==0.4.3, dotgen -devel, - any.easy-file ==0.2.3, + any.easy-file ==0.2.5, any.either ==5.0.2, any.entropy ==0.4.1.10, entropy -donotgetentropy, @@ -140,7 +139,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.foldable1-classes-compat ==0.1, foldable1-classes-compat +tagged, any.free ==5.2, - any.generic-deriving ==1.14.3, + any.generic-deriving ==1.14.4, generic-deriving +base-4-9, any.generic-lens ==2.2.2.0, any.generic-lens-core ==2.2.1.0, @@ -155,7 +154,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.9.0, any.ghci ==9.4.4, - any.githash ==0.1.6.3, any.gitrev ==1.3.1, any.graphviz ==2999.20.1.0, graphviz -test-parsing, @@ -179,9 +177,10 @@ constraints: any.BoundedChan ==1.0.3.0, any.hpc ==0.6.1.0, any.hsc2hs ==0.68.9, hsc2hs -in-ghc-tree, - any.hspec ==2.10.10, - any.hspec-core ==2.10.10, - any.hspec-discover ==2.10.10, + any.hspec ==2.11.0.1, + any.hspec-api ==2.11.0.1, + any.hspec-core ==2.11.0.1, + any.hspec-discover ==2.11.0.1, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, @@ -221,7 +220,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.lifted-async ==0.10.2.4, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.8.0.0, + any.logict ==0.8.1.0, any.lucid ==2.11.20230408, any.lumberjack ==1.0.2.0, any.math-functions ==0.3.4.2, @@ -231,7 +230,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.memory ==0.18.0, memory +support_bytestring +support_deepseq, any.microlens ==0.4.13.1, - any.microlens-th ==0.4.3.12, + any.microlens-th ==0.4.3.13, any.microstache ==1.0.2.3, any.mmorph ==1.2.0, any.mod ==0.2.0.1, @@ -243,7 +242,7 @@ constraints: any.BoundedChan ==1.0.3.0, any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, any.mwc-random ==0.15.0.2, - any.network ==3.1.2.8, + any.network ==3.1.2.9, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.1, @@ -253,8 +252,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, - any.optparse-simple ==0.1.1.4, - optparse-simple -build-example, any.ordered-containers ==0.2.3, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, @@ -298,17 +295,16 @@ constraints: any.BoundedChan ==1.0.3.0, any.scotty ==0.12.1, any.semialign ==1.3, semialign +semigroupoids, - any.semigroupoids ==5.3.7, + any.semigroupoids ==6.0.0.1, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, any.semirings ==0.6, semirings +containers +unordered-containers, - any.setenv ==0.1.1.3, any.silently ==1.2.5.3, any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, + any.simple-sendfile ==0.2.31, + simple-sendfile +allow-bsd -fallback, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.5, @@ -319,8 +315,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.streaming-commons ==0.2.2.6, streaming-commons -use-bytestring-builder, any.strict ==0.5, - any.string-interpolate ==0.3.2.0, - string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.3, any.tagged ==0.8.7, tagged +deepseq +transformers, @@ -332,11 +326,11 @@ constraints: any.BoundedChan ==1.0.3.0, any.tasty-golden ==2.3.5, tasty-golden -build-example, any.tasty-hedgehog ==1.4.0.1, - any.tasty-hspec ==1.2.0.3, + any.tasty-hspec ==1.2.0.4, any.tasty-hunit ==0.10.0.3, any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==2.1.0.0, + any.tasty-sugar ==2.2.0.0, any.template-haskell ==2.19.0.0, any.temporary ==1.3, any.terminal-size ==0.3.3, @@ -345,7 +339,6 @@ constraints: any.BoundedChan ==1.0.3.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==2.0.1, - any.text-conversions ==0.3.1.1, any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, @@ -419,4 +412,4 @@ constraints: any.BoundedChan ==1.0.3.0, any.zlib ==0.6.3.0, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2023-04-18T11:48:49Z +index-state: hackage.haskell.org 2023-05-08T16:29:53Z diff --git a/deps/crucible b/deps/crucible index b4422dd2f7..b146bcf77a 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit b4422dd2f75f5a7310bc038a6ca67a91f3692a42 +Subproject commit b146bcf77a8c69ea389e738f541eef91d4e98293 diff --git a/deps/llvm-pretty b/deps/llvm-pretty index d099d5d0fe..a454fcbe41 160000 --- a/deps/llvm-pretty +++ b/deps/llvm-pretty @@ -1 +1 @@ -Subproject commit d099d5d0feab8066bc682f11c8a46c82fb7166b5 +Subproject commit a454fcbe4192c07bcced2cf1384686dc7359a4a3 diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index 59e6991e1b..65be0b0e38 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 59e6991e1b89252d4a4aa28a84ab1ac022c18b8d +Subproject commit 65be0b0e3898716b1e39659f3d3d49dcc5208d31 diff --git a/deps/what4 b/deps/what4 index ffbad75b1c..2d22d4afaf 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit ffbad75b1ce65577422a19a30a39a5059be8b95f +Subproject commit 2d22d4afaf141195bd4a43a9e5498c2b2e7eaa3d diff --git a/doc/manual/manual.md b/doc/manual/manual.md index b6c9727fd0..4dab9d048a 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1580,7 +1580,7 @@ The resulting `LLVMModule` can be passed into the various functions described below to perform analysis of specific LLVM functions. The LLVM bitcode parser should generally work with LLVM versions between -3.5 and 14.0, though it may be incomplete for some versions. Debug +3.5 and 16.0, though it may be incomplete for some versions. Debug metadata has changed somewhat throughout that version range, so is the most likely case of incompleteness. We aim to support every version after 3.5, however, so report any parsing failures as [on diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 6df257516b..f470783359 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -178,34 +178,44 @@ translateLLVMType _ tp = -- | Helper function for 'translateLLVMValue' applied to a constant expression translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) -translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr : ixs)) = +translateLLVMConstExpr w (L.ConstGEP _ _ _ (L.Typed tp ptr) ixs) = translateLLVMValue w tp ptr >>= \ptr_trans -> translateLLVMGEP w tp ptr_trans ixs translateLLVMConstExpr w (L.ConstConv L.BitCast - (L.Typed tp@(L.PtrTo _) v) (L.PtrTo _)) = - -- A bitcast from one LLVM pointer type to another is a no-op for us - translateLLVMValue w tp v + (L.Typed fromTp v) toTp) + | L.isPointer fromTp && L.isPointer toTp + = -- A bitcast from one LLVM pointer type to another is a no-op for us + translateLLVMValue w fromTp v translateLLVMConstExpr _ ce = traceAndZeroM ("translateLLVMConstExpr does not yet handle:\n" ++ ppLLVMConstExpr ce) --- | Helper function for 'translateLLVMValue' applied to a @getelemptr@ --- expression +-- | Helper function for 'translateLLVMValue' applied to a constant +-- @getelementptr@ expression. +-- +-- For now, we only support uses of @getelementptr@ where all indices are zero, +-- as this will return the pointer argument without needing to compute an offset +-- into the pointer. Of course, this does mean that any @getelementptr@ +-- expressions involving non-zero indices aren't supported (see #1875 for a +-- contrived example of this). Thankfully, this function is only used to +-- translate LLVM globals, and using @getelementptr@ to initialize globals is +-- quite rare in practice. As such, we choose to live with this limitation until +-- someone complains about it. translateLLVMGEP :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> (PermExpr (LLVMShapeType w), OpenTerm) -> [L.Typed L.Value] -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) -translateLLVMGEP _ _ vtrans [] = return vtrans -translateLLVMGEP w (L.Array _ tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP w (L.PtrTo tp) vtrans (L.Typed _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP w (L.PackedStruct [tp]) vtrans (L.Typed - _ (L.ValInteger 0) : ixs) = - translateLLVMGEP w tp vtrans ixs -translateLLVMGEP _ tp _ ixs = - traceAndZeroM ("translateLLVMGEP cannot handle arguments:\n" ++ - " " ++ intercalate "," (show tp : map show ixs)) +translateLLVMGEP _ tp vtrans ixs + | all (isZeroIdx . L.typedValue) ixs + = return vtrans + | otherwise + = traceAndZeroM ("translateLLVMGEP cannot handle arguments:\n" ++ + " " ++ intercalate "," (show tp : map show ixs)) + where + -- Check if an index is equal to 0. + isZeroIdx :: L.Value -> Bool + isZeroIdx (L.ValInteger 0) = True + isZeroIdx _ = False -- | Build an LLVM value for a @zeroinitializer@ field of the supplied type llvmZeroInitValue :: L.Type -> LLVMTransM (L.Value) diff --git a/intTests/test1132-opaque/Makefile b/intTests/test1132-opaque/Makefile new file mode 100644 index 0000000000..a639efae03 --- /dev/null +++ b/intTests/test1132-opaque/Makefile @@ -0,0 +1,13 @@ +# NB: Ensure that clang-15 or later is used so that the resulting LLVM bitcode +# uses opaque pointers. +CC = clang +CFLAGS = -g -emit-llvm -frecord-command-line -O0 + +all: test.bc + +test.bc: test.c + $(CC) $(CFLAGS) -c $< -o $@ + +.PHONY: clean +clean: + rm -f test.bc diff --git a/intTests/test1132-opaque/test.bc b/intTests/test1132-opaque/test.bc new file mode 100644 index 0000000000..57dd28b8f4 Binary files /dev/null and b/intTests/test1132-opaque/test.bc differ diff --git a/intTests/test1132-opaque/test.c b/intTests/test1132-opaque/test.c new file mode 100644 index 0000000000..a02777bd88 --- /dev/null +++ b/intTests/test1132-opaque/test.c @@ -0,0 +1,7 @@ +#include +#include + +void f(uint8_t **x) { + *x = malloc(sizeof(uint8_t)); + **x = 42; +} diff --git a/intTests/test1132-opaque/test.saw b/intTests/test1132-opaque/test.saw new file mode 100644 index 0000000000..91d5afa1cf --- /dev/null +++ b/intTests/test1132-opaque/test.saw @@ -0,0 +1,11 @@ +bc <- llvm_load_module "test.bc"; + +let f_contract = do { + x <- llvm_alloc (llvm_pointer (llvm_int 8)); + llvm_execute_func [x]; + p <- llvm_alloc (llvm_int 8); + llvm_points_to x p; + llvm_points_to p (llvm_term {{ 42 : [8] }}); +}; + +llvm_verify bc "f" [] false f_contract abc; diff --git a/intTests/test1132-opaque/test.sh b/intTests/test1132-opaque/test.sh new file mode 100644 index 0000000000..06d9f2a4ae --- /dev/null +++ b/intTests/test1132-opaque/test.sh @@ -0,0 +1,5 @@ +# A variant of test1132 that instead uses opaque pointers to ensure that the +# basics of SAW work in an opaque pointer context. +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index aa8591b13a..3ddc66f29b 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -2124,15 +2124,24 @@ cryptolTypeOfActual dl mt = do cty <- cryptolTypeOfActual dl ty return $ Cryptol.tSeq (Cryptol.tNum n) cty Crucible.PtrType _ -> - return $ Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl)) + return cryptolPtrType + Crucible.PtrOpaqueType -> + return cryptolPtrType Crucible.StructType si -> do let memtypes = V.toList (Crucible.siFieldTypes si) ctys <- traverse (cryptolTypeOfActual dl) memtypes case ctys of [cty] -> return cty _ -> return $ Cryptol.tTuple ctys - _ -> + Crucible.X86_FP80Type -> Nothing + Crucible.VecType{} -> + Nothing + Crucible.MetadataType -> + Nothing + where + cryptolPtrType :: Cryptol.Type + cryptolPtrType = Cryptol.tWord (Cryptol.tNum (Crucible.ptrBitwidth dl)) -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. @@ -2227,6 +2236,13 @@ constructExpandedSetupValue cc sc loc t = Crucible.MetadataType -> failUnsupportedType "Metadata" Crucible.VecType{} -> failUnsupportedType "Vec" Crucible.X86_FP80Type{} -> failUnsupportedType "X86_FP80" + -- See https://github.com/GaloisInc/saw-script/issues/1879 for why it is + -- tricky to support opaque pointers here. + Crucible.PtrOpaqueType -> + panic "SAWScript.Crucible.LLVM.Builtins.constructExpandedSetupValue" + [ "llvm_fresh_expanded_val does not support opaque pointers" + , "Please report this at: https://github.com/GaloisInc/saw-script/issues/1879" + ] where failUnsupportedType tyName = throwCrucibleSetup loc $ unwords ["llvm_fresh_expanded_var: " ++ tyName ++ " not supported"] diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 6c9359aaa5..d193f73864 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1241,9 +1241,15 @@ diffMemTypes x0 y0 = (Crucible.IntType x, Crucible.IntType y) | x == y -> [] (Crucible.FloatType, Crucible.FloatType) -> [] (Crucible.DoubleType, Crucible.DoubleType) -> [] - (Crucible.PtrType{}, Crucible.PtrType{}) -> [] - (Crucible.IntType w, Crucible.PtrType{}) | w == wptr -> [] - (Crucible.PtrType{}, Crucible.IntType w) | w == wptr -> [] + (_, _) + | Crucible.isPointerMemType x0 && Crucible.isPointerMemType y0 -> + [] + (Crucible.IntType w, _) + | Crucible.isPointerMemType y0 && w == wptr -> + [] + (_, Crucible.IntType w) + | Crucible.isPointerMemType x0 && w == wptr -> + [] (Crucible.ArrayType xn xt, Crucible.ArrayType yn yt) | xn == yn -> [ (Nothing : path, l , r) | (path, l, r) <- diffMemTypes xt yt ] @@ -1314,7 +1320,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = (V.toList (Crucible.fiType <$> Crucible.siFields fields)) zs ] - (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupElem () v i) -> + (Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy -> do let tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs delta <- exceptToFail $ resolveSetupElemOffset cc tyenv nameEnv v i @@ -1322,7 +1328,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = =<< W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToBV (W4.bvWidth off) delta) matchArg opts sc cc cs prepost md (Crucible.LLVMValInt blk off') expectedTy v - (Crucible.LLVMValInt blk off, Crucible.PtrType _, SetupField () v n) -> + (Crucible.LLVMValInt blk off, _, SetupField () v n) | Crucible.isPointerMemType expectedTy -> do let tyenv = MS.csAllocations cs nameEnv = MS.csTypeNames cs fld <- exceptToFail $ diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index c9d7647ddc..9223c5b909 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -473,8 +473,8 @@ typeOfSetupValue cc env nameEnv val = SetupCast () v ltp -> do memTy <- typeOfSetupValue cc env nameEnv v - case memTy of - Crucible.PtrType _symTy -> + if Crucible.isPointerMemType memTy + then case let ?lc = lc in Crucible.liftMemType (L.PtrTo ltp) of Left err -> throwError $ unlines [ "typeOfSetupValue: invalid type " ++ show ltp @@ -483,10 +483,11 @@ typeOfSetupValue cc env nameEnv val = ] Right mt -> pure mt - _ -> throwError $ unwords $ - [ "typeOfSetupValue: tried to cast the type of a non-pointer value" - , "actual type of value: " ++ show memTy - ] + else + throwError $ unwords $ + [ "typeOfSetupValue: tried to cast the type of a non-pointer value" + , "actual type of value: " ++ show memTy + ] SetupElem () v i -> do do memTy <- typeOfSetupValue cc env nameEnv v diff --git a/src/SAWScript/Crucible/LLVM/Skeleton.hs b/src/SAWScript/Crucible/LLVM/Skeleton.hs index d55d5cf71b..d9c2b22df5 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton.hs @@ -39,6 +39,8 @@ import qualified Data.Set as Set import qualified Text.LLVM as LLVM import qualified Text.LLVM.DebugUtils as LLVM +import SAWScript.Panic (panic) + -------------------------------------------------------------------------------- -- ** Skeletons @@ -98,6 +100,14 @@ makeLenses ''ModuleSkeleton parseType :: LLVM.Type -> IO TypeSkeleton parseType (LLVM.PtrTo t) = pure $ TypeSkeleton t True [SizeGuess 1 True "default guess of size 1"] +-- It is unclear how to combine opaque pointers with type skeletons due to the +-- lack of a pointee type. For now, we simply fail if we encounter one +-- (see #1877). +parseType LLVM.PtrOpaque = + panic "SAWScript.Crucible.LLVM.Skeleton.parseType" + [ "Skeleton generation does not support opaque pointers" + , "Please report this at: https://github.com/GaloisInc/saw-script/issues/1877" + ] parseType (LLVM.Array i t) = pure $ TypeSkeleton t True [ SizeGuess (fromIntegral i) True $ "default guess of size " <> Text.pack (show i) ] diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 5c2e738a84..8cadba3856 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -1158,7 +1158,7 @@ setArgs env tyenv nameEnv args let setRegSetupValue rs (reg, sval) = exceptToFail (typeOfSetupValue cc tyenv nameEnv sval) >>= \case - C.LLVM.PtrType _ -> do + ty | C.LLVM.isPointerMemType ty -> do val <- C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) =<< resolveSetupVal cc mem env tyenv nameEnv sval setReg reg val rs