rem-verification 0.1.0

Verification tool for the REM toolchain. Built to be implemented into the VSCode extension for REM. Relies on AENEAS and CoQ
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

use clap::{ArgAction, Parser, Subcommand};
use std::path::PathBuf;

// Local modules
use crate::messages::{about::ABOUT, author::AUTHOR, version::VERSION};

#[derive(Parser)]
#[command(
    version = VERSION,
    about = ABOUT,
    author = AUTHOR,
)]
pub struct CLIArgs {
    #[command(subcommand)]
    pub command: CLICommands,
}

#[derive(Subcommand)]
pub enum CLICommands {
    /// Run the whole process. Converts the LLBC files to CoQ, then
    /// runs verification checks on the CoQ files.
    Run {
        #[arg(help = "Path to the LLBC of the original program.")]
        original_llbc: PathBuf,

        #[arg(help = "Path to the LLBC of the refactored program.")]
        refactored_llbc: PathBuf,

        #[arg(help = "Top Level Function Name")]
        top_level_function: String,

        /// Optional output directory for the generated `.v` files
        #[arg(short, long, help = "Output directory for generated Coq files")]
        out_dir: Option<PathBuf>,

        #[arg(short, long, help = "Enable verbose output", action = ArgAction::SetTrue)]
        verbose: bool,

        #[arg(short, long, help = "Cleanup all files other than .llbc", action= ArgAction::SetTrue)]
        cleanup: bool,

        /// Optional path to the Aeneas binary.
        #[arg(long, help = "Optional path to the Aeneas binary")]
        aeneas_path: Option<PathBuf>,
    },

    /// Run various verification checks on the CoQ files.
    Verify {
        #[arg(help = "Path to the CoQ of the original program.")]
        original_coq: PathBuf,

        #[arg(help = "Path to the CoQ of the refactored program.")]
        refactored_coq: PathBuf,

        #[arg(help = "Top Level Function Name")]
        top_level_function: String,

        #[arg(short, long, help = "Enable verbose output", action = ArgAction::SetTrue)]
        verbose: bool,

        /// Optional path to the Aeneas binary.
        #[arg(long, help = "Optional path to the Aeneas binary")]
        aeneas_path: Option<PathBuf>,
    },

    /// Convert the LLBC files to CoQ using AENEAS.
    Convert {
        #[arg(help = "Path to the LLBC of the original program.")]
        original_llbc: PathBuf,

        #[arg(help = "Path to the LLBC of the refactored program.")]
        refactored_llbc: PathBuf,

        /// Optional output directory for the generated `.llbc` files
        #[arg(short, long, help = "Output directory for generated llbc files")]
        out_dir: Option<PathBuf>,

        #[arg(short, long, help = "Enable verbose output", action = ArgAction::SetTrue)]
        verbose: bool,

        /// Optional path to the Aeneas binary.
        #[arg(long, help = "Optional path to the Aeneas binary")]
        aeneas_path: Option<PathBuf>,
    },

    /// Run the crate tests.
    Test {
        #[arg(short, long, help = "Enable verbose test output", action = ArgAction::SetTrue)]
        verbose: bool,

        /// Optional path to the Aeneas binary.
        #[arg(long, help = "Optional path to the Aeneas binary")]
        aeneas_path: Option<PathBuf>,
    },
}