From 9485208d7c9898a4c61c9139ea5fe351ca03e809 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 28 Jun 2024 17:45:27 +0300 Subject: [PATCH 1/9] Remove deadcode that catches `SetDomain.Unsupported` --- src/analyses/base.ml | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 29fa74c5a9..7f39db6b50 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1735,21 +1735,16 @@ struct match Addr.to_mval x with | Some x -> update_one_addr x store | None -> store - in try - (* We start from the current state and an empty list of global deltas, - * and we assign to all the the different possible places: *) - let nst = AD.fold update_one lval st in - (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) - (* If the address was definite, then we just return it. If the address - * was ambiguous, we have to join it with the initial state. *) - let nst = if AD.cardinal lval > 1 then D.join st nst else nst in - (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) - nst - with - (* If any of the addresses are unknown, we ignore it!?! *) - | SetDomain.Unsupported x -> - (* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'" x; *) - M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st + in + (* We start from the current state and an empty list of global deltas, + * and we assign to all the the different possible places: *) + let nst = AD.fold update_one lval st in + (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) + (* If the address was definite, then we just return it. If the address + * was ambiguous, we have to join it with the initial state. *) + let nst = if AD.cardinal lval > 1 then D.join st nst else nst in + (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) + nst let set_many ~ctx (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) From 65e1ccc7b0a52940466223344a44d6cef4fc15fd Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 28 Jun 2024 17:57:45 +0300 Subject: [PATCH 2/9] Replace complicated set logic with simplified AD.fold --- src/analyses/base.ml | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 7f39db6b50..104bc7e861 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1736,15 +1736,10 @@ struct | Some x -> update_one_addr x store | None -> store in - (* We start from the current state and an empty list of global deltas, - * and we assign to all the the different possible places: *) - let nst = AD.fold update_one lval st in - (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) - (* If the address was definite, then we just return it. If the address - * was ambiguous, we have to join it with the initial state. *) - let nst = if AD.cardinal lval > 1 then D.join st nst else nst in - (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) - nst + if AD.is_empty lval then + st + else + AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ()) let set_many ~ctx (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) From 87a979a42cfd03fa71a2b91bfb728300bdce7611 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 28 Jun 2024 18:01:19 +0300 Subject: [PATCH 3/9] Make update_one case handling explicit --- src/analyses/base.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 104bc7e861..7734e9a98c 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1731,10 +1731,12 @@ struct effect_on_arrays ask with_dep end in - let update_one x store = - match Addr.to_mval x with - | Some x -> update_one_addr x store - | None -> store + let update_one (x : Addr.t) store = + match x with + | Addr x -> update_one_addr x store + | NullPtr + | UnknownPtr + | StrPtr _ -> store in if AD.is_empty lval then st From c4d96e86c11ddeed260b4ea87c41be42fa4141fe Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 1 Jul 2024 16:15:37 +0300 Subject: [PATCH 4/9] Assert that the set of lvals is not empty when written to --- src/analyses/base.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 7734e9a98c..89936e66ee 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1737,11 +1737,9 @@ struct | NullPtr | UnknownPtr | StrPtr _ -> store - in - if AD.is_empty lval then - st - else - AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ()) + in + assert (not @@ AD.is_empty lval); + AD.fold (fun addr acc -> D.join (update_one addr st) acc) lval (D.bot ()) let set_many ~ctx (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) From c7199a04656119b03fa3facf80146495790defc6 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 1 Jul 2024 16:18:05 +0300 Subject: [PATCH 5/9] Do not remove NullPtr-s from address sets --- src/analyses/base.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 89936e66ee..872c0a7d5a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -540,9 +540,9 @@ struct if not (VD.is_immediate_type t) then M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty | Bot -> (*M.debug ~category:Analyzer "A bottom value when computing reachable addresses!";*) empty | Address adrs when AD.is_top adrs -> - M.info ~category:Unsound "Unknown address in %s has escaped." description; AD.remove Addr.NullPtr adrs (* return known addresses still to be a bit more sane (but still unsound) *) + M.info ~category:Unsound "Unknown address in %s has escaped." description; adrs (* return known addresses still to be a bit more sane (but still unsound) *) (* The main thing is to track where pointers go: *) - | Address adrs -> AD.remove Addr.NullPtr adrs + | Address adrs -> adrs (* Unions are easy, I just ingore the type info. *) | Union (f,e) -> reachable_from_value ask e t description (* For arrays, we ask to read from an unknown index, this will cause it @@ -2029,7 +2029,7 @@ struct collect_funargs ~ctx ~warn st exps else ( let mpt e = match eval_rv_address ~ctx st e with - | Address a -> AD.remove NullPtr a + | Address a -> a | _ -> AD.empty () in List.map mpt exps From 7816bed8049b77290b60d4b50f38b5c80b875884 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 1 Jul 2024 16:20:07 +0300 Subject: [PATCH 6/9] Add stdlib.h for correctly importing strtol --- tests/regression/41-stdlib/05-more.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/regression/41-stdlib/05-more.c b/tests/regression/41-stdlib/05-more.c index 019eb84110..a18a2a9418 100644 --- a/tests/regression/41-stdlib/05-more.c +++ b/tests/regression/41-stdlib/05-more.c @@ -2,6 +2,7 @@ #include #include #include +#include int g = 8; From 7d87b3545ad4ba9279eb4a22384b97aab1508a5a Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 1 Jul 2024 17:46:58 +0300 Subject: [PATCH 7/9] Fix `17-per_elem_simp`: nowarn -> norace --- tests/regression/05-lval_ls/17-per_elem_simp.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/05-lval_ls/17-per_elem_simp.c b/tests/regression/05-lval_ls/17-per_elem_simp.c index 7769de2b8a..9997a96028 100644 --- a/tests/regression/05-lval_ls/17-per_elem_simp.c +++ b/tests/regression/05-lval_ls/17-per_elem_simp.c @@ -21,7 +21,7 @@ struct t { void* f(struct t* in) { start_unpack(in); pthread_mutex_lock(&(in->lock)); - in->data++; // NOWARN + in->data++; // NORACE pthread_mutex_unlock(&(in->lock)); end_unpack(in); return 0; From a30fbfc3add97d40d400bce360f9cb821439f35e Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Mon, 1 Jul 2024 17:51:09 +0300 Subject: [PATCH 8/9] Do not remove `UnknownPtr` from address set before running `reachable_vars` --- src/analyses/base.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 872c0a7d5a..6f329b5d9a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1486,13 +1486,9 @@ struct | Top -> Queries.Result.top q | Bot -> Queries.Result.bot q (* TODO: remove *) | 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 ~ctx ctx.local [a'] in - 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' + [a] + |> reachable_vars ~ctx ctx.local + |> List.fold_left (AD.join) (AD.empty ()) | Int i -> begin match Cilfacade.typeOf e with | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *) From 684378481b30aca9655a0036127011125b97fb6c Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 16 Aug 2024 14:31:05 +0300 Subject: [PATCH 9/9] Use `sem.null-pointer.dereference` option for writing as well --- src/analyses/base.ml | 9 +++++++-- src/config/options.schema.json | 2 +- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 6f329b5d9a..7b9d2ad31a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1730,7 +1730,12 @@ struct let update_one (x : Addr.t) store = match x with | Addr x -> update_one_addr x store - | NullPtr + | NullPtr -> + begin match get_string "sem.null-pointer.dereference" with + | "assume_none" -> D.bot () + | "assume_top" -> store + | _ -> assert false + end | UnknownPtr | StrPtr _ -> store in @@ -2032,7 +2037,7 @@ struct ) let invalidate ?(deep=true) ~ctx (st:store) (exps: exp list): store = - if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " d_plainexp) exps; + if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " d_exp) exps; if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps; (* To invalidate a single address, we create a pair with its corresponding * top value. *) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index d259a6f418..6b60d1fc8b 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1474,7 +1474,7 @@ "properties": { "dereference": { "title": "sem.null-pointer.dereference", - "description": "NULL pointer dereference handling. assume_top: assume it results in a top value, assume_none: assume it doesn't happen", + "description": "NULL pointer dereference handling. assume_top: reading returns top value, writing is ignored; assume_none: assumes that reading or writing to NULL pointer does not happen", "type": "string", "enum": ["assume_top", "assume_none"], "default": "assume_none"