|
| 1 | +# Spacecraft C (Clang) Guidelines — Full Reference |
| 2 | + |
| 3 | +**Version:** 1.0 |
| 4 | +**Date:** 2026-07-13 |
| 5 | +**Author:** Mohamed Hammad & Spacecraft Software |
| 6 | +**Compatibility:** Clang 18+ (with `-fbounds-safety`), GCC 12+, Fil-C Compiler |
| 7 | + |
| 8 | +This document expands on the `SKILL.md` for C systems programming. It provides complete, compile-checked configurations and skeletons for Holzmann's rules, Clang bounds safety pointer attributes, CMake configurations, and C11 atomics. |
| 9 | + |
| 10 | +--- |
| 11 | + |
| 12 | +## 1. Holzmann's Rules: Bounded Loops & Preallocated Arrays |
| 13 | + |
| 14 | +Gerard J. Holzmann's NASA Power of 10 rules ban dynamic memory allocations after initialization and require all loops to have constant upper bounds that can be statically verified. |
| 15 | + |
| 16 | +```c |
| 17 | +#include <stdio.h> |
| 18 | +#include <stdint.h> |
| 19 | +#include <stdbool.h> |
| 20 | +#include <assert.h> |
| 21 | + |
| 22 | +#define MAX_TELEMETRY_SIZE 256 |
| 23 | +#define MAX_LOOP_LIMIT 1000 |
| 24 | + |
| 25 | +typedef struct { |
| 26 | + uint32_t sensor_id; |
| 27 | + float value; |
| 28 | +} TelemetryPacket; |
| 29 | + |
| 30 | +// Static pre-allocated pool (Rule 3: No dynamic allocation after initialization) |
| 31 | +static TelemetryPacket telemetry_pool[MAX_TELEMETRY_SIZE]; |
| 32 | +static uint32_t pool_count = 0; |
| 33 | + |
| 34 | +// Function length is short (Rule 4: fits on one page) |
| 35 | +bool register_packet(uint32_t id, float val) { |
| 36 | + // Assertions verify preconditions (Rule 5: high assertion density) |
| 37 | + assert(val >= -100.0f); |
| 38 | + assert(val <= 100.0f); |
| 39 | + |
| 40 | + if (pool_count >= MAX_TELEMETRY_SIZE) { |
| 41 | + return false; |
| 42 | + } |
| 43 | + |
| 44 | + // Small variable scope (Rule 6) |
| 45 | + TelemetryPacket *packet = &telemetry_pool[pool_count]; |
| 46 | + packet->sensor_id = id; |
| 47 | + packet->value = val; |
| 48 | + pool_count++; |
| 49 | + |
| 50 | + return true; |
| 51 | +} |
| 52 | + |
| 53 | +float calculate_average(void) { |
| 54 | + // Rule 7: check parameters/state |
| 55 | + if (pool_count == 0) { |
| 56 | + return 0.0f; |
| 57 | + } |
| 58 | + |
| 59 | + float sum = 0.0f; |
| 60 | + |
| 61 | + // Rule 2: Loop must have a statically verifiable upper bound (MAX_TELEMETRY_SIZE) |
| 62 | + for (uint32_t i = 0; i < MAX_TELEMETRY_SIZE; ++i) { |
| 63 | + if (i >= pool_count) { |
| 64 | + break; // loop terminated safely before max bound |
| 65 | + } |
| 66 | + sum += telemetry_pool[i].value; |
| 67 | + } |
| 68 | + |
| 69 | + return sum / (float)pool_count; |
| 70 | +} |
| 71 | +``` |
| 72 | +
|
| 73 | +--- |
| 74 | +
|
| 75 | +## 2. Clang Bounds Safety Pointer Attributes (`-fbounds-safety`) |
| 76 | +
|
| 77 | +Clang's `-fbounds-safety` extension enables compile-time and runtime bounds checks for pointers in C. Use annotations like `__counted_by` to link pointer variables to length inputs. |
| 78 | +
|
| 79 | +```c |
| 80 | +#include <stdint.h> |
| 81 | +#include <stddef.h> |
| 82 | +#include <assert.h> |
| 83 | +
|
| 84 | +// __counted_by(count) ensures ptr dereferences are checked against count |
| 85 | +void process_readings(const float *__counted_by(count) readings, size_t count) { |
| 86 | + // Validate parameters at entry |
| 87 | + if (readings == NULL || count == 0) { |
| 88 | + return; |
| 89 | + } |
| 90 | +
|
| 91 | + for (size_t i = 0; i < count; ++i) { |
| 92 | + // Under -fbounds-safety, this index access is automatically bounds-checked. |
| 93 | + // Attempting to read index i >= count traps out-of-bounds and panics at runtime. |
| 94 | + float value = readings[i]; |
| 95 | + assert(value >= 0.0f); |
| 96 | + } |
| 97 | +} |
| 98 | +``` |
| 99 | + |
| 100 | +--- |
| 101 | + |
| 102 | +## 3. CMakeLists.txt Hardened Configuration |
| 103 | + |
| 104 | +Force warnings-as-errors diagnostics and configure sanitizers and bounds safety compiler flags. |
| 105 | + |
| 106 | +```cmake |
| 107 | +cmake_minimum_required(VERSION 3.20) |
| 108 | +project(SpacecraftC C) |
| 109 | +
|
| 110 | +set(CMAKE_C_STANDARD 11) |
| 111 | +set(CMAKE_C_STANDARD_REQUIRED ON) |
| 112 | +
|
| 113 | +# Enforce strict compiler warnings |
| 114 | +add_compile_options(-Wall -Wextra -Wpedantic -Werror) |
| 115 | +
|
| 116 | +# Compiler hardening modes |
| 117 | +if(CMAKE_C_COMPILER_ID STREQUAL "Clang") |
| 118 | + # Enable Clang bounds safety extension |
| 119 | + add_compile_options(-fbounds-safety) |
| 120 | + |
| 121 | + # Configure AddressSanitizer and UndefinedBehaviorSanitizer for testing builds |
| 122 | + if(CMAKE_BUILD_TYPE STREQUAL "Debug") |
| 123 | + add_compile_options(-fsanitize=address,undefined -fno-omit-frame-pointer) |
| 124 | + add_link_options(-fsanitize=address,undefined) |
| 125 | + endif() |
| 126 | +elseif(CMAKE_C_COMPILER_ID STREQUAL "GNU") |
| 127 | + # Enable GCC hardening assertions |
| 128 | + add_compile_definitions(_GLIBCXX_ASSERTIONS _FORTIFY_SOURCE=3) |
| 129 | + add_compile_options(-fhardened -fstack-protector-strong) |
| 130 | +endif() |
| 131 | +
|
| 132 | +add_executable(telemetry_c_node main.c telemetry.c) |
| 133 | +``` |
| 134 | + |
| 135 | +--- |
| 136 | + |
| 137 | +## 4. Concurrency: C11 Threads & Atomics |
| 138 | + |
| 139 | +Manage concurrency using standard C11 threads (`<threads.h>`) and atomic operations (`<stdatomic.h>`) to avoid race conditions. |
| 140 | + |
| 141 | +```c |
| 142 | +#include <threads.h> |
| 143 | +#include <stdatomic.h> |
| 144 | +#include <stdbool.h> |
| 145 | +#include <stdio.h> |
| 146 | + |
| 147 | +// Atomic variables prevent data races |
| 148 | +static _Atomic bool running = true; |
| 149 | +static _Atomic uint64_t packet_counter = 0; |
| 150 | + |
| 151 | +int worker_task(void *arg) { |
| 152 | + (void)arg; |
| 153 | + |
| 154 | + while (atomic_load(&running)) { |
| 155 | + // Perform non-blocking I/O or polling... |
| 156 | + thrd_sleep(&(struct timespec){.tv_sec = 0, .tv_nsec = 50000000}, NULL); |
| 157 | + |
| 158 | + // Safe atomic increment |
| 159 | + atomic_fetch_add(&packet_counter, 1); |
| 160 | + } |
| 161 | + return 0; |
| 162 | +} |
| 163 | + |
| 164 | +int main(void) { |
| 165 | + thrd_t thread; |
| 166 | + |
| 167 | + // Launch worker thread |
| 168 | + if (thrd_create(&thread, worker_task, NULL) != thrd_success) { |
| 169 | + return 1; |
| 170 | + } |
| 171 | + |
| 172 | + // Run for a short duration |
| 173 | + thrd_sleep(&(struct timespec){.tv_sec = 1, .tv_nsec = 0}, NULL); |
| 174 | + |
| 175 | + // Stop worker thread cooperatively |
| 176 | + atomic_store(&running, false); |
| 177 | + |
| 178 | + // Join thread to prevent leak |
| 179 | + int res; |
| 180 | + thrd_join(thread, &res); |
| 181 | + |
| 182 | + printf("Processed %lu packets.\n", atomic_load(&packet_counter)); |
| 183 | + return 0; |
| 184 | +} |
| 185 | +``` |
| 186 | +
|
| 187 | +--- |
| 188 | +
|
| 189 | +## 5. Legacy C Safety: Fil-C Compiler Setup |
| 190 | +
|
| 191 | +Compile legacy C source code with **Fil-C** to enforce dynamic bounds checks and block memory exploits. |
| 192 | +
|
| 193 | +### Compilation commands |
| 194 | +```bash |
| 195 | +# Configure Fil-C compiler paths |
| 196 | +export CC=/usr/local/fil-c/bin/clang |
| 197 | +
|
| 198 | +# Build C target |
| 199 | +$CC -O2 -std=c11 main.c -o telemetry_c_safe |
| 200 | +
|
| 201 | +# Executing the binary panics immediately on memory violations |
| 202 | +./telemetry_c_safe |
| 203 | +``` |
| 204 | + |
| 205 | +--- |
| 206 | + |
| 207 | +## 6. Common Pitfalls & Troubleshooting |
| 208 | + |
| 209 | +| Pitfall | Symptom | Corrective Action | |
| 210 | +| :--- | :--- | :--- | |
| 211 | +| **Dynamic allocations** | Memory leaks, heap fragmentation | Replace dynamic allocations with static memory pools. | |
| 212 | +| **Pointer arithmetic** | Out-of-bounds memory access | Wrap pointers with Clang `-fbounds-safety` attributes. | |
| 213 | +| **Data races on indices** | Undefined behaviors, race conditions| Lock mutexes or use C11 `<stdatomic.h>` primitives. | |
| 214 | +| **Unbounded loops** | Infinite loops, hang crashes | Enforce constant upper limits on loops. | |
| 215 | +| **Recursion** | Stack overflow crashes | Convert recursive algorithms into iterative loops. | |
| 216 | + |
| 217 | +--- |
| 218 | + |
| 219 | +## 7. Code Review Compliance Gate |
| 220 | + |
| 221 | +Before merging C code, verify: |
| 222 | +1. Dynamic heap actions are strictly forbidden after initialization. |
| 223 | +2. Every loop defines a constant upper limit. |
| 224 | +3. No recursive functions or jumping constructs are used. |
| 225 | +4. Function inputs check for `NULL` and return values are verified. |
| 226 | +5. Pointer arguments use `__counted_by` bounds safety attributes under Clang. |
| 227 | +6. C11 `<stdatomic.h>` variable updates are used for thread-safe state variables. |
| 228 | +7. Warnings compile cleanly with warnings-as-errors flag `-Werror`. |
0 commit comments