jennalwise / graphblas-verif

Formal verification of the GraphBLAS C API implementation by Tim Davis using Frama-C/WP.

graphblas-verif

*** THIS README AND REPOSITORY ARE WORKS IN PROGRESS: Mostly finalized versions will be available after August 24, 2018 ***

Formal verification of the GraphBLAS C API implementation by Tim Davis using Frama-C/WP and VeriFast (potentially). Modified versions of GraphBLAS 2.0.1 (for verification) are contained within this repository as well as an unmodified version for comparison.

For those interested, the most recent version of GraphBLAS is packaged with SuiteSparse and can be downloaded here.

Documentation

For more information and documentation, please visit the Wiki.

Acknowledgments

Mentors

• Manoj Kumar, IBM Research
• Jonathan Aldrich, Carnegie Mellon University
• Joshua Sunshine, Carnegie Mellon University
• Pratap Pattniak, IBM Research

We would like to thank Tim Davis (Texas A&M University) for allowing the use, modification, and distribution of his GraphBLAS implementation.

We would also like to thank IBM for funding this research.

graphblas-verif's Issues

Verify the matrix queue linked list internal to matrix structs

Includes modifying the matrix valid predicate to ensure matrices are in the queue when they should be, not in the queue when they shouldn't be, etc. (see GB_object_check.c)

Possible bug in identity_is_zero_bool_valid predicate for monoid validation

EVA is crashing with an error claiming it doesn't support ACSL logic inductive types. identity_is_zero_bool_valid is the predicate where the logic inductive types apparently show up. Determine if logic inductive types are used (I didn't think they were) and try to get around it, otherwise leave it out. Commented out for now.

Change \pow(2,60) to (GrB_Index) (1ULL << 60) everywhere in annotations

EVA and WP cannot discharge proofs with \pow(2,60), but can with 1ULL << 60; representing 2^60 which is the GB_INDEX_MAX.

Refactor the logic function name matrix_nvals to matrix_nzmax

nzmax may not be the same as nvals in meaning

Need extra requires statements for callee's preconditions (WP)

• GrB_Matrix_new & dependencies
• GrB_Matrix_free & dependencies
• GrB_Matrix_nrows/ncols & dependencies
• GrB_Matrix_clear & dependencies
• GrB_AxB_numeric & dependencies

Valid matrices should have correct number of zombies

Using ghost code it should be possible to validate that a matrix has the correct number of zombies.

GB_Matrix_clear assigns clause not proving correctly

Change (0..size-1) to (0 .. size-1) to ensure always parsed/interpreted correctly

Quirk of the specification language is that (0..size-1) has to contain spaces around .., ie. (0 .. size-1). Need to make sure annotated code reflects this.

GraphBLAS struct memory footprints may be incorrect and need refactored

• Need to refactor memory footprint logic functions into separated predicates, because WP doesn't support most heterogeneous pointer casts, Alt-Ergo throws an error when using logic functions which return set<T>, and \separated does not ensure pointers within a set are separated from themselves, but rather it ensures those pointers are separated from pointers in other argument sets to \separated. This will make the logic/annotations significantly longer. [The last reason is the most important, because the others can be resolved through the Value Analysis plug-in]
• Need to take a second look at how I deal with pointers to other GraphBLAS structs within the current GraphBLAS struct
• Some pointers can alias within and between structs, ie. type and function pointers, so make sure this is handled correctly within footprints and when they are used

Try refactoring predicate/logic functions in annotlib.acsl for increased elegance and encapsulation

Move assigns/frees/allocates clauses out of behaviors

WP doesn't support assigns clauses well within behaviors, particularly when verifying a call hierarchy. WP doesn't support frees/allocates clauses at all, but may in the future and most likely will not support them well within behaviors as with assigns clauses.

• GrB_Matrix_free and dependencies
• GrB_Matrix_new and dependencies
• GrB_Matrix_nrows and dependencies - no assigns/frees/allocates clauses
• GrB_Matrix_ncols and dependencies - no assigns/frees/allocates clauses
• GB_AxB_numeric dependencies

Null pointers alias to eachother in EVA memory model; fix use of separated predicates

Use of separation predicates should involve checking for null pointers as EVA's memory model ensures null pointers alias, ie. \separated(null,null) == false.

• Matrix footprint separated predicate
• GrB_Matrix_new and dependencies
• GrB_Matrix_free and dependencies
• GrB_Matrix_nrows/ncols and dependencies
• GB_shallow_cast and dependencies
• GB_Matrix_clear and dependencies
• GB_Work_alloc/free and dependencies
• Other footprint separated predicates

Verify global and local thread storage

Currently, not verifying anything about global and local thread storage structs during method/function calls.

Verify algebraic properties of monoids in monoid_valid predicate

• verify that the binary operator of a monoid is associative
• verify that the identity element of a monoid is in fact an identity element of the binary operator and monoid domain
• validate any other algebraic properties of a monoid

Refactor annotlib.acsl preds & logic functions to ensure sound casting of ptrs (void ptrs in particular)

WP's Typed+cast memory model (Byte not implemented yet) does support heterogeneous casts of polymorphic void ptrs, so long as it is casted to the proper type ptr that it should be.

Ie.

    bool b = (bool)true;
    bool *b_ptr = &b;
    void* f = (void*)b_ptr;
    //@ assert \valid((bool*)f);

Therefore, annotlib.acsl predicates and logic functions must be refactored to ensure sound casting of void ptrs. Otherwise, proofs will be unsound following the Typed+cast memory model.

EVA crashing on shallow_cast annotation

Annotations for shallow_cast and cast_array written with minimal testing for matrix multiply. WP can parse the annotations fine, but EVA is crashing when being run on shallow_cast + its dependencies. Does not crash on cast_array. Need to fix this.

Something in matrix_valid predicate is crashing it.

A valid semiring should have a valid commutative monoid

Should check that the valid monoid within a semiring is in fact commutative. Monoid validity should check for algebraic properties of monoid structures, such as having an associative binary operator and a proper identity for that operator. Therefore, resolution of this issue depends on resolution of issue 2.

Equality of specified objects

Write predicates to determine the equality of the GraphBLAS structs annotated in annotlib.acsl.

Added extra requires clauses for RTE gaurds where behaviors exist

RTE gaurds can't be proven by behaviors - need top level requires clauses to discharge the proofs.

• GrB_Matrix_free and dependencies
• GrB_Matrix_new and dependencies
• GrB_Matrix_nrows and dependencies - no assigns/frees/allocates clauses
• GrB_Matrix_ncols and dependencies - no assigns/frees/allocates clauses
• GB_AxB_numeric and dependencies

GB_Matrix_free does not ensure anything about internal aliased objects: GrB_Type, GrB_BinaryOp, etc.

GB_Matrix_free should probably ensure that internal graphblas objects are still valid, since they may alias with other objects which have not been freed or may be used in following program statements.

• GrB_Type
• GrB_BinaryOp

Matrix queue pointers will be handled when verifying the Matrix queue.

Annotation for GrB_Matrix_new & dependencies should include matrix_storage_init pred

Write matrix_storage_init predicate that describes the internal storage values after a call to GrB_Matrix_new

All free methods should be able to handle non valid matrices

Currently, free method annotations do not handle non-valid matrices which is technically incorrect, but done currently for simplicity.