#[cfg_attr(coverage_nightly, coverage(off))]
#[cfg(test)]
mod cb060_falsification {
use super::*;
#[test]
fn tp_031_ptx_bra_before_barrier_simple() {
let ptx = r#"
setp.ge.u32 %p0, %r5, %r7;
@%p0 bra exit;
bar.sync 0;
"#;
let violations = detect_ptx_barrier_divergence_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed simple barrier divergence"
);
}
#[test]
fn tp_032_ptx_bra_before_barrier_multiline() {
let ptx = r#"
@%p0 bra skip_section;
mov.u32 %r1, 0;
mov.u32 %r2, 0;
mov.u32 %r3, 0;
mov.u32 %r4, 0;
bar.sync 0;
skip_section:
"#;
let violations = detect_ptx_barrier_divergence_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed barrier divergence with intervening code"
);
}
#[test]
fn tp_033_wgsl_barrier_in_if() {
let wgsl = r#"
if (local_id.x < 16u) {
workgroupBarrier();
}
"#;
let violations = detect_wgsl_barrier_divergence_in_str(wgsl);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed WGSL barrier in if"
);
}
#[test]
fn tp_034_wgsl_barrier_in_else() {
let wgsl = r#"
if (condition) {
// no barrier
} else {
workgroupBarrier();
}
"#;
let violations = detect_wgsl_barrier_divergence_in_str(wgsl);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed WGSL barrier in else"
);
}
#[test]
fn tn_035_ptx_barrier_before_branch() {
let ptx = r#"
bar.sync 0;
setp.ge.u32 %p0, %r5, %r7;
@%p0 bra exit;
"#;
let violations = detect_ptx_barrier_divergence_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Barrier before branch flagged"
);
}
#[test]
fn tn_036_wgsl_barrier_outside_control_flow() {
let wgsl = r#"
workgroupBarrier();
if (condition) {
// no barrier here
}
workgroupBarrier();
"#;
let violations = detect_wgsl_barrier_divergence_in_str(wgsl);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Non-divergent barrier flagged"
);
}
#[test]
fn edge_037_ptx_barrier_in_comment() {
let ptx = r#"
// bar.sync 0; -- this is a comment
@%p0 bra exit;
"#;
let violations = detect_ptx_barrier_divergence_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Barrier in comment flagged"
);
}
#[test]
fn edge_038_ptx_nested_predicates() {
let ptx = r#"
@%p0 bra check1;
@%p1 bra check2;
bar.sync 0;
check1:
check2:
"#;
let violations = detect_ptx_barrier_divergence_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed nested predicate divergence"
);
}
#[test]
fn edge_039_wgsl_barrier_in_loop() {
let wgsl = r#"
for (var i = 0u; i < 4u; i++) {
workgroupBarrier();
}
"#;
let violations = detect_wgsl_barrier_divergence_in_str(wgsl);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Barrier in uniform loop flagged"
);
}
#[test]
fn edge_040_wgsl_barrier_in_divergent_loop() {
let wgsl = r#"
for (var i = 0u; i < local_id.x; i++) {
workgroupBarrier();
}
"#;
let violations = detect_wgsl_barrier_divergence_in_str(wgsl);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed barrier in divergent loop"
);
}
#[test]
fn tp_041_unbounded_shared_load() {
let ptx = r#"
mul.u32 %r10, %r5, 64;
ld.shared.f32 %f1, [%r10];
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed unbounded shared memory load"
);
}
#[test]
fn tp_042_unbounded_shared_store() {
let ptx = r#"
mul.u32 %r10, %r5, 64;
st.shared.f32 [%r10], %f1;
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed unbounded shared memory store"
);
}
#[test]
fn tn_043_bounded_shared_load() {
let ptx = r#"
setp.lt.u32 %p1, %r5, 256;
@%p1 ld.shared.f32 %f1, [%r10];
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Bounded shared load flagged"
);
}
#[test]
fn tn_044_shared_with_constant_offset() {
let ptx = r#"
ld.shared.f32 %f1, [shared_mem + 128];
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Constant offset flagged"
);
}
#[test]
fn edge_045_shared_in_comment() {
let ptx = r#"
// ld.shared.f32 %f1, [%r10]; -- commented out
mov.f32 %f1, 0.0;
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Commented shared access flagged"
);
}
#[test]
fn edge_046_shared_complex_index() {
let ptx = r#"
mad.lo.u32 %r10, %r5, 64, %r6;
add.u32 %r10, %r10, %r7;
ld.shared.f32 %f1, [%r10];
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed complex index without bounds"
);
}
#[test]
fn edge_047_shared_bounds_far_apart() {
let ptx = r#"
setp.lt.u32 %p1, %r5, 256;
mov.u32 %r10, 0;
mov.u32 %r11, 0;
mov.u32 %r12, 0;
mul.u32 %r13, %r5, 64;
@%p1 ld.shared.f32 %f1, [%r13];
"#;
let violations = detect_shared_memory_unbounded_in_str(ptx);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Distant bounds check not recognized"
);
}
#[test]
fn tp_048_tiled_no_boundary_check() {
let rust_code = r#"
// Tiled GEMM kernel
for tile in 0..k_tiles {
// Load A tile - no bounds check for m < tile_size
let a_elem = a_smem[local_row * TILE_K + k];
let b_elem = b_smem[k * TILE_N + local_col];
acc += a_elem * b_elem;
}
// Store without checking row < m && col < n
c[row * n + col] = acc;
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed tiled kernel without bounds"
);
}
#[test]
fn tn_049_tiled_with_boundary_check() {
let rust_code = r#"
// Tiled GEMM with proper bounds
for tile in 0..k_tiles {
let a_elem = a_smem[local_row * TILE_K + k];
let b_elem = b_smem[k * TILE_N + local_col];
acc += a_elem * b_elem;
}
// Proper bounds check before store
if row < m && col < n {
c[row * n + col] = acc;
}
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Properly bounded tiled kernel flagged"
);
}
#[test]
fn tp_050_ptx_tiled_early_exit() {
let ptx = r#"
setp.ge.u32 %p0, %r_row, %r_m;
@%p0 bra exit;
setp.ge.u32 %p1, %r_col, %r_n;
@%p1 bra exit;
// Tile loop starts here
tile_loop:
ld.shared.f32 %f1, [smem_a];
bar.sync 0;
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(ptx);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed early exit before tile loop"
);
}
#[test]
fn edge_051_wgsl_tiled_workgroup_size() {
let wgsl = r#"
@workgroup_size(32, 32)
fn tiled_matmul() {
// No bounds check
let a_tile = a[global_id.y * K + local_id.x];
}
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(wgsl);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed WGSL tiled without bounds"
);
}
#[test]
fn edge_052_partial_bounds_check() {
let rust_code = r#"
if row < m {
// Missing: && col < n
c[row * n + col] = acc;
}
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
!violations.is_empty(),
"FALSIFIED: Missed partial bounds check"
);
}
#[test]
fn edge_053_bounds_in_wrong_place() {
let rust_code = r#"
c[row * n + col] = acc;
if row < m && col < n {
// Too late!
}
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
!violations.is_empty(),
"FALSIFIED: Accepted bounds check after store"
);
}
#[test]
fn edge_054_tiled_in_string() {
let rust_code = r#"
let kernel_src = "c[row * n + col] = acc;";
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Kernel code in string flagged"
);
}
#[test]
fn edge_055_complex_bounds_expression() {
let rust_code = r#"
if (row * stride + offset) < (m * stride) && col < n {
c[row * n + col] = acc;
}
"#;
let violations = detect_tiled_kernel_no_bounds_in_str(rust_code);
assert!(
violations.is_empty(),
"FALSIFIED (FP): Complex bounds expression not recognized"
);
}
}