Compare commits

..

7 commits

Author SHA1 Message Date
Cesar Strauss 3771cea78e
Gather the FIFO debug ports in a bundle
All checks were successful
/ deps (pull_request) Successful in 15s
/ test (pull_request) Successful in 3m35s
/ deps (push) Successful in 16s
/ test (push) Successful in 3m59s
2024-12-29 13:17:24 -03:00
Cesar Strauss dcf865caec
Add assertions and debug ports in order for the FIFO to pass induction
As some proofs involving memories, it is necessary to add more ports to
the queue interface, to sync state. These changes are predicated on the
test environment, so normal use is not affected.

Since some speedup is achieved, use the saved time to test with a deeper
FIFO.
2024-12-29 13:12:58 -03:00
Cesar Strauss 31d01046a8
Initial queue formal proof based on one-entry FIFO equivalence
For now, only check that the basic properties work in bounded model check
mode, leave the induction proof for later.

Partially replace the previously existing proof.

Remove earlier assumptions and bounds that don't apply for this proof.

Use parameterized types instead of hard-coded types.
2024-12-29 13:04:01 -03:00
Jacob Lifshay c16726cee6
fix #[hdl]/#[hdl_module] attributes getting the wrong hygiene when processing #[cfg]s
All checks were successful
/ deps (pull_request) Successful in 17s
/ test (pull_request) Successful in 5m13s
/ deps (push) Successful in 14s
/ test (push) Successful in 5m42s
2024-12-29 00:48:15 -08:00
Jacob Lifshay b63676d0ca
add test for cfgs
All checks were successful
/ deps (pull_request) Successful in 18s
/ test (pull_request) Successful in 5m23s
/ deps (push) Successful in 14s
/ test (push) Successful in 6m5s
2024-12-28 23:39:50 -08:00
Jacob Lifshay 7005fa3330
implement handling #[cfg] and #[cfg_attr] in proc macro inputs 2024-12-28 23:39:08 -08:00
Jacob Lifshay 2ab8428062
upgrade syn version 2024-12-28 23:39:08 -08:00
8 changed files with 3010 additions and 16 deletions

8
Cargo.lock generated
View file

@ -543,9 +543,9 @@ dependencies = [
[[package]]
name = "proc-macro2"
version = "1.0.83"
version = "1.0.92"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b33eb56c327dec362a9e55b3ad14f9d2f0904fb5a5b03b513ab5465399e9f43"
checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0"
dependencies = [
"unicode-ident",
]
@ -647,9 +647,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
[[package]]
name = "syn"
version = "2.0.66"
version = "2.0.93"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5"
checksum = "9c786062daee0d6db1132800e623df74274a0a87322d8e183338e01b3d98d058"
dependencies = [
"proc-macro2",
"quote",

View file

@ -37,7 +37,7 @@ quote = "1.0.36"
serde = { version = "1.0.202", features = ["derive"] }
serde_json = { version = "1.0.117", features = ["preserve_order"] }
sha2 = "0.10.8"
syn = { version = "2.0.66", features = ["full", "fold", "visit", "extra-traits"] }
syn = { version = "2.0.93", features = ["full", "fold", "visit", "extra-traits"] }
tempfile = "3.10.1"
thiserror = "1.0.61"
trybuild = "1.0"

View file

@ -3,14 +3,20 @@
#![cfg_attr(test, recursion_limit = "512")]
use proc_macro2::{Span, TokenStream};
use quote::{quote, ToTokens};
use std::io::{ErrorKind, Write};
use std::{
collections::{hash_map::Entry, HashMap},
io::{ErrorKind, Write},
};
use syn::{
bracketed, parenthesized,
bracketed,
ext::IdentExt,
parenthesized,
parse::{Parse, ParseStream, Parser},
parse_quote,
punctuated::Pair,
punctuated::{Pair, Punctuated},
spanned::Spanned,
AttrStyle, Attribute, Error, Item, ItemFn, Token,
token::{Bracket, Paren},
AttrStyle, Attribute, Error, Ident, Item, ItemFn, LitBool, LitStr, Meta, Token,
};
mod fold;
@ -19,6 +25,7 @@ mod hdl_enum;
mod hdl_type_alias;
mod hdl_type_common;
mod module;
mod process_cfg;
pub(crate) trait CustomToken:
Copy
@ -59,6 +66,11 @@ mod kw {
};
}
custom_keyword!(__evaluated_cfgs);
custom_keyword!(all);
custom_keyword!(any);
custom_keyword!(cfg);
custom_keyword!(cfg_attr);
custom_keyword!(clock_domain);
custom_keyword!(connect_inexact);
custom_keyword!(custom_bounds);
@ -75,6 +87,7 @@ mod kw {
custom_keyword!(no_reset);
custom_keyword!(no_runtime_generics);
custom_keyword!(no_static);
custom_keyword!(not);
custom_keyword!(outline_generated);
custom_keyword!(output);
custom_keyword!(reg_builder);
@ -901,15 +914,346 @@ fn hdl_module_impl(item: ItemFn) -> syn::Result<TokenStream> {
Ok(contents)
}
pub fn hdl_module(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
let kw = kw::hdl_module::default();
hdl_module_impl(syn::parse2(quote! { #[#kw(#attr)] #item })?)
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) enum CfgExpr {
Option {
ident: Ident,
value: Option<(Token![=], LitStr)>,
},
All {
all: kw::all,
paren: Paren,
exprs: Punctuated<CfgExpr, Token![,]>,
},
Any {
any: kw::any,
paren: Paren,
exprs: Punctuated<CfgExpr, Token![,]>,
},
Not {
not: kw::not,
paren: Paren,
expr: Box<CfgExpr>,
trailing_comma: Option<Token![,]>,
},
}
pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
let kw = kw::hdl::default();
let item = quote! { #[#kw(#attr)] #item };
let item = syn::parse2::<Item>(item)?;
impl Parse for CfgExpr {
fn parse(input: ParseStream) -> syn::Result<Self> {
match input.cursor().ident() {
Some((_, cursor)) if cursor.eof() => {
return Ok(CfgExpr::Option {
ident: input.call(Ident::parse_any)?,
value: None,
});
}
_ => {}
}
if input.peek(Ident::peek_any) && input.peek2(Token![=]) {
return Ok(CfgExpr::Option {
ident: input.call(Ident::parse_any)?,
value: Some((input.parse()?, input.parse()?)),
});
}
let contents;
if input.peek(kw::all) {
Ok(CfgExpr::All {
all: input.parse()?,
paren: parenthesized!(contents in input),
exprs: contents.call(Punctuated::parse_terminated)?,
})
} else if input.peek(kw::any) {
Ok(CfgExpr::Any {
any: input.parse()?,
paren: parenthesized!(contents in input),
exprs: contents.call(Punctuated::parse_terminated)?,
})
} else if input.peek(kw::not) {
Ok(CfgExpr::Not {
not: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
trailing_comma: contents.parse()?,
})
} else {
Err(input.error("expected cfg-pattern"))
}
}
}
impl ToTokens for CfgExpr {
fn to_tokens(&self, tokens: &mut TokenStream) {
match self {
CfgExpr::Option { ident, value } => {
ident.to_tokens(tokens);
if let Some((eq, value)) = value {
eq.to_tokens(tokens);
value.to_tokens(tokens);
}
}
CfgExpr::All { all, paren, exprs } => {
all.to_tokens(tokens);
paren.surround(tokens, |tokens| exprs.to_tokens(tokens));
}
CfgExpr::Any { any, paren, exprs } => {
any.to_tokens(tokens);
paren.surround(tokens, |tokens| exprs.to_tokens(tokens));
}
CfgExpr::Not {
not,
paren,
expr,
trailing_comma,
} => {
not.to_tokens(tokens);
paren.surround(tokens, |tokens| {
expr.to_tokens(tokens);
trailing_comma.to_tokens(tokens);
});
}
}
}
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) struct Cfg {
cfg: kw::cfg,
paren: Paren,
expr: CfgExpr,
trailing_comma: Option<Token![,]>,
}
impl Cfg {
fn parse_meta(meta: &Meta) -> syn::Result<Self> {
syn::parse2(meta.to_token_stream())
}
}
impl ToTokens for Cfg {
fn to_tokens(&self, tokens: &mut TokenStream) {
let Self {
cfg,
paren,
expr,
trailing_comma,
} = self;
cfg.to_tokens(tokens);
paren.surround(tokens, |tokens| {
expr.to_tokens(tokens);
trailing_comma.to_tokens(tokens);
});
}
}
impl Parse for Cfg {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
Ok(Self {
cfg: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
trailing_comma: contents.parse()?,
})
}
}
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub(crate) struct CfgAttr {
cfg_attr: kw::cfg_attr,
paren: Paren,
expr: CfgExpr,
comma: Token![,],
attrs: Punctuated<Meta, Token![,]>,
}
impl CfgAttr {
pub(crate) fn to_cfg(&self) -> Cfg {
Cfg {
cfg: kw::cfg(self.cfg_attr.span),
paren: self.paren,
expr: self.expr.clone(),
trailing_comma: None,
}
}
fn parse_meta(meta: &Meta) -> syn::Result<Self> {
syn::parse2(meta.to_token_stream())
}
}
impl Parse for CfgAttr {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
Ok(Self {
cfg_attr: input.parse()?,
paren: parenthesized!(contents in input),
expr: contents.parse()?,
comma: contents.parse()?,
attrs: contents.call(Punctuated::parse_terminated)?,
})
}
}
pub(crate) struct CfgAndValue {
cfg: Cfg,
eq_token: Token![=],
value: LitBool,
}
impl Parse for CfgAndValue {
fn parse(input: ParseStream) -> syn::Result<Self> {
Ok(Self {
cfg: input.parse()?,
eq_token: input.parse()?,
value: input.parse()?,
})
}
}
pub(crate) struct Cfgs<T> {
pub(crate) bracket: Bracket,
pub(crate) cfgs_map: HashMap<Cfg, T>,
pub(crate) cfgs_list: Vec<Cfg>,
}
impl<T> Default for Cfgs<T> {
fn default() -> Self {
Self {
bracket: Default::default(),
cfgs_map: Default::default(),
cfgs_list: Default::default(),
}
}
}
impl<T> Cfgs<T> {
fn insert_cfg(&mut self, cfg: Cfg, value: T) {
match self.cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
self.cfgs_list.push(entry.key().clone());
entry.insert(value);
}
}
}
}
impl Parse for Cfgs<bool> {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
let bracket = bracketed!(contents in input);
let mut cfgs_map = HashMap::new();
let mut cfgs_list = Vec::new();
for CfgAndValue {
cfg,
eq_token,
value,
} in contents.call(Punctuated::<CfgAndValue, Token![,]>::parse_terminated)?
{
let _ = eq_token;
match cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
cfgs_list.push(entry.key().clone());
entry.insert(value.value);
}
}
}
Ok(Self {
bracket,
cfgs_map,
cfgs_list,
})
}
}
impl Parse for Cfgs<()> {
fn parse(input: ParseStream) -> syn::Result<Self> {
let contents;
let bracket = bracketed!(contents in input);
let mut cfgs_map = HashMap::new();
let mut cfgs_list = Vec::new();
for cfg in contents.call(Punctuated::<Cfg, Token![,]>::parse_terminated)? {
match cfgs_map.entry(cfg) {
Entry::Occupied(_) => {}
Entry::Vacant(entry) => {
cfgs_list.push(entry.key().clone());
entry.insert(());
}
}
}
Ok(Self {
bracket,
cfgs_map,
cfgs_list,
})
}
}
impl ToTokens for Cfgs<()> {
fn to_tokens(&self, tokens: &mut TokenStream) {
let Self {
bracket,
cfgs_map: _,
cfgs_list,
} = self;
bracket.surround(tokens, |tokens| {
for cfg in cfgs_list {
cfg.to_tokens(tokens);
<Token![,]>::default().to_tokens(tokens);
}
});
}
}
fn hdl_main(
kw: impl CustomToken,
attr: TokenStream,
item: TokenStream,
) -> syn::Result<TokenStream> {
fn parse_evaluated_cfgs_attr<R>(
input: ParseStream,
parse_inner: impl FnOnce(ParseStream) -> syn::Result<R>,
) -> syn::Result<R> {
let _: Token![#] = input.parse()?;
let bracket_content;
bracketed!(bracket_content in input);
let _: kw::__evaluated_cfgs = bracket_content.parse()?;
let paren_content;
parenthesized!(paren_content in bracket_content);
parse_inner(&paren_content)
}
let (evaluated_cfgs, item): (_, TokenStream) = Parser::parse2(
|input: ParseStream| {
let peek = input.fork();
if parse_evaluated_cfgs_attr(&peek, |_| Ok(())).is_ok() {
let evaluated_cfgs = parse_evaluated_cfgs_attr(input, Cfgs::<bool>::parse)?;
Ok((Some(evaluated_cfgs), input.parse()?))
} else {
Ok((None, input.parse()?))
}
},
item,
)?;
let cfgs = if let Some(cfgs) = evaluated_cfgs {
cfgs
} else {
let cfgs = process_cfg::collect_cfgs(syn::parse2(item.clone())?)?;
if cfgs.cfgs_list.is_empty() {
Cfgs::default()
} else {
return Ok(quote! {
::fayalite::__cfg_expansion_helper! {
[]
#cfgs
{#[::fayalite::#kw(#attr)]} { #item }
}
});
}
};
let item = syn::parse2(quote! { #[#kw(#attr)] #item })?;
let Some(item) = process_cfg::process_cfgs(item, cfgs)? else {
return Ok(TokenStream::new());
};
match item {
Item::Enum(item) => hdl_enum::hdl_enum(item),
Item::Struct(item) => hdl_bundle::hdl_bundle(item),
@ -921,3 +1265,11 @@ pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream
)),
}
}
pub fn hdl_module(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
hdl_main(kw::hdl_module::default(), attr, item)
}
pub fn hdl_attr(attr: TokenStream, item: TokenStream) -> syn::Result<TokenStream> {
hdl_main(kw::hdl::default(), attr, item)
}

File diff suppressed because it is too large Load diff

View file

@ -5,6 +5,9 @@ use std::{env, fs, path::Path};
fn main() {
println!("cargo::rustc-check-cfg=cfg(todo)");
println!("cargo::rustc-check-cfg=cfg(cfg_false_for_tests)");
println!("cargo::rustc-check-cfg=cfg(cfg_true_for_tests)");
println!("cargo::rustc-cfg=cfg_true_for_tests");
let path = "visit_types.json";
println!("cargo::rerun-if-changed={path}");
println!("cargo::rerun-if-changed=build.rs");

View file

@ -11,6 +11,59 @@ extern crate self as fayalite;
#[doc(hidden)]
pub use std as __std;
#[doc(hidden)]
#[macro_export]
macro_rules! __cfg_expansion_helper {
(
[
$($evaluated_cfgs:ident($($evaluated_exprs:tt)*) = $evaluated_results:ident,)*
]
[
$cfg:ident($($expr:tt)*),
$($unevaluated_cfgs:ident($($unevaluated_exprs:tt)*),)*
]
// pass as tt so we get right span for attribute
$after_evaluation_attr:tt $after_evaluation_body:tt
) => {
#[$cfg($($expr)*)]
$crate::__cfg_expansion_helper! {
[
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
$cfg($($expr)*) = true,
]
[
$($unevaluated_cfgs($($unevaluated_exprs)*),)*
]
$after_evaluation_attr $after_evaluation_body
}
#[$cfg(not($($expr)*))]
$crate::__cfg_expansion_helper! {
[
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
$cfg($($expr)*) = false,
]
[
$($unevaluated_cfgs($($unevaluated_exprs)*),)*
]
$after_evaluation_attr $after_evaluation_body
}
};
(
[
$($evaluated_cfgs:ident($($evaluated_exprs:tt)*) = $evaluated_results:ident,)*
]
[]
// don't use #[...] so we get right span for `#` and `[]` of attribute
{$($after_evaluation_attr:tt)*} {$($after_evaluation_body:tt)*}
) => {
$($after_evaluation_attr)*
#[__evaluated_cfgs([
$($evaluated_cfgs($($evaluated_exprs)*) = $evaluated_results,)*
])]
$($after_evaluation_body)*
};
}
#[doc(inline)]
/// The `#[hdl_module]` attribute is applied to a Rust function so that that function creates
/// a [`Module`][`::fayalite::module::Module`] when called.

View file

@ -50,6 +50,7 @@ impl<T: Type> ReadyValid<T> {
}
/// This debug port is only meant to assist the formal proof of the queue.
#[cfg(test)]
#[doc(hidden)]
#[hdl]
pub struct QueueDebugPort<Element, Index> {

View file

@ -4287,3 +4287,61 @@ circuit check_deduce_resets:
",
};
}
// intentionally not outline_generated to ensure we get correct macro hygiene
#[hdl_module]
pub fn check_cfgs<#[cfg(cfg_false_for_tests)] A: Type, #[cfg(cfg_true_for_tests)] B: Type>(
#[cfg(cfg_false_for_tests)] a: A,
#[cfg(cfg_true_for_tests)] b: B,
) {
#[hdl]
struct S<#[cfg(cfg_false_for_tests)] A, #[cfg(cfg_true_for_tests)] B> {
#[cfg(cfg_false_for_tests)]
a: A,
#[cfg(cfg_true_for_tests)]
b: B,
}
#[hdl]
#[cfg(cfg_false_for_tests)]
let i_a: A = m.input(a);
#[hdl]
#[cfg(cfg_true_for_tests)]
let i_b: B = m.input(b);
#[hdl]
let w: S<UInt<8>> = wire();
#[cfg(cfg_false_for_tests)]
{
#[hdl]
let o_a: A = m.output(a);
connect(o_a, w.a.cast_bits_to(a));
connect_any(w.a, i_a.cast_to_bits());
}
#[cfg(cfg_true_for_tests)]
{
#[hdl]
let o_b: B = m.output(b);
connect(o_b, w.b.cast_bits_to(b));
connect_any(w.b, i_b.cast_to_bits());
}
}
#[test]
fn test_cfgs() {
let _n = SourceLocation::normalize_files_for_tests();
let m = check_cfgs(UInt[8]);
dbg!(m);
#[rustfmt::skip] // work around https://github.com/rust-lang/rustfmt/issues/6161
assert_export_firrtl! {
m =>
"/test/check_cfgs.fir": r"FIRRTL version 3.2.0
circuit check_cfgs:
type Ty0 = {b: UInt<8>}
module check_cfgs: @[the_test_file.rs 9962:1]
input i_b: UInt<8> @[the_test_file.rs 9979:20]
output o_b: UInt<8> @[the_test_file.rs 9992:24]
wire w: Ty0 @[the_test_file.rs 9981:25]
connect o_b, w.b @[the_test_file.rs 9993:9]
connect w.b, i_b @[the_test_file.rs 9994:9]
",
};
}