Skip to content

Relational: Use same invalidation strategy as base #1646

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Relational: Use same invalidation strategy as base #1646

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
508d7e2
Use same invalidation strategy as base (References #1535)
michael-schwarz Jul 6, 2024
406ad22
Make name unique?
michael-schwarz Dec 17, 2024
563a5b1
Support for `threadenter` for unknown function
michael-schwarz Dec 17, 2024
79df614
Merge branch 'master' into issue_1535
michael-schwarz Dec 19, 2024
e03a6f7
Update comment
michael-schwarz Dec 30, 2024
bb534ff
Simplify invalidation
michael-schwarz Dec 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
104 changes: 48 additions & 56 deletions src/analyses/apron/relationAnalysis.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -465,34 +465,22 @@ struct
(* Give the set of reachables from argument. *)
let reachables (ask: Queries.ask) es =
let reachable e st =
match st with
| None -> None
| Some st ->
let ad = ask.f (Queries.ReachableFrom e) in
if Queries.AD.is_top ad then
None
else
Some (Queries.AD.join ad st)
let ad = ask.f (Queries.ReachableFrom e) in
Queries.AD.join ad st
in
List.fold_right reachable es (Some (Queries.AD.empty ()))
List.fold_right reachable es (Queries.AD.empty ())


let forget_reachable man st es =
let ask = Analyses.ask_of_man man in
let rs =
match reachables ask es with
| None ->
(* top reachable, so try to invalidate everything *)
RD.vars st.rel
|> List.filter_map RV.to_cil_varinfo
|> List.map Cil.var
| Some ad ->
let to_cil addr rs =
match addr with
| Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs
| _ -> rs
in
Queries.AD.fold to_cil ad []
let ad = reachables ask es in
let to_cil addr rs =
match addr with
| Queries.AD.Addr.Addr mval -> (ValueDomain.Addr.Mval.to_cil mval) :: rs
| _ -> rs
in
Queries.AD.fold to_cil ad []
in
List.fold_left (fun st lval ->
invalidate_one ask man st lval
Expand All @@ -513,6 +501,36 @@ struct
if RD.is_bot_env res then raise Deadcode;
{st with rel = res}

let special_unknown_invalidate man f args =
(* No warning here, base already prodcues the appropriate warnings *)
let desc = LibraryFunctions.find f in
let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
let deep_addrs =
if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
foldGlobals !Cilfacade.current_file (fun acc global ->
match global with
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
mkAddrOf (Var vi, NoOffset) :: acc
(* TODO: what about GVarDecl? *)
| _ -> acc
) deep_addrs
)
else
deep_addrs
in
let lvallist e =
match man.ask (Queries.MayPointTo e) with
| ad when Queries.AD.is_top ad -> []
| ad ->
Queries.AD.to_mval ad
|> List.map ValueDomain.Addr.Mval.to_cil
in
let st' = forget_reachable man man.local deep_addrs in
let shallow_lvals = List.concat_map lvallist shallow_addrs in
List.fold_left (invalidate_one (Analyses.ask_of_man man) man) st' shallow_lvals


let special man r f args =
let ask = Analyses.ask_of_man man in
let st = man.local in
Expand Down Expand Up @@ -548,31 +566,7 @@ struct
assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
| None -> st)
| _, _ ->
let lvallist e =
match ask.f (Queries.MayPointTo e) with
| ad when Queries.AD.is_top ad -> []
| ad ->
Queries.AD.to_mval ad
|> List.map ValueDomain.Addr.Mval.to_cil
in
let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
let deep_addrs =
if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
foldGlobals !Cilfacade.current_file (fun acc global ->
match global with
| GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
mkAddrOf (Var vi, NoOffset) :: acc
(* TODO: what about GVarDecl? *)
| _ -> acc
) deep_addrs
)
else
deep_addrs
in
let st' = forget_reachable man st deep_addrs in
let shallow_lvals = List.concat_map lvallist shallow_addrs in
let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in
let st' = special_unknown_invalidate man f args in
(* invalidate lval if present *)
match r with
| Some lv -> invalidate_one ask man st' lv
Expand Down Expand Up @@ -674,21 +668,19 @@ struct

let threadenter man ~multiple lval f args =
let st = man.local in
(* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
EnterMultithreaded events only execute after threadenter and threadspawn. *)
if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then
ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st);
Comment on lines +671 to +676
Copy link
Member

Choose a reason for hiding this comment

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

Why is this moved out? Base only does it for non-unknown thread functions.

Copy link
Member Author

Choose a reason for hiding this comment

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

The logic of why it is needed is the same here as it is for the case where a known thread is created: One should not go into multi-threaded mode without notifying the privatization that this switch happened to ensure everything that should be published is published.

Maybe base has some reason this can be avoided, but I'm not really sure why that should be the case. We may want to make an issue to investigate this.

Copy link
Member Author

Choose a reason for hiding this comment

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

Also see the last few comments in #1551

Copy link
Member Author

Choose a reason for hiding this comment

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

#1551 (comment)

Copy link
Member

Choose a reason for hiding this comment

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

The one test in this PR doesn't cover this, does it?

I tried the very simple thing of creating a thread from unknown function pointer and that seems to work with base. That's because threadflag analysis emits the EnterMultiThreaded event which is handled by base (and relational).
The comment for this hack is about the globals values that get used when analyzing the created thread. For an unknown function pointer, there's no thread body to analyze anyway, so it's not clear to me when it would make a difference.

Copy link
Member Author

Choose a reason for hiding this comment

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

The test covers it in some sense. We mean to invalidate e and output

[Info][Imprecise] Invalidating expressions: & e (1.c:11:3-11:35)

But this invalidation does not take and we still claim to be able to prove things about e.

Copy link
Member Author

Choose a reason for hiding this comment

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

Edit: That case is listed in the linked issue.

Copy link
Member

Choose a reason for hiding this comment

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

Do you mean this?

#include<pthread.h>
pthread_mutex_t c;
int d, e, f;

void b(void* arg);

void main(int argc, char *argv) {
  pthread_t t;
  e = pthread_create(&t, 0, b, &f);
  pthread_mutex_lock(&c);
  d++;
  pthread_mutex_unlock(&c);
  pthread_mutex_lock(&c);
}

Where or what are we claiming to prove about e? There aren't any assertions. Can you add it as a test?

I traced sol and sol2 on it and what this changes is that we no longer have -e+2147483647.>=0, e+2147483648.>=0 and all derived octagon constraints from that. But these are just type bounds, so they shouldn't be unsound to begin with.

The point of this PR is to unify logic between base and relation analyses, but this move introduces a new difference. If the old place is really wrong, then we should also fix it in base.
I want to avoid another issue like #1535 down the line where the inconsistency comes up and there's no understanding of why they're different.

Copy link
Member Author

Choose a reason for hiding this comment

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

Sure, I guess I should have linked to this comment: #1551 (comment)

Relying on YAML might make debugging easier. There we get

./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid 1.c --sets exp.relation.prec-dump cluster.prec --html --enable witness.yaml.enabled --set witness.yaml.path 1.yml

./goblint --conf conf/traces-rel.json --set ana.activated[+] threadJoins --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 1.c --set witness.yaml.validate 1.yml

[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )e) + (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )e) + (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )e) - (long long )f >= 0LL (1.c:14:1)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )e) - (long long )f >= 0LL (1.c:14:1)

[Info][Witness] witness validation summary:
confirmed: 32
unconfirmed: 4

The invariants provided here look slightly dubious to me as to whether they actually hold.

These invariants exploit that e is supposedly 0, even thoughe and f have been invalidated.

match Cilfacade.find_varinfo_fundec f with
| fd ->
(* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
EnterMultithreaded events only execute after threadenter and threadspawn. *)
if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then
ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st);
let st' = Priv.threadenter (Analyses.ask_of_man man) man.global st in
let new_rel = make_callee_rel ~thread:true man fd args in
[{st' with rel = new_rel}]
| exception Not_found ->
(* Unknown functions *)
(* TODO: do something like base? *)
failwith "relation.threadenter: unknown function"
[special_unknown_invalidate man f args]

let threadspawn man ~multiple lval f args fman =
man.local
Expand Down
22 changes: 22 additions & 0 deletions tests/regression/46-apron2/98-invalidate-more.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none
#include <pthread.h>
#include <goblint.h>
#include <stdio.h>

int debug;
int other;

int main() {
int top;

// Needed so Base & DefExc doesn't find this information because it invalidates less
if(top) {
debug = 3;
}

fscanf(stdin, "%d", &other);

// Use to fail as debug was invalidated
__goblint_check(debug <= 3);
return 0;
}
Loading