From 2726079a63188e10a741c6d6402efc2346cf2972 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 2 Dec 2020 13:48:56 -0800 Subject: [PATCH] [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 | 7 +------ sledge/model/cxxabi.cpp | 17 ++++++++++++++++- sledge/model/llair_intrinsics.h | 13 +++++++------ sledge/sledge-help.txt | 3 --- sledge/src/control.ml | 5 +---- sledge/src/control.mli | 1 - sledge/src/domain_sh.ml | 2 +- sledge/src/exec.ml | 9 ++------- sledge/src/exec.mli | 7 +------ sledge/src/llair/intrinsics.ml | 2 -- sledge/src/llair/llair.ml | 18 ++++++++---------- 11 files changed, 37 insertions(+), 47 deletions(-) diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index d920af30a..789d1b819 100644 --- a/sledge/cli/sledge_cli.ml +++ b/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:" stop execution exploration at depth " - 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 () diff --git a/sledge/model/cxxabi.cpp b/sledge/model/cxxabi.cpp index e094848df..819e490a9 100644 --- a/sledge/model/cxxabi.cpp +++ b/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 } diff --git a/sledge/model/llair_intrinsics.h b/sledge/model/llair_intrinsics.h index 81ca43882..3f74125a9 100644 --- a/sledge/model/llair_intrinsics.h +++ b/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 diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 4c09423c2..860d1685a 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -53,7 +53,6 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s [-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 @@ -151,7 +150,6 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo [-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 @@ -238,7 +236,6 @@ The file must be binary LLAIR, such as produced by `sledge translate`. [-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) [-margin ] wrap debug tracing at columns [-no-simplify-states] do not simplify states during symbolic execution diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 802150538..6f9b98665 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/control.mli b/sledge/src/control.mli index d97d08aef..cf8619fd1 100644 --- a/sledge/src/control.mli +++ b/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 } diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 7176a37f8..4a59975a2 100644 --- a/sledge/src/domain_sh.ml +++ b/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 = diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index 57f98fbf3..2811e7165 100644 --- a/sledge/src/exec.ml +++ b/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) diff --git a/sledge/src/exec.mli b/sledge/src/exec.mli index 90d2935bd..3f9235d08 100644 --- a/sledge/src/exec.mli +++ b/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 diff --git a/sledge/src/llair/intrinsics.ml b/sledge/src/llair/intrinsics.ml index 15aaf257b..4eef1da58 100644 --- a/sledge/src/llair/intrinsics.ml +++ b/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] diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index a1f252777..168d28a4d 100644 --- a/sledge/src/llair/llair.ml +++ b/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 *)