feat(semantics): add boolean semantics
TODO: Testing this
This commit is contained in:
parent
e982dfe5a5
commit
22c099a058
7 changed files with 288 additions and 11 deletions
|
|
@ -5,4 +5,7 @@ edition = "2021"
|
||||||
|
|
||||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
|
argus-core = { version = "0.1.0", path = "../argus-core" }
|
||||||
|
itertools = "0.10.5"
|
||||||
|
paste = "1.0.12"
|
||||||
|
|
|
||||||
40
argus-semantics/src/eval.rs
Normal file
40
argus-semantics/src/eval.rs
Normal file
|
|
@ -0,0 +1,40 @@
|
||||||
|
use argus_core::{
|
||||||
|
expr::NumExpr,
|
||||||
|
signals::{AnySignal, ConstantSignal},
|
||||||
|
};
|
||||||
|
|
||||||
|
use crate::{utils::signal_num_op_impl, Trace};
|
||||||
|
|
||||||
|
/// Helper struct to evaluate a [`NumExpr`] given a trace.
|
||||||
|
pub struct NumExprEval;
|
||||||
|
|
||||||
|
impl NumExprEval {
|
||||||
|
pub fn eval(root: &NumExpr, trace: &impl Trace) -> AnySignal {
|
||||||
|
match root {
|
||||||
|
NumExpr::IntLit(val) => ConstantSignal::new(*val).into(),
|
||||||
|
NumExpr::UIntLit(val) => ConstantSignal::new(*val).into(),
|
||||||
|
NumExpr::FloatLit(val) => ConstantSignal::new(*val).into(),
|
||||||
|
NumExpr::IntVar { name } | NumExpr::UIntVar { name } | NumExpr::FloatVar { name } => {
|
||||||
|
// TODO(anand): Type check!
|
||||||
|
trace.get(name.as_str()).cloned().unwrap()
|
||||||
|
}
|
||||||
|
NumExpr::Neg { arg } => {
|
||||||
|
let arg_sig = Self::eval(arg, trace);
|
||||||
|
signal_num_op_impl!(-arg_sig)
|
||||||
|
}
|
||||||
|
NumExpr::Add { args } => {
|
||||||
|
let args_signals = args.iter().map(|arg| Self::eval(arg, trace));
|
||||||
|
args_signals.reduce(|acc, arg| signal_num_op_impl!(acc + arg)).unwrap()
|
||||||
|
}
|
||||||
|
NumExpr::Mul { args } => {
|
||||||
|
let args_signals = args.iter().map(|arg| Self::eval(arg, trace));
|
||||||
|
args_signals.reduce(|acc, arg| signal_num_op_impl!(acc * arg)).unwrap()
|
||||||
|
}
|
||||||
|
NumExpr::Div { dividend, divisor } => {
|
||||||
|
let dividend = Self::eval(dividend, trace);
|
||||||
|
let divisor = Self::eval(divisor, trace);
|
||||||
|
signal_num_op_impl!(dividend / divisor)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -1,14 +1,66 @@
|
||||||
pub fn add(left: usize, right: usize) -> usize {
|
//! Argus offline semantics
|
||||||
left + right
|
//!
|
||||||
|
//! In this crate, we are predominantly concerned with the monitoring of _offline system
|
||||||
|
//! traces_, i.e., a collection of signals that have been extracted from observing and
|
||||||
|
//! sampling from some system.
|
||||||
|
use argus_core::expr::BoolExpr;
|
||||||
|
use argus_core::ArgusResult;
|
||||||
|
use argus_core::{expr::ExprRef, signals::AnySignal};
|
||||||
|
|
||||||
|
pub mod eval;
|
||||||
|
pub mod semantics;
|
||||||
|
pub mod utils;
|
||||||
|
|
||||||
|
pub use semantics::boolean::BooleanSemantics;
|
||||||
|
pub use semantics::quantitative::QuantitativeSemantics;
|
||||||
|
|
||||||
|
/// A trace is a collection of signals
|
||||||
|
///
|
||||||
|
/// # Example
|
||||||
|
///
|
||||||
|
/// An example of a `Trace` may be:
|
||||||
|
///
|
||||||
|
/// ```rust
|
||||||
|
/// # use std::collections::HashMap;
|
||||||
|
/// # use argus_core::signals::{ConstantSignal, AnySignal};
|
||||||
|
/// # use argus_semantics::Trace;
|
||||||
|
///
|
||||||
|
/// struct MyTrace(HashMap<String, AnySignal>);
|
||||||
|
///
|
||||||
|
/// impl Trace for MyTrace {
|
||||||
|
/// fn signal_names(&self) -> Vec<&str> {
|
||||||
|
/// self.0.keys().map(|k| k.as_str()).collect()
|
||||||
|
/// }
|
||||||
|
///
|
||||||
|
/// fn get(&self, name: &str) -> Option<&AnySignal> {
|
||||||
|
/// self.0.get(name)
|
||||||
|
/// }
|
||||||
|
/// }
|
||||||
|
///
|
||||||
|
/// let trace = MyTrace(HashMap::from([
|
||||||
|
/// ("x".to_string(), ConstantSignal::new(true).into()),
|
||||||
|
/// ("y".to_string(), ConstantSignal::new(2.0).into()),
|
||||||
|
/// ]));
|
||||||
|
/// let names = trace.signal_names();
|
||||||
|
///
|
||||||
|
/// assert!(names == &["x", "y"] || names == &["y", "x"]);
|
||||||
|
/// assert!(matches!(trace.get("x"), Some(AnySignal::ConstBool(_))));
|
||||||
|
/// assert!(matches!(trace.get("y"), Some(AnySignal::ConstFloat(_))));
|
||||||
|
/// ```
|
||||||
|
pub trait Trace {
|
||||||
|
/// Get the list of signal names contained within the trace.
|
||||||
|
fn signal_names(&self) -> Vec<&str>;
|
||||||
|
|
||||||
|
/// Query a signal using its name
|
||||||
|
fn get(&self, name: &str) -> Option<&AnySignal>;
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
/// General interface for defining semantics for the [`argus-core`](argus_core) logic.
|
||||||
mod tests {
|
pub trait Semantics {
|
||||||
use super::*;
|
/// The output of applying the given semantics to an expression and trace.
|
||||||
|
type Output;
|
||||||
|
/// Any additional possible context that can be passed to the semantics evaluator.
|
||||||
|
type Context;
|
||||||
|
|
||||||
#[test]
|
fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output>;
|
||||||
fn it_works() {
|
|
||||||
let result = add(2, 2);
|
|
||||||
assert_eq!(result, 4);
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
59
argus-semantics/src/semantics/boolean.rs
Normal file
59
argus-semantics/src/semantics/boolean.rs
Normal file
|
|
@ -0,0 +1,59 @@
|
||||||
|
use argus_core::{expr::BoolExpr, prelude::*};
|
||||||
|
|
||||||
|
use crate::{
|
||||||
|
eval::NumExprEval,
|
||||||
|
utils::{signal_bool_op_impl, signal_cmp_op_impl},
|
||||||
|
Semantics, Trace,
|
||||||
|
};
|
||||||
|
|
||||||
|
/// Boolean semantics of Argus expressions
|
||||||
|
pub struct BooleanSemantics;
|
||||||
|
|
||||||
|
impl Semantics for BooleanSemantics {
|
||||||
|
// TODO: figure out how to make Output concrete Signal<bool> or ConstantSignal<bool>
|
||||||
|
type Output = AnySignal;
|
||||||
|
type Context = ();
|
||||||
|
|
||||||
|
fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> {
|
||||||
|
match expr {
|
||||||
|
BoolExpr::BoolLit(val) => Ok(ConstantSignal::new(*val).into()),
|
||||||
|
BoolExpr::BoolVar { name } => trace.get(name.as_str()).cloned().ok_or(ArgusError::SignalNotPresent),
|
||||||
|
BoolExpr::Cmp { op, lhs, rhs } => {
|
||||||
|
use argus_core::expr::Ordering::*;
|
||||||
|
let lhs = NumExprEval::eval(lhs, trace);
|
||||||
|
let rhs = NumExprEval::eval(rhs, trace);
|
||||||
|
let ret = match op {
|
||||||
|
Eq => signal_cmp_op_impl!(lhs == rhs),
|
||||||
|
NotEq => signal_cmp_op_impl!(lhs != rhs),
|
||||||
|
Less { strict } if *strict => signal_cmp_op_impl!(lhs < rhs),
|
||||||
|
Less { strict: _ } => signal_cmp_op_impl!(lhs <= rhs),
|
||||||
|
Greater { strict } if *strict => signal_cmp_op_impl!(lhs > rhs),
|
||||||
|
Greater { strict: _ } => signal_cmp_op_impl!(lhs >= rhs),
|
||||||
|
};
|
||||||
|
ret.ok_or(ArgusError::InvalidOperation)
|
||||||
|
}
|
||||||
|
BoolExpr::Not { arg } => {
|
||||||
|
let arg = Self::eval(arg, trace, ctx)?;
|
||||||
|
Ok(signal_bool_op_impl!(!arg))
|
||||||
|
}
|
||||||
|
BoolExpr::And { args } => {
|
||||||
|
let args: ArgusResult<Vec<_>> = args.iter().map(|arg| Self::eval(arg, trace, ctx)).collect();
|
||||||
|
let ret = args?
|
||||||
|
.into_iter()
|
||||||
|
.fold(AnySignal::from(ConstantSignal::new(true)), |lhs, rhs| {
|
||||||
|
signal_bool_op_impl!(lhs & rhs)
|
||||||
|
});
|
||||||
|
Ok(ret)
|
||||||
|
}
|
||||||
|
BoolExpr::Or { args } => {
|
||||||
|
let args: ArgusResult<Vec<_>> = args.iter().map(|arg| Self::eval(arg, trace, ctx)).collect();
|
||||||
|
let ret = args?
|
||||||
|
.into_iter()
|
||||||
|
.fold(AnySignal::from(ConstantSignal::new(true)), |lhs, rhs| {
|
||||||
|
signal_bool_op_impl!(lhs | rhs)
|
||||||
|
});
|
||||||
|
Ok(ret)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
2
argus-semantics/src/semantics/mod.rs
Normal file
2
argus-semantics/src/semantics/mod.rs
Normal file
|
|
@ -0,0 +1,2 @@
|
||||||
|
pub mod boolean;
|
||||||
|
pub mod quantitative;
|
||||||
1
argus-semantics/src/semantics/quantitative.rs
Normal file
1
argus-semantics/src/semantics/quantitative.rs
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
pub struct QuantitativeSemantics;
|
||||||
120
argus-semantics/src/utils.rs
Normal file
120
argus-semantics/src/utils.rs
Normal file
|
|
@ -0,0 +1,120 @@
|
||||||
|
macro_rules! signal_num_op_impl {
|
||||||
|
// Unary numeric opeartions
|
||||||
|
(- $signal:ident) => {{
|
||||||
|
use argus_core::prelude::*;
|
||||||
|
use AnySignal::*;
|
||||||
|
match $signal {
|
||||||
|
Bool(_) | ConstBool(_) => panic!("cannot perform unary operation (-) on Boolean signals"),
|
||||||
|
Int(signal) => AnySignal::from(-(&signal)),
|
||||||
|
ConstInt(signal) => AnySignal::from(-(&signal)),
|
||||||
|
UInt(_) | ConstUInt(_) => panic!("cannot perform unary operation (-) on unsigned integer signals"),
|
||||||
|
Float(signal) => AnySignal::from(-(&signal)),
|
||||||
|
ConstFloat(signal) => AnySignal::from(-(&signal)),
|
||||||
|
}
|
||||||
|
}};
|
||||||
|
|
||||||
|
($lhs:ident $op:tt $rhs:ident, [$( $type:ident ),*]) => {
|
||||||
|
paste::paste!{
|
||||||
|
{
|
||||||
|
use argus_core::prelude::*;
|
||||||
|
use AnySignal::*;
|
||||||
|
match ($lhs, $rhs) {
|
||||||
|
(Bool(_), _) | (ConstBool(_), _) | (_, Bool(_)) | (_, ConstBool(_)) => panic!("cannot perform numeric operation {} for boolean arguments", stringify!($op)),
|
||||||
|
$(
|
||||||
|
([<$type >](lhs), [< $type >](rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
([<$type >](lhs), [< Const $type >](rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
([<Const $type >](lhs), [< $type >](rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
([<Const $type >](lhs), [< Const $type >](rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
)*
|
||||||
|
_ => panic!("mismatched argument types for {} operation", stringify!($op)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
// Binary numeric opeartions
|
||||||
|
($lhs:ident $op:tt $rhs:ident) => {
|
||||||
|
signal_num_op_impl!(
|
||||||
|
$lhs $op $rhs,
|
||||||
|
[Int, UInt, Float]
|
||||||
|
)
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
macro_rules! signal_cmp_op_impl {
|
||||||
|
($lhs:ident, $rhs:ident, $op:ident, [$( $type:ident ),*]) => {
|
||||||
|
paste::paste!{
|
||||||
|
{
|
||||||
|
use argus_core::signals::traits::SignalPartialOrd;
|
||||||
|
use argus_core::prelude::*;
|
||||||
|
use AnySignal::*;
|
||||||
|
match ($lhs, $rhs) {
|
||||||
|
(Bool(_), _) | (ConstBool(_), _) | (_, Bool(_)) | (_, ConstBool(_)) => panic!("cannot perform comparison operation ({}) for boolean arguments", stringify!($op)),
|
||||||
|
$(
|
||||||
|
([<$type >](lhs), [< $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
|
||||||
|
([<$type >](lhs), [< Const $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
|
||||||
|
([<Const $type >](lhs), [< $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
|
||||||
|
([<Const $type >](lhs), [< Const $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
|
||||||
|
)*
|
||||||
|
_ => panic!("mismatched argument types for comparison operation ({})", stringify!($op)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
($lhs:ident < $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_lt, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
|
||||||
|
($lhs:ident <= $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_le, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
|
||||||
|
($lhs:ident > $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_gt, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
($lhs:ident >= $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_ge, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
|
||||||
|
($lhs:ident == $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_eq, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
|
||||||
|
($lhs:ident != $rhs:ident) => {
|
||||||
|
signal_cmp_op_impl!($lhs, $rhs, signal_ne, [Int, UInt, Float])
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
macro_rules! signal_bool_op_impl {
|
||||||
|
// Unary bool opeartions
|
||||||
|
(! $signal:ident) => {{
|
||||||
|
use argus_core::prelude::*;
|
||||||
|
use AnySignal::*;
|
||||||
|
match $signal {
|
||||||
|
Bool(sig) => AnySignal::from(!(&sig)),
|
||||||
|
ConstBool(sig) => AnySignal::from(!(&sig)),
|
||||||
|
_ => panic!("cannot perform unary operation (!) on numeric signals"),
|
||||||
|
}
|
||||||
|
}};
|
||||||
|
|
||||||
|
($lhs:ident $op:tt $rhs:ident) => {
|
||||||
|
paste::paste! {
|
||||||
|
{
|
||||||
|
use argus_core::prelude::*;
|
||||||
|
use AnySignal::*;
|
||||||
|
match ($lhs, $rhs) {
|
||||||
|
(Bool(lhs), Bool(rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
(Bool(lhs), ConstBool(rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
(ConstBool(lhs), Bool(rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
(ConstBool(lhs), ConstBool(rhs)) => AnySignal::from(&lhs $op &rhs),
|
||||||
|
_ => panic!("mismatched argument types for {} operation", stringify!($op)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
pub(crate) use signal_bool_op_impl;
|
||||||
|
pub(crate) use signal_cmp_op_impl;
|
||||||
|
pub(crate) use signal_num_op_impl;
|
||||||
Loading…
Add table
Add a link
Reference in a new issue