Generate flow-insensitive YAML witness invariants with ghosts for privatized variables #1394

sim642 · 2024-03-14T10:20:14Z

This is a quick implementation of the idea we had a long time ago for exporting our protected invariants into YAML witnesses with ghosts.

protection privatization

For the Freiburg mutex.c example, we essentially generate the same witness with ghosts as the example:

A ghost variable m_locked is declared and updated to match lock and unlock operations of the mutex m.
A flow-insensitive invariant used == 0 || m_locked is generated using the ghost variable.

This is still our special flow_insensitive_invariant because there's the question where one would place the location_invariant when our result in fact holds at every point.

Currently tested only manually with:

./goblint ~/Documents/concurrency-witnesses/examples/VEWIT2023/mutex.c --enable ana.sv-comp.functions --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE" --html --set ana.activated[+] mutexGhosts --enable witness.yaml.enabled --set witness.yaml.entry-types[+] flow_insensitive_invariant

mutex-meet privatization

For this example, the result is the same, but one invariant is generated per-mutex with a conjunction for all the protected variables. Also for the relational privatization.

TODO

This also means that the global variable is (lazily) not accessed when the condition isn't met.

Happened on 13-privatized/01-priv_nr

…utexes Happened on 13-privatized/02-priv_rc.

Avoids unsound rwlock struct content invariants in witnesses.

tests/regression/13-privatized/74-mutex.c

src/witness/witnessGhostVar.ml

michael-schwarz · 2024-07-30T11:53:09Z

src/witness/yamlWitness.ml

                  let invs = WitnessUtil.InvariantExp.process_exp inv in
                  List.fold_left (fun acc inv ->
                      let invariant = Entry.invariant (CilType.Exp.show inv) in
                      let entry = Entry.flow_insensitive_invariant ~task ~invariant in
                      entry :: acc
                    ) acc invs
-                | `Bot | `Top -> (* global bot might only be possible for alloc variables, if at all, so emit nothing *)
+                | `Lifted inv, true ->
+                  (* TODO: or do at location_invariant loop for each node and query if should also do global invariants there? *)


What happened with this TODO?

It would be possible to do this without the InvariantGlobalNodes query by querying InvariantGlobal for each location_invariant location. It might be more confusing though (the same query can be made both globally or locally) and possibly less efficient (although that might depend on how many nodes InvariantGlobalNodes returns and how big the invariants are).

michael-schwarz · 2024-07-30T11:56:02Z

src/analyses/basePriv.ml

+      else if VD.equal (getg (V.protected g')) (getg (V.unprotected g')) then
+        Invariant.none (* don't output protected invariant because it's the same as unprotected *)
+      else (
+        let inv = ValueDomain.invariant_global (fun g -> getg (V.protected g)) g' in (* TODO: this takes protected values of everything *)


What's up with this TODO?

The problem here is that it can be unsound I think. If a global pointer is protected but what it points to isn't, then this invariant will assume both are protected.
Surprisingly, Ultimate hasn't found any of such to be wrong. Maybe because if the pointee is jointly protected, then it's fine again?

We cannot just delegate to read_global here because this is in flow-sensitive context, so there's no notion of current lockset, etc.

michael-schwarz · 2024-07-30T11:56:37Z

src/analyses/basePriv.ml

+        (* Very conservative about multiple (write-)protecting mutexes: invariant is not claimed when any of them is held.
+           It should be possible to be more precise because writes only happen with all of them held,
+           but conjunction is unsound when one of the mutexes is temporarily unlocked.
+           Hypothetical read-protection is also somehow relevant. *)


What does this sentence mean?

We decided not to come up with more precise invariants here, so it's hard to say anything more precisely about it. Simply that read-protection also plays into it (if nobody reads it with fewer locks then we can claim a stronger invariant, kind of like the protection-read privatization).

michael-schwarz · 2024-07-30T11:58:18Z

src/analyses/basePriv.ml

@@ -250,7 +250,7 @@ struct

  let invariant_global ask getg = function
    | `Right g' -> (* global *)
-      ValueDomain.invariant_global (read_unprotected_global getg) g'
+      ValueDomain.invariant_global (read_unprotected_global getg) g' (* TODO: disjunct with mutex_inits instead of join? *)


What's the plan with this?

Using duplicate versions of read_unprotected_global and get_mutex_global_x_with_mutex_inits which operate on invariant expressions rather than ValueDomain, we could make these invariants maybe more precise.

I just don't know if it's worth it though. Currently the logic is shared with the usual read_global used by the analysis. Duplicating would require them to be maintained in sync.

michael-schwarz · 2024-07-30T12:03:40Z

src/analyses/basePriv.ml

+      if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then
+        sideg V.mutex_inits side_cpa (* Also side to inits because with earlyglobs enter_multithreaded does not side everything to inits *)
+        (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write. *)


Why is this needed and what effect does it have?

Did you check whether this causes any precision regressions?

Without it

goblint --enable ana.sv-comp.functions --set ana.base.privatization mutex-meet --enable exp.earlyglobs 74-mutex.c

does not pass because the variable will be missing from mutex_inits, so we'll read bottom from the map and turn it into top I think. So this is actually to increase precision with earlyglobs.

A similar thing is already in protection privatization. I think we never really tested mutex-meet with earlyglobs.

src/analyses/base.ml

michael-schwarz · 2024-07-30T12:08:30Z

src/analyses/apron/relationPriv.apron.ml

+      else
+        Invariant.none
+    | g -> (* global *)
+      Invariant.none (* TODO: ? *)


It would be possible to emit unprotected invariants from relational mutex-meet, but these will be inherently non-relational, so this might be rather useless.

It is now enabled by default and default mutex type is assumed non-recursive now.

…r flow-insensitive location invariants to work

… location_invariant-s in YAML witnesses

sim642 added 11 commits March 13, 2024 15:31

Add reach_error to library functions

9ee9ce7

Make some YAML witness validation messages more severe

4752ddf

Add ghost_variable and ghost_update to YAML witness types

2e22af7

Add mutexGhosts analysis

688c4dc

Add YamlEntryGlobal query

45be164

Generate YAML witness ghosts for mutexes

5d3f5fe

Make protection privatization more precise with earlyglobs

a80242a

Add ask argument to BasePriv invariant_global-s

086e60d

Add MustProtectingLocks query

b2d09da

Generate protected flow-insensitive invariants with ghosts

526d88a

Make mutex ghost variable names distinct from mutex variables

d536db4

sim642 added feature sv-comp SV-COMP (analyses, results), witnesses labels Mar 14, 2024

sim642 self-assigned this Mar 14, 2024

sim642 added 12 commits March 14, 2024 12:26

Document MutexGhosts

2eafa69

Fix coverage build

470ddbc

Make mutex-meet privatization more precise with earlyglobs

0d5ef63

Generate mutex-meet flow-insensitive invariants with ghosts

a714dc6

Add ghost variable for multithreaded mode

652aeae

Reorder disjuncts in privatized invariants in implication order

7c33c72

This also means that the global variable is (lazily) not accessed when the condition isn't met.

Fix MustProtectingLocks query crash with top

4381e9f

Happened on 13-privatized/01-priv_nr

Fix protection privatization protected invariant with no protecting m…

60a51b9

…utexes Happened on 13-privatized/02-priv_rc.

Fix mutex-meet privatization protected invariant with no protecting m…

fd84cd9

…utexes Happened on 13-privatized/02-priv_rc.

Use RichVarinfo for witness ghost variables

516e3ad

Deduplicate witness ghost entry creation

a10c973

Allow non-void types for RichVarinfo

932ac3b

sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Mar 18, 2024

sim642 mentioned this pull request Apr 2, 2024

Change YAML witness columns to 1-indexed #1400

Merged

1 task

Merge branch 'yaml-witness-test' into yaml-witness-ghost

7951588

sim642 force-pushed the yaml-witness-ghost branch from 5694838 to 7951588 Compare April 2, 2024 08:53

sim642 added 4 commits June 4, 2024 10:45

Add comment about multiple protecting mutexes for ghost invariants

2a79e42

Merge branch 'master' into yaml-witness-ghost

e6bf34d

Add ghost_variable and ghost_update YAML entry types to option

2e42c7b

Make InvariantGlobalNodes query lazy in YAML witness generation

e7931ff

sim642 marked this pull request as ready for review June 5, 2024 10:04

sim642 added 2 commits June 5, 2024 13:46

Fix comment about YamlEntryGlobal

36ff621

Handle pthread_rwlock_t as opaque mutex in base analysis

7fcb10c

Avoids unsound rwlock struct content invariants in witnesses.

jerhard requested review from jerhard and michael-schwarz July 30, 2024 11:44

michael-schwarz reviewed Jul 30, 2024

View reviewed changes

sim642 added 4 commits July 31, 2024 11:14

Merge branch 'master' into yaml-witness-ghost

1570adb

Remove pthreadMutexType from ghost witness tests

c18061e

It is now enabled by default and default mutex type is assumed non-recursive now.

Activate abortUnless in svcomp-ghost conf also

6055e8d

Update TODO comment about base earlyglobs flow-insensitive invariants

6e79314

sim642 added this to the v2.5.0 milestone Jul 31, 2024

sim642 added 15 commits August 7, 2024 11:18

Merge branch 'master' into yaml-witness-ghost

13333f5

Add options ana.base.invariant.local and ana.base.invariant.global

d937d68

Add option ana.var_eq.invariant.enabled

fbc9e62

Update svcomp-ghost conf

58aaf53

Merge branch 'master' into yaml-witness-ghost

641d447

Re-enable witness.invariant.{loop-head,other} in svcomp-ghost conf fo…

f20ed62

…r flow-insensitive location invariants to work

Merge branch 'master' into yaml-witness-ghost

342ed74

Add YAML witness ghost_instrumentation entry type

9c60418

Add ghost_instrumentation support to mutexGhosts

d220653

Add option for emitting flow_insensitive_invariant-s as invariant_set…

f79ad18

… location_invariant-s in YAML witnesses

Use invariant_set in svcomp-ghost conf

e9e652d

Make invariant_set and ghost_instrumentation deterministic in tests

431b34d

Remove ghost_ prefix from ghost_instrumentation update entries

2c99550

Wrap ghost_instrumentation in content

12dadf4

Add value and format to ghost_instrumentation

852297b

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generate flow-insensitive YAML witness invariants with ghosts for privatized variables #1394

Generate flow-insensitive YAML witness invariants with ghosts for privatized variables #1394

sim642 commented Mar 14, 2024 •

edited

Loading

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

michael-schwarz Jul 30, 2024

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

sim642 Jul 31, 2024

michael-schwarz Jul 30, 2024

sim642 Jul 31, 2024

Generate flow-insensitive YAML witness invariants with ghosts for privatized variables #1394

Are you sure you want to change the base?

Generate flow-insensitive YAML witness invariants with ghosts for privatized variables #1394

Conversation

sim642 commented Mar 14, 2024 • edited Loading

protection privatization

mutex-meet privatization

TODO

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sim642 commented Mar 14, 2024 •

edited

Loading