Validate configuration through its owning schemas and keep board declarations separate from shared F722 resource ownership. Bound USB transitions, isolate transport failures and retain restart-only activation. Migrate navigation and flight consumers with the sensor and schema contracts. Require explicit installation data and synchronous output authority; board motor outputs remain inhibited. Validation: assembled-prefix host tests, strict Clippy, platform/USB tests and both ARM release builds. Final-source coverage and scoped Miri/Kani evidence are retained separately from hardware qualification.
133 lines
4.8 KiB
Rust
133 lines
4.8 KiB
Rust
//! Source checks only for hardware boundaries that host execution cannot probe.
|
|
use std::{fs, path::PathBuf};
|
|
fn source(relative: &str) -> String {
|
|
fs::read_to_string(PathBuf::from(env!("CARGO_MANIFEST_DIR")).join(relative)).unwrap()
|
|
}
|
|
#[test]
|
|
fn motor_pins_are_inhibited_before_initialization() {
|
|
let module = source("src/f722/mod.rs");
|
|
let interlock = module.find("motor_inhibit::inhibit(").unwrap();
|
|
let validation = module.find("board::validate_board_config").unwrap();
|
|
let initialize = module.find("board::initialize").unwrap();
|
|
assert!(interlock < validation && validation < initialize);
|
|
let interlock = source("src/f722/motor_inhibit.rs");
|
|
assert!(
|
|
interlock.find("rcc.ahb1enr().read()").unwrap() < interlock.find("port.bsrr()").unwrap()
|
|
);
|
|
assert!(interlock.find("port.bsrr()").unwrap() < interlock.find("port.moder()").unwrap());
|
|
}
|
|
|
|
#[test]
|
|
fn board_images_have_no_actuator_route() {
|
|
let sources = [
|
|
"src/lib.rs",
|
|
"src/f722/mod.rs",
|
|
"src/f722/board.rs",
|
|
"src/f722/firmware.rs",
|
|
"src/f722/interrupts.rs",
|
|
]
|
|
.map(source)
|
|
.join("\n");
|
|
for forbidden in [
|
|
"mod actuator",
|
|
"MotorOutput",
|
|
"MotorRoute",
|
|
"TIM3",
|
|
"TIM5",
|
|
"Dshot",
|
|
"Pwm",
|
|
] {
|
|
assert!(!sources.contains(forbidden), "{forbidden}");
|
|
}
|
|
assert!(!source("Cargo.toml").contains("kaptan-actuator"));
|
|
}
|
|
#[test]
|
|
fn uart_runtime_has_no_dma_or_static_register_aliases() {
|
|
for path in [
|
|
"src/f722/serial.rs",
|
|
"src/f722/peripherals/usart.rs",
|
|
"src/f722/data_channel.rs",
|
|
] {
|
|
let code = source(path);
|
|
for forbidden in [
|
|
"DMA1::ptr",
|
|
"DMA2::ptr",
|
|
"USART1::ptr",
|
|
"USART2::ptr",
|
|
"USART3::ptr",
|
|
"UART4::ptr",
|
|
"USART6::ptr",
|
|
"DmaReadableBuffer",
|
|
"MavlinkTransmitter",
|
|
"dmat()",
|
|
] {
|
|
assert!(!code.contains(forbidden), "{path}: {forbidden}");
|
|
}
|
|
}
|
|
let firmware = source("src/f722/firmware.rs");
|
|
assert!(!firmware.contains("DMA2_STREAM7"));
|
|
assert!(!firmware.contains("DMA1_STREAM6"));
|
|
assert_eq!(firmware.matches("imu_worker::spawn()").count(), 1);
|
|
assert_eq!(firmware.matches("mavlink_worker::spawn()").count(), 1);
|
|
}
|
|
#[test]
|
|
fn source_keeps_atomic_chip_select_without_gpio_owner() {
|
|
let routes = source("src/f722/routes.rs");
|
|
let compact: String = routes.split_whitespace().collect();
|
|
assert!(compact.contains("pub(crate)structMpu6000Spi1Route{spi:Spi1,}"));
|
|
for bit in ["br2", "bs2", "br15", "bs15"] {
|
|
assert!(routes.contains(&format!("write.{bit}().set_bit()")));
|
|
}
|
|
}
|
|
#[test]
|
|
fn source_keeps_flash_irq_mask_and_reset() {
|
|
let config = source("src/f722/config.rs");
|
|
for required in [
|
|
"link_section = \".data.kaptan_flash_operation\"",
|
|
"\"mrs {primask}, PRIMASK\"",
|
|
"\"cpsid i\"",
|
|
"\"cpsie i\"",
|
|
"fn reset_after_flash_timeout() -> !",
|
|
"SYSRESETREQ",
|
|
"core::arch::asm!(\"dsb sy\"",
|
|
] {
|
|
assert!(config.contains(required), "{required}");
|
|
}
|
|
assert!(!config.contains("BusyTimeout"));
|
|
}
|
|
#[test]
|
|
fn normal_images_keep_usb_configuration_and_shared_file_service() {
|
|
let manifest = source("Cargo.toml");
|
|
assert!(!manifest.contains("development-config"));
|
|
let board = source("src/f722/board.rs");
|
|
assert_eq!(board.matches("FileService::new").count(), 1);
|
|
assert!(board.contains("usb_mavlink("));
|
|
assert!(board.contains("IngressId(id)"));
|
|
assert!(board.contains("result.refresh_lease"));
|
|
assert!(!board.contains("file_lease_ticks"));
|
|
}
|
|
|
|
#[test]
|
|
fn source_keeps_protocol_local_and_irq_priorities() {
|
|
let firmware = source("src/f722/firmware.rs");
|
|
let shared =
|
|
&firmware[firmware.find("struct Shared").unwrap()..firmware.find("#[local]").unwrap()];
|
|
assert!(!shared.contains("mavlink:"));
|
|
for owner in ["uarts:", "usb:", "serial_clock:"] {
|
|
assert!(shared.contains(owner));
|
|
}
|
|
assert!(firmware.contains("context.local.mavlink.process_worker_events"));
|
|
assert!(!firmware.contains(".lock(|mavlink|"));
|
|
assert!(firmware.contains("priority = 7, local = [mavlink]"));
|
|
for vector in ["USART1", "USART2", "USART3", "UART4", "USART6"] {
|
|
assert!(firmware.contains(&format!("binds = {vector}, priority = 14")));
|
|
}
|
|
assert!(firmware.contains("binds = OTG_FS, priority = 8, shared = [usb]"));
|
|
assert!(firmware.contains("binds = TIM2, priority = 10"));
|
|
assert!(firmware.contains("local = [timer], shared = [lidar]"));
|
|
let timer_irq = &firmware
|
|
[firmware.find("fn tim2(").unwrap()..firmware.find("async fn imu_worker").unwrap()];
|
|
assert!(timer_irq.contains("if !context.local.timer.on_interrupt()"));
|
|
assert!(timer_irq.find(".on_interrupt()").unwrap() < timer_irq.find(".lidar.lock").unwrap());
|
|
}
|