From 3485100b77209734c346fc063a7f3fdff59cf8e8 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 Nov 2023 20:11:49 +0200 Subject: [PATCH 1/4] Add test for special function lval --- tests/regression/00-sanity/51-base-special-lval.c | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 tests/regression/00-sanity/51-base-special-lval.c diff --git a/tests/regression/00-sanity/51-base-special-lval.c b/tests/regression/00-sanity/51-base-special-lval.c new file mode 100644 index 0000000000..8f74a1babe --- /dev/null +++ b/tests/regression/00-sanity/51-base-special-lval.c @@ -0,0 +1,13 @@ +// Making sure special function lval is not invalidated recursively +#include + +extern int * anIntPlease(); +int main() { + int x = 0; + int *p = &x; + p = anIntPlease(); + + __goblint_check(x == 0); + + return 0; +} From 60923ea18f414a2d609497f2f1f03b136d9bb3d0 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 Nov 2023 20:15:31 +0200 Subject: [PATCH 2/4] Special function lval not invalidated recursively --- src/analyses/base.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 84be8c7a19..8b6350aa2d 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2123,7 +2123,7 @@ struct let invalidate_ret_lv st = match lv with | Some lv -> if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s\n" d_plainlval lv f.vname; - invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv] + invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv] | None -> st in let addr_type_of_exp exp = @@ -2328,7 +2328,7 @@ struct | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in - let apply_abs ik x = +let apply_abs ik x = let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in begin match eval_x with | Int int_x -> From 895bd9fe468a064016f5c130f9f38174f4949369 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 Nov 2023 20:35:29 +0200 Subject: [PATCH 3/4] Update cram tests --- tests/regression/04-mutex/49-type-invariants.t | 4 ---- tests/regression/04-mutex/77-type-nested-fields.t | 4 ---- tests/regression/04-mutex/79-type-nested-fields-deep1.t | 4 ---- tests/regression/04-mutex/80-type-nested-fields-deep2.t | 4 ---- tests/regression/04-mutex/90-distribute-fields-type-1.t | 4 ---- tests/regression/04-mutex/91-distribute-fields-type-2.t | 4 ---- tests/regression/04-mutex/92-distribute-fields-type-deep.t | 4 ---- tests/regression/04-mutex/93-distribute-fields-type-global.t | 2 -- 8 files changed, 30 deletions(-) diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index 4c105d1559..4b8118eec1 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -14,8 +14,6 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) @@ -39,8 +37,6 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index bb935cb0ed..68d9cdb779 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -15,11 +15,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:31:3-31:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:31:3-31:20) [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:38:3-38:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:38:3-38:22) [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22) [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20) diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index ba1399d225..85f7bfb709 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -15,11 +15,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:36:3-36:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:36:3-36:20) [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:43:3-43:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:43:3-43:24) [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24) [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20) diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index 71bdcfb2e2..a2e9e2ab15 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -15,11 +15,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:36:3-36:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:36:3-36:22) [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22) - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:43:3-43:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:43:3-43:24) [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24) [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22) diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index 46435045b9..a3b5faf083 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -17,11 +17,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:31:3-31:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:31:3-31:20) [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:39:3-39:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:39:3-39:17) [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17) [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20) diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index c7e66c0527..5773245114 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -17,11 +17,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:32:3-32:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:32:3-32:17) [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:40:3-40:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:40:3-40:17) [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17) [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17) diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index 4fc1c7e101..798374d63c 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -17,11 +17,7 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:36:3-36:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:36:3-36:20) [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:44:3-44:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20) [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20) diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index bf34d99936..07999854ff 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -16,8 +16,6 @@ live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:13:3-13:29) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:13:3-13:29) [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29) [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29) [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) From cb06f70f99b5c149e4afcb1ba6dcae53beb80cd2 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 22 Nov 2023 11:31:03 +0200 Subject: [PATCH 4/4] Fix indentation --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 8b6350aa2d..98badad489 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2328,7 +2328,7 @@ struct | _ -> failwith ("non-floating-point argument in call to function "^f.vname) end in -let apply_abs ik x = + let apply_abs ik x = let eval_x = eval_rv (Analyses.ask_of_ctx ctx) gs st x in begin match eval_x with | Int int_x ->