From 216d1c0ab05068c4a381e0f324b5a2cc32bdc8f4 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Mon, 21 Sep 2026 08:09:08 +0700 Subject: [PATCH] A program written to fault cannot be compared at -O2 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 --- spike/x86/survey.sh | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index 8a245f5..8c0678e 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -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.