Always-happens-before property (#37)

## What Changed?

This adds an `always_happens_before` combinator to the properties like
we had before. In addition to providing similar functionality as the old
Forge combinator it returns statistics at the end of its execution with
information that is helpful to for debugging.

In particular the `AlwaysHappensBefore` struct lets users query whether
the property `holds` and if it `is_vacuous`ly true (no paths from source
to sink found).

In addition the `Display` implementation prints the number of violating
paths found, the number of total paths scanned and the number of
violating paths that were found.

Note that the traversal skips already seen nodes and thus the number of
paths seen is not the total number of paths between source and sink.

It also uncovered a bug in `Context::is_function`.

## Why Does It Need To?

Lets us express a new type of property in the rust engine.

## 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] Documentation in Notion has been updated
- [x] Tests for new behaviors are provided
  - [x] 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.

crates/dfcheck/src/context.rs

@@ -1,8 +1,9 @@
 use dfgraph::{
-    Annotation, CallSite, Ctrl, DataSink, DataSource, HashMap, Identifier, MarkerAnnotation,
-    MarkerRefinement, ProgramDescription,
+    Annotation, CallSite, Ctrl, DataSink, DataSource, HashMap, HashSet, Identifier,
+    MarkerAnnotation, MarkerRefinement, ProgramDescription,
 };
 
+use anyhow::{anyhow, ensure, Result};
 use indexical::ToIndex;
 use itertools::Itertools;
 
@@ -146,11 +147,131 @@ impl Context {
 
     /// Returns true if `id` identifies a function with name `name`.
     pub fn is_function(&self, id: Identifier, name: &str) -> bool {
-        match id.as_str().split_once('_') {
+        match id.as_str().rsplit_once('_') {
             Some((id_name, _)) => id_name == name,
             None => false,
         }
     }
+
+    /// Enforce that on every path from the `starting_points` to `is_terminal` a
+    /// node satisfying `is_checkpoint` is passed.
+    ///
+    /// Fails if `ctrl` is not found.
+    ///
+    /// The return value contains some statistics information about the
+    /// traversal. The property holds if [`AlwaysHappensBefore::holds`] is true.
+    ///
+    /// Note that `is_checkpoint` and `is_terminal` will be called many times
+    /// and should thus be efficient computations. In addition they should
+    /// always return the same result for the same input.
+    pub fn always_happens_before(
+        &self,
+        ctrl: Identifier,
+        starting_points: impl Iterator<Item = DataSource>,
+        mut is_checkpoint: impl FnMut(&DataSink) -> bool,
+        mut is_terminal: impl FnMut(&DataSink) -> bool,
+    ) -> Result<AlwaysHappensBefore> {
+        let mut seen = HashSet::<&DataSink>::new();
+        let mut num_reached = 0;
+        let mut num_checkpointed = 0;
+
+        let mut queue = starting_points.collect::<Vec<_>>();
+
+        let started_with = queue.len();
+
+        let flow = &self
+            .desc()
+            .controllers
+            .get(&ctrl)
+            .ok_or_else(|| anyhow!("Controller {ctrl} not found"))?
+            .data_flow
+            .0;
+
+        while let Some(current) = queue.pop() {
+            for sink in flow.get(&current).into_iter().flatten() {
+                if is_checkpoint(sink) {
+                    num_checkpointed += 1;
+                } else if is_terminal(sink) {
+                    num_reached += 1;
+                } else if let DataSink::Argument { function, .. } = sink {
+                    if seen.insert(sink) {
+                        queue.push(DataSource::FunctionCall(function.clone()));
+                    }
+                }
+            }
+        }
+
+        Ok(AlwaysHappensBefore {
+            num_reached,
+            num_checkpointed,
+            started_with,
+        })
+    }
+}
+
+/// Statistics about the result of running [`Context::always_happens_before`]
+/// that are useful to understand how the property failed.
+///
+/// The [`std::fmt::Display`] implementation presents the information in human
+/// readable form.
+///
+/// Note: Both the number of seen paths and the number of violation paths are
+/// approximations. This is because the traversal terminates when it reaches a
+/// node that was already seen. However it is guaranteed that if there
+/// are any violating paths, then the number of reaching paths reported in this
+/// struct is at least one (e.g. [`Self::holds`] is sound).
+///
+/// The stable API of this struct is [`Self::holds`], [`Self::assert_holds`] and
+/// [`Self::found_any`]. Otherwise the information in this struct and its
+/// printed representations should be considered unstable and
+/// for-human-eyes-only.
+pub struct AlwaysHappensBefore {
+    /// How many paths terminated at the end?
+    num_reached: i32,
+    /// How many paths lead to the checkpoints?
+    num_checkpointed: i32,
+    /// How large was the set of initial nodes this traversal started with.
+    started_with: usize,
+}
+
+impl std::fmt::Display for AlwaysHappensBefore {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let Self {
+            num_reached,
+            num_checkpointed,
+            started_with,
+        } = self;
+        write!(
+            f,
+            "{num_reached} paths reached the terminal, \
+            {num_checkpointed} paths reached the checkpoints, \
+            started with {started_with} nodes"
+        )
+    }
+}
+
+impl AlwaysHappensBefore {
+    /// Returns `true` if the property that created these statistics holds.
+    pub fn holds(&self) -> bool {
+        self.num_reached == 0
+    }
+
+    /// Fails if [`Self::holds`] is false.
+    pub fn assert_holds(&self) -> Result<()> {
+        ensure!(
+            self.holds(),
+            "AlwaysHappensBefore failed: found {} violating paths",
+            self.num_reached
+        );
+        Ok(())
+    }
+
+    /// `true` if this policy applied to no paths. E.g. either no starting nodes
+    /// or no path from them can reach the terminal or the checkpoints (the
+    /// graphs are disjoined).
+    pub fn is_vacuous(&self) -> bool {
+        self.num_checkpointed + self.num_reached == 0
+    }
 }
 
 #[test]
@@ -173,3 +294,104 @@ fn test_context() {
     assert_eq!(ctx.marked_sinks(ctrl.data_sinks(), input).count(), 0);
     assert_eq!(ctx.marked_sinks(ctrl.data_sinks(), sink).count(), 2);
 }
+
+#[test]
+fn test_happens_before() -> Result<()> {
+    let ctx = crate::test_utils::test_ctx();
+    let desc = ctx.desc();
+
+    fn has_marker(desc: &ProgramDescription, sink: &DataSink, marker: Identifier) -> bool {
+        if let DataSink::Argument { function, arg_slot } = sink {
+            desc.annotations
+                .get(&function.function)
+                .map_or(false, |(anns, _)| {
+                    anns.iter().filter_map(Annotation::as_label_ann).any(|ann| {
+                        ann.marker == marker
+                            && (ann
+                                .refinement
+                                .on_argument()
+                                .contains(*arg_slot as u32)
+                                .unwrap()
+                                || ann.refinement.on_self())
+                    })
+                })
+        } else {
+            false
+        }
+    }
+
+    fn is_checkpoint(desc: &ProgramDescription, checkpoint: &DataSink) -> bool {
+        has_marker(desc, checkpoint, Identifier::new_intern("bless"))
+    }
+    fn is_terminal(end: &DataSink) -> bool {
+        matches!(end, DataSink::Return)
+    }
+
+    fn marked_sources(
+        desc: &ProgramDescription,
+        ctrl_name: Identifier,
+        marker: Marker,
+    ) -> impl Iterator<Item = &DataSource> {
+        desc.controllers[&ctrl_name]
+            .data_flow
+            .0
+            .keys()
+            .filter(move |source| match source {
+                DataSource::Argument(arg) => desc.annotations[&ctrl_name]
+                    .0
+                    .iter()
+                    .filter_map(Annotation::as_label_ann)
+                    .any(|ann| {
+                        ann.marker == marker
+                            && (ann.refinement.on_self()
+                                || ann
+                                    .refinement
+                                    .on_argument()
+                                    .contains(*arg as u32)
+                                    .unwrap_or(false))
+                    }),
+                DataSource::FunctionCall(cs) => desc.annotations[&cs.function]
+                    .0
+                    .iter()
+                    .filter_map(Annotation::as_label_ann)
+                    .any(|ann| {
+                        ann.marker == marker
+                            && (ann.refinement.on_self() || ann.refinement.on_return())
+                    }),
+            })
+    }
+
+    let ctrl_name = *desc
+        .controllers
+        .keys()
+        .find(|id| ctx.is_function(**id, "happens_before_pass"))
+        .unwrap();
+
+    let pass = ctx.always_happens_before(
+        ctrl_name,
+        marked_sources(desc, ctrl_name, Identifier::new_intern("start")).cloned(),
+        |checkpoint| is_checkpoint(desc, checkpoint),
+        is_terminal,
+    )?;
+
+    ensure!(pass.holds());
+    ensure!(!pass.is_vacuous(), "{pass}");
+
+    let ctrl_name = *desc
+        .controllers
+        .keys()
+        .find(|id| ctx.is_function(**id, "happens_before_fail"))
+        .unwrap();
+
+    let fail = ctx.always_happens_before(
+        ctrl_name,
+        marked_sources(desc, ctrl_name, Identifier::new_intern("start")).cloned(),
+        |check| is_checkpoint(desc, check),
+        is_terminal,
+    )?;
+
+    ensure!(!fail.holds());
+    ensure!(!fail.is_vacuous());
+
+    Ok(())
+}

crates/dfcheck/tests/test-crate/src/lib.rs

@@ -15,3 +15,24 @@ fn controller(a: Foo, b: Foo) {
     sink1(a);
     sink2(b);
 }
+
+#[dfpp::marker(start, return)]
+fn create() -> u32 {
+    9
+}
+
+#[dfpp::marker(bless, arguments = [0])]
+fn id<T>(t: T) -> T {
+    t
+}
+
+#[dfpp::analyze]
+fn happens_before_pass() -> u32 {
+    id(create())
+}
+
+#[dfpp::analyze]
+fn happens_before_fail() -> u32 {
+    let val = create();
+    id(val) + val
+}