Skip to content
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

Jump to bottom

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

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

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

wants to merge 98 commits into from

Commits on Mar 13, 2024

  1. Add reach_error to library functions

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    9ee9ce7 View commit details
    Browse the repository at this point in the history

  2. Make some YAML witness validation messages more severe

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    4752ddf View commit details
    Browse the repository at this point in the history

  3. Add ghost_variable and ghost_update to YAML witness types

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    2e22af7 View commit details
    Browse the repository at this point in the history

  4. Add mutexGhosts analysis

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    688c4dc View commit details
    Browse the repository at this point in the history

  5. Add YamlEntryGlobal query

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    45be164 View commit details
    Browse the repository at this point in the history

  6. Generate YAML witness ghosts for mutexes

    @sim642
    sim642 committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    5d3f5fe View commit details
    Browse the repository at this point in the history

Commits on Mar 14, 2024

  1. Make protection privatization more precise with earlyglobs

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    a80242a View commit details
    Browse the repository at this point in the history

  2. Add ask argument to BasePriv invariant_global-s

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    086e60d View commit details
    Browse the repository at this point in the history

  3. Add MustProtectingLocks query

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    b2d09da View commit details
    Browse the repository at this point in the history

  4. Generate protected flow-insensitive invariants with ghosts

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    526d88a View commit details
    Browse the repository at this point in the history

  5. Make mutex ghost variable names distinct from mutex variables

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    d536db4 View commit details
    Browse the repository at this point in the history

  6. Document MutexGhosts

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    2eafa69 View commit details
    Browse the repository at this point in the history

  7. Fix coverage build

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    470ddbc View commit details
    Browse the repository at this point in the history

  8. Make mutex-meet privatization more precise with earlyglobs

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    0d5ef63 View commit details
    Browse the repository at this point in the history

  9. Generate mutex-meet flow-insensitive invariants with ghosts

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    a714dc6 View commit details
    Browse the repository at this point in the history

  10. Add ghost variable for multithreaded mode

    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    652aeae View commit details
    Browse the repository at this point in the history

  11. Reorder disjuncts in privatized invariants in implication order 

    This also means that the global variable is (lazily) not accessed when the condition isn't met.
    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    7c33c72 View commit details
    Browse the repository at this point in the history

  12. Fix MustProtectingLocks query crash with top 

    Happened on 13-privatized/01-priv_nr
    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    4381e9f View commit details
    Browse the repository at this point in the history

  13. Fix protection privatization protected invariant with no protecting m… 

    …utexes

Happened on 13-privatized/02-priv_rc.
    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    60a51b9 View commit details
    Browse the repository at this point in the history

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

    …utexes

Happened on 13-privatized/02-priv_rc.
    @sim642
    sim642 committed Mar 14, 2024
    Configuration menu
    Copy the full SHA
    fd84cd9 View commit details
    Browse the repository at this point in the history

Commits on Mar 15, 2024

  1. Use RichVarinfo for witness ghost variables

    @sim642
    sim642 committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    516e3ad View commit details
    Browse the repository at this point in the history

  2. Deduplicate witness ghost entry creation

    @sim642
    sim642 committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    a10c973 View commit details
    Browse the repository at this point in the history

  3. Allow non-void types for RichVarinfo

    @sim642
    sim642 committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    932ac3b View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

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

    @sim642
    sim642 committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    7951588 View commit details
    Browse the repository at this point in the history

  2. Add cram test for privatized witness ghosts

    @sim642
    sim642 committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    b018265 View commit details
    Browse the repository at this point in the history

  3. Add cram test for witness ghosts with multiple protecting locks

    @sim642
    sim642 committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    7992462 View commit details
    Browse the repository at this point in the history

  4. mutex-meet ghost invariants are maybe unsound

    @sim642
    sim642 committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    01c9b98 View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2024

  1. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    a07e890 View commit details
    Browse the repository at this point in the history

  2. Add NOWARNs to commented out checks in 56-witness/64-ghost-multiple-p… 

    …rotecting
    @sim642
    sim642 committed Apr 4, 2024
    Configuration menu
    Copy the full SHA
    d3a5a0a View commit details
    Browse the repository at this point in the history

Commits on Apr 15, 2024

  1. Remove TODO about mutex-meet unsound witness invariants

    @sim642
    sim642 committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    612c1cc View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    ff0d6a5 View commit details
    Browse the repository at this point in the history

  3. Rewrite mutexGhosts with may locksets per node 

    This makes 56-witness/65-ghost-ambiguous-lock have sensible ghost updates.
    @sim642
    sim642 committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    e235ba7 View commit details
    Browse the repository at this point in the history

  4. Add test for mutex ghosts for alloc variables

    @sim642
    sim642 committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    726f646 View commit details
    Browse the repository at this point in the history

  5. Add valid names to alloc mutex ghosts

    @sim642
    sim642 committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    3e9d7c3 View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2024

  1. Fix mutexGhosts indentation

    @sim642
    sim642 committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    b19cc2d View commit details
    Browse the repository at this point in the history

  2. Use non-recursive mutex in 56-witness/66-ghost-alloc-lock 

    This fixes unlock ghost update locations.
    @sim642
    sim642 committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    885d0cf View commit details
    Browse the repository at this point in the history

  3. Fix mutexGhosts unlocking everything at function return

    @sim642
    sim642 committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    21ae83a View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2024

  1. Revert "Rewrite mutexGhosts with may locksets per node" 

    This partially reverts commits e235ba7 and 21ae83a.
    @sim642
    sim642 committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    d67c083 View commit details
    Browse the repository at this point in the history

  2. Add lock global unknowns to mutexGhosts

    @sim642
    sim642 committed Apr 18, 2024
    Configuration menu
    Copy the full SHA
    c472adf View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2024

  1. Add PARAM to 56-witness/64-ghost-multiple-protecting

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    fd64898 View commit details
    Browse the repository at this point in the history

  2. Find ambiguous mutexes in mutexGhosts

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    e3ded4e View commit details
    Browse the repository at this point in the history

  3. Avoid emitting witness ghosts for ambiguous mutexes

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    b96f8a2 View commit details
    Browse the repository at this point in the history

  4. Move LockDomain.Symbolic to SymbLocksDomain

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    c6f12a6 View commit details
    Browse the repository at this point in the history

  5. Extract WitnessGhostVar to break dependency cycle

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    8985d64 View commit details
    Browse the repository at this point in the history

  6. Refactor GhostVarAvailable query

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    b04af51 View commit details
    Browse the repository at this point in the history

  7. Exclude WitnessGhostVar from docs check

    @sim642
    sim642 committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    d8bd13d View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2024

  1. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Apr 22, 2024
    Configuration menu
    Copy the full SHA
    6750c7c View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2024

  1. Fix __VERIFIER_atomic special mutex ghost varialbe name

    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    947d6bc View commit details
    Browse the repository at this point in the history

  2. Avoid emitting useless protected invariants from protection privatiza… 

    …tion
    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    4ada6eb View commit details
    Browse the repository at this point in the history

  3. Avoid useless work in mutex-meet invariant_global if ghost variable i… 

    …sn't available
    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    a7d43a9 View commit details
    Browse the repository at this point in the history

  4. Fix struct field mutex ghost variable name

    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    d6abc0b View commit details
    Browse the repository at this point in the history

  5. Fix definite array index mutex ghost variable name

    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    6db1d04 View commit details
    Browse the repository at this point in the history

  6. Make non-definite ghost variables unavailable

    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    53a714f View commit details
    Browse the repository at this point in the history

  7. Disable mutex ghosts with indices

    @sim642
    sim642 committed Apr 23, 2024
    Configuration menu
    Copy the full SHA
    413b2e1 View commit details
    Browse the repository at this point in the history

Commits on Apr 24, 2024

  1. Detect thread create nodes in mutexGhosts

    @sim642
    sim642 committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    ea849fb View commit details
    Browse the repository at this point in the history

  2. Refactor mutexGhosts thread creation collection

    @sim642
    sim642 committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    594beac View commit details
    Browse the repository at this point in the history

  3. Add option to emit flow_insensitive_invariant-s as location_invariant-s

    @sim642
    sim642 committed Apr 24, 2024
    Configuration menu
    Copy the full SHA
    584b788 View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2024

  1. Add svcomp-ghost conf

    @sim642
    sim642 committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    8d5cc12 View commit details
    Browse the repository at this point in the history

  2. Use YAML witness format-version 0.1 for svcomp-ghost

    @sim642
    sim642 committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    96d862e View commit details
    Browse the repository at this point in the history

  3. Test witness.invariant.flow_insensitive-as-location with for loop

    @sim642
    sim642 committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    257fa8c View commit details
    Browse the repository at this point in the history

  4. Fix witness.invariant.flow_insensitive-as-location at loop node

    @sim642
    sim642 committed Apr 25, 2024
    Configuration menu
    Copy the full SHA
    10dfba1 View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2024

  1. Add cram test for relational mutex-meet flow-insensitive invariants

    @sim642
    sim642 committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    16c97fd View commit details
    Browse the repository at this point in the history

  2. Add InvariantGlobal interface to relational privatizations

    @sim642
    sim642 committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    5650784 View commit details
    Browse the repository at this point in the history

  3. Implement relational mutex-meet flow-insensitive invariants

    @sim642
    sim642 committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    d3565cb View commit details
    Browse the repository at this point in the history

  4. Filter relational mutex-meet ghost invariant with keep_only_protected… 

    …_globals

lock does it too, so let's be safe.
    @sim642
    sim642 committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    1aa35d8 View commit details
    Browse the repository at this point in the history

  5. Add filters to relational InvariantGlobal

    @sim642
    sim642 committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    c4a8936 View commit details
    Browse the repository at this point in the history

Commits on May 7, 2024

  1. Add test with __VERIFIER_atomic_locked ghost variable

    @sim642
    sim642 committed May 7, 2024
    Configuration menu
    Copy the full SHA
    535de76 View commit details
    Browse the repository at this point in the history

  2. Treat __VERIFIER_atomic_locked as false in witnesses 

    Others cannot observe anything else anyway.
But in the atomic section could?!
    @sim642
    sim642 committed May 7, 2024
    Configuration menu
    Copy the full SHA
    6f3b6fb View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed May 7, 2024
    Configuration menu
    Copy the full SHA
    2e26aab View commit details
    Browse the repository at this point in the history

Commits on May 8, 2024

  1. Disable 13-privatized/04-priv_multi cram test on OSX 

    OSX has its own weird diff.
    @sim642
    sim642 committed May 8, 2024
    Configuration menu
    Copy the full SHA
    2e6673f View commit details
    Browse the repository at this point in the history

  2. Make 36-apron/12-traces-min-rpb1 cram test warnings deterministic 

    Needed for OSX CI to pass.
    @sim642
    sim642 committed May 8, 2024
    Configuration menu
    Copy the full SHA
    b7582a4 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2024

  1. Add BasePriv invariant_global tracing

    @sim642
    sim642 committed May 20, 2024
    Configuration menu
    Copy the full SHA
    cad5f6e View commit details
    Browse the repository at this point in the history

Commits on May 21, 2024

  1. Fix mutex-meet invariant_global not including MUTEX_INITS

    @sim642
    sim642 committed May 21, 2024
    Configuration menu
    Copy the full SHA
    bd329e1 View commit details
    Browse the repository at this point in the history

Commits on Jun 4, 2024

  1. Add comment about multiple protecting mutexes for ghost invariants

    @sim642
    sim642 committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    2a79e42 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    e6bf34d View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2024

  1. Add ghost_variable and ghost_update YAML entry types to option

    @sim642
    sim642 committed Jun 5, 2024
    Configuration menu
    Copy the full SHA
    2e42c7b View commit details
    Browse the repository at this point in the history

  2. Make InvariantGlobalNodes query lazy in YAML witness generation

    @sim642
    sim642 committed Jun 5, 2024
    Configuration menu
    Copy the full SHA
    e7931ff View commit details
    Browse the repository at this point in the history

  3. Fix comment about YamlEntryGlobal

    @sim642
    sim642 committed Jun 5, 2024
    Configuration menu
    Copy the full SHA
    36ff621 View commit details
    Browse the repository at this point in the history

Commits on Jun 18, 2024

  1. Handle pthread_rwlock_t as opaque mutex in base analysis 

    Avoids unsound rwlock struct content invariants in witnesses.
    @sim642
    sim642 committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    7fcb10c View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2024

  1. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    1570adb View commit details
    Browse the repository at this point in the history

  2. Remove pthreadMutexType from ghost witness tests 

    It is now enabled by default and default mutex type is assumed non-recursive now.
    @sim642
    sim642 committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    c18061e View commit details
    Browse the repository at this point in the history

  3. Activate abortUnless in svcomp-ghost conf also

    @sim642
    sim642 committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    6055e8d View commit details
    Browse the repository at this point in the history

  4. Update TODO comment about base earlyglobs flow-insensitive invariants

    @sim642
    sim642 committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    6e79314 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2024

  1. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    13333f5 View commit details
    Browse the repository at this point in the history

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

    @sim642
    sim642 committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    d937d68 View commit details
    Browse the repository at this point in the history

  3. Add option ana.var_eq.invariant.enabled

    @sim642
    sim642 committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    fbc9e62 View commit details
    Browse the repository at this point in the history

  4. Update svcomp-ghost conf

    @sim642
    sim642 committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    58aaf53 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    641d447 View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2024

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

    …r flow-insensitive location invariants to work
    @sim642
    sim642 committed Aug 8, 2024
    Configuration menu
    Copy the full SHA
    f20ed62 View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2024

  1. Merge branch 'master' into yaml-witness-ghost

    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    342ed74 View commit details
    Browse the repository at this point in the history

  2. Add YAML witness ghost_instrumentation entry type

    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    9c60418 View commit details
    Browse the repository at this point in the history

  3. Add ghost_instrumentation support to mutexGhosts

    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    d220653 View commit details
    Browse the repository at this point in the history

  4. Add option for emitting flow_insensitive_invariant-s as invariant_set… 

    … location_invariant-s in YAML witnesses
    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    f79ad18 View commit details
    Browse the repository at this point in the history

  5. Use invariant_set in svcomp-ghost conf

    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    e9e652d View commit details
    Browse the repository at this point in the history

  6. Make invariant_set and ghost_instrumentation deterministic in tests

    @sim642
    sim642 committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    431b34d View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. Remove ghost_ prefix from ghost_instrumentation update entries

    @sim642
    sim642 committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    2c99550 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2024

  1. Wrap ghost_instrumentation in content

    @sim642
    sim642 committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    12dadf4 View commit details
    Browse the repository at this point in the history

  2. Add value and format to ghost_instrumentation

    @sim642
    sim642 committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    852297b View commit details
    Browse the repository at this point in the history