From b8065e9b62b1c39a96448b69daca49d1d9b261b9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 1 Jul 2019 07:16:40 -0700 Subject: [PATCH] [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 | 2 +- sledge/src/symbheap/domain.ml | 6 ++++-- sledge/src/symbheap/domain.mli | 7 ++++++- sledge/src/symbheap/exec.ml | 7 ++++++- sledge/src/symbheap/exec.mli | 7 ++++++- sledge/src/symbheap/state_domain.mli | 7 ++++++- 6 files changed, 29 insertions(+), 7 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index d0475ea1b..845c01892 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index f0bb550bd..0c11ff88b 100644 --- a/sledge/src/symbheap/domain.ml +++ b/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) diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index 9fc792548..24f021e75 100644 --- a/sledge/src/symbheap/domain.mli +++ b/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] diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 7ea7650ca..4a7f77bd0 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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 diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli index 715777120..2bedae2a1 100644 --- a/sledge/src/symbheap/exec.mli +++ b/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 diff --git a/sledge/src/symbheap/state_domain.mli b/sledge/src/symbheap/state_domain.mli index 9517221e7..faf79c4f1 100644 --- a/sledge/src/symbheap/state_domain.mli +++ b/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]