blob: d43b44ade35ce14e5a6806c7eaad25623c5723de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
Problem description:
====================
There's a collection of hard-coded FFI hooks in `miri.cpp` to handle both API
rules (e.g. that the `write` syscall takes a count and a buffer of at least
that valid size) and wrapping non-trivial or dangerous calls (e.g. the pthread
ones).
It would be more useful to have a runtime description/encoding of these APIs
that runs safety checks and handles the magic.
Requirements
============
- Validity checks (pointer validity, tags)
- These checks should provide useful error messages
- Returned allocation tagging (valid size, opaque tags)
- Some returned allocations can be complex
- Completely re-definining operations
- E.g. replacing pthread APIs with checked versions
Design Ideas
============
Raw MIR?
-------
- Downside: How would it differ from actual MIR?
Basic-alike instruction sequence
--------------------------------
- All lines start with a keyword
- `ASSIGN`
- `LET`
- `CALL`
Simplified rust-ish language
----------------------------
- Basic type inference (uni-directional)
- Full AST
|
