Automated Static Code Verification¶

The tests/verification module (and embedded tests) implement automatic checks that the code in vc2_conformance matches the pseudocode definitions in the VC-2 specification.

The tests/verification/test_equivalence.py test script (which is part of the normal Pytest test suite) automatically finds functions in the vc2_conformance codebase (using vc2_conformance.pseudocode.metadata) and checks they match the equivalent function in the VC-2 specification (which are copied out verbatim in tests/verification/reference_pseudocode.py).

Note

To ensure that vc2_conformance.pseudocode.metadata contains information about all submodules of vc2_conformance, the conftest.py file in this directory ensures all submodules of vc2_conformance are loaded.

Pseudocode deviations¶

In some cases, a limited set of well-defined differences are allowed to exist between the specification and the code used in vc2_conformance. For example, docstrings need not match and in some cases, extra changes may be allowed to facilitate, e.g. bitstream deserialisation. The specific comparator used depends on the deviation parameter given in the metadata as follows:

deviation=None: verification.comparators.Identical
deviation="serdes": verification.comparators.SerdesChangesOnly

Functions marked with the following additional deviation values will not undergo automatic verification, but are used to indicate other kinds of pseudocode derived function:

deviation="alternative_implementation": An alternative, orthogonal implementation intended to perform the same role as an existing pseudocode function.
deviation="inferred_implementation": A function whose existence is implied or whose behaviour is explained in prose and therefore has no corresponding pseudocode definition.

Amendment comments¶

In some cases it is necessary for an implementation to differ arbitrarily from the standard (i.e. to make ‘amendments’). For example, additional type checks may be added or picture decoding functions disabled when not required. Such amendments must be marked by special ‘amendment comments’ which start with either two or three # characters, as shown by the snippet below:

def example_function(a, b):
    # The following lines are not part of the standard and so are marked by
    # an amendment comment to avoid the pseudocode equivalence checking
    # logic complaining about them
    ## Begin not in spec
    if b <= 0:
        raise Exception("'b' cannot be zero or negative!")
    ## End not in spec

    # For single-line snippets which are not in the standard you can use
    # the following end-of-line amendment comment
    assert b > 0  ## Not in spec

    # The following code is part of the standard but is disabled in this
    # example. Even though it is commented out, it will still be checked
    # against the standard. If the standard changes this check ensures that
    # the maintainer must revisit the commented-out code and re-evaluate
    # the suitability of any amendments made.
    ### if do_something(a):
    ###     do_something_else(b)

    return a / b

More details of the amendment comment syntax can be found in verification.amendment_comments.

Internals¶

This module does not attempt to perform general purpose functional equivalence checking – a known uncomputable problem. Instead, comparisons are made at the Abstract Syntax Tree (AST) level. By performing checks at this level semantically insignificant differences (e.g. whitespace and comments) are ignored while all other changes are robustly identified. The Python built-in ast module is used to produce ASTs ensuring complete support for all Python language features.

To compare ASTs, this module provides the verification.node_comparator.NodeComparator. Instances of this class can be used to compare pairs of ASTs and report differences between them.

The subclasses in verification.comparators are similar but allow certain well-defined differences to exist between ASTs. As an example, verification.comparators.SerdesChangesOnly will allow calls to the read_* functions to be swapped for their equivalent vc2_conformance.bitstream.serdes.SerDes method calls with otherwise identical arguments.

To allow differences between function implementations and the specification, functions are pre-processed according to the amendment comment syntax described above. This preprocessing step is implemented in verification.amendment_comments and uses the built-in Python tokenize module to ensure correct interoperability with all other Python language features.

Finally the verification.compare module provides the compare_functions() function which ties all of the above components together and produces human-readable reports of differences between functions.

All of the above functionality is tested by the other test_*.py test scripts in this module’s directory.

`verification.node_comparator`: AST Comparison Framework¶

The NodeComparator class is intended to form the basis of comparison routines which allow controlled differences between two ASTs to be ignored.

For exapmle, the following can be used to compare two ASTs, ignoring docstrings at the start of functions:

from itertools import dropwhile

from verification.node_comparator import NodeComparator

class SameExceptDocstrings(NodeComparator):

    def compare_FunctionDef(self, n1, n2):
        def without_docstrings(body):
            return dropwhile(
                lambda e: isinstance(e, ast.Expr) and isinstance(e.value, ast.Str),
                body,
            )

        return self.generic_compare(
            n1, n2, filter_fields={"body": without_docstrings}
        )

This can then be used like so:

>>> func_1 = "def func(a, b):\n    '''Add a and b'''\n    return a + b"
>>> func_2 = "def func(a, b):\n    return a + b"

>>> import ast
>>> c = SameExceptDocstrings()
>>> c.compare(ast.parse(func_1), ast.parse(func_2))
True

`NodeComparator` API¶

class NodeComparator¶

An ast.AST visitor object (similar to ast.NodeVisitor which simultaneously walks two ASTs, testing them for equivalence.

The compare() method of instances of this class may be used to recursively compare two AST nodes.

get_row_col()¶: Find the current row and column offsets for the tokens currently being compared with compare().

compare(n1, n2)¶

Recursively compare two AST nodes.

If n1 has the type named N1Type and n2 has the type named N2Type, this function will try to call one of the following methods:

compare_N1Type (if N1Type is the same as N2Type)
compare_N1Type_N2_type
compare_N1Type_ANY
compare_ANY_N2Type
generic_compare

The first method to be found will be called and its return value returned. The various compare_* methods may be overridden by subclasses of NodeComparator and should implement the same interface as this method.

Parameters

n1, n2ast.AST: The nodes to compare

Returns

resultTrue or NodesDiffer: True if the ASTs are equal and NodesDiffer (which is faslsey) otherwise.

generic_compare(n1, n2, ignore_fields=[], filter_fields={})¶

Base implementation of recurisive comparison of two AST nodes.

Compare the type of AST node and recursively compares field values. Recursion is via calls to compare().

Options are provided for ignoring differences in certain fields of the passed AST nodes. Authors of custom compare_* methods may wish to use these arguments when calling generic_compare() to allow certain fields to differ while still reporting equality.

Parameters

n1, n2ast.AST

The nodes to compare

ignore_fields[str, …]

A list of field names to ignore while comparing the AST nodes.

filter_fields{fieldname: fn or (fn, fn) …}

When a list-containing field is encountered, functions may be provided for pre-filtering the entries of the lists being compared. For example, one might supply a filtering function which removes docstrings from function bodies.

Entries in this dictionary may be either:

Functions which take the list of values and should return a new list of values to use in the comparison. This function must not mutate the list passed to it.
A pair of functions like the one above but the first will be used for filtering n1’s field and the second for n2’s field. Either may be None if no filtering is to take place for one of the nodes.

Returns

resultTrue or NodesDiffer: True if the ASTs are equal and NodesDiffer (which is faslsey) otherwise.

`NodesDiffer` types¶

class NodesDiffer(n1, n1_row_col, n2, n2_row_col, reason=None)¶

A result from NodeComparator indicating that two ASTs differ.

This object is ‘falsy’ (i.e. calling bool() on a NodeComparator instance returns False).

Attributes

n1, n2ast.AST: The two ASTs being compared.
n1_row_col, n2_row_col(row, col) or (None, None): The row and column of the ‘n1’ and ‘n2’ tokens, or the values for the row and column of the nearest token with a known position.
reasonstr or None: A string describing how the two nodes differ with a human-readable message.

class NodeTypesDiffer(n1, n1_row_col, n2, n2_row_col)¶: A pair of nodes have different types.

class NodeFieldsDiffer(n1, n1_row_col, n2, n2_row_col, field)¶

A pair of nodes differ in the value of a particular field.

Attributes

fieldstr: The field name where the AST nodes differ.

class NodeFieldLengthsDiffer(n1, n1_row_col, n2, n2_row_col, field, v1, v2)¶

A pair of nodes differ in the length of the list of values in a particular field.

Attributes

fieldstr: The field name where the AST nodes differ.
v1, v2list: The values of the fields (after any filtering has taken place).

class NodeListFieldsDiffer(n1, n1_row_col, n2, n2_row_col, field, index, v1, v2)¶

A pair of nodes differ in the value of a list field entry.

Attributes

fieldstr: The field name where the AST nodes differ.
indexint: The index of the value in the v1 and v2 lists.
v1, v2list: The values of the fields (after any filtering has taken place).

`verification.comparators`¶

A series of verification.node_comparator.NodeComparator based comparators for checking the equivalence of VC-2 pseudocode functions from the spec with their implementations in the vc2_conformance package.

class Identical¶

Bases: verification.node_comparator.NodeComparator

Compares two function implementations only allowing the following differences:

Their docstrings may be different.
A vc2_conformance.pseudocode.metadata.ref_pseudocode() decorator may be used.
Constants from the vc2_data_tables module may be used in place of their numerical literal equivalents.

class SerdesChangesOnly¶

Bases: verification.node_comparator.NodeComparator

Compares two function implementations where the first is a VC-2 pseudocode definition and the second is a function for use with the vc2_conformance.bitstream.serdes framework. The following differences are allowed:

Differing docstrings. (Justification: has no effect on behaviour.)
The addition of a vc2_conformance.pseudocode.metadata.ref_pseudocode() decorator to the second function. (Justification: has no effect on behaviour.)
The addition of a vc2_conformance.bitstream.serdes.context_type() decorator to the second function. (Justification: has no effect on behaviour.)
The addition of serdes as a first argument to the second function. (Justification: required for use of the serdes framework, has no effect on behaviour.)
The wrapping of statements in with serdes.subcontext context managers in the second function will be ignored. (Justification: these context managers have no effect on behaviour but are required to set the serdes state.)
The addition of the following methods calls in the second function (Justification: these method calls have no effect on behaviour but are required to set the serdes state):
The substitution of an assignment to state.bits_left with a call to vc2_conformance.bitstream.serdes.SerDes.bounded_block_begin() in the second function, taking the assigned value as argument. (Justification: this has the equivalent effect in the bitstream I/O system).
The following I/O function substitutions in the second function are allowed with an additional first argument (for the target name). (Justification: these functions have the equivalent effect in the bitstream I/O system).
- read_bool -> serdes.bool
- read_nbits -> serdes.nbits
- read_uint_lit -> serdes.uint_lit or serdes.bytes
- read_uint or read_uintb -> serdes.uint
- read_sint or read_sintb -> serdes.sint
- byte_align -> serdes.byte_align
- flush_inputb -> serdes.bounded_block_end
Substitution of empty dictionary creation for creation of vc2_conformance.pseudocode.state.State or vc2_conformance.pseudocode.video_parameters.VideoParameters fixed dicts is allowed. (Justification: These are valid dictionary types, but provide better type checking and pretty printing which is valuable here).

`verification.amendment_comments`¶

In the vc2_conformance module it is sometimes necessary to make amendments to the pseudocode. For example, validity checks may be added or unneeded steps removed (such as performing a wavelet transform while simply deserialising a bitstream).

To make changes made to a VC-2 function implementations explicit, the following conventions are used:

When code present in the spec is removed or disabled, it is commented out using triple-hash comments like so:

def example_1(a, b):
    # Code as-per the VC-2 spec
    c = a + b

    # No need to actually perform wavelet transform
    ### if c > 1:
    ###     wavelet_transform()
    ###     display_picture()

    # More code per the spec
    return c

When code is added, it should be indicated using either a ## Not in spec double-hash comment:

def example_2(a, b):
    assert b > 0  ## Not in spec

    return a / b

Or within a ## Begin not in spec, ## End not in spec block:

def example_2(a, b):
    ## Begin not in spec
    if b < 0:
        raise Exception("Negative 'b' not allowed")
    elif b == 0:
        raise Exception("Can't divide by 'b' when it is 0")
    ## End not in spec

    return a / b

To enable the automated verification that implemented functions match the VC-2 spec (e.g. using verification.comparators), any amendments to the code must first be undone. The undo_amendments() function may be used to performs this step.

undo_amendments(source)¶

Given a Python source snippet, undo all amendments marked by special ‘amendment comments’ (comments starting with ## and ###).

The following actions will be taken:

Disabled code prefixed ### ... (three hashes and a space) will be uncommented.
Lines ending with a ## Not in spec comment will be commented out.
Blocks of code starting with a ## Begin not in spec line and ending with a ## End not in spec line will be commented out.

Returns

(source, indent_corrections): The modified source is returned along with a dictionary mapping line number to an indentation correction. These corrections may be used to map column numbers in the new source to column numbers in the old source.

Raises

tokenize.TokenError
BadAmendmentCommentError
UnmatchedNotInSpecBlockError
UnclosedNotInSpecBlockError

The following exception custom exception types are defined:

exception BadAmendmentCommentError(comment, row, col)¶

An unrecognised amendment comment (a comment with two or more hashes) was found.

Attributes

commentstr: The contents of the comment
row, colint: The position in the source where the unrecognised comment starts

exception UnmatchedNotInSpecBlockError(row)¶

An ‘End not in spec’ amendment comment block was encountered without a corresponding ‘Begin not in spec’ block.

Attributes

rowint: The line in the source where the ‘end’ comment was encounterd

exception UnclosedNotInSpecBlockError(row)¶

A ‘Begin not in spec’ amendment comment block was not closed.

Attributes

rowint: The line in the source where the block was started.

`verification.compare`: Compare function implementations¶

This module provides a function, compare_functions(), which uses a specified comparator (verification.comparators) to determine if a given function matches the reference VC-2 pseudocode.

compare_functions(ref_func, imp_func, comparator)¶

Compare two Python functions where one is a reference implementation and the other an implementation used in vc2_conformance.

Parameters

ref_funcFunctionType: The reference VC-2 implementation of a function.
imp_funcFunctionType: The implementation of the same function used in vc2_conformance. Will be pre-processed using verification.amendment_comments.undo_amendments() prior to comparison.
comparatorverification.node_comparator.NodeComparator: The comparator instance to use to test for equivalence.

Returns

True or Difference: True is returned if the implementations are equal (according to the supplied comparator). Otherwise a Difference is returned enumerating the differences.

Raises

ComparisonError

compare_sources(ref_source, imp_source, comparator)¶

Compare two Python sources, one containing a reference VC-2 pseudocode function and the other containing an implementation.

Parameters

ref_sourcestr: The reference VC-2 pseudocode implementation of a function.
imp_sourcestr: The implementation of the same function used in vc2_conformance. Will be pre-processed using verification.amendment_comments.undo_amendments() prior to comparison.
comparatorverification.node_comparator.NodeComparator: The comparator instance to use to test for equivalence.

Returns

True or Difference: True is returned if the implementations are equal (according to the supplied comparator). Otherwise a Difference is returned enumerating the differences.

Raises

ComparisonError

class Difference(message, ref_row=None, ref_col=None, imp_row=None, imp_col=None, ref_func=None, imp_func=None)¶

A description of the difference between a reference function and its implementation.

Use str to turn into a human-readable description (including source code snippets).

Parameters

messagestr
ref_row, ref_colint or None: The position in the reference code where the difference ocurred. May be None if not related to the reference code.
imp_row, imp_colint or None: The position in the implementation code where the difference ocurred. May be None if not related to the implementation code.
ref_func, imp_funcFunctionType or None: The Python function objects being compared.

exception ComparisonError(message, ref_row=None, ref_col=None, imp_row=None, imp_col=None, ref_func=None, imp_func=None)¶

An error occurred while attempting to compare two function implementations.

Use str to turn into a human-readable description (including source code snippets).

Parameters

messagestr
ref_row, ref_colint or None: The position in the reference code where the error ocurred. May be None if not related to the reference code.
imp_row, imp_colint or None: The position in the implementation code where the error ocurred. May be None if not related to the implementation code.
ref_func, imp_funcFunctionType or None: The Python function objects being compared.

Automated Static Code Verification¶

Pseudocode deviations¶

Amendment comments¶

Internals¶

`verification.node_comparator`: AST Comparison Framework¶

`NodeComparator` API¶

`NodesDiffer` types¶

`verification.comparators`¶

`verification.amendment_comments`¶

`verification.compare`: Compare function implementations¶

Table of Contents

Previous topic

Next topic

This Page

Automated Static Code Verification¶

Pseudocode deviations¶

Amendment comments¶

Internals¶

verification.node_comparator: AST Comparison Framework¶

NodeComparator API¶

NodesDiffer types¶

verification.comparators¶

verification.amendment_comments¶

verification.compare: Compare function implementations¶

`verification.node_comparator`: AST Comparison Framework¶

`NodeComparator` API¶

`NodesDiffer` types¶

`verification.comparators`¶

`verification.amendment_comments`¶

`verification.compare`: Compare function implementations¶