JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A program written to fault cannot be compared at -O2

Browse Source 
The two new fault-by-design programs came into the corpus with the
bytes/bytes-view lane and the survey has been comparing them at its own
optimisation level, where the store into .rodata is undefined, LLVM
deletes it and exits 0, and this backend -- which has no optimiser to
delete anything with -- executes it and takes 139. That reads as a
lowering disagreement and is not one: at -O0 the two backends agree
exactly, and test_acceptance.ml's dies_segv rows already pin that on
both of them.

So a second exclusion list beside the one for the programs that never
stop, with its own reason written down, rather than building the whole
corpus at -O0 and changing the measurement every baseline was taken
against. dev-segv would belong on it in any case: it calls agent/start,
and under --dev it parks in the break loop rather than dying.

  MATCH 171, DIFFER 0, REFUSED 0, NOX86 0, SKIP 47
This commit is contained in:
Joseph Ferano 2026-09-21 08:09:08 +07:00
parent 190fdadcb8
commit 216d1c0ab0
1 changed files with 21 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
spike/x86/survey.sh
View File

@ -92,6 +92,26 @@ forever="dev-loop dev-watch dev-chatty agent-auto"
# in the epilogue that every exit already went through. The five are in the
# sweep now and they are five of the MATCHes.
# The ones whose whole point is a fault, and which therefore cannot be compared
# at this sweep's optimisation level. Both write through a bytes-view of a
# string literal, which is a store into .rodata: measured here, LLVM exits 0
# having printed the unmodified literal and this backend exits 139, because the
# store is undefined and the optimiser deleted it on one side and there is no
# optimiser on the other. That is not a lowering disagreement. At -O0 the two
# agree exactly -- 139, no output, both backends -- and test_acceptance.ml's
# dies_segv rows pin precisely that, on both backends, which is the coverage
# this sweep would otherwise be duplicating at the one level where, as that
# file's own comment puts it, there is nothing left to pin but the UB.
#
# Excluded by name rather than by building the whole corpus at -O0: the counts
# below are one measurement and every handoff's baseline was taken against it.
#
# dev-segv would not belong here even if the store survived. It calls
# agent/start, so it leaves a socket in /tmp on both runs, and under
# SURVEY_FLAGS=--dev it parks in the break loop instead of dying -- two
# truncations at the timeout, which is the dev-chatty failure by another road.
faults="bytes-view-write dev-segv"
TIMEOUT=${TIMEOUT:-20}
# Extra flags, given to *both* sides. SURVEY_FLAGS=--dev is the one that has a
@ -115,6 +135,7 @@ for src in "$corpus"/test/programs/*.flan "$corpus"/spike/x86/*.flan \
[ $want = 1 ] || continue
fi
case " $forever " in *" $name "*) skip+=("$name:runs-forever"); continue;; esac
case " $faults " in *" $name "*) skip+=("$name:faults-by-design"); continue;; esac
# LLVM first. A program that does not compile at all, or has no main, is not
# this backend's business -- the frontend refused it either way.