Summary:
This diff lifts the `PulseAbductiveDomain.t` in `PulseExecutionState` by tracking whether the program continues the analysis normally or exits unusually (e.g. by calling `exit` or `throw`):
```
type exec_state =
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
| ExitProgram of PulseAbductiveDomain.t
(** represents the state originating at exit/divergence. *)
```
Now, Pulse's actual domain is tracked by `PulseExecutionState` and as soon as we try to analyze an instruction at `ExitProgram`, we simply return its state.
The aim is to recover the state at the time of the exit, rather than simply ignoring them (i.e. returning empty disjuncts). This allows us to get rid of some FNs that we were not able to detect before. Moreover, it also allows the impurity analysis to be more precise since we will know how the state changed up to exit.
TODO:
- Impurity analysis needs to be improved to consider functions that simply exit as impure.
- The next goal is to handle error state similarly so that when pulse finds an error, we recover the state at the error location (and potentially continue to analyze?).
Disclaimer: currently, we handle throw statements like exit (as was the case before). However, this is not correct. Ideally, control flow from throw nodes follows catch nodes rather than exiting the program entirely.
Reviewed By: jvillard
Differential Revision: D20791747
fbshipit-source-id: df9e5445a
master
Ezgi Çiçek
5 years ago
committed by
Facebook GitHub Bot
parent
f0afa18cbf
commit
5a2b285fff
File diff suppressed because it is too large
Load Diff
@ -0,0 +1,43 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
open! IStd
|
||||
module F = Format
|
||||
|
||||
type exec_state =
|
||||
| ContinueProgram of PulseAbductiveDomain.t
|
||||
| ExitProgram of PulseAbductiveDomain.t
|
||||
|
||||
type t = exec_state
|
||||
|
||||
let continue astate = ContinueProgram astate
|
||||
|
||||
let mk_initial pdesc = ContinueProgram (PulseAbductiveDomain.mk_initial pdesc)
|
||||
|
||||
let leq ~lhs ~rhs =
|
||||
match (lhs, rhs) with
|
||||
| ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 ->
|
||||
PulseAbductiveDomain.leq ~lhs:astate1 ~rhs:astate2
|
||||
| ExitProgram _, ContinueProgram _ | ContinueProgram _, ExitProgram _ ->
|
||||
false
|
||||
|
||||
|
||||
let pp fmt = function
|
||||
| ContinueProgram astate ->
|
||||
PulseAbductiveDomain.pp fmt astate
|
||||
| ExitProgram astate ->
|
||||
F.fprintf fmt "{ExitProgram %a}" PulseAbductiveDomain.pp astate
|
||||
|
||||
|
||||
let map ~f exec_state =
|
||||
match exec_state with
|
||||
| ContinueProgram astate ->
|
||||
ContinueProgram (f astate)
|
||||
| ExitProgram astate ->
|
||||
ExitProgram (f astate)
|
||||
|
||||
|
||||
let of_post pdesc = map ~f:(PulseAbductiveDomain.of_post pdesc)
|
||||
@ -0,0 +1,20 @@
|
||||
(*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
open! IStd
|
||||
|
||||
type exec_state =
|
||||
| ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *)
|
||||
| ExitProgram of PulseAbductiveDomain.t
|
||||
(** represents the state originating at exit/divergence. *)
|
||||
|
||||
include AbstractDomain.NoJoin with type t = exec_state
|
||||
|
||||
val continue : PulseAbductiveDomain.t -> t
|
||||
|
||||
val of_post : Procdesc.t -> t -> t
|
||||
|
||||
val mk_initial : Procdesc.t -> t
|
||||
@ -0,0 +1,20 @@
|
||||
/*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
#include <stdlib.h>
|
||||
|
||||
int x;
|
||||
|
||||
void exit_positive_impure_FN(int a[10], int b) {
|
||||
if (b > 0) {
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
|
||||
void unreachable_impure_FN(int a[10], int b) {
|
||||
exit_positive_impure_FN(a, 10);
|
||||
x = 9;
|
||||
}
|
||||
@ -0,0 +1,29 @@
|
||||
/*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
#include <stdlib.h>
|
||||
|
||||
// we get two disjuncts one for each branch
|
||||
void exit_positive(int a[10], int b) {
|
||||
if (b < 1) {
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
|
||||
void unreachable_double_free_ok(int a[10], int b) {
|
||||
exit_positive(a, 0);
|
||||
free(a);
|
||||
free(a);
|
||||
}
|
||||
|
||||
void store_exit(int* x, bool b) {
|
||||
if (b) {
|
||||
*x = 42;
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
|
||||
void store_exit_null_bad(bool b) { store_exit(NULL, b); }
|
||||
@ -0,0 +1,35 @@
|
||||
/*
|
||||
* Copyright (c) Facebook, Inc. and its affiliates.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
#include <stdlib.h>
|
||||
|
||||
int double_free_in_catch_bad_FN(int a[10], int b) {
|
||||
try {
|
||||
if (b > 0) {
|
||||
free(a);
|
||||
throw(0);
|
||||
}
|
||||
} catch (...) {
|
||||
free(a);
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
void throw_positive(int a[10], int b) {
|
||||
if (b > 0) {
|
||||
free(a);
|
||||
throw(1);
|
||||
}
|
||||
}
|
||||
|
||||
int double_free_interproc_bad_FN(int a[10], int b) {
|
||||
try {
|
||||
throw_positive(a, 2);
|
||||
} catch (...) {
|
||||
free(a);
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
Loading…
Reference in new issue