[sledge] Do not explore exceptional control flow by default

Summary:
The frontend translation of exceptional control flow is untrusted
enough that it makes sense to disable it by default.

Reviewed By: bennostein

Differential Revision: D16061018

fbshipit-source-id: 65dca36ae

sledge/sledge-help.txt

@@ -50,6 +50,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-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>
@@ -61,7 +62,6 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-no-models]            do not add models for C/C++ runtime and standard
                           libraries
   [-preanalyze-globals]   pre-analyze global variables used by each function
-  [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
                           (alias: -?)
@@ -137,6 +137,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-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>
@@ -146,7 +147,6 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-no-models]            do not add models for C/C++ runtime and standard
                           libraries
   [-preanalyze-globals]   pre-analyze global variables used by each function
-  [-skip-throw]           do not explore past throwing an exception
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
                           (alias: -?)
@@ -190,10 +190,10 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-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)
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-preanalyze-globals]  pre-analyze global variables used by each function
-  [-skip-throw]          do not explore past throwing an exception
   [-trace <spec>]        enable debug tracing
   [-help]                print this help text and exit
                          (alias: -?)

sledge/src/sledge.ml

@@ -90,9 +90,9 @@ let analyze =
     flag "bound"
       (optional_with_default 1 int)
       ~doc:"<int> stop execution exploration at depth <int>"
-  and skip_throw =
+  and exceptions =
-    flag "skip-throw" no_arg
+    flag "exceptions" no_arg
-      ~doc:"do not explore past throwing an exception"
+      ~doc:"explore executions that throw and handle exceptions"
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"
@@ -114,6 +114,7 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
+    let skip_throw = not exceptions in
     exec {bound; skip_throw; function_summaries; globals} pgm
 
 let analyze_cmd =