From 83e413cc83063a9a91d68e485835477bfde37ad7 Mon Sep 17 00:00:00 2001 From: Tomas Dacik Date: Wed, 4 May 2022 14:55:29 +0200 Subject: [PATCH 01/21] malloc uniqueness analysis --- src/analyses/mallocWrapperAnalysis.ml | 118 +++++++++++++----- src/util/options.schema.json | 6 + .../11-heap/03-threads_malloc_no_race.c | 35 ++++++ .../11-heap/04-malloc_unique_addresses.c | 27 ++++ .../11-heap/05-malloc_not_unique_address.c | 23 ++++ .../06-wrapper_plus_unique_addresses.c | 34 +++++ 6 files changed, 215 insertions(+), 28 deletions(-) create mode 100644 tests/regression/11-heap/03-threads_malloc_no_race.c create mode 100644 tests/regression/11-heap/04-malloc_unique_addresses.c create mode 100644 tests/regression/11-heap/05-malloc_not_unique_address.c create mode 100644 tests/regression/11-heap/06-wrapper_plus_unique_addresses.c diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index cde2fe265c..096ef98273 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -3,8 +3,9 @@ open Prelude.Ana open Analyses open GobConfig +open ThreadIdDomain -module Spec : Analyses.MCPSpec = +module Spec () : Analyses.MCPSpec = struct include Analyses.DefaultSpec @@ -13,23 +14,62 @@ struct let bot_name = "Unreachable node" end) - module Node = struct - include Node + module Chain = Lattice.Chain (struct + let n = + let p = get_int "ana.malloc.unique_address_count" in + if p < 0 then + failwith "Option ana.malloc.unique_address_count has to be non-negative" + else p + 1 (* Unique addresses + top address *) + + let names x = if Int.equal x (n - 1) then "top" else Format.asprintf "%d" x + + end) + + (* Map for counting malloc node visits up to n. *) + module MallocCounter = struct + include MapDomain.MapBot_LiftTop(PL)(Chain) + + (* Increase counter for given node. If it does not exists yet, create it. *) + let add_malloc counter node = + let malloc = `Lifted node in + let count = find malloc counter in + if Chain.is_top count then + counter + else + remove malloc counter + |> add malloc (count + 1) + end + + module Domain = struct + include Lattice.Prod (MallocCounter) (PL) + + let join (counter1, node1) (counter2, node2) = + (MallocCounter.join counter1 counter2, node1) + + let has_wrapper_node (_, wrapper_node) = not @@ PL.is_top wrapper_node + + let get_count (counter, _) node = MallocCounter.find (`Lifted node) counter + + end + + module ThreadNode = + struct + include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain) + (* Description that gets appended to the varinfo-name in user ouptut. *) - let describe_varinfo (v: varinfo) node = + let describe_varinfo (v: varinfo) (t, node, c) = let loc = UpdateCil.getLoc node in CilType.Location.show loc - let name_varinfo node = match node with - | Node.Statement s -> "(alloc@sid:" ^ (string_of_int s.sid) ^ ")" - | _ -> failwith "A function entry or return node can not be the node after a malloc" + let name_varinfo (t, node, c) = + Format.asprintf "(allocs@%s@%s(#%s))" (ThreadLifted.show t) (Node.show node) (Chain.show c) + end - module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(Node) + module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode) let name () = "mallocWrapper" - module D = PL - module G = BoolDomain.MayBool - module C = D + module D = Domain + module C = Domain module Q = Queries @@ -49,45 +89,64 @@ struct ctx.local let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - let calleeofinterest = Hashtbl.mem wrappers f.svar.vname in - let calleectx = if calleeofinterest then - if ctx.local = `Top then - `Lifted ctx.node (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) - else ctx.local (* if an interesting callee is called by an interesting caller, then we remember the caller context *) - else D.top () in (* if an uninteresting callee is called, then we forget what was called before *) - [(ctx.local, calleectx)] + let counter, wrapper_node = ctx.local in + let new_counter = + if Hashtbl.mem wrappers f.svar.vname then + MallocCounter.add_malloc counter ctx.prev_node + else counter + in + let new_wrapper_node = + if Hashtbl.mem wrappers f.svar.vname then + if not @@ D.has_wrapper_node ctx.local then + (`Lifted ctx.prev_node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) + else wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *) + else PL.top () (* if an uninteresting callee is called, then we forget what was called before *) + in + let caller_ctx = (new_counter, wrapper_node) in + let callee_ctx = (new_counter, new_wrapper_node) in + [(caller_ctx, callee_ctx)] let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = - ctx.local + D.join ctx.local au - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - ctx.local + let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = + let counter, wrapper_node = ctx.local in + match LibraryFunctions.classify f.vname arglist with + | `Malloc _ | `Calloc _ | `Realloc _ -> (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node) + | _ -> ctx.local let startstate v = D.bot () - let threadenter ctx lval f args = [D.top ()] + let threadenter ctx lval f args = [D.bot ()] let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () type marshal = NodeVarinfoMap.marshal let get_heap_var = NodeVarinfoMap.to_varinfo + + let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result = + let _, wrapper_node = ctx.local in match q with | Q.HeapVar -> - let node = match ctx.local with - | `Lifted vinfo -> vinfo - | _ -> ctx.node + let node = match wrapper_node with + | `Lifted wrapper_node -> wrapper_node + | _ -> ctx.prev_node in - let var = get_heap_var node in + let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, D.get_count ctx.local node) in var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *) `Lifted var | Q.IsHeapVar v -> NodeVarinfoMap.mem_varinfo v | Q.IsMultiple v -> - NodeVarinfoMap.mem_varinfo v + begin match NodeVarinfoMap.from_varinfo v with + | Some (_, _, c) -> Chain.is_top c || not (ctx.ask Q.MustBeUniqueThread) + | None -> false + end | _ -> Queries.Result.top q let init marshal = + Printexc.record_backtrace true; List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "ana.malloc.wrappers"); NodeVarinfoMap.unmarshal marshal @@ -95,5 +154,8 @@ struct NodeVarinfoMap.marshal () end +let after_config () = + MCP.register_analysis (module Spec ()) + let _ = - MCP.register_analysis (module Spec : MCPSpec) + AfterConfig.register after_config diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 668857c705..e712e1b626 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -724,6 +724,12 @@ "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca", "kzalloc" ] + }, + unique_address_count: { + "title": "ana.malloc.unique_address_count", + "description": "Number of unique memory addresses allocated for each malloc node.", + "type": "integer", + "default": 0 } }, "additionalProperties": false diff --git a/tests/regression/11-heap/03-threads_malloc_no_race.c b/tests/regression/11-heap/03-threads_malloc_no_race.c new file mode 100644 index 0000000000..2750cb640b --- /dev/null +++ b/tests/regression/11-heap/03-threads_malloc_no_race.c @@ -0,0 +1,35 @@ +// No race should be reported because thread1 and thread2 are both unique +// and work with their own allocated memory + +#include +#include + +int *f() +{ + int *x = malloc(sizeof(int)); + return x; +} + +void *thread1(void *v) +{ + int *x = f(); + (*x)++; // NORACE +} + +void *thread2(void *v) +{ + int *x = f(); + (*x)++; // NORACE +} + +int main(int argc, char **argv) +{ + pthread_t tid1; + pthread_t tid2; + + pthread_create(&tid1, NULL, thread1, NULL); + pthread_create(&tid2, NULL, thread2, NULL); + + pthread_join(tid1, NULL); + pthread_join(tid2, NULL); +} diff --git a/tests/regression/11-heap/04-malloc_unique_addresses.c b/tests/regression/11-heap/04-malloc_unique_addresses.c new file mode 100644 index 0000000000..7252763a39 --- /dev/null +++ b/tests/regression/11-heap/04-malloc_unique_addresses.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.malloc.unique_address_count 2 + +// Copied from 29/07. Here, unique addresses are allocated for both x and y. +// Therefore, it is not necessary to specify wrapper function. + +#include +#include + +void* myalloc(size_t s) { + return malloc(s); +} + +int main() { + int* x = myalloc(sizeof(int)); + int* y = myalloc(sizeof(int)); + int *p; + + *x = 0; + *y = 1; + + assert(*x == 0); + assert(*y == 1); + + p = x; x = y; y = p; + assert(*x == 1); + assert(*y == 0); +} diff --git a/tests/regression/11-heap/05-malloc_not_unique_address.c b/tests/regression/11-heap/05-malloc_not_unique_address.c new file mode 100644 index 0000000000..88877c3835 --- /dev/null +++ b/tests/regression/11-heap/05-malloc_not_unique_address.c @@ -0,0 +1,23 @@ +// PARAM: --set ana.malloc.unique_address_count 1 + +// Copied from 11/05. Here, malloc will allocate an unique address for x only. + +#include +#include + +void* myalloc(size_t s) { + return malloc(s); +} + +int main() { + int* x = myalloc(sizeof(int)); + int* y = myalloc(sizeof(int)); + int* z = myalloc(sizeof(int)); + + *x = 0; + *y = 1; + *z = 0; + + assert(*x == 0); + assert(*y == 1); // UNKNOWN! +} diff --git a/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c b/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c new file mode 100644 index 0000000000..f96dd1b9da --- /dev/null +++ b/tests/regression/11-heap/06-wrapper_plus_unique_addresses.c @@ -0,0 +1,34 @@ +// PARAM: --set ana.malloc.wrappers "['myalloc2']" --set ana.malloc.unique_address_count 2 + + +// Copied from 02/21. Here, only the inner wrapper function is specified. This should tests +// the combination of uniqueness analysis and malloc wrapper analysis. + +#include +#include + +void *myalloc(size_t n) { + return malloc(n); +} + +void *myalloc2(size_t n) { + return myalloc(n); +} + +int main() { + int *x = myalloc2(sizeof(int)); + int *y = myalloc2(sizeof(int)); + int *p; + + *x = 0; + *y = 1; + + assert(*x == 0); + assert(*y == 1); + + p = x; x = y; y = p; + assert(*x == 1); + assert(*y == 0); + + return 0; +} From 8e688735a50e4b29f7c20c479fe772333d60704f Mon Sep 17 00:00:00 2001 From: Tomas Dacik Date: Wed, 4 May 2022 14:57:28 +0200 Subject: [PATCH 02/21] enable strong updates of unique heap variables --- src/cdomains/valueDomain.ml | 17 +++++++++- tests/regression/11-heap/07-strong_updates.c | 25 ++++++++++++++ .../regression/11-heap/08-no_strong_update.c | 25 ++++++++++++++ .../09-no_strong_update_not_unique_thread.c | 33 +++++++++++++++++++ .../10-no_strong_update_different_size.c | 20 +++++++++++ 5 files changed, 119 insertions(+), 1 deletion(-) create mode 100644 tests/regression/11-heap/07-strong_updates.c create mode 100644 tests/regression/11-heap/08-no_strong_update.c create mode 100644 tests/regression/11-heap/09-no_strong_update_not_unique_thread.c create mode 100644 tests/regression/11-heap/10-no_strong_update_different_size.c diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 9b04c65ea2..26a6cabf21 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -896,7 +896,22 @@ struct begin let l', o' = shift_one_over l o in let x = zero_init_calloced_memory orig x t in - mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig)) + (* 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.f (Q.IsMultiple var) + && not @@ Cil.isVoidType t (* Size of value is known *) + && Option.is_some blob_size_opt (* Size of blob is known *) + && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t) + | _ -> false + end + in + if do_strong_update then + `Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig) + else + mu (`Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig)) end | `Thread _, _ -> (* hack for pthread_t variables *) diff --git a/tests/regression/11-heap/07-strong_updates.c b/tests/regression/11-heap/07-strong_updates.c new file mode 100644 index 0000000000..d18b35d1cf --- /dev/null +++ b/tests/regression/11-heap/07-strong_updates.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.malloc.unique_address_count 2 + +// Both variables x and y are unique and can be strongly (destructively) updated. + +#include +#include +#include + +void* myalloc(size_t s) { + return malloc(s); +} + +int main() { + int* x = myalloc(sizeof(int)); + int* y = myalloc(sizeof(int)); + + *x = 0; + *y = 1; + + *x = 2; + *y = 3; + + assert (*x == 2); + assert (*y == 3); +} diff --git a/tests/regression/11-heap/08-no_strong_update.c b/tests/regression/11-heap/08-no_strong_update.c new file mode 100644 index 0000000000..ab8801439f --- /dev/null +++ b/tests/regression/11-heap/08-no_strong_update.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.malloc.unique_address_count 1 + +// Copied from 11/05. Here, variable y is not unique and cannot be strongly updated. + +#include +#include + +void* myalloc(size_t s) { + return malloc(s); +} + +int main() { + int* x = myalloc(sizeof(int)); + int* y = myalloc(sizeof(int)); + int *p; + + *x = 0; + *y = 1; + + *x = 2; + *y = 3; + + assert (*x == 2); + assert (*y == 3); // UNKNOWN! +} diff --git a/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c b/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c new file mode 100644 index 0000000000..025e219b26 --- /dev/null +++ b/tests/regression/11-heap/09-no_strong_update_not_unique_thread.c @@ -0,0 +1,33 @@ +// PARAM: --set ana.malloc.unique_address_count 2 + +// Strong updates are not possible in thread because it is not unique. + +#include +#include +#include + +void *thread(void *v) +{ + int *x = malloc(sizeof(int)); + int *y = malloc(sizeof(int)); + + *x = 0; + *y = 1; + + *x = 2; + *y = 3; + + assert (*x == 2); // UNKNOWN! + assert (*y == 3); // UNKNOWN! +} + +int main(int argc, char **argv) +{ + pthread_t tids[argc]; + + for (int i = 0; i < argc; i++) + pthread_create(&tids[i], NULL, thread, NULL); + + for (int i = 0; i < argc; i++) + pthread_join(tids[i], NULL); +} diff --git a/tests/regression/11-heap/10-no_strong_update_different_size.c b/tests/regression/11-heap/10-no_strong_update_different_size.c new file mode 100644 index 0000000000..6ddde7d013 --- /dev/null +++ b/tests/regression/11-heap/10-no_strong_update_different_size.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.malloc.unique_address_count 2 + +#include +#include +#include + +void* myalloc(size_t s) { + return malloc(s); +} + +int main() { + int *x = myalloc(2 * sizeof(int)); + int *y = myalloc(2 * sizeof(int)); + + *x = 0; + *y = 1; + *x = 2; // Size of written value is shorter than blob + + assert (*x == 2); // UNKNOWN! +} From 68db36de2b2ab6df1647e5b555fb02f9a2a93831 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 10 May 2022 14:46:39 +0200 Subject: [PATCH 03/21] Fix JSON syntax error in options schema Co-authored-by: Simmo Saan --- src/util/options.schema.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 4d51420350..57cf21928e 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -815,7 +815,7 @@ "kzalloc" ] }, - unique_address_count: { + "unique_address_count": { "title": "ana.malloc.unique_address_count", "description": "Number of unique memory addresses allocated for each malloc node.", "type": "integer", From d4fe8f2f4197b7bd34d83b7a61438a1bd616d764 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 10 May 2022 14:47:55 +0200 Subject: [PATCH 04/21] Remove explicit enabling of recording of backtraces (done via `-v`) Co-authored-by: Simmo Saan --- src/analyses/mallocWrapperAnalysis.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 2ca1a22d28..647f2dd318 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -146,7 +146,6 @@ struct | _ -> Queries.Result.top q let init marshal = - Printexc.record_backtrace true; List.iter (fun wrapper -> Hashtbl.replace wrappers wrapper ()) (get_string_list "ana.malloc.wrappers"); NodeVarinfoMap.unmarshal marshal From 2ce399aef6dd6458acbb348139234bc8f51a6f25 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 14:40:45 +0200 Subject: [PATCH 05/21] Fix indentation --- src/analyses/libraryFunctions.ml | 2 +- src/cdomains/arrayDomain.ml | 4 ++-- src/extract/pml_arinc.ml | 2 +- src/incremental/compareCIL.ml | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index ffd14339e3..9da6a724ee 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -42,7 +42,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ (** Linux kernel functions. *) let linux_descs_list: (string * LibraryDesc.t) list = (* LibraryDsl. *) [ - ] +] (** Goblint functions. *) let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml index c666ee138c..355ad77dcf 100644 --- a/src/cdomains/arrayDomain.ml +++ b/src/cdomains/arrayDomain.ml @@ -458,7 +458,7 @@ struct (e,(xl,a,xr)) else let left = if equals_zero i then Val.bot () else Val.join xl @@ Val.join - (match Q.may_be_equal ask e' i' with (* TODO: untested *) + (match Q.may_be_equal ask e' i' with (* TODO: untested *) | false -> Val.bot() | _ -> xm) (* if e' may be equal to i', but e' may not be smaller than i' then we only need xm *) ( @@ -475,7 +475,7 @@ struct ) in let right = if equals_maxIndex i then Val.bot () else Val.join xr @@ Val.join - (match Q.may_be_equal ask e' i' with (* TODO: untested *) + (match Q.may_be_equal ask e' i' with (* TODO: untested *) | false -> Val.bot() | _ -> xm) diff --git a/src/extract/pml_arinc.ml b/src/extract/pml_arinc.ml index a6eb17c198..2fb6f9d1d8 100644 --- a/src/extract/pml_arinc.ml +++ b/src/extract/pml_arinc.ml @@ -17,7 +17,7 @@ let init ?(nproc=99) ?(nsema=99) ?(nevent=99) ?(nbboard=99) () = (* TODO better let nsema = fst @@ var (Byte nsema) "nsema" in let nevent = fst @@ var (Byte nevent) "nevent" in let nbboard = fst @@ var (Byte nbboard) "nbboard" in - + (* Pml.do_; (* ppx_monadic: from now on ; is bind *) *) (* switched to ocaml-monadic because ppx_monadic was constraining us to ocaml <4.08, now have to use ;%bind instead of just ; and `let%bind x = e in` instead of `x <-- e;` *) (* Dropped ocaml-monadic and used let* syntax introduced in OCaml 4.08. Use `let* () = e in` instead of `e;%bind` *) diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index a956cb6609..13a1be4f69 100644 --- a/src/incremental/compareCIL.ml +++ b/src/incremental/compareCIL.ml @@ -137,7 +137,7 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) = with Not_found -> map in - + let changes = empty_change_info () in global_typ_acc := []; let findChanges map global global_rename_mapping = From 2c40bb76e37d476c1edb9eac6cd3c6d4815d56fb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 14:56:35 +0200 Subject: [PATCH 06/21] Modify ChainLattice to have function n: unit -> int instead of int: n --- src/analyses/mallocWrapperAnalysis.ml | 11 ++++------- src/cdomains/threadFlagDomain.ml | 2 +- src/domains/lattice.ml | 4 ++-- src/domains/printable.ml | 4 ++-- src/witness/observerAnalysis.ml | 2 +- src/witness/yamlWitness.ml | 2 +- 6 files changed, 11 insertions(+), 14 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index e7024ccbe7..075b113492 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -5,7 +5,7 @@ open Analyses open GobConfig open ThreadIdDomain -module Spec () : Analyses.MCPSpec = +module Spec: Analyses.MCPSpec = struct include Analyses.DefaultSpec @@ -15,13 +15,13 @@ struct end) module Chain = Lattice.Chain (struct - let n = + let n () = let p = get_int "ana.malloc.unique_address_count" in if p < 0 then failwith "Option ana.malloc.unique_address_count has to be non-negative" else p + 1 (* Unique addresses + top address *) - let names x = if Int.equal x (n - 1) then "top" else Format.asprintf "%d" x + let names x = if x = (n () - 1) then "top" else Format.asprintf "%d" x end) @@ -154,8 +154,5 @@ struct NodeVarinfoMap.marshal () end -let after_config () = - MCP.register_analysis (module Spec ()) - let _ = - AfterConfig.register after_config + MCP.register_analysis (module Spec) diff --git a/src/cdomains/threadFlagDomain.ml b/src/cdomains/threadFlagDomain.ml index 8fef40ac7d..09d19d9e74 100644 --- a/src/cdomains/threadFlagDomain.ml +++ b/src/cdomains/threadFlagDomain.ml @@ -30,7 +30,7 @@ module Simple: S = struct module SimpleNames = struct - let n = 3 + let n () = 3 let names = function | 0 -> "Singlethreaded" | 1 -> "Multithreaded (main)" diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml index c6920d9e3f..09f52bb8a3 100644 --- a/src/domains/lattice.ml +++ b/src/domains/lattice.ml @@ -580,8 +580,8 @@ struct let bot () = 0 let is_bot x = x = 0 - let top () = P.n - 1 - let is_top x = x = P.n - 1 + let top () = P.n () - 1 + let is_top x = x = P.n () - 1 let leq x y = x <= y let join x y = max x y diff --git a/src/domains/printable.ml b/src/domains/printable.ml index a67bee25c8..77e65f3de3 100644 --- a/src/domains/printable.ml +++ b/src/domains/printable.ml @@ -463,7 +463,7 @@ struct end module type ChainParams = sig - val n: int + val n: unit -> int val names: int -> string end @@ -477,7 +477,7 @@ struct let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (P.names x) let to_yojson x = `String (P.names x) - let arbitrary () = QCheck.int_range 0 (P.n - 1) + let arbitrary () = QCheck.int_range 0 (P.n () - 1) let relift x = x end diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml index 8837d9fe6c..ec39fd9020 100644 --- a/src/witness/observerAnalysis.ml +++ b/src/witness/observerAnalysis.ml @@ -24,7 +24,7 @@ struct module ChainParams = struct (* let n = List.length Arg.path *) - let n = -1 + let n () = -1 let names x = "state " ^ string_of_int x end module D = Lattice.Flat (Printable.Chain (ChainParams)) (Printable.DefaultNames) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 03885a31fe..028f99e65d 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -194,7 +194,7 @@ struct module ChainParams = struct - let n = max_result - 1 + let n () = max_result - 1 let names i = show_result (Option.get (result_of_enum i)) end include Lattice.Chain (ChainParams) From 41aa0e712103e1d89a1d330485ef4e1e144e28d9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 15:34:05 +0200 Subject: [PATCH 07/21] typo --- tests/regression/22-partitioned_arrays/17-large_arrays.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/22-partitioned_arrays/17-large_arrays.c b/tests/regression/22-partitioned_arrays/17-large_arrays.c index fc29839a36..c449a8ec91 100644 --- a/tests/regression/22-partitioned_arrays/17-large_arrays.c +++ b/tests/regression/22-partitioned_arrays/17-large_arrays.c @@ -5,7 +5,7 @@ #include #include -// Test to check whether partitioned arrays can have an index expression evaluating to values largers than the max value of int64 +// Test to check whether partitioned arrays can have an index expression evaluating to values larger than the max value of int64 #define LENGTH (LONG_MAX - 600) #define STOP (LENGTH - 1) From 768963f7e038bc95905e71f068410b44363bea83 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 15:38:26 +0200 Subject: [PATCH 08/21] Better readable output for malloc nodes --- src/analyses/mallocWrapperAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 075b113492..3c5e271505 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -55,13 +55,13 @@ struct module ThreadNode = struct include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain) - (* Description that gets appended to the varinfo-name in user ouptut. *) + (* Description that gets appended to the varinfo-name in user output. *) let describe_varinfo (v: varinfo) (t, node, c) = let loc = UpdateCil.getLoc node in CilType.Location.show loc let name_varinfo (t, node, c) = - Format.asprintf "(allocs@%s@%s(#%s))" (ThreadLifted.show t) (Node.show node) (Chain.show c) + Format.asprintf "(alloc@sid:%s@tid:%s(#%s))" (Node.show_id node) (ThreadLifted.show t) (Chain.show c) end From 5234d22f0cf0eafd2487c570fdab7c41cbd828be Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 15:57:37 +0200 Subject: [PATCH 09/21] Simplify logic in combine --- src/analyses/mallocWrapperAnalysis.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 3c5e271505..2dd0c30ef3 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -43,9 +43,6 @@ struct module Domain = struct include Lattice.Prod (MallocCounter) (PL) - let join (counter1, node1) (counter2, node2) = - (MallocCounter.join counter1 counter2, node1) - let has_wrapper_node (_, wrapper_node) = not @@ PL.is_top wrapper_node let get_count (counter, _) node = MallocCounter.find (`Lifted node) counter @@ -106,8 +103,10 @@ struct let callee_ctx = (new_counter, new_wrapper_node) in [(caller_ctx, callee_ctx)] - let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = - D.join ctx.local au + let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) : D.t = + (* Keep (potentially higher) counter from callee and keep wrapper node from caller *) + let lcounter, lnode = ctx.local in + (counter, lnode) let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = let counter, wrapper_node = ctx.local in From 82b24546ee901a1cf66a1f67441b34ea8b9addab Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 17:03:21 +0200 Subject: [PATCH 10/21] Simplify mallocWrapper --- src/analyses/mallocWrapperAnalysis.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 2dd0c30ef3..056a4c9ae8 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -87,11 +87,6 @@ struct let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let counter, wrapper_node = ctx.local in - let new_counter = - if Hashtbl.mem wrappers f.svar.vname then - MallocCounter.add_malloc counter ctx.prev_node - else counter - in let new_wrapper_node = if Hashtbl.mem wrappers f.svar.vname then if not @@ D.has_wrapper_node ctx.local then @@ -99,9 +94,8 @@ struct else wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *) else PL.top () (* if an uninteresting callee is called, then we forget what was called before *) in - let caller_ctx = (new_counter, wrapper_node) in - let callee_ctx = (new_counter, new_wrapper_node) in - [(caller_ctx, callee_ctx)] + let callee = (counter, new_wrapper_node) in + [(ctx.local, callee)] let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) : D.t = (* Keep (potentially higher) counter from callee and keep wrapper node from caller *) @@ -109,10 +103,11 @@ struct (counter, lnode) let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - let counter, wrapper_node = ctx.local in let desc = LibraryFunctions.find f in match desc.special arglist, f.vname with - | Malloc _, _ | Calloc _, _ | Realloc _, _ -> (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node) + | Malloc _, _ | Calloc _, _ | Realloc _, _ -> + let counter, wrapper_node = ctx.local in + (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node) | _ -> ctx.local let startstate v = D.bot () From bd22bfaff861a4313beb0bd8df571c164566436d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 18:01:57 +0200 Subject: [PATCH 11/21] mallocWrapper: rm `has_wrapper_node` --- src/analyses/mallocWrapperAnalysis.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 056a4c9ae8..2f666b9d54 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -43,10 +43,7 @@ struct module Domain = struct include Lattice.Prod (MallocCounter) (PL) - let has_wrapper_node (_, wrapper_node) = not @@ PL.is_top wrapper_node - let get_count (counter, _) node = MallocCounter.find (`Lifted node) counter - end module ThreadNode = struct @@ -89,10 +86,11 @@ struct let counter, wrapper_node = ctx.local in let new_wrapper_node = if Hashtbl.mem wrappers f.svar.vname then - if not @@ D.has_wrapper_node ctx.local then - (`Lifted ctx.prev_node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) - else wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *) - else PL.top () (* if an uninteresting callee is called, then we forget what was called before *) + match wrapper_node with + | `Lifted _ -> wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *) + | _ -> (`Lifted ctx.prev_node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) + else + PL.top () (* if an uninteresting callee is called, then we forget what was called before *) in let callee = (counter, new_wrapper_node) in [(ctx.local, callee)] From 932c752c80787c6569e02fcc5f195458a7151d08 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 18:05:58 +0200 Subject: [PATCH 12/21] simplify --- src/analyses/mallocWrapperAnalysis.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 2f666b9d54..b41ce6653b 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -40,12 +40,6 @@ struct |> add malloc (count + 1) end - module Domain = struct - include Lattice.Prod (MallocCounter) (PL) - - let get_count (counter, _) node = MallocCounter.find (`Lifted node) counter - end - module ThreadNode = struct include Printable.Prod3 (ThreadIdDomain.ThreadLifted) (Node) (Chain) @@ -61,8 +55,8 @@ struct module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode) let name () = "mallocWrapper" - - module D = Domain + + module D = Lattice.Prod (MallocCounter) (PL) module C = D module Q = Queries @@ -119,14 +113,15 @@ struct let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result = - let _, wrapper_node = ctx.local in + let counter, wrapper_node = ctx.local in match q with | Q.HeapVar -> let node = match wrapper_node with | `Lifted wrapper_node -> wrapper_node | _ -> ctx.prev_node in - let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, D.get_count ctx.local node) in + let count = MallocCounter.find (`Lifted node) counter in + let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, count) in var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *) `Lifted var | Q.IsHeapVar v -> From 53b810290d799d788efc825dd18bae329dff6064 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 18:07:01 +0200 Subject: [PATCH 13/21] simplify --- src/analyses/mallocWrapperAnalysis.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index b41ce6653b..31f9d624d6 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -91,7 +91,7 @@ struct let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) : D.t = (* Keep (potentially higher) counter from callee and keep wrapper node from caller *) - let lcounter, lnode = ctx.local in + let _, lnode = ctx.local in (counter, lnode) let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = From 8fdc8a6adb971585960d6be8d5f6e5d3bef62425 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 18:12:22 +0200 Subject: [PATCH 14/21] save a line --- src/analyses/mallocWrapperAnalysis.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 31f9d624d6..c31698c88d 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -36,8 +36,7 @@ struct if Chain.is_top count then counter else - remove malloc counter - |> add malloc (count + 1) + remove malloc counter |> add malloc (count + 1) end module ThreadNode = struct From 430f1addb0b6f9cfb8828f73913b362a2aaa5f1e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 18 Jul 2022 18:13:56 +0200 Subject: [PATCH 15/21] Pull out alias for Queroes, use consistently --- src/analyses/mallocWrapperAnalysis.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index c31698c88d..8bf97fe2c1 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -4,6 +4,7 @@ open Prelude.Ana open Analyses open GobConfig open ThreadIdDomain +module Q = Queries module Spec: Analyses.MCPSpec = struct @@ -58,8 +59,6 @@ struct module D = Lattice.Prod (MallocCounter) (PL) module C = D - module Q = Queries - let wrappers = Hashtbl.create 13 (* transfer functions *) @@ -111,7 +110,7 @@ struct let get_heap_var = NodeVarinfoMap.to_varinfo - let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Queries.result = + let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Q.result = let counter, wrapper_node = ctx.local in match q with | Q.HeapVar -> From a992328e40dcb0965270eb7609eae693e832e427 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 24 Jul 2022 14:54:12 +0200 Subject: [PATCH 16/21] Add example for unsoundness for calloc --- tests/regression/11-heap/12-calloc.c | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 tests/regression/11-heap/12-calloc.c diff --git a/tests/regression/11-heap/12-calloc.c b/tests/regression/11-heap/12-calloc.c new file mode 100644 index 0000000000..db1b21d5a5 --- /dev/null +++ b/tests/regression/11-heap/12-calloc.c @@ -0,0 +1,8 @@ +// PARAM: --set ana.malloc.unique_address_count 1 +#include +#include +int main() { + int* arr = calloc(5,sizeof(int)); + arr[0] = 3; + assert(arr[2] == 0); //UNKNOWN +} From c0da1e4ba5515596561deac6be1865c262b1d8f9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 24 Jul 2022 15:17:07 +0200 Subject: [PATCH 17/21] Fix incorrect size for calloc blobs (Introduced in 3d27f41c665c60a6080d66ccfb64dd85404cb314) --- src/analyses/base.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index bbf43eed3a..5d990030a6 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2428,8 +2428,10 @@ struct if get_bool "sem.malloc.fail" then AD.join addr AD.null_ptr (* calloc can fail and return NULL *) else addr in + let ik = Cilfacade.ptrdiff_ikind () in + let blobsize = ID.mul (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st size) (ID.cast_to ik @@ eval_int (Analyses.ask_of_ctx ctx) gs st n) in (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *) - set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, false)))); + set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.from_var heap_var), TVoid [], `Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.one) (`Blob (VD.bot (), blobsize, false)))); (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), `Address (add_null (AD.from_var_offset (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero, `NoOffset)))))] | _ -> st end From e256f8086b9c69feedc23fccc3f6dbb8a1f7a4eb Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 24 Jul 2022 15:40:00 +0200 Subject: [PATCH 18/21] Add linear search regression --- tests/regression/11-heap/13-linear-search.c | 30 +++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 tests/regression/11-heap/13-linear-search.c diff --git a/tests/regression/11-heap/13-linear-search.c b/tests/regression/11-heap/13-linear-search.c new file mode 100644 index 0000000000..e5f586cba6 --- /dev/null +++ b/tests/regression/11-heap/13-linear-search.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.malloc.unique_address_count 3 --enable ana.sv-comp.functions +extern void *calloc(unsigned int num, unsigned int size); + +void __VERIFIER_as(int cond) { + if (!(cond)) { + assert(1); // reachable + } + return; +} +unsigned int __VERIFIER_nondet_uint(); +unsigned int SIZE; +const unsigned int MAX = 100000; +int linear_search(int *a, int n, int q) { + unsigned int j=0; + while (j 1 && SIZE < MAX) { + int *a = calloc(SIZE,sizeof(int)); + a[SIZE/2]=3; + __VERIFIER_as(linear_search(a,SIZE,3)); + } +} From dba164a5b4ba241511afb1fd846745d2cc9246c1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 25 Jul 2022 10:49:52 +0200 Subject: [PATCH 19/21] Comment that counter is per thread --- src/analyses/mallocWrapperAnalysis.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 8bf97fe2c1..6851aae2b0 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -26,7 +26,7 @@ struct end) - (* Map for counting malloc node visits up to n. *) + (* Map for counting malloc node visits up to n (of the current thread). *) module MallocCounter = struct include MapDomain.MapBot_LiftTop(PL)(Chain) @@ -101,7 +101,11 @@ struct | _ -> ctx.local let startstate v = D.bot () - let threadenter ctx lval f args = [D.bot ()] + + let threadenter ctx lval f args = + (* The new thread receives a fresh counter *) + [D.bot ()] + let threadspawn ctx lval f args fctx = ctx.local let exitstate v = D.top () From 0f70fbc6766b642bf388470cca622d997e03c1e7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 25 Jul 2022 10:53:23 +0200 Subject: [PATCH 20/21] Rm spurious pattern match on `f.vname` --- src/analyses/mallocWrapperAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 6851aae2b0..ad83236676 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -94,8 +94,8 @@ struct let special (ctx: (D.t, G.t, C.t, V.t) ctx) (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = let desc = LibraryFunctions.find f in - match desc.special arglist, f.vname with - | Malloc _, _ | Calloc _, _ | Realloc _, _ -> + match desc.special arglist with + | Malloc _ | Calloc _ | Realloc _ -> let counter, wrapper_node = ctx.local in (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node) | _ -> ctx.local From 77c0423640c50bb82e4290bcc97f33d4082715d0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 25 Jul 2022 11:10:52 +0200 Subject: [PATCH 21/21] Use `ctx.node` instead of `ctx.prev_node` again --- src/analyses/mallocWrapperAnalysis.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index ad83236676..90c167bdad 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -80,7 +80,7 @@ struct if Hashtbl.mem wrappers f.svar.vname then match wrapper_node with | `Lifted _ -> wrapper_node (* if an interesting callee is called by an interesting caller, then we remember the caller context *) - | _ -> (`Lifted ctx.prev_node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) + | _ -> (`Lifted ctx.node) (* if an interesting callee is called by an uninteresting caller, then we remember the callee context *) else PL.top () (* if an uninteresting callee is called, then we forget what was called before *) in @@ -97,7 +97,7 @@ struct match desc.special arglist with | Malloc _ | Calloc _ | Realloc _ -> let counter, wrapper_node = ctx.local in - (MallocCounter.add_malloc counter ctx.prev_node, wrapper_node) + (MallocCounter.add_malloc counter ctx.node, wrapper_node) | _ -> ctx.local let startstate v = D.bot () @@ -120,7 +120,7 @@ struct | Q.HeapVar -> let node = match wrapper_node with | `Lifted wrapper_node -> wrapper_node - | _ -> ctx.prev_node + | _ -> ctx.node in let count = MallocCounter.find (`Lifted node) counter in let var = get_heap_var (ctx.ask Q.CurrentThreadId, node, count) in