Skip to content

Commit

Permalink
A mechanism for diagnostics with context (#42)
Browse files Browse the repository at this point in the history
## What Changed?

Implements a suggestion from #38.

Adds the ability to register simple context information, such as the
currently executing policy or combinator with the `Context` that is
emitted as part of the diagnostics.

For instance the named policy `community-safety` in a hypothetical
combinator `reaches` would output diagnostics such as:

```
[policy: community-safety] [reaches] Vacuous: no nodes matching starting conditions
```

This is achieved by transparently attaching diagnostic context. 

First off the `error` and `warning` convenience methods on `Context`
still work. Both are now part of the `Diagnostics` trait,

The trait is also implemented on `PolicyContext`, which is created by
`Context::named_policy()` an transparently attaches the name of the
policy to all diagnostic messages emitted from it. It `Deref`s to
`Context` so all if its functionality is included.
Both `Context` and `PolicyContext` can also create a `CombinatorContext`
with the `named_combinator()` method that attaches a combinator name.
`CombinatorContext` also `Deref`s to `Context`.


## Why Does It Need To?

Right now every diagnostic message has to track where it occurs. By
adding this way of accumulating contextual information we can, for
instance, have a combinator like `always_happens_before` interrogate
itself and dispatch generic diagnostics which are then enriched with
contextual information, making them more specific and understandable
again.

## Checklist

- [x] Above description has been filled out so that upon quash merge we
have a
  good record of what changed.
- [x] New functions, methods, types are documented. Old documentation is
updated
  if necessary
- [x] A module level documentation section for how to use diagnostic
context
- [ ] Documentation in Notion has been updated
- [ ] Tests for new behaviors are provided
  - [ ] New test suites (if any) ave been added to the CI tests (in
`.github/workflows/rust.yml`) either as compiler test or integration
test.
*Or* justification for their omission from CI has been provided in this
PR
    description.
  • Loading branch information
JustusAdam authored Oct 2, 2023
1 parent a2afa5e commit 5094e00
Show file tree
Hide file tree
Showing 8 changed files with 467 additions and 95 deletions.
1 change: 1 addition & 0 deletions Cargo.lock

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

3 changes: 2 additions & 1 deletion crates/paralegal-policy/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ itertools = "0.11.0"
indexical = { workspace = true }
serde_json = "1"
simple_logger = "2"
lazy_static = "1"

[dev-dependencies]
paralegal-flow = { path = "../paralegal-flow", features = ["test"] }
paralegal-flow = { path = "../paralegal-flow", features = ["test"] }
65 changes: 25 additions & 40 deletions crates/paralegal-policy/src/context.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use std::{io::Write, process::exit};
use std::{io::Write, process::exit, sync::Arc};

use paralegal_spdg::{
Annotation, CallSite, Ctrl, DataSink, DataSource, HashMap, HashSet, Identifier,
Expand All @@ -13,9 +13,10 @@ use itertools::Itertools;

use super::flows_to::CtrlFlowsTo;

use crate::diagnostics::{Diagnostics, Severity};

pub use crate::diagnostics::DiagnosticMessage;
use crate::{
assert_error, assert_warning,
diagnostics::{CombinatorContext, DiagnosticsRecorder, HasDiagnosticsBase},
};

/// User-defined PDG markers.
pub type Marker = Identifier;
Expand All @@ -28,26 +29,6 @@ pub type FunctionId = DefId;
type MarkerIndex = HashMap<Marker, Vec<(DefId, MarkerRefinement)>>;
type FlowsTo = HashMap<ControllerId, CtrlFlowsTo>;

/// Check the condition and emit a [`Context::error`] if it fails.
#[macro_export]
macro_rules! assert_error {
($ctx:expr, $cond: expr, $msg:expr $(,)?) => {
if !$cond {
$ctx.error($msg);
}
};
}

/// Check the condition and emit a [`Context::warning`] if it fails.
#[macro_export]
macro_rules! assert_warning {
($ctx:expr, $cond: expr, $msg:expr $(,)?) => {
if !$cond {
$ctx.warning($msg);
}
};
}

/// Interface for defining policies.
///
/// Holds a PDG ([`Self::desc`]) and defines basic queries like
Expand All @@ -56,9 +37,10 @@ macro_rules! assert_warning {
/// policies.
///
/// To communicate the results of your policies with the user you can emit
/// diagnostic messages. To communicate a policy failure use [`Self::error`] or
/// the [`assert_error`] macro. To communicate suspicious circumstances that are
/// not outright cause for failure use [`Self::warning`] or [`assert_warning`].
/// diagnostic messages. To communicate a policy failure use
/// [`error`](crate::Diagnostics::error) or the [`assert_error`] macro. To
/// communicate suspicious circumstances that are not outright cause for failure
/// use [`warning`](crate::Diagnostics::error) or [`assert_warning`].
///
/// Note that these methods just queue the diagnostics messages. To emit them
/// (and potentially terminate the program if the policy does not hold) use
Expand All @@ -70,7 +52,7 @@ pub struct Context {
marker_to_ids: MarkerIndex,
desc: ProgramDescription,
flows_to: FlowsTo,
diagnostics: Diagnostics,
pub(crate) diagnostics: Arc<DiagnosticsRecorder>,
name_map: HashMap<Identifier, Vec<DefId>>,
}

Expand Down Expand Up @@ -150,18 +132,6 @@ impl Context {
Ok(())
}

/// Record a message to the user indicating a problem that will not cause
/// verification to fail.
pub fn warning(&self, msg: impl Into<DiagnosticMessage>) {
self.diagnostics.record(msg, Severity::Warning)
}

/// Record a message to the user for a problem that will cause verification
/// to fail.
pub fn error(&self, msg: impl Into<DiagnosticMessage>) {
self.diagnostics.record(msg, Severity::Fail)
}

fn build_index_on_markers(desc: &ProgramDescription) -> MarkerIndex {
desc.annotations
.iter()
Expand Down Expand Up @@ -369,7 +339,22 @@ impl std::fmt::Display for AlwaysHappensBefore {
}
}

lazy_static::lazy_static! {
static ref ALWAYS_HAPPENS_BEFORE_NAME: Identifier = Identifier::new_intern("always_happens_before");
}

impl AlwaysHappensBefore {
/// Check this property holds and report it as diagnostics in the context.
///
/// Additionally reports if the property was vacuous or had no starting
/// nodes.
pub fn report(&self, ctx: Arc<dyn HasDiagnosticsBase>) {
let ctx = CombinatorContext::new(*ALWAYS_HAPPENS_BEFORE_NAME, ctx);
assert_warning!(ctx, self.started_with != 0, "Started with 0 nodes.");
assert_warning!(ctx, !self.is_vacuous(), "Is vacuously true.");
assert_error!(ctx, self.holds(), format!("Violation detected: {}", self));
}

/// Returns `true` if the property that created these statistics holds.
pub fn holds(&self) -> bool {
self.num_reached == 0
Expand Down
Loading

0 comments on commit 5094e00

Please sign in to comment.