pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[sledge] Improve the option and file naming of binary vs text llair output

Browse Source 
Summary:
Change `-llair-output` to `-output`, for binary form, and
`-llair-txt-output` to `-llair-output`, for textual form. Also
correspondingly change `.llair` to `.bllair`, for binary, and
`.llair.txt` to `.llair` for text.

This improves command line argument completion, and makes `.llair` the
extension of the files most commonly interacted with.

Reviewed By: ngorogiannis

Differential Revision: D24951506

fbshipit-source-id: ad4c73ca2
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent f02952c003
commit fe93dd754e
3 changed files with 101 additions and 103 deletions
Show Stats Download Patch File Download Diff File

14
sledge/cli/sledge_cli.ml
Unescape View File

@ -154,15 +154,15 @@ let analyze_cmd =
command ~summary ~readme param
let disassemble =
let%map_open llair_txt_output =
flag "llair-txt-output" (optional string)
let%map_open llair_output =
flag "llair-output" (optional string)
~doc:
"<file> write generated textual LLAIR to <file>, or to standard \
output if omitted"
in
fun program () ->
let pgm = program () in
( match llair_txt_output with
( match llair_output with
| None -> Format.printf "%a@." Llair.Program.pp pgm
| Some file ->
Out_channel.with_file file ~f:(fun oc ->
@ -182,9 +182,9 @@ let disassemble_cmd =
command ~summary ~readme param
let translate =
let%map_open llair_output =
flag "llair-output" (optional string)
~doc:"<file> write generated LLAIR to <file>"
let%map_open output =
flag "output" (optional string)
~doc:"<file> write generated binary LLAIR to <file>"
and no_models =
flag "no-models" no_arg
~doc:"do not add models for C/C++ runtime and standard libraries"
@ -201,7 +201,7 @@ let translate =
Frontend.translate ~models:(not no_models) ~fuzzer
~internalize:(not no_internalize) bitcode_inputs
in
Option.iter ~f:(marshal program) llair_output ;
Option.iter ~f:(marshal program) output ;
program
let llvm_grp =

172
sledge/sledge-help.txt
Unescape View File

@ -47,31 +47,31 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
=== flags ===
[-append-report] append to report file
[-bound <int>] stop execution exploration at depth <int>
[-colors] enable printing in colors
[-domain <string>] select abstract domain; must be one of "sh" (default,
symbolic heap domain), "globals" (used-globals
domain), or "unit" (unit domain)
[-exceptions] explore executions that throw and handle exceptions
[-function-summaries] use function summaries (in development)
[-fuzzer] add a harness for libFuzzer targets
[-llair-output <file>] write generated LLAIR to <file>
[-margin <cols>] wrap debug tracing at <cols> columns
[-modules <file>] write list of bitcode files to <file>, or to standard
output if <file> is `-`
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-no-simplify-states] do not simplify states during symbolic execution
[-preanalyze-globals] pre-analyze global variables used by each function
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-stats] output performance statistics to stderr
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
[-append-report] append to report file
[-bound <int>] stop execution exploration at depth <int>
[-colors] enable printing in colors
[-domain <string>] select abstract domain; must be one of "sh" (default,
symbolic heap domain), "globals" (used-globals domain),
or "unit" (unit domain)
[-exceptions] explore executions that throw and handle exceptions
[-function-summaries] use function summaries (in development)
[-fuzzer] add a harness for libFuzzer targets
[-margin <cols>] wrap debug tracing at <cols> columns
[-modules <file>] write list of bitcode files to <file>, or to standard
output if <file> is `-`
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-no-simplify-states] do not simplify states during symbolic execution
[-output <file>] write generated binary LLAIR to <file>
[-preanalyze-globals] pre-analyze global variables used by each function
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-stats] output performance statistics to stderr
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
====== sledge buck bitcode ======
@ -145,29 +145,29 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
=== flags ===
[-append-report] append to report file
[-bound <int>] stop execution exploration at depth <int>
[-colors] enable printing in colors
[-domain <string>] select abstract domain; must be one of "sh" (default,
symbolic heap domain), "globals" (used-globals
domain), or "unit" (unit domain)
[-exceptions] explore executions that throw and handle exceptions
[-function-summaries] use function summaries (in development)
[-fuzzer] add a harness for libFuzzer targets
[-llair-output <file>] write generated LLAIR to <file>
[-margin <cols>] wrap debug tracing at <cols> columns
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-no-simplify-states] do not simplify states during symbolic execution
[-preanalyze-globals] pre-analyze global variables used by each function
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-stats] output performance statistics to stderr
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
[-append-report] append to report file
[-bound <int>] stop execution exploration at depth <int>
[-colors] enable printing in colors
[-domain <string>] select abstract domain; must be one of "sh" (default,
symbolic heap domain), "globals" (used-globals domain),
or "unit" (unit domain)
[-exceptions] explore executions that throw and handle exceptions
[-function-summaries] use function summaries (in development)
[-fuzzer] add a harness for libFuzzer targets
[-margin <cols>] wrap debug tracing at <cols> columns
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-no-simplify-states] do not simplify states during symbolic execution
[-output <file>] write generated binary LLAIR to <file>
[-preanalyze-globals] pre-analyze global variables used by each function
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-stats] output performance statistics to stderr
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
====== sledge llvm translate ======
@ -178,17 +178,43 @@ translate LLVM bitcode to LLAIR
Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be either: an LLVM bitcode file, in binary (.bc) or textual (.ll) form; or of the form @<argsfile>, where <argsfile> names a file containing one <input> per line.
=== flags ===
[-append-report] append to report file
[-colors] enable printing in colors
[-fuzzer] add a harness for libFuzzer targets
[-margin <cols>] wrap debug tracing at <cols> columns
[-no-internalize] do not internalize all functions except the entry points
specified in the config file
[-no-models] do not add models for C/C++ runtime and standard libraries
[-output <file>] write generated binary LLAIR to <file>
[-report <file>] write report sexp to <file>, or to standard error if "-"
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
====== sledge llvm disassemble ======
translate LLVM bitcode to LLAIR and print in textual form
sledge llvm disassemble <input> [<input> ...]
The <input> file must be LLVM bitcode.
=== flags ===
[-append-report] append to report file
[-colors] enable printing in colors
[-fuzzer] add a harness for libFuzzer targets
[-llair-output <file>] write generated LLAIR to <file>
[-llair-output <file>] write generated textual LLAIR to <file>, or to
standard output if omitted
[-margin <cols>] wrap debug tracing at <cols> columns
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-output <file>] write generated binary LLAIR to <file>
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-trace <spec>] enable debug tracing
@ -196,34 +222,6 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
(alias: -?)
====== sledge llvm disassemble ======
translate LLVM bitcode to LLAIR and print in textual form
sledge llvm disassemble <input> [<input> ...]
The <input> file must be LLVM bitcode.
=== flags ===
[-append-report] append to report file
[-colors] enable printing in colors
[-fuzzer] add a harness for libFuzzer targets
[-llair-output <file>] write generated LLAIR to <file>
[-llair-txt-output <file>] write generated textual LLAIR to <file>, or to
standard output if omitted
[-margin <cols>] wrap debug tracing at <cols> columns
[-no-internalize] do not internalize all functions except the entry
points specified in the config file
[-no-models] do not add models for C/C++ runtime and standard
libraries
[-report <file>] write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
====== sledge analyze ======
analyze LLAIR code
@ -263,16 +261,16 @@ The <input> file must be LLAIR code, as produced by `sledge llvm translate`.
=== flags ===
[-append-report] append to report file
[-colors] enable printing in colors
[-llair-txt-output <file>] write generated textual LLAIR to <file>, or to
standard output if omitted
[-margin <cols>] wrap debug tracing at <cols> columns
[-report <file>] write report sexp to <file>, or to standard error
if "-"
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
[-append-report] append to report file
[-colors] enable printing in colors
[-llair-output <file>] write generated textual LLAIR to <file>, or to
standard output if omitted
[-margin <cols>] wrap debug tracing at <cols> columns
[-report <file>] write report sexp to <file>, or to standard error if
"-"
[-trace <spec>] enable debug tracing
[-help] print this help text and exit
(alias: -?)
====== sledge smt ======

18
sledge/test/Makefile
Unescape View File

@ -45,14 +45,14 @@ default: test
%.ll : %.bc
@(cd $(@D) && llvm-dis -show-annotations -o $(@F) $(<F))
%.llair : %.bc
$(SLEDGE_DBG) llvm translate $< -llair-output $@
%.bllair : %.bc
$(SLEDGE_DBG) llvm translate $< -output $@
%.llair.txt : %.bc
$(SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-txt-output $@
%.llair : %.bc
$(SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-output $@
%.llair.txt : %.ll
$(SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-txt-output $@
%.llair : %.ll
$(SLEDGE_DBG) llvm disassemble -no-models -no-internalize $< -llair-output $@
# code to test sledge translate
TranslateCs:=$(shell find -L {,local/}translate -name '*.c' 2>/dev/null)
@ -210,7 +210,7 @@ warnings:
@find -L * -name '*.out' | xargs grep -h "Warning:" | sort
test-translate:
-@find -L {,local/,extra/}translate -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.llair' -or -name '*.llair.txt' -delete 2>/dev/null
-@find -L {,local/,extra/}translate -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -or -name '*.llair' -delete 2>/dev/null
-@$(MAKE) --no-print-directory translate
@$(MAKE) --no-print-directory translate-status
@ -225,7 +225,7 @@ test-smt:
@$(MAKE) --no-print-directory smt-status
test-llvm:
-@find -L {,local/,extra/}llvm -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.llair' -delete 2>/dev/null
-@find -L {,local/,extra/}llvm -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -delete 2>/dev/null
-@$(MAKE) --no-print-directory llvm
@$(MAKE) --no-print-directory llvm-status
@ -253,7 +253,7 @@ cleanbc:
# remove result files
cleanout:
@find -L * -not -path 'baseline/*' -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.llair' -or -name '*.llair.txt' \
@find -L * -not -path 'baseline/*' -name "*.sexp" -or -name "*.out" -or -name '*.err' -or -name '*.bllair' -or -name '*.llair' \
| xargs rm -f
clean: cleanbc cleanout

Write Preview
Loading…
Cancel
Save