vargo: refactor to use clap and clean up code

[bsdinis]

Motivation

Vargo is quite inscrutable from a user perspective. Besides the most basic subcommands, figuring out the options requires looking over the code. However, vargo's code was... complicated.
This PR refactors vargo into a hopefully cleaner structure, which would allow new contributors to have a better experience when developing and would allow us to add support for more cargo commands without much hassle (e.g., I think running cargo-clippy on our codebase might be worthwhile).

Apologies for the big diff. I sincerely could not find a piecemeal way of breaking this up. See Testing for more details on how I validated the changes were correct.

The changes

This started as a migration to clap, which will help us by having a nice cli help cmd.

new CLI interface

% vargo
Usage: vargo [OPTIONS] <COMMAND>

Commands:
  build     Build Verus
  test      Run Verus tests
  nextest   Run Verus tests with nextest
  run       Run a binary package
  clean     Clean current build
  metadata  Get metadata from cargo
  fmt       Run the formatter on the codebase
  cmd       Run an arbitrary command in vargo's environment
  update    Update dependencies
  help      Print this message or the help of the given subcommand(s)

Options:
      --offline                  Run without accessing the network
  -v, --verbose...               Use verbose output
      --color <COLOR>            Coloring [default: auto] [possible values: auto, always, never]
      --vargo-verbose            Turn on `vargo`s verbose logging
      --no-solver-version-check  Skip checking that the server's solver version is correct
  -h, --help                     Print help

`vargo build` CLI example

% vargo build --help
Build Verus

Usage: vargo build [OPTIONS] [-- <VERUS_ARGS>...]

Arguments:
  [VERUS_ARGS]...  Arguments to pass on to verus (in case verification is needed)

Options:
  -p, --package <PACKAGE>    Package to build
      --exclude <EXCLUDE>    Exclude packages from building
      --no-default-features  Do not activate the default features
  -F, --features <FEATURES>  Features to activate [possible values: singular, axiom-usage-info, record-history]
  -r, --release              Build artifacts in release mode, with optimizations
      --vstd-no-verify       Do not verify vstd when building
      --vstd-no-std          Build vstd in `no-std` mode
      --vstd-no-alloc        Build vstd in `no-alloc` mode
      --vstd-trace           Turn tracing on when building vstd
      --vstd-log-all         Turn verbose logging on when building vstd
  -h, --help                 Print help

Because of vargos previously intertwined structure (argument parsing and execution were intermingled, and executing a subcommand was done in stages, mixed with more argument parsing, in a function with 1000+ lines) the diff is less than clean (i.e., it shows a full removal and full addition, even though many core lines of code were just transplanted into their own functions)

But, overall, the changes are as follows:

• A new cli module that handles parsing with clap
• A new context module that builds the context for vargo (e.g., where is the target dir)
• A new commands module. Each submodule corresponds to a subcommand (e.g., vargo build), and implements the core logic for that command
• All the SmtBinary... functions were moved to a smt_solver module

Testing

Because the changes are so large, I suspect reviewing per line of code will be less than scalable.

To that end, here I scripts I developed to test the changes. They essentially run vargo in verbose mode and allow for comparing the logs between the old and new version. I recommend running them on two fresh clones of the repo.

Test Script (test_vargo.sh)

#!/usr/bin/env zsh

set -x
set -e

# vargo clean is not assumed to be correct
rm -rf target target-verus

# vargo build tests
vargo --vargo-verbose -vv build -p rust_verify &> build_rust_verify.log
vargo --vargo-verbose -vv build -p rust_verify --release &> build_rust_verify_release.log

# test vargo clean
vargo clean --release &> clean_release.log
vargo clean &> clean.log

vargo --vargo-verbose -vv build &> build.log
vargo --vargo-verbose -vv build --release &> build_release.log
vargo --vargo-verbose -vv build --features record-history &> build_record_history.log

vargo clean &> /dev/null

# test vargo test
vargo --vargo-verbose -vv test --package rust_verify_test test_out_of_order &> test.log
vargo --vargo-verbose -vv test --package rust_verify_test --release test_out_of_order &> test_release.log

vargo clean &> /dev/null

# test vargo nextest
vargo --vargo-verbose -vv nextest run --package rust_verify_test test_out_of_order &> nextest.log
vargo --vargo-verbose -vv nextest run --package rust_verify_test --release test_out_of_order &> nextest_release.log

vargo clean &> /dev/null

# test vargo run
vargo --vargo-verbose -vv run --package rust_verify -- ../examples/adts.rs &> run.log
vargo --vargo-verbose -vv run --package rust_verify --release -- ../examples/adts.rs &> run_release.log

# test vargo metadata
vargo --vargo-verbose -vv metadata &> metadata.log
vargo metadata --format-version 1 | jq --sort-keys . > metadata.json

# test vargo fmt
if [ "$1" = "--new" ]; then
vargo --vargo-verbose -vv fmt -- --check &> fmt.log
else
vargo --vargo-verbose fmt -- --check &> fmt.log
fi

# test vargo cmd
if [ "$1" = "--new" ]; then
  vargo --vargo-verbose -vv cmd echo a &> cmd.log
else
  vargo --vargo-verbose cmd echo a &> cmd.log
fi

# test vargo update
vargo --vargo-verbose -vv update &> update.log

Comparing logs (log_check.sh)

#!/usr/bin/env zsh

set -x
set -e

if [ $2 -ne 2 ];
then
    echo "usage: $0 <dir 1> <dir 2>"
    echo "point the script at two \`source\` dirs"
    exit 1
fi

DIR_1=$1
DIR_2=$2

function clean_output {
    # this looks for vargo log messages
    # removes the warning for not running in a git repo
    # removes ANSI color codes (new version bolds the info/warn/part)
    grep 'vargo' $1 \
    | grep -v 'could not obtain version info from git' \
    | sed  's/\x1b\[[0-9;]*[a-zA-Z]//g'
}

function cmp_logs {
    wdiff -n <( clean_output ${DIR_2}/$1) <( clean_output ${DIR_1}/$1) | colordiff
}

# vargo build tests
cmp_logs build_rust_verify.log
cmp_logs build_rust_verify_release.log

# test vargo clean
cmp_logs clean_release.log
cmp_logs clean.log

cmp_logs build.log
cmp_logs build_release.log
cmp_logs build_record_history.log

# test vargo test
cmp_logs test.log
cmp_logs test_release.log

# test vargo nextest
cmp_logs nextest.log
cmp_logs nextest_release.log

# test vargo run
cmp_logs run.log
cmp_logs run_release.log


# test vargo metadata
cmp_logs metadata.log
diff ${DIR_2}/metadata.json ${DIR_1}/metadata.json || echo


# test vargo fmt
cmp_logs fmt.log

# test vargo cmd
cmp_logs cmd.log

# test vargo update
cmp_logs update.log

To run and verify the tests, do the following.

$ cd new_verus/source
$ ./test_vargo.sh --new # this takes a while
$ cd ../../old_verus/source
$ ./test_vargo.sh # this takes a while
$ cd ../../
$ ./log_check.sh ./new_verus/source ./old_verus/source

Warning: running test_vargo will change the repo (it will write log files and run vargo update). Exercise caution.
(You can also extract the cmp_logs function from the script to analyze a particular log).

The main things I've found:

• Some flags old vargo does not accept new vargo does
• New vargo has all env variables on consistently
• New vargo writes --package <p> instead of -p <p>
• The order of arguments is different
• Instead of shelling out to itself to rebuild, new vargo just calls the build function.

These were the main differences I could grok. Functionally, they seem equivalent.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[bsdinis]

FYI, I have ready some more wholesale refactorings ready. Mainly moving error handling to anyhow and code organization in other vargo portions. I opted to leave it out of this PR since it's already to big, but if you prefer I can add it here.

[tjhance]

This looks fine to me, though please also get a review from @parno who knows more about build needs than I do.

[bsdinis]

One other thing that I was wondering about was VARGO_NEST. It seems to serve the purpose of counting how many times vargo is calling itself. But this refactoring eliminates that pattern. Might be worth removing it.

Similarly the VARGO_IN_NEXTEST was somewhat confusing when I was refactoring. I wonder if we could do without it (I don't think nextest can call vargo directly)

[bsdinis]

Similarly the VARGO_IN_NEXTEST was somewhat confusing when I was refactoring. I wonder if we could do without it (I don't think nextest can call vargo directly)

I now understand that nextest with vargo sets the CARGO env var to point to vargo itself. Is this needed?