Adapt to ConstGEP gaining explicit basis type and expression

This commit bumps the `llvm-pretty` submodule to bring in a commit from GaloisInc/llvm-pretty#110 that adds additional fields to `ConstGEP` to represent the basis type and expression to use for offset calculations. This also bumps the `llvm-pretty-bc-parser` and `crucible` submodule to bring in corresponding changes from GaloisInc/llvm-pretty-bc-parser#221 and GaloisInc/crucible#1085, respectively. This change affects one use site in `heapster-saw`, which is easily adapted.
GaloisInc · Jun 16, 2023 · fdd6366 · fdd6366
1 parent c5301b0
commit fdd6366
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs
@@ -178,7 +178,7 @@ 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
+1 −1		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
+6 −6		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs
+6 −6		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+2 −0		crux-llvm/crux-llvm.cabal
+4 −4		crux-llvm/test-data/golden/abd-test-file-32.cvc5.good
+0 −9		crux-llvm/test-data/golden/abd-test-file-32.pre-clang13.cvc5.good
+4 −4		crux-llvm/test-data/golden/abd-test-file-8.cvc5.good
+3 −3		crux-llvm/test-data/golden/abd-test-maxint-32.cvc5.good
+4 −4		crux-llvm/test-data/golden/abd-test-trans-8.cvc5.good
+50 −1		crux-llvm/test/Test.hs
+13 −3		crux/src/Crux/FormatOut.hs
+1 −1		dependencies/llvm-pretty
+1 −1		dependencies/llvm-pretty-bc-parser
+20 −1		uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+104 −107		disasm-test/Main.hs
+45 −0		disasm-test/README.md
+0 −0		disasm-test/tests/btf-tag-dicompositetype.ll
+1 −0		disasm-test/tests/btf-tag-dicompositetype.pre-llvm14.ll
+0 −0		disasm-test/tests/btf-tag-diderivedtype.ll
+1 −0		disasm-test/tests/btf-tag-diderivedtype.pre-llvm14.ll
+0 −0		disasm-test/tests/btf-tag-diglobalvariable.ll
+1 −0		disasm-test/tests/btf-tag-diglobalvariable.pre-llvm14.ll
+0 −0		disasm-test/tests/btf-tag-dilocalvariable.ll
+1 −0		disasm-test/tests/btf-tag-dilocalvariable.pre-llvm14.ll
+0 −0		disasm-test/tests/btf-tag-disubprogram.ll
+1 −0		disasm-test/tests/btf-tag-disubprogram.pre-llvm14.ll
+0 −0		disasm-test/tests/di-arg-list.ll
+1 −0		disasm-test/tests/di-arg-list.pre-llvm13.ll
+0 −0		disasm-test/tests/dilocalvariable.ll
+1 −0		disasm-test/tests/dilocalvariable.pre-llvm14.ll
+0 −0		disasm-test/tests/poison.ll
+1 −0		disasm-test/tests/poison.pre-llvm12.ll
+1 −1		llvm-pretty
+3 −2		llvm-pretty-bc-parser.cabal
+55 −19		src/Data/LLVM/BitCode/IR/Constants.hs
+13 −12		src/Data/LLVM/BitCode/IR/Function.hs