Skip to content

initializes causes severe Z3 error #1220

@pedroclobo

Description

@pedroclobo

The following reduced test causes Alive to crash:

declare void @llvm.memset.p0.i64(ptr writeonly captures(none), i8, i64, i1 immarg)

define void @src(ptr initializes((0, 24), (40, 48), (56, 64)) %pReadr) {
entry:
  %0 = load ptr, ptr null, align 8
  call void @llvm.memset.p0.i64(ptr align 8 null, i8 0, i64 80, i1 false)
  ret void
}

define void @tgt(ptr initializes((0, 24), (40, 48), (56, 64)) %pReadr) {
entry:
  call void @llvm.memset.p0.i64(ptr align 8 null, i8 0, i64 80, i1 false)
  ret void
}
Severe Z3 error: Argument #x08 at position 1 has sort (_ BitVec 8) it does not match declaration (declare-fun bvudiv ((_ BitVec 5) (_ BitVec 5)) (_ BitVec 5)) [code=12]

Removing the initializes prevents the crash.

Found while running alivecc on sqlite3 amalgamation.

./alivecc -c -O2 ./sqlite3.c -mllvm -tv-quiet -mllvm -tv-disable-undef-input -mllvm -tv-func=vdbePmaReaderClear

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions