2021.06.08: RefinedC

Sammler, Lepigre, Krebbers, Memarian, Dreyer, Garg, [2021] “RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types”

presenter: Nikita

adds refinement types to C
both foundational & automated reasoning
based on Iris
syntax looks inspired by Rust

Hackernews discussion

https://news.ycombinator.com/item?id=27265329

1. Introduction

Memory allocator example
Uses new C2x annotation syntax
Embeds Iris/Coq code into annotations
Several parts:
- Lithium - decidable assertions
- Caesium - deep embedding of C

2. RefinedC by Example

What is uninit?
- Rust-style tag for indicating that the client should initialize the memory?
Ownership types: (de)allocation and write access
- line 7: acquire ownershop, line 9: release ownership
What is own p?
- https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/ANNOTATIONS.md#constraints
Embed nulls into optional types (so you can’t pass unguarded null)
Another allocator for showing lists and loop invariants

3. RefinedC Front End and Caesium

4. RefinedC Types and Specifications

5. Lithium: Separation Logic Programming

Decidable fragment of separation logic, no backtracking
Split goal into left and right subterms (restricted on the left)
Can be extended?
Not complete, so the automation argument is a bit weak - for some programs you’d still need to manually work out additional annotations

6. Examples of RefinedC Typing Rules

7. Evaluation and Case Studies

Cheating with overhead? They ignore the Spec
No numbers on running time for checking

uses Mezzo-like [71] alias types [83,101] instead of Rust’s lifetimes and mutable references

9. Limitations and Future Work

not full C (floats/casts)
liveness (transfinite Iris)