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: 8 additions & 1 deletion .github/workflows/abi-ffi-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,15 @@ jobs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install Julia 1.11.5
run: |
curl -fsSL https://julialang-s3.julialang.org/bin/linux/x64/1.11/julia-1.11.5-linux-x86_64.tar.gz -o /tmp/julia.tar.gz
tar -xf /tmp/julia.tar.gz -C /tmp
echo "/tmp/julia-1.11.5/bin" >> "$GITHUB_PATH"
- name: Run ABI-FFI gate
run: python3 scripts/abi-ffi-gate.py
run: |
julia --version # confirms the pinned 1.11.5 is on PATH, not the runner default
julia scripts/abi-ffi-gate.jl

zig-build:
name: Zig FFI builds + tests (Zig 0.14.0)
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/rust-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ permissions:

jobs:
rust-ci:
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@8dc2bf039d1ff0372d650895c46bea7fbaec68ff
8 changes: 3 additions & 5 deletions benches/typedqliser_bench.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
//! - `schema_check` and `type_check` overhead per query size.
//! - Plugin creation cost.

use criterion::{black_box, criterion_group, criterion_main, BenchmarkId, Criterion, Throughput};
use criterion::{BenchmarkId, Criterion, Throughput, black_box, criterion_group, criterion_main};
use typedqliser::plugins::{ColumnDef, Schema, TableDef, get_plugin};

// ---------------------------------------------------------------------------
Expand All @@ -19,17 +19,15 @@ use typedqliser::plugins::{ColumnDef, Schema, TableDef, get_plugin};
const SMALL_QUERY: &str = "SELECT id FROM accounts WHERE id = 1";

/// Medium query (~180 bytes) — a two-table JOIN with a WHERE clause.
const MEDIUM_QUERY: &str =
"SELECT accounts.id, accounts.username, transactions.amount \
const MEDIUM_QUERY: &str = "SELECT accounts.id, accounts.username, transactions.amount \
FROM accounts \
INNER JOIN transactions ON accounts.id = transactions.account_id \
WHERE accounts.id > 10 AND transactions.amount > 0 \
ORDER BY transactions.amount DESC \
LIMIT 50";

/// Large query (~400 bytes) — a CTE + subquery + GROUP BY.
const LARGE_QUERY: &str =
"WITH high_value AS ( \
const LARGE_QUERY: &str = "WITH high_value AS ( \
SELECT account_id, SUM(amount) AS total \
FROM transactions \
WHERE amount > 100 \
Expand Down
116 changes: 116 additions & 0 deletions scripts/abi-ffi-gate.jl
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
#!/usr/bin/env julia
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# abi-ffi-gate.jl — fail (exit 1) if the Zig FFI does not conform to the Idris2
# ABI. The Idris2 ABI is the source of truth. Checks, with no compile toolchain
# needed (pure base-Julia text analysis):
#
# 1. the Zig FFI carries no unrendered `{{...}}` template tokens;
# 2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
# sources is exported by the Zig FFI (`export fn <name>`);
# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
# names and integer values (the `Error`/`err` spelling is treated as one).
#
# Usage: julia scripts/abi-ffi-gate.jl [repo_root] (defaults to cwd)
#
# Julia port of the former scripts/abi-ffi-gate.py (Python is banned estate-wide,
# RSR-H4); behaviour is identical.

"camelCase / PascalCase → snake_case (insert `_` before each non-initial capital)."
camel_to_snake(s) = lowercase(replace(s, r"(?<!^)(?=[A-Z])" => "_"))

"Canonical result-code key: lowercased, with `err`/`error` unified to `error`."
function canon_rc(name)
n = lowercase(name)
(n == "err" || n == "error") ? "error" : n
end

"Return {variant => value} for the C-ABI `Result` enum (the `enum(c_int)` block whose `ok = 0`), or empty."
function find_result_enum(zig::AbstractString)
best = Dict{String,Int}()
for m in eachmatch(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}"s, zig)
body = m.captures[1]
variants = Dict{String,Int}()
for vm in eachmatch(r"@?\"?([A-Za-z_][A-Za-z0-9_]*)\"?\s*=\s*(\d+)", body)
variants[canon_rc(vm.captures[1])] = parse(Int, vm.captures[2])
end
# The Result enum is the one starting at ok = 0.
if get(variants, "ok", nothing) == 0 && length(variants) > length(best)
best = variants
end
end
return best
end

"Collect every `*.idr` under `abi_dir`, skipping any `build/` output directory."
function idr_sources(abi_dir::AbstractString)
files = String[]
isdir(abi_dir) || return files
for (root, _dirs, fs) in walkdir(abi_dir)
occursin("/build/", root * "/") && continue
for f in fs
endswith(f, ".idr") && push!(files, joinpath(root, f))
end
end
return files
end

function main(root::AbstractString)::Int
name = basename(rstrip(abspath(root), '/'))
abi_dir = joinpath(root, "src/interface/abi")
zig_path = joinpath(root, "src/interface/ffi/src/main.zig")
errs = String[]

idr_files = idr_sources(abi_dir)
if isempty(idr_files)
println("ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir")
return 0
end
if !isfile(zig_path)
println("ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path")
return 1
end

idr = join((read(p, String) for p in idr_files), "\n")
zig = read(zig_path, String)

# 1. unrendered template tokens
toks = sort(unique(String(m.match) for m in eachmatch(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
isempty(toks) || push!(errs, "Zig FFI has unrendered template tokens: $(toks)")

# 2. foreign C symbols must be exported
csyms = sort(unique(String(m.captures[1]) for m in eachmatch(r"C:([A-Za-z0-9_]+)", idr)))
exports = Set(String(m.captures[1]) for m in eachmatch(r"export fn ([A-Za-z0-9_]+)", zig))
missing_syms = [s for s in csyms if !(s in exports)]
isempty(missing_syms) ||
push!(errs, "$(length(missing_syms)) ABI function(s) not exported by the Zig FFI: $(missing_syms)")

# 3. result-code map (names + values) must agree
idr_rc = Dict{String,Int}()
for m in eachmatch(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr)
idr_rc[canon_rc(camel_to_snake(m.captures[1]))] = parse(Int, m.captures[2])
end
zig_rc = find_result_enum(zig)
if !isempty(idr_rc) && isempty(zig_rc)
push!(errs, "no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
elseif !isempty(idr_rc) && !isempty(zig_rc) && idr_rc != zig_rc
push!(errs, "Result-code map differs (name or value):\n" *
" Idris resultToInt: $(sort(collect(idr_rc)))\n" *
" Zig Result enum: $(sort(collect(zig_rc)))")
end

if !isempty(errs)
println("ABI-FFI GATE: FAIL ($name)")
for e in errs
println(" - " * e)
end
return 1
end
println("ABI-FFI GATE: OK ($name) — $(length(csyms)) ABI functions exported, " *
"$(length(idr_rc)) result codes match")
return 0
end

root = length(ARGS) >= 1 ? ARGS[1] : "."
exit(main(root))
103 changes: 0 additions & 103 deletions scripts/abi-ffi-gate.py

This file was deleted.

19 changes: 9 additions & 10 deletions src/plugins/sql.rs
Original file line number Diff line number Diff line change
Expand Up @@ -205,18 +205,17 @@ impl SqlPlugin {
| BinaryOperator::Lt
| BinaryOperator::LtEq
| BinaryOperator::Gt
| BinaryOperator::GtEq => {
| BinaryOperator::GtEq
if lt_cat != rt_cat
&& lt_cat != TypeCategory::Unknown
&& rt_cat != TypeCategory::Unknown
{
issues.push(TypeIssue {
message: format!(
"Comparing incompatible types: {} ({:?}) vs {} ({:?})",
lt, lt_cat, rt, rt_cat
),
});
}
&& rt_cat != TypeCategory::Unknown =>
{
issues.push(TypeIssue {
message: format!(
"Comparing incompatible types: {} ({:?}) vs {} ({:?})",
lt, lt_cat, rt, rt_cat
),
});
}
_ => {}
}
Expand Down
10 changes: 5 additions & 5 deletions tests/e2e_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -137,10 +137,7 @@ fn e2e_unknown_table_fails_at_l2() {

assert!(plugin.parse_check(query).is_ok(), "L1 must pass");
let l2 = plugin.schema_check(query, &s).unwrap();
assert!(
!l2.is_empty(),
"E2E: unknown table must produce L2 issues"
);
assert!(!l2.is_empty(), "E2E: unknown table must produce L2 issues");
assert!(
l2.iter().any(|i| i.message.contains("ghost_table")),
"L2 issue must mention the missing table name"
Expand Down Expand Up @@ -307,7 +304,10 @@ fn e2e_cte_parses_at_l1() {
let plugin = get_plugin("sql").unwrap();
let query = "WITH top_accounts AS (SELECT id FROM accounts WHERE balance > 100) \
SELECT id FROM top_accounts";
assert!(plugin.parse_check(query).is_ok(), "E2E: CTE must parse at L1");
assert!(
plugin.parse_check(query).is_ok(),
"E2E: CTE must parse at L1"
);
}

// ---------------------------------------------------------------------------
Expand Down
12 changes: 9 additions & 3 deletions tests/property_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,10 @@ const CORPUS: &[(&str, &str)] = &[
// 0 — simple valid select
("simple_select", "SELECT 1"),
// 1 — select from known table (requires schema)
("select_known", "SELECT id, username FROM accounts WHERE id = 1"),
(
"select_known",
"SELECT id, username FROM accounts WHERE id = 1",
),
// 2 — invalid syntax
("invalid_syntax", "NOT SQL AT ALL @@@ !!!"),
// 3 — type mismatch: integer vs string
Expand All @@ -45,7 +48,10 @@ const CORPUS: &[(&str, &str)] = &[
"SELECT id FROM accounts WHERE id IN (SELECT account_id FROM transactions)",
),
// 9 — aggregate
("aggregate", "SELECT account_id, COUNT(*) FROM transactions GROUP BY account_id"),
(
"aggregate",
"SELECT account_id, COUNT(*) FROM transactions GROUP BY account_id",
),
];

// ---------------------------------------------------------------------------
Expand Down Expand Up @@ -333,7 +339,7 @@ fn property_no_panic_on_full_corpus() {
// We cannot move plugin/s into catch_unwind easily, so we just
// verify the calls succeed outside of catch_unwind — if they
// panic, the test fails.
drop(label);
let _ = label;
});
let _ = plugin.schema_check(query, &s);
let _ = plugin.type_check(query, &s);
Expand Down
Loading