[sledge] Model __cxa_allocate_exception as unreachable with -skip-throw

Summary:
Each call to __cxa_allocate_exception, in practice, is shortly
followed by raising an exception. With -skip-throw, execution will not
proceed past the throw. Since the concrete implementation of
__cxa_allocate_exception and the following initialization of the
exception object is very low-level code that plays tricks, the
analyzer has trouble with it. So model __cxa_allocate_exception as
unreachable to avoid (needlessly) executing that code and potentially
failing spuriously.

Reviewed By: kren1

Differential Revision: D16069451

fbshipit-source-id: bea1dae09

sledge/src/control.ml

@@ -400,7 +400,7 @@ let exec_term :
     | callees ->
         List.fold callees ~init:Work.skip ~f:(fun x callee ->
             ( match
-                Domain.exec_intrinsic state
+                Domain.exec_intrinsic ~skip_throw:opts.skip_throw state
                   (List.hd return.dst.params)
                   callee.name.var args
               with

sledge/src/symbheap/domain.ml

@@ -37,8 +37,10 @@ let exec_inst (entry, current) inst =
 let exec_return (entry, current) formal actual =
   (entry, State_domain.exec_return current formal actual)
 
-let exec_intrinsic (entry, current) result intrinsic actuals =
-  match State_domain.exec_intrinsic current result intrinsic actuals with
+let exec_intrinsic ~skip_throw (entry, current) result intrinsic actuals =
+  match
+    State_domain.exec_intrinsic ~skip_throw current result intrinsic actuals
+  with
   | None -> None
   | Some (Ok current) -> Some (Ok (entry, current))
   | Some (Error e) -> Some (Error e)

sledge/src/symbheap/domain.mli

@@ -19,7 +19,12 @@ val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
-  t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
+     skip_throw:bool
+  -> t
+  -> Var.t option
+  -> Var.t
+  -> Exp.t list
+  -> (t, unit) result option
 
 type from_call [@@deriving sexp_of]
 

sledge/src/symbheap/exec.ml

@@ -620,7 +620,7 @@ let inst : Sh.t -> Llair.inst -> (Sh.t, unit) result =
 
 let skip : Sh.t -> (Sh.t, _) result option = fun pre -> Some (Ok pre)
 
-let intrinsic :
+let intrinsic ~skip_throw :
        Sh.t
     -> Var.t option
     -> Var.t
@@ -697,4 +697,9 @@ let intrinsic :
   (* size_t strlen (const char* ptr) *)
   | Some reg, "strlen", [ptr] ->
       Some (exec_spec pre (strlen_spec us reg ptr))
+  (*
+   * cxxabi
+   *)
+  | Some _, "__cxa_allocate_exception", [_] when skip_throw ->
+      skip (Sh.false_ pre.us)
   | _ -> None

sledge/src/symbheap/exec.mli

@@ -12,4 +12,9 @@ val return : Sh.t -> Var.t -> Exp.t -> Sh.t
 val inst : Sh.t -> Llair.inst -> (Sh.t, unit) result
 
 val intrinsic :
-  Sh.t -> Var.t option -> Var.t -> Exp.t list -> (Sh.t, unit) result option
+     skip_throw:bool
+  -> Sh.t
+  -> Var.t option
+  -> Var.t
+  -> Exp.t list
+  -> (Sh.t, unit) result option

sledge/src/symbheap/state_domain.mli

@@ -18,7 +18,12 @@ val exec_inst : t -> Llair.inst -> (t, unit) result
 val exec_return : t -> Var.t -> Exp.t -> t
 
 val exec_intrinsic :
-  t -> Var.t option -> Var.t -> Exp.t list -> (t, unit) result option
+     skip_throw:bool
+  -> t
+  -> Var.t option
+  -> Var.t
+  -> Exp.t list
+  -> (t, unit) result option
 
 type from_call [@@deriving compare, equal, sexp]