The llvm.dbg.assign intrinsic was introduced in LLVM 16 and replaces the llvm.dbg.declare intrinsic in LLVM 17. In order to support LLVM 17, we will need to teach crucible-llvm about it. For example, crux-llvm will fail to process this program (when building on top of the llvm-pretty-bc-parser changes from https://github.com/GaloisInc/llvm-pretty-bc-parser/pull/261):
__attribute__((noinline)) int foo(int x[2]) {
return x[0];
}
int main(void) {
int x[2] = { 0, 0 };
return foo(x);
}
$ PATH=~/Software/clang+llvm-17.0.2/bin:$PATH cabal run exe:crux-llvm -- test.c
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-0
[Crux] *** break on line: 0
[Crux] Found counterexample for verification goal
[Crux] test.c:0:0: error: in main
[Crux] unsupported LLVM value: ValMd (ValMdValue (Typed {typedType = PrimType (Integer 1), typedValue = ValUndef})) of type metadata
[Crux] Goal status:
[Crux] Total: 1
[Crux] Proved: 0
[Crux] Disproved: 1
[Crux] Incomplete: 0
[Crux] Unknown: 0
[Crux] Overall status: Invalid.
In order to make this work, we need to alter the special-casing for llvm.dbg.* intrinsics here. For now, it will suffice to skip calls to llvm.dbg.assign intrinsic, just like most other llvm.dbg.* intrinsics are skipped. If someone wants to reason about the contents of llvm.dbg.assign in a way similar to how other code reasons about llvm.dbg.declare (e.g., how it's done in SAW here), then someone will need to add an LLVM_Dbg_Assign data constructor (similar to the existing LLVM_Dbg_Declare data constructor). I don't have a need for LLVM_Dbg_Assign just yet, so I propose not doing this until someone needs it.
The
llvm.dbg.assignintrinsic was introduced in LLVM 16 and replaces thellvm.dbg.declareintrinsic in LLVM 17. In order to support LLVM 17, we will need to teachcrucible-llvmabout it. For example,crux-llvmwill fail to process this program (when building on top of thellvm-pretty-bc-parserchanges from https://github.com/GaloisInc/llvm-pretty-bc-parser/pull/261):In order to make this work, we need to alter the special-casing for
llvm.dbg.*intrinsics here. For now, it will suffice to skip calls tollvm.dbg.assignintrinsic, just like most otherllvm.dbg.*intrinsics are skipped. If someone wants to reason about the contents ofllvm.dbg.assignin a way similar to how other code reasons aboutllvm.dbg.declare(e.g., how it's done in SAW here), then someone will need to add anLLVM_Dbg_Assigndata constructor (similar to the existingLLVM_Dbg_Declaredata constructor). I don't have a need forLLVM_Dbg_Assignjust yet, so I propose not doing this until someone needs it.