-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
10 changed files
with
505 additions
and
0 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
{ mk, versions, localCrates, smoltcpWith, serdeWith, authors }: | ||
|
||
mk { | ||
package.name = "sel4-hal-adapters"; | ||
package.authors = with authors; [ | ||
nspin | ||
"Ben Hamlin <hamlinb@galois.com>" | ||
]; | ||
dependencies = { | ||
inherit (versions) log; | ||
smoltcp = smoltcpWith [] // { optional = true; }; | ||
serde = serdeWith []; | ||
} // (with localCrates; { | ||
inherit sel4-microkit-message; | ||
sel4-microkit = sel4-microkit // { default-features = false; }; | ||
|
||
# smoltcp-phy deps | ||
sel4-bounce-buffer-allocator = sel4-bounce-buffer-allocator // { optional = true; }; | ||
sel4-externally-shared = sel4-externally-shared // { optional = true; features = ["unstable"]; }; | ||
sel4-shared-ring-buffer = sel4-shared-ring-buffer // { optional = true; }; | ||
}); | ||
features = { | ||
default = ["smoltcp-hal"]; | ||
smoltcp-hal = [ | ||
"smoltcp" | ||
"sel4-shared-ring-buffer" | ||
"sel4-externally-shared" | ||
"sel4-bounce-buffer-allocator" | ||
]; | ||
}; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
# | ||
# Copyright 2023, Colias Group, LLC | ||
# | ||
# SPDX-License-Identifier: BSD-2-Clause | ||
# | ||
# | ||
# This file is generated from './Cargo.nix'. You can edit this file directly | ||
# if you are not using this project's Cargo manifest management tools. | ||
# See 'hacking/cargo-manifest-management/README.md' for more information. | ||
# | ||
|
||
[package] | ||
name = "sel4-hal-adapters" | ||
version = "0.1.0" | ||
authors = ["Nick Spinale <nick.spinale@coliasgroup.com>", "Ben Hamlin <hamlinb@galois.com>"] | ||
edition = "2021" | ||
license = "BSD-2-Clause" | ||
|
||
[features] | ||
default = ["smoltcp-hal"] | ||
smoltcp-hal = [ | ||
"smoltcp", | ||
"sel4-shared-ring-buffer", | ||
"sel4-externally-shared", | ||
"sel4-bounce-buffer-allocator", | ||
] | ||
|
||
[dependencies] | ||
log = "0.4.17" | ||
sel4-bounce-buffer-allocator = { path = "../sel4-bounce-buffer-allocator", optional = true } | ||
sel4-microkit = { path = "../sel4-microkit", default-features = false } | ||
sel4-microkit-message = { path = "../sel4-microkit/message" } | ||
sel4-shared-ring-buffer = { path = "../sel4-shared-ring-buffer", optional = true } | ||
serde = { version = "1.0.147", default-features = false } | ||
|
||
[dependencies.sel4-externally-shared] | ||
path = "../sel4-externally-shared" | ||
features = ["unstable"] | ||
optional = true | ||
|
||
[dependencies.smoltcp] | ||
version = "0.10.0" | ||
default-features = false | ||
features = ["proto-ipv4", "proto-dhcpv4", "proto-dns", "socket-dhcpv4", "socket-dns", "socket-tcp"] | ||
optional = true |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,239 @@ | ||
#![no_std] | ||
|
||
use num_enum::{IntoPrimitive, TryFromPrimitive}; | ||
use zerocopy::{AsBytes, FromBytes}; | ||
use core::fmt; | ||
use heapless::Deque; | ||
|
||
use embedded_hal::serial; | ||
use embedded_hal::prelude::_embedded_hal_serial_Write; | ||
use sel4cp::{Channel, Handler}; | ||
use sel4cp::message::{MessageInfo, NoMessageValue, StatusMessageLabel}; | ||
use sel4cp::message::MessageInfoRecvError; | ||
|
||
/// Handle messages using an implementor of [serial::Read<u8>] and [serial::Write<u8>]. | ||
#[derive(Clone, Debug)] | ||
pub struct SerialHandler<Device, const READ_BUF_SIZE: usize = 256> { | ||
/// Device implementing [serial::Read<u8>] and [serial::Write<u8>]. | ||
device: Device, | ||
/// Channel for this component. | ||
serial: Channel, | ||
/// Channel for client component. | ||
client: Channel, | ||
/// Read buffer. | ||
buffer: Deque<u8, READ_BUF_SIZE>, | ||
/// Whether to notify client. | ||
notify: bool, | ||
} | ||
|
||
impl<Device> SerialHandler<Device> | ||
where | ||
Device: serial::Read<u8> + serial::Write<u8> + IrqDevice | ||
{ | ||
pub fn new(device: Device, serial: Channel, client: Channel) -> Self { | ||
Self { | ||
device, | ||
serial, | ||
client, | ||
buffer: Deque::new(), | ||
notify: true, | ||
} | ||
} | ||
} | ||
|
||
pub trait IrqDevice { | ||
fn handle_irq(&self); | ||
} | ||
|
||
#[non_exhaustive] | ||
#[derive(Clone, Debug)] | ||
pub enum SerialHandlerError<Device> | ||
where | ||
Device: serial::Read<u8> + serial::Write<u8>, | ||
<Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone, | ||
<Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone, | ||
{ | ||
ReadError(<Device as serial::Read<u8>>::Error), | ||
WriteError(<Device as serial::Write<u8>>::Error), | ||
BufferFull, | ||
// XXX Other errors? | ||
} | ||
|
||
impl<Device> fmt::Display for SerialHandlerError<Device> | ||
where | ||
Device: serial::Read<u8> + serial::Write<u8>, | ||
<Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone, | ||
<Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone, | ||
{ | ||
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { | ||
match *self { | ||
SerialHandlerError::ReadError(_) => write!(f, "SerialHandlerError::ReadError"), | ||
SerialHandlerError::WriteError(_) => write!(f, "SerialHandlerError::WriteError"), | ||
SerialHandlerError::BufferFull => write!(f, "SerialHandlerError::BufferFull"), | ||
} | ||
} | ||
} | ||
|
||
impl<Device> Handler for SerialHandler<Device> | ||
where | ||
Device: serial::Read<u8> + serial::Write<u8> + IrqDevice, | ||
<Device as serial::Read<u8>>::Error: core::fmt::Debug + Clone, | ||
<Device as serial::Write<u8>>::Error: core::fmt::Debug + Clone, | ||
{ | ||
type Error = SerialHandlerError<Device>; | ||
|
||
fn notified(&mut self, channel: Channel) -> Result<(), Self::Error> { | ||
// TODO Handle errors | ||
if channel == self.serial { | ||
while let Ok(c) = self.device.read() { | ||
if let Err(_) = self.buffer.push_back(c) { | ||
return Err(SerialHandlerError::BufferFull); | ||
} | ||
} | ||
self.device.handle_irq(); | ||
self.serial.irq_ack().unwrap(); | ||
if self.notify { | ||
self.client.notify(); | ||
self.notify = false; | ||
} | ||
} else { | ||
unreachable!() // XXX Is this actually unreachable? | ||
} | ||
Ok(()) | ||
} | ||
|
||
fn protected( | ||
&mut self, | ||
channel: Channel, | ||
msg_info: MessageInfo, | ||
) -> Result<MessageInfo, Self::Error> { | ||
// TODO Handle errors | ||
if channel == self.client { | ||
match msg_info.label().try_into().ok() /* XXX Handle errors? */ { | ||
Some(RequestTag::Write) => match msg_info.recv() { | ||
Ok(WriteRequest { val }) => { | ||
// Blocking write | ||
while let Err(nb::Error::WouldBlock) = self.device.write(val) {} | ||
Ok(MessageInfo::send(StatusMessageLabel::Ok, NoMessageValue)) | ||
} | ||
Err(_) => Ok(MessageInfo::send(StatusMessageLabel::Error, NoMessageValue)), | ||
}, | ||
Some(RequestTag::Read) => match self.buffer.pop_front() { | ||
Some(val) => { | ||
Ok(MessageInfo::send(ReadResponseTag::Some, ReadSomeResponse { val })) | ||
} | ||
None => { | ||
self.notify = true; | ||
Ok(MessageInfo::send(ReadResponseTag::None, NoMessageValue)) | ||
} | ||
}, | ||
None => Ok(MessageInfo::send(StatusMessageLabel::Error, NoMessageValue)), | ||
} | ||
} else { | ||
unreachable!() // XXX Is this actually unreachable? | ||
} | ||
} | ||
} | ||
|
||
/// Device-independent embedded_hal::serial interface to a serial-device | ||
/// component. Interact with it using [serial::Read], [serial::Write], | ||
/// and [fmt::Write]. | ||
#[derive(Clone, Debug, PartialEq, Eq)] | ||
pub struct SerialDriver { | ||
pub channel: Channel | ||
} | ||
|
||
impl SerialDriver { | ||
pub fn new(channel: Channel) -> Self { | ||
SerialDriver { channel } | ||
} | ||
} | ||
|
||
#[derive(Clone, Debug)] | ||
pub enum ReadError { | ||
RecvError(MessageInfoRecvError), | ||
InvalidResponse, | ||
EOF, | ||
} | ||
|
||
impl serial::Read<u8> for SerialDriver { | ||
type Error = ReadError; | ||
|
||
// XXX Unclear if this blocks or how to prevent it from doing so... | ||
fn read(&mut self) -> nb::Result<u8, Self::Error> { | ||
let msg_info = self.channel | ||
.pp_call(MessageInfo::send(RequestTag::Read, NoMessageValue)); | ||
|
||
match msg_info.label().try_into() { | ||
Ok(ReadResponseTag::Some) => match msg_info.recv() { | ||
Ok(ReadSomeResponse { val }) => Ok(val), | ||
Err(e) => Err(nb::Error::Other(ReadError::RecvError(e))), | ||
}, | ||
Ok(ReadResponseTag::None) => Err(nb::Error::Other(ReadError::EOF)), | ||
Err(_) => Err(nb::Error::Other(ReadError::InvalidResponse)), | ||
} | ||
} | ||
} | ||
|
||
#[derive(Clone, Debug, PartialEq, Eq)] | ||
pub enum WriteError { | ||
SendError, | ||
InvalidResponse, | ||
} | ||
|
||
impl serial::Write<u8> for SerialDriver { | ||
type Error = WriteError; | ||
|
||
// XXX Unclear if this blocks or how to prevent it from doing so... | ||
fn write(&mut self, val: u8) -> nb::Result<(), Self::Error> { | ||
let msg_info = self.channel | ||
.pp_call(MessageInfo::send(RequestTag::Write, WriteRequest { val })); | ||
|
||
match msg_info.label().try_into() { | ||
Ok(StatusMessageLabel::Ok) => Ok(()), | ||
Ok(StatusMessageLabel::Error) => Err(nb::Error::Other(WriteError::SendError)), | ||
Err(_) => Err(nb::Error::Other(WriteError::InvalidResponse)), | ||
} | ||
} | ||
|
||
fn flush(&mut self) -> nb::Result<(), Self::Error> { | ||
todo!() | ||
} | ||
} | ||
|
||
// XXX There's already an implementation of core::fmt::Write for serial::Write | ||
// in embedded_hal::fmt, but I'm not clear on how to use it. | ||
impl fmt::Write for SerialDriver { | ||
fn write_str(&mut self, s: &str) -> fmt::Result { | ||
s.as_bytes().iter().copied().for_each(|b| { let _ = self.write(b); }); | ||
Ok(()) | ||
} | ||
} | ||
|
||
#[derive(Clone, Copy, PartialEq, Eq, IntoPrimitive, TryFromPrimitive)] | ||
#[cfg_attr(target_pointer_width = "32", repr(u32))] | ||
#[cfg_attr(target_pointer_width = "64", repr(u64))] | ||
pub enum RequestTag { | ||
Write, | ||
Read, | ||
} | ||
|
||
#[derive(Clone, Copy, PartialEq, Eq, AsBytes, FromBytes)] | ||
#[repr(C)] | ||
pub struct WriteRequest { | ||
pub val: u8, | ||
} | ||
|
||
#[derive(Clone, Copy, PartialEq, Eq, IntoPrimitive, TryFromPrimitive)] | ||
#[cfg_attr(target_pointer_width = "32", repr(u32))] | ||
#[cfg_attr(target_pointer_width = "64", repr(u64))] | ||
pub enum ReadResponseTag { | ||
None, | ||
Some, | ||
} | ||
|
||
#[derive(Clone, Copy, PartialEq, Eq, AsBytes, FromBytes)] | ||
#[repr(C)] | ||
pub struct ReadSomeResponse { | ||
pub val: u8, | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
#![no_std] | ||
#![feature(never_type)] | ||
#![feature(strict_provenance)] | ||
#![feature(let_chains)] | ||
|
||
#[cfg(feature = "smoltcp-hal")] | ||
pub mod smoltcp; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
pub mod phy; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
//! Client-side [`smoltcp::phy::Device`] implementation | ||
pub use sel4_shared_ring_buffer::*; |
Oops, something went wrong.