diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index ad2fc4345..36ef7a8ab 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -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: " write generated textual LLAIR to , 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:" write generated LLAIR to " + let%map_open output = + flag "output" (optional string) + ~doc:" write generated binary LLAIR to " 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 = diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 67eb9dfdc..4c09423c2 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -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 ] stop execution exploration at depth - [-colors] enable printing in colors - [-domain ] 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 ] write generated LLAIR to - [-margin ] wrap debug tracing at columns - [-modules ] write list of bitcode files to , or to standard - output if 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 ] write report sexp to , or to standard error if - "-" - [-stats] output performance statistics to stderr - [-trace ] enable debug tracing - [-help] print this help text and exit - (alias: -?) + [-append-report] append to report file + [-bound ] stop execution exploration at depth + [-colors] enable printing in colors + [-domain ] 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 ] wrap debug tracing at columns + [-modules ] write list of bitcode files to , or to standard + output if 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 ] write generated binary LLAIR to + [-preanalyze-globals] pre-analyze global variables used by each function + [-report ] write report sexp to , or to standard error if + "-" + [-stats] output performance statistics to stderr + [-trace ] 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 ] stop execution exploration at depth - [-colors] enable printing in colors - [-domain ] 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 ] write generated LLAIR to - [-margin ] wrap debug tracing at 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 ] write report sexp to , or to standard error if - "-" - [-stats] output performance statistics to stderr - [-trace ] enable debug tracing - [-help] print this help text and exit - (alias: -?) + [-append-report] append to report file + [-bound ] stop execution exploration at depth + [-colors] enable printing in colors + [-domain ] 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 ] wrap debug tracing at 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 ] write generated binary LLAIR to + [-preanalyze-globals] pre-analyze global variables used by each function + [-report ] write report sexp to , or to standard error if + "-" + [-stats] output performance statistics to stderr + [-trace ] 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 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 === + + [-append-report] append to report file + [-colors] enable printing in colors + [-fuzzer] add a harness for libFuzzer targets + [-margin ] wrap debug tracing at 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 ] write generated binary LLAIR to + [-report ] write report sexp to , or to standard error if "-" + [-trace ] 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 [ ...] + +The 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 ] write generated LLAIR to + [-llair-output ] write generated textual LLAIR to , or to + standard output if omitted [-margin ] wrap debug tracing at 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 ] write generated binary LLAIR to [-report ] write report sexp to , or to standard error if "-" [-trace ] enable debug tracing @@ -196,34 +222,6 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be (alias: -?) -====== sledge llvm disassemble ====== - -translate LLVM bitcode to LLAIR and print in textual form - - sledge llvm disassemble [ ...] - -The 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 ] write generated LLAIR to - [-llair-txt-output ] write generated textual LLAIR to , or to - standard output if omitted - [-margin ] wrap debug tracing at 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 ] write report sexp to , or to standard error - if "-" - [-trace ] enable debug tracing - [-help] print this help text and exit - (alias: -?) - - ====== sledge analyze ====== analyze LLAIR code @@ -263,16 +261,16 @@ The 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 ] write generated textual LLAIR to , or to - standard output if omitted - [-margin ] wrap debug tracing at columns - [-report ] write report sexp to , or to standard error - if "-" - [-trace ] enable debug tracing - [-help] print this help text and exit - (alias: -?) + [-append-report] append to report file + [-colors] enable printing in colors + [-llair-output ] write generated textual LLAIR to , or to + standard output if omitted + [-margin ] wrap debug tracing at columns + [-report ] write report sexp to , or to standard error if + "-" + [-trace ] enable debug tracing + [-help] print this help text and exit + (alias: -?) ====== sledge smt ====== diff --git a/sledge/test/Makefile b/sledge/test/Makefile index df5761209..e78c5fd36 100644 --- a/sledge/test/Makefile +++ b/sledge/test/Makefile @@ -45,14 +45,14 @@ default: test %.ll : %.bc @(cd $(@D) && llvm-dis -show-annotations -o $(@F) $(/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