From f606f5df1bb0b963d2f1b3a08fa09aafa2653b48 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 9 Aug 2024 19:20:52 +0200 Subject: [PATCH 1/3] Make `update_offset` idempotent for blobs --- src/cdomain/value/cdomains/valueDomain.ml | 43 ++++++++++--------- tests/regression/13-privatized/95-mm-calloc.c | 28 ++++++++++++ 2 files changed, 51 insertions(+), 20 deletions(-) create mode 100644 tests/regression/13-privatized/95-mm-calloc.c diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index b126d712bf..2f841568f7 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -1003,26 +1003,29 @@ struct end | Blob (x,s,zeroinit), _ -> begin - let l', o' = shift_one_over l o in - let x = zero_init_calloced_memory zeroinit x t in - (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *) - let do_strong_update = - begin match v with - | (Var var, _) -> - let blob_size_opt = ID.to_int s in - not @@ ask.is_multiple var - && GobOption.exists (fun blob_size -> (* Size of blob is known *) - (not @@ Cil.isVoidType t (* Size of value is known *) - && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t)) - || blob_destructive - ) blob_size_opt - | _ -> false - end - in - if do_strong_update then - Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit) - else - mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit)) + match offs, value with + | `NoOffset, Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2,ZeroInit.join zeroinit zeroinit2)) + | _ -> + let l', o' = shift_one_over l o in + let x = zero_init_calloced_memory zeroinit x t in + (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *) + let do_strong_update = + begin match v with + | (Var var, _) -> + let blob_size_opt = ID.to_int s in + not @@ ask.is_multiple var + && GobOption.exists (fun blob_size -> (* Size of blob is known *) + (not @@ Cil.isVoidType t (* Size of value is known *) + && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t)) + || blob_destructive + ) blob_size_opt + | _ -> false + end + in + if do_strong_update then + Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit) + else + mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit)) end | Thread _, _ -> (* hack for pthread_t variables *) diff --git a/tests/regression/13-privatized/95-mm-calloc.c b/tests/regression/13-privatized/95-mm-calloc.c new file mode 100644 index 0000000000..60a88379fc --- /dev/null +++ b/tests/regression/13-privatized/95-mm-calloc.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.base.privatization mutex-meet +#include +#include +#include +struct a { + void (*b)(); +}; + +int g = 0; + +struct a* t; +void m() { + // Reachable! + g = 1; +} + +void* j(void* arg) {}; + +void main() { + pthread_t tid; + pthread_create(&tid, 0, j, NULL); + t = calloc(1, sizeof(struct a)); + t->b = &m; + struct a r = *t; + r.b(); + + __goblint_check(g ==0); //UNKNOWN! +} From 250d660b8e4c975b1c04cd1fa6203f64b6f87d1a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 30 Dec 2024 17:33:11 +0100 Subject: [PATCH 2/3] Copy `zeroinit` from left arg Co-authored-by: Simmo Saan --- src/cdomain/value/cdomains/valueDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 2f841568f7..03273d3911 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -1004,7 +1004,7 @@ struct | Blob (x,s,zeroinit), _ -> begin match offs, value with - | `NoOffset, Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2,ZeroInit.join zeroinit zeroinit2)) + | `NoOffset, Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2, zeroinit)) | _ -> let l', o' = shift_one_over l o in let x = zero_init_calloced_memory zeroinit x t in From f85f8a335c7d3c324355c8418423ac662244bcb1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 30 Dec 2024 17:37:42 +0100 Subject: [PATCH 3/3] Make control-flow more transparent --- src/cdomain/value/cdomains/valueDomain.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 03273d3911..615cf58e1a 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -1001,10 +1001,10 @@ struct else mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit)) end - | Blob (x,s,zeroinit), _ -> + | Blob (x,s,zeroinit), `NoOffset -> (* `NoOffset is only remaining possibility for Blob here *) begin - match offs, value with - | `NoOffset, Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2, zeroinit)) + match value with + | Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2, zeroinit)) | _ -> let l', o' = shift_one_over l o in let x = zero_init_calloced_memory zeroinit x t in