question: propagation through closure containing tagged values

[mimoo]

Looking at the propagation options, it doesn't seem like a tagged values => a tagged closure containing that value. The problem is that I want a method to detect when one of its argument contains a closure, which is tagged

(unless that's the UninterpretedCall?)

[hermanventer]

This seems like an oversight to me. I would expect SuperComponent to tag a closure that captures a tagged value. To get the ball rolling, why don't you construct a test case that can be used to drive an implementation of the feature.

[mimoo]

I'm trying to make the following work, but I've been failing to do so:

#![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

#[cfg(mirai)]
use mirai_annotations::{TagPropagationSet, TAG_PROPAGATION_ALL};

use std::borrow::Borrow;

#[macro_use]
extern crate mirai_annotations;

#[macro_use]
extern crate contracts;

/// Our tag for detecting out-of-circuit values that are reinserted into the circuit.
// TODO: OOC value doesn't quite describe it, here we're looking specifically for OOC values that were previously in the circuit. So perhaps boomerang values?
#[cfg(mirai)]
struct OOCTaintKind<const MASK: TagPropagationSet> {}

/// our tag with all propagation set
#[cfg(mirai)]
type OOCTaint = OOCTaintKind<TAG_PROPAGATION_ALL>;
#[cfg(not(mirai))]
type OOCTaint = ();

trait R1CS {
    type Value;

    fn value(&self) -> Self::Value;
}

trait Var<V>
where
    Self: Sized,
    V: ?Sized,
{
    fn new_variable<T: Borrow<V>>(f: impl FnOnce() -> Result<T, String>) -> Result<Self, String>;
}

#[derive(Debug)]
pub struct FieldVar {
    value: u8,
}

impl R1CS for FieldVar {
    type Value = u8;

    fn value(&self) -> Self::Value {
        add_tag!(&self.value, OOCTaint);
        let result = self.value;
        postcondition!(has_tag!(&result, OOCTaint));
        return result;
    }
}

impl Var<u8> for FieldVar {
    #[requires(does_not_have_tag!(&f, OOCTaint))]
    fn new_variable<T: Borrow<u8>>(f: impl FnOnce() -> Result<T, String>) -> Result<Self, String> {
        let value = f()?.borrow().clone();
        Ok(FieldVar { value })
    }
}

impl FieldVar {
    #[requires(does_not_have_tag!(&value, OOCTaint))]
    fn without_closure(value: u8) -> Result<Self, String> {
        Ok(FieldVar { value })
    }

    fn try_2(value: u8) -> Result<Self, String> {
        precondition!(does_not_have_tag!(&value, OOCTaint));
        verify!(does_not_have_tag!(&value, OOCTaint));
        Ok(FieldVar { value })
    }
}

fn main() {
    // create a new field var
    let x = FieldVar::new_variable(|| Ok(1)).unwrap();

    // move it to OOC
    let ooc = x.value();

    verify!(has_tag!(&ooc, OOCTaint));

    // REINSERT IT! OMG!
    let y = FieldVar::new_variable(|| Ok(ooc)).unwrap();
    verify!(has_tag!(&ooc, OOCTaint));

    let y2 = FieldVar::without_closure(ooc).unwrap();

    verify!(has_tag!(&ooc, OOCTaint));
    let y3 = FieldVar::try_2(ooc).unwrap();

    dbg!(&y, &y2, &y3);
}

running cargo mirai I get this:

warning: this is unreachable, mark it as such by using the verify_unreachable! macro
  --> src/main.rs:91:5
   |
91 |     verify!(has_tag!(&ooc, OOCTaint));
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: `try_tag_analysis` (bin "try_tag_analysis") generated 1 warning

which doesn't seem correct to me

[mimoo]

note that TAG_PROPAGATION_ALL does not contain all of them (for example Transmute is not there)

[mimoo]

OK I think I figured out what went wrong:

1. the use of the annotations seems to break MIRAI. I removed the dependency on contracts = "0.6.3" and encoded the precondition checks as precondition!() in the logic of the function and it works
2. note that when I use a precondition!(does_not_have_tag!(&value, OOCTaint)); somewhere, all code that comes after logically (not necessarily as part of the same function) will assume that it does not have the tag (even if that's not true). I'm guessing that it is expected behavior due to this comment on the precondition macro (that is a bit vague I find): "When compiled with MIRAI, this causes MIRAI to assume the condition at the point where it appears in a function"

[mimoo]

In addition, MIRAI does not seem to propagate on closures containing a tagged value.

In the modified code that now works, only y2 (and if I comment y2, then y3) get detected by MIRAI. Even in paranoid mode.

impl Var<Val> for FieldVar {
    //    #[requires(does_not_have_tag!(&f, OOCTaint))]
    fn new_variable<T: Borrow<Val>>(f: impl FnOnce() -> Result<T, String>) -> Result<Self, String> {
        precondition!(does_not_have_tag!(&f, OOCTaint));
        let value = f()?.borrow().clone();
        Ok(FieldVar { value })
    }
}

impl FieldVar {
    //    #[requires(does_not_have_tag!(&value, OOCTaint))]
    fn without_closure(value: Val) -> Result<Self, String> {
        precondition!(does_not_have_tag!(&value, OOCTaint));
        Ok(FieldVar { value })
    }

    fn try_2(value: Val) -> Result<Self, String> {
        precondition!(does_not_have_tag!(&value, OOCTaint));
        verify!(does_not_have_tag!(&value, OOCTaint));
        Ok(FieldVar { value })
    }
}

EDIT: if I use verify! instead of precondition! everywhere, mirai actually detects the closure case as a "possible false verification condition"

[mimoo]

At this point I think it'd be good to have a "gotchas" document for MIRAI with mistakes or surprising behaviors that people run into when playing with MIRAI :)

when I run mirai on a library (with no main() ) then it can't find any issues, not sure why : o (even with --diag=library)

another question I'm wondering about now is, does mirai work across crates? (I remember that cfg(test) didn't). For example if I want to analyze specific functions in crate A, which depends on crate B and C which have mirai annotations, will that work?

[mimoo]

BTW, I'm also trying the MIRAI_FLAGS="--single_func=name_of_function" cargo mirai, but it's not clear exactly what's the format of the string the single_func option expects. Furthermore, I still get MIRAI warnings in other parts of the codebase even when they're not in the specified function's path

[hermanventer]

BTW, I'm also trying the MIRAI_FLAGS="--single_func=name_of_function" cargo mirai, but it's not clear exactly what's the format of the string the single_func option expects. Furthermore, I still get MIRAI warnings in other parts of the codebase even when they're not in the specified function's path

MIRAI_LOG=info will log the name of all functions being analyzed. To format output in the log is the format to use in single_func. The name of the option is now a bit misleading and should rather be -root=name_of_function. I.e. it will start with the given function and analyze it AS WELL AS all the functions it calls and all the functions they call and so on. The reason being that you cannot accurately summarize the root without first summarizing all the other functions that can be reached from the root.

[mimoo]

I think I remember that I have to touch some_file to make sure the analyze works correctly (if I change something in the MIRAI_FLAGS). I just had to do this to make it work

[hermanventer]

touch or just cargo clean. While MIRAI still works the ways it did way back when you last used it, it is now integrated into Cargo and cargo mirai is the best way to use it.

[mimoo]

I tried:

• touch src/lib.rs && MIRAI_FLAGS="-root= and got "Unrecognized option: 'r'"
• touch src/lib.rs && MIRAI_FLAGS="--root= and got "Unrecognized option: 'root'"

EDIT: oh I think you meant it should be called root, but isn't.

This works now : ) as long as I call touch on a file that exists (that really tripped me).

I'm now going to try to see if this works across crates. Thanks for the help @hermanventer ! Hopefuly this thread is also useful to other people trying to do similar things : )

[mimoo]

OK it does not seem to work across crates as I expected. Are you aware of this problem? Unless I'm missing something it's the same issue as with cfg(test), which will only be true on the crate you're running, but not on dependency crates.

Would it make sense to change any if cfg!(mirai) into if cfg!(mirai) || cfg!(feature = "mirai") so that I can define all my crates with a [features] mirai = ["depA/mirai", "depB/mirai"] to make sure the analysis is not bounded by a single crate?

[hermanventer]

If you use cargo mirai, it should compile all crates with the MIRAI configuration and things should work across crates.

[mimoo]

yeah I see the cmd.env("RUSTFLAGS", "--cfg mirai -Z always_encode_mir"); now, I'm not sure why it doesn't detect the issue when it's inside a crate : |