1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

//! Diagnostic errors produced by the partial evaluator.

use crate::diagnostics::{DiagnosticRecord, DiagnosticRegistry};

macro_rules! define_errors {
    ($($(#[doc = $doc:expr])+ $code:ident: $error:ident $gen_macro:tt)*) => {$(
        $(#[doc = $doc])+
        pub(crate) struct $error;

        impl DiagnosticRecord for $error {
            const CODE: &'static str = stringify!($code);
            const EXPLANATION: &'static str = concat!($($doc, "\n"),+);
        })*

        pub struct PartialEvaluatorErrors;

        impl DiagnosticRegistry for PartialEvaluatorErrors {
            fn codes_with_explanations() -> Vec<(&'static str, &'static str)> {
                let mut vec = Vec::new();
                $(vec.push(($error::CODE, $error::EXPLANATION));)*
                vec
            }
        }

        $(
            macro_rules! $error $gen_macro
        )*
    };
}

define_errors! {
    ///This error is fired on variable definitions provided to a slide program that can never be
    ///compatible. For example, given the program
    ///
    ///```text
    ///a := 1
    ///a := 12 - 10
    ///```
    ///
    ///"a" is defined as "1" and "2" simultaneously, which are incompatible definitions.
    ///
    ///This error is only fired when slide is able to statically detect incompatibility of
    ///defintions. For example, without having information on what "c" is defined as, the program
    ///
    ///```text
    ///a := c
    ///a := 2c
    ///```
    ///
    ///would not have an incompatible definitions error, because the program is valid when "c = 0".
    ///However, if slide knew about that value of "c", as it would in the program
    ///
    ///```text
    ///a := c
    ///a := 2c
    ///c := 1
    ///```
    ///
    ///an incompatible definitions error could now be fired on the two definitions of "a".
    V0001: IncompatibleDefinitions {
        ($var:expr, $a_def:expr, $b_def:expr) => {
            Diagnostic::span_err(
                $a_def.span,
                format!(r#"Definitions of "{}" are incompatible"#, $var),
                "V0001",
                format!(r#"this definition evaluates to "{}""#, $a_def),
            )
            .with_spanned_err(
                $b_def.span,
                format!(r#"this definition evaluates to "{}""#, $b_def),
            )
            .with_note(format!(
                r#""{}" and "{}" are never equal"#,
                $a_def.rhs, $b_def.rhs
            ))
        }
    }

    // TODO(#263): unify this with other lints.
    ///This warning is fired on variable definitions that may be incompatible. For example, given
    ///the program
    ///
    ///```text
    ///a := b
    ///a := 2*b
    ///```
    ///
    ///The definitions of "a" are maybe-incompatible; in particular, they are compatible iff
    ///"b := 0". This ambiguity is considered error-prone because it does not clearly communicate
    ///intent of the definitions, and there is no information to validate the soundness of a program
    ///in such a state.
    ///
    ///The behavior of maybe-incompatible definitions is considered undefined behavior.
    L0005: MaybeIncompatibleDefinitions {
        ($var:expr, $a_def:expr, $b_def:expr, $dep_vars:expr) => {{
            let last = $dep_vars.len() - 1;
            let mut dep_vars = if last == 0 { "variable " } else { "variables " }.to_string();
            for (i, var) in $dep_vars.into_iter().enumerate() {
                // Cases:
                //   a
                //   a and b
                //   a, b, and c
                dep_vars.push_str(&match i {
                    0 => format!("\"{}\"", var),
                    1 if i == last => format!(" and \"{}\"", var),
                    _ if i == last => format!(", and \"{}\"", var),
                    _ => format!(", \"{}\"", var),
                });
            }
            Diagnostic::span_warn(
                $a_def.span,
                format!(r#"Definitions of "{}" may be incompatible"#, $var),
                "L0002",
                format!(r#"this definition evaluates to "{}""#, $a_def),
            )
            .with_spanned_warn(
                $b_def.span,
                format!(r#"this definition evaluates to "{}""#, $b_def),
            )
            .with_note(format!(
                r#""{}" and "{}" may not be equal"#,
                $a_def.rhs, $b_def.rhs
            ))
            .with_note(
                format!("equivalence of the definitions depends on the {}", dep_vars)
            )
            .with_note(
                "there is not enough information to conclude whether the definitions are compatible"
            )
        }}
    }
}