Better goto-instrument error reporting for missing files

[NlightNFotis]

In the past, goto-instrument was failing with the default --help error message if it didn't get the correct number of positional arguments, making it unnecessarily hard to understand what was failing and why (since the help message is long and it also didn't have any particular signalling for what went wrong). This makes it so that it reports it as an invalid user input exception. Fixes #2861.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[NlightNFotis]

Before the change, this looked like this:

$ goto-instrument main.gb
Reading GOTO program from `main.gb'

* *  Goto-Instrument 5.11 (cbmc-5.11-1461-g99aabb4) 64-bit  * *
* *                 Copyright (C) 2008-2013                 * *
* *                     Daniel Kroening                     * *
* *                  [email protected]                  * *

Usage:                       Purpose:

 goto-instrument [-?] [-h] [--help]  show help
 goto-instrument in out              perform instrumentation

Main options:
 --document-properties-html   generate HTML property documentation
 --document-properties-latex  generate Latex property documentation
 --dump-c                     generate C source
 --dump-cpp                   generate C++ source
 --dot                        generate CFG graph in DOT format
 --interpreter                do concrete execution

Diagnosis:
 --show-loops                 show the loops in the program
 --show-properties            show the properties, but don't run analysis
 --show-symbol-table          show loaded symbol table
 --list-symbols               list symbols with type information
 --show-goto-functions        show loaded goto program
 --list-goto-functions        list loaded goto functions
 --count-eloc                 count effective lines of code
 --list-eloc                  list full path names of lines containing code
 --print-global-state-size    count the total number of bits of global objects
 --print-path-lengths         print statistics about control-flow graph paths
 --drop-unused-functions      drop functions trivially unreachable from main function
 --print-internal-representation
                              show verbose internal representation of the program
 --list-undefined-functions   list functions without body
 --show-struct-alignment      show struct members that might be concurrently accessed
 --show-natural-loops         show natural loop heads
 --list-calls-args            list all function calls with their arguments
 --call-graph                 show graph of function calls
 --reachable-call-graph       show graph of function calls potentially reachable from main function
 --show-class-hierarchy       show the class hierarchy
 --show-threaded              show instructions that may be executed by more than one thread
 --show-local-safe-pointers   show pointer expressions that are trivially dominated by a not-null check
 --show-safe-dereferences     show pointer expressions that are trivially dominated by a not-null check
                              *and* used as a dereference operand
 --validate-goto-model        enable additional well-formedness checks on the
                              goto program
 --validate-ssa-equation      enable additional well-formedness checks on the
                              SSA representation
 --validate-goto-binary       check the well-formedness of the passed in goto
                              binary and then exit

Safety checks:
 --no-assertions              ignore user assertions
 --bounds-check               enable array bounds checks
 --pointer-check              enable pointer checks
 --memory-leak-check          enable memory leak checks
 --div-by-zero-check          enable division by zero checks
 --signed-overflow-check      enable signed arithmetic over- and underflow checks
 --unsigned-overflow-check    enable arithmetic over- and underflow checks
 --pointer-overflow-check     enable pointer arithmetic over- and underflow checks
 --conversion-check           check whether values can be represented after type cast
 --undefined-shift-check      check shift greater than bit-width
 --float-overflow-check       check floating-point for +/-Inf
 --nan-check                  check floating-point for NaN
 --no-built-in-assertions     ignore assertions in built-in library
 --uninitialized-check        add checks for uninitialized locals (experimental)
 --error-label label          check that label is unreachable
 --stack-depth n              add check that call stack size of non-inlined functions never exceeds n
 --race-check                 add floating-point data race checks

Semantic transformations:
 --nondet-volatile            makes reads from volatile variables non-deterministic
 --unwind <n>                 unwinds the loops <n> times
 --unwindset L:B,...          unwind loop L with a bound of B
 --unwindset-file <file>      read unwindset from file
 --partial-loops              permit paths with partial loops
 --unwinding-assertions       generate unwinding assertions
 --continue-as-loops          add loop for remaining iterations after unwound part
 --isr <function>             instruments an interrupt service routine
 --mmio                       instruments memory-mapped I/O
 --nondet-static              add nondeterministic initialization of variables with static lifetime
 --check-invariant function   instruments invariant checking function
 --remove-pointers            converts pointer arithmetic to base+offset expressions
 --splice-call caller,callee  prepends a call to callee in the body of caller
 --undefined-function-is-assume-false
                              convert each call to an undefined function to assume(false)
 --generate-function-body <regex>
                              Generate bodies for functions matching regex
 --generate-function-body-options <option>
                              One of assert-false, assume-false,
                              nondet-return, assert-false-assume-false and
                              havoc[,params:<regex>][,globals:<regex>]
                              (default: nondet-return) --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;
                              at level N pointers are set to null
 --min-null-tree-depth N      minimum level at which a pointer can first be
                              NULL in a recursively nondet initialized struct

Loop transformations:
 --k-induction <k>            check loops with k-induction
 --step-case                  k-induction: do step-case
 --base-case                  k-induction: do base-case
 --havoc-loops                over-approximate all loops
 --accelerate                 add loop accelerators
 --skip-loops <loop-ids>      add gotos to skip selected loops during execution

Memory model instrumentations:
 --mm <tso,pso,rmo,power>     instruments a weak memory model
 --scc                        detects critical cycles per SCC (one thread per SCC)
 --one-event-per-cycle        only instruments one event per cycle
 --minimum-interference       instruments an optimal number of events
 --my-events                  only instruments events whose ids appear in inst.evt
 --cfg-kill                   enables symbolic execution used to reduce spurious cycles
 --no-dependencies            no dependency analysis
 --no-po-rendering            no representation of the threads in the dot
 --render-cluster-file        clusterises the dot by files
 --render-cluster-function    clusterises the dot by functions

Slicing:
 --fp-reachability-slice f    remove instructions that cannot appear on a trace
                              that visits all given functions. The list of
                              functions has to be given as a comma separated
                              list f.
 --reachability-slice         remove instructions that cannot appear on a trace
                              from entry point to a property
 --full-slice                 slice away instructions that don't affect assertions
 --property id                slice with respect to specific property only
 --slice-global-inits         slice away initializations of unused global variables
 --aggressive-slice           remove bodies of any functions not on the shortest path between
                              the start function and the function containing the property(s)
 --aggressive-slice-call-depth <n>
                              used with aggressive-slice, preserves all functions within <n> function calls
                              of the functions on the shortest path
 --aggressive-slice-preserve-function <f>
                             force the aggressive slicer to preserve function <f>
 --aggressive-slice-preserve-function containing <f>
                              force the aggressive slicer to preserve all functions with names containing <f>
--aggressive-slice-preserve-all-direct-paths 
                             force aggressive slicer to preserve all direct paths

Further transformations:
 --constant-propagator        propagate constants and simplify expressions
 --inline                     perform full inlining
 --partial-inline             perform partial inlining
 --function-inline <function> transitively inline all calls <function> makes
 --no-caching                 disable caching of intermediate results during transitive function inlining
 --log <file>                 log in json format which code segments were inlined, use with --function-inline
 --remove-function-pointers   replace function pointers by case statement over function calls
 --remove-calls-no-body       remove calls to functions without a body
 --remove-const-function-pointers    Remove function pointers that are constant or constant part of an array
 --add-library                add models of C library functions
 --model-argc-argv <n>        model up to <n> command line arguments
 --remove-function-body <f>   remove the implementation of function <f> (may be repeated)
 --replace-calls f:g           replace calls to f with calls to g

Other options:
 --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes
 --use-all-headers            with --dump-c/--dump-cpp: generate C source with all includes
 --harness                    with --dump-c/--dump-cpp: include input generator in output
 --version                    show version and exit
 --flush                      flush every line of output
 --xml-ui                     use XML-formatted output
 --json-ui                    use JSON-formatted output
 --timestamp <monotonic|wall> print microsecond-precision timestamps.
                              monotonic: stamps increase monotonically.
                              wall: ISO-8601 wall clock timestamps.

Notice how there's no indicator of any failed process, and it's nearly indistinguishible from a successful execution (aside from an extra --help message, which is confusing because it comes with no indicator as to why it appeared). Now it looks like this:

$ goto-instrument main.gb
Reading GOTO program from `main.gb'
Invalid User Input
Option: [in] [out]
Reason: Invalid number of positional arguments passed
Suggestion: goto-instrument needs one input and one output file, aside from other flags

[tautschnig]

Thank you :-)

[danpoe]

Looks good to me. Maybe we could throw an exception as well right at the beginning in doit() when cmdline.args.size()!=1 && cmdline.args.size()!=2 holds.

[chrisr-diffblue]

You could also maybe add an additional line here to say "use goto-instrument --help for additional help" or something similar.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: fd5b9c0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101077690