atsiser 0.1.0

Wrap C codebases in ATS linear types for zero-cost memory safety without rewrites
Documentation 
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
47
48
49
50
51
52

# SPDX-License-Identifier: PMPL-1.0-or-later
# atsiser example: safe-malloc
#
# Wraps standard C memory allocation (malloc/free/realloc) with ATS2 linear
# types. After wrapping, the ATS2 type-checker guarantees:
# - Every malloc'd pointer is freed exactly once
# - No use-after-free (the linear type is consumed by free)
# - No double-free (the linear type can only be consumed once)
# - Borrows (e.g., memcpy, strlen) do not consume the resource

[project]
name = "safe-malloc"
version = "0.1.0"
description = "ATS2 linear type wrappers for malloc/free/realloc"
output-dir = "generated/ats"

[[c-sources]]
path = "include/stdlib_subset.h"
include-dirs = ["include"]
description = "Subset of stdlib.h with memory allocation functions"

[[ownership-rules]]
function = "malloc"
pattern = "alloc"
resource-type = "void"
description = "Allocates size bytes; returns pointer that must be freed"

[[ownership-rules]]
function = "free"
pattern = "free"
param-index = 0
resource-type = "void"
description = "Deallocates a malloc'd pointer"

[[ownership-rules]]
function = "realloc"
pattern = "transfer"
param-index = 0
resource-type = "void"
description = "Transfers ownership: old pointer consumed, new pointer returned"

[[ownership-rules]]
function = "memcpy"
pattern = "borrow"
param-index = 0
description = "Borrows dest and src pointers for copying"

[ats2]
patsopt = "patsopt"
patscc = "patscc"
flags = ["-DATS_MEMALLOC_LIBC"]
c-flags = ["-O2", "-Wall"]