Skip to content

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

Merged
sim642 merged 41 commits intomasterfrom
apron_track_address
Jun 23, 2022
Merged

Apron: Track relational information for variables that have their address taken#742
sim642 merged 41 commits intomasterfrom
apron_track_address

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented May 22, 2022 •
edited
Loading

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 michael-schwarz changed the title Apron: Track relational information that have their address taken Apron: Track relational information for variables that have their address taken May 22, 2022
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented May 22, 2022

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
sim642 reviewed May 23, 2022
View reviewed changes
@sim642
Copy link
Copy Markdown
Member

sim642 commented May 23, 2022

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
Copy link
Copy Markdown
Member

sim642 commented May 25, 2022

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.

@michael-schwarz @sim642
Normalize whitespace
ea41437 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@sim642 sim642 mentioned this pull request Jun 13, 2022
Merged
@michael-schwarz michael-schwarz requested a review from sim642 June 21, 2022 16:17
sim642
sim642 reviewed Jun 22, 2022
View reviewed changes
src/analyses/apron/apronAnalysis.apron.ml Outdated
let vname = Var.to_string var in
match List.find_opt (fun v -> v.vname = vname) (fundec.sformals @ fundec.slocals) with
| None -> true
| Some v -> Queries.LS.exists (fun (v',_) -> v'.vid = v.vid) reachable_from_args
Copy link
Copy Markdown
Member

@sim642 sim642 Jun 22, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Copy Markdown
Member

sim642 commented Jun 22, 2022

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
Copy link
Copy Markdown
Member Author

michael-schwarz commented Jun 22, 2022

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
Copy link
Copy Markdown
Member

sim642 commented Jun 22, 2022

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
Copy link
Copy Markdown
Member

sim642 commented Jun 22, 2022

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.

sim642
sim642 reviewed Jun 22, 2022
View reviewed changes
@sim642 sim642 merged commit 57850dc into master Jun 23, 2022
@sim642 sim642 deleted the apron_track_address branch June 23, 2022 10:01
sim642 added a commit that referenced this pull request Jun 23, 2022
@sim642
Fix ApronAnalysis indentation (PR #742)
cc725c6
@sim642 sim642 mentioned this pull request Jun 23, 2022
Merged
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

feature precision

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

Handle variables that have their addresses taken in Apron

2 participants

@michael-schwarz @sim642