From c5136d1cdf945b9990376476bbd0881ee2f817ad Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 19 Sep 2023 14:28:13 +0300 Subject: [PATCH 1/4] Add tests for library function races via NULL --- .../regression/05-lval_ls/20-race-null-void.c | 54 ++++++++++++++++++ .../regression/05-lval_ls/21-race-null-type.c | 55 ++++++++++++++++++ .../05-lval_ls/22-race-null-void-deep.c | 56 +++++++++++++++++++ .../05-lval_ls/23-race-null-type-deep.c | 54 ++++++++++++++++++ 4 files changed, 219 insertions(+) create mode 100644 tests/regression/05-lval_ls/20-race-null-void.c create mode 100644 tests/regression/05-lval_ls/21-race-null-type.c create mode 100644 tests/regression/05-lval_ls/22-race-null-void-deep.c create mode 100644 tests/regression/05-lval_ls/23-race-null-type-deep.c diff --git a/tests/regression/05-lval_ls/20-race-null-void.c b/tests/regression/05-lval_ls/20-race-null-void.c new file mode 100644 index 0000000000..1950ada73e --- /dev/null +++ b/tests/regression/05-lval_ls/20-race-null-void.c @@ -0,0 +1,54 @@ +#include +#include + +void *t_fun(void *arg) { + void **top; + free(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + pthread_join(id, NULL); // NORACE + break; + case 1: + pthread_join(id, 0); // NORACE + break; + case 2: + pthread_join(id, zero); // NORACE + break; + case 3: + pthread_join(id, 1); // RACE + break; + case 4: + pthread_join(id, one); // RACE + break; + case 5: + pthread_join(id, r); // RACE + break; + case 6: + pthread_join(id, null); // NORACE + break; + case 7: + pthread_join(id, unknown); // RACE + break; + case 8: + pthread_join(id, top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/21-race-null-type.c b/tests/regression/05-lval_ls/21-race-null-type.c new file mode 100644 index 0000000000..6b5e6e42fd --- /dev/null +++ b/tests/regression/05-lval_ls/21-race-null-type.c @@ -0,0 +1,55 @@ +// PARAM: --enable ana.race.direct-arithmetic +#include +#include + +void *t_fun(void *arg) { + void *top; + time(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + time(NULL); // NORACE + break; + case 1: + time(0); // NORACE + break; + case 2: + time(zero); // NORACE + break; + case 3: + time(1); // RACE + break; + case 4: + time(one); // RACE + break; + case 5: + time(r); // RACE + break; + case 6: + time(null); // NORACE + break; + case 7: + time(unknown); // RACE + break; + case 8: + time(top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/22-race-null-void-deep.c b/tests/regression/05-lval_ls/22-race-null-void-deep.c new file mode 100644 index 0000000000..7e99f286b6 --- /dev/null +++ b/tests/regression/05-lval_ls/22-race-null-void-deep.c @@ -0,0 +1,56 @@ +#include +#include + +pthread_key_t key; + +void *t_fun(void *arg) { + void *top; + pthread_setspecific(key, top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + pthread_setspecific(key, NULL); // NORACE + break; + case 1: + pthread_setspecific(key, 0); // NORACE + break; + case 2: + pthread_setspecific(key, zero); // NORACE + break; + case 3: + pthread_setspecific(key, 1); // RACE + break; + case 4: + pthread_setspecific(key, one); // RACE + break; + case 5: + pthread_setspecific(key, r); // RACE + break; + case 6: + pthread_setspecific(key, null); // NORACE + break; + case 7: + pthread_setspecific(key, unknown); // RACE + break; + case 8: + pthread_setspecific(key, top); // RACE + break; + default: + break; + } + return 0; +} diff --git a/tests/regression/05-lval_ls/23-race-null-type-deep.c b/tests/regression/05-lval_ls/23-race-null-type-deep.c new file mode 100644 index 0000000000..6f29964d1e --- /dev/null +++ b/tests/regression/05-lval_ls/23-race-null-type-deep.c @@ -0,0 +1,54 @@ +#include +#include + +void *t_fun(void *arg) { + void *top; + fclose(top); // RACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + int r; // rand + int zero = 0; // IntDomain zero + void *null; + __goblint_assume(null == NULL); // AddressDomain NULL + int one = 1; // IntDomain one + void *unknown; + __goblint_assume(unknown != NULL); // AddressDomain unknown + void *top; + switch (r) { + case 0: + feof(NULL); // NORACE + break; + case 1: + feof(0); // NORACE + break; + case 2: + feof(zero); // NORACE + break; + case 3: + feof(1); // RACE + break; + case 4: + feof(one); // RACE + break; + case 5: + feof(r); // RACE + break; + case 6: + feof(null); // NORACE + break; + case 7: + feof(unknown); // RACE + break; + case 8: + feof(top); // RACE + break; + default: + break; + } + return 0; +} From 83978e953dbbf7d6a8c920d071b380bbd1441637 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 19 Sep 2023 17:22:41 +0300 Subject: [PATCH 2/4] Fix ReachableFrom not adding back unknown pointer Regression from f7b38a0. --- src/analyses/base.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 71e2661997..c225da2939 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1287,7 +1287,11 @@ struct | Address a -> let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe: TODO why? *) let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in - List.fold_left (AD.join) (AD.empty ()) addrs + let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in + if AD.may_be_unknown a then + AD.add UnknownPtr addrs' (* add unknown back *) + else + addrs' | _ -> AD.empty () end | Q.ReachableUkTypes e -> begin From c458db248993021a753772beead0754697f2f73a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 19 Sep 2023 17:44:44 +0300 Subject: [PATCH 3/4] Add Int cases to MayPointTo and ReachableFrom queries --- src/analyses/base.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c225da2939..4e7235de2b 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1270,6 +1270,7 @@ struct match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with | Address a -> a | Bot -> Queries.Result.bot q (* TODO: remove *) + | Int i -> AD.of_int i | _ -> Queries.Result.top q end | Q.EvalThread e -> begin @@ -1292,6 +1293,7 @@ struct AD.add UnknownPtr addrs' (* add unknown back *) else addrs' + | Int i -> AD.of_int i | _ -> AD.empty () end | Q.ReachableUkTypes e -> begin From 204594e695c92d106e6e9e628109228f20712339 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 19 Sep 2023 17:45:22 +0300 Subject: [PATCH 4/4] Fix ReachableFrom precision loss with int argument in 68-longjmp/41-poison-rec --- src/analyses/base.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4e7235de2b..0e6ad8f516 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1293,7 +1293,12 @@ struct AD.add UnknownPtr addrs' (* add unknown back *) else addrs' - | Int i -> AD.of_int i + | Int i -> + begin match Cilfacade.typeOf e with + | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *) + | _ + | exception Cilfacade.TypeOfError _ -> AD.empty () (* avoid unknown pointer result for non-pointer expression *) + end | _ -> AD.empty () end | Q.ReachableUkTypes e -> begin