You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 GaloisInc/llvm-pretty-bc-parser#261):
$ 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 text was updated successfully, but these errors were encountered:
….assign
This adds `llvm.experimental.noalias.scope.decl` and `llvm.dbg.assign` to the
list of LLVM intrinsics that `crucible-llvm` skips over during simulation.
Doing so unlocks more support for recent LLVM versions.
It is conceivable that we may want to reason about these intrinsics at a deeper level some
day. If so, see:
* #1196 (comment) for
how this would be done for `llvm.experimental.noalias.scope.decl`
* #1204 (comment) for how
this would be done for `llvm.dbg.assign`
Fixes#1196. Fixes#1204.
….assign (#1205)
This adds `llvm.experimental.noalias.scope.decl` and `llvm.dbg.assign` to the
list of LLVM intrinsics that `crucible-llvm` skips over during simulation.
Doing so unlocks more support for recent LLVM versions.
It is conceivable that we may want to reason about these intrinsics at a deeper level some
day. If so, see:
* #1196 (comment) for
how this would be done for `llvm.experimental.noalias.scope.decl`
* #1204 (comment) for how
this would be done for `llvm.dbg.assign`
Fixes#1196. Fixes#1204.
The
llvm.dbg.assign
intrinsic was introduced in LLVM 16 and replaces thellvm.dbg.declare
intrinsic in LLVM 17. In order to support LLVM 17, we will need to teachcrucible-llvm
about it. For example,crux-llvm
will fail to process this program (when building on top of thellvm-pretty-bc-parser
changes from GaloisInc/llvm-pretty-bc-parser#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.assign
intrinsic, just like most otherllvm.dbg.*
intrinsics are skipped. If someone wants to reason about the contents ofllvm.dbg.assign
in 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_Assign
data constructor (similar to the existingLLVM_Dbg_Declare
data constructor). I don't have a need forLLVM_Dbg_Assign
just yet, so I propose not doing this until someone needs it.The text was updated successfully, but these errors were encountered: