Translation failure on rustc-produced LLVM bitcode

[langston-barrett]

Crucible-LLVM runs into a translation error on some rustc-produced LLVM bitcode:

use std::alloc::{Layout, dealloc};

#[inline(never)]
#[no_mangle]
pub fn free(p: *mut usize) {
    unsafe {
        dealloc(p.cast(), Layout::new::<usize>());
    }
}

#[inline(never)]
#[no_mangle]
pub fn test(p: *mut usize, x: usize) {
    if x > 0 && x < 10 && x % 2 == 0 {
        free(p);
    }
    if x % 3 == 0 {
        free(p);
    }
}

fn main() { 
    test(Box::leak(Box::new(5)), 7);
}

rustc --version --verbose

rustc 1.79.0 (129f3b996 2024-06-10)
binary: rustc
commit-hash: 129f3b9964af4d4a709d1383930ade12dfe7c081
commit-date: 2024-06-10
host: x86_64-unknown-linux-gnu
release: 1.79.0
LLVM version: 18.1.7

rustc --emit=llvm-bc double-free.rs

internal: error: in test
Arithmetic comparison on incompatible values
Comparison operation: Iugt
Value 1: $1
Value 2: extensionApp(pointerExpr natLit(0) bVLit(64, BV 0))

Here's the bitcode for @test:

; Function Attrs: noinline nonlazybind uwtable
define dso_local void @test(ptr %p, i64 %x) unnamed_addr #0 {
start:
  %_3 = icmp ugt i64 %x, 0
  br i1 %_3, label %bb1, label %bb5

bb5:                                              ; preds = %bb4, %bb2, %bb1, %start
  %_8 = urem i64 %x, 3
  %0 = icmp eq i64 %_8, 0
  br i1 %0, label %bb7, label %bb8

bb1:                                              ; preds = %start
  %_4 = icmp ult i64 %x, 10
  br i1 %_4, label %bb2, label %bb5

bb2:                                              ; preds = %bb1
  %_5 = urem i64 %x, 2
  %1 = icmp eq i64 %_5, 0
  br i1 %1, label %bb4, label %bb5

bb4:                                              ; preds = %bb2
  call void @free(ptr %p)
  br label %bb5

bb7:                                              ; preds = %bb5
  call void @free(ptr %p)
  br label %bb8

bb8:                                              ; preds = %bb7, %bb5
  ret void
}

And the bitcode itself: double-free.zip

[RyanGlScott]

Is it possible to reproduce this error using crux-llvm?

[langston-barrett]

Hmm, evidently not. I tried adding an entrypoint foo as follows:

#[inline(never)]
#[no_mangle]
pub fn foo() {
    test(&mut 5, 7);
}

; Function Attrs: noinline nonlazybind uwtable
define dso_local void @foo() unnamed_addr #0 {
start:
  %_4 = alloca [8 x i8], align 8
  store i64 5, ptr %_4, align 8
  call void @test(ptr %_4, i64 7)
  ret void
}

but got

cabal run exe:crux-llvm -- --no-compile prog.bc --entry-point=foo

[Crux] Using pointer width: 64 for file prog.bc
[Crux] Simulating function foo
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.