commit 87dfbfa3744d0903c988918f841aff3e48719dff
parent c6911c285ec337df8733870c7e5c434aceb1ea26
Author: Jared Tobin <jared@jtobin.io>
Date: Sat, 31 Oct 2026 13:22:12 +0400
merge impl/cpu-models: a CPU model for QEMU to emulate
record --cpu MODEL has QEMU emulate MODEL (its -cpu) and records it in
the dump; diff refuses runs recorded on other models and names the
model in its report; diffOf takes cpu. QEMU's AArch64 models take
crypto=off (qemu-crypto.patch), removing the cryptographic extension
as a CPU without it reports.
Diffstat:
6 files changed, 147 insertions(+), 29 deletions(-)
diff --git a/CHANGELOG b/CHANGELOG
@@ -21,6 +21,12 @@
* `read` resolves the objects a harness reports to the files they
name, as memcheck names a frame's object, so a library reached by
its soname's link has its sites placed by offset.
+ * `record --cpu MODEL` has QEMU emulate MODEL (its -cpu), which the
+ dump records (a `P` line); `diff` refuses runs recorded on other
+ models and names the model in its report; `diffOf` takes `cpu`.
+ * QEMU's AArch64 models take `crypto=off`, removing the
+ cryptographic extension as a CPU without it reports
+ (qemu-crypto.patch).
- 0.1.0 (2026-10-22)
* Initial version, with two instruments over a harness that marks
diff --git a/app/Main.hs b/app/Main.hs
@@ -71,6 +71,7 @@ data Opts = Opts {
, oContract :: !(Maybe T.Text)
, oObjdump :: !(Maybe FilePath)
, oWatch :: !(Maybe FilePath)
+ , oCpu :: !(Maybe String)
}
main :: IO ()
@@ -108,11 +109,12 @@ usage e = do
, " vestigia run [--valgrind PATH] [--dir DIR] [--out FILE] \
\[--object TEXT]... -- PROGRAM [ARG...]"
, " vestigia read [--out FILE] [--object TEXT]... RUN..."
- , " vestigia record [--qemu PATH] [--plugin PATH] --dump FILE \
- \[--contract NAME [--watch FILE | [--objdump PATH] \
+ , " vestigia record [--qemu PATH] [--plugin PATH] [--cpu MODEL] \
+ \--dump FILE [--contract NAME [--watch FILE | [--objdump PATH] \
\[--object TEXT]...]] -- PROGRAM [ARG...]"
- , " vestigia watch [--qemu PATH] [--out FILE] --contract NAME \
- \[--objdump PATH] [--object TEXT]... -- PROGRAM [ARG...]"
+ , " vestigia watch [--qemu PATH] [--cpu MODEL] [--out FILE] \
+ \--contract NAME [--objdump PATH] [--object TEXT]... -- PROGRAM \
+ \[ARG...]"
, " vestigia diff [--out FILE] [--addr2line PATH] \
\[--object TEXT]... [--control DUMP]... [--designed DUMP]... \
\DUMP DUMP..."
@@ -139,6 +141,9 @@ usage e = do
, "operands differed beside the origins. watch writes the list of"
, "those instructions once, for record --watch to read in runs of"
, "one program rather than make anew in each."
+ , "--cpu has QEMU emulate MODEL (its -cpu, with any properties),"
+ , "which the dump records; a program choosing its code by the"
+ , "CPU's features takes the path MODEL's features lead it to."
, "--object keeps origins in objects whose path contains TEXT;"
, "--control names a run repeating the first run's secret, and"
, "what differs in it is unsteady, not an origin."
@@ -152,7 +157,7 @@ usage e = do
-- options before the program; "--" ends them
options :: [String] -> Either String (Opts, [String])
options = go (Opts Nothing Nothing Nothing Nothing Nothing Nothing
- Nothing [] [] [] Nothing Nothing Nothing)
+ Nothing [] [] [] Nothing Nothing Nothing Nothing)
where
go o xs = case xs of
("--" : rest) -> Right (o, rest)
@@ -172,6 +177,7 @@ options = go (Opts Nothing Nothing Nothing Nothing Nothing Nothing
("--contract" : c : rest) -> go o { oContract = Just (T.pack c) } rest
("--objdump" : p : rest) -> go o { oObjdump = Just p } rest
("--watch" : p : rest) -> go o { oWatch = Just p } rest
+ ("--cpu" : c : rest) -> go o { oCpu = Just c } rest
(x : _) | take 2 x == "--" -> Left ("unknown option: " <> x)
_ -> Right (o, xs)
@@ -366,6 +372,7 @@ record o prog progArgs = do
others = filter ((/= tunables) . fst) environment
r <- try (withCreateProcess
((proc qemu (guest
+ <> cpuArgs o
<> [ "-seed", "0"
, "-plugin", plugin <> ",out=" <> dump
<> maybe "" (",watch=" <>) watchFile
@@ -385,8 +392,13 @@ record o prog progArgs = do
-- environment is QEMU's, with its own tunables restored
appendRun dump (prog : progArgs)
(others <> [ (tunables, v) | Just v <- [ own ] ]) c isa contract
+ (oCpu o)
exitWith c
+-- QEMU's -cpu, where a model is named
+cpuArgs :: Opts -> [String]
+cpuArgs o = maybe [] (\m -> [ "-cpu", m ]) (oCpu o)
+
refuseRecord :: String -> IO a
refuseRecord e = do
hPutStrLn stderr ("vestigia: " <> e)
@@ -421,7 +433,7 @@ watchList :: Opts -> FilePath -> Contract -> FilePath -> [String]
-> IO T.Text
watchList o qemu c prog progArgs = do
objdump <- tool (oObjdump o) "VESTIGIA_OBJDUMP" "llvm-objdump"
- loaded <- loadedObjects qemu prog progArgs
+ loaded <- loadedObjects qemu (cpuArgs o) prog progArgs
objects <- fmap L.nub (traverse canonicalizePath (prog : loaded))
let kept = [ p | p <- objects
, null (oObjects o)
@@ -434,10 +446,11 @@ watchList o qemu c prog progArgs = do
-- the shared objects a program loads, as its dynamic loader resolves
-- them, run under QEMU so that any ISA's are found
-loadedObjects :: FilePath -> FilePath -> [String] -> IO [FilePath]
-loadedObjects qemu prog progArgs = do
+loadedObjects :: FilePath -> [String] -> FilePath -> [String]
+ -> IO [FilePath]
+loadedObjects qemu cpu prog progArgs = do
r <- try (readCreateProcessWithExitCode
- (proc qemu ([ "-E", "LD_TRACE_LOADED_OBJECTS=1", prog ]
+ (proc qemu (cpu <> [ "-E", "LD_TRACE_LOADED_OBJECTS=1", prog ]
<> progArgs)) "")
case r of
Left e -> refuseRecord ("cannot run " <> qemu <> ": "
@@ -495,10 +508,10 @@ machineOf prog = do
-- append a run's record to its dump (Vestigia.Diff.readDump): its
-- arguments' bytes, its environment's variables and the bytes they
-- take, its exit status, the guest's ISA, and any contract it was
--- recorded under
+-- recorded under and CPU model QEMU emulated
appendRun :: FilePath -> [String] -> [(String, String)] -> ExitCode
- -> String -> Maybe Contract -> IO ()
-appendRun dump args env code isa contract = do
+ -> String -> Maybe Contract -> Maybe String -> IO ()
+appendRun dump args env code isa contract cpu = do
enc <- getFileSystemEncoding
let bytes s = GF.withCStringLen enc s BS.packCStringLen
as <- traverse bytes args
@@ -511,6 +524,7 @@ appendRun dump args env code isa contract = do
, "X " <> show (exitStatus code)
, "M " <> isa ]
<> [ "G " <> T.unpack (contractName c) | Just c <- [ contract ] ]
+ <> [ "P " <> m | Just m <- [ cpu ] ]
where
byte w = case showHex w "" of
[ d ] -> [ '0', d ]
@@ -553,6 +567,15 @@ diff o paths = do
\contract than " <> p0 <> "; runs compared must watch the \
\same instructions")
[] -> pure ()
+ -- runs on other CPU models may take other code wherever a program
+ -- chooses its code by the CPU's features
+ case zip (paths <> oDesigned o <> oControls o)
+ (dumps <> designed <> controls) of
+ ((p0, first) : rest) -> for_ rest $ \(p, d) ->
+ when (dpCpu d /= dpCpu first) $
+ refuse (p <> " was recorded on another CPU model than " <> p0
+ <> "; runs compared must run on the same one")
+ [] -> pure ()
-- runs laid out apart differ wherever they touch memory, not by
-- the secret: such runs are refused, not compared
case zip paths dumps of
diff --git a/lib/Vestigia/Diff.hs b/lib/Vestigia/Diff.hs
@@ -150,10 +150,11 @@ data Dump = Dump {
, dpOutside :: !(M.Map Integer T.Text)
-- | the text of each instruction the watch list named
, dpTexts :: !(M.Map Integer T.Text)
- -- | the guest's ISA, and the contract, as `vestigia record`
- -- appends them
+ -- | the guest's ISA, the contract, and the CPU model QEMU
+ -- emulated, as `vestigia record` appends them
, dpIsa :: !(Maybe T.Text)
, dpContract :: !(Maybe T.Text)
+ , dpCpu :: !(Maybe T.Text)
} deriving (Eq, Show)
-- | Read a plugin dump. A dump in which no instruction ran records
@@ -164,12 +165,14 @@ data Dump = Dump {
-- program's own. The record `vestigia record` appends (an @A@ line
-- per argument, its bytes in hex; @N@, the environment's variables
-- and bytes, in hex; @X@, the exit status, in decimal) is read
--- whole or not at all. Beside it, @M@ names the guest's ISA and @G@
--- the contract the run was recorded under.
+-- whole or not at all. Beside it, @M@ names the guest's ISA, @G@
+-- the contract the run was recorded under, and @P@ the CPU model
+-- QEMU emulated, where one was named.
readDump :: T.Text -> Either String Dump
readDump t = do
d <- foldM line (Dump M.empty M.empty S.empty M.empty M.empty M.empty
- Nothing M.empty M.empty Nothing Nothing, [], Nothing
+ Nothing M.empty M.empty Nothing Nothing Nothing, []
+ , Nothing
, Nothing) (T.lines t)
let (dump, as, env, st) = d
cx = dpContexts dump
@@ -216,6 +219,7 @@ readDump t = do
, env, st)
[ "M", isa ] -> pure (d { dpIsa = Just isa }, as, env, st)
[ "G", c ] -> pure (d { dpContract = Just c }, as, env, st)
+ [ "P", c ] -> pure (d { dpCpu = Just c }, as, env, st)
[ "C", c, caller, call ] -> do
v <- (,) <$> unhex caller <*> unhex call
k <- unhex c
@@ -363,10 +367,11 @@ data Divergence = Divergence {
, dvWatched :: !(M.Map T.Text (S.Set Integer))
-- | the text of each instruction the watch list named
, dvTexts :: !(M.Map Integer T.Text)
- -- | the guest's ISA and the contract, as the declared runs name
- -- them
+ -- | the guest's ISA, the contract, and the CPU model, as the
+ -- declared runs name them
, dvIsa :: !(Maybe T.Text)
, dvContract :: !(Maybe T.Text)
+ , dvCpu :: !(Maybe T.Text)
} deriving (Eq, Show)
-- | Compare runs, uncontrolled.
@@ -429,6 +434,9 @@ diffDesigned cs ds xs = Divergence {
, dvContract = case ds of
(d : _) -> dpContract d
[] -> Nothing
+ , dvCpu = case ds of
+ (d : _) -> dpCpu d
+ [] -> Nothing
}
where
ranIn' rs pc = [ (k, d) | (k, d) <- zip [ 0 .. ] rs
@@ -612,8 +620,8 @@ originText o = case o of
-- runs alike at it by the first two. An origin's stacks are its own
-- frames then its calls', innermost first, each frame with the
-- object and address of the instruction it names, as memcheck's
--- are in a taint report. The ISA and contract the runs were
--- recorded under head it; the instructions outside the contract
+-- are in a taint report. The ISA, contract, and CPU model the runs
+-- were recorded under head it; the instructions outside the contract
-- whose operands differed are given as origins are, and those that
-- ran, by object, as what was executed is.
divergenceJson
@@ -630,6 +638,7 @@ divergenceJson version runs places dv = Object
, ("source", maybe Null (String . contractSource)
(readContract n)) ]
Nothing -> Null)
+ , ("cpu", maybe Null String (dvCpu dv))
, ("runs", Array
[ Object
[ ("name", String (nmName r))
diff --git a/nix/lib.nix b/nix/lib.nix
@@ -27,12 +27,16 @@ let
# instruction, and the QEMU that runs a harness under it, for
# either ISA, whatever the host's: user mode alone, its guest's
# getrandom drawn from the generator -seed fixes
- # (qemu-getrandom.patch)
+ # (qemu-getrandom.patch), and an Arm CPU without the cryptographic
+ # extension to be had (crypto=off, qemu-crypto.patch)
qemu = (pkgs.qemu.override {
userOnly = true;
hostCpuTargets = [ "x86_64-linux-user" "aarch64-linux-user" ];
}).overrideAttrs (o: {
- patches = (o.patches or [ ]) ++ [ ./qemu-getrandom.patch ];
+ patches = (o.patches or [ ]) ++ [
+ ./qemu-getrandom.patch
+ ./qemu-crypto.patch
+ ];
});
plugin = pkgs.runCommandCC "vestigia-qemu-plugin" {
nativeBuildInputs = [ pkgs.pkg-config ];
@@ -116,12 +120,17 @@ let
# diff --designed). Under a `contract` (arm-dit or intel-doitm, the
# harness's ISA's), every run also fingerprints the operands of the
# instructions outside it in `objects`, listed once (vestigia watch,
- # kept as `watch`) for every run to read (record --watch).
+ # kept as `watch`) for every run to read (record --watch). On a
+ # `cpu`, every run is recorded with QEMU emulating that model (its
+ # -cpu, properties and all), so that a harness choosing its code by
+ # the CPU's features runs the code that model leads it to.
# A run's own failure leaves its status; a dump vestigia cannot read
# fails the build.
diffOf = { name, harness, runs, objects ? [ ], designed ? [ ]
- , contract ? null }:
+ , contract ? null, cpu ? null }:
let
+ model = lib.optionalString (cpu != null)
+ "--cpu ${lib.escapeShellArg cpu} ";
watch = lib.optionalString (contract != null)
"--contract ${lib.escapeShellArg contract} --watch $out/watch ";
in
@@ -129,7 +138,7 @@ let
mkdir -p $out
start=$(date +%s%N)
${lib.optionalString (contract != null) ''
- ${vestigia}/bin/vestigia watch --out $out/watch \
+ ${vestigia}/bin/vestigia watch --out $out/watch ${model}\
--contract ${lib.escapeShellArg contract} \
${lib.concatMapStrings (o: "--object ${lib.escapeShellArg o} ")
objects}-- ${harness} \
@@ -138,7 +147,7 @@ let
${lib.concatImapStrings (k: args: ''
set +e
${vestigia}/bin/vestigia record --dump $out/dump-${toString k} \
- ${watch}-- ${harness} ${lib.escapeShellArgs args} \
+ ${model}${watch}-- ${harness} ${lib.escapeShellArgs args} \
> $out/stdout-${toString k} 2> $out/stderr-${toString k}
echo $? > $out/status-${toString k}
set -e
@@ -146,7 +155,7 @@ let
set +e
${vestigia}/bin/vestigia record \
--dump $out/designed-${toString k} \
- ${watch}-- ${harness} ${lib.escapeShellArgs args} \
+ ${model}${watch}-- ${harness} ${lib.escapeShellArgs args} \
> $out/stdout-designed-${toString k} \
2> $out/stderr-designed-${toString k}
echo $? > $out/status-designed-${toString k}
@@ -154,7 +163,8 @@ let
'') designed}
set +e
${vestigia}/bin/vestigia record --dump $out/control-1 \
- ${watch}-- ${harness} ${lib.escapeShellArgs (builtins.head runs)} \
+ ${model}${watch}-- ${harness} \
+ ${lib.escapeShellArgs (builtins.head runs)} \
> $out/stdout-control-1 2> $out/stderr-control-1
echo $? > $out/status-control-1
set -e
diff --git a/nix/qemu-crypto.patch b/nix/qemu-crypto.patch
@@ -0,0 +1,65 @@
+QEMU's Arm CPU models all have the cryptographic extension (AES,
+PMULL, SHA1, SHA2, SHA3, SHA512, SM3, SM4), and none can be told to
+lack it, while CPUs built without it (a Raspberry Pi 4's Cortex-A72)
+run in the field: a program choosing its code by the CPU's features
+runs other code on them than any emulated CPU leads it to. crypto=off,
+on any AArch64 model, clears the extension's ID register fields, as
+such a CPU reports them: the instructions UNDEF, and a guest's HWCAP
+and ID register reads say they are absent.
+
+--- a/target/arm/cpu.c
++++ b/target/arm/cpu.c
+@@ -1581,6 +1581,41 @@
+ ARMCPU *cpu = ARM_CPU(obj);
+
+ return arm_feature(&cpu->env, ARM_FEATURE_AARCH64);
++}
++
++static bool aarch64_cpu_get_crypto(Object *obj, Error **errp)
++{
++ ARMCPU *cpu = ARM_CPU(obj);
++
++ return cpu_isar_feature(aa64_aes, cpu);
++}
++
++/*
++ * crypto=off removes the cryptographic extension (AES, PMULL, SHA1,
++ * SHA2, SHA3, SHA512, SM3, SM4), as a CPU built without it reports,
++ * from the ID registers: the instructions UNDEF, and a guest's
++ * HWCAP and ID register reads say they are absent.
++ */
++static void aarch64_cpu_set_crypto(Object *obj, bool value, Error **errp)
++{
++ ARMCPU *cpu = ARM_CPU(obj);
++
++ if (value) {
++ if (!cpu_isar_feature(aa64_aes, cpu)) {
++ error_setg(errp, "'crypto' feature cannot be enabled on "
++ "this CPU");
++ }
++ return;
++ }
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, AES, 0);
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, SHA1, 0);
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, SHA2, 0);
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, SHA3, 0);
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, SM3, 0);
++ FIELD_DP64_IDREG(&cpu->isar, ID_AA64ISAR0, SM4, 0);
++ FIELD_DP32_IDREG(&cpu->isar, ID_ISAR5, AES, 0);
++ FIELD_DP32_IDREG(&cpu->isar, ID_ISAR5, SHA1, 0);
++ FIELD_DP32_IDREG(&cpu->isar, ID_ISAR5, SHA2, 0);
+ }
+
+ static void aarch64_cpu_set_aarch64(Object *obj, bool value, Error **errp)
+@@ -1738,6 +1773,11 @@
+ object_property_set_description(obj, "aarch64",
+ "Set on/off to enable/disable aarch64 "
+ "execution state ");
++ object_property_add_bool(obj, "crypto", aarch64_cpu_get_crypto,
++ aarch64_cpu_set_crypto);
++ object_property_set_description(obj, "crypto",
++ "Set off to remove the "
++ "cryptographic extension");
+ }
+ #ifndef CONFIG_USER_ONLY
+ if (arm_feature(&cpu->env, ARM_FEATURE_CBAR) ||
diff --git a/test/Main.hs b/test/Main.hs
@@ -420,6 +420,11 @@ diffTests = testGroup "diff"
(readDump (under dumpA <> "3333\nM x86_64\nG intel-doitm\n"))
dpIsa a @?= Just "x86_64"
dpContract a @?= Just "intel-doitm"
+ dpCpu a @?= Nothing
+ c <- either assertFailure pure
+ (readDump (dumpA <> "M aarch64\nP max,crypto=off\n"))
+ dpCpu c @?= Just "max,crypto=off"
+ dvCpu (diffDumps [ c, c ]) @?= Just "max,crypto=off"
M.lookup 0x30 (dpTexts a) @?= Just "popcnt rax, rbx"
let dv = diffDumps [ a, b ]
-- not an origin: the contract says nothing either way of it
