Files
sanderling/internal/verifier/worker.go
T
pj 6b0d6cb971 WIP: Drive physical Android devices over USB (#67)
* feat(sidecar): reach USB devices via the adb server by serial

* feat(test): add --device flag to target a specific Android device by serial

* feat(folio): select Android device via ANDROID_DEVICE in justfile

* feat(conformance): add android backend to the gate suite

* feat(android): keep device awake and unlocked so the app stays foreground

* feat(conformance): prep physical android device (autofill/verifier/stayon)

* fix(android): make device prep best-effort so OEM-blocked commands don't abort the run

* fix(verifier): require positive bounds for swipe candidates

A zero-bounds element centers at (0,0); a downward swipe from the
top-left corner is the system gesture that pulls down the notification
shade, dragging the fuzzer out of the app. Swipes now require positive
bounds like every other verb.

* fix(runner): harden app-scope guard against launcher and overlays

The per-step guard now relaunches and waits until the app window is
actually drawn before proceeding, so a slow physical-device relaunch no
longer lets an observe or action land on the launcher. It also detects a
system overlay (notification shade) stealing window focus while the app
stays resumed, and dismisses it with back.

* feat(android): harden physical-device runs in device prep

Device prep now disables the AOSP cached-app freezer, phantom-process
killer, and Doze (and exempts the driver) so OEM background management
stops suspending the driver mid-run. Adds ReinstallApp for clear-state on
ROMs that deny pm clear, and teaches focus detection to report the
notification shade as systemui so the scope guard can dismiss it.

* feat(driver): clear-state via APK reinstall when pm clear is blocked

When an APK path is set, Android clear-state resets the app by
uninstalling and reinstalling instead of asking the sidecar to pm clear,
which hardened OEM builds (ColorOS) deny even to the adb shell user.
Falls back to the sidecar clear path when no APK path is provided.

* feat(cli): add --android-app-path for clear-state reinstall

Wires the APK path from the test command through to the sidecar client so
Android clear-state can reset apps on OEM builds that deny pm clear.

* chore(folio): pass --android-app-path in just test

* fix(runner): clamp swipe/scroll origin out of edge gesture zones

A gesture starting in the top status-bar strip pulls down the
notification shade; the bottom and side strips are the home and back
gestures. Any of them drags the fuzzer out of the app. Swipe and scroll
origins are now clamped into a safe inner area sized from the maximum
element extent (the Android hierarchy root reports zero bounds, so the
extent is the reliable screen size). Calibrated on device: origins below
~7% of height no longer open the shade.

* perf(sidecar): faster Android text input and drop redundant settle poll

inputText now uses adb `input text` for short shell-safe ASCII (~5x
faster than the driver's per-character path) and falls back to the driver
for unicode, injection payloads, and overflow-length strings. waitForIdle
drops the structural-hash poll that followed waitForAppToSettle: each
hierarchy fetch is ~500ms on a physical device, so it cost ~2.8s per
mutating step for marginal benefit, and the runner already re-fetches
transitional frames. Cuts p95 step latency from ~6.5s to ~5.1s; G1-G4
still pass.

* fix(verifier): exclude soft-keyboard region from action candidates

The fuzzer was tapping Gboard's "Settings" key, navigating out of the
app. That key is a bare FrameLayout with a content-desc and no package or
resource-id, so the package-based scope filter missed it. Candidates whose
center falls in the keyboard region (derived from the IME elements' bounds)
are now dropped, so no tap or long-press lands on a key. Opt-in with app
scoping; unscoped runs keep every node.

* perf(runner): replace focus-tap settle with a brief wait

The full WaitForIdle after a field-focus tap cost ~0.5-1s per InputText
step on a physical device while the keyboard animated in. The tap registers
focus immediately and text is injected into the focused view, so a short
fixed wait suffices. Drops p95 step latency ~5.1s to ~4.0s; G1-G4 stay
green.

* chore(conformance): platform-aware G5 p95 budget for android

The 2500ms ceiling was calibrated on the iOS simulator. A physical Android
device drives every step over USB (snapshot + settle + adb round-trips), so
its per-step floor is several times higher; holding it to 2500ms would force
removing the settle/retry logic the correctness gates depend on. The android
backend now defaults to 4500ms (override with P95_LIMIT_MS); iOS stays 2500.

* fix(sidecar): retry maestro android driver startup

The maestro Android driver's dadb.open() occasionally misses its startup
deadline (its instrumentation host is slow to come up right after a reboot
or per-run reinstall), which aborted the whole run. Retry the open a few
times with a short backoff so a transient timeout recovers.

* chore(conformance): widen android G5 budget to 5500ms

Physical-device p95 swung 3209-4612ms across sessions (cold runs right
after a reboot are slower). 4500ms was too tight for that jitter; 5500ms
covers the observed ceiling with headroom.

* web replay fix

* feat(android): force 3-button nav during runs to prevent app drift

On gesture navigation a fuzzer swipe can trigger swipe-up-home or
edge-back and fling the app off screen. Device-prep now switches to
3-button navigation for the run (no edge gestures; the nav bar's buttons
are systemui-owned and already excluded from action candidates) and
restores the original navigation mode when the run ends. Best effort:
leaves nav untouched if the overlay command is unavailable.

* fix(android): target the selected device in adb reads; don't strand nav mode

Review fixes:
- ForegroundPackage/FocusedWindowPackage now take a serial and pass -s, so the
  foreground/scope guard works when several devices are attached (the --device
  path). Previously they ran bare `adb shell`, which errors with multiple
  devices, silently disabling app-scope enforcement. The sidecar client passes
  its serial through.
- Extract an adbArgs helper and route every adb call through it, removing four
  duplicated serial-arg builders.
- ForceThreeButtonNav now decides what to restore before changing anything: if
  the current mode is unknown or already 3-button it leaves nav untouched,
  instead of switching and then stranding the device in 3-button. Logic split
  into the pure navModeToRestore, now unit tested.

* fix(runner): restore scrollBounds doc; cover destination clamp and screenBounds

Review fixes: move the scrollBounds doc comment back onto scrollBounds (it was
stranded above screenBounds by an insertion). Extend the clamp test to assert an
off-screen destination is clamped onto the screen and that the origin lands
exactly on the margin.

* test(verifier): cover keyboardRegionTop, including the decor-view guard

The full-screen IME decor view rejection had no test; removing it left the
suite green. Add direct cases: no keyboard -> sentinel, decor view ignored in
favor of the real keyboard line, and decor-only -> sentinel.

* style(cli): gofmt testOptions field alignment

* fix(sidecar): keep a leading dash off the fast input path

A value starting with '-' could be read as an option by `adb input text`, so
the fast-path regex now requires a non-dash first character; such values fall
back to the driver. Also cover the dadb-target branch where a colon precedes a
non-numeric port (a USB serial, not host:port).

* refactor(verifier): scope action candidates by window ownership

Replaces the leaky per-element package check and the keyboard-region Y
heuristic with one rule: walk the window tree propagating each node's owning
package (empty and the neutral android framework package are transparent); a
node is in scope only when no concrete foreign package owns it (the app's own
window carries no package on Compose apps) or the owner is the app package.

This drops whole foreign windows (soft keyboard, system UI, launcher) AND
their empty-package child wrappers -- e.g. a keyboard's 'Settings' key, which
the old empty-package-is-in-scope rule admitted and which navigated out of the
app. Deletes keyboardRegionTop/isInputMethodElement.

* fix(runner): re-check foreground at apply time, skip stale actions

ensureForeground runs before observe, but the app can leave between observe and
apply (a prior gesture settling late); swipes/keys then fire stale coordinates
onto whatever screen is now up. Re-check foreground immediately before applying
and, when the app is gone, skip the action and log it (making the escape
visible) so the next step's guard relaunches instead.

* fix(android): type long ASCII via fast guarded path to stop keystroke escape

A 4096-char corpus string exceeded the fast input cap and fell to the
per-character driver path, which takes ~120s. During that uninterruptible
window focus could leave the app and the remaining keystrokes sprayed into
the launcher search box. Route shell-safe ASCII of any length through adb
input text, chunked, re-checking the foreground app between chunks and
stopping if it changed.

* chore: ignore gate artifacts and local scratch files

* refactor(runner): narrow gesture clamp to the top shade strip

3-button nav (forced for every run) disables the side back and bottom home
gestures at the OS level. On-device probing confirmed side and bottom swipe
origins no longer drift, leaving the notification shade as the only edge
gesture a swipe can trigger. Clamp only the top strip; keep origin and
destination on screen otherwise.

* chore(format): add .editorconfig enforcing 80-column limit

* chore(format): add prettier config with 80-char printWidth

* chore(deps): add prettier devDependency to replay-ui

* chore(deps): add prettier devDependency to folio-web

* chore(deps): add prettier devDependency to spec package

* chore(format): add swift-format config with 80-char lineLength

* feat(format): add make fmt targets for per-language 80-col formatting

* fix(runner): translate gesture to safe area so near-top scrolls keep direction

Clamping the swipe origin to the top margin while leaving the destination on the full screen used two reference frames: a scrollable container pinned in the top strip had its origin pushed past the destination, reversing the gesture. Translate the whole from->to segment down by the same delta so the origin clears the shade strip without flipping direction. Adds a scroll-near-top test that fails under the old origin-only clamp.

* fix(runner): apply-time guard consults focused window, not just resumed activity

ensureForeground detects a system overlay (notification shade) owning the focused window while the app stays the resumed activity, but appIsForeground only queried ForegroundApp. A swipe that pulls the shade over the app between observe and apply then fired onto the shade. Mirror the focus check at apply time so the action skips and the next step dismisses the overlay.

* test(runner): cover apply-time foreground skip and appIsForeground table

Adds a Run-level test asserting no tap reaches the driver while a system overlay holds focus (guards against the skip branch being dead-coded), plus a decision-table test for appIsForeground. Adds ForegroundErr/FocusedWindowErr to the mock driver so the guard's transient-read paths are exercised.

* fix(sidecar): harden android driver open, input guard, pressKey, foreground marker

- openWithRetry rebuilt a closed AndroidDriver, whose gRPC channel is final and shut down by close(); the retry then ran against a dead channel. Build a fresh driver per attempt and extract a unit-tested retryOpen helper (named DRIVER_OPEN_ATTEMPTS/BACKOFF).
- pressKey on the Maestro backend did KEY_MAP[key] (no lowercase, no throw), silently dropping unknown or wrong-case keys; route through a pure maestroKeyFor that lowercases and rejects unknown keys like the Stub contract.
- the mid-type foreground guard (typeShellSafe) was untested; extract a pure typeChunks and cover stop-on-foreground-change, always-send-first-chunk, and unknown-owner.
- foreground detection required the literal topResumedActivity=ActivityRecord; align parseResumedPackage to the same *ResumedActivity marker set Go reads so OEM wording does not disable the guard.

* fix(conformance): pin self-test p95 budget and score install failures as run failures

self_test reused the backend-dependent P95_LIMIT_MS, so under BACKEND=android the 4000ms slow fixture rated PASS and the offline analyzer check failed from an env var; pin it to 2500. A per-run adb install failure ran unguarded under set -e and aborted the whole harness; guard it, record the run as a G1 failure, and continue.

* fix(android): require --device when several devices are connected

With no serial requested and more than one device online, pickDevice silently returned connected[0], but that serial is never threaded into the per-step adb calls, so every later bare adb command failed with "more than one device". Error instead and ask for --device, mirroring pickAVD; a single device stays unambiguous.

* refactor(android): move PrepareDevice doc onto it; extract tested wakeCommands

The PrepareDevice doc block was stranded above adbArgs, leaving the exported function undocumented under godoc. Move it back and split the wake/keyguard tuples into wakeCommands so they have a unit test.

* perf(verifier): memoize scopedElements per tree

scopedElements rebuilt a full tree walk plus map on every candidatesForVerb call (~16 per step). Cache the result keyed on lastTree and invalidate it in PushSnapshot.

* fix(sidecar): default reinstallApp in SetClearStateReinstall; cover non-android clear

Only Dial set reinstallApp, so a Client built another way would nil-deref on Android clear-state. Default it in SetClearStateReinstall too. Add a non-android test so the platform guard has negative coverage: dropping the android check would now fail.

* test(runner): make focusTapSettle injectable so apply tests don't sleep 250ms

The focus-tap settle was a const, so five InputText apply tests each blocked the full 250ms. Make it a package var and shorten it per-test with cleanup.

* refactor(runner,android): drop unused bringToForeground return; grep no-match yields empty

bringToForeground's bool return was read by no caller. FocusedWindowPackage's on-device grep exited 1 on no match, surfacing as an error instead of the documented ""; add || true.

* perf(sidecar): reuse a single Jackson ObjectMapper

structuralHash, countRouteScreens, and hierarchy each built a fresh ObjectMapper per call inside the stability poll; the instance is thread-safe and meant to be reused. Hoist one shared val.

* refactor(android): remove unused AdbReverse/AdbReverseRemove

No callers anywhere in the tree; they were also the only adb calls bypassing adbArgs. Dead code, removed.

* style(runner): trim non-load-bearing comments from this PR's runner code and tests

* style(sidecar): trim non-load-bearing comments from this PR's driver code and tests
2026-06-11 10:10:05 +05:30

743 lines
25 KiB
Go

// Package verifier runs the spec's extractors and property formulas against each observed step.
package verifier
import (
"bytes"
"encoding/json"
"errors"
"fmt"
"maps"
"sort"
"time"
"github.com/dop251/goja"
"github.com/priyanshujain/sanderling/internal/hierarchy"
"github.com/priyanshujain/sanderling/internal/ltl"
)
type Verifier struct {
runtime *goja.Runtime
extractors []*extractorState
formulas []*formulaState
formulaSpecs []formulaSpec
properties map[string]int // property name -> formula-spec index
// nextActionFn is the bundle-installed __sanderlingNextAction__, which runs
// the shared picker (pick.ts) over the shared Pcg.
nextActionFn goja.Callable
evaluators map[string]*ltl.Evaluator
priorVerdicts map[string]ltl.Verdict
newlyViolated []string
witnesses map[string]Witness
lastTree *hierarchy.Tree
scopeCache map[*hierarchy.Element]bool
scopeCacheTree *hierarchy.Tree
lastAction *Action
lastLogs []LogEntry
lastExceptions []Exception
stepTime time.Time
stepIndex int
runStart time.Time
appPackage string
platform string
seed uint64
// unsupported collects verbs the picker requested but the platform cannot
// dispatch (reportUnsupported host callback), deduped and in first-seen
// order, so the runner can surface them in the run report.
unsupported []string
unsupportedSeen map[string]bool
// extracting is true only while an extractor getter is running. The handle's
// current/previous accessors consult it so a getter that reaches into
// another extractor's handle throws instead of reading a stale value.
extracting bool
}
// UnsupportedVerbs returns the verbs the picker requested that this platform
// cannot dispatch, deduped and in first-seen order.
func (v *Verifier) UnsupportedVerbs() []string {
return v.unsupported
}
type Option func(*Verifier)
// WithSeed sets the 64-bit seed the JS picker constructs its Pcg from
// (new Pcg(seed, 0), matching the web bundle's SANDERLING_SEED). The verifier
// exposes it to the bundle via the __sanderlingHost__.seedHi/seedLo binds.
func WithSeed(seed uint64) Option {
return func(v *Verifier) { v.seed = seed }
}
// WithPlatform names the platform the host reports to the picker
// ("android"/"ios"/"web"); it drives the verb-support matrix and the press-key
// pool. Empty defaults to "android".
func WithPlatform(platform string) Option {
return func(v *Verifier) { v.platform = platform }
}
// WithAppPackage scopes random-action target selection to the app under test.
// Nodes belonging to another package (the soft keyboard, system UI, permission
// dialogs) are excluded so exploration never spends steps fuzzing the IME or
// inserting keyboard glyphs into fields. Empty package keeps current behavior.
func WithAppPackage(appPackage string) Option {
return func(v *Verifier) { v.appPackage = appPackage }
}
func New(options ...Option) (*Verifier, error) {
verifier := &Verifier{
runtime: goja.New(),
properties: map[string]int{},
evaluators: map[string]*ltl.Evaluator{},
priorVerdicts: map[string]ltl.Verdict{},
witnesses: map[string]Witness{},
platform: "android",
unsupportedSeen: map[string]bool{},
}
for _, option := range options {
option(verifier)
}
if verifier.platform == "" {
verifier.platform = "android"
}
if err := verifier.installRuntimeBindings(); err != nil {
return nil, fmt.Errorf("install bindings: %w", err)
}
return verifier, nil
}
// Load executes the bundled spec source. The spec is expected to assign its
// property formulas to globalThis.properties, its root action generator to
// globalThis.actions, and optionally a setup (precondition) action generator
// to globalThis.setup.
func (v *Verifier) Load(source string) error {
if _, err := v.runtime.RunString(source); err != nil {
return fmt.Errorf("run spec: %w", err)
}
propertiesValue := v.runtime.GlobalObject().Get("properties")
if propertiesValue != nil && !goja.IsUndefined(propertiesValue) && !goja.IsNull(propertiesValue) {
propertiesObject := propertiesValue.ToObject(v.runtime)
for _, name := range propertiesObject.Keys() {
handle := propertiesObject.Get(name).ToObject(v.runtime)
if handle == nil {
return fmt.Errorf("property %q is not an object", name)
}
specIndex, ok := v.extractSpecIndex(handle)
if !ok {
return fmt.Errorf("property %q was not produced by always()", name)
}
formula, err := v.buildFormula(specIndex)
if err != nil {
return fmt.Errorf("property %q: %w", name, err)
}
v.properties[name] = specIndex
v.evaluators[name] = ltl.NewEvaluator(formula)
}
}
// The bundle's goja runtime entry installs __sanderlingNextAction__ once the
// spec assigned globalThis.actions. Capture it; a spec bundled without the
// runtime entry (raw-JS unit fixtures) leaves it nil and NextAction reports
// ErrNoAction.
if fn := v.runtime.GlobalObject().Get("__sanderlingNextAction__"); fn != nil {
if callable, ok := goja.AssertFunction(fn); ok {
v.nextActionFn = callable
}
}
return nil
}
// buildFormula walks the formula-spec registry and produces a Go ltl.Formula
// tree rooted at the given spec index. Specs built at the top level are
// always wrapped in Always unless the top-level spec is already an Always.
func (v *Verifier) buildFormula(rootIndex int) (ltl.Formula, error) {
inner, err := v.buildFormulaNode(rootIndex)
if err != nil {
return nil, err
}
if _, ok := inner.(ltl.AlwaysFormula); ok {
return inner, nil
}
return ltl.Always(inner), nil
}
func (v *Verifier) buildFormulaNode(index int) (ltl.Formula, error) {
if index < 0 || index >= len(v.formulaSpecs) {
return nil, fmt.Errorf("formula spec index %d out of range", index)
}
spec := v.formulaSpecs[index]
switch spec.kind {
case specKindPure:
return ltl.Pure(spec.pureValue), nil
case specKindThunk:
name := fmt.Sprintf("p%d", spec.predicateIndex)
return ltl.ThunkNamed(name, v.formulaThunk(spec.predicateIndex)), nil
case specKindNow:
child, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
return ltl.Now(child), nil
case specKindNext:
child, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
return ltl.Next(child), nil
case specKindEventually:
child, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
formula := ltl.EventuallyFormula{Inner: child}
if spec.hasStepBound {
formula.StepBound = spec.stepBound
formula.HasStepBound = true
}
if spec.duration > 0 {
formula.Duration = spec.duration
}
return formula, nil
case specKindImplies:
left, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
right, err := v.buildFormulaNode(spec.childB)
if err != nil {
return nil, err
}
return ltl.Implies(left, right), nil
case specKindOr:
left, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
right, err := v.buildFormulaNode(spec.childB)
if err != nil {
return nil, err
}
return ltl.Or(left, right), nil
case specKindAnd:
left, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
right, err := v.buildFormulaNode(spec.childB)
if err != nil {
return nil, err
}
return ltl.And(left, right), nil
case specKindNot:
child, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
return ltl.Not(child), nil
case specKindAlways:
child, err := v.buildFormulaNode(spec.childA)
if err != nil {
return nil, err
}
return ltl.Always(child), nil
default:
return nil, fmt.Errorf("unknown formula spec kind %d", spec.kind)
}
}
// PushSnapshot updates the JS-side state and refreshes every extractor's
// current/previous values in registration order. Passing a nil tree is
// allowed and yields an empty ax scope.
func (v *Verifier) PushSnapshot(input SnapshotInput) error {
v.lastTree = input.Tree
v.scopeCache = nil
v.lastAction = input.LastAction
v.lastLogs = input.Logs
v.lastExceptions = input.Exceptions
v.stepTime = input.StepTime
v.stepIndex = input.StepIndex
if v.runStart.IsZero() {
v.runStart = input.RunStart
}
state, err := stateObject(v.runtime, stateInput{
snapshots: input.Snapshots,
tree: input.Tree,
lastAction: input.LastAction,
stepTime: input.StepTime,
runStart: v.runStart,
logs: input.Logs,
exceptions: input.Exceptions,
})
if err != nil {
return fmt.Errorf("build state: %w", err)
}
if err := v.runtime.GlobalObject().Set("state", state); err != nil {
return fmt.Errorf("set state: %w", err)
}
// Extractor previous/current advance exactly once per PushSnapshot.
// Predicate thunks read these slots but never trigger advancement, so
// invoking a thunk multiple times between snapshots is value-stable.
for index, extractor := range v.extractors {
extractor.previousValue = extractor.currentValue
newValue, err := v.runExtractor(extractor, state)
if err != nil {
return fmt.Errorf("extractor %d: %w", index, err)
}
extractor.currentValue = newValue
extractor.prev = extractor.curr
extractor.curr = encodeExtractorValue(newValue)
}
return nil
}
// runExtractor invokes an extractor's getter with the extracting flag set, so a
// getter that reads another extractor's current/previous throws. The flag is
// cleared even if the getter panics.
func (v *Verifier) runExtractor(extractor *extractorState, state goja.Value) (goja.Value, error) {
v.extracting = true
defer func() { v.extracting = false }()
return extractor.getter(goja.Undefined(), state)
}
// encodeExtractorValue produces a stable JSON encoding of an extractor's
// current value for diff comparison. goja values that don't survive Export
// (e.g. wrapped host functions) yield nil; callers treat nil as "unknown" and
// emit no diff entry.
func encodeExtractorValue(value goja.Value) []byte {
if value == nil || goja.IsUndefined(value) || goja.IsNull(value) {
return []byte("null")
}
exported := value.Export()
body, err := json.Marshal(exported)
if err != nil {
return nil
}
return body
}
// ChangedExtractors returns the named extractors whose value changed between
// the prior PushSnapshot and the current one. The map is keyed by extractor
// name; unnamed extractors (extractor_N fallback) are included so the replay
// UI can still display them under a numeric label. The very first snapshot
// emits every non-null extractor as a change (Prev=null, Curr=current) since
// the runner can otherwise misread "no diff yet" as "nothing initialized".
func (v *Verifier) ChangedExtractors() map[string]ExtractorChange {
changes := map[string]ExtractorChange{}
for _, extractor := range v.extractors {
if extractor.curr == nil {
continue
}
prev := extractor.prev
if prev == nil {
prev = []byte("null")
}
if bytes.Equal(prev, extractor.curr) {
continue
}
changes[extractor.name] = ExtractorChange{
Prev: append([]byte(nil), prev...),
Curr: append([]byte(nil), extractor.curr...),
}
}
return changes
}
// OverrideExtractorValues replaces each extractor's `current` slot with a
// caller-supplied value, keyed by registration index. Used by the web tick
// path so extractor bodies that ran in V8 (against the real DOM) drive the
// goja-side LTL predicates without re-running the getter against an empty
// state.ax shim. Passing a nil/empty map is a no-op so the mobile path can
// call this unconditionally. The override must run *after* PushSnapshot
// (which advanced `previous`) and *before* EvaluateProperties.
//
// Out-of-range indices are tolerated (skipped) rather than fatal: V8 and goja
// register extractors from the same spec bundle so counts should always
// match, but a stale or partial override map should not block valid overrides
// from applying. The number of skipped entries is reported so the caller can
// surface a mismatch.
func (v *Verifier) OverrideExtractorValues(overrides map[int]json.RawMessage) (skipped int, err error) {
if len(overrides) == 0 {
return 0, nil
}
for index, raw := range overrides {
if index < 0 || index >= len(v.extractors) {
skipped++
continue
}
value, conversionErr := jsonToJSValue(v.runtime, raw)
if conversionErr != nil {
return skipped, fmt.Errorf("extractor override %d: %w", index, conversionErr)
}
v.extractors[index].currentValue = value
}
return skipped, nil
}
// SnapshotInput bundles everything a step feeds into the verifier. Fields
// other than Snapshots are optional; callers that only have snapshots can
// populate Snapshots alone and leave the rest zero.
type SnapshotInput struct {
Snapshots Snapshots
Tree *hierarchy.Tree
LastAction *Action
StepTime time.Time
// StepIndex is the runner's step number for this snapshot. Evaluators label
// observations with it so violation witnesses carry runner step numbers even
// when transitional steps were skipped. Zero means unlabeled; evaluators
// then fall back to their internal counter.
StepIndex int
RunStart time.Time
Logs []LogEntry
Exceptions []Exception
}
// EvaluateProperties returns each registered property's running verdict
// after the most recent PushSnapshot. The step time passed in PushSnapshot is
// forwarded to each evaluator so deadline-bound operators see the snapshot's
// wall clock rather than time.Now().
//
// As a side effect, the set of properties that newly transitioned to violated
// on this call is recorded; see NewlyViolatedProperties.
func (v *Verifier) EvaluateProperties() map[string]ltl.Verdict {
verdicts := map[string]ltl.Verdict{}
stepTime := v.stepTime
if stepTime.IsZero() {
stepTime = time.Now()
}
for name, evaluator := range v.evaluators {
if v.stepIndex > 0 {
verdicts[name] = evaluator.ObserveAtStep(stepTime, v.stepIndex)
} else {
verdicts[name] = evaluator.ObserveAt(stepTime)
}
}
var onset []string
for name, verdict := range verdicts {
if verdict == ltl.VerdictViolated && v.priorVerdicts[name] != ltl.VerdictViolated {
onset = append(onset, name)
v.captureWitness(name)
}
}
sort.Strings(onset)
v.newlyViolated = onset
next := make(map[string]ltl.Verdict, len(verdicts))
maps.Copy(next, verdicts)
v.priorVerdicts = next
return verdicts
}
// Witness is the verifier-level record of a property violation: the LTL reason
// (a predicate's thrown-error text, "predicate false", or a liveness failure),
// the step it fired at, and a snapshot of every extractor's current value at
// that step. The snapshot lets a reader see the state that produced the
// violation without replaying the run.
type Witness struct {
Property string
Reason string
Step int
IsError bool
Extractors map[string]json.RawMessage
}
// captureWitness records the witness for a property that just transitioned to
// violated, snapshotting the current extractor values so the cause is visible
// after the run.
func (v *Verifier) captureWitness(name string) {
evaluator, ok := v.evaluators[name]
if !ok {
return
}
violation := evaluator.Violation()
if violation == nil {
return
}
v.witnesses[name] = Witness{
Property: name,
Reason: violation.Reason,
Step: violation.Step,
IsError: violation.IsError,
Extractors: v.extractorSnapshot(),
}
}
// extractorSnapshot encodes every named extractor's current value as JSON. A
// nil value (extractor never advanced or its value did not survive Export)
// is recorded as JSON null.
func (v *Verifier) extractorSnapshot() map[string]json.RawMessage {
if len(v.extractors) == 0 {
return nil
}
snapshot := make(map[string]json.RawMessage, len(v.extractors))
for _, extractor := range v.extractors {
value := extractor.curr
if value == nil {
value = []byte("null")
}
snapshot[extractor.name] = append(json.RawMessage(nil), value...)
}
return snapshot
}
// Witness returns the captured violation witness for a property, or nil if the
// property has not violated. Callers consult this after EvaluateProperties (or
// Finalize) reports a violation to surface the cause and the state at onset.
func (v *Verifier) Witness(name string) *Witness {
witness, ok := v.witnesses[name]
if !ok {
return nil
}
return &witness
}
// Finalize drives each evaluator to its terminal verdict and returns the names
// of properties that violate only at run end (a liveness obligation that never
// discharged), capturing a witness for each. Properties already violated
// mid-run are not re-reported here.
func (v *Verifier) Finalize() []string {
var ended []string
for name, evaluator := range v.evaluators {
if v.priorVerdicts[name] == ltl.VerdictViolated {
continue
}
if evaluator.Finalize() == ltl.VerdictViolated {
ended = append(ended, name)
v.captureWitness(name)
v.priorVerdicts[name] = ltl.VerdictViolated
}
}
sort.Strings(ended)
return ended
}
// NewlyViolatedProperties returns the names of properties whose verdict
// transitioned from non-Violated to Violated on the most recent
// EvaluateProperties call, sorted lexicographically. Returns nil if no
// transition occurred or EvaluateProperties has not been called.
//
// This is the onset set: each property name appears at most once across a
// run's traces, at the step where the violation first fired. Subsequent
// steps where the property remains violated (LTL `always` sticky semantics)
// will not list it. Use this for trace emission and summary reporting so the
// onset is the only step that surfaces the violation event; use
// EvaluateProperties for residual / current-verdict needs.
func (v *Verifier) NewlyViolatedProperties() []string {
return append([]string(nil), v.newlyViolated...)
}
// Residuals returns the residual formula for each registered property after
// the most recent EvaluateProperties call. Properties whose violation was
// caused by a thrown predicate surface as ErrorFormula, sourced from the
// captured witness, so the replay UI can render "predicate threw" inline.
func (v *Verifier) Residuals() map[string]ltl.Formula {
residuals := map[string]ltl.Formula{}
for name, evaluator := range v.evaluators {
if witness, ok := v.witnesses[name]; ok && witness.IsError {
residuals[name] = ltl.ErrorFormula{Message: witness.Reason}
continue
}
residuals[name] = evaluator.Residual()
}
return residuals
}
// NextAction resolves an action for the current step by invoking the bundled
// __sanderlingNextAction__(), which runs the SHARED picker (pick.ts) over the
// shared Pcg. Setup-generator precedence and the 16-attempt retry both live in
// runtime-entry.ts now, so this is a thin call-and-decode. A null result (the
// generator declined to act) reports ErrNoAction.
func (v *Verifier) NextAction() (Action, error) {
if v.nextActionFn == nil {
return Action{}, ErrNoAction
}
value, err := v.nextActionFn(goja.Undefined())
if err != nil {
return Action{}, fmt.Errorf("next action: %w", err)
}
if value == nil || goja.IsNull(value) || goja.IsUndefined(value) {
return Action{}, ErrNoAction
}
raw, err := json.Marshal(value.Export())
if err != nil {
return Action{}, fmt.Errorf("marshal action: %w", err)
}
return DecodeAction(raw)
}
var ErrNoAction = errors.New("verifier: no action available")
func (v *Verifier) formulaThunk(index int) func() (bool, error) {
return func() (bool, error) {
formula := v.formulas[index]
result, err := formula.predicate(goja.Undefined())
if err != nil {
return false, err
}
return result.ToBoolean(), nil
}
}
// frameworkPackage is the AOSP framework package. Both the app's own window
// (android:id/content) and system chrome carry it, so it is treated as neutral
// (transparent) when deciding which window owns a node, rather than as a foreign
// package that would put the app's content out of scope.
const frameworkPackage = "android"
// scopedElements returns the set of elements that belong to the app under test.
// It walks the window tree propagating each node's owning package: a node's
// owner is the nearest ancestor-or-self with a concrete package (empty and the
// neutral android framework package are transparent). A node is in scope when no
// concrete foreign package owns it -- the app's own window carries no package on
// Compose apps -- or the owner is the app package itself. This drops whole
// foreign windows (the soft keyboard, system UI, the launcher) AND their
// empty-package child wrappers, e.g. a keyboard's "Settings" key, which a
// per-element package check admits because the wrapper itself has no package.
//
// With no app package configured (iOS/web, or an unscoped run) every node is in
// scope, preserving prior behavior.
func (v *Verifier) scopedElements() map[*hierarchy.Element]bool {
if v.scopeCacheTree == v.lastTree && v.scopeCache != nil {
return v.scopeCache
}
scope := make(map[*hierarchy.Element]bool, len(v.lastTree.Elements))
unscoped := v.appPackage == ""
if v.lastTree.Root == nil {
for _, element := range v.lastTree.Elements {
scope[element] = true
}
} else {
var walk func(node *hierarchy.Node, owner string)
walk = func(node *hierarchy.Node, owner string) {
if pkg := node.Element.Package; pkg != "" && pkg != frameworkPackage {
owner = pkg
}
if unscoped || owner == "" || owner == v.appPackage {
scope[&node.Element] = true
}
for _, child := range node.Children {
walk(child, owner)
}
}
walk(v.lastTree.Root, "")
}
v.scopeCache = scope
v.scopeCacheTree = v.lastTree
return scope
}
// selectorForElement builds a canonical "key:value" selector that resolves
// back to the given element via hierarchy.Tree.Find. Prefers resource-id (the
// testTag carrier on Android / accessibilityIdentifier on iOS), falling back
// to text and content-description so action-gated properties can still tell
// what was tapped even on legacy nodes without a testTag. Returns "" when no
// candidate selector uniquely resolves to the picked element so the runner
// keeps using the action's coordinates without re-routing to a sibling that
// shares the same id/text.
func selectorForElement(tree *hierarchy.Tree, element *hierarchy.Element) string {
if element == nil || tree == nil {
return ""
}
candidates := make([]string, 0, 4)
if element.ResourceID != "" {
candidates = append(candidates, "id:"+element.ResourceID)
}
// Some platforms surface the Compose testTag only in the attributes map
// (the sidecar doesn't always promote it to resource-id). Try the raw
// attribute keys before falling back to text-based selectors so an
// element with a unique testTag still gets identified.
for _, key := range []string{"testTag", "identifier", "accessibilityIdentifier"} {
if value := element.Attributes[key]; value != "" {
candidates = append(candidates, key+":"+value)
}
}
if element.Text != "" {
candidates = append(candidates, "text:"+element.Text)
}
if element.Description != "" {
candidates = append(candidates, "desc:"+element.Description)
}
for _, selector := range candidates {
resolved := tree.Find(selector)
if resolved == nil || resolved != element {
continue
}
return selector
}
return ""
}
// candidatesForVerb enumerates the host-side targets a builtin verb may draw
// from, in v.lastTree.Elements ORDER (the order is part of the picker's parity
// contract). The filters are LIFTED from the old Go picker:
//
// taps/doubleTaps/longPresses: clickable + enabled + positive bounds
// typing: editable + enabled + positive bounds
// scrolls: scrollable attribute + positive bounds
// swipes: any in-scope element with positive bounds
//
// Every candidate carries the resolving selector so the runner can re-route by
// id/text. Out-of-scope nodes (the soft keyboard, system UI, the launcher) are
// dropped by scopedElements.
func (v *Verifier) candidatesForVerb(verb string) []candidate {
if v.lastTree == nil {
return nil
}
scope := v.scopedElements()
var result []candidate
for _, element := range v.lastTree.Elements {
if !scope[element] {
continue
}
if !verbAccepts(verb, element) {
continue
}
x, y := element.Bounds.Center()
result = append(result, candidate{
x: x,
y: y,
width: element.Bounds.Width(),
height: element.Bounds.Height(),
selector: selectorForElement(v.lastTree, element),
})
}
return result
}
type candidate struct {
x, y int
width, height int
selector string
}
// verbAccepts applies the per-verb element filter.
func verbAccepts(verb string, element *hierarchy.Element) bool {
positiveBounds := element.Bounds.Width() > 0 && element.Bounds.Height() > 0
switch verb {
case "taps", "doubleTaps", "longPresses":
return element.Clickable && element.Enabled && positiveBounds
case "typing":
return element.Editable && element.Enabled && positiveBounds
case "scrolls":
return element.Attributes["scrollable"] == "true" && positiveBounds
case "swipes":
// Any visible element is a valid swipe origin, but it must have real
// bounds: a zero-bounds node centers at (0,0), and a downward swipe from
// the top-left corner is the system gesture that pulls down the
// notification shade, dragging the fuzzer out of the app.
return positiveBounds
default:
return false
}
}