AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
721 stars 93 forks source link

arm-tv bug that won't repro in alive-tv #1013

Closed regehr closed 5 months ago

regehr commented 5 months ago

so all along I've been careful to keep a clean separation between the ARM lifter and Alive2, so that problems I run into can repro in alive-tv. but now I'm having a problem where alive-tv is fine with this IR but the ARM lifter is not:

; ModuleID = 'reduced.bc'
target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
target triple = "arm64-apple-macosx14.0.0"

; Function Attrs: strictfp
define ptr @src() #0 {
entry:
  %call = call ptr @png_create_write_struct_2()
  ret ptr %call
}

define ptr @tgt() local_unnamed_addr #0 {
arm_tv_entry:
  %0 = tail call ptr @png_create_write_struct_2()
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  tail call void @llvm.assert(i1 true)
  ret ptr %0
}

; Function Attrs: strictfp
declare noalias ptr @png_create_write_struct_2() #0

attributes #0 = { strictfp }

here's the final part of the output:

----------------------------------------
declare ptr @png_create_write_struct_2() noalias

define ptr @src() {
entry:
  %call = call ptr @png_create_write_struct_2() noalias
  ret ptr %call
}
=>
declare ptr @png_create_write_struct_2()

define ptr @src() asm {
arm_tv_entry:
  %#0 = call ptr @png_create_write_struct_2()
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  assume i1 1
  ret ptr %#0
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:

Source:
ptr %call = null

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 1    alloc type: 0   alive: false    address: 0
Block 1 >   size: 2 align: 1    alloc type: 0   alive: true address: 0
Contents:
*: #x00

LOCAL BLOCKS:
Block 2 >   size: 0 align: 1    alloc type: 2   alive: true

Target:
ptr %#0 = null
Source value: null
Target value: null

done comparing functions
Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

now obviously I don't expect you to be able to debug something you can't repro, but does anything suggest itself here? some kind of mistake I could be making that triggers this behavior? ugh!!!!

nunoplopes commented 5 months ago

There's a mismatch in the input IR you give and the alive2 report. In the IR, the noalias attribute is in the decl of @png_create_write_struct_2. But in the output, the attribute is in the function call of the source only. The target doesn't have the attribute.

The easiest solution is to propagate the noalias attribute to the tgt decls. It's something you can't read from assembly, but it has to preserve this property anyway.

regehr commented 5 months ago

ack!! thanks. sorry to bother.