Apron: Track relational information for variables that have their address taken

[michael-schwarz]

TODOs:

• Handle escapes
• Handle variables that need to be updated weakly
• Check if it still works with local of outer functions with different names reachable
• Rectify locals of function in which thread is created leaking to created thread
• Test

The strange numbering in apron2 is for consistency with #391

Closes #660

[michael-schwarz]

Looks like this is not a simple local change but will require extensive changes, as after considering escaping, it no longer is true that a variable is either a global or a local, but instead it may be both depending on whether it escaped. 😮‍💨

[sim642]

considering escaping, it no longer is true that a variable is either a global or a local, but instead it may be both depending on whether it escaped.

But at any particular program point, it's either must-local or may-escaped, no?

[sim642]

Something I just remembered related to this: previously special in apron analysis could completely avoid having to invalidate arguments:

analyzer/src/analyses/apron/apronAnalysis.apron.ml

Lines 372 to 388 in 739ef9c

	let st' = match LibraryFunctions.get_invalidate_action f.vname with
	| Some fnc -> st (* nothing to do because only AddrOf arguments may be invalidated *)
	| None ->
	(* nothing to do for args because only AddrOf arguments may be invalidated *)
	if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then (
	let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
	match global with
	| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
	(Var vi, NoOffset) :: acc
	(* TODO: what about GVarDecl? *)
	| _ -> acc
	) []
	in
	List.fold_left invalidate_one st globals
	)
	else
	st

With these changes-to-be, this is no longer true and it will have to invalidate written arguments, similarly to how base analysis does it.

In doing so, #720 might be very useful to have such that some library function doesn't completely top-ify everything. Because pre-#720, Write accesses to arguments all followed pointers transitively (using ReachableFrom query), which in real-world programs often ends up invalidating almost everything. That could be disastrous to relational traces benchmarking, if it makes us forget all invariants.

[sim642]

I guess it's fine for now as-is so we can quickly move to see if this helps us find any more relational invariants.

Totally off-topic, but exists on a topped set being true is actually weird, since it claims that exists (fun _ -> false) is also true 🙃

[sim642]

I just tried running the relational traces bench on this branch and they all seem to immediately crash with:

Fatal error: exception IntDomain.IncompatibleIKinds("ikinds char and int are incompatible. Values: (Unknown int([-7,7]),not {} ([-7,7])) and (Unknown int([-31,31]),not {} ([-31,31]))")

[michael-schwarz]

Is it only this branch or also already on master? There should be no changes to the handling of non-apron things in here, and apron does not do anything with ints.

[sim642]

Only on this branch, the initial problem is that dereferencing doesn't exclude the unknown pointer. This patch fixes that:

diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 3ac185d7a..5c5b494ef 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -158,8 +158,8 @@ struct
       | Lval (Var v, off) -> Lval (Var v, off)
       | Lval (Mem e, NoOffset) ->
         (match ask (Queries.MayPointTo e) with
-         | (`Lifted _) as r when (Queries.LS.cardinal r) = 1 ->
-           let lval = Lval.CilLval.to_lval (Queries.LS.choose r) in
+         | a when not (Queries.LS.is_top a || Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && (Queries.LS.cardinal a) = 1 ->
+           let lval = Lval.CilLval.to_lval (Queries.LS.choose a) in
            Lval lval
          (* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
          (* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)

After fixing that, a TypeOfError appears because when responding to EvalInt queries, the apron analysis tries to get the ikind (through the type) of the expression, but that fails for our wonderful alloc variables that have void type, but may have offsets on them, e.g. (alloc@sid:138)#in[(int )"unknown"].

[sim642]

Ok, this goes deep, but I think I've managed to fix all the following crashes. I'll just go ahead and commit my fixes to this branch.