---
tags: prusti, prusti-student-projects
---

# Prusti PW project: FFI specification

project dates: 19. 9. 2022 - (mid-January 2023)
meetings: Mondays at 13:00, https://ethz.zoom.us/j/68834336092

## Attaching specs to extern functions

extern "C" {
    #[ensures(input >= 0 ==> result == input)]
    #[ensures(input < 0 ==> result == -input)]
    fn abs(input: i32) -> i32;
}

- [x] currently runs into a compiler error
- we are expanding the specification item for the precondition within the `extern "C"` block
- need something similar to `#[refine_trait_spec]`

- [x] if fixed manually (using `PRUSTI_PRINT_DESUGARED_SPECS`), specifications are still not attached to the call
- see what goes on in the MIR representation
- does the spec collector find the specs?
- does the call resolve to the same `DefId`?
- does an extern call use the `Call` terminator in MIR?

- [x] make sure specs can be exported across crate boundaries

## Set up CI

- (unit) test specifications on native functions
- compile a `.so`/`.dylib`/`.dll` with a simple function in C

## Features needed for Python C extension APIs

- note: based on the internals of [PyO3](https://github.com/PyO3/pyo3/)
- this is an "FFI generator" (i.e. wraps the raw C APIs in a nicer, more declarative interface)
- larger scope and harder to verify
- the [actual internals](https://github.com/PyO3/pyo3/tree/main/pyo3-ffi) use the C API

- Python manual reference
- https://docs.python.org/3/extending/index.html#creating-extensions-without-third-party-tools
- https://docs.python.org/3/c-api/index.html

- support for [opaque types](https://github.com/PyO3/pyo3/blob/554bc84c885e296622b629245b610623cd02c878/pyo3-ffi/src/lib.rs#L251-L259), such as [`PyObject*`](https://github.com/PyO3/pyo3/blob/9777faddc6464699f6580fb7b176989aacb5193f/pyo3-ffi/src/object.rs#L8-L9)
- make sure the generated snapshot domain is empty
- pure functions over opaque types, e.g. [`Py_IsNone`](https://github.com/PyO3/pyo3/blob/9777faddc6464699f6580fb7b176989aacb5193f/pyo3-ffi/src/object.rs#L495)
- incl. marking external functions as pure
- incref/decref -> obligations
- incref creates an obligation
- decref consumes it
- pass it around? certain C APIs expect incref'd instances, although docs are very unclear for this

- assorted topics to tackle
- [exception handling](https://docs.python.org/3/c-api/exceptions.html) - deal with exceptions (obligation?) after calls that might throw
- [buffer protocol](https://docs.python.org/3/c-api/buffer.html) - verify accesses are in-bounds

- [survey of common problems](https://onlinelibrary.wiley.com/doi/abs/10.1002/smr.2507), table on page 11:
- mishandling exceptions
- insufficient error checking
- memory management flaws
- integer overflows
- API evolution flaws
- buffer overflow
- reference counting errors
- type misuses
- GIL bugs

## Encoding obligations in Prusti

- pure functions are insufficient for resource reasoning without manual heap versioning

  #[pure] fn resource(uid: i32);

  #[requires(resource(uid))]
  #[ensures(...?)] // resource(uid) will always be true in the postcondition
  fn consume_resource(uid: i32) { ... }

- use owned types: arguments for consumed resources, additional return values for created resources

  struct Resource;
  fn consume_resource(x: Resource) { ... }

- ideally: ghost arguments, for now actual (ZST) arguments and wrappers over external APIs
- [`ManuallyDrop`](https://doc.rust-lang.org/std/mem/struct.ManuallyDrop.html) on resource types to prevent leakage and to model obligations specifically (cannot simply forget an obligation resource)

- `#[resource]` or `#[obligation]` attributes in Prusti?
- ensure type is ZST
- ensure `ManuallyDrop` is implemented and the correct Prusti-specific error is emitted
- (future: ensure type is only used in ghost code, ghost arguments, ghost returns, ghost fields)