anodized-core 0.6.0

Core interoperability for the Anodized specification system
Documentation 
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

use proc_macro2::TokenStream;
use syn::{ExprForLoop, ExprWhile, parse_quote};

use crate::{LoopSpec, instrument::Mode, test_util::assert_tokens_eq};

#[test]
fn embed_spec_expr_while() {
    let while_spec: LoopSpec = parse_quote! {
        maintains: [
            INVAR_1,
            INVAR_2,
        ],
        decreases: DECREASES_1,
    };
    let mut expr_while: ExprWhile = parse_quote! {
        while WHILE_COND {
            LOOP_BODY
        }
    };

    let expected: TokenStream = parse_quote! {
        while WHILE_COND {
            let __anodized_loop_maintains = || -> bool {
                let __anodized_clause_1 = (|| -> bool { INVAR_1 })();
                let __anodized_clause_2 = (|| -> bool { INVAR_2 })();
                __anodized_clause_1 && __anodized_clause_2
            };
            let __anodized_loop_decreases = || {
                let __anodized_value_1 = (|| DECREASES_1)();
                (__anodized_value_1)
            };
            LOOP_BODY
        }
    };

    Mode::EmbedSpecs.instrument_expr_while(while_spec, &mut expr_while);
    let observed = expr_while;

    assert_tokens_eq(&observed, &expected);
}

#[test]
fn embed_spec_expr_for() {
    let for_spec: LoopSpec = parse_quote! {
        maintains: [
            INVAR_1,
            INVAR_2,
        ],
    };
    let mut expr_for_loop: ExprForLoop = parse_quote! {
        for FOR_VAR in FOR_EXPR {
            LOOP_BODY
        }
    };

    let expected: TokenStream = parse_quote! {
        for FOR_VAR in FOR_EXPR {
            let __anodized_loop_maintains = || -> bool {
                let __anodized_clause_1 = (|| -> bool { INVAR_1 })();
                let __anodized_clause_2 = (|| -> bool { INVAR_2 })();
                __anodized_clause_1 && __anodized_clause_2
            };
            let __anodized_loop_decreases = || {};
            LOOP_BODY
        }
    };

    Mode::EmbedSpecs.instrument_expr_for_loop(for_spec, &mut expr_for_loop);
    let observed = expr_for_loop;

    assert_tokens_eq(&observed, &expected);
}