Skip to content

fix: bitcast from ptr to <1 x ptr> - #1373

Merged
nunoplopes merged 1 commit into
AliveToolkit:masterfrom
pedroclobo:ptr-vector-bitcast
Oct 25, 2026
Merged

nunoplopes merged 1 commit into
AliveToolkit:masterfrom
pedroclobo:ptr-vector-bitcast

Conversation

@pedroclobo

@pedroclobo pedroclobo commented Oct 25, 2026 •

Copy link
Copy Markdown
Contributor

The following crashes Alive2 (https://alive2.llvm.org/ce/z/K86YU9):

define <1 x ptr> @src(ptr %p, ptr %v) {
  store ptr %v, ptr %p
  %l = load <1 x ptr>, ptr %p
  ret <1 x ptr> %l
}

define <1 x ptr> @tgt(ptr %p, ptr %v) {
  store ptr %v, ptr %p
  %l = bitcast ptr %v to <1 x ptr>
  ret <1 x ptr> %l
}

; Severe Z3 error: sort is not a bit-vector [code=3]

ConversionOp::toSMT treats every bitcast to a vector of pointers as a no-op, returning the operand unchanged. That holds for <N x ptr> -> <N x ptr>, but not for ptr -> <1 x ptr>.

This can be avoided by taking the shortcut only when the source is also a vector:

-    if (getType().isVectorType() &&
+    if (getType().isVectorType() && val->getType().isVectorType() &&
         getType().getAsAggregateType()->getChild(0).isPtrType())
       return v;

Found while working on llvm/llvm-project#235505.

@nunoplopes
nunoplopes merged commit adacbd5 into AliveToolkit:master Oct 25, 2026
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants