Skip to content

Commit

Permalink
Merge branch 'main' into tcb_unbind_ntfn
Browse files Browse the repository at this point in the history
  • Loading branch information
alwin-joshy authored Jul 2, 2024
2 parents dda5f14 + 4f13dd2 commit 3589567
Show file tree
Hide file tree
Showing 28 changed files with 95 additions and 94 deletions.
5 changes: 5 additions & 0 deletions .reuse/dep5
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,11 @@ Upstream-Name: seL4
Upstream-Contact: seL4 team <[email protected]>
Source: http://sel4.systems

Files:
VERSION
Copyright: 2024, Colias Group, LLC
License: CC-BY-SA-4.0

Files:
Cargo.lock
support/*.json
Expand Down
10 changes: 5 additions & 5 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions Cargo.nix
Original file line number Diff line number Diff line change
Expand Up @@ -24,9 +24,9 @@
members = lib.naturalSort (lib.mapAttrsToList (_: v: v.path) localCrates);
};
patch.crates-io = {
ring = {
ring = localCrates.ring or {
git = "https://github.com/coliasgroup/ring.git";
rev = "0e644b7837cffcd53a3ff67d7f478801b4e9e0ed";
rev = "0f749acc5d5a8310dfc3ff985df04056f497fc1b"; # branch sel4
};
};
}
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -148,4 +148,4 @@ members = [

[patch.crates-io.ring]
git = "https://github.com/coliasgroup/ring.git"
rev = "0e644b7837cffcd53a3ff67d7f478801b4e9e0ed"
rev = "0f749acc5d5a8310dfc3ff985df04056f497fc1b"
10 changes: 5 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,14 @@ Microkit](https://github.com/seL4/microkit). In particular, this project works w
following versions of those related projects:

- seL4, when used without Microkit:
[`ddeb18a015199a28393d654ad8349788ab492d8a`](https://github.com/seL4/seL4/tree/ddeb18a015199a28393d654ad8349788ab492d8a)
(on [github.com/seL4/seL4:master](https://github.com/seL4/seL4/tree/master))
[`cd6d3b8c25d49be2b100b0608cf0613483a6fffa`](https://github.com/seL4/seL4/tree/cd6d3b8c25d49be2b100b0608cf0613483a6fffa)
(version 13.0.0, on [github.com/seL4/seL4:master](https://github.com/seL4/seL4/tree/master))
- seL4, when used with Microkit:
[`57975d485397ce1744f7163644dd530560d0b7ec`](https://github.com/seL4/seL4/tree/57975d485397ce1744f7163644dd530560d0b7ec)
[`0cdbffec9cf6b4c7c9c57971cbee5a24a70c8fd0`](https://github.com/seL4/seL4/tree/0cdbffec9cf6b4c7c9c57971cbee5a24a70c8fd0)
(on [github.com/seL4/seL4:microkit](https://github.com/seL4/seL4/tree/microkit))
- seL4 Microkit:
[`0cdcd54ed4b2152678c4312e738b9b1830046234`](https://github.com/seL4/microkit/tree/0cdcd54ed4b2152678c4312e738b9b1830046234)
(on [github.com/seL4/microkit:main](https://github.com/seL4/microkit/tree/main))
[`1ccdfcb3b224533c965fd6508de3dd56657f959c`](https://github.com/seL4/microkit/tree/1ccdfcb3b224533c965fd6508de3dd56657f959c)
(version 1.3.0, on [github.com/seL4/microkit:main](https://github.com/seL4/microkit/tree/main))

### Demos

Expand Down
1 change: 1 addition & 0 deletions VERSION
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
1.0.0-dev
4 changes: 2 additions & 2 deletions crates/examples/microkit/http-server/http-server.system
Original file line number Diff line number Diff line change
Expand Up @@ -41,13 +41,13 @@

<protection_domain name="pl031_driver" pp="true" priority="251">
<program_image path="microkit-http-server-example-pl031-driver.elf" />
<map mr="pl031_mmio" vaddr="0x5_000_000_000" perms="rw" cached="false" setvar_vaddr="pl031_mmio_vaddr" />
<map mr="pl031_mmio" vaddr="0x5_000_000_000" perms="rw" cached="false" setvar_vaddr="pl031_mmio_vaddr" />
<irq irq="34" id="0" />
</protection_domain>

<protection_domain name="sp804_driver" pp="true" priority="254">
<program_image path="microkit-http-server-example-sp804-driver.elf" />
<map mr="sp804_mmio" vaddr="0x5_000_000_000" perms="rw" cached="false" setvar_vaddr="sp804_mmio_vaddr" />
<map mr="sp804_mmio" vaddr="0x5_000_000_000" perms="rw" cached="false" setvar_vaddr="sp804_mmio_vaddr" />
<irq irq="43" id="0" />
</protection_domain>

Expand Down
2 changes: 1 addition & 1 deletion crates/examples/microkit/http-server/pds/server/Cargo.nix
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
# SPDX-License-Identifier: BSD-2-Clause
#

{ mk, localCrates, versions, serdeWith, smoltcpWith, ringWith }:
{ mk, localCrates, versions, serdeWith, smoltcpWith }:

mk {
package.name = "microkit-http-server-example-server";
Expand Down
6 changes: 3 additions & 3 deletions crates/sel4-microkit/base/src/channel.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ const BASE_ENDPOINT_SLOT: usize = BASE_OUTPUT_NOTIFICATION_SLOT + 64;
const BASE_IRQ_SLOT: usize = BASE_ENDPOINT_SLOT + 64;
const BASE_TCB_SLOT: usize = BASE_IRQ_SLOT + 64;

const MAX_CHANNELS: usize = 63;
const MAX_CHANNELS: usize = 62;

/// A channel between this protection domain and another, identified by a channel index.
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
Expand Down Expand Up @@ -83,11 +83,11 @@ impl fmt::Display for IrqAckError {

/// A handle to a child protection domain, identified by a child protection domain index.
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
pub struct ProtectionDomain {
pub struct Child {
index: usize,
}

impl ProtectionDomain {
impl Child {
pub const fn new(index: usize) -> Self {
Self { index }
}
Expand Down
12 changes: 6 additions & 6 deletions crates/sel4-microkit/base/src/handler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use core::fmt;
use crate::{
defer::{DeferredAction, PreparedDeferredAction},
ipc::{self, Event},
pd_is_passive, Channel, MessageInfo, ProtectionDomain,
pd_is_passive, Channel, Child, MessageInfo,
};

pub use core::convert::Infallible;
Expand Down Expand Up @@ -39,10 +39,10 @@ pub trait Handler {

fn fault(
&mut self,
pd: ProtectionDomain,
child: Child,
msg_info: MessageInfo,
) -> Result<MessageInfo, Self::Error> {
panic!("unexpected fault from protection domain {pd:?} with msg_info={msg_info:?}")
) -> Result<Option<MessageInfo>, Self::Error> {
panic!("unexpected fault from protection domain {child:?} with msg_info={msg_info:?}")
}

/// An advanced feature for use by protection domains which seek to coalesce syscalls when
Expand Down Expand Up @@ -81,8 +81,8 @@ pub trait Handler {
Event::Protected(channel, msg_info) => {
reply_tag = Some(self.protected(channel, msg_info)?);
}
Event::Fault(pd, msg_info) => {
reply_tag = Some(self.fault(pd, msg_info)?);
Event::Fault(child, msg_info) => {
reply_tag = self.fault(child, msg_info)?;
}
};

Expand Down
8 changes: 4 additions & 4 deletions crates/sel4-microkit/base/src/ipc.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

use crate::MessageInfo;

use crate::{defer::PreparedDeferredAction, Channel, ProtectionDomain};
use crate::{defer::PreparedDeferredAction, Channel, Child};

const INPUT_CAP: sel4::cap::Endpoint = sel4::Cap::from_bits(1);
const REPLY_CAP: sel4::cap::Reply = sel4::Cap::from_bits(4);
Expand All @@ -29,7 +29,7 @@ fn strip_flag(badge: sel4::Badge, bit: usize) -> Option<sel4::Word> {
pub enum Event {
Notified(NotifiedEvent),
Protected(Channel, MessageInfo),
Fault(ProtectionDomain, MessageInfo),
Fault(Child, MessageInfo),
}

impl Event {
Expand All @@ -41,7 +41,7 @@ impl Event {
)
} else if let Some(pd_index) = strip_flag(badge, PD_BADGE_BIT) {
Self::Fault(
ProtectionDomain::new(pd_index.try_into().unwrap()),
Child::new(pd_index.try_into().unwrap()),
MessageInfo::from_inner(tag),
)
} else {
Expand Down Expand Up @@ -106,6 +106,6 @@ pub(crate) fn nb_send_recv(action: PreparedDeferredAction) -> Event {
pub(crate) fn forfeit_sc() -> PreparedDeferredAction {
PreparedDeferredAction::new(
MONITOR_EP_CAP.cast(),
sel4::MessageInfoBuilder::default().length(1).build(),
sel4::MessageInfoBuilder::default().build(),
)
}
4 changes: 2 additions & 2 deletions crates/sel4-microkit/base/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ mod symbols;
#[doc(hidden)]
pub mod ipc;

pub use channel::{Channel, IrqAckError, ProtectionDomain};
pub use channel::{Channel, Child, IrqAckError};
pub use defer::{DeferredAction, DeferredActionInterface, DeferredActionSlot};
pub use handler::{Handler, Infallible, NullHandler};
pub use handler::{Handler, Infallible, Never, NullHandler};
pub use message::{
get_mr, set_mr, with_msg_bytes, with_msg_bytes_mut, with_msg_regs, with_msg_regs_mut,
MessageInfo, MessageLabel, MessageRegisterValue,
Expand Down
6 changes: 4 additions & 2 deletions crates/sel4-shared-ring-buffer/smoltcp/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,10 @@ impl<A: AbstractBounceBufferAllocator> Device for DeviceImpl<A> {
}

fn receive(&mut self, _timestamp: Instant) -> Option<(Self::RxToken<'_>, Self::TxToken<'_>)> {
let r = self.inner().borrow_mut().receive();
r.map(|(rx_ix, tx_ix)| (self.new_rx_token(rx_ix), self.new_tx_token(tx_ix)))
self.inner()
.borrow_mut()
.receive()
.map(|(rx_ix, tx_ix)| (self.new_rx_token(rx_ix), self.new_tx_token(tx_ix)))
}

fn transmit(&mut self, _timestamp: Instant) -> Option<Self::TxToken<'_>> {
Expand Down
20 changes: 0 additions & 20 deletions crates/sel4/build-env/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,23 +81,3 @@ pub fn find_in_libsel4_include_dirs(relative_path: impl AsRef<Path>) -> PathBuf
)
})
}

pub fn try_get_or_find_in_libsel4_include_dirs(
var: &str,
relative_path: impl AsRef<Path>,
) -> Option<PathBuf> {
get_asserting_valid_unicode(var)
.map(PathBuf::from)
.or_else(|| try_find_in_libsel4_include_dirs(relative_path))
}

pub fn get_or_find_in_libsel4_include_dirs(var: &str, relative_path: impl AsRef<Path>) -> PathBuf {
let relative_path = relative_path.as_ref();
try_get_or_find_in_libsel4_include_dirs(var, relative_path).unwrap_or_else(|| {
panic!(
"{} not in env and {} not found in libsel4 include path",
var,
relative_path.display(),
)
})
}
2 changes: 1 addition & 1 deletion crates/sel4/src/object.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ impl From<ObjectTypeArch> for ObjectType {
}
}

/// An object description for [`Untyped::untyped_retype`](crate::Untyped::untyped_retype).
/// An object description for [`Untyped::untyped_retype`](crate::cap::Untyped::untyped_retype).
#[sel4_cfg_enum]
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub enum ObjectBlueprint {
Expand Down
4 changes: 2 additions & 2 deletions crates/sel4/src/syscalls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -247,14 +247,14 @@ pub fn set_tls_base(addr: usize) {

const UNUSED_FOR_IN: Word = 0;

/// The result of [`Endpoint::recv_with_mrs`].
/// The result of [`cap::Endpoint::recv_with_mrs`].
pub struct RecvWithMRs {
pub info: MessageInfo,
pub badge: Badge,
pub msg: [Word; NUM_FAST_MESSAGE_REGISTERS],
}

/// The result of [`Endpoint::call_with_mrs`].
/// The result of [`cap::Endpoint::call_with_mrs`].
pub struct CallWithMRs {
pub info: MessageInfo,
pub msg: [Word; NUM_FAST_MESSAGE_REGISTERS],
Expand Down
16 changes: 4 additions & 12 deletions crates/sel4/sys/build/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,7 @@ use std::path::{Path, PathBuf};
use glob::glob;
use proc_macro2::TokenStream;

use sel4_build_env::{
find_in_libsel4_include_dirs, get_libsel4_include_dirs, get_or_find_in_libsel4_include_dirs,
};
use sel4_build_env::{find_in_libsel4_include_dirs, get_libsel4_include_dirs};
use sel4_rustfmt_helper::Rustfmt;

mod bf;
Expand Down Expand Up @@ -48,15 +46,9 @@ fn main() {
{
let interface_definition_files = vec![
// order must be consistent with C libsel4
get_or_find_in_libsel4_include_dirs("SEL4_OBJECT_API", "interfaces/object-api.xml"),
get_or_find_in_libsel4_include_dirs(
"SEL4_OBJECT_API_SEL4_ARCH",
"interfaces/object-api-sel4-arch.xml",
),
get_or_find_in_libsel4_include_dirs(
"SEL4_OBJECT_API_ARCH",
"interfaces/object-api-arch.xml",
),
find_in_libsel4_include_dirs("interfaces/object-api.xml"),
find_in_libsel4_include_dirs("interfaces/object-api-sel4-arch.xml"),
find_in_libsel4_include_dirs("interfaces/object-api-arch.xml"),
];

let (invocation_labels_fragment, invocations_fragment) = xml::invocations::generate_rust(
Expand Down
4 changes: 3 additions & 1 deletion hacking/cargo-manifest-management/manifest-scope.nix
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,9 @@ in rec {

ringWith = features: {
version = "=0.17.8";
features = [ "less-safe-getrandom-custom-or-rdrand" ] ++ features;
features = [
"less-safe-getrandom-custom-or-rdrand"
] ++ features;
};

rustlsWith = features: {
Expand Down
16 changes: 15 additions & 1 deletion hacking/nix/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,21 @@ let
inherit lib pkgs;
} // import ./top-level self);

this = makeOverridableWith lib.id mkThis baseArgs;
this = lib.fix (self: makeOverridableWith lib.id mkThis baseArgs // rec {
overrideNixpkgsArgs = f: self.override (superArgs: selfBase:
let
concreteSuperArgs = superArgs selfBase;
in
concreteSuperArgs // {
nixpkgsArgsFor = crossSystem: f (concreteSuperArgs.nixpkgsArgsFor crossSystem);
}
);
withOverlays = overlays: self.overrideNixpkgsArgs (superNixpkgsArgs:
superNixpkgsArgs // {
overlays = superNixpkgsArgs.overlays ++ overlays;
}
);
});

in
this
12 changes: 5 additions & 7 deletions hacking/nix/scope/crates.nix
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ let

globalPatchSection = workspaceManifest.patch;

overrides = {
overridesForMkCrate = {
sel4-sys = {
extraPaths = [
"build"
Expand Down Expand Up @@ -59,13 +59,11 @@ let
};

unAugmentedCrates = lib.listToAttrs (lib.forEach workspaceMemberPaths (cratePath: rec {
name = (crateUtils.crateManifest cratePath).package.name; # TODO redundant
value = crateUtils.mkCrate cratePath (overrides.${name} or {});
name = (crateUtils.crateManifest cratePath).package.name;
value = crateUtils.mkCrate cratePath (overridesForMkCrate.${name} or {});
}));

augmentedCrates = crateUtils.augmentCrates unAugmentedCrates;

crates = augmentedCrates;
crates = crateUtils.augmentCrates unAugmentedCrates;

isPrivate = crateName: builtins.match "^sel4-.*" crateName == null;

Expand All @@ -75,5 +73,5 @@ let
(lib.concatMapStrings (crateName: "${crateName}\n") (lib.attrNames publicCrates));

in {
inherit crates globalPatchSection publicCrates publicCratesTxt;
inherit crates overridesForMkCrate globalPatchSection publicCrates publicCratesTxt;
}
3 changes: 2 additions & 1 deletion hacking/nix/scope/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,8 @@ superCallPackage ../rust-utils {} self //
{ name = fname; path = builtins.toFile fname (builtins.readFile "${dir}/${fname}"); }
];

inherit (callPackage ./crates.nix {}) crates globalPatchSection publicCrates publicCratesTxt;
inherit (callPackage ./crates.nix {})
crates overridesForMkCrate globalPatchSection publicCrates publicCratesTxt;

distribution = callPackage ./distribution.nix {};

Expand Down
2 changes: 1 addition & 1 deletion hacking/nix/scope/microkit/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -73,9 +73,9 @@ let
--sel4=${kernelSourcePatched} \
--boards ${board} \
--configs ${config} \
--skip-tool \
--skip-docs \
--skip-tar
'';

installPhase = ''
Expand Down
Loading

0 comments on commit 3589567

Please sign in to comment.