anodized-core 0.5.0

use crate::test_util::assert_tokens_eq;

use super::*;
use proc_macro2::TokenStream;
use syn::{Block, ItemFn, Type, parse_quote};

#[test]
fn embed_spec_item_fn() {
    let fn_spec: Spec = parse_quote! {
        requires: COND_1,
        #[cfg(META_1)]
        requires: [COND_2, COND_3],
        maintains: [COND_4, COND_5],
        #[cfg(META_2)]
        maintains: COND_6,
        captures: [
            EXPR_1 as ALIAS_1,
            EXPR_2 as (ALIAS_2, ALIAS_3),
        ],
        binds: PAT_1,
        ensures: COND_7,
        #[cfg(META_3)]
        ensures: [
            COND_8,
            |PAT_2: TYPE| COND_9,
        ],
    };
    let item_fn: ItemFn = parse_quote! {
        fn FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) -> RET_TYPE {
            BODY
        }
    };

    let qualifier_bits = FnQualifiers::empty().bits();
    let expected: TokenStream = parse_quote! {
        #[doc(hidden)]
        #[allow(warnings)]
        const __anodized_fn_qualifiers_FUNC: u32 = #qualifier_bits;

        #[doc(hidden)]
        #[allow(warnings)]
        fn __anodized_fn_requires_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
            let _ = | | COND_1;
            let _ = | | COND_2;
            let _ = | | COND_3;
        }

        #[doc(hidden)]
        #[allow(warnings)]
        fn __anodized_fn_maintains_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
            let _ = | | COND_4;
            let _ = | | COND_5;
            let _ = | | COND_6;
        }

        #[doc(hidden)]
        #[allow(warnings)]
        fn __anodized_fn_ensures_FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) {
            let (ALIAS_1, (ALIAS_2, ALIAS_3)) = ((| | EXPR_1)(), (| | EXPR_2)());
            let _ = |PAT_1: &RET_TYPE| COND_7;
            let _ = |PAT_1: &RET_TYPE| COND_8;
            let _ = |PAT_2: TYPE| COND_9;
        }

        fn FUNC(&self, PARAM_1: TYPE_1, PARAM_2: TYPE_2) -> RET_TYPE {
            BODY
        }
    };

    let observed = Config::DEFAULT
        .instrument_item_fn(fn_spec, item_fn)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

fn make_fn_body() -> Block {
    parse_quote! {
        {
            this_is_the_body()
        }
    }
}

fn make_return_type() -> Type {
    parse_quote! { SomeType }
}

#[test]
fn simple_requires() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn requires_disable_runtime_checks() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let observed = Config::DEFAULT
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    let expected: Block = body;
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn requires_no_panic_runtime() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            if !((| | CONDITION_1)()) {
                eprintln!("Precondition failed: {}", "CONDITION_1");
            }
            let (__anodized_output): (#ret_type) = ((|| #body)());
            __anodized_output
        }
    };

    let observed = Config::PRINT
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_maintains() {
    let spec: Spec = parse_quote! {
        maintains: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Pre-invariant failed: {}", "CONDITION_1");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_1)(), "Post-invariant failed: {}", "CONDITION_1");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_ensures() {
    let spec: Spec = parse_quote! {
        ensures: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((|output: &#ret_type| CONDITION_1)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_1");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_requires_and_maintains() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        maintains: CONDITION_2,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            assert!((| | CONDITION_2)(), "Pre-invariant failed: {}", "CONDITION_2");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_2)(), "Post-invariant failed: {}", "CONDITION_2");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_requires_and_ensures() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        ensures: CONDITION_2,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((|output: &#ret_type| CONDITION_2)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_2");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_maintains_and_ensures() {
    let spec: Spec = parse_quote! {
        maintains: CONDITION_1,
        ensures: CONDITION_2,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Pre-invariant failed: {}", "CONDITION_1");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_1)(), "Post-invariant failed: {}", "CONDITION_1");
            assert!((|output: &#ret_type| CONDITION_2)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_2");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_requires_maintains_and_ensures() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        maintains: CONDITION_2,
        ensures: CONDITION_3,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            assert!((| | CONDITION_2)(), "Pre-invariant failed: {}", "CONDITION_2");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_2)(), "Post-invariant failed: {}", "CONDITION_2");
            assert!((|output: &#ret_type| CONDITION_3)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_3");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn simple_async_requires_maintains_and_ensures() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        maintains: CONDITION_2,
        ensures: CONDITION_3,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = true;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            assert!((| | CONDITION_2)(), "Pre-invariant failed: {}", "CONDITION_2");
            let (__anodized_output): (#ret_type) = ((async || #body)().await);
            assert!((| | CONDITION_2)(), "Post-invariant failed: {}", "CONDITION_2");
            assert!((|output: &#ret_type| CONDITION_3)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_3");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn multiple_conditions_in_clauses() {
    let spec: Spec = parse_quote! {
        requires: [CONDITION_1, CONDITION_2],
        maintains: [CONDITION_3, CONDITION_4],
        ensures: [CONDITION_5, CONDITION_6],
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            assert!((| | CONDITION_2)(), "Precondition failed: {}", "CONDITION_2");
            assert!((| | CONDITION_3)(), "Pre-invariant failed: {}", "CONDITION_3");
            assert!((| | CONDITION_4)(), "Pre-invariant failed: {}", "CONDITION_4");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_3)(), "Post-invariant failed: {}", "CONDITION_3");
            assert!((| | CONDITION_4)(), "Post-invariant failed: {}", "CONDITION_4");
            assert!((|output: &#ret_type| CONDITION_5)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_5");
            assert!((|output: &#ret_type| CONDITION_6)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_6");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn binds_parameter() {
    let spec: Spec = parse_quote! {
        binds: OUTPUT_PATTERN,
        ensures: CONDITION_1,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((|OUTPUT_PATTERN: &#ret_type| CONDITION_1)(&__anodized_output), "Postcondition failed: {}", "| OUTPUT_PATTERN | CONDITION_1");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn ensures_with_mixed_conditions() {
    let spec: Spec = parse_quote! {
        ensures: [
            CONDITION_1,
            |PATTERN_1| CONDITION_2,
            CONDITION_3,
            |PATTERN_2| CONDITION_4
        ],
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((|output: &#ret_type| CONDITION_1)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_1");
            assert!((|PATTERN_1: &#ret_type| CONDITION_2)(&__anodized_output), "Postcondition failed: {}", "| PATTERN_1 | CONDITION_2");
            assert!((|output: &#ret_type| CONDITION_3)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_3");
            assert!((|PATTERN_2: &#ret_type| CONDITION_4)(&__anodized_output), "Postcondition failed: {}", "| PATTERN_2 | CONDITION_4");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn cfg_attributes() {
    let spec: Spec = parse_quote! {
        #[cfg(SETTING_1)]
        requires: CONDITION_1,
        #[cfg(SETTING_2)]
        maintains: CONDITION_2,
        #[cfg(SETTING_3)]
        ensures: CONDITION_3,
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            if cfg!(SETTING_1) {
                assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            }
            if cfg!(SETTING_2) {
                assert!((| | CONDITION_2)(), "Pre-invariant failed: {}", "CONDITION_2");
            }
            let (__anodized_output): (#ret_type) = ((|| #body)());
            if cfg!(SETTING_2) {
                assert!((| | CONDITION_2)(), "Post-invariant failed: {}", "CONDITION_2");
            }
            if cfg!(SETTING_3) {
                assert!((|output: &#ret_type| CONDITION_3)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_3");
            }
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn cfg_on_single_and_list_conditions() {
    let spec: Spec = parse_quote! {
        #[cfg(SETTING_1)]
        requires: CONDITION_1,
        maintains: [CONDITION_2, CONDITION_3],
        #[cfg(SETTING_2)]
        ensures: [CONDITION_4, CONDITION_5],
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            if cfg!(SETTING_1) {
                assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            }
            assert!((| | CONDITION_2)(), "Pre-invariant failed: {}", "CONDITION_2");
            assert!((| | CONDITION_3)(), "Pre-invariant failed: {}", "CONDITION_3");
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_2)(), "Post-invariant failed: {}", "CONDITION_2");
            assert!((| | CONDITION_3)(), "Post-invariant failed: {}", "CONDITION_3");
            if cfg!(SETTING_2) {
                assert!((|output: &#ret_type| CONDITION_4)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_4");
            }
            if cfg!(SETTING_2) {
                assert!((|output: &#ret_type| CONDITION_5)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_5");
            }
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn complex_mixed_conditions() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        #[cfg(SETTING_1)]
        requires: [CONDITION_2, CONDITION_3],
        maintains: [CONDITION_4, CONDITION_5],
        #[cfg(SETTING_2)]
        maintains: CONDITION_6,
        ensures: CONDITION_7,
        #[cfg(SETTING_3)]
        ensures: [CONDITION_8, |PATTERN_1| CONDITION_9],
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            if cfg!(SETTING_1) {
                assert!((| | CONDITION_2)(), "Precondition failed: {}", "CONDITION_2");
            }
            if cfg!(SETTING_1) {
                assert!((| | CONDITION_3)(), "Precondition failed: {}", "CONDITION_3");
            }
            assert!((| | CONDITION_4)(), "Pre-invariant failed: {}", "CONDITION_4");
            assert!((| | CONDITION_5)(), "Pre-invariant failed: {}", "CONDITION_5");
            if cfg!(SETTING_2) {
                assert!((| | CONDITION_6)(), "Pre-invariant failed: {}", "CONDITION_6");
            }
            let (__anodized_output): (#ret_type) = ((|| #body)());
            assert!((| | CONDITION_4)(), "Post-invariant failed: {}", "CONDITION_4");
            assert!((| | CONDITION_5)(), "Post-invariant failed: {}", "CONDITION_5");
            if cfg!(SETTING_2) {
                assert!((| | CONDITION_6)(), "Post-invariant failed: {}", "CONDITION_6");
            }
            assert!((|output: &#ret_type| CONDITION_7)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_7");
            if cfg!(SETTING_3) {
                assert!((|output: &#ret_type| CONDITION_8)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_8");
            }
            if cfg!(SETTING_3) {
                assert!((|PATTERN_1: &#ret_type| CONDITION_9)(&__anodized_output), "Postcondition failed: {}", "| PATTERN_1 | CONDITION_9");
            }
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}

#[test]
fn captures() {
    let spec: Spec = parse_quote! {
        requires: CONDITION_1,
        captures: [
            EXPR_1 as ALIAS_1,
            EXPR_2 as ALIAS_2,
        ],
        ensures: [
            CONDITION_2,
            CONDITION_3,
        ],
    };
    let body = make_fn_body();
    let ret_type = make_return_type();
    let is_async = false;

    let expected: Block = parse_quote! {
        {
            assert!((| | CONDITION_1)(), "Precondition failed: {}", "CONDITION_1");
            let (ALIAS_1, ALIAS_2, __anodized_output): (_, _, #ret_type) = ((| | EXPR_1) (), (| | EXPR_2) (), (|| #body)());
            assert!((|output: &#ret_type| CONDITION_2)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_2");
            assert!((|output: &#ret_type| CONDITION_3)(&__anodized_output), "Postcondition failed: {}", "| output | CONDITION_3");
            __anodized_output
        }
    };

    let observed = Config::PANIC
        .instrument_fn_body(&spec, &body, is_async, &ret_type)
        .unwrap();
    assert_tokens_eq(&observed, &expected);
}