merge main

Author: UnsignedByte

Cargo.toml

@@ -34,6 +34,8 @@ lazy_static = "1.4"
 easy-smt = "0.2.3"
 struct-variant = "1.0"
 tempfile = "3.13.0"
+strum = "0.26.3"
+strum_macros = "0.26.3"
 
 fil-utils = { version = "0.1.0", path = "crates/utils" }
 fil-ast = { version = "0.1.0", path = "crates/ast" }

crates/ast/Cargo.toml

@@ -22,10 +22,8 @@ lazy_static.workspace = true
 struct-variant.workspace = true
 pest.workspace = true
 pest_consume.workspace = true
+strum_macros.workspace = true
+strum.workspace = true
 
 fil-utils.workspace = true
-fil-gen.workspace = true
-strum = "0.26.3"
-strum_macros = "0.26.3"
-enumflags2 = "0.7.10"
-enum-map = "2.7.3"
+fil-gen.workspace = true

crates/ast/src/attribute.rs

@@ -1,7 +1,6 @@
-use crate::BoolAttr;
-
 use super::{Command, Id, Signature};
 use fil_gen as gen;
+use fil_utils::{self as utils, AttrCtx};
 use gen::GenConfig;
 use std::path::PathBuf;
 
@@ -96,7 +95,7 @@ impl Namespace {
     pub fn main_idx(&self) -> Option<usize> {
         self.components
             .iter()
-            .position(|c| c.sig.attributes.has(BoolAttr::TopLevel))
+            .position(|c| c.sig.attributes.has(utils::CompBool::TopLevel))
     }
 
     /// Get the toplevel component name

crates/ast/src/component.rs

@@ -1,4 +1,3 @@
-mod attribute;
 mod bind_map;
 mod component;
 mod constraint;
@@ -12,7 +11,6 @@ mod port;
 mod signature;
 mod time;
 
-pub use attribute::{Attr, Attributes, BoolAttr, NumAttr};
 pub use bind_map::Binding;
 pub use component::{Component, Extern, Namespace};
 pub use constraint::{Constraint, OrderConstraint, OrderOp};

crates/ast/src/lib.rs

@@ -2,13 +2,16 @@
 #![allow(clippy::type_complexity)]
 
 //! Parser for Filament programs.
-use crate::{self as ast, Attributes, Loc, TimeSub};
-use fil_utils::{self as utils, FilamentResult};
-use fil_utils::{FileIdx, GPosIdx, GlobalPositionTable};
+use crate::{self as ast, Loc, TimeSub};
+use fil_utils::{
+    self as utils, AttrCtx, FilamentResult, FileIdx, GPosIdx,
+    GlobalPositionTable,
+};
 use itertools::Itertools;
 use pest::pratt_parser::{Assoc, Op, PrattParser};
 use pest_consume::{match_nodes, Error, Parser};
 use std::fs;
+use std::hash::Hash;
 use std::path::Path;
 use std::str::FromStr;
 
@@ -830,29 +833,30 @@ impl FilamentParser {
         Ok(())
     }
 
-    fn attr_bind(input: Node) -> ParseResult<Vec<(ast::Attr, GPosIdx, u64)>> {
-        match_nodes!(
-            input.clone().into_children();
-            [identifier(name)] =>
-            ast::BoolAttr::from_str(name.as_ref()).map(
-                |attr| vec![(ast::Attr::Bool(attr), name.pos(), 1)]).map_err(
-                    |_| input.error(format!("Found unknown attribute flag \"{name}\""))),
-            [not(_), identifier(name)] =>
-            ast::BoolAttr::from_str(name.as_ref()).map(
-                |attr| vec![(ast::Attr::Bool(attr), name.pos(), 0)]).map_err(
-                    |_| input.error(format!("Found unknown attribute flag \"{name}\""))),
-            [identifier(name), bitwidth(val)] =>
-            ast::NumAttr::from_str(name.as_ref()).map(
-                |attr| vec![(ast::Attr::Num(attr), name.pos(), val)]).map_err(
-                    |_| input.error(format!("Found unknown numeric attribute \"{name}\""))),
-        )
-    }
+    fn attributes<Bool, Num>(
+        input: Node,
+    ) -> ParseResult<utils::Attributes<Bool, Num>>
+    where
+        Bool: FromStr + Hash + Eq + Copy,
+        Num: FromStr + Hash + Eq + Copy,
+    {
+        let mut attrs = utils::Attributes::default();
+        for attr in input.into_children() {
+            match_nodes!(
+                attr.clone().into_children();
+                [identifier(name)] => Bool::from_str(name.as_ref()).map(
+                    |attr| attrs.set(attr, true, name.pos())).map_err(
+                        |_| attr.error(format!("Found unknown attribute flag \"{name}\""))),
+                [not(_), identifier(name)] => Bool::from_str(name.as_ref()).map(
+                    |attr| attrs.set(attr, false, name.pos())).map_err(
+                        |_| attr.error(format!("Found unknown attribute flag \"{name}\""))),
+                [identifier(name), bitwidth(val)] => Num::from_str(name.as_ref()).map(
+                    |attr| attrs.set(attr, val, name.pos())).map_err(
+                        |_| attr.error(format!("Found unknown numeric attribute \"{name}\""))),
+            )?;
+        }
 
-    fn attributes(input: Node) -> ParseResult<Attributes> {
-        Ok(match_nodes!(
-            input.into_children();
-            [attr_bind(attr)..] => ast::Attributes::new(attr.into_iter().flatten())
-        ))
+        Ok(attrs)
     }
 
     fn component(input: Node) -> ParseResult<ast::Component> {

crates/ast/src/parser.rs

@@ -2,8 +2,7 @@ use super::{
     Binding, Expr, Id, InterfaceDef, Loc, OrderConstraint, PortDef, Time,
     TimeSub,
 };
-use crate::Attributes;
-use fil_utils::GPosIdx;
+use fil_utils::{CompAttrs, GPosIdx};
 
 #[derive(Clone)]
 /// An event variable bound in the signature
@@ -113,7 +112,7 @@ pub struct Signature {
     /// Name of the component
     pub name: Loc<Id>,
     /// Attributes associated with this component
-    pub attributes: Attributes,
+    pub attributes: CompAttrs,
     /// Parameters for the Signature
     pub params: Vec<Loc<ParamBind>>,
     /// Parameters bound in the signature binding. These always have a default value.
@@ -139,7 +138,7 @@ impl Signature {
     #[allow(clippy::too_many_arguments)]
     pub fn new(
         name: Loc<Id>,
-        attributes: Attributes,
+        attributes: CompAttrs,
         params: Vec<Loc<ParamBind>>,
         events: Vec<Loc<EventBind>>,
         unannotated_ports: Vec<(Id, u64)>,

crates/ast/src/signature.rs

@@ -1,6 +1,6 @@
 use crate::ast_visitor::{Action, Visitor};
 use fil_ast as ast;
-use fil_utils::{Diagnostics, Error, GPosIdx};
+use fil_utils::{self as utils, AttrCtx, Diagnostics, Error, GPosIdx};
 
 /// Sets the proper FSM Attributes for every component
 #[derive(Default)]
@@ -17,7 +17,7 @@ impl Visitor for TopLevel {
     }
 
     fn signature(&mut self, sig: &mut ast::Signature) -> Action {
-        if sig.attributes.get(ast::BoolAttr::TopLevel) == Some(1) {
+        if sig.attributes.get(utils::CompBool::TopLevel) == Some(&true) {
             if self.has_toplevel.is_some() {
                 let err = Error::malformed("Multiple top-level components")
                     .add_note(self.diag.add_info(
@@ -28,15 +28,15 @@ impl Visitor for TopLevel {
                         self.diag.add_info(
                             "second top-level component here",
                             sig.attributes
-                                .get_loc(ast::BoolAttr::TopLevel)
+                                .get_loc(utils::CompBool::TopLevel)
                                 .unwrap(),
                         ),
                     );
 
                 self.diag.add_error(err);
             } else {
                 self.has_toplevel = Some(
-                    sig.attributes.get_loc(ast::BoolAttr::TopLevel).unwrap(),
+                    sig.attributes.get_loc(utils::CompBool::TopLevel).unwrap(),
                 );
             }
         }
@@ -47,14 +47,14 @@ impl Visitor for TopLevel {
 
     fn external(&mut self, ext: &mut ast::Extern) {
         for sig in &mut ext.comps {
-            if sig.attributes.get(ast::BoolAttr::TopLevel) == Some(1) {
+            if sig.attributes.get(utils::CompBool::TopLevel) == Some(&true) {
                 let err =
                     Error::malformed("External components cannot be top-level")
                         .add_note(
                             self.diag.add_info(
                                 "toplevel attribute here",
                                 sig.attributes
-                                    .get_loc(ast::BoolAttr::TopLevel)
+                                    .get_loc(utils::CompBool::TopLevel)
                                     .unwrap(),
                             ),
                         );
@@ -74,7 +74,11 @@ impl Visitor for TopLevel {
             for comp in ast.components.iter_mut() {
                 if comp.sig.name.as_ref() == "main" {
                     // Add the toplevel attribute to the component
-                    comp.sig.attributes.set(ast::BoolAttr::TopLevel, 1);
+                    comp.sig.attributes.set(
+                        utils::CompBool::TopLevel,
+                        true,
+                        GPosIdx::UNKNOWN,
+                    );
 
                     return;
                 }

crates/filament/src/ast_passes/toplevel.rs

@@ -459,6 +459,10 @@ impl Discharge {
                 self.diagnostics.push(diag);
                 return;
             };
+            log::debug!(
+                "Cannot prove constraint: {}",
+                ctx.display(fact.prop.consequent(ctx))
+            );
             let mut diag = reason.diag(ctx);
             if self.show_models {
                 diag = reason.diag(ctx).with_notes(vec![format!(

crates/filament/src/ir_passes/discharge.rs

@@ -1,6 +1,6 @@
 use crate::ir_visitor::{Action, Visitor, VisitorData};
-use fil_ast as ast;
 use fil_ir::TimeSub;
+use fil_utils::{self as utils, AttrCtx};
 
 /// Sets the proper FSM Attributes for every component
 #[derive(Default)]
@@ -15,7 +15,7 @@ impl Visitor for FSMAttributes {
         let attrs = &data.comp.attrs;
 
         // Check if the component already has FSM attributes
-        if attrs.get(ast::BoolAttr::CounterFSM).is_some() {
+        if attrs.get(utils::CompBool::CounterFSM).is_some() {
             return Action::Stop;
         }
 
@@ -37,12 +37,20 @@ impl Visitor for FSMAttributes {
             // If the delay is > 1, add a slow FSM attribute
             // TODO(UnsignedByte): Find a better heuristic for slow FSMs
             if delay > 1 {
-                data.comp.attrs.set(ast::BoolAttr::CounterFSM, 1);
+                data.comp.attrs.set(
+                    utils::CompBool::CounterFSM,
+                    true,
+                    utils::GPosIdx::UNKNOWN,
+                );
                 return Action::Stop;
             }
         }
 
-        data.comp.attrs.set(ast::BoolAttr::CounterFSM, 0);
+        data.comp.attrs.set(
+            utils::CompBool::CounterFSM,
+            false,
+            utils::GPosIdx::UNKNOWN,
+        );
 
         Action::Stop
     }