WIP: use argparse to parse CLI options #242
Conversation
|
@lzaoral Hi. Could you have a look whether you see something wrong with the patch conceptually, e.g. the FIXME comment about transition to argparse does not hold anymore? I have opened this PR before the migration is fully finished so I can gather your feedback before I invest too much effort into the wrong direction 😸 |
There was a problem hiding this comment.
Thanks A LOT, @MichalHe for this effort! Minor nits inline. It would be nice to use multiline strings for the help messages (so that you don't have to escape the ' and the newlines are redundant), do some parsing for the comma-separated lists, use metavals for options that take arguments, and maybe group related options into argument groups?
You can look into https://gist.github.com/lzaoral/6872728c1af2eb28d85b85f2baf81d6b for the inspiration (comma-separated list parsing, options you haven't ported yet, some additional kwargs for options you've already ported and maybe some tweaks to the help messages). I've actually started the migration like an year ago but since then I did not have the time or need to finish it so this gist is all I've done.
| arg_parser.add_argument('--verifier', metavar='VERIFIER_TOOL', | ||
| choices=['Ceagle', 'KLEE', 'CPAchecker', 'Seahorn', 'Skink', 'Smack'], | ||
| help=('Use the tool \'name\'. Default is KLEE, other tools that\n' | ||
| 'can be integrated are Ceagle, CPAchecker, Seahorn,\n' | ||
| 'Skink and SMACK.')) | ||
|
|
||
| arg_parser.add_argument('--target', metavar='VERIFIER_TOOL', | ||
| choices=['Ceagle', 'KLEE', 'CPAchecker', 'Seahorn', 'Skink', 'Smack'], | ||
| help=('Use the tool \'name\'. Default is KLEE, other tools that\n' | ||
| 'can be integrated are Ceagle, CPAchecker, Seahorn,\n' | ||
| 'Skink and SMACK. Synonymous to --verifier.')) |
There was a problem hiding this comment.
You can combine these options into one:
| arg_parser.add_argument('--verifier', metavar='VERIFIER_TOOL', | |
| choices=['Ceagle', 'KLEE', 'CPAchecker', 'Seahorn', 'Skink', 'Smack'], | |
| help=('Use the tool \'name\'. Default is KLEE, other tools that\n' | |
| 'can be integrated are Ceagle, CPAchecker, Seahorn,\n' | |
| 'Skink and SMACK.')) | |
| arg_parser.add_argument('--target', metavar='VERIFIER_TOOL', | |
| choices=['Ceagle', 'KLEE', 'CPAchecker', 'Seahorn', 'Skink', 'Smack'], | |
| help=('Use the tool \'name\'. Default is KLEE, other tools that\n' | |
| 'can be integrated are Ceagle, CPAchecker, Seahorn,\n' | |
| 'Skink and SMACK. Synonymous to --verifier.')) | |
| arg_parser.add_argument('--target', '--verifier', default='klee', ...) |
Also, since KLEE is the default, it should be reflected using the default kwarg. Don't forget to update the help message.
I'm not that familiar with this part of Symbiotic, but the list of all supported verifiers should be stored in the following dictionary, so the current choices in the argument won't actually work (@mchalupa can you please confirm?):
symbiotic/lib/symbioticpy/symbiotic/targets/__init__.py
Lines 24 to 52 in bfc50eb
| # TODO(MichalHe): @review maybe it should be more robust to use choices here | ||
| arg_parser.add_argument('--no-link', metavar='CATEGORIES', | ||
| help=('Do not link missing functions from the given category\n' | ||
| '(libc, svcomp, verifier, posix, kernel). The argument\n' | ||
| 'is a comma-separated list of values.')) |
There was a problem hiding this comment.
Yeah, categories would be awesome! The list is the following (without symbitoicpy): https://github.com/staticafi/symbiotic/tree/main/lib
| # TODO(MichalHe): @review Original docs contain a fragment `but continue searching` after the end of sentence. | ||
| # maybe a left over? |
There was a problem hiding this comment.
Nice catch! Yes, that was a leftover from 7e32ff8.
| arg_parser.add_argument('--dump-env', action='store_true', | ||
| default=False, help='Only dump environment variables (for debugging)') | ||
| arg_parser.add_argument('--dump-env-cmd', action='store_true', | ||
| default=False, help='Dump environment variables for using them in command line') |
There was a problem hiding this comment.
Nit. default values for store_X are redundant.
| arg_parser.add_argument('--malloc-never-fails', action='store_true', default=False, | ||
| help='Suppose malloc and calloc never return NULL') | ||
| arg_parser.add_argument('--undefines-are-pure', action='store_true', default=False, | ||
| help='Suppose that undefined functions have no side-effects') | ||
| arg_parser.add_argument('--statistics', action='store_true', default=False, help='Dump statistics about bitcode') |
| # # TODO(MichalHe): @review Missing docs. | ||
| arg_parser.add_argument('--cc', dest='run_in_cc_mode', default=False, | ||
| help='') |
There was a problem hiding this comment.
@mchalupa any ideas? I've never used this option myself.
| # # TODO(MichalHe): @review Docs filled in. | ||
| arg_parser.add_argument('--link', default='', metavar='LINKFILES', | ||
| help='A comma separated list of extra link files.') |
There was a problem hiding this comment.
Would be nice to expand the help message with a description of the format these file should be in.
| """ Return a tuple (VERSION, versions, llvm_versions) """ | ||
| """ Return a tuple (VERSION, versions, llvm_versions) """ |
There was a problem hiding this comment.
Probably committed by a mistake.
|
On a second thought, the argument groups in the linked gist are not really thought through, something like: compilation, slicing, instrumentation, optimization, verification, etc... would be better a better distinction. |
Rewrites CLI options parsing from
getopttoargparse(based on the FIXME comment above).