-
Notifications
You must be signed in to change notification settings - Fork 0
817 lines (759 loc) · 42.1 KB
/
Copy pathci.yml
File metadata and controls
817 lines (759 loc) · 42.1 KB
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
name: CI
# What this workflow asserts.
#
# The claim this package makes is that a C library ported once onto openkal runs
# above every implementation of the specification, so the claim is tested by
# running the same two programs on three systems and comparing what they produce
# against what the system's own tools produce.
#
# posix a program that opens a file by an absolute name, reads a
# variable, measures an interval, starts another program and waits
# for it --- thirty-two observations, none of which the program
# contains an implementation of
# wordcount the same counts as the system's own `wc'
#
# Two compiler families, gcc and llvm. The third of the three mcpp offers is
# absent from this package and the reason is recorded in the manifest: musl's
# four remaining assembly definitions are in an object format that toolchain
# does not assemble, so the question that toolchain would answer is not one this
# package can ask.
on:
push:
branches: [main]
pull_request:
workflow_dispatch:
inputs:
mcpp_ref:
description: "Branch of mcpp-community/mcpp to build and test against (empty = the released pin)"
required: false
default: ""
env:
MCPP_SOURCE_REF: ${{ github.event.inputs.mcpp_ref || vars.MCPP_SOURCE_REF }}
MCPP_VERSION: 2026.8.27.1
XLINGS_VERSION: v2026.8.17.2
XLINGS_NON_INTERACTIVE: '1'
jobs:
programs:
name: ${{ matrix.name }}
runs-on: ${{ matrix.os }}
timeout-minutes: 90
strategy:
fail-fast: false
matrix:
include:
# ⭐ `net`, `fork` and `shell` STATE WHAT THE BACKEND BENEATH THIS ROW
# PROVIDES, and they are part of the criterion rather than a
# convenience. openkal permits an implementation to decline an
# interface in whole (clause 3), so "the probe was not run" and "the
# probe was run and the refusal was the expected answer" are
# different outcomes, and only the second is evidence.
#
# ⭐⭐ `abort` NAMES WHAT EACH BACKEND'S `kal_abort` PRODUCES, AND IT IS
# THREE DIFFERENT THINGS ON PURPOSE.
#
# Until 0.6.0 `abort` did not end the program at all: musl's `raise` is
# `tkill`, this port had no case for it, and `abort` fell through to
# musl's own `a_crash()` --- `hlt` on x86_64 --- so every uncaught
# exception and every `assert` reported a segmentation fault. A row
# asserting only "the end was not an ordinary one" would have passed
# throughout that, because a fault is not an ordinary end either. So
# each row asserts the PARTICULAR end its implementation produces:
#
# --abort-signal SIGABRT: openkal-linux raises it with tgkill
# --abort-status exit 134: openkal-macos ends with a status no
# program returns
# --abort-terminated a termination rather than a return: Windows
# fail-fasts, and the fault this replaces was
# reported there as an exit
- { name: 'linux, gcc', os: ubuntu-24.04, toolchain: 'gcc@16.1.0', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-signal' }
- { name: 'linux, llvm', os: ubuntu-24.04, toolchain: 'llvm@22.1.8', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-signal' }
- { name: 'macos, llvm', os: macos-14, toolchain: 'llvm@20.1.7', target: '', net: 'yes', fork: '--fork', shell: '--shell', abort: '--abort-status' }
# ⚠️ openkal-windows declines `openkal.space`: this system has no
# primitive that copies an address space and starts a context in the
# copy, and inventing one would be the simulation clause 3.1
# forbids. `--no-fork` asserts the refusal.
- { name: 'windows, gcc', os: windows-2022, toolchain: 'gcc@16.1.0', target: 'x86_64-windows-gnu', net: 'yes', fork: '--no-fork', shell: '--no-shell', abort: '--abort-terminated' }
defaults:
run:
shell: bash
steps:
- uses: actions/checkout@v4
# WHAT IS COMMITTED NAMES NO DIRECTORY OF ANYBODY'S MACHINE.
#
# tools/working-trees.sh rewrites this manifest to name working trees and
# deliberately does not restore it: the rewrite must survive for the rest
# of the job. A run by hand therefore leaves the manifest naming absolute
# paths, and committing that publishes them --- a consumer resolving from
# the index is handed a manifest pointing at a directory that exists
# nowhere.
#
# ⚠️ THAT HAS HAPPENED. This step runs BEFORE the rewrite, so what it
# examines is what the commit contains rather than what the job has done
# to it.
- name: The committed manifest names no local directory
run: |
set -euo pipefail
bad=$(grep -nE '^[a-z-]+ = \{[^}]*path = "(/|[A-Za-z]:)' mcpp.toml || true)
if [ -n "$bad" ]; then
echo "::error::the committed manifest names an absolute path"
printf '%s\n' "$bad" | sed 's/^/ /'
echo " tools/working-trees.sh rewrites these and does not restore them;"
echo " run 'git checkout -- mcpp.toml' after using it by hand."
exit 1
fi
echo " ok every dependency is named by version or by a relative path"
- name: The specification and the implementation for this system
run: |
bash tools/working-trees.sh '${{ github.head_ref || github.ref_name }}' \
'${{ matrix.target }}'
- name: Install xlings (Unix)
if: runner.os != 'Windows'
run: |
curl -fsSL https://raw.githubusercontent.com/openxlings/xlings/main/tools/other/quick_install.sh \
| bash -s "$XLINGS_VERSION"
echo "$HOME/.xlings/subos/current/bin" >> "$GITHUB_PATH"
- name: Install xlings (Windows)
if: runner.os == 'Windows'
shell: pwsh
run: |
irm https://d2learn.org/xlings-install.ps1.txt | iex
"$env:USERPROFILE\.xlings\subos\current\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
- name: Install mcpp
run: |
xlings update
# ⚠️ THE PIN MAY NAME THE RELEASE THIS RUN IS VALIDATING, which does
# not exist yet — that is the whole point of MCPP_SOURCE_REF. Bootstrap
# from whatever the index has; the step below replaces it with the
# build under review, and the pin is what an ordinary run tests.
if [ -n "${MCPP_SOURCE_REF:-}" ]; then
xlings install mcpp -y -g
else
xlings install "mcpp@$MCPP_VERSION" -y -g
fi
mcpp --version
mcpp self config --mirror GLOBAL
# ⭐⭐ CROSS-VALIDATION: BUILD THE mcpp UNDER REVIEW AND USE THAT ONE.
#
# Empty in the ordinary run, so this job keeps testing the RELEASED
# mcpp the pin above names. Set it — `workflow_dispatch` input, or the
# repository variable — and the same job runs against that source.
#
# ⚠️ THIS EXISTS BECAUSE THE ORDER USED TO BE WRONG. Several mcpp
# releases went out green and only then turned this ecosystem red: the
# engine's own CI cannot see a defect that appears only in a real
# dependency graph, and this repository could not see the engine until
# it had been published. Validating before the release closes that gap.
#
# The released mcpp installed just above is the bootstrap that compiles
# it; mcpp builds itself and there is no other compiler for it here.
if [ -n "${MCPP_SOURCE_REF:-}" ]; then
src="$RUNNER_TEMP/mcpp-src"
[ -d "$src" ] || git clone --quiet --depth 1 \
--branch "$MCPP_SOURCE_REF" \
https://github.com/mcpp-community/mcpp.git "$src"
# ⚠️ THE CLONE'S OWN WORKSPACE PIN MUST NOT DECIDE WHICH mcpp
# BUILDS IT. `.xlings.json` at mcpp's root pins the mcpp that
# compiles mcpp, and that pin does not move when mcpp is released —
# so a build inside the checkout obeys it and tries to install a
# version the index may no longer carry:
#
# [error] xlings: version '2026.8.17.1' not found for 'mcpp'
# available: 2026.8.25.1
#
# What is wanted here is the source compiled by the mcpp installed
# above, which is exactly what removing the file leaves.
rm -f "$src/.xlings.json"
( cd "$src" && mcpp build --release )
# ⚠️ BOTH SPELLINGS, AND NO `-perm`. The matrix reaches Windows and
# macOS runners too: on Windows the artefact is `mcpp.exe`, and
# `-perm -u+x` is not a question that filesystem answers the way this
# expects. Measured: `Finished release [optimized] in 173.44s`
# followed by "mcpp did not build" — the build had succeeded and the
# search was looking for the wrong name.
#
# `$src` is a FRESH clone each run, so `target/` holds exactly what
# this step just built; `-printf` would be the safer form on a cached
# tree and is a GNU extension this must not use.
built=$(find "$src/target" -type f \
\( -name mcpp -o -name mcpp.exe \) | head -1)
[ -n "$built" ] || { echo "::error::mcpp did not build from $MCPP_SOURCE_REF"; exit 1; }
echo "$(cd "$(dirname "$built")" && pwd)" >> "$GITHUB_PATH"
# ⚠️ Reported, because a PATH entry that does not win looks exactly
# like one that does until something built with the wrong engine.
echo "under review: $("$built" --version) (from $MCPP_SOURCE_REF)"
fi
- name: Select the toolchain
run: |
spec='${{ matrix.toolchain }}'
mcpp toolchain install "${spec%@*}" "${spec#*@}"
mcpp toolchain default "$spec"
mcpp toolchain list
- name: The library builds
run: |
extra=''
[ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}'
mcpp build $extra
# ⭐ AN OPTIONAL INTERFACE IS REFERENCED WEAKLY, WHICH IS A PROPERTY OF
# THE OBJECT AND NOT OF ANY ONE LINK.
#
# `openkal.random` is optional, and clause 6.1 expresses an
# implementation that does not provide it as the absence of a link-time
# definition. This dispatcher is linked into every program, so a strong
# reference to `kal_random_fill` makes an optional interface mandatory:
# every program over a backend without it fails to link, whether or not
# it wanted a random byte.
#
# ⚠️ THAT DEFECT SHIPPED, AND NOTHING HERE SAW IT. It was found one
# repository downstream, by a bare-metal program in openkal-llvm-runtime
# linking over openkal-opensbi:
#
# ld.lld: error: undefined symbol: kal_random_fill
#
# Reproducing it here would need a bare-metal toolchain and a backend
# that declines the interface. The symbol class needs neither, and states
# the invariant more directly than a link would: `w` for the optional
# one, `U` for a required one beside it.
- name: An optional interface is referenced weakly
if: runner.os == 'Linux'
run: |
set -euo pipefail
# ⚠️ ONE FINGERPRINT DIRECTORY, ASSERTED BEFORE ANYTHING IS READ.
# `target/` accumulates one per configuration, and a search across all
# of them answers for a build that is not this one. The step that
# checks the withheld set already learned this; the assertion is made
# here for the same reason and not by reference to that one.
fps=$(ls -d target/*/*/ 2>/dev/null | wc -l)
[ "$fps" = 1 ] || { echo "::error::expected one fingerprint directory under target/, found $fps"
ls -d target/*/*/ 2>/dev/null | sed 's/^/ /'
exit 1; }
# ⚠️⚠️ AND THIS PACKAGE'S OWN OBJECTS, WHICH IS NOT WHAT A SEARCH UNDER
# `target/` FINDS. Measured while this step was extended: a search of
# everything under `target/` reported `kal_net_accept` and
# `kal_datagram_recv_from` as undefined STRONG references and the other
# nine as weak — because the DEPENDENCY's objects are there too, under
# `obj/mcpplibs_*`, and openkal-linux's `kal_timeout_accept` refers to
# its own `kal_net_accept` strongly. That is correct for an
# implementation and says nothing about this port.
objs=$(find target/*/*/obj -maxdepth 1 -name '*.o')
n=$(printf '%s\n' "$objs" | grep -c . || true)
echo " examining $n of this package's own objects"
[ "$n" -gt 100 ] || { echo "::error::only $n objects; nothing was examined"; exit 1; }
nm="$(command -v llvm-nm || command -v nm)"
"$nm" $objs > syms.txt 2>/dev/null || true
# The control: a required interface must still be a strong reference,
# so that a backend failing to provide one is still a link error.
grep -qE '^ *U kal_time_sleep$' syms.txt \
|| { echo "::error::kal_time_sleep is not an undefined strong reference — the check below proves nothing"
grep kal_time syms.txt; exit 1; }
grep -qE '^ *w kal_random_fill$' syms.txt \
|| { echo "::error::kal_random_fill is not a weak reference; an optional interface has been made mandatory"
grep kal_random syms.txt; exit 1; }
# ⭐⭐ AND THE SAME FOR EVERY INTERFACE THE 0.8 ROUTES REACH, WHICH IS
# WHY THIS STEP IS NOT A SINGLE ASSERTION ANY MORE.
#
# `openkal.net`, `openkal.datagram`, `openkal.timeout` and
# `openkal.space` are optional in exactly the sense `openkal.random`
# is, and openkal-opensbi and openkal-uefi decline all four. A strong
# reference to any one of them would make a bare-metal program that
# never opens a socket fail to link — which is the defect this step
# already exists because of, arriving through a different name.
#
# ⚠️ THE SYMBOL IS SOUGHT ACROSS THE PORT'S OBJECTS RATHER THAN IN ONE,
# because the routes are spread over three sources: okm_net.c,
# okm_poll.c and okm_fork.c. Naming one file would assert a property of
# that file and report nothing about the others.
weakfail=0
for name in kal_net_connect kal_net_listen kal_net_accept kal_net_close \
kal_datagram_open kal_datagram_recv_from \
kal_timeout_read kal_timeout_write kal_timeout_accept \
kal_timeout_wait_process \
kal_space_start kal_process_channel; do
if grep -qE "^ *U $name\$" syms.txt; then
echo "::error::$name is an undefined STRONG reference; an interface a backend may decline has been made mandatory"
weakfail=1
elif grep -qE "^ *w $name\$" syms.txt; then
echo " weak: $name"
else
echo "::error::$name is referenced nowhere; the route that was added does not call it"
weakfail=1
fi
done
[ "$weakfail" = 0 ] || exit 1
echo " ok every optional interface is referenced weakly, and kal_time_sleep is strong"
# ⚠️⚠️ AND ONE OF THEM IS AN OBJECT, WHICH IS NOT TESTED THE WAY THE
# ELEVEN ABOVE ARE.
#
# Every name above is a function, so `if (kal_net_connect)` tests the
# ADDRESS and is correct. `kal_process_props` is a capability word:
# the same spelling would READ it, and where the definition is absent
# the object sits at address zero --- so the test written to prevent a
# null dereference would be one. okm_opt.h takes the address, once, and
# every caller reaches the word through that.
#
# ⚠️ WHAT THIS STEP CAN AND CANNOT SEE. That the reference is weak, it
# can. That the source takes the address rather than reading the value,
# it cannot --- both forms leave a relocation. The rule is stated where
# it is used and asserted here only against the failure a link can
# produce: a strong reference, which would make a backend that declines
# `openkal.process` fail to link every program.
case "$(grep -E '^ *[wv] kal_process_props$' syms.txt | wc -l)" in
0) echo "::error::kal_process_props is not a weak reference in these objects"
grep kal_process_props syms.txt || echo " (it is referenced nowhere)"
exit 1 ;;
*) echo " weak object: kal_process_props" ;;
esac
# ⭐⭐ ASKING WHETHER A STREAM IS A TERMINAL GETS THE RIGHT ANSWER.
#
# musl's `isatty' asks with TIOCGWINSZ; this port answered only TCGETS,
# so every `isatty' returned 0 — for a real terminal as readily as for a
# pipe. Nothing failed: `std::print' simply never took its terminal path,
# and a program deciding on colour or on line buffering decided wrongly
# and in silence.
#
# ⭐ THE CRITERION IS A RELATION, NOT A VALUE. `isatty` under a pipe and
# under a pseudo-terminal must DIFFER, and must differ the same way the
# system's own C library does. A test asserting "0 in a pipe" alone would
# have passed throughout the defect.
- name: Asking whether a stream is a terminal is answered, not refused
if: runner.os == 'Linux' && matrix.target == ''
run: |
d="$(mktemp -d)"; mkdir -p "$d/src"
cat > "$d/mcpp.toml" <<TOML
[package]
name = "isattyprobe"
version = "0.1.0"
[dependencies]
openkal-musl = { path = "$PWD" }
[targets.isattyprobe]
kind = "bin"
main = "src/main.c"
[build]
cxx_runtime = "host-coupled"
TOML
sed -i 's/^ //' "$d/mcpp.toml"
printf '#include <unistd.h>\n#include <stdio.h>\nint main(void){ printf("%%d\\n", isatty(1)); return 0; }\n' > "$d/src/main.c"
( cd "$d" && mcpp build --toolchain '${{ matrix.toolchain }}' )
bin="$(find "$d/target" -name isattyprobe -type f | head -1)"
test -n "$bin" || { echo "::error::the probe did not build"; exit 1; }
# The control: the system's own C library, through the same harness.
# Without it a `script` that fails to allocate a pty would make the
# port look broken.
printf '#include <unistd.h>\n#include <stdio.h>\nint main(void){ printf("%%d\\n", isatty(1)); return 0; }\n' > "$d/ctrl.c"
cc "$d/ctrl.c" -o "$d/ctrl"
ctrl_pipe="$("$d/ctrl" | cat | tr -d '\r')"
ctrl_tty="$(script -qec "$d/ctrl" /dev/null | tr -d '\r' | head -1)"
[ "$ctrl_pipe" = 0 ] && [ "$ctrl_tty" = 1 ] \
|| { echo "::error::the harness cannot tell a pty from a pipe (control gave $ctrl_pipe/$ctrl_tty) — this check would prove nothing"
exit 1; }
port_pipe="$("$bin" | cat | tr -d '\r')"
port_tty="$(script -qec "$bin" /dev/null | tr -d '\r' | head -1)"
echo " control: pipe=$ctrl_pipe tty=$ctrl_tty port: pipe=$port_pipe tty=$port_tty"
[ "$port_pipe" = "$ctrl_pipe" ] && [ "$port_tty" = "$ctrl_tty" ] \
|| { echo "::error::isatty over this port disagrees with the system's own C library"; exit 1; }
echo " ok isatty answers the same as the system's own C library"
# ⭐⭐ THE INTERNAL OVERLAY STOPS AT THIS PACKAGE'S BOUNDARY.
#
# musl reaches its own declarations through `src/include`, whose headers
# define `hidden`, `weak` and `weak_alias` — names that mean something
# only to musl's own sources. This package publishes the path it is built
# from, so every consumer used to see them too, and which consumer broke
# on which name was found one at a time (openkal-musl#13).
#
# `[build] private_include_dirs` (mcpp 2026.8.27.1) says which entries of
# `include_dirs` stop here. This asserts the DIRECTORY is absent from a
# consumer's command line — not that one macro no longer collides, which
# would go green again the moment the package patched that macro while
# the leak stayed.
# WHAT IS WITHHELD IS NOT DEFINED BY THIS PACKAGE, AND WHAT IS NOT
# WITHHELD IS.
#
# ⚠️⚠️ THE CRITERION IS THE PACKAGE'S OWN OBJECTS, NOT A PROGRAM'S LINK.
#
# It was a program's link, and that measured the wrong thing. Under one
# toolchain the probe built successfully for symbols this package does not
# define at all --- something else on the link line supplied them --- so
# the check reported "did not fail at the link" for a facility that had in
# fact been withheld. A program's link is closed over this port only when
# nothing else answers, and that is a property of the toolchain rather than
# of this package.
#
# A definition either is in these objects or is not. That holds under every
# toolchain and cannot be satisfied by a host C library.
#
# ⚠️ AND THE OBJECTS ARE SCOPED TO ONE FINGERPRINT DIRECTORY. `target/`
# accumulates one per configuration, so a search across all of them reads
# definitions from a build made before the change --- which is how this
# check first reported every withheld symbol as still present.
- name: What is withheld is not defined, and what is not withheld is
if: runner.os == 'Linux' && matrix.target == ''
run: |
set -euo pipefail
fps=$(ls -d target/*/*/ 2>/dev/null | wc -l)
[ "$fps" = 1 ] || { echo "::error::expected one fingerprint directory under target/, found $fps"
ls -d target/*/*/ 2>/dev/null | sed 's/^/ /'
exit 1; }
objs=$(find target -name '*.o')
n=$(printf '%s\n' "$objs" | grep -c . || true)
echo " examining $n objects in $(ls -d target/*/*/)"
[ "$n" -gt 100 ] || { echo "::error::only $n objects; nothing was examined"; exit 1; }
defines() { # symbol -> the number of definitions in these objects
nm $objs 2>/dev/null | grep -cE "^[0-9a-f]+ [TWi] $1\$" || true
}
fail=0
for s in epoll_create1 eventfd timerfd_create inotify_init signalfd; do
d=$(defines "$s")
if [ "$d" = 0 ]; then echo " withheld, not defined: $s"
else echo "::error::$s is withheld and yet defined $d time(s)"; fail=1; fi
done
# The other half. Without it the check above would pass for a package
# that had stopped compiling anything at all. `pipe` is here because
# openkal 0.8 made it expressible; `socket` and `fork` because their
# closures reach the password functions and the thread implementation,
# so they are deliberately NOT withheld and the manifest says why.
for s in printf malloc open pipe faccessat chmod socket fork; do
d=$(defines "$s")
if [ "$d" -ge 1 ]; then echo " defined here: $s"
else echo "::error::$s is not withheld and yet is not defined"; fail=1; fi
done
[ "$fail" = 0 ] || exit 1
echo " ok the withheld set is exactly what the manifest names"
- name: What this package is built from is not what it publishes
working-directory: examples/cross-hello
run: |
extra=''
[ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}'
mcpp build --toolchain '${{ matrix.toolchain }}' $extra
test -s compile_commands.json \
|| { echo "::error::no compile_commands.json — nothing to check"; exit 1; }
# ⚠️⚠️ PER ROW, NOT OVER THE FILE. This example depends on the
# package by path, so THE PROVIDER'S OWN ROWS ARE IN THIS SAME FILE
# and they carry the overlay legitimately — that is what "private,
# not unused" means. A `grep` over the whole file cannot tell the two
# apart and would call the package's own build a leak.
#
# ⚠️ Separators are normalised because the Windows runner writes
# `…\musl\src\include`, and a check that silently stops matching on
# one platform is a check that platform does not have.
norm='(.arguments // (.command | split(" "))) | join(" ") | gsub("\\\\"; "/")'
jq -r ".[] | select((.file | gsub(\"\\\\\\\\\"; \"/\")) | test(\"examples/cross-hello\")) | $norm" \
compile_commands.json > consumer.txt
jq -r ".[] | select((.file | gsub(\"\\\\\\\\\"; \"/\")) | test(\"examples/cross-hello\") | not) | $norm" \
compile_commands.json > provider.txt
# ⚠️ DENOMINATORS ON BOTH SIDES. With no consumer row every absence
# below is vacuously true; with no provider row the control is.
cons="$(wc -l < consumer.txt)"; prov="$(wc -l < provider.txt)"
echo " rows: consumer=$cons provider=$prov"
[ "$cons" -ge 1 ] && [ "$prov" -ge 1 ] \
|| { echo "::error::consumer=$cons provider=$prov — nothing was checked"; exit 1; }
bad=0
for d in musl/src/include musl/src/internal musl-generated/internal; do
if grep -q -- "$d" consumer.txt; then
echo "::error::the internal overlay '$d' reached a consumer"
bad=1
fi
# The other half of the same key: private is not the same as
# dropped. musl's own sources must still reach their declarations.
grep -q -- "$d" provider.txt \
|| { echo "::error::'$d' is on nobody's command line — private_include_dirs withheld it from this package too"
bad=1; }
done
# And something PUBLIC must still cross the boundary, or this check
# would pass for a build that published nothing at all.
grep -q -- 'port/include' consumer.txt \
|| { echo "::error::no public include directory reached the consumer — the check above proves nothing"
exit 1; }
[ "$bad" = 0 ] || exit 1
echo " ok the internal overlay stops here; the public headers do not"
# A program above this package names one package. It does not name
# openkal, it does not name an implementation, and it says nothing about
# the platform.
#
# ⚠️ FOUR PROBES, ONE RUNNER. tools/run-probe.sh holds the watchdog, the
# report of where a program that stopped was, and the two readings of the
# output. Four copies of that would be four places for one of them to fall
# behind.
- name: The posix probe
env:
MCPP_TARGET: ${{ matrix.target }}
run: bash tools/run-probe.sh examples/posix posix
# ⭐ THE NAMES THIS LIBRARY MUST NOT TAKE FROM A PROGRAM ABOVE IT.
#
# Reported as openkal-musl#13. This one is a COMPILE-TIME criterion: the
# source declares `hidden`, `weak` and `weak_alias` as ordinary
# identifiers, and if any of the three is a macro again the file does not
# compile. It is run as well as built so that something links afterwards,
# which is what distinguishes a source that compiles from a package that
# works.
- name: A program may use the names the internal overlay defines
env:
MCPP_TARGET: ${{ matrix.target }}
run: |
bash tools/run-probe.sh examples/identifiers identifiers
grep -q 'hidden+weak+weak_alias = 41' examples/identifiers/run.log
# ⭐⭐ THE ROUTES openkal 0.8 MADE POSSIBLE, EXERCISED THROUGH POSIX.
#
# `socket`, `bind`, `listen`, `accept`, `connect`, `sendto`, `recvfrom`,
# `poll` and `select` reached this port's default arm and returned ENOSYS
# until `openkal.net`, `openkal.datagram` and `openkal.timeout` existed to
# route them onto (openkal-linux#13). The probe names no openkal symbol:
# a probe that called `kal_net_connect` to check that `connect` works
# would be checking the wrong thing.
#
# ⚠️ `matrix.net` DECIDES WHETHER THE ROW RUNS IT, and the value is a
# property of the BACKEND rather than of the system. A backend that
# declines `openkal.net` is behaving correctly; a row that expected it and
# silently did not get it is what this must not read as a pass.
- name: The network probe
if: matrix.net == 'yes'
env:
MCPP_TARGET: ${{ matrix.target }}
run: bash tools/run-probe.sh examples/net net
# Another program, started three ways. ⭐ WHAT IS EXPECTED IS PASSED IN
# RATHER THAN INFERRED: `--no-fork` requires that duplicating the calling
# image be REFUSED, so a system whose backend declines `openkal.space` is
# asserted to decline it rather than merely not asked.
- name: The subprocess probe
env:
MCPP_TARGET: ${{ matrix.target }}
run: bash tools/run-probe.sh examples/subprocess subprocess ${{ matrix.fork }} ${{ matrix.shell }} ${{ matrix.abort }}
# ⭐⭐ WHERE A STARTED PROGRAM'S OUTPUT WENT, WHICH THE PROBE CANNOT ASK
# ABOUT ITSELF.
#
# A caller that redirects descriptor 1 and then starts a program used to
# get the program's bytes on the stream IT had been started with, and the
# file it had redirected onto stayed empty (openkal-linux#13). The probe
# asserts the file; it cannot assert the other half, because a program
# cannot read its own output. This log is that output.
#
# ⚠️ BOTH DIRECTIONS, AND THE SECOND IS NOT DECORATION. Requiring only that
# the redirected markers are absent would pass for a library that had
# stopped letting a started program write anywhere at all; requiring only
# that the inherited one is present would pass for the defect. The probe's
# own messages are worded so that neither token can appear in one.
- name: A started program's output went where the caller sent it
working-directory: examples/subprocess
run: |
set -euo pipefail
test -s run.log || { echo "::error::no run.log — nothing to read"; exit 1; }
if grep -q 'redirected-bytes' run.log; then
echo "::error::a started program's output arrived on the caller's own stream"
grep -n 'redirected-bytes' run.log | sed 's/^/ /'
exit 1
fi
grep -q 'inherited-child-bytes' run.log \
|| { echo "::error::a started program that redirected nothing wrote nowhere; the check above proves nothing"
exit 1; }
echo " ok redirected output reached the file; inherited output reached the caller"
# ⭐ AN OPERATION THIS LIBRARY DOES NOT HAVE CAN SAY SO WHEN ASKED.
#
# The default arm of the dispatcher answers ENOSYS in silence, and the only
# way a consumer could learn WHICH operation was missing was to read
# port/src/okm_syscall.c. Two rounds of openkal-linux#13 went on that
# question.
#
# ⚠️ THREE OBSERVATIONS, BECAUSE THE INTERESTING FAILURES ARE THE QUIET
# ONES: a channel that reports nothing when asked, a channel that reports
# when it was not asked, and a channel that reports the same thing once per
# attempt so that a reader counting lines concludes it happened once.
- name: An absent operation reports which one it was, and only when asked
if: runner.os == 'Linux' && matrix.target == ''
run: |
set -euo pipefail
d="$(mktemp -d)"; mkdir -p "$d/src"
cat > "$d/mcpp.toml" <<TOML
[package]
name = "traceprobe"
version = "0.1.0"
[dependencies]
openkal-musl = { path = "$PWD" }
[targets.traceprobe]
kind = "bin"
main = "src/main.c"
[build]
cxx_runtime = "host-coupled"
TOML
sed -i 's/^ //' "$d/mcpp.toml"
# ⚠️⚠️ THE OPERATION THIS PROBE NAMES MUST STILL BE ABSENT, AND THE
# ONE IT NAMED STOPPED BEING SO.
#
# It was `symlinkat`, chosen because openkal had no atom that creates a
# link. openkal 0.9 added `kal_fs_link_create`, this dispatcher gained
# a case for it, and the probe --- unchanged, still green in intent ---
# began exercising an operation that now SUCCEEDS. It reported zero
# diagnostics for a hundred attempts, which is the same reading a
# broken diagnostic channel gives.
#
# ⭐ SO THE ABSENCE IS NOW ASSERTED RATHER THAN ASSUMED. `mknodat`
# creates a device node, which openkal does not express and is not
# going to; if a case for it ever appears, the grep below fails and
# says to pick another operation --- instead of this step passing
# while measuring nothing.
if grep -q 'SYS_mknodat' port/src/okm_syscall.c; then
echo "::error::the dispatcher now handles mknodat, so this probe no"
echo "::error::longer exercises an absent operation. Pick another"
echo "::error::operation openkal has no atom for and name it here."
exit 1
fi
# The number is printed by the probe rather than computed here, so the
# expectation comes from the same headers the dispatcher was compiled
# with; a number worked out on the host would answer for the host's C
# library.
printf '%s\n' \
'#include <sys/syscall.h>' \
'#include <sys/stat.h>' \
'#include <fcntl.h>' \
'#include <unistd.h>' \
'#include <stdio.h>' \
'int main(void) {' \
' for (int i = 0; i < 100; i++)' \
' (void)!mknodat(AT_FDCWD, "node", S_IFIFO | 0600, 0);' \
' printf("%ld\n", (long)SYS_mknodat);' \
' return 0;' \
'}' > "$d/src/main.c"
( cd "$d" && mcpp build --toolchain '${{ matrix.toolchain }}' )
bin="$(find "$d/target" -name traceprobe -type f | head -1)"
test -n "$bin" || { echo "::error::the probe did not build"; exit 1; }
want="$("$bin" 2> /dev/null)"
[ -n "$want" ] || { echo "::error::the probe printed no operation number"; exit 1; }
quiet="$("$bin" 2>&1 > /dev/null | wc -l)"
[ "$quiet" = 0 ] \
|| { echo "::error::the channel reported $quiet line(s) without being asked"
"$bin" 2>&1 > /dev/null | sed 's/^/ /'; exit 1; }
asked="$(OPENKAL_MUSL_TRACE=enosys "$bin" 2>&1 > /dev/null)"
echo " what it reported: $asked"
n="$(printf '%s\n' "$asked" | grep -c 'no operation for system call' || true)"
[ "$n" = 1 ] \
|| { echo "::error::expected exactly one report for one hundred attempts, got $n"
exit 1; }
printf '%s\n' "$asked" | grep -q "no operation for system call $want\$" \
|| { echo "::error::the report does not name the operation the probe asked for ($want)"
exit 1; }
echo " ok silent unless asked, one line per operation, and it names the operation"
- name: The same program, built the ordinary way, as a control
run: |
# ⚠️ THIS STEP EXISTS BECAUSE IT ALREADY EARNED ITS PLACE.
#
# The cross-built copy failed on a machine of the other system, and the
# obvious reading was a defect in this port or in the way it was
# cross-built. A native build of the SAME source reproduced it here ---
# which said it was neither, and the defect was in the program's own
# assertion macro, which evaluated its condition twice and so closed a
# stream that was already closed.
#
# Two failures that look alike are told apart by building the same
# source two ways, and that is cheap enough to do every time.
# ⚠️ The target has to be named here as it is everywhere else in this
# job: one system needs it, and a step that omitted it built for that
# system's other toolchain and failed at the link with names kernel32
# supplies. Measured, on the first run of this step.
extra=''
[ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}'
cd examples/cross-hello
mcpp build $extra
binary="$(bash "$GITHUB_WORKSPACE/tools/one-artifact.sh" cross-hello)"
"./$binary" 2>&1 | tee out.log
grep -q -- '-- failures: 0 --' out.log
- name: The counts agree with the system's own
working-directory: examples/wordcount
run: |
printf 'alpha beta\ngamma\n' > sample.txt
expected="$(wc < sample.txt | tr -s ' ' | sed 's/^ //')"
extra=''
[ -n '${{ matrix.target }}' ] && extra='--target ${{ matrix.target }}'
mcpp build $extra
binary="$(bash "$GITHUB_WORKSPACE/tools/one-artifact.sh" wordcount)"
WORDCOUNT_VERBOSE=1 "$binary" sample.txt 2>&1 | tee run.log
counts="$(sed -n 's/^lines \([0-9]*\) words \([0-9]*\) bytes \([0-9]*\)$/\1 \2 \3/p' run.log)"
test -n "$counts" || { echo "the program printed no count" >&2; exit 1; }
echo "wordcount: $counts"
echo "wc: $expected"
test "$counts" = "$expected"
# The variable was consulted, and the interval was measured.
grep -q 'elapsed .* nanoseconds' run.log
# ---------------------------------------------------------------------------
# The measurement musl/PATCHES.md records, made from a machine that is not the
# system it is about.
#
# It is a job rather than a note because the claim it supports --- that a
# program for that system can be built, and linked, without any file that
# system supplies --- is one that a change to this port could silently undo.
# The two numbers it asserts are zero indirect symbols and exactly two names.
cross-macos:
name: cross-link for the other system, from this one
runs-on: ubuntu-24.04
timeout-minutes: 30
steps:
- uses: actions/checkout@v4
- name: The implementation for that system
run: |
branch='${{ github.head_ref || github.ref_name }}'
git clone --quiet https://github.com/mcpplibs/openkal-macos.git ../openkal-macos
git -C ../openkal-macos checkout --quiet "origin/$branch" 2>/dev/null || true
git clone --quiet https://github.com/mcpplibs/openkal.git ../openkal
git -C ../openkal checkout --quiet "origin/$branch" 2>/dev/null || true
- name: Install LLVM
run: |
sudo apt-get update -qq
sudo apt-get install -y -qq clang lld llvm
# ld64.lld is the Mach-O driver of the same binary; Ubuntu's package
# installs it under a version suffix and without the plain name.
v=$(ls /usr/lib/llvm-*/bin/ld64.lld 2>/dev/null | sort -V | tail -1)
test -n "$v" || { echo "::error::this image has no ld64.lld"; exit 1; }
d=$(dirname "$v")
echo "LD64=$v" >> "$GITHUB_ENV"
# The tools are installed under a version suffix and the probe asks for
# them by their plain names, so the directory that has both spellings
# is named rather than assumed.
echo "NM=$d/llvm-nm" >> "$GITHUB_ENV"
echo "$d" >> "$GITHUB_PATH"
"$d/llvm-nm" --version | head -1
clang --version | head -1
- name: Zero indirect symbols, and two names
run: |
bash tools/probe-cross-macos.sh aarch64
bash tools/probe-cross-macos.sh x86_64
# ⚠️ LINKING IS NOT RUNNING, AND THIS IS WHERE THAT IS ADMITTED.
#
# Everything above happens on a machine that is not the system in
# question, and everything above is about the objects and the link. Whether
# the result STARTS is a different question, and it cannot be asked here:
# that system's 64-bit ARM variant refuses to start an image that is not
# signed, and the signature can only be made on a machine of that system.
#
# So the artifact is carried there. The job that receives it is the only
# place in this workflow where the claim becomes "a program built here
# runs there" rather than "a program built here links".
- name: A program for that system, built here
run: |
bash tools/cross-build-macos.sh aarch64 examples/cross-hello/src/main.c cross-hello-arm64
file cross-hello-arm64
- uses: actions/upload-artifact@v4
with:
name: cross-hello-arm64
path: cross-hello-arm64
retention-days: 1
# ---------------------------------------------------------------------------
# The other half of the claim, on a machine of that system.
cross-macos-run:
name: what was cross-built starts, on that system
needs: cross-macos
runs-on: macos-14
timeout-minutes: 15
steps:
- uses: actions/checkout@v4
- uses: actions/download-artifact@v4
with:
name: cross-hello-arm64
- name: Sign it, because this system will not start it otherwise
run: |
chmod +x cross-hello-arm64
# Ad hoc: the identity is `-', which asserts nothing about who made
# the program and is exactly what this system requires before it will
# start one on this architecture. A program that is distributed needs
# more; a program that is checked needs this.
codesign -s - --force cross-hello-arm64
codesign -dv cross-hello-arm64 2>&1 | head -3
- name: It starts, and the C library beneath it came up
run: |
./cross-hello-arm64 | tee run.log
grep -q -- '-- failures: 0 --' run.log