From b8bd639ad8c9252cfdc5317571dea390a1cf0ae0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 30 Jun 2019 11:30:05 -0700 Subject: [PATCH] [sledge] Generate and commit cli help Summary: To easily monitor and track changes to the help generated by the command line interface, generate it in full and add it to the repo. Reviewed By: kren1 Differential Revision: D16059783 fbshipit-source-id: be15f9943 --- sledge/Makefile | 4 +- sledge/dune | 8 ++ sledge/sledge-help.txt | 206 ++++++++++++++++++++++++++++++++++++ sledge/src/sledge.ml | 2 +- sledge/tools/gen_help.sh | 25 +++++ sledge/tools/gen_version.sh | 1 - 6 files changed, 242 insertions(+), 4 deletions(-) create mode 100644 sledge/sledge-help.txt create mode 100755 sledge/tools/gen_help.sh diff --git a/sledge/Makefile b/sledge/Makefile index a353f4201..378481fce 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -10,8 +10,8 @@ EXES = src/sledge INSTALLS = sledge FMTS = @_build/dev/src/fmt -DBG_TARGETS = $(patsubst %,_build/dev/%.exe,$(EXES)) $(patsubst %,_build/dev/%.install,$(INSTALLS)) -OPT_TARGETS = $(patsubst %,_build/release/%.exe,$(EXES)) $(patsubst %,_build/release/%.install,$(INSTALLS)) +DBG_TARGETS = $(patsubst %,_build/dev/%.exe,$(EXES)) $(patsubst %,_build/dev/%.install,$(INSTALLS)) _build/dev/sledge-help.txt +OPT_TARGETS = $(patsubst %,_build/release/%.exe,$(EXES)) $(patsubst %,_build/release/%.install,$(INSTALLS)) _build/release/sledge-help.txt DUNEINS = $(shell find src model -name dune.in) DUNES = $(patsubst %.in,%,$(DUNEINS)) diff --git a/sledge/dune b/sledge/dune index da639ce8d..3ed3699a8 100644 --- a/sledge/dune +++ b/sledge/dune @@ -1 +1,9 @@ (ignored_subdirs (llvm test)) + +(rule + (targets sledge-help.txt) + (deps src/sledge.ml src/sledge_buck.ml tools/gen_help.sh src/sledge.exe) + (action + (with-stdout-to sledge-help.txt + (run tools/gen_help.sh))) + (mode promote-until-clean)) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt new file mode 100644 index 000000000..4c9ca6d88 --- /dev/null +++ b/sledge/sledge-help.txt @@ -0,0 +1,206 @@ +SLEdge static analyzer + + sledge SUBCOMMAND + +The [-trace ] argument of each subcommand enables debug tracing according to , which is a sequence of module and function names separated by + or -. For example, M-M.f enables all tracing in the M module except the M.f function. The value * enables all debug tracing. + +=== subcommands === + + buck integration with Buck + . analyze analyze buck target + . bitcode report bitcode files in buck target + . link link buck target to LLVM bitcode + llvm integration with LLVM + . analyze analyze LLVM bitcode + . translate translate LLVM bitcode to LLAIR + analyze analyze LLAIR code + disassemble print LLAIR code in textual form + version print version information + help explain a given subcommand (perhaps recursively) + + +====== sledge buck ====== + +integration with Buck + + sledge buck SUBCOMMAND + +Code can be provided by a buck build target, such as //fully/qualified/build:target. The mechanism used to integrate with buck uses the arguments passed to the linker, so the target must specify a binary that will be linked, not for instance a library archive. Sledge passes the --config sledge.build=True flag to buck, which can be used to configure buck targets for sledge. + +=== subcommands === + + analyze analyze buck target + bitcode report bitcode files in buck target + link link buck target to LLVM bitcode + help explain a given subcommand (perhaps recursively) + + +====== sledge buck analyze ====== + +analyze buck target + + sledge buck analyze + +Analyze code in a buck target. This is a convenience wrapper for the sequence `sledge buck bitcode`; `sledge llvm translate`; `sledge analyze`. + +=== flags === + + [-bound ] stop execution exploration at depth + [-function-summaries] use function summaries (in development) + [-lib-fuzzer] add a harness for lib fuzzer binaries + [-output-llair ] write generated LLAIR to + [-output-modules ] write list of bitcode files to + [-skip-throw] do not explore past throwing an exception + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge buck bitcode ====== + +report bitcode files in buck target + + sledge buck bitcode + +Build a buck target and report the included bitcode files. + +=== flags === + + [-output-modules ] write list of bitcode files to + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge buck link ====== + +link buck target to LLVM bitcode + + sledge buck link + +Link code in a buck target to a single LLVM bitcode module. This also internalizes all symbols except `main` and removes dead code. + +=== flags === + + -output write linked output to + [-lib-fuzzer] add a harness for lib fuzzer binaries + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge llvm ====== + +integration with LLVM + + sledge llvm SUBCOMMAND + +Code can be provided by one or more LLVM bitcode files. + +=== subcommands === + + analyze analyze LLVM bitcode + translate translate LLVM bitcode to LLAIR + help explain a given subcommand (perhaps recursively) + + +====== sledge llvm analyze ====== + +analyze LLVM bitcode + + sledge llvm analyze [ ...] + +Analyze code in one or more LLVM bitcode files. This is a convenience wrapper for the sequence `sledge llvm translate`; `sledge analyze`. + +=== flags === + + [-bound ] stop execution exploration at depth + [-function-summaries] use function summaries (in development) + [-lib-fuzzer] add a harness for lib fuzzer binaries + [-output-llair ] write generated LLAIR to + [-skip-throw] do not explore past throwing an exception + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge llvm translate ====== + +translate LLVM bitcode to LLAIR + + sledge llvm translate [ ...] + +Translate one or more LLVM bitcode files to LLAIR. Each filename may be either: an LLVM bitcode file, in binary (.bc) or textual (.ll) form; or of the form @, where names a file containing one per line. + +=== flags === + + [-lib-fuzzer] add a harness for lib fuzzer binaries + [-output-llair ] write generated LLAIR to + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge analyze ====== + +analyze LLAIR code + + sledge analyze + +The file must be binary LLAIR, such as produced by `sledge translate`. + +=== flags === + + [-bound ] stop execution exploration at depth + [-function-summaries] use function summaries (in development) + [-skip-throw] do not explore past throwing an exception + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge disassemble ====== + +print LLAIR code in textual form + + sledge disassemble + +The file must be LLAIR code, as produced by `sledge llvm translate`. + +=== flags === + + [-output ] write generated textual LLAIR to , or to standard + output if omitted + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) + + +====== sledge version ====== + +print version information + + sledge version + +=== flags === + + [-build-info] print build info for this build + [-version] print the version of this build + [-help] print this help text and exit + (alias: -?) + + +====== sledge help ====== + +explain a given subcommand (perhaps recursively) + + sledge help [SUBCOMMAND] + +=== flags === + + [-expand-dots] expand subcommands in recursive help + [-flags] show flags as well in recursive help + [-recursive] show subcommands of subcommands, etc. + [-help] print this help text and exit + (alias: -?) + diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 5b4814e08..7ebd44f59 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -68,7 +68,7 @@ let analyze = ~doc:"do not explore past throwing an exception" and function_summaries = flag "function-summaries" no_arg - ~doc:"Use function summaries (in development)" + ~doc:"use function summaries (in development)" in fun program () -> Control.exec_pgm {bound; skip_throw; function_summaries} (program ()) diff --git a/sledge/tools/gen_help.sh b/sledge/tools/gen_help.sh new file mode 100755 index 000000000..660e15650 --- /dev/null +++ b/sledge/tools/gen_help.sh @@ -0,0 +1,25 @@ +#!/bin/bash + +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +sledge=$(dirname $PWD)/install/$(basename $PWD)/bin/sledge + +line=$(\ + $sledge help -recursive -expand \ + | grep -n "== subcommands ===" \ + | cut -d : -f1,1) + +line=$(($line+1)) + +$sledge help -recursive + +$sledge h -r -e \ + | tail -n +$line \ + | sed -e "/^$/d;s/ \(.*\) .*/\1/g" \ + | while read cmd; do \ + printf "\n====== sledge $cmd ======\n\n"; \ + $sledge $cmd -help; \ + done diff --git a/sledge/tools/gen_version.sh b/sledge/tools/gen_version.sh index d8b61ad59..3229af41a 100755 --- a/sledge/tools/gen_version.sh +++ b/sledge/tools/gen_version.sh @@ -1,6 +1,5 @@ #!/bin/bash - # Copyright (c) Facebook, Inc. and its affiliates. # # This source code is licensed under the MIT license found in the