关于Verifiable-C支持的C语言子集及CompCert C程序可验证性的技术咨询

Great question—let’s unpack this step by step, using the reference you cited from Program Logics For Certified Compilers (page 143).

First, let’s recap the relationships you mentioned to set the stage:

• Verifiable-C is a subset of Clight: This means Verifiable-C only supports a restricted portion of Clight’s syntax and semantics, specifically tailored for formal verification.
• CompCert compiles CompCert C to Clight: The CompCert compiler takes programs written in its own CompCert C dialect (a carefully defined subset of standard C) and translates them down to the Clight intermediate language.

Now, to answer your core question: No, not all CompCert C programs can be verified with Verifiable-C. Here’s why:

1. CompCert C includes features outside Verifiable-C’s scope #

CompCert C is a larger dialect than Verifiable-C. Even though CompCert can translate CompCert C to Clight, some CompCert C constructs get turned into Clight code that Verifiable-C doesn’t support. For example:

• Certain low-level pointer operations or non-structured control flow patterns allowed in CompCert C (and valid in Clight) may not be expressible or verifiable using Verifiable-C’s program logic (like separation logic).
• CompCert C allows some syntax sugar or convenience features that, while compilable to Clight, don’t map cleanly to Verifiable-C’s verified subset.

2. Verifiable-C requires more than just valid syntax #

Verifiable-C isn’t just a syntactic subset—it’s a verifiable subset. To use it, your code needs formal verification annotations that CompCert C doesn’t require:

• Function contracts (preconditions, postconditions)
• Loop invariants
• Assertions about memory safety and correctness

CompCert C programs only need to follow CompCert’s syntactic and semantic rules to compile. They don’t include these verification specs, so even if a CompCert C program translates to Clight, it won’t be ready for Verifiable-C verification until you add these formal annotations.

3. Clight has features not covered by Verifiable-C #

The book explicitly states Verifiable-C is a subset of Clight, which means Clight has functionality that Verifiable-C doesn’t target. CompCert’s translation of CompCert C might produce Clight code that uses these non-Verifiable-C features, making it incompatible with the verification framework.

To sum up #

CompCert’s ability to translate CompCert C to Clight is about compilation, not verification. Verifiable-C is a narrower, verification-focused subset of Clight, so only CompCert C programs that:

• Translate to Clight code within Verifiable-C’s supported subset, and
• Include the necessary formal verification annotations

can be verified using Verifiable-C.

内容的提问来源于stack exchange，提问作者Artem Kokorin