---
# System prepended metadata

title: 'Prusti PW project: FFI specification'
tags: [' prusti-student-projects', prusti]

---

---
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

```rust=
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)
