Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .github/workflows/ml-kem.yml
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,15 @@ jobs:
- run: cargo test
- run: cargo test --all-features

checkct:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: Ledger-Donjon/cargo-checkct@85271e5ce9eab9ba895c62c8b5d4129810a635a0
with:
directory: ml-kem
timeout: 120

cross:
needs: set-msrv
strategy:
Expand Down
20 changes: 20 additions & 0 deletions ml-kem/checkct/.cargo/config.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
[build]
target = [
# TODO(tarcieri): investigate codegen problems on commented out platforms
#"riscv32imac-unknown-none-elf",
#"thumbv6m-none-eabi",
"thumbv7em-none-eabihf",
#"x86_64-unknown-linux-gnu",
]

[target.x86_64-unknown-linux-gnu]
rustflags = [
"-C", "linker=rust-lld",
"-C", "linker-flavor=ld.lld",
"-C", "relocation-model=static",
]

[unstable]
unstable-options = true
build-std = ["core", "panic_abort"]
build-std-features = ["compiler-builtins-mem"]
1 change: 1 addition & 0 deletions ml-kem/checkct/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
/target/
231 changes: 231 additions & 0 deletions ml-kem/checkct/Cargo.lock

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

10 changes: 10 additions & 0 deletions ml-kem/checkct/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
[workspace]
members = ["driver"]
resolver = "2"

[profile.release]
debug = true
panic = "abort"

[patch.crates-io]
module-lattice = { path = "../../module-lattice" }
14 changes: 14 additions & 0 deletions ml-kem/checkct/checkct_macros/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#----- AUTOGENERATED BY CARGO-CHECKCT: DO NOT MODIFY -----
[package]
name = "checkct_macros"
version = "0.1.0"
publish = false
edition = "2021"

[lib]
proc-macro = true

[dependencies]
proc-macro2 = "1.0.86"
quote = "1.0.37"
syn = { version = "2.0.77", features = ["full"] }
91 changes: 91 additions & 0 deletions ml-kem/checkct/checkct_macros/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,91 @@
use proc_macro::TokenStream;
use proc_macro2::{Literal, Span};
use quote::quote;
use syn::{
parse::{Parse, ParseStream},
parse_macro_input, Error, Ident, ItemFn, LitStr, Result, Token,
};

struct AttributeArgs {
descriptor_link_section: Option<String>,
}

impl Parse for AttributeArgs {
fn parse(input: ParseStream) -> Result<Self> {
if input.is_empty() {
return Ok(Self {
descriptor_link_section: None,
});
}

let arg_name: Ident = input.parse()?;
if arg_name != "descriptor_link_section" {
return Err(Error::new(
arg_name.span(),
"expected `descriptor_link_section`",
));
}
input.parse::<Token![=]>()?;
let descriptor_link_section: LitStr = input.parse()?;

Ok(Self {
descriptor_link_section: Some(descriptor_link_section.value()),
})
}
}

#[proc_macro_attribute]
pub fn checkct(args: TokenStream, input: TokenStream) -> TokenStream {
let args = parse_macro_input!(args as AttributeArgs);
// By default the descriptor will be stored in the .note.checkct section
let descriptor_link_section = Literal::string(
args.descriptor_link_section
.as_deref()
.unwrap_or(".note.checkct"),
);

let item_fn = parse_macro_input!(input as ItemFn);
let name = &item_fn.sig.ident;

let entrypoint_descriptor_name = Ident::new(
&format!("__checkct_entrypoint_descriptor__{name}"),
Span::call_site(),
);
let entrypoint_descriptor_type = Ident::new(
&format!("__CheckctEntrypointDescriptor__{name}"),
Span::call_site(),
);

quote! {
// The descriptor is laid out as an ELF note (which binsec parses), since it is stored
// in a note section by default. It ends with the address of the entrypoint.
#[doc(hidden)]
#[allow(non_camel_case_types, dead_code)]
#[repr(C, packed(4))]
pub struct #entrypoint_descriptor_type {
namesz: u32,
descsz: u32,
kind: u32,
name: [u8; 8],
entrypoint: fn(),
}

// This variable is used to prevent the compiler from removing the code of the entrypoint
// function if it is unused. Moreover this variable name has a special format which allows
// cargo-checkct to find it.
// Make sure that the descriptor link section is kept by the linker.
#[unsafe(link_section = #descriptor_link_section)]
#[used]
pub static #entrypoint_descriptor_name: #entrypoint_descriptor_type =
#entrypoint_descriptor_type {
namesz: 8,
descsz: ::core::mem::size_of::<fn()>() as u32,
kind: 1,
name: *b"checkct\0",
entrypoint: #name,
};

#item_fn
}
.into()
}
Loading
Loading