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.

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

Better property handling #10

Merged
merged 15 commits into from
Jan 29, 2024
Merged

Better property handling #10

merged 15 commits into from
Jan 29, 2024

Conversation

zafer-esen
Copy link
Collaborator

@zafer-esen zafer-esen commented Jan 29, 2024

This is a large PR adding support for checking SV-COMP style properties in TriCera.

Checked properties can now also be toggled, or using the -splitProperties option checked individually in sequence.

Properties to check can be specified using SV-COMP's task definition format, or passed through the command-line interface. Explicit assert statements are always checked, and if no properties are specified, the unreachability of the error function reach_error is checked by default.

Memory safety properties are not checked by default now, which was the case before. See the properties section of TriCera help documentation.

The PR also fixes a few lingering issues and improves on others:

  • Now failing assertions will provide more information on what went wrong (i.e., the violated property).
  • Above also extends into function contracts: if the pre/post-condition of a function is not satisfied, TriCera will point out to the violated property and where the violation happens.
  • Printed solutions sometimes contained errors due to an implementation containing string replacement - this is fixed by eliminating string replacement, which should be much more robust.
  • Fixed the formatting of the help text.

The goal is to refactor assertions so that each one corresponds
to a property. Properties can be toggled - this allowed finer
grained control over which properties TriCera checks. After the
refactor is complete, it should also be clear which property an
input program does not satisfy.
- Added properties package.
- Refactored Main to collect properties from YAML files in a more
  structured way.
- Started refactoring of existing memsafety properties.
Non-heap allocated pointers now throw an error as soon as they
are tried to be freed. They are no longer automatically freed -
this was done for memvalid-track, but that will now be implemented
in another way, so freeing non-heap pointers is no longer
necessary.
Also added regression tests for memvalid-free.
- Adds CLI options for specifying properties.
- Fixes valid-deref properties always being added.
- Formatting of CLI help text.
- Fixes the regression tests based on properties, removing
  redundant ones.
- Fixes a bug where valid-cleanup ghost variable was initialized
  twice.
- Fixes a bug in printing contracts for void functions.
- Makes printing of solutions more robust by replacing
  string replacement with term rewriting.
- Fixes how certain properties are checked.
- It is now possible to check each property separately.
- Updates regression tests.
- Many other changes related to properties.
@zafer-esen zafer-esen merged commit 98736b7 into master Jan 29, 2024
1 check passed
@zafer-esen zafer-esen deleted the properties branch January 29, 2024 19:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant