wit4java / wit4java Goto Github PK

View Code? Open in Web Editor NEW

6.0 6.0 0.0 23.14 MB

An execution-based violation-witness validator for Java

License: Other

Python 66.99% Java 33.01%

java python sv-comp validation

wit4java's Introduction

Wit4Java: A Violation-Witness Validator for Java Verifiers

Description

Modern verification tools report a violation witness amidst verification if a bug is encountered. To check the validity of the counterexample wit4java can be used for Java-based verifiers.

The tool employs execution-based validation to assert the violation of a witness. This process involves extracting information on the assumptions of the verifier from the standardised exchange format for violation witnesses and building a test harness to provide a concrete execution of the program. The tool then executes the test harness on the code under verification and can either confirm or reject the violation witness if the relevant assertion is reached.

Literature

Wit4Java: A violation-witness validator for Java verifiers (competition contribution) by Wu, T., Schrammel, P., & Cordeiro, L. C. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham, 2022. Springer doi.org/10.1007/978-3-030-99527-0_36

Usage

usage: wit4java [-h] [--packages [PACKAGE_PATHS [PACKAGE_PATHS ...]]]
                --witness WITNESS_FILE [--version]
                benchmark

Validate a given Java program with a witness conforming to the appropriate SV-COMP exchange format.

positional arguments:
  benchmark             Path to the benchmark directory

optional arguments:
  -h, --help            show this help message and exit
  --packages [PACKAGE_PATHS [PACKAGE_PATHS ...]]
                        Path to the packages used by the benchmark
  --witness WITNESS_FILE
                        Path to the witness file. Must conform to the exchange
                        format
  --version             show program's version number and exit

Authors

Tong Wu (University of Manchester, United Kingdom) [email protected]

Lucas Cordeiro (University of Manchester, United Kingdom) [email protected]

Peter Schrammel (University of Sussex, United Kingdom) [email protected]

Maintainers

Joss Moffatt (University of Manchester, United Kingdom) [email protected]

wit4java's People

Contributors

Stargazers

Watchers

wit4java's Issues

📝 Upgrade README

What needs changing?

Currently, the readme is not very informative and could do with upgrading.
I think adding the following could improve the look of the repository and ease of working with wit4java:

Badges: code quality, licence, etc.
A more informative description of how wit4java works
Link to the existing literature
Usage and Installation

Additional Context

N/A

Update frontend to use argparse

Context

By using argparse we can also allow new flags to be added and will make code easier to develop

Fix Linting Issue

Context

Currently have a collection of linting issues which should not exist for code quality.

🐛 Fix JBMC Floating Point Parsing

Describe the bug
On a floating point assumption JBMC returns the following:

<edge source="202.126" target="206.139">
      <data key="originfile">Main.java</data>
      <data key="startline">12</data>
      <data key="threadId">0</data>
      <data key="assumption">a = 0x1p-111f /* 3.85186e-34 */;</data>
      <data key="assumption.scope">java::Main.main:([Ljava/lang/String;)V</data>
</edge>

To Reproduce
Steps to reproduce the behaviour:

Run wit4java on jdart-regression/float
Output is OK

Expected behaviour
The test harness should make the Main class throw an AssertionError

Screenshots
N/A

Desktop

OS: Ubuntu
Version 3

Additional context
N/A

✨ Regression Tests

Is your feature request related to a problem? Please describe.
Currently no support for regression tests. This would be useful to run on a PR merging as we can concretely verify nothing has broken

Describe the solution you'd like
A test suite to run all/some of the sv-benchmarks.

Describe alternatives you've considered
N/A

Additional context
N/A

🐛 Refactor to remove pylint issues

Describe the bug
Currently, pylint has suggested refactoring certain pieces of code. Before version 3 is released it would be good to fix all of these to have a clean base

To Reproduce
Steps to reproduce the behavior:

Run pylint on files

Expected behaviour
Little to no pylint issues detected.

Additional context
N/A

[Errno 13] Permission denied: '/tmp/tmpl4h4oi65/org/sosy_lab/sv_benchmarks/Verifier.java'

In the sv-comp prerun, all runs return the same error:

[https://sv-comp.sosy-lab.org/2023/results/results-verified/jbmc.2022-11-14_11-01-34.res[…]rt_java.ReachSafety-Java.xml.bz2.merged.xml.bz2.table.html](https://sv-comp.sosy-lab.org/2023/results/results-verified/jbmc.2022-11-14_11-01-34.results.SV-COMP23_assert_java.ReachSafety-Java.xml.bz2.merged.xml.bz2.table.html#/table)

✨ CI/CD Support

Is your feature request related to a problem? Please describe.
Currently, there is no CI/CD support which is a problem as would be useful for on releases we can trigger jobs etc.

Describe the solution you'd like
Using Github Actions the following would be useful:

Have testing pipeline on merge to master
Packaging on release
Zenodo publish on release

Describe alternatives you've considered
Could use other pipelines, however, Github Actions is free and will require less setup.

Additional context
N/A

wit4java / wit4java Goto Github PK

wit4java's Introduction

Wit4Java: A Violation-Witness Validator for Java Verifiers

Description

Literature

Usage

Authors

Maintainers

Links

wit4java's People

Contributors

Stargazers

Watchers

wit4java's Issues

What needs changing?

Additional Context

Context

Context

Recommend Projects

Recommend Topics

Recommend Org