Skip to content
This repository has been archived by the owner on Oct 14, 2022. It is now read-only.

Introduce entry type 'location_invariant' for YAML-based witnesses. #59

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Introduce entry type 'location_invariant' for YAML-based witnesses. #59

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 109 additions & 0 deletions README-YAML.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ The format of an entry depends on its entry type.
Currently, we have the following entry types:
- `loop_invariant`
- `loop-invariant_certificate`
- `location_invariant`

Entry types are use-case specific and independent.
Each producer and consumer of entries can filter those entry types that it supports.
Expand Down Expand Up @@ -211,3 +212,111 @@ The following tables describe the format in more detail.

TODO

### Location Invariant

Location invariants can be helpful in verifying a given loop invariant and
in furthering the understanding of a human reader by giving information
about an intermediate state of the computation.

In the following, we provide an example as well as a detailed description
of the various components of a location invariant entry.

#### Example

We consider the file [trex04.invariant_witness.yml](trex04.invariant_witness.yml),
which is a file of verification entries that contains a verification entry of type
location invariant.
The verification entries were produced for the verification task
[trex04.yml](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/trex04.yml)
for program file
[trex04.c](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/trex04.c).

Just like for loop invariants, the verification entry consists of 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: location_invariant
metadata:
format_version: 0.2
uuid: 92c380d6-00a1-4e97-8c63-0f246206c6ab
creation_time: 2022-05-16T11:56:13.480768Z
producer:
name: A2Y
version: 1.0
task:
input_files:
- c/loops/trex04.c
input_file_hashes:
c/loops/trex04.c: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
location:
file_name: c/loops/trex04.c
file_hash: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
line: 47
column: 0
function: main
location_invariant:
string: x <= 0
type: assertion
format: C
```

#### Description

The following tables describe the format in more detail.

##### entry
| Property | Data Type | Format | Description |
|--- | --- | --- | --- |
| `entry_type` | string | "location_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 location invariant that holds at some location in a program. |
| `metadata` | assoc. array | [see below](#metadata-1) | Additional information about the "environment" in which the entry was produced. |
| `location` | assoc. array | [see below](#location-1) | Location in the source code to which the entry refers, i.e., at which the invariant holds. |
| `location_invariant` | assoc. array | [see below](#location_invariant) | Actual location invariant. |

##### metadata
| Property | Data Type | Format | Description |
|--- | --- | --- | --- |
| `format_version` | string | Format version specifier | Version of the verification-entries format that the entry is formatted in. The entry type "location_invariant" was introduced in version 0.2 of the format.|
| `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-1) | Tool that produced the entry. |
| `task` | assoc. array | [see below](#task-1) | Verification task during which the entry was produced. |

##### producer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might get a bit redundant if we start copying sections like this. I would rather have the description refactored such that we have a section for common keys like producer and then just point to that section for the different entry types.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's a radical idea: ditch the hand-written Markdown altogether and have everything in a nice JSON schema, see #61.

| 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 |`<file-pattern> : <file-hash>` | 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 location where the invariant holds. Must be present in `task.input_files`. |
| `file_hash` | string | SHA-256 hash | Hash of the file containing the location 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. |

##### location_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: <ul><li><em>assertion:</em> Has the C semantics of `assert(<string>)` inserted at the specified `location`.</li></ul> |
| `format` | string | "C" | Format of the string. The following values are supported: <ul><li><em>C:</em> Expression in C language.</li></ul> |
27 changes: 27 additions & 0 deletions trex04.invariant_witness.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
- entry_type: location_invariant
metadata:
format_version: 0.2
uuid: 92c380d6-00a1-4e97-8c63-0f246206c6ab
creation_time: 2022-05-16T11:56:13.480768Z
producer:
name: A2Y
version: 1.0
task:
input_files:
- c/loops/trex04.c
input_file_hashes:
c/loops/trex04.c: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
data_model: ILP32
language: C
location:
file_name: c/loops/trex04.c
file_hash: f70ffe9cd45c37f44e9e780e31340fab45b6a2fb7f7ef23a2d90faf4241229d6
line: 47
column: 0
function: main
location_invariant:
string: x <= 0
type: assertion
format: C