`malloc_null`: Interprocedural analysis unsound

[michael-schwarz]

While fixing the bug that surfaced in #1688, I realized that the interprocedural handling of the malloc_null analysis is completely broken.
Even without any top pointers involved, callees always seem to get the empty set of addresses.

// PARAM: --set ana.activated[+] malloc_null --set ana.path_sens[-] malloc_null
#include <stdlib.h>
#include <goblint.h>

void fun(int* a) {
        *a = 5; //WARN
}


int main(void) {
        int *x;

        x = malloc(sizeof(int));
        fun(x);
        *x =8; //WARN

        return 0;
}

In this example, we produce warnings at both program points. However, at the dereference of a only base warns

[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (tests/regression/08-malloc_null/03-more.c:6:9-6:15)

while at the dereference of x, we also get a warning from malloc_null:

[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (tests/regression/08-malloc_null/03-more.c:15:9-15:15)
[Warning][Behavior > Undefined > NullPointerDereference] Possible dereferencing of null on variable 'x'. (tests/regression/08-malloc_null/03-more.c:15:9-15:15)

I traced the problem part of the way already:

analyzer/src/analyses/malloc_null.ml

Lines 95 to 118 in 746d436

	let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
	let reachable =
	let do_exp e a =
	match ask.f (Queries.ReachableFrom e) with
	| ad when not (Queries.AD.is_top ad) ->
	ad
	|> Queries.AD.filter (function
	| Queries.AD.Addr.Addr _ -> true
	| _ -> false)
	|> Queries.AD.join a
	(* Ignore soundness warnings, as invalidation proper will raise them. *)
	| _ -> AD.empty ()
	in
	List.fold_right do_exp args (AD.empty ())
	in
	let vars =
	reachable
	|> AD.to_var_may
	|> List.concat_map to_addrs
	|> AD.of_list
	in
	if D.is_top st
	then D.top ()
	else D.filter (fun x -> AD.mem x vars) st

Here, vars correctly contains x, but it is somehow filtered out in the last step even though st supposedly also contains it.

The reason we have not seen any issues with this likely is that base now seems to duplicate the warnings of malloc_nulll anyway, which I guess means malloc_null is only useful for the fact that it causes path splitting.

What do we want to do here? Do we repair it? Or remove the warning facilities from the analysis and trim it down to a helper analysis that causes additional path-splitting?

[sim642]

I haven't looked closely at the malloc_null analysis and its domain, but its warning facilities sound redundant indeed if they can't be more precise than base.

Either way, it seems to do its own access iteration which is also redundant because we have the access analysis for emitting events about those. Other analyses like uninit and memOutOfBounds also fall into that category.

[sim642]

Fun fact: I recently happened upon Kalmer's MSc thesis (http://hdl.handle.net/10062/71802), which is in Estonian, but has Section 3, which seems to be exactly about this analysis.
The thesis also seems to describe the uninit analysis, which, if I remember correctly, looks quite similar. So maybe it also has similar issues?