Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions src/mem/heap.h
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,15 @@
* Checked by HNSW builtins before dereferencing. User must (hnsw-free h). */
#define RAY_ATTR_HNSW 0x04

/* I64 atom carries an owning dl_program_t* (a Datalog program) in its .i64
* slot. Checked by the dl-* builtins before dereferencing, so a forged/plain
* integer or an arithmetic copy (which drops attrs) is rejected with a type
* error instead of being reinterpreted as a pointer — see dl_unwrap_program.
* Reuses 0x20 (RAY_ATTR_SORTED on vectors / ATTR_QUOTED on -RAY_SYM); the
* -RAY_I64 type tag disambiguates, and no free-path or generic check reads
* 0x20 on a -RAY_I64 atom. User must (dl-free h). */
#define RAY_ATTR_DLPROG 0x20

/* Vector is a linked column. The 8 bytes of the aux union at offset
* 8 (i.e. parent->_idx_pad / parent->slice_offset / parent->str_pool
* slot, depending on which arm is in use) hold an int64
Expand Down
31 changes: 21 additions & 10 deletions src/ops/datalog.c
Original file line number Diff line number Diff line change
Expand Up @@ -4409,18 +4409,23 @@ ray_t* ray_query_fn(ray_t** args, int64_t n) {
* Programmatic Datalog API builtins
* ══════════════════════════════════════════ */

/* Opaque handle for dl_program_t stored in a ray_t atom.
* We store the pointer in the i64 field. */
/* Opaque handle for dl_program_t stored in a ray_t atom. The pointer lives
* in the i64 field, tagged with RAY_ATTR_DLPROG so dl_unwrap_program can reject
* a plain integer (or an arithmetic copy, which does not carry the attr)
* instead of dereferencing an arbitrary value as a dl_program_t*. Mirrors the
* RAY_ATTR_GRAPH / RAY_ATTR_HNSW handle scheme. */
static ray_t* dl_wrap_program(dl_program_t* prog) {
ray_t* obj = ray_alloc(0);
if (!obj || RAY_IS_ERR(obj)) return ray_error("oom", NULL);
obj->type = -RAY_I64;
obj->i64 = (int64_t)(uintptr_t)prog;
obj->attrs |= RAY_ATTR_DLPROG;
return obj;
}

static dl_program_t* dl_unwrap_program(ray_t* obj) {
if (!obj || obj->type != -RAY_I64) return NULL;
if (!obj || obj->type != -RAY_I64 || !(obj->attrs & RAY_ATTR_DLPROG))
return NULL;
return (dl_program_t*)(uintptr_t)obj->i64;
}

Expand Down Expand Up @@ -4514,16 +4519,22 @@ ray_t* ray_dl_provenance_fn(ray_t* prog_obj, ray_t* pred_obj) {
/* (dl-free prog) — free a dl-program handle created by (dl-program).
* The handle wraps a raw dl_program_t* with no automatic finalizer, so
* without an explicit free the program block and all relation tables it
* owns leak. Idempotent: zeroes the handle so a second call is a no-op
* (returns false) instead of double-freeing. */
* owns leak. On free we clear RAY_ATTR_DLPROG and zero the pointer, so a
* second call is an idempotent no-op (returns false) rather than a
* double-free. A tagged pointer that isn't an i64 is a type error, and a
* plain/forged integer (RAY_ATTR_DLPROG absent, non-zero value) is rejected
* as a type error instead of being dereferenced as a dl_program_t*. */
ray_t* ray_dl_free_fn(ray_t* x) {
if (!x || x->type != -RAY_I64)
return ray_error("type", "dl-free: arg must be a dl-program");
dl_program_t* prog = dl_unwrap_program(x);
if (!prog) return ray_bool(false); /* already freed / null handle */
dl_program_free(prog);
x->i64 = 0;
return ray_bool(true);
if (x->attrs & RAY_ATTR_DLPROG) {
dl_program_free((dl_program_t*)(uintptr_t)x->i64);
x->attrs &= (uint8_t)~RAY_ATTR_DLPROG;
x->i64 = 0;
return ray_bool(true);
}
if (x->i64 == 0) return ray_bool(false); /* already-freed handle: idempotent */
return ray_error("type", "dl-free: not a dl-program handle");
}

/* Reset global Datalog rule storage (called from ray_lang_destroy) */
Expand Down
18 changes: 18 additions & 0 deletions test/rfl/datalog/datalog_coverage.rfl
Original file line number Diff line number Diff line change
Expand Up @@ -544,6 +544,24 @@
(dl-query FP 'edge) !- type
(dl-free 'notprog) !- type

;; --- Claim 5b: forged/copied dl-program handles must not be dereferenced ---
;; A plain integer is NOT a dl-program handle. Every dl-* builtin that unwraps
;; one must reject it with a type error rather than reinterpreting the value as
;; a dl_program_t* pointer — before the RAY_ATTR_DLPROG tag check, (dl-free 1)
;; and friends dereferenced address 1 and crashed with SIGSEGV.
(dl-free 1) !- type
(dl-stratify 1) !- type
(dl-eval 1) !- type
(dl-query 1 'edge) !- type
(dl-add-edb 1 'edge (table ['a 'b] (list [1] [2])) 2) !- type
;; An arithmetic copy of a live handle drops the tag (attrs are not carried
;; through arithmetic), so it can't be freed — which would otherwise
;; double-free the original. The original still frees exactly once.
(set CP (dl-program))
(set CPcopy (+ CP 0))
(dl-free CPcopy) !- type
(dl-free CP) -- true


;; --- Claim 4: fixpoint non-convergence must error loudly, not return a partial result ---
;; Reachability over a linear chain needs ~N iterations. The loop caps at 1000.
Expand Down
Loading