diff --git a/loom-core/src/fused_optimizer.rs b/loom-core/src/fused_optimizer.rs index eb11a32..1284ab0 100644 --- a/loom-core/src/fused_optimizer.rs +++ b/loom-core/src/fused_optimizer.rs @@ -571,26 +571,24 @@ fn adapter_uses_single_memory(instructions: &[Instruction], expected_mem: u32) - | Instruction::I32Store16 { mem, .. } | Instruction::I64Store8 { mem, .. } | Instruction::I64Store16 { mem, .. } - | Instruction::I64Store32 { mem, .. } => { - if *mem != expected_mem { - return false; - } + | Instruction::I64Store32 { mem, .. } + if *mem != expected_mem => + { + return false; } - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if !adapter_uses_single_memory(body, expected_mem) { - return false; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if !adapter_uses_single_memory(body, expected_mem) => + { + return false; } Instruction::If { then_body, else_body, .. - } => { - if !adapter_uses_single_memory(then_body, expected_mem) - || !adapter_uses_single_memory(else_body, expected_mem) - { - return false; - } + } if (!adapter_uses_single_memory(then_body, expected_mem) + || !adapter_uses_single_memory(else_body, expected_mem)) => + { + return false; } _ => {} } diff --git a/loom-core/src/lib.rs b/loom-core/src/lib.rs index 6fa8f8c..5cac1ce 100644 --- a/loom-core/src/lib.rs +++ b/loom-core/src/lib.rs @@ -6614,21 +6614,19 @@ pub mod optimize { for instr in instructions { match instr { // Recursively check nested blocks - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if has_unsupported_isle_instructions_in_block(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if has_unsupported_isle_instructions_in_block(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if has_unsupported_isle_instructions_in_block(then_body) - || has_unsupported_isle_instructions_in_block(else_body) - { - return true; - } + } if (has_unsupported_isle_instructions_in_block(then_body) + || has_unsupported_isle_instructions_in_block(else_body)) => + { + return true; } // Unknown instructions (opaque — cannot model stack effects) @@ -6699,21 +6697,19 @@ pub mod optimize { for instr in instructions { match instr { Instruction::BrIf { .. } | Instruction::BrTable { .. } => return true, - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if has_dataflow_unsafe_control_flow_in_block(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if has_dataflow_unsafe_control_flow_in_block(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if has_dataflow_unsafe_control_flow_in_block(then_body) - || has_dataflow_unsafe_control_flow_in_block(else_body) - { - return true; - } + } if (has_dataflow_unsafe_control_flow_in_block(then_body) + || has_dataflow_unsafe_control_flow_in_block(else_body)) => + { + return true; } _ => {} } @@ -7355,20 +7351,18 @@ pub mod optimize { } // Recursively check nested structures - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if contains_branches(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if contains_branches(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if contains_branches(then_body) || contains_branches(else_body) { - return true; - } + } if (contains_branches(then_body) || contains_branches(else_body)) => { + return true; } _ => {} @@ -7713,13 +7707,12 @@ pub mod optimize { // Clear equivalence when a local is set (unless it's from the pattern above) // This ensures we don't use stale equivalences after a local is modified match instr { - Instruction::LocalSet(idx) => { + Instruction::LocalSet(idx) // Check if this is NOT the target of a local.get; local.set pattern - if i == 0 || !matches!(&instructions[i - 1], Instruction::LocalGet(_)) { + if (i == 0 || !matches!(&instructions[i - 1], Instruction::LocalGet(_))) => { // This set breaks any prior equivalence equivalences.remove(idx); } - } Instruction::LocalTee(idx) => { // Tee also breaks equivalence (unless immediately after local.get of same local) equivalences.remove(idx); @@ -8166,26 +8159,18 @@ pub mod optimize { *position += 1; match instr { - Instruction::LocalSet(_) => { - if redundant_positions.contains(¤t_pos) { - // Replace redundant set with drop (preserves stack effects) - result.push(Instruction::Drop); - *changed = true; - } else { - result.push(instr.clone()); - } + Instruction::LocalSet(_) if redundant_positions.contains(¤t_pos) => { + // Replace redundant set with drop (preserves stack effects) + result.push(Instruction::Drop); + *changed = true; } - Instruction::LocalTee(_) => { - if tee_positions_to_remove.contains(¤t_pos) { - // Remove redundant tee entirely (value stays on stack) - // Don't push anything - this preserves stack because: - // tee: pop value, set local, push value -> net effect: value stays - // nothing: value stays - *changed = true; - } else { - result.push(instr.clone()); - } + Instruction::LocalTee(_) if tee_positions_to_remove.contains(¤t_pos) => { + // Remove redundant tee entirely (value stays on stack) + // Don't push anything - this preserves stack because: + // tee: pop value, set local, push value -> net effect: value stays + // nothing: value stays + *changed = true; } Instruction::Block { block_type, body } => { @@ -9796,9 +9781,9 @@ pub mod optimize { use crate::Instruction; for instr in instructions { match instr { - Instruction::LocalGet(idx) => { + Instruction::LocalGet(idx) // Parameters are always live (don't coalesce them) - if *idx >= param_count as u32 { + if *idx >= param_count as u32 => { let info = local_info.entry(*idx).or_default(); info.last_use = Some(*position); if info.first_def.is_none() { @@ -9806,9 +9791,8 @@ pub mod optimize { info.first_def = Some(0); } } - } - Instruction::LocalSet(idx) | Instruction::LocalTee(idx) => { - if *idx >= param_count as u32 { + Instruction::LocalSet(idx) | Instruction::LocalTee(idx) + if *idx >= param_count as u32 => { let info = local_info.entry(*idx).or_default(); if info.first_def.is_none() { info.first_def = Some(*position); @@ -9818,7 +9802,6 @@ pub mod optimize { info.last_use = Some(*position); } } - } // Recurse into control flow Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { scan_instructions(body, local_info, position, param_count); @@ -10315,10 +10298,10 @@ pub mod optimize { | Instruction::Return => return false, // Local modifications invalidate if they reference our locals - Instruction::LocalSet(idx) | Instruction::LocalTee(idx) => { - if first.referenced_locals.contains(idx) { - return false; - } + Instruction::LocalSet(idx) | Instruction::LocalTee(idx) + if first.referenced_locals.contains(idx) => + { + return false; } // Memory operations are conservatively rejected for now diff --git a/loom-core/src/stack.rs b/loom-core/src/stack.rs index f7abfb3..dfdb94d 100644 --- a/loom-core/src/stack.rs +++ b/loom-core/src/stack.rs @@ -1209,29 +1209,25 @@ pub mod validation { // Call and CallIndirect need type context - only unanalyzable if we don't have it // CallIndirect's stack signature is fully determined by type_idx (statically known), // even though the target function is resolved at runtime from the table. - Call(_) | CallIndirect { .. } => { - if !has_context { - return true; - } + Call(_) | CallIndirect { .. } if !has_context => { + return true; } // Unknown instructions have unknown stack effects - can't validate Unknown(_) => return true, // Recursively check nested bodies - Block { body, .. } | Loop { body, .. } => { - if contains_unanalyzable_instructions(body, has_context) { - return true; - } + Block { body, .. } | Loop { body, .. } + if contains_unanalyzable_instructions(body, has_context) => + { + return true; } If { then_body, else_body, .. - } => { - if contains_unanalyzable_instructions(then_body, has_context) - || contains_unanalyzable_instructions(else_body, has_context) - { - return true; - } + } if (contains_unanalyzable_instructions(then_body, has_context) + || contains_unanalyzable_instructions(else_body, has_context)) => + { + return true; } _ => {} } diff --git a/loom-core/src/verify.rs b/loom-core/src/verify.rs index 36e3a26..d8ea7be 100644 --- a/loom-core/src/verify.rs +++ b/loom-core/src/verify.rs @@ -755,26 +755,23 @@ fn block_type_width(block_type: &BlockType) -> Option { fn contains_complex_loops(instructions: &[Instruction]) -> bool { for instr in instructions { match instr { - Instruction::Loop { body, .. } => { + Instruction::Loop { body, .. } // Check if this loop is too complex for bounded verification - if is_complex_loop(body) { + if is_complex_loop(body) => { return true; } - } - Instruction::Block { body, .. } => { - if contains_complex_loops(body) { + Instruction::Block { body, .. } + if contains_complex_loops(body) => { return true; } - } Instruction::If { then_body, else_body, .. - } => { - if contains_complex_loops(then_body) || contains_complex_loops(else_body) { + } + if (contains_complex_loops(then_body) || contains_complex_loops(else_body)) => { return true; } - } _ => {} } } @@ -842,23 +839,21 @@ fn is_complex_loop_at_depth(body: &[Instruction], depth: usize) -> bool { } Instruction::Block { body: inner_body, .. - } => { + } // Recurse into blocks (they don't increase loop depth) - if is_complex_loop_at_depth(inner_body, depth) { + if is_complex_loop_at_depth(inner_body, depth) => { return true; } - } Instruction::If { then_body, else_body, .. - } => { - if is_complex_loop_at_depth(then_body, depth) - || is_complex_loop_at_depth(else_body, depth) - { + } + if (is_complex_loop_at_depth(then_body, depth) + || is_complex_loop_at_depth(else_body, depth)) + => { return true; } - } _ => {} } } @@ -874,19 +869,15 @@ fn contains_any_loop(instructions: &[Instruction]) -> bool { for instr in instructions { match instr { Instruction::Loop { .. } => return true, - Instruction::Block { body, .. } => { - if contains_any_loop(body) { - return true; - } + Instruction::Block { body, .. } if contains_any_loop(body) => { + return true; } Instruction::If { then_body, else_body, .. - } => { - if contains_any_loop(then_body) || contains_any_loop(else_body) { - return true; - } + } if (contains_any_loop(then_body) || contains_any_loop(else_body)) => { + return true; } _ => {} } @@ -1154,68 +1145,50 @@ fn encode_loop_body_for_kinduction( } // Basic arithmetic (i32) - Instruction::I32Add => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvadd(&b)); - } - } - Instruction::I32Sub => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvsub(&b)); - } - } - Instruction::I32Mul => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvmul(&b)); - } - } - Instruction::I32And => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvand(&b)); - } - } - Instruction::I32Or => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvor(&b)); - } - } - Instruction::I32Xor => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvxor(&b)); - } - } - Instruction::I32Shl => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvshl(&b)); - } - } - Instruction::I32ShrU => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvlshr(&b)); - } - } - Instruction::I32ShrS => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(a.bvashr(&b)); - } + Instruction::I32Add if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvadd(&b)); + } + Instruction::I32Sub if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvsub(&b)); + } + Instruction::I32Mul if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvmul(&b)); + } + Instruction::I32And if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvand(&b)); + } + Instruction::I32Or if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvor(&b)); + } + Instruction::I32Xor if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvxor(&b)); + } + Instruction::I32Shl if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvshl(&b)); + } + Instruction::I32ShrU if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvlshr(&b)); + } + Instruction::I32ShrS if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + stack.push(a.bvashr(&b)); } // Comparisons @@ -1227,95 +1200,75 @@ fn encode_loop_body_for_kinduction( stack.push(result); } } - Instruction::I32Eq => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.eq(&b).ite(&one, &zero)); - } + Instruction::I32Eq if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.eq(&b).ite(&one, &zero)); } - Instruction::I32Ne => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.eq(&b).not().ite(&one, &zero)); - } + Instruction::I32Ne if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.eq(&b).not().ite(&one, &zero)); } - Instruction::I32LtS => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvslt(&b).ite(&one, &zero)); - } + Instruction::I32LtS if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvslt(&b).ite(&one, &zero)); } - Instruction::I32LtU => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvult(&b).ite(&one, &zero)); - } + Instruction::I32LtU if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvult(&b).ite(&one, &zero)); } - Instruction::I32GtS => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvsgt(&b).ite(&one, &zero)); - } + Instruction::I32GtS if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvsgt(&b).ite(&one, &zero)); } - Instruction::I32GtU => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvugt(&b).ite(&one, &zero)); - } + Instruction::I32GtU if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvugt(&b).ite(&one, &zero)); } - Instruction::I32LeS => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvsle(&b).ite(&one, &zero)); - } + Instruction::I32LeS if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvsle(&b).ite(&one, &zero)); } - Instruction::I32LeU => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvule(&b).ite(&one, &zero)); - } + Instruction::I32LeU if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvule(&b).ite(&one, &zero)); } - Instruction::I32GeS => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvsge(&b).ite(&one, &zero)); - } + Instruction::I32GeS if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvsge(&b).ite(&one, &zero)); } - Instruction::I32GeU => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let one = BV::from_i64(1, 32); - stack.push(a.bvuge(&b).ite(&one, &zero)); - } + Instruction::I32GeU if stack.len() >= 2 => { + let b = stack.pop().unwrap(); + let a = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let one = BV::from_i64(1, 32); + stack.push(a.bvuge(&b).ite(&one, &zero)); } // Control flow - simplified handling @@ -1381,15 +1334,13 @@ fn encode_loop_body_for_kinduction( Instruction::Drop => { stack.pop(); } - Instruction::Select => { - if stack.len() >= 3 { - let cond = stack.pop().unwrap(); - let val2 = stack.pop().unwrap(); - let val1 = stack.pop().unwrap(); - let zero = BV::from_i64(0, 32); - let cond_bool = cond.eq(&zero).not(); - stack.push(cond_bool.ite(&val1, &val2)); - } + Instruction::Select if stack.len() >= 3 => { + let cond = stack.pop().unwrap(); + let val2 = stack.pop().unwrap(); + let val1 = stack.pop().unwrap(); + let zero = BV::from_i64(0, 32); + let cond_bool = cond.eq(&zero).not(); + stack.push(cond_bool.ite(&val1, &val2)); } // End of block @@ -1468,21 +1419,19 @@ fn contains_unverifiable_instructions(instructions: &[Instruction]) -> bool { } // Recurse into control flow structures - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if contains_unverifiable_instructions(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if contains_unverifiable_instructions(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if contains_unverifiable_instructions(then_body) - || contains_unverifiable_instructions(else_body) - { - return true; - } + } if (contains_unverifiable_instructions(then_body) + || contains_unverifiable_instructions(else_body)) => + { + return true; } // All other instructions have precise SMT encodings @@ -1853,21 +1802,19 @@ fn contains_memory_instructions(instructions: &[Instruction]) -> bool { // Note: I32Load, I64Load, I32Store, I64Store are now verifiable // via Z3 Array theory (Array[BitVec32 -> BitVec8] with little-endian encoding) - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if contains_memory_instructions(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if contains_memory_instructions(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if contains_memory_instructions(then_body) - || contains_memory_instructions(else_body) - { - return true; - } + } if (contains_memory_instructions(then_body) + || contains_memory_instructions(else_body)) => + { + return true; } _ => {} } @@ -2315,36 +2262,30 @@ fn has_multi_memory_ops(instructions: &[Instruction]) -> bool { | Instruction::I64Store8 { mem, .. } | Instruction::I64Store16 { mem, .. } | Instruction::I64Store32 { mem, .. } - | Instruction::MemoryFill(mem) => { - if *mem != 0 { - return true; - } + | Instruction::MemoryFill(mem) + if *mem != 0 => + { + return true; } // MemoryCopy has two memory indices - skip if either is non-zero - Instruction::MemoryCopy { dst_mem, src_mem } => { - if *dst_mem != 0 || *src_mem != 0 { - return true; - } + Instruction::MemoryCopy { dst_mem, src_mem } if (*dst_mem != 0 || *src_mem != 0) => { + return true; } // MemoryInit targets a specific memory - Instruction::MemoryInit { mem, .. } => { - if *mem != 0 { - return true; - } + Instruction::MemoryInit { mem, .. } if *mem != 0 => { + return true; } - Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { - if has_multi_memory_ops(body) { - return true; - } + Instruction::Block { body, .. } | Instruction::Loop { body, .. } + if has_multi_memory_ops(body) => + { + return true; } Instruction::If { then_body, else_body, .. - } => { - if has_multi_memory_ops(then_body) || has_multi_memory_ops(else_body) { - return true; - } + } if (has_multi_memory_ops(then_body) || has_multi_memory_ops(else_body)) => { + return true; } _ => {} } diff --git a/loom-testing/src/emi/analysis.rs b/loom-testing/src/emi/analysis.rs index 04cf38a..adc8dac 100644 --- a/loom-testing/src/emi/analysis.rs +++ b/loom-testing/src/emi/analysis.rs @@ -63,27 +63,24 @@ fn analyze_function_body(func_idx: u32, body: &FunctionBody) -> Result { - if i + 1 < operators.len() { - if let (Operator::If { .. }, _) = &operators[i + 1] { - // Found constant condition if - if let Some(region) = - find_dead_if_branch(&operators, i + 1, *value != 0, func_idx) - { + Operator::I32Const { value } if i + 1 < operators.len() => { + if let (Operator::If { .. }, _) = &operators[i + 1] { + // Found constant condition if + if let Some(region) = + find_dead_if_branch(&operators, i + 1, *value != 0, func_idx) + { + dead_regions.push(region); + } + } else if let (Operator::BrIf { .. }, _) = &operators[i + 1] { + // Found constant condition br_if + if *value != 0 { + // br_if always taken - code after is dead + if let Some(region) = find_dead_after_br_if(&operators, i + 1, func_idx) { dead_regions.push(region); } - } else if let (Operator::BrIf { .. }, _) = &operators[i + 1] { - // Found constant condition br_if - if *value != 0 { - // br_if always taken - code after is dead - if let Some(region) = find_dead_after_br_if(&operators, i + 1, func_idx) - { - dead_regions.push(region); - } - } - // If value == 0, br_if never taken - the br_if itself could be removed - // but that's an optimization, not dead code detection } + // If value == 0, br_if never taken - the br_if itself could be removed + // but that's an optimization, not dead code detection } } @@ -134,10 +131,8 @@ fn find_dead_if_branch( Operator::If { .. } | Operator::Block { .. } | Operator::Loop { .. } => { depth += 1; } - Operator::Else => { - if depth == 1 { - else_offset = Some(operators[j].1); - } + Operator::Else if depth == 1 => { + else_offset = Some(operators[j].1); } Operator::End => { depth -= 1; diff --git a/loom-testing/src/emi/mutation.rs b/loom-testing/src/emi/mutation.rs index dcaca78..485f245 100644 --- a/loom-testing/src/emi/mutation.rs +++ b/loom-testing/src/emi/mutation.rs @@ -215,12 +215,11 @@ where data: &wasm_bytes[reader.range().start..reader.range().end], }); } - Payload::End(_) => { + Payload::End(_) // Write code section if we haven't yet - if in_code_section && !code_section_entries.is_empty() { + if in_code_section && !code_section_entries.is_empty() => { write_code_section(&mut module, &code_section_entries); } - } _ => { // Skip other payloads } diff --git a/safety/requirements/requirements.yaml b/safety/requirements/requirements.yaml index 4c9d40e..c9a80f7 100644 --- a/safety/requirements/requirements.yaml +++ b/safety/requirements/requirements.yaml @@ -16,6 +16,16 @@ artifacts: links: - type: mitigates target: SC-1 + - type: constraint-satisfies + target: SC-1 + - type: constraint-satisfies + target: SC-2 + - type: constraint-satisfies + target: SC-4 + - type: constraint-satisfies + target: SC-10 + - type: constraint-satisfies + target: SC-13 - id: REQ-2 type: requirement @@ -27,6 +37,11 @@ artifacts: fields: priority: must category: constraint + links: + - type: satisfies + target: DD-3 + - type: satisfies + target: DD-6 - id: REQ-3 type: requirement @@ -70,6 +85,15 @@ artifacts: fields: priority: must category: constraint + links: + - type: constraint-satisfies + target: SC-5 + - type: constraint-satisfies + target: SC-6 + - type: constraint-satisfies + target: SC-7 + - type: constraint-satisfies + target: SC-8 # ============================================================================ # Verification requirements @@ -90,6 +114,10 @@ artifacts: target: SC-1 - type: mitigates target: SC-11 + - type: constraint-satisfies + target: SC-11 + - type: constraint-satisfies + target: SC-17 - id: REQ-7 type: requirement @@ -132,6 +160,10 @@ artifacts: links: - type: mitigates target: SC-10 + - type: constraint-satisfies + target: SC-9 + - type: constraint-satisfies + target: SC-18 - id: REQ-10 type: requirement @@ -181,6 +213,10 @@ artifacts: links: - type: mitigates target: SC-9 + - type: constraint-satisfies + target: SC-3 + - type: constraint-satisfies + target: SC-14 - id: REQ-13 type: requirement @@ -196,6 +232,8 @@ artifacts: links: - type: mitigates target: SC-3 + - type: constraint-satisfies + target: SC-16 - id: REQ-14 type: requirement @@ -208,6 +246,9 @@ artifacts: fields: priority: must category: non-functional + links: + - type: constraint-satisfies + target: SC-19 - id: REQ-15 type: requirement @@ -250,6 +291,10 @@ artifacts: links: - type: mitigates target: SC-12 + - type: constraint-satisfies + target: SC-12 + - type: constraint-satisfies + target: SC-15 - id: REQ-18 type: requirement diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml index f83a295..aef9a66 100644 --- a/safety/stpa/control-structure.yaml +++ b/safety/stpa/control-structure.yaml @@ -190,6 +190,13 @@ controlled-processes: The in-memory Module struct containing types, functions, tables, memories, globals, and exports. All optimization phases read and modify this structure. + links: + - type: acted-on-by + target: CTRL-1 + - type: acted-on-by + target: CTRL-3 + - type: acted-on-by + target: CTRL-7 - id: CP-2 name: ISLE term environment @@ -197,6 +204,9 @@ controlled-processes: The term environment used during ISLE rewriting. Contains Value terms representing instruction sequences, local variable bindings, and the simplification context. + links: + - type: acted-on-by + target: CTRL-2 - id: CP-3 name: Output WASM binary @@ -204,3 +214,6 @@ controlled-processes: The final encoded WebAssembly binary. Once encoded, this is the artifact consumed by downstream tools (Meld, Kiln, Synth, or direct execution runtimes). + links: + - type: acted-on-by + target: CTRL-6 diff --git a/safety/stpa/controller-constraints.yaml b/safety/stpa/controller-constraints.yaml index fbc7ff7..832b2db 100644 --- a/safety/stpa/controller-constraints.yaml +++ b/safety/stpa/controller-constraints.yaml @@ -15,6 +15,9 @@ controller-constraints: signedness, immediate values) preserved. ucas: [UCA-1, UCA-3] hazards: [H-11] + links: + - type: satisfies + target: REQ-9 - id: CC-2 controller: CTRL-1 @@ -24,6 +27,9 @@ controller-constraints: silently dropped from the instruction stream. ucas: [UCA-2] hazards: [H-11] + links: + - type: satisfies + target: REQ-9 # ── ISLE term rewriter constraints ────────────────────────────────── - id: CC-3 @@ -34,6 +40,11 @@ controller-constraints: negative values, NaN, infinity, and subnormals where applicable. ucas: [UCA-4] hazards: [H-1] + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-6 - id: CC-4 controller: CTRL-2 @@ -44,6 +55,9 @@ controller-constraints: If it cannot be determined statically, the fold must not occur. ucas: [UCA-5] hazards: [H-1] + links: + - type: satisfies + target: REQ-1 - id: CC-5 controller: CTRL-2 @@ -54,6 +68,9 @@ controller-constraints: the instruction's observable behavior. ucas: [UCA-6] hazards: [H-2] + links: + - type: satisfies + target: REQ-1 - id: CC-6 controller: CTRL-2 @@ -63,6 +80,9 @@ controller-constraints: verify round-trip fidelity for every supported instruction type. ucas: [UCA-7] hazards: [H-3] + links: + - type: satisfies + target: REQ-1 - id: CC-7 controller: CTRL-2 @@ -72,6 +92,9 @@ controller-constraints: shift for negative numbers), or must only apply to unsigned operations. ucas: [UCA-8] hazards: [H-14] + links: + - type: satisfies + target: REQ-1 # ── Pipeline orchestrator constraints ─────────────────────────────── - id: CC-8 @@ -82,6 +105,9 @@ controller-constraints: check must be updated whenever new instruction support is added. ucas: [UCA-9] hazards: [H-1, H-2] + links: + - type: satisfies + target: REQ-5 - id: CC-9 controller: CTRL-3 @@ -92,6 +118,9 @@ controller-constraints: only if all branch targets are covered. ucas: [UCA-10] hazards: [H-5] + links: + - type: satisfies + target: REQ-1 - id: CC-10 controller: CTRL-3 @@ -102,6 +131,11 @@ controller-constraints: may be cached. ucas: [UCA-11] hazards: [H-6] + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-5 - id: CC-11 controller: CTRL-3 @@ -112,6 +146,9 @@ controller-constraints: semantics correctly. ucas: [UCA-12] hazards: [H-7] + links: + - type: satisfies + target: REQ-1 - id: CC-12 controller: CTRL-3 @@ -121,6 +158,9 @@ controller-constraints: enforce a maximum inlined body size to prevent code explosion. ucas: [UCA-13] hazards: [H-7] + links: + - type: satisfies + target: REQ-5 - id: CC-13 controller: CTRL-3 @@ -131,6 +171,9 @@ controller-constraints: have arbitrary effects via imported functions). ucas: [UCA-14] hazards: [H-8] + links: + - type: satisfies + target: REQ-1 - id: CC-14 controller: CTRL-3 @@ -141,6 +184,11 @@ controller-constraints: modified set and it does not access memory or globals. ucas: [UCA-15] hazards: [H-9] + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-5 - id: CC-15 controller: CTRL-3 @@ -150,6 +198,9 @@ controller-constraints: block layers. Loop blocks must never be merged away. ucas: [UCA-16] hazards: [H-15] + links: + - type: satisfies + target: REQ-1 - id: CC-16 controller: CTRL-3 @@ -159,6 +210,11 @@ controller-constraints: global.get replaced with a constant. ucas: [UCA-17] hazards: [H-16] + links: + - type: satisfies + target: REQ-1 + - type: satisfies + target: REQ-5 # ── Stack validator constraints ───────────────────────────────────── - id: CC-17 @@ -170,6 +226,9 @@ controller-constraints: rather than using a default signature. ucas: [UCA-18] hazards: [H-4] + links: + - type: satisfies + target: REQ-13 - id: CC-18 controller: CTRL-4 @@ -180,6 +239,9 @@ controller-constraints: validation algorithm. ucas: [UCA-19] hazards: [H-4] + links: + - type: satisfies + target: REQ-13 # ── Z3 verifier constraints ───────────────────────────────────────── - id: CC-19 @@ -191,6 +253,9 @@ controller-constraints: bvsdiv, bvsrem). ucas: [UCA-20] hazards: [H-12] + links: + - type: satisfies + target: REQ-6 - id: CC-20 controller: CTRL-5 @@ -201,6 +266,9 @@ controller-constraints: just that non-trapping results match. ucas: [UCA-21] hazards: [H-12] + links: + - type: satisfies + target: REQ-6 # ── Binary encoder constraints ────────────────────────────────────── - id: CC-21 @@ -212,6 +280,9 @@ controller-constraints: encoding correctness. ucas: [UCA-22] hazards: [H-10] + links: + - type: satisfies + target: REQ-12 - id: CC-22 controller: CTRL-6 @@ -222,6 +293,9 @@ controller-constraints: actual encoding is not acceptable. ucas: [UCA-23] hazards: [H-10] + links: + - type: satisfies + target: REQ-12 # ── Component model optimizer constraints ─────────────────────────── - id: CC-23 @@ -233,6 +307,9 @@ controller-constraints: adapters where source and destination types are identical. ucas: [UCA-24] hazards: [H-13] + links: + - type: satisfies + target: REQ-17 - id: CC-24 controller: CTRL-7 @@ -242,3 +319,6 @@ controller-constraints: resource handle allocation, table mutations). ucas: [UCA-25] hazards: [H-13] + links: + - type: satisfies + target: REQ-17