Deeply Integrating C11 Code Support into Isabelle/PIDE

TL;DR

This paper introduces a flexible framework that integrates C11 code support into Isabelle/PIDE, enabling various verification techniques to work seamlessly on the same source with customizable semantics and annotations.

Contribution

It presents a novel, extensible interface for C code verification back-ends within Isabelle/PIDE, supporting semantic annotations and multiple semantics configurations.

Findings

Framework supports multiple verification techniques on same source

Semantic annotations enable local control of back-end settings

Case studies validate the integration approach

Abstract

We present a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. Thus, various techniques such as deductive program verification or white-box testing can be applied to the same source, which is part of an integrated PIDE document model. Semantic back-ends are free to choose the supported C fragment and its semantics. In particular, they can differ on the chosen memory model or the specification mechanism for framing conditions. Our framework supports semantic annotations of C sources in the form of comments. Annotations serve to locally control back-end settings, and can express the term focus to which an annotation refers. Both the logical and the syntactic context are available when semantic annotations are evaluated. As a consequence, a formula in an annotation can refer both to HOL or C variables. Our approach demonstrates the degree of maturity and expressive power the Isabelle/PIDE subsystem has achieved in recent years. Our integration technique employs Lex and Yacc style grammars to ensure efficient deterministic parsing. We present two case studies for the integration of (known) semantic back-ends in order to validate the design decisions for our back-end interface.