Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Does the behavior of add_tag!() and does_not_have_tag!() be affected by type and clone()? #1236

Open
AiDaiP opened this issue Sep 1, 2023 · 1 comment

Comments

@AiDaiP
Copy link

AiDaiP commented Sep 1, 2023

Issue

For S1, there is no warning at verify!(does_not_have_tag!(self, TraitTag)) in my_clone(). In f2(), clone() is deleted and a warning appears at verify!(does_not_have_tag!(self, TraitTag)).
For S2, warnings appear for both my_clone() and f2().
Does the behavior of add_tag!() and does_not_have_tag!() be affected by type and clone()?

Steps to Reproduce

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

#[macro_use]
extern crate mirai_annotations;

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

#[cfg(mirai)]
struct TaintedKind<const MASK: TagPropagationSet> {}

#[cfg(mirai)]
const TAINTED_MASK: TagPropagationSet = tag_propagation_set!(TagPropagation::SubComponent);

#[cfg(mirai)]
type TraitTag = TaintedKind<TAINTED_MASK>;
#[cfg(not(mirai))]
type TraitTag = ();

pub struct S1(Box<str>);

impl S1 {
    pub fn my_clone(&self) -> Self {
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
        Self(self.0.clone())
    }

    pub fn f2(&self){
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
    }
}

pub struct S2(Box<u8>);

impl S2 {
    pub fn my_clone(&self) -> Self {
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
        Self(self.0.clone())
    }

    pub fn f2(&self){
        add_tag!(self, TraitTag);
        verify!(does_not_have_tag!(self, TraitTag));
    }
}

fn main() {
    println!("helloworld")
}

cargo mirai

Expected Behavior

warning: provably false verification condition warning appears at all does_not_have_tag!()

Actual Results

warning: provably false verification condition
  --> src/main.rs:31:9
   |
31 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: provably false verification condition
  --> src/main.rs:40:9
   |
40 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: provably false verification condition
  --> src/main.rs:46:9
   |
46 |         verify!(does_not_have_tag!(self, TraitTag));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

warning: `helloworld` (bin "helloworld") generated 3 warnings
    Finished dev [unoptimized + debuginfo] target(s) in 13.39s

Environment

rustc 1.69.0-nightly (ef982929c 2023-01-27)
@hermanventer
Copy link
Contributor

This looks like a bug.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants