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

SV-COMP "Memory Safety" benchmark additions #1201

Merged
merged 83 commits into from
Oct 14, 2023
Merged

SV-COMP "Memory Safety" benchmark additions #1201

merged 83 commits into from
Oct 14, 2023

Commits on Sep 6, 2023

  1. Merge remote-tracking branch 'stanimir/mem-oob-analysis' into staging… 

    …_memsafety
    @michael-schwarz
    michael-schwarz committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    0e849e4 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'stanimir/improve-uaf-analysis' into sta… 

    …ging_memsafety
    @michael-schwarz
    michael-schwarz committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    9e430ab View commit details
    Browse the repository at this point in the history

  3. Fix numbering

    @michael-schwarz
    michael-schwarz committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    dac7983 View commit details
    Browse the repository at this point in the history

  4. Set the global SV-COMP analysis state vars at all necessary places

    @mrstanb
    mrstanb committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    b3d9fe1 View commit details
    Browse the repository at this point in the history

  5. Add extra parentheses in witness.ml for memory safety result generation

    @mrstanb
    mrstanb committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    46ae6ee View commit details
    Browse the repository at this point in the history

  6. Add quick and dirty workaround attempt for working with 

    SV-COMP's memory-safety category
    @mrstanb
    mrstanb committed Sep 6, 2023
    2 Configuration menu
    Copy the full SHA
    d4ef555 View commit details
    Browse the repository at this point in the history

  7. Use logical AND and not OR for the memory-safety category in witness

    @mrstanb
    mrstanb committed Sep 6, 2023
    Configuration menu
    Copy the full SHA
    2fb4d74 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2023

  1. Add util function for setting mem safety global vars 

    Make sure to do this only if we're in postsolving
    @mrstanb
    mrstanb committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    9cbf2ab View commit details
    Browse the repository at this point in the history

  2. Don't warn for pointers that only contain strings in their pts

    @mrstanb
    mrstanb committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    3258cce View commit details
    Browse the repository at this point in the history

  3. Set global mem safety flags upon array oob as well

    @mrstanb
    mrstanb committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    0881fb7 View commit details
    Browse the repository at this point in the history

  4. Cast pointer arithmetic offsets without using Option.get

    @mrstanb
    mrstanb committed Sep 9, 2023
    Configuration menu
    Copy the full SHA
    b9faa8f View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2023

  1. Check and warn everywhere for a top points-to set in memOutOfBounds

    @mrstanb
    mrstanb committed Sep 10, 2023
    Configuration menu
    Copy the full SHA
    8a6cf0a View commit details
    Browse the repository at this point in the history

  2. Simplify string address check and remove extra warning

    @mrstanb
    mrstanb committed Sep 10, 2023
    Configuration menu
    Copy the full SHA
    29f13a2 View commit details
    Browse the repository at this point in the history

  3. Add check for dereferencing a pointer containing an unknown address

    @mrstanb
    mrstanb committed Sep 10, 2023
    Configuration menu
    Copy the full SHA
    7bdce29 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2023

  1. Remove unused function

    @mrstanb
    mrstanb committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    3c01418 View commit details
    Browse the repository at this point in the history

  2. Add exception handling for intdom arithmetic in memOutOfBounds

    @mrstanb
    mrstanb committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    15f782b View commit details
    Browse the repository at this point in the history

  3. Ignore info messages for test case 77/05 due to MacOS CI

    @mrstanb
    mrstanb committed Sep 13, 2023
    Configuration menu
    Copy the full SHA
    20433e3 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2023

  1. Merge branch 'master' into staging_memsafety

    @mrstanb
    mrstanb committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    9e59043 View commit details
    Browse the repository at this point in the history

  2. Set SV-COMP memory safety global flags at all necessary locations

    @mrstanb
    mrstanb committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    dee2a60 View commit details
    Browse the repository at this point in the history

  3. Clean up UAF analysis a bit

    @mrstanb
    mrstanb committed Oct 1, 2023
    Configuration menu
    Copy the full SHA
    da45e40 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2023

  1. Recognize mem-safety props in any order

    @mrstanb
    mrstanb committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    1335123 View commit details
    Browse the repository at this point in the history

  2. Add support for SV-COMP's valid-memcleanup property

    @mrstanb
    mrstanb committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    1384f73 View commit details
    Browse the repository at this point in the history

  3. Set SV-COMP global flag for invalid-memcleanup

    @mrstanb
    mrstanb committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    4e70422 View commit details
    Browse the repository at this point in the history

  4. Enable memory safety analyses in autoTune

    @mrstanb
    mrstanb committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    00cc9b5 View commit details
    Browse the repository at this point in the history

  5. Rename UAF tests from number 78 to 74

    @mrstanb
    mrstanb committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    2c8e927 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2023

  1. Fix print for valid-memtrack and valid-memcleanup in autoTune.ml 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Oct 3, 2023
    Configuration menu
    Copy the full SHA
    f872854 View commit details
    Browse the repository at this point in the history

  2. Set ana.malloc.unique_address_count to 1 when activating memLeak … 

    …analysis
    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    edaef42 View commit details
    Browse the repository at this point in the history

  3. Improve some AnalysisState global flag comments

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    7f0b43c View commit details
    Browse the repository at this point in the history

  4. Clean up some commented out code

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    a975702 View commit details
    Browse the repository at this point in the history

  5. Set ana.malloc.unique_address_count to 1 only if it's not already… 

    … set to a value >= 1
    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    b26010a View commit details
    Browse the repository at this point in the history

  6. Add a valid-memcleanup.prp file

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    89d68af View commit details
    Browse the repository at this point in the history

  7. Comment out reachability filter in useAfterFree's enter

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    171ba57 View commit details
    Browse the repository at this point in the history

  8. Fix wrong callee_state in enter

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    4a1c038 View commit details
    Browse the repository at this point in the history

  9. Add test case for UAF in callee through a global var

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    bb2091e View commit details
    Browse the repository at this point in the history

  10. Fix typo for warning about top address offsets

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    fb4ad24 View commit details
    Browse the repository at this point in the history

  11. Add test case with invalid deref in complex loop

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    9d64db1 View commit details
    Browse the repository at this point in the history

  12. Disable info messages which confuse make test in 77/10

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    1afac02 View commit details
    Browse the repository at this point in the history

  13. Add option for enabling the marking of variables as pulled out of scope

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    f5c197e View commit details
    Browse the repository at this point in the history

  14. Warn for accesses to variables pulled out of scope

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    003b814 View commit details
    Browse the repository at this point in the history

  15. Automatically set cil.addNestedScopeAttr in autoTune when running `… 

    …memOutOfBounds`
    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    ac7dd71 View commit details
    Browse the repository at this point in the history

  16. Bump goblint-cil

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    c95a846 View commit details
    Browse the repository at this point in the history

  17. Merge branch 'master' into svcomp-memsafety-benchmarks

    @mrstanb
    mrstanb authored Oct 3, 2023
    Configuration menu
    Copy the full SHA
    500a444 View commit details
    Browse the repository at this point in the history

  18. set also for meta property

    @michael-schwarz
    michael-schwarz committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    c9a846b View commit details
    Browse the repository at this point in the history

  19. Fix address offset calculation in memOutOfBounds

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    9efae6f View commit details
    Browse the repository at this point in the history

  20. Adapt 77/10 test case to correctly account for address offsets

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    dcc3d5c View commit details
    Browse the repository at this point in the history

  21. Add further test case to check address offset calculation in `memOutO… 

    …fBounds`
    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    a64e9c3 View commit details
    Browse the repository at this point in the history

  22. Set ana.malloc.unique_address_count for MemorySafety as well

    @mrstanb
    mrstanb committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    44476ce View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2023

  1. Move cil.addNestedScopeAttr setting to init_options

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    e052544 View commit details
    Browse the repository at this point in the history

  2. Try with cil.addNestedScopeAttr always set to true

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    3341470 View commit details
    Browse the repository at this point in the history

  3. Use rand() in 77/10

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    1211a9f View commit details
    Browse the repository at this point in the history

  4. Activate cil.addNestedScopeAttr in cilfacade only conditionally

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    2039675 View commit details
    Browse the repository at this point in the history

  5. Activate SV-COMP memory-safety-related options before CIL has complet… 

    …ely parsed the program
    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    fb4979b View commit details
    Browse the repository at this point in the history

  6. Fix again scoping check

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    1eb7309 View commit details
    Browse the repository at this point in the history

  7. Fix conditional enabling of cil.addNestedScopeAttr

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    4a4b6ab View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into svcomp-memsafety-benchmarks

    @mrstanb
    mrstanb authored Oct 4, 2023
    Configuration menu
    Copy the full SHA
    ead8976 View commit details
    Browse the repository at this point in the history

  9. Warn for invalid deallocation when encountering invalid addresses

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    395c30d View commit details
    Browse the repository at this point in the history

  10. Add invalid address test case for invalid deallocation

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    055d9cc View commit details
    Browse the repository at this point in the history

  11. Warn if lval contains an address with a non-local var

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    2c883eb View commit details
    Browse the repository at this point in the history

  12. Don't warn for non-local vars in address set if they're globals

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    5cb10f6 View commit details
    Browse the repository at this point in the history

  13. Add test cases for invalid deref due to scoping

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    ea4410d View commit details
    Browse the repository at this point in the history

  14. Slightly refactor check_count and check for src's size in memcpy

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    6745d79 View commit details
    Browse the repository at this point in the history

  15. Add test case with wrong src size for memcpy

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    136bec0 View commit details
    Browse the repository at this point in the history

  16. Correct test 77/07 to warn for src OOB access in memcpy as well

    @mrstanb
    mrstanb committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    3a2fe3f View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2023

  1. Set dest in memcpy to top if n doesn't match its size

    @mrstanb
    mrstanb committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    9b728d3 View commit details
    Browse the repository at this point in the history

  2. Add test case for UAF due to bad memcpy

    @mrstanb
    mrstanb committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    48f2cfe View commit details
    Browse the repository at this point in the history

  3. Check offsets of dereferenced lvalues as well

    @mrstanb
    mrstanb committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    753b5c1 View commit details
    Browse the repository at this point in the history

  4. Add regr. test case for OOB due to too large lval offset

    @mrstanb
    mrstanb committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    d683281 View commit details
    Browse the repository at this point in the history

  5. Fix exceptions due to ID ops

    @mrstanb
    mrstanb committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    22e4df5 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2023

  1. Fix size check in memory_copying 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    b9c2134 View commit details
    Browse the repository at this point in the history

  2. Use Option.map_default instead of match 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    625e90b View commit details
    Browse the repository at this point in the history

  3. Use _ in place of unused offset in lambda 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    fbab25e View commit details
    Browse the repository at this point in the history

  4. Set Cabs2cil.addNestedScopeAttr based on the Goblint config option 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    91aeee7 View commit details
    Browse the repository at this point in the history

  5. Remove extra semicolon

    @mrstanb
    mrstanb committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    992e5c0 View commit details
    Browse the repository at this point in the history

  6. Use Option.default in place of Option.value

    @mrstanb
    mrstanb committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    cc351e0 View commit details
    Browse the repository at this point in the history

  7. Use AD.exists to warn about non-local vars in address set instead o… 

    …f using `AD.iter`
    @mrstanb
    mrstanb committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    de0220b View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2023

  1. Remove unnecessary pin 

    Co-authored-by: Simmo Saan <[email protected]>
    @mrstanb @sim642
    mrstanb and sim642 authored Oct 11, 2023
    Configuration menu
    Copy the full SHA
    e98911d View commit details
    Browse the repository at this point in the history

  2. Remove commented out code from enter in UAF analysis 

    Add TODOs for future improvement there
    @mrstanb
    mrstanb committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    072f99d View commit details
    Browse the repository at this point in the history

  3. Remove unnecessary stuff from test case 74/15 

    Co-authored-by: Simmo Saan <[email protected]>
    @mrstanb @sim642
    mrstanb and sim642 authored Oct 11, 2023
    Configuration menu
    Copy the full SHA
    e339ed1 View commit details
    Browse the repository at this point in the history

  4. Reduce duplication

    @michael-schwarz
    michael-schwarz committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    f018ea3 View commit details
    Browse the repository at this point in the history

  5. Reorganize memsafety regr. tests

    @mrstanb
    mrstanb committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    a2f36fb View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into svcomp-memsafety-benchmarks

    @mrstanb
    mrstanb committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    33e69af View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2023

  1. Merge branch 'master' into svcomp-memsafety-benchmarks

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    7fad157 View commit details
    Browse the repository at this point in the history

  2. Activate cil.addNestedScopeAttr when memOutOfBounds analysis is a… 

    …ctive
    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    910a11f View commit details
    Browse the repository at this point in the history