Skip to content

Commit e582563

Browse files
hyperpolymathclaude
andcommitted
feat: implement Phase 1 — manifest, codegen pipeline, ABI types, and tests
Implement the complete atsiser Phase 1 pipeline for wrapping C codebases in ATS2 linear types with zero-cost memory safety: Manifest (src/manifest/mod.rs): - [project], [[c-sources]] (path, include-dirs), [[ownership-rules]] (function, pattern: alloc/free/borrow/transfer), [ats2] (compiler flags) - Validation, init template generation, info display Codegen pipeline (src/codegen/): - parser.rs: regex-based C header parser extracting function signatures with heuristic alloc/free/borrow pattern detection - ats_gen.rs: generates ATS2 viewtype wrappers (.sats/.dats) from parsed C signatures and ownership rules, with proof obligations - compiler.rs: constructs patsopt/patscc commands for ATS2 compilation ABI types (src/abi/mod.rs): - OwnershipPattern, Viewtype (standard/nullable/sized), LinearPtr, MemorySafetyProof (alloc/free/borrow/bounds/null-check), ATSModule, ATSFunction, ATSParam — with ATS2 source generation Tests: 32 unit tests + 12 integration tests covering manifest round-trip, C header parsing, ownership detection, module generation, code rendering, compiler commands, and end-to-end file generation. Example: examples/safe-malloc/ with stdlib_subset.h and atsiser.toml. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 8bc8866 commit e582563

13 files changed

Lines changed: 3803 additions & 54 deletions

File tree

Cargo.lock

Lines changed: 945 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ anyhow = "1"
1818
thiserror = "2"
1919
handlebars = "6"
2020
walkdir = "2"
21+
regex = "1"
2122

2223
[dev-dependencies]
2324
tempfile = "3"

examples/safe-malloc/atsiser.toml

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# atsiser example: safe-malloc
3+
#
4+
# Wraps standard C memory allocation (malloc/free/realloc) with ATS2 linear
5+
# types. After wrapping, the ATS2 type-checker guarantees:
6+
# - Every malloc'd pointer is freed exactly once
7+
# - No use-after-free (the linear type is consumed by free)
8+
# - No double-free (the linear type can only be consumed once)
9+
# - Borrows (e.g., memcpy, strlen) do not consume the resource
10+
11+
[project]
12+
name = "safe-malloc"
13+
version = "0.1.0"
14+
description = "ATS2 linear type wrappers for malloc/free/realloc"
15+
output-dir = "generated/ats"
16+
17+
[[c-sources]]
18+
path = "include/stdlib_subset.h"
19+
include-dirs = ["include"]
20+
description = "Subset of stdlib.h with memory allocation functions"
21+
22+
[[ownership-rules]]
23+
function = "malloc"
24+
pattern = "alloc"
25+
resource-type = "void"
26+
description = "Allocates size bytes; returns pointer that must be freed"
27+
28+
[[ownership-rules]]
29+
function = "free"
30+
pattern = "free"
31+
param-index = 0
32+
resource-type = "void"
33+
description = "Deallocates a malloc'd pointer"
34+
35+
[[ownership-rules]]
36+
function = "realloc"
37+
pattern = "transfer"
38+
param-index = 0
39+
resource-type = "void"
40+
description = "Transfers ownership: old pointer consumed, new pointer returned"
41+
42+
[[ownership-rules]]
43+
function = "memcpy"
44+
pattern = "borrow"
45+
param-index = 0
46+
description = "Borrows dest and src pointers for copying"
47+
48+
[ats2]
49+
patsopt = "patsopt"
50+
patscc = "patscc"
51+
flags = ["-DATS_MEMALLOC_LIBC"]
52+
c-flags = ["-O2", "-Wall"]
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
/* SPDX-License-Identifier: PMPL-1.0-or-later */
2+
/* Subset of stdlib.h for atsiser safe-malloc example.
3+
*
4+
* These are the standard C memory allocation functions that atsiser wraps
5+
* with ATS2 linear types to provide compile-time memory safety guarantees.
6+
*/
7+
8+
#ifndef STDLIB_SUBSET_H
9+
#define STDLIB_SUBSET_H
10+
11+
#include <stddef.h>
12+
13+
/* Allocate SIZE bytes of memory. Returns a pointer that MUST be freed. */
14+
void* malloc(size_t size);
15+
16+
/* Free a block allocated by malloc/realloc. Pointer MUST NOT be used after. */
17+
void free(void* ptr);
18+
19+
/* Re-allocate a block to NEW_SIZE bytes. Old pointer is CONSUMED. */
20+
void* realloc(void* ptr, size_t new_size);
21+
22+
/* Copy N bytes from SRC to DEST. Both pointers are BORROWED (not consumed). */
23+
void* memcpy(void* dest, const void* src, size_t n);
24+
25+
/* Set N bytes of DEST to VALUE. Pointer is BORROWED. */
26+
void* memset(void* dest, int value, size_t n);
27+
28+
#endif /* STDLIB_SUBSET_H */

0 commit comments

Comments
 (0)