Files
sanderling/internal/verifier/worker.go
T
pj 15f3906f1c feat(verifier): scope random-action targets to app package
Random tap/doubleTap/type/swipe candidates now exclude nodes whose package differs from the app under test, so exploration never fuzzes the soft keyboard, system UI, or permission dialogs. An unset app package or an element with no package stays in scope, preserving behavior on iOS.
2026-05-31 12:50:26 +05:30

781 lines
24 KiB
Go

package verifier
import (
"bytes"
"encoding/json"
"errors"
"fmt"
"maps"
"math/rand/v2"
"sort"
"strings"
"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
actionGenerator goja.Value
setupGenerator goja.Value
evaluators map[string]*ltl.Evaluator
priorVerdicts map[string]ltl.Verdict
newlyViolated []string
lastTree *hierarchy.Tree
lastAction *Action
lastLogs []LogEntry
lastExceptions []Exception
stepTime time.Time
runStart time.Time
appPackage string
rng *rand.Rand
}
type Option func(*Verifier)
func WithRand(rng *rand.Rand) Option {
return func(v *Verifier) { v.rng = rng }
}
// 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{},
rng: rand.New(rand.NewPCG(0, 0)),
}
for _, option := range options {
option(verifier)
}
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)
}
}
if actionsValue := v.runtime.GlobalObject().Get("actions"); actionsValue != nil && !goja.IsUndefined(actionsValue) && !goja.IsNull(actionsValue) {
v.actionGenerator = actionsValue
}
if setupValue := v.runtime.GlobalObject().Get("setup"); setupValue != nil && !goja.IsUndefined(setupValue) && !goja.IsNull(setupValue) {
v.setupGenerator = setupValue
}
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:
return ltl.Thunk(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.lastAction = input.LastAction
v.lastLogs = input.Logs
v.lastExceptions = input.Exceptions
v.stepTime = input.StepTime
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.
// refreshPredicateErrors relies on this to safely re-call predicates.
for index, extractor := range v.extractors {
previous := extractor.handle.Get("current")
_ = extractor.handle.Set("previous", previous)
newValue, err := extractor.getter(goja.Undefined(), state)
if err != nil {
return fmt.Errorf("extractor %d: %w", index, err)
}
_ = extractor.handle.Set("current", newValue)
extractor.prev = extractor.curr
extractor.curr = encodeExtractorValue(newValue)
}
return nil
}
// 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 inspect
// 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].handle.Set("current", 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
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 {
verdicts[name] = evaluator.ObserveAt(stepTime)
}
v.refreshPredicateErrors()
var onset []string
for name, verdict := range verdicts {
if verdict == ltl.VerdictViolated && v.priorVerdicts[name] != ltl.VerdictViolated {
onset = append(onset, name)
}
}
sort.Strings(onset)
v.newlyViolated = onset
next := make(map[string]ltl.Verdict, len(verdicts))
maps.Copy(next, verdicts)
v.priorVerdicts = next
return verdicts
}
// 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 that errored during
// predicate evaluation surface as ErrorFormula so the inspect 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 predicateErr := v.PredicateError(name); predicateErr != nil {
residuals[name] = ltl.ErrorFormula{Message: predicateErr.Error()}
continue
}
residuals[name] = evaluator.Residual()
}
return residuals
}
// NextAction resolves an action for the current step. The setup generator,
// when registered, runs first; if it yields an action, that wins. When setup
// returns ErrNoAction (all branches empty) the call falls through to the
// root action generator with the existing retry semantics. Setup is consulted
// every step, so state regression (e.g. a logout under fuzz) automatically
// re-engages the precondition.
func (v *Verifier) NextAction() (Action, error) {
if v.setupGenerator != nil {
action, err := v.resolveGenerator(v.setupGenerator)
if err == nil {
return action, nil
}
if !errors.Is(err, ErrNoAction) {
return Action{}, err
}
}
if v.actionGenerator == nil {
return Action{}, ErrNoAction
}
const maxRetries = 16
for range maxRetries {
action, err := v.resolveGenerator(v.actionGenerator)
if err == nil {
return action, nil
}
if !errors.Is(err, ErrNoAction) {
return Action{}, err
}
}
return Action{}, ErrNoAction
}
var ErrNoAction = errors.New("verifier: no action available")
func (v *Verifier) formulaThunk(index int) func() bool {
return func() bool {
formula := v.formulas[index]
result, err := formula.predicate(goja.Undefined())
if err != nil {
formula.err = err
return false
}
formula.err = nil
return result.ToBoolean()
}
}
// refreshPredicateErrors re-invokes every registered predicate so that
// formula.err reflects the current step rather than a latched first-step
// throw. EvaluateProperties short-circuits once a property has latched to
// violated, so without this refresh the runner's per-step "predicate error"
// log freezes on whatever the predicate threw at step 1. The refreshed errors
// have no effect on verdicts.
//
// Invariant: predicates may be re-invoked here outside the LTL gate that
// would normally skip them (e.g. an `implies` consequent whose antecedent is
// false). They must therefore be side-effect-free reads of extractor state;
// any spec that asserts internal preconditions inside a predicate could
// surface a spurious error in the inspect UI without affecting verdicts.
func (v *Verifier) refreshPredicateErrors() {
for _, formula := range v.formulas {
result, err := formula.predicate(goja.Undefined())
if err != nil {
formula.err = err
continue
}
_ = result
formula.err = nil
}
}
// PredicateError returns the first goja error raised by any thunk in the
// named property's formula tree, or nil if none fired. Callers typically
// consult this after EvaluateProperties reports a violation to distinguish
// a genuine predicate-false verdict from a malformed spec.
func (v *Verifier) PredicateError(name string) error {
rootIndex, ok := v.properties[name]
if !ok {
return nil
}
return v.firstThunkError(rootIndex)
}
func (v *Verifier) firstThunkError(index int) error {
if index < 0 || index >= len(v.formulaSpecs) {
return nil
}
spec := v.formulaSpecs[index]
switch spec.kind {
case specKindThunk:
return v.formulas[spec.predicateIndex].err
case specKindImplies, specKindOr, specKindAnd:
if err := v.firstThunkError(spec.childA); err != nil {
return err
}
return v.firstThunkError(spec.childB)
case specKindNow, specKindNext, specKindEventually, specKindNot, specKindAlways:
return v.firstThunkError(spec.childA)
}
return nil
}
func (v *Verifier) resolveGenerator(generator goja.Value) (Action, error) {
object := generator.ToObject(v.runtime)
if object == nil {
return Action{}, fmt.Errorf("generator is not an object")
}
kindValue := object.Get(tagInternalKind)
if kindValue == nil {
return Action{}, fmt.Errorf("generator missing internal kind tag")
}
switch kindValue.String() {
case internalKindActions:
generateValue := object.Get("generate")
generate, ok := goja.AssertFunction(generateValue)
if !ok {
return Action{}, fmt.Errorf("actions handle missing generate function")
}
result, err := generate(goja.Undefined())
if err != nil {
return Action{}, fmt.Errorf("generate: %w", err)
}
return v.pickFromResult(result)
case internalKindWeighted:
entries := object.Get("entries").ToObject(v.runtime)
if entries == nil {
return Action{}, fmt.Errorf("weighted handle missing entries")
}
picked, err := v.pickWeighted(entries)
if err != nil {
return Action{}, err
}
return v.resolveGenerator(picked)
case internalKindBuiltinTaps:
return v.generateRandomTap()
case internalKindBuiltinDoubleTaps:
return v.generateRandomDoubleTap()
case internalKindBuiltinTyping:
return v.generateRandomInput()
case internalKindBuiltinSwipes:
return v.generateRandomSwipe()
case internalKindBuiltinWaitOnce:
return Action{Kind: ActionKindWait, DurationMillis: 500}, nil
case internalKindBuiltinPressKey:
return v.generateRandomPressKey()
default:
return Action{}, fmt.Errorf("unknown generator kind %q", kindValue.String())
}
}
// generateRandomTap picks a visible, tappable element from the last
// hierarchy snapshot and returns a Tap action targeting its center.
func (v *Verifier) generateRandomTap() (Action, error) {
return v.generateRandomTapKind(ActionKindTap)
}
// generateRandomDoubleTap is the DoubleTap counterpart of generateRandomTap.
// Real user gestures include double-tap (image zoom, like-to-favorite,
// play/pause); a fuzzer that never emits one cannot exercise either those
// features or the sub-100ms race windows that single-step Tap cadence misses.
func (v *Verifier) generateRandomDoubleTap() (Action, error) {
return v.generateRandomTapKind(ActionKindDoubleTap)
}
// inScope reports whether an element belongs to the app under test. Nodes from
// another package (the soft keyboard, system UI, permission dialogs) are out of
// scope. An unset app package or an element with no package falls through to in
// scope, preserving behavior on platforms that omit the attribute (e.g. iOS).
func (v *Verifier) inScope(element *hierarchy.Element) bool {
if v.appPackage == "" || element.Package == "" {
return true
}
return element.Package == v.appPackage
}
func (v *Verifier) generateRandomTapKind(kind ActionKind) (Action, error) {
if v.lastTree == nil {
return Action{}, ErrNoAction
}
candidates := make([]*hierarchy.Element, 0, len(v.lastTree.Elements))
for _, element := range v.lastTree.Elements {
if !element.Clickable || !element.Enabled {
continue
}
if !v.inScope(element) {
continue
}
if element.Bounds.Right-element.Bounds.Left <= 0 || element.Bounds.Bottom-element.Bounds.Top <= 0 {
continue
}
candidates = append(candidates, element)
}
if len(candidates) == 0 {
return Action{}, ErrNoAction
}
picked := candidates[v.rng.IntN(len(candidates))]
x, y := picked.Bounds.Center()
return Action{Kind: kind, X: x, Y: y}, nil
}
// inputCorpus is the edge-case string pool the typing builtin draws from to
// stress field parsing: empty, whitespace, overflow length, unicode, numeric
// boundaries, and common injection payloads.
var inputCorpus = []string{
"",
"a",
strings.Repeat("a", 4096),
"🙂🔥💸",
" ",
"\t\n",
"-1",
"999999999999999999999",
"0.0000001",
"1e10",
"'; DROP TABLE--",
"<script>alert(1)</script>",
"../../etc/passwd",
"%s%n",
"NaN",
}
// generateRandomInput picks a visible, editable, enabled element from the last
// hierarchy snapshot and types a random edge-case value into it. The runner
// taps the target coordinates to focus before typing, so this works on both
// native and web with no driver-side dispatch change.
func (v *Verifier) generateRandomInput() (Action, error) {
if v.lastTree == nil {
return Action{}, ErrNoAction
}
candidates := make([]*hierarchy.Element, 0, len(v.lastTree.Elements))
for _, element := range v.lastTree.Elements {
if !element.Editable || !element.Enabled {
continue
}
if !v.inScope(element) {
continue
}
if element.Bounds.Right-element.Bounds.Left <= 0 || element.Bounds.Bottom-element.Bounds.Top <= 0 {
continue
}
candidates = append(candidates, element)
}
if len(candidates) == 0 {
return Action{}, ErrNoAction
}
picked := candidates[v.rng.IntN(len(candidates))]
x, y := picked.Bounds.Center()
value := inputCorpus[v.rng.IntN(len(inputCorpus))]
return Action{Kind: ActionKindInputText, X: x, Y: y, Text: value}, nil
}
// generateRandomSwipe emits a swipe over a random enabled element or the
// whole screen, in a random direction. Returns ErrNoAction only when we have
// no tree to size a gesture off of.
func (v *Verifier) generateRandomSwipe() (Action, error) {
if v.lastTree == nil || len(v.lastTree.Elements) == 0 {
return Action{}, ErrNoAction
}
candidates := make([]*hierarchy.Element, 0, len(v.lastTree.Elements))
for _, element := range v.lastTree.Elements {
if v.inScope(element) {
candidates = append(candidates, element)
}
}
if len(candidates) == 0 {
return Action{}, ErrNoAction
}
element := candidates[v.rng.IntN(len(candidates))]
cx, cy := element.Bounds.Center()
if cx <= 0 || cy <= 0 {
return Action{}, ErrNoAction
}
// Pick a direction: 0=up 1=down 2=left 3=right; magnitude 200-600 px.
magnitude := 200 + v.rng.IntN(401)
toX, toY := cx, cy
switch v.rng.IntN(4) {
case 0:
toY = cy - magnitude
case 1:
toY = cy + magnitude
case 2:
toX = cx - magnitude
case 3:
toX = cx + magnitude
}
if toX < 0 {
toX = 0
}
if toY < 0 {
toY = 0
}
return Action{
Kind: ActionKindSwipe,
FromX: cx,
FromY: cy,
ToX: toX,
ToY: toY,
DurationMillis: 250,
}, nil
}
func (v *Verifier) generateRandomPressKey() (Action, error) {
// Keep exploration gentle: only "back" for now. Home/menu would navigate
// away from the app under test.
return Action{Kind: ActionKindPressKey, Key: "back"}, nil
}
func (v *Verifier) pickFromResult(result goja.Value) (Action, error) {
if result == nil || goja.IsUndefined(result) || goja.IsNull(result) {
return Action{}, ErrNoAction
}
object := result.ToObject(v.runtime)
if object == nil {
return Action{}, ErrNoAction
}
lengthValue := object.Get("length")
if lengthValue == nil {
return jsValueToAction(v.runtime, result)
}
length := int(lengthValue.ToInteger())
if length == 0 {
return Action{}, ErrNoAction
}
pick := v.rng.IntN(length)
return jsValueToAction(v.runtime, object.Get(fmt.Sprintf("%d", pick)))
}
func (v *Verifier) pickWeighted(entries *goja.Object) (goja.Value, error) {
lengthValue := entries.Get("length")
if lengthValue == nil {
return nil, fmt.Errorf("weighted entries missing length")
}
length := int(lengthValue.ToInteger())
if length == 0 {
return nil, ErrNoAction
}
weights := make([]float64, length)
generators := make([]goja.Value, length)
totalWeight := 0.0
for index := range length {
entry := entries.Get(fmt.Sprintf("%d", index)).ToObject(v.runtime)
if entry == nil {
return nil, fmt.Errorf("weighted entry %d not an array", index)
}
weight := entry.Get("0").ToFloat()
generator := entry.Get("1")
if weight < 0 {
weight = 0
}
weights[index] = weight
generators[index] = generator
totalWeight += weight
}
if totalWeight == 0 {
return nil, ErrNoAction
}
pick := v.rng.Float64() * totalWeight
cumulative := 0.0
for index := range length {
cumulative += weights[index]
if pick < cumulative {
return generators[index], nil
}
}
return generators[length-1], nil
}