diff --git a/.github/workflows/schema.yml b/.github/workflows/schema.yml new file mode 100644 index 0000000..7ffdb2c --- /dev/null +++ b/.github/workflows/schema.yml @@ -0,0 +1,37 @@ +name: YAML schema + +on: + push: + branches: + - main + +permissions: + contents: read + +jobs: + deploy-html: + runs-on: ubuntu-latest + permissions: + contents: write + + steps: + - uses: actions/checkout@v3 + - name: Set up Python 3.9 + uses: actions/setup-python@v3 + with: + python-version: '3.9' + cache: 'pip' + - name: Install dependencies + run: | + python -m pip install --upgrade pip + pip install -r requirements.txt + - name: Generate schema HTML + run: | + mkdir pages + generate-schema-doc --config-file jsfh.yml witness.schema.json pages/index.html + - name: Deploy to GitHub Pages + uses: peaceiris/actions-gh-pages@v3 + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + publish_dir: pages + destination_dir: yaml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..c0f3a99 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +pages/ +schema_doc* diff --git a/README-YAML.md b/README-YAML.md index c1e6f76..1c687af 100644 --- a/README-YAML.md +++ b/README-YAML.md @@ -27,187 +27,31 @@ Files of verification entries are UTF-8 encoded. Each file of verification entries contains an array of entries. The format of an entry depends on its entry type. -Currently, we have the following entry types: -- `loop_invariant` -- `loop-invariant_certificate` - Entry types are use-case specific and independent. Each producer and consumer of entries can filter those entry types that it supports. -The following sections describe the format of a verification entry for each entry-type. +### Schema +All entry types and their formats are specified using +a [json-schema](http://json-schema.org/): +[witness.schema.json](witness.schema.json). -### Loop Invariant +This schema can be used for documentation generation, validation and code generation. -Loop invariants are important building blocks in software verification. -There are many verification approaches that use loop invariants as lemmata -to construct a proof of correctness. -Verification entries of entry type loop invariant -can be used as verification witness, more specifically, correctness witnesses. +## Examples -In the following, we provide an example, and then a detailed description of the various components. +The schema itself contains some examples. -#### Example +### multivar_1-1 -We consider the file [multivar_1-1.c.invariant_witness.yaml](multivar_1-1.c.invariant_witness.yaml), -which is a file of verification entries that contains a verification entry of type -loop invariant. -The verification entries where produced for the verification task +Consider the verification task [multivar_1-1.yml](https://github.com/sosy-lab/sv-benchmarks/tree/master/c/loop-acceleration/multivar_1-1.yml) -for program file +with the input program [multivar_1-1.c](https://github.com/sosy-lab/sv-benchmarks/tree/master/c/loop-acceleration/multivar_1-1.c). -The verification entry has four parts: -the entry type, -the metadata to describe the provenance of the entry, -the location that this entry talks about, and -the invariant at that location. - -```yaml -- entry_type: loop_invariant - metadata: - format_version: 0.1 - uuid: 91023a0f-9f45-4385-88c4-1152ade45537 - creation_time: 2021-05-05T15:18:43+02:00 - producer: - name: CPAchecker - version: 2.0.1-svn - configuration: (Optional) svcomp21--04-kInduction - description: (Optional) - command_line: (Optional) - task: - input_files: - - multivar_1-1.c - input_file_hashes: - multivar_1-1.c: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c - specification: CHECK( init(main()), LTL(G ! call(reach_error())) ) - data_model: ILP32 - language: C - location: - file_name: multivar_1-1.c - file_hash: 511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c - line: 22 - column: 0 - function: main - loop_invariant: - string: (x >= 1024U) && (x <= 4294967295U) && (y == x) - type: assertion - format: C -``` - -#### Description - -The following tables describe the format in more detail. - -##### entry -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `entry_type` | string | "loop_invariant" | The type of this entry. The format is specific to the entry type. In this case, the entry type declares that the entry contains a loop invariant that holds at some location in a program. | -| `metadata` | assoc. array | [see below](#metadata) | Additional information about the "environment" in which the entry was produced. | -| `location` | assoc. array | [see below](#location) | Location in the source code to which the entry refers, i.e., at which the loop invariant holds. | -| `loop_invariant` | assoc. array | [see below](#loop_invariant) | Actual loop invariant. | - -##### metadata -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `format_version` | string | "0.1" | Version of the verification-entries format that the entry is formatted in. | -| `uuid` | string | UUID | Unique identifier of the entry ([RFC4122](https://www.ietf.org/rfc/rfc4122.txt) defines the UUID format). | -| `creation_time` | string | ISO 8601 | Date and time when the entry (not the file) was created. | -| `producer` | assoc. array | [see below](#producer) | Tool that produced the entry. | -| `task` | assoc. array | [see below](#task) | Verification task during which the entry was produced. | - -##### producer -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `name` | string | Any | Name of the tool that produced the invariant. | -| `version` | string | Any | Version of the tool. | -| `configuration` | (optional) string | Any | Configuration in which the tool ran. Consider using this property if there are substantially different configurations of the tool. | -| `command_line` | (optional) string | Bash-compliant command | Command line with which the tool ran. Specifying the exact command possibly increases reproducibility. | -| `description` | (optional) string | Any | Additional description. Use this property for any information that does not fit into any of the above properties. | - -##### task -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `input_files` | string[] | Bash-compliant file-name pattern | File(s) that were given as input to the verfier. Each file pattern must represent exactly one input file. | -| `input_file_hashes` | assoc. array |` : ` | Mapping of each input file to its SHA-256 hash. Every file-name pattern listed in `input_files` must appear in this property. | -| `specification` | string | [SV-COMP format](https://sv-comp.sosy-lab.org/2021/rules.php) | Specification against which the program was analyzed for producing the entry. | -| `data_model` | string | "ILP32" *or* "LP64" | Data model that was assumed for the input program. | -| `language` | string | Any | Source language of the input files. | - -##### location -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `file_name` | string | Bash-compliant file-name pattern | Name of the file containing the loop where the invariant holds. Must be present in `task.input_files`. | -| `file_hash` | string | SHA-256 hash | Hash of the file containing the loop where the invariant holds. | -| `line` | integer | natural number > 1 | Line where the invariant holds (starting with 1). | -| `column` | integer | natural number >= 0 | Column where the invariant holds in that line (starting with 0). For example, if `column` has value `0` then the invariant holds *before* the first source-code token of the line. | -| `function` | string | func. name in the source language | Name of the function in which the invariant holds. | - -##### loop_invariant -| Property | Data Type | Format | Description | -|--- | --- | --- | --- | -| `string` | string | defined in `format` | The actual invariant formula. | -| `type` | string | "assertion" | How to interpret `string`. The following values are supported: | -| `format` | string | "C" | Format of the string. The following values are supported: | - -#### Schema - -A [json-schema](http://json-schema.org/) of the format can be found in file -[loop-invariant-schema.json](loop-invariant-schema.json). -This schema can be used for validation and for code generation. - - -### Loop-Invariant Certificate - -Verification entries of entry type loop-invariant certificate -can be used to document the outcome of validation attempts. -That is, a validation of the verification result took place, -in which a tool used the referenced loop invariant -in its attempt to construct a proof of correctness, -and its findings are documented in the entry of type loop-invariant certificate. - -This entry type helps to document trust in an invariant -(if an invariant has many confirmed certificates then it is likely to hold) -and scoring decisions in competitions that assign scores only after confirmation from -a results validation. - -#### Example - -The file of verification entries [multivar_1-1.c.invariant_witness.yaml](multivar_1-1.c.invariant_witness.yaml) -also contains an entry of type `loop-invariant_certificate`, -which has also four parts: -the entry type, -the metadata to describe the provenance of the entry, -the target that identifies what is certified, and -the certification result. - - -```yaml -- entry_type: loop_invariant_certificate - metadata: - format_version: 0.1 - uuid: 954affa9-32e4-4b35-85ae-888da3a6a53b - creation_time: 2021-05-05T15:18:43+02:00 - producer: - name: CPAchecker - version: 2.0.1-svn - configuration: (Optional) svcomp21--04-kInduction - description: (Optional) - command_line: (Optional) - target: - uuid: 91023a0f-9f45-4385-88c4-1152ade45537 - type: loop-invariant - file_hash: XXXf45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c - certification: - string: confirmed - type: verdict - format: confirmed | rejected -``` - -#### Description - -The following tables describe the format in more detail. - -TODO - +The file +[multivar_1-1.c.invariant_witness.yaml](multivar_1-1.c.invariant_witness.yaml) +contains two verification entries: +1. A `loop_invariant` +2. and a `loop_invariant_certificate` that confirms the `loop_invariant`. diff --git a/jsfh.yml b/jsfh.yml new file mode 100644 index 0000000..7ffe30d --- /dev/null +++ b/jsfh.yml @@ -0,0 +1,5 @@ +expand_buttons: true +collapse_long_descriptions: false +collapse_long_examples: false +link_to_reused_ref: false +examples_as_yaml: true diff --git a/loop-invariant-schema.json b/loop-invariant-schema.json deleted file mode 100644 index 6196e67..0000000 --- a/loop-invariant-schema.json +++ /dev/null @@ -1,161 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "title": "Loop Invariant Entry", - "description": "An loop invariant entry", - "type": "object", - "required": [ - "entry_type", - "metadata", - "location", - "loop_invariant" - ], - "properties": { - "entry_type": { - "const": "loop_invariant" - }, - "metadata": { - "type": "object", - "required": [ - "format_version", - "uuid", - "creation_time", - "producer", - "task" - ], - "properties": { - "format_version": { - "type": "string" - }, - "uuid": { - "type": "string", - "format": "uuid" - }, - "creation_time": { - "type": "string", - "format": "date-time" - }, - "producer": { - "type": "object", - "required": [ - "name", - "version" - ], - "properties": { - "name": { - "type": "string" - }, - "version": { - "type": "string" - }, - "configuration": { - "type": "string" - }, - "description": { - "type": "string" - }, - "command_line": { - "type": "string" - } - } - }, - "task": { - "type": "object", - "required": [ - "input_files", - "input_file_hashes", - "specification", - "data_model", - "language" - ], - "properties": { - "input_files": { - "anyOf": [ - { - "type": "array", - "items": { - "type": "string" - } - }, - { - "type": "string" - } - ] - }, - "input_file_hashes": { - "type": "object", - "additionalProperties": { - "type": "string" - } - }, - "specification": { - "type": "string" - }, - "data_model": { - "enum": [ - "32bit", - "64bit" - ] - }, - "language": { - "enum": [ - "C" - ] - } - } - } - } - }, - "location": { - "type": "object", - "required": [ - "file_name", - "file_hash", - "line", - "column", - "function" - ], - "properties": { - "file_name": { - "type": "string" - }, - "file_hash": { - "type": "string" - }, - "line": { - "type": "integer", - "minimum": 0 - }, - "column": { - "type": "integer", - "minimum": 0 - }, - "function": { - "type": "string" - } - } - }, - "loop_invariant": { - "type": "object", - "required": [ - "string", - "type", - "format" - ], - "properties": { - "string": { - "type": "string" - }, - "type": { - "enum": [ - "assertion" - ] - }, - "format": { - "enum": [ - "C" - ] - } - } - } - } -} \ No newline at end of file diff --git a/requirements.txt b/requirements.txt new file mode 100644 index 0000000..414a7ef --- /dev/null +++ b/requirements.txt @@ -0,0 +1 @@ +json-schema-for-humans==0.41.8 diff --git a/witness.schema.json b/witness.schema.json new file mode 100644 index 0000000..3cc4975 --- /dev/null +++ b/witness.schema.json @@ -0,0 +1,391 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$defs": { + "format-version": { + "description": "Version of the format.", + "const": "0.1" + }, + "producer": { + "description": "Producer. Could be a tool, a human or something else.", + "type": "object", + "required": [ + "name", + "version" + ], + "properties": { + "name": { + "type": "string", + "description": "Name of the producer." + }, + "version": { + "type": "string", + "description": "Version of the producer." + }, + "configuration": { + "type": "string", + "description": "Configuration of the producer. Should be used to distinguish different configurations of the same version of the producer." + }, + "description": { + "type": "string", + "description": "Additional description about the producer. Could be used for any information that does not fit into any of the other producer properties." + }, + "command_line": { + "type": "string", + "description": "Bash-compliant command line used to produce the entry. Should be used to improve reproducibility." + } + } + }, + "hash": { + "type": "string", + "description": "SHA-256 hash.", + "pattern": "[0-9a-fA-F]{64}" + }, + "entry-uuid": { + "type": "string", + "description": "Unique identifier of the entry ([RFC4122](https://www.ietf.org/rfc/rfc4122.txt) defines the UUID format).", + "format": "uuid" + }, + "task": { + "description": "Verification task.", + "type": "object", + "required": [ + "input_files", + "input_file_hashes", + "specification", + "data_model", + "language" + ], + "properties": { + "input_files": { + "description": "Files belonging to the verification task that were given as input to the producer.", + "type": "array", + "items": { + "type": "string", + "description": "Bash-compliant file name pattern, which must represent _exactly one_ file." + } + }, + "input_file_hashes": { + "type": "object", + "description": "SHA-256 hashes of each file in `input_files`. Every file name pattern listed in `input_files` must appear as a key.", + "additionalProperties": { + "$ref": "#/$defs/hash" + } + }, + "specification": { + "type": "string", + "description": "Specification in [SV-COMP format](https://sv-comp.sosy-lab.org/2022/rules.php) against which the verification is done." + }, + "data_model": { + "description": "Data model to be assumed for the task.", + "enum": [ + "ILP32", + "LP64" + ] + }, + "language": { + "description": "Source language of the input files.", + "type": "string", + "examples": [ + "C", + "Java" + ] + } + } + }, + "metadata": { + "description": "Information that identifies the entry and describes the context of its production.", + "type": "object", + "required": [ + "format_version", + "uuid", + "creation_time", + "producer", + "task" + ], + "properties": { + "format_version": { + "$ref": "#/$defs/format-version", + "description": "Version of the format of the entry." + }, + "uuid": { + "$ref": "#/$defs/entry-uuid" + }, + "creation_time": { + "type": "string", + "description": "Date and time in ISO8601 format when the entry (not the file) was created.", + "format": "date-time" + }, + "producer": { + "$ref": "#/$defs/producer", + "description": "Producer of the entry." + }, + "task": { + "$ref": "#/$defs/task", + "description": "Verification task for which the entry was produced." + } + } + }, + "metadata-certificate": { + "description": "Information that identifies the certificate entry and describes the context of its production.", + "type": "object", + "required": [ + "format_version", + "uuid", + "creation_time", + "producer" + ], + "properties": { + "format_version": { + "$ref": "#/$defs/format-version", + "description": "Version of the format of the certificate entry." + }, + "uuid": { + "$ref": "#/$defs/entry-uuid" + }, + "creation_time": { + "type": "string", + "description": "Date and time in ISO8601 format when the certificate entry (not the file or target entry) was created.", + "format": "date-time" + }, + "producer": { + "$ref": "#/$defs/producer", + "description": "Producer of the certificate entry." + } + } + }, + "location": { + "description": "Location in the source code.", + "type": "object", + "required": [ + "file_name", + "file_hash", + "line", + "column", + "function" + ], + "properties": { + "file_name": { + "type": "string", + "description": "Name of the file. Must be present in `task.input_files`." + }, + "file_hash": { + "$ref": "#/$defs/hash", + "description": "SHA-256 hash of the file." + }, + "line": { + "type": "integer", + "description": "Line in the file (starting with 1).", + "minimum": 1 + }, + "column": { + "type": "integer", + "description": "Column in the file (starting with 0). Column 0 refers to the very beginning of the line (before any characters).", + "minimum": 0 + }, + "function": { + "type": "string", + "description": "Name of the surrounding function." + } + } + }, + "invariant": { + "description": "Invariant.", + "type": "object", + "required": [ + "string", + "type", + "format" + ], + "properties": { + "string": { + "type": "string", + "description": "The invariant itself." + }, + "type": { + "description": "Interpretation of `string`. The following values are supported:\n\n* `assertion`: Assertion, e.g. `assert()` in C, inserted at the specified location. The insertion is hypothetical and doesn't affect other locations.", + "enum": [ + "assertion" + ] + }, + "format": { + "description": "Format of `string`. The following values are supported:\n\n* `C`: Expression in C language.", + "enum": [ + "C" + ] + } + } + }, + "target": { + "description": "Target entry of certification.", + "type": "object", + "required": [ + "uuid", + "type", + "file_hash" + ], + "properties": { + "uuid": { + "$ref": "#/$defs/entry-uuid", + "description": "Unique identifier of the target entry." + }, + "type": { + "type": "string", + "description": "`entry_type` of the target entry." + }, + "file_hash": { + "$ref": "#/$defs/hash", + "description": "SHA-256 hash of the target file." + } + } + }, + "certification": { + "description": "Certification result.", + "type": "object", + "required": [ + "string", + "type", + "format" + ], + "properties": { + "string": { + "type": "string", + "description": "The certification result itself." + }, + "type": { + "description": "Interpretation of `string`. The following values are supported:\n\n* `verdict`: Verdict about the targeted entry.", + "enum": [ + "verdict" + ] + }, + "format": { + "description": "Format of `string`. The following values are supported:\n\n* `confirmed | rejected`: Either \"confirmed\" or \"rejected\".", + "enum": [ + "confirmed | rejected" + ] + } + } + } + }, + "type": "array", + "items": { + "oneOf": [ + { + "title": "Loop invariant", + "description": "Loop invariants are important building blocks in software verification. Many verification approaches use loop invariants as lemmata to construct proofs of correctness.", + "type": "object", + "required": [ + "entry_type", + "metadata", + "location", + "loop_invariant" + ], + "properties": { + "entry_type": { + "const": "loop_invariant" + }, + "metadata": { + "$ref": "#/$defs/metadata" + }, + "location": { + "$ref": "#/$defs/location", + "description": "Location in the source code where the loop invariant holds." + }, + "loop_invariant": { + "$ref": "#/$defs/invariant", + "description": "The loop invariant description." + } + }, + "examples": [ + { + "entry_type": "loop_invariant", + "metadata": { + "format_version": 0.1, + "uuid": "91023a0f-9f45-4385-88c4-1152ade45537", + "creation_time": "2021-05-05T13:18:43.000Z", + "producer": { + "name": "CPAchecker", + "version": "2.0.1-svn", + "configuration": "svcomp21--04-kInduction" + }, + "task": { + "input_files": [ + "multivar_1-1.c" + ], + "input_file_hashes": { + "multivar_1-1.c": "511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c" + }, + "specification": "CHECK( init(main()), LTL(G ! call(reach_error())) )", + "data_model": "ILP32", + "language": "C" + } + }, + "location": { + "file_name": "multivar_1-1.c", + "file_hash": "511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c", + "line": 22, + "column": 0, + "function": "main" + }, + "loop_invariant": { + "string": "(x >= 1024U) && (x <= 4294967295U) && (y == x)", + "type": "assertion", + "format": "C" + } + } + ] + }, + { + "title": "Loop invariant certificate", + "description": "Loop invariant certificates document validation attempts of loop invariants, for example by trying to use the target loop invariant in a proof of correctness.\n\nCertificates document correctness and trustworthiness of invariants.", + "type": "object", + "required": [ + "entry_type", + "metadata", + "target", + "certification" + ], + "properties": { + "entry_type": { + "const": "loop_invariant_certificate" + }, + "metadata": { + "$ref": "#/$defs/metadata-certificate" + }, + "target": { + "$ref": "#/$defs/target", + "description": "Target entry of type `loop_invariant` which is being certified." + }, + "certification": { + "$ref": "#/$defs/certification", + "description": "The loop invariant certification result description." + } + }, + "examples": [ + { + "entry_type": "loop_invariant_certificate", + "metadata": { + "format_version": 0.1, + "uuid": "954affa9-32e4-4b35-85ae-888da3a6a53b", + "creation_time": "2021-05-05T13:18:43.000Z", + "producer": { + "name": "CPAchecker", + "version": "2.0.1-svn", + "configuration": "svcomp21--04-kInduction" + } + }, + "target": { + "uuid": "91023a0f-9f45-4385-88c4-1152ade45537", + "type": "loop-invariant", + "file_hash": "511f45a8d763ef520f6d92e4135c8572805994a66531c6216b17157d0dde2f9c" + }, + "certification": { + "string": "confirmed", + "type": "verdict", + "format": "confirmed | rejected" + } + } + ] + } + ] + } +} \ No newline at end of file