[sledge] Handle whether to follow exceptional control flow at model compilation

Summary:
Currently there is a symbolic execution option to ignore exceptional
control flow. This hack does not fit well, and it is unclear how much
backend functionality should take it into consideration. This diff
removes this option and replaces it with an option during model
compilation. This has the advantage of clarifying and simplifying the
backend, with the disadvantage of no longer supporting switching
between exceptions and no-exceptions modes at analysis time. Since the
possibility of ignoring exceptional control flow is due to it not being
ready yet, this is a good trade to make.

Reviewed By: jvillard

Differential Revision: D25146148

fbshipit-source-id: 1f1299ee1

sledge/cli/sledge_cli.ml

@@ -83,7 +83,6 @@ let used_globals pgm preanalyze : Domain_used_globals.r =
     let summary_table =
       Used_globals_executor.compute_summaries
         { bound= 1
-        ; skip_throw= false
         ; function_summaries= true
         ; entry_points
         ; globals= Declared Llair.Global.Set.empty }
@@ -101,9 +100,6 @@ let analyze =
     flag "bound"
       (optional_with_default 1 int)
       ~doc:"<int> stop execution exploration at depth <int>"
-  and exceptions =
-    flag "exceptions" no_arg
-      ~doc:"explore executions that throw and handle exceptions"
   and function_summaries =
     flag "function-summaries" no_arg
       ~doc:"use function summaries (in development)"
@@ -131,10 +127,9 @@ let analyze =
   fun program () ->
     let pgm = program () in
     let globals = used_globals pgm preanalyze_globals in
-    let skip_throw = not exceptions in
     Domain_sh.simplify_states := not no_simplify_states ;
     Timer.enabled := stats ;
-    exec {bound; skip_throw; function_summaries; entry_points; globals} pgm ;
+    exec {bound; function_summaries; entry_points; globals} pgm ;
     Report.coverage pgm ;
     Report.safe_or_unsafe ()
 

sledge/model/cxxabi.cpp

@@ -6,19 +6,34 @@
  */
 
 #include "cxa_default_handlers.cpp"
-#include "cxa_exception.cpp"
 #include "cxa_exception_storage.cpp"
 #include "cxa_guard.cpp"
 #include "cxa_handlers.cpp"
 #include "llair_intrinsics.h"
+#ifdef EXCEPTIONS
+#include "cxa_exception.cpp"
+#endif
 
 extern "C" {
 
 void abort_message(const char* format, ...) { abort(); }
 
+#ifndef EXCEPTIONS
+
+__attribute__((noreturn)) void __llair_throw(void* thrown_exception) {
+  __llair_unreachable();
+}
+
+void* __cxa_allocate_exception(size_t thrown_size) throw() {
+  __llair_unreachable();
+}
+
+#else
+
 __attribute__((always_inline)) _Unwind_Reason_Code
 _Unwind_RaiseException(_Unwind_Exception* unwind_exception) {
   __llair_throw(thrown_object_from_cxa_exception(
       abi::cxa_exception_from_exception_unwind_exception(unwind_exception)));
 }
+#endif
 }

sledge/model/llair_intrinsics.h

@@ -11,17 +11,18 @@
 extern "C" {
 #endif
 
-__attribute__((noreturn)) void __llair_throw(void* thrown_exception);
-
-/* express assumption that an execution is not possible */
-__attribute__((noreturn)) void __llair_unreachable();
-
-/* allocation that cannot fail. */
+/* allocation that cannot fail */
 void* __llair_alloc(unsigned size);
 
 /* non-deterministic choice */
 int __llair_choice();
 
+/* throw an exception */
+__attribute__((noreturn)) void __llair_throw(void* thrown_exception);
+
+/* executions that call __llair_unreachable are assumed to be impossible */
+__attribute__((noreturn)) void __llair_unreachable();
+
 #ifdef __cplusplus
 }
 #endif

sledge/sledge-help.txt

@@ -53,7 +53,6 @@ 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
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -151,7 +150,6 @@ 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
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -238,7 +236,6 @@ 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
   [-no-simplify-states]  do not simplify states during symbolic execution

sledge/src/control.ml

@@ -11,7 +11,6 @@
 
 type exec_opts =
   { bound: int
-  ; skip_throw: bool
   ; function_summaries: bool
   ; entry_points: string list
   ; globals: Domain_used_globals.r }
@@ -446,9 +445,7 @@ module Make (Dom : Domain_intf.Dom) = struct
                   (Domain_used_globals.by_function opts.globals callee.name)
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
-    | Throw {exc} ->
-        if opts.skip_throw then Work.skip
-        else exec_throw stk state block exc
+    | Throw {exc} -> exec_throw stk state block exc
     | Unreachable -> Work.skip
 
   let exec_inst : Llair.inst -> Dom.t -> (Dom.t, Dom.t * Llair.inst) result

sledge/src/control.mli

@@ -9,7 +9,6 @@
 
 type exec_opts =
   { bound: int  (** Loop/recursion unrolling bound *)
-  ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
   ; entry_points: string list  (** C linkage names of entry points *)
   ; globals: Domain_used_globals.r }

sledge/src/domain_sh.ml

@@ -68,7 +68,7 @@ let exec_inst inst pre =
   | Intrinsic {reg; name; args; _} ->
       let areturn = Option.map ~f:X.reg reg in
       let actuals = IArray.map ~f:X.term args in
-      Exec.intrinsic ~skip_throw:true pre areturn name actuals )
+      Exec.intrinsic pre areturn name actuals )
   |> Option.map ~f:simplify
 
 let value_determined_by ctx us a =

sledge/src/exec.ml

@@ -734,7 +734,7 @@ let free pre ~ptr = exec_spec pre (free_spec ptr)
 let nondet pre = function Some reg -> kill pre reg | None -> pre
 let abort _ = None
 
-let intrinsic ~skip_throw :
+let intrinsic :
        Sh.t
     -> Var.t option
     -> Llair.Intrinsic.t
@@ -809,11 +809,6 @@ let intrinsic ~skip_throw :
    *)
   (* size_t strlen (const char* ptr) *)
   | Some reg, `strlen, [|ptr|] -> exec_spec pre (strlen_spec reg ptr)
-  (*
-   * cxxabi
-   *)
-  | Some _, `__cxa_allocate_exception, [|_|] when skip_throw ->
-      Some (Sh.false_ pre.us)
   (*
    * folly
    *)
@@ -827,7 +822,7 @@ let intrinsic ~skip_throw :
       | `posix_memalign | `realloc | `mallocx | `rallocx | `xallocx
       | `sallocx | `dallocx | `sdallocx | `nallocx | `malloc_usable_size
       | `mallctl | `mallctlnametomib | `mallctlbymib | `strlen
-      | `__cxa_allocate_exception | `_ZN5folly13usingJEMallocEv )
+      | `_ZN5folly13usingJEMallocEv )
     , _ ) ->
       fail "%aintrinsic %a%a;"
         (Option.pp "%a := " Var.pp)

sledge/src/exec.mli

@@ -20,9 +20,4 @@ val nondet : Sh.t -> Var.t option -> Sh.t
 val abort : Sh.t -> Sh.t option
 
 val intrinsic :
-     skip_throw:bool
-  -> Sh.t
-  -> Var.t option
-  -> Llair.Intrinsic.t
-  -> Term.t iarray
-  -> Sh.t option
+  Sh.t -> Var.t option -> Llair.Intrinsic.t -> Term.t iarray -> Sh.t option

sledge/src/llair/intrinsics.ml

@@ -33,8 +33,6 @@ type t =
   | `malloc_stats_print
   | (* cstring *)
     `strlen
-  | (* cxxabi *)
-    `__cxa_allocate_exception
   | (* folly *)
     `_ZN5folly13usingJEMallocEv ]
 [@@deriving compare, equal, hash, sexp, enumerate, variants]

sledge/src/llair/llair.ml

@@ -572,9 +572,14 @@ module BlockQ = HashQueue.Make (Block_label)
 module Func = struct
   type t = func [@@deriving compare, equal, hash, sexp_of]
 
-  let is_undefined = function
-    | {entry= {cmnd; term= Unreachable; _}; _} -> IArray.is_empty cmnd
-    | _ -> false
+  let undefined_entry =
+    Block.mk ~lbl:"undefined" ~cmnd:IArray.empty ~term:Term.unreachable
+
+  let mk_undefined ~name ~formals ~freturn ~fthrow ~loc =
+    let locals = Reg.Set.empty in
+    {name; formals; freturn; fthrow; locals; entry= undefined_entry; loc}
+
+  let is_undefined func = func.entry == undefined_entry
 
   let fold_cfg func s ~f =
     let seen = BlockS.create 0 in
@@ -672,13 +677,6 @@ module Func = struct
     resolve_parent_and_jumps entry ;
     IArray.iter cfg ~f:resolve_parent_and_jumps ;
     func |> check invariant
-
-  let mk_undefined ~name ~formals ~freturn ~fthrow =
-    let entry =
-      Block.mk ~lbl:"" ~cmnd:IArray.empty ~term:Term.unreachable
-    in
-    let cfg = IArray.empty in
-    mk ~name ~entry ~formals ~freturn ~fthrow ~cfg
 end
 
 (** Derived meta-data *)