Merge branch 'held-step-soundness' into correctness-and-spec-skills

This commit is contained in:
pj committed 2026-08-16 01:26:55 +05:30
commit c420b84768
8 files changed
+429 -57

No files matched your search

+233 -21
View File
@@ -14,6 +14,7 @@ import (
"github.com/priyanshujain/sanderling/internal/driver" "github.com/priyanshujain/sanderling/internal/driver"
mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock" mockdriver "github.com/priyanshujain/sanderling/internal/driver/mock"
"github.com/priyanshujain/sanderling/internal/trace"
) )
// homeWithRows is one settled route whose list holds rows. A row arriving // homeWithRows is one settled route whose list holds rows. A row arriving
@@ -133,22 +134,25 @@ func TestRunner_AStepWhoseTreeChangedBetweenReadsIsNotVerified(t *testing.T) {
}) })
} }
// submitsOnTapDriver commits a transaction on every tap, shows the running // submitsOnTapDriver commits commitsPerTap transactions on every tap, shows the
// total in the tree, and grows a row under the hierarchy read that follows the // running total in the tree, and grows a row under the hierarchy read that
// paired Snapshot: on one chosen step, or on every one of them. // follows the paired Snapshot: on one chosen step, on the run of steps from
// composingRead through composingThrough, or on every one of them.
type submitsOnTapDriver struct { type submitsOnTapDriver struct {
*mockdriver.Driver *mockdriver.Driver
composingRead int64 commitsPerTap int64
everyRead bool composingRead int64
reads atomic.Int64 composingThrough int64
committed atomic.Int64 everyRead bool
reads atomic.Int64
committed atomic.Int64
} }
func (d *submitsOnTapDriver) Tap(context.Context, int, int) error { return d.commit() } func (d *submitsOnTapDriver) Tap(context.Context, int, int) error { return d.commit() }
func (d *submitsOnTapDriver) TapSelector(context.Context, string) error { return d.commit() } func (d *submitsOnTapDriver) TapSelector(context.Context, string) error { return d.commit() }
func (d *submitsOnTapDriver) commit() error { func (d *submitsOnTapDriver) commit() error {
d.committed.Add(1) d.committed.Add(d.commitsPerTap)
return nil return nil
} }
@@ -157,7 +161,10 @@ func (d *submitsOnTapDriver) Snapshot(context.Context) (string, driver.Image, er
} }
func (d *submitsOnTapDriver) Hierarchy(context.Context) (string, error) { func (d *submitsOnTapDriver) Hierarchy(context.Context) (string, error) {
if read := d.reads.Add(1); d.everyRead || read == d.composingRead { read := d.reads.Add(1)
composing := d.everyRead || read == d.composingRead ||
(read >= d.composingRead && read <= d.composingThrough)
if composing {
return fmt.Sprintf(homeWithTxnCountComposing, d.committed.Load()), nil return fmt.Sprintf(homeWithTxnCountComposing, d.committed.Load()), nil
} }
return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
@@ -188,7 +195,11 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) {
run := func(t *testing.T, composingRead int64) (Summary, int64) { run := func(t *testing.T, composingRead int64) (Summary, int64) {
t.Helper() t.Helper()
state := newHarnessWithSpec(t, spec) state := newHarnessWithSpec(t, spec)
device := &submitsOnTapDriver{Driver: state.mock, composingRead: composingRead} device := &submitsOnTapDriver{
Driver: state.mock,
commitsPerTap: 1,
composingRead: composingRead,
}
ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second) ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
defer cancel() defer cancel()
@@ -243,13 +254,92 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) {
}) })
} }
// Holding an action back is bounded. A screen that changes shape under every // One skipped step is held; a run of them has to be held too. A bound that lets
// pair of reads (a live list, a spinner mounting and unmounting) would // the runner act again while the verifier is still being skipped puts back the
// otherwise take the whole run: nothing verified, nothing tapped, and a green // exact swallow the hold exists to prevent, only later: the action drawn on the
// summary at the end of it. // step past the bound overwrites the one the hold was carrying, and the carried
func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) { // action is never reported to any spec.
//
// The screen composes on steps 3 through 5 of 6 and the device commits one
// transaction per tap throughout, so the property has a clean pair to judge
// (step 2 to step 6) and nothing in between it can be told about except the
// action step 2 applied.
func TestRunner_ARunOfSkippedStepsReportsEveryActionItApplied(t *testing.T) {
spec := specWithFolioPredicates(t)
run := func(t *testing.T, commitsPerTap int64) (Summary, int64) {
t.Helper()
state := newHarnessWithSpec(t, spec)
device := &submitsOnTapDriver{
Driver: state.mock,
commitsPerTap: commitsPerTap,
composingRead: 3,
composingThrough: 5,
}
ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
defer cancel()
summary, err := Run(ctx, Options{
Duration: time.Hour,
IdleTimeout: 20 * time.Millisecond,
MaxSteps: 6,
Driver: device,
Verifier: state.verifier,
TraceWriter: state.writer,
})
if err != nil {
t.Fatalf("Run: %v", err)
}
if summary.Steps != 6 {
t.Fatalf("steps = %d, want 6", summary.Steps)
}
if summary.SkippedVerification != 3 {
t.Fatalf("the run skipped %d step(s), want 3; the reread never fired across "+
"the run this test is about", summary.SkippedVerification)
}
return summary, device.committed.Load()
}
t.Run("no submit is lost to the run of skipped steps", func(t *testing.T) {
summary, committed := run(t, 1)
if committed == 0 {
t.Fatal("the device committed nothing; a runner that never acts passes this " +
"test without meaning anything")
}
if len(summary.Violations) != 0 {
t.Errorf("the counting property convicted a healthy app: %v\n"+
"one transaction per submit rose, and a submit went unreported because "+
"the runner acted on a step the verifier skipped", summary.Violations)
}
if committed != 3 {
t.Errorf("the device committed %d transaction(s), want 3: one per verified "+
"step (1, 2 and 6) and none from a step nothing would judge", committed)
}
})
// The control. Without it a green above proves nothing: a property handed
// no comparable pair is silently vacuous and reports the same empty list.
t.Run("two transactions per tap still convicts across the same run", func(t *testing.T) {
summary, _ := run(t, 2)
if len(summary.Violations) == 0 {
t.Fatal("the counting property missed a double submit; the skipped steps left " +
"it with nothing to judge, so the case above proves nothing")
}
if got := summary.Violations[0].Properties[0]; got != "submitCommitsOneTransactionPerAction" {
t.Errorf("violated %v, want submitCommitsOneTransactionPerAction",
summary.Violations[0].Properties)
}
})
}
// A screen that changes shape under every pair of reads (a live list, a spinner
// mounting and unmounting) costs the run its actions: an action applied onto it
// would be the one the next verified step never hears about, and there is no
// next verified step. What the run must not do is come back green off that,
// which is what the "judged by nothing" count and the run's outcome are for.
func TestRunner_AScreenThatNeverSettlesActsOnNothingAndSaysSo(t *testing.T) {
state := newHarnessWithSpec(t, specWithFolioPredicates(t)) state := newHarnessWithSpec(t, specWithFolioPredicates(t))
device := &submitsOnTapDriver{Driver: state.mock, everyRead: true} device := &submitsOnTapDriver{Driver: state.mock, commitsPerTap: 1, everyRead: true}
ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second) ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second)
defer cancel() defer cancel()
@@ -264,19 +354,141 @@ func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) {
if err != nil { if err != nil {
t.Fatalf("Run: %v", err) t.Fatalf("Run: %v", err)
} }
if summary.Steps != 5 {
t.Fatalf("steps = %d, want 5; the run stalled instead of finishing its budget",
summary.Steps)
}
if summary.SkippedVerification != 5 { if summary.SkippedVerification != 5 {
t.Fatalf("the run verified some step of a screen that never settled: skipped %d of 5", t.Fatalf("the run verified some step of a screen that never settled: skipped %d of 5",
summary.SkippedVerification) summary.SkippedVerification)
} }
if device.committed.Load() == 0 { if got := device.committed.Load(); got != 0 {
t.Error("the fuzzer never acted across 5 steps; a screen that keeps moving must " + t.Errorf("the fuzzer applied %d action(s) onto a screen no property would judge; "+
"cost the run a step or two, not all of them") "each one is an action no spec will ever be told about", got)
}
}
// homeWithTicker is one settled route holding a total that ticks and a button
// whose measured bounds shift under it. The nodes, their ids and their classes
// are the same in every rendering of it.
const homeWithTicker = `{"attributes":{"resource-id":"HomeScreen","class":"android.view.View"},"children":[
{"attributes":{"resource-id":"Total","class":"android.widget.TextView","text":"%s"},"children":[]},
{"attributes":{"resource-id":"TxnSubmit","class":"android.widget.Button","bounds":"%s"},"children":[]}
]}`
// The same route with a node in it that was not there a read ago.
const homeWithTickerAndRow = `{"attributes":{"resource-id":"HomeScreen","class":"android.view.View"},"children":[
{"attributes":{"resource-id":"Total","class":"android.widget.TextView","text":"120.00"},"children":[]},
{"attributes":{"resource-id":"TxnSubmit","class":"android.widget.Button","bounds":"[40,80,240,160]"},"children":[]},
{"attributes":{"resource-id":"TxnRowLate","class":"android.view.View"},"children":[]}
]}`
// rereadsDriver answers the paired Snapshot with one fixed tree and the
// hierarchy read that follows with another, so a test can say exactly what
// moved between the two reads the detector compares.
type rereadsDriver struct {
*mockdriver.Driver
snapshotTree string
rereadTree string
}
func (d *rereadsDriver) Snapshot(context.Context) (string, driver.Image, error) {
return d.snapshotTree, driver.Image{}, nil
}
func (d *rereadsDriver) Hierarchy(context.Context) (string, error) {
return d.rereadTree, nil
}
// What the two reads are compared ON is the whole feature. Comparing the values
// in the tree instead of the nodes in it would fire on every step of a screen
// with a total on it or a measure pass in flight, and a runner that skips every
// step verifies nothing while reporting no violations: green and vacuous, which
// is a worse answer than the composition the comparison set out to catch.
//
// The always-false property is the witness: it fires on the first step that
// reaches the verifier, so its presence and its step index say whether the step
// was judged at all.
func TestRunner_OnlyAChangeOfShapeCostsAStepItsVerdict(t *testing.T) {
settled := fmt.Sprintf(homeWithTicker, "120.00", "[40,80,240,160]")
cases := []struct {
name string
reread string
verified bool
}{
{
name: "a total that ticked between the two reads",
reread: fmt.Sprintf(homeWithTicker, "121.00", "[40,80,240,160]"),
verified: true,
},
{
name: "a measure pass that moved the button",
reread: fmt.Sprintf(homeWithTicker, "120.00", "[40,84,240,164]"),
verified: true,
},
{
name: "a node that was not in the tree a read ago",
reread: homeWithTickerAndRow,
verified: false,
},
}
for _, testCase := range cases {
t.Run(testCase.name, func(t *testing.T) {
state := newHarnessWithSpec(t, violationSpec)
device := &rereadsDriver{
Driver: state.mock,
snapshotTree: settled,
rereadTree: testCase.reread,
}
ctx, cancel := context.WithTimeout(context.Background(), 10*time.Second)
defer cancel()
summary, err := Run(ctx, Options{
Duration: time.Hour,
IdleTimeout: 20 * time.Millisecond,
MaxSteps: 3,
Driver: device,
Verifier: state.verifier,
TraceWriter: state.writer,
})
if err != nil {
t.Fatalf("Run: %v", err)
}
if summary.Steps != 3 {
t.Fatalf("steps = %d, want 3", summary.Steps)
}
if !testCase.verified {
if summary.SkippedVerification != 3 {
t.Errorf("the run judged %d of 3 steps whose tree grew a node between "+
"the two reads; a screen still composing must reach no property",
3-summary.SkippedVerification)
}
if len(summary.Violations) != 0 {
t.Errorf("a skipped step reached the verifier anyway: %v",
summary.Violations)
}
return
}
if summary.SkippedVerification != 0 {
t.Fatalf("the run judged nothing: %d of 3 steps were skipped over a tree "+
"whose nodes never changed", summary.SkippedVerification)
}
if len(summary.Violations) != 1 {
t.Fatalf("violations = %v, want exactly one", summary.Violations)
}
if got := summary.Violations[0].StepIndex; got != 1 {
t.Errorf("the property first judged step %d, want 1", got)
}
})
} }
} }
type traceLine struct { type traceLine struct {
Step int `json:"step"` Step int `json:"step"`
Violations []string `json:"violations"` Violations []string `json:"violations"`
ExtractorChanges map[string]trace.ExtractorChange `json:"extractor_changes"`
} }
func traceSteps(t *testing.T, directory string) []traceLine { func traceSteps(t *testing.T, directory string) []traceLine {
@@ -74,8 +74,10 @@ func (d *leavesForegroundAfterSubmitDriver) Snapshot(context.Context) (string, d
return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), driver.Image{}, nil
} }
// No device answers Snapshot and Hierarchy off different trees, and the runner // The runner reads both per step and compares them, so a device that answered
// reads both per step, so this one answers them off the same commit count. // them off different trees would make every step of this test transitional and
// judged by nothing. The sidecar serves both off one read path (snapshotTree)
// for the same reason; this one answers them off the same commit count.
func (d *leavesForegroundAfterSubmitDriver) Hierarchy(context.Context) (string, error) { func (d *leavesForegroundAfterSubmitDriver) Hierarchy(context.Context) (string, error) {
return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil
} }
@@ -285,3 +287,79 @@ func TestRunner_AnOverlayDoesNotConvictTheSubmitCountingProperty(t *testing.T) {
} }
}) })
} }
// reportedActionSpec puts what the runner told the spec about the last action
// into an extractor, so a test can read it out of the trace. `applied` and
// `relaunched` have no other producer: the runner's two guard writes are the
// only thing that ever sets them, and every spec-side guard built on them (see
// acrossRelaunch and confirmedApplied in the folio predicates) reads nothing
// else. A regression in either write leaves those guards permanently off with
// no property anywhere able to notice.
const reportedActionSpec = `
import { actions, always, extract, Tap } from "@sanderling/spec";
const reportedAction = extract("reportedAction", state => {
const last = state.lastAction;
if (last == null) return "none";
const dispatch = last.applied === true ? "applied" : "unconfirmed";
const process = last.relaunched === true ? "relaunched" : "same-process";
return dispatch + "/" + process;
});
globalThis.properties = {
theGuardTheRunnerRanReachesTheSpec: always(
() => reportedAction.current !== "applied/same-process",
),
};
globalThis.actions = actions(() => [Tap({ on: "id:TxnSubmit" })]);
`
// runReportingTheGuard drives two steps against a device whose submit tap trips
// one of the foreground guards, and hands back what the spec read off
// state.lastAction on the step the guard fired.
func runReportingTheGuard(t *testing.T, device committingDevice, state *harness) string {
t.Helper()
if violations := runTwoSubmitSteps(t, state, device, 1); len(violations) != 0 {
t.Errorf("the spec was told the action ran untouched by any guard: %v", violations)
}
steps := traceSteps(t, state.writer.Directory())
if len(steps) != 2 {
t.Fatalf("trace holds %d step(s), want 2", len(steps))
}
change, ok := steps[1].ExtractorChanges["reportedAction"]
if !ok {
t.Fatalf("step 2 recorded no reading of the reported action: %+v", steps[1])
}
return string(change.Curr)
}
func TestRunner_TheSpecIsToldTheAppWasRelaunchedUnderTheAction(t *testing.T) {
state := newHarnessWithSpec(t, reportedActionSpec)
device := &leavesForegroundAfterSubmitDriver{Driver: state.mock, commitsPerTap: 1}
reported := runReportingTheGuard(t, device, state)
if countMockActions(state, mockdriver.ActionLaunch, "") == 0 {
t.Fatal("the app was never relaunched, so the write this test is about never ran")
}
if reported != `"applied/relaunched"` {
t.Errorf("the spec read %s off state.lastAction, want \"applied/relaunched\"; "+
"a property relaxed across a relaunch cannot fire on a run that never "+
"tells it one happened", reported)
}
}
func TestRunner_TheSpecIsToldAnObscuredActionWasNotConfirmed(t *testing.T) {
state := newHarnessWithSpec(t, reportedActionSpec)
device := &obscuredAfterSubmitDriver{Driver: state.mock, commitsPerTap: 1}
reported := runReportingTheGuard(t, device, state)
if countMockActions(state, mockdriver.ActionPressKey, "back") == 0 {
t.Fatal("the overlay was never dismissed, so the write this test is about never ran")
}
if reported != `"unconfirmed/same-process"` {
t.Errorf("the spec read %s off state.lastAction, want "+
"\"unconfirmed/same-process\"; a system window held the focused window, "+
"so whether the app received the tap is exactly what nobody can say",
reported)
}
}
+28 -18
View File
@@ -100,7 +100,6 @@ func Run(ctx context.Context, options Options) (Summary, error) {
deadline := summary.StartTime.Add(options.Duration) deadline := summary.StartTime.Add(options.Duration)
stepIndex := 0 stepIndex := 0
consecutiveApplyFailures := 0 consecutiveApplyFailures := 0
heldSteps := 0
var lastAction *verifier.Action var lastAction *verifier.Action
var lastLogTime time.Time var lastLogTime time.Time
for time.Now().Before(deadline) { for time.Now().Before(deadline) {
@@ -287,16 +286,16 @@ func Run(ctx context.Context, options Options) (Summary, error) {
// their effects would then see an effect whose cause the runner // their effects would then see an effect whose cause the runner
// swallowed. See TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt. // swallowed. See TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt.
// //
// Bounded, because a screen that never settles must not stall the whole // Unbounded, because lastAction holds exactly one action: any bound that
// run: past the bound the runner acts anyway, which is where it was // let the runner act again while the verifier was still being skipped
// before this held anything back. // would overwrite the action the hold was carrying, and that is the same
held := skippedVerification && heldSteps < maxHeldSteps // swallow arriving one step later. A screen that keeps moving therefore
// costs the run its actions rather than its soundness, and a run that
// verified nothing says so in its outcome (internal/testrun).
held := skippedVerification
if held { if held {
heldSteps++
logger.Warn("screen still moving; holding this step's action back", logger.Warn("screen still moving; holding this step's action back",
"step", stepIndex, "held", heldSteps) "step", stepIndex)
} else {
heldSteps = 0
} }
var nextAction verifier.Action var nextAction verifier.Action
@@ -401,7 +400,16 @@ func Run(ctx context.Context, options Options) (Summary, error) {
// concurrent fetches observe a stable post-action state. A transient // concurrent fetches observe a stable post-action state. A transient
// apply error means nothing landed, so the idle poll has nothing to // apply error means nothing landed, so the idle poll has nothing to
// settle and may itself hang on the same device condition. // settle and may itself hang on the same device condition.
if nextErr == nil && !applySkipped && nextAction.Kind != verifier.ActionKindWait { //
// A held step settles too, and it is the only case here that waits with
// nothing applied. The reread that held it takes its two reads a round
// trip apart, which is a tighter window than the one the detector was
// measured over (an action and a settle); looping straight back into it
// would compare two reads of a composing screen closer together still,
// so the screen that most needs to settle is the one given least room.
mutated := nextErr == nil && !applySkipped &&
nextAction.Kind != verifier.ActionKindWait
if held || mutated {
idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout) idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout)
idleErr := options.Driver.WaitForIdle(idleCtx, options.IdleTimeout) idleErr := options.Driver.WaitForIdle(idleCtx, options.IdleTimeout)
if idleErr != nil && idleCtx.Err() == nil { if idleErr != nil && idleCtx.Err() == nil {
@@ -1071,6 +1079,13 @@ retryLoop:
// filling in. Two reads a read apart are the cheapest thing that can see it // filling in. Two reads a read apart are the cheapest thing that can see it
// happening: the round trip IS the interval, so there is no sleep here. // happening: the round trip IS the interval, so there is no sleep here.
// //
// The comparison only means anything because the Hierarchy RPC serves the tree
// the snapshot's own read produces (see snapshotTree in the sidecar). Off the
// bare device read it does not: with an IME standing open, the snapshot answers
// with 134 nodes and the bare read with 489, and the pair then differs over
// whether the sidecar closed a keyboard between them rather than over anything
// the app did.
//
// Waiting for the change to stop was measured on an API 34 device and refused: // Waiting for the change to stop was measured on an API 34 device and refused:
// a 750ms-quiet poll capped at 2s cost a median 1434ms against 76ms for one // a 750ms-quiet poll capped at 2s cost a median 1434ms against 76ms for one
// read, hit its cap on every frame it fired for, and still handed back a frame // read, hit its cap on every frame it fired for, and still handed back a frame
@@ -1122,6 +1137,9 @@ func changedOnReread(
// worse than the composition it set out to catch. The trade is measured rather // worse than the composition it set out to catch. The trade is measured rather
// than assumed: over 100 folio steps on an API 35 emulator, text moved under // than assumed: over 100 folio steps on an API 35 emulator, text moved under
// an unchanged shape on 1 step, and the shape itself moved on 1 other. // an unchanged shape on 1 step, and the shape itself moved on 1 other.
//
// TestRunner_OnlyAChangeOfShapeCostsAStepItsVerdict is what holds the line:
// adding either field back to the shape turns one of its cases red.
func structuralShape(tree *hierarchy.Tree) string { func structuralShape(tree *hierarchy.Tree) string {
var shape strings.Builder var shape strings.Builder
for _, element := range tree.Elements { for _, element := range tree.Elements {
@@ -1316,14 +1334,6 @@ func encodeResiduals(residuals map[string]ltl.Formula) (map[string]json.RawMessa
// would be spent doing nothing. // would be spent doing nothing.
const maxConsecutiveApplyFailures = 3 const maxConsecutiveApplyFailures = 3
// maxHeldSteps bounds how many steps in a row the runner will decline to act on
// because their screen was still moving. It is a livelock bound, not a settle
// budget: a screen that changes shape under every pair of reads (a live list, a
// spinner that mounts and unmounts) would otherwise take the whole run without
// the fuzzer ever touching it. Two is what the measured cases need, which came
// one step at a time and never twice in a row.
const maxHeldSteps = 2
// isWDADrop reports that the sidecar could not restart the iOS XCTest // isWDADrop reports that the sidecar could not restart the iOS XCTest
// runner: the channel is gone for good and the run must abort. Transient // runner: the channel is gone for good and the run must abort. Transient
// drops are classified by the sidecar itself (it reconnects and surfaces // drops are classified by the sidecar itself (it reconnects and surfaces
+24
View File
@@ -242,7 +242,15 @@ func Execute(ctx context.Context, options Options, stdout io.Writer) error {
// --exit-on-violation a run that found violations is still a successful run // --exit-on-violation a run that found violations is still a successful run
// (the summary reports them), which is the behaviour every existing caller // (the summary reports them), which is the behaviour every existing caller
// depends on. // depends on.
//
// A run none of whose steps reached the verifier fails whatever the flags say,
// because it holds no verdict to report. The threshold is every step and not a
// fraction of them: a screen that composes now and then costs a healthy android
// run a step or two, and a check that fired on those would be red on every run.
func runOutcome(options Options, summary runner.Summary) error { func runOutcome(options Options, summary runner.Summary) error {
if summary.Steps > 0 && summary.SkippedVerification == summary.Steps {
return VacuousRunError{Steps: summary.Steps}
}
if options.ExitOnViolation && len(summary.Violations) > 0 { if options.ExitOnViolation && len(summary.Violations) > 0 {
return ViolationsError{Count: len(summary.Violations)} return ViolationsError{Count: len(summary.Violations)}
} }
@@ -261,6 +269,22 @@ func (e ViolationsError) Error() string {
return fmt.Sprintf("%d violation record(s)", e.Count) return fmt.Sprintf("%d violation record(s)", e.Count)
} }
// VacuousRunError reports a run in which no step reached the verifier, so no
// property ever judged anything. It is not a clean run and it is not a found
// bug: it is a run that produced no evidence either way, and the absence of
// violations in it says nothing about the app. It stays untyped to the CLI's
// violation path on purpose, so it exits 1 as a broken run rather than 2.
type VacuousRunError struct {
Steps int
}
func (e VacuousRunError) Error() string {
return fmt.Sprintf(
"%d step(s) ran and none of them reached the verifier: the screen was "+
"still moving every time it was read, so no property judged this run",
e.Steps)
}
// bundleInputs holds the pre-driver assembly: alias map, seed, esbuild defines, // bundleInputs holds the pre-driver assembly: alias map, seed, esbuild defines,
// and the resolved spec-API/goja-runtime paths the bundler consumes. // and the resolved spec-API/goja-runtime paths the bundler consumes.
type bundleInputs struct { type bundleInputs struct {
+25
View File
@@ -266,6 +266,31 @@ func TestRunOutcome_ReportsViolationsOnlyUnderTheFlag(t *testing.T) {
} }
} }
// A step the verifier skipped was judged by nothing, so a run whose every step
// was skipped holds no verdict at all: "no violations" there is the absence of
// an answer rather than a clean one. Reporting it as a successful run is the
// green and vacuous outcome structuralShape's own design notes call worse than
// the composition it catches, and the runner's hold is what makes a fully
// skipped run reachable.
func TestRunOutcome_ARunThatJudgedNothingIsNotASuccess(t *testing.T) {
nothingJudged := runner.Summary{Steps: 6, SkippedVerification: 6}
err := runOutcome(Options{}, nothingJudged)
var vacuous VacuousRunError
if !errors.As(err, &vacuous) {
t.Fatalf("a run that judged none of its 6 steps came back %v, want a VacuousRunError", err)
}
if vacuous.Steps != 6 {
t.Errorf("steps: got %d, want 6", vacuous.Steps)
}
// A screen that composes now and then costs a run steps, not its verdict. A
// check that fired here would turn every healthy android run red.
mostlyJudged := runner.Summary{Steps: 6, SkippedVerification: 5}
if err := runOutcome(Options{}, mostlyJudged); err != nil {
t.Errorf("a run that judged one of its 6 steps must succeed, got %v", err)
}
}
// wedgedLaunchDriver never returns from Launch, standing in for a driver whose // wedgedLaunchDriver never returns from Launch, standing in for a driver whose
// device-side session is stuck. // device-side session is stuck.
type wedgedLaunchDriver struct { type wedgedLaunchDriver struct {
@@ -30,11 +30,21 @@ interface DriverBackend {
fun healthy(): Boolean fun healthy(): Boolean
fun metrics(bundleId: String): MetricsSample fun metrics(bundleId: String): MetricsSample
// snapshotTree is the tree a snapshot reads, without the screenshot. It is
// what the Hierarchy RPC serves, so the runner's two reads of a step come
// off one pipeline: a backend that waits out a transition or closes a
// keyboard before reading has to do the same on both, or the two trees
// differ over what the backend did between them rather than over what the
// app did. Measured on an API 34 emulator, an IME standing open is a
// 489-node bare read against the snapshot's 134.
fun snapshotTree(): String = hierarchy()
// snapshot captures hierarchy then screenshot back-to-back. The service // snapshot captures hierarchy then screenshot back-to-back. The service
// layer holds a mutex around the call so concurrent callers observe a // layer holds a mutex around the call so concurrent callers observe a
// serialized pair from the same on-device frame. Backends may override // serialized pair from the same on-device frame. Backends may override
// to fuse the two reads more tightly when their native API allows. // to fuse the two reads more tightly when their native API allows.
fun snapshot(): SnapshotSample = SnapshotSample(hierarchy(), screenshot()) fun snapshot(): SnapshotSample =
SnapshotSample(snapshotTree(), screenshot())
// close releases device-side resources on shutdown. The iOS backend must // close releases device-side resources on shutdown. The iOS backend must
// stop its XCTest runner here: an orphaned runner session auto-restarts // stop its XCTest runner here: an orphaned runner session auto-restarts
@@ -1250,8 +1260,8 @@ class MaestroDriverBackend(private val serial: String?) : DriverBackend {
override fun recentLogs(sinceUnixMillis: Long, minLevel: String) = override fun recentLogs(sinceUnixMillis: Long, minLevel: String) =
readLogcat(serial, sinceUnixMillis, minLevel) readLogcat(serial, sinceUnixMillis, minLevel)
// snapshot waits out a NavHost cross-fade before it reads, so the runner is // snapshotTree waits out a NavHost cross-fade before it reads, so the runner
// never handed a tree holding two routes at once. It belongs here rather // is never handed a tree holding two routes at once. It belongs here rather
// than in waitForIdle: the runner gives waitForIdle a one-second deadline // than in waitForIdle: the runner gives waitForIdle a one-second deadline
// and abandons the RPC when it expires, which is not enough room for a // and abandons the RPC when it expires, which is not enough room for a
// 700ms fade that began before the settle did, and a wait that outlives the // 700ms fade that began before the settle did, and a wait that outlives the
@@ -1262,16 +1272,15 @@ class MaestroDriverBackend(private val serial: String?) : DriverBackend {
// The predicate costs nothing on a settled frame: the read it needs is the // The predicate costs nothing on a settled frame: the read it needs is the
// read the snapshot was going to do anyway. That is what makes this // read the snapshot was going to do anyway. That is what makes this
// affordable, where the structural poll that used to run in waitForIdle was // affordable, where the structural poll that used to run in waitForIdle was
// not: it fetched the hierarchy ~4 more times on every mutating step. // not: it fetched the hierarchy ~4 more times on every mutating step. The
override fun snapshot(): SnapshotSample { // keyboard leg costs nothing either when no IME is standing in the tree,
val tree = treeWithoutKeyboard( // which is what lets the Hierarchy RPC serve this too.
awaitSettledTree { hierarchy() }, override fun snapshotTree(): String = treeWithoutKeyboard(
imePackage, awaitSettledTree { hierarchy() },
dismiss = { runCatching { dadb.shell("input keyevent 4") } }, imePackage,
reread = { awaitSettledTree { hierarchy() } }, dismiss = { runCatching { dadb.shell("input keyevent 4") } },
) reread = { awaitSettledTree { hierarchy() } },
return SnapshotSample(tree, screenshot()) )
}
override fun waitForIdle(durationMillis: Long) { override fun waitForIdle(durationMillis: Long) {
// waitForAppToSettle blocks on the View-system animation and maestro's // waitForAppToSettle blocks on the View-system animation and maestro's
@@ -170,12 +170,18 @@ class DriverService(
} }
} }
// The runner reads this a second time per step to see whether the screen
// changed while it was looking, so it has to describe the same thing the
// snapshot's tree describes: same settle, same keyboard handling, same
// lock. Served off the bare backend read, the pair differed over what the
// backend did between them rather than over what the app did.
override fun hierarchy( override fun hierarchy(
request: Empty, request: Empty,
responseObserver: StreamObserver<HierarchyJSON>, responseObserver: StreamObserver<HierarchyJSON>,
) { ) {
runRpc(responseObserver) { runRpc(responseObserver) {
HierarchyJSON.newBuilder().setJson(backend.hierarchy()).build() val tree = synchronized(snapshotLock) { backend.snapshotTree() }
HierarchyJSON.newBuilder().setJson(tree).build()
} }
} }
@@ -333,9 +333,17 @@ class DriverServiceTest {
assertEquals(3, image.png.size()) assertEquals(3, image.png.size())
} }
@Test fun hierarchyReturnsBackendJson() { // The runner reads the hierarchy a second time per step to see whether the
// screen changed while it was looking, so this has to answer with the tree
// the snapshot's read produces: same settle, same keyboard handling. Served
// off the bare backend read, the pair differs over what the backend did
// between the two reads rather than over what the app did. Measured on an
// API 34 emulator with an IME standing open, that is a 489-node tree
// against the snapshot's 134.
@Test fun hierarchyServesTheTreeTheSnapshotReads() {
val backend = object : DriverBackend by StubDriverBackend("android") { val backend = object : DriverBackend by StubDriverBackend("android") {
override fun hierarchy(): String = "{\"x\":1}" override fun hierarchy(): String = "{\"bare\":1}"
override fun snapshotTree(): String = "{\"x\":1}"
} }
val client = newClient(backend) val client = newClient(backend)