search

flux-rs / flux

Refinement Types for Rust
MIT License
648 stars 21 forks source link

Tracking issue: Tock errors #740

Open enjhnsn2 opened 2 months ago

enjhnsn2 commented 2 months ago

This issue is intended to track progress on supporting Tock kernel code. Below, I have made two tables describing the code that we currently have to ignore or trust in Tock. As I create minimized examples and create issues for these individual bugs, I will add links here

Trusted functions

Category Num bugs Example Related issues
ICE: to_sort_list called on bound variable list with non-refinements 6 PrioritySched::next #808
ICE: Expected array or slice type 5 ReadableProcessSlice::copy_to_slice_or_err #733
Error jumping to join point 4 Kernel::process_each #702
assignment might be unsafe caused by extern spec on Option 2 ProcessStandard::switch_to #782
Cannot move out of non-strong reference 1 ProcessStandard::create #671
ICE: incompatible types 1 ProcessGrant::access_grant_with_allocator
ICE: Invalid deref of *mut 1 assign_gpios
Other (below) 11 N/A N/A
Total 31 N/A N/A

Here I outline the functions that are trusted because of valid refinement errors (i.e., Arithmetic errors, OOB, can't prove predondition, etc.) for my own use.

Other

Category Num functions Reasons
Arithmetic 7 Need range spec, bitwise logic
Refinement 3
??? 1
Total 11