preprocessor

package
v0.0.29 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Apr 19, 2026 License: MIT Imports: 16 Imported by: 0

Documentation

Overview

Package preprocessor implements the proven -toolexec preprocessor.

Run is the single entrypoint. It is called from cmd/proven's main with os.Args[1:] and returns a shell-style exit code. Everything below is intentionally private: the preprocessor is distributed as the proven binary, not as an importable library.

Shape follows rewire (github.com/GiGurra/rewire) closely: a fast dispatch on the tool being wrapped, AST-based scanning of the source files the Go tool received, a minimal set of rewrites emitted to temp files that are appended to the tool's argv, and a final forward to the real tool. Nothing in the original source tree is modified.

See docs/todo/roadmap.md for the sequence of phases; the current implementation covers Phase 1 (stub injection for pkg/proven) only.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func AnalyzeFuncWithReturns added in v0.0.9 

func AnalyzeFuncWithReturns(caller *ast.FuncDecl, summary *PackageSummary, imp *importInfo, imports map[string]*PackageSummary, fset *token.FileSet, diags *[]Diagnostic) ([]CallDischarge, []Predicate, [][]Predicate)

AnalyzeFuncWithReturns is the richer variant of AnalyzeFunc: in addition to the call-discharge list, it returns the derived postconditions — the intersection of leaf / Or facts on the returned identifier across every ReturnStmt. An empty slice is returned when the function has no return statements, returns a non-identifier result, or carries no facts at exit.

The analyzer runs the same flow-sensitive walk either way; the return-snapshot bookkeeping is linear in the number of returns and does not add an asymptotic cost. Functions whose bodies establish no facts produce empty snapshots cheaply.

func AnalyzePackage 

func AnalyzePackage(importPath string, sources []string) (*PackageSummary, []CallDischarge, *token.FileSet, error)

AnalyzePackage parses each source file once, builds the package summary (Phase 2), then walks every FuncDecl in every file and collects the call-site discharges (Phase 3/4). Returns the summary, the flat list of discharges across the package, and the FileSet that owns the Pos values inside each discharge — callers need the same fset to resolve Pos to (file, line, col) for diagnostics.

Short-circuits packages that need no analysis: if the scan finds no obligations (summary.Funcs empty) the analyzer is skipped entirely — no caller in the package can reference an obligation that is not in summary.Funcs. This is the common case for the many stdlib and non-proven-using user packages that pass through the preprocessor on every build.

func Run 

func Run(args []string, stderr io.Writer) int

Run executes the preprocessor with the toolexec-style arguments (os.Args[1:]): the first element is the path to the underlying Go tool (compile, link, asm, ...), and the rest are the tool's own arguments. Run returns the exit code to hand back to the OS.

The planner decides the effect of this invocation: forward unchanged, forward with modified argv (Phase 1 stub injection), or abort the build with one or more Go-standard diagnostics (Phase 5, undischarged obligation). Diagnostics go to stderr in the `file:line:col: message` layout cmd/compile uses so editors and CI log scrapers handle them without special casing.

Types

type CallDischarge 

type CallDischarge struct {
	Pos       token.Pos
	CalleePkg string
	CalleeKey string
	Params    []ParamDischarge
}

CallDischarge records the obligation-discharge status for one call site analyzed against the caller's flow facts.

CalleePkg is empty for same-package callees and holds the callee's import path for cross-package ones; CalleeKey is the summary key within that package (bare function name, or "Recv.Method" for methods). Together they uniquely identify which callee's obligation signature was consulted.

func AnalyzeFunc 

func AnalyzeFunc(caller *ast.FuncDecl, summary *PackageSummary, imp *importInfo, imports map[string]*PackageSummary, fset *token.FileSet, diags *[]Diagnostic) []CallDischarge

AnalyzeFunc walks caller's body and returns one CallDischarge per call to a function whose key appears in summary.Funcs (same-package) or in any of imports[pkg].Funcs (cross-package). Callees without a summary entry (external, or annotated only via proven.Returns with no ParamPreds) produce no entries.

imports may be nil — same-package-only mode. Tests that do not need cross-package resolution pass nil; Phase 6's compile path assembles the map from the compile's -importcfg.

fset + diags enable strict-mode reporting at prove/trust/proven sites where a predicate expression cannot be resolved to a named func or pkg.Name selector. Pass nil for either to disable strict mode (used by tests that do not surface diagnostics).

func (CallDischarge) Undischarged 

func (c CallDischarge) Undischarged() bool

Undischarged reports whether any parameter of this call site still has a missing predicate after flow analysis.

type Chain added in v0.0.29 

type Chain struct {
	// NextCmd is the argv that should replace the bare tool
	// invocation. Empty when no --and-then was present.
	NextCmd []string
}

Chain captures the optional `--and-then` chain of successor preprocessor invocations. A non-empty NextCmd means proven was invoked as one link in a chain like: 

proven [proven-args...] --and-then pre2 [pre2-args...] --and-then pre3 ... /abs/go/tool args...

When the chain is active, proven still does its normal preprocessing work, but instead of exec'ing the real Go tool directly it exec's NextCmd with the tool path (and possibly-rewritten tool args) appended. Each link in the chain peels off one --and-then and forwards the remainder, so the last link sees a classic toolexec invocation and needs no --and-then awareness at all.

type Diagnostic 

type Diagnostic struct {
	File string
	Line int
	Col  int
	Msg  string
}

Diagnostic is one Go-standard preprocessor message. The String form matches `cmd/compile`'s `file:line:col: message` layout so editors and CI output parsers pick it up without special casing.

func (Diagnostic) String 

func (d Diagnostic) String() string

type EvalResult added in v0.0.19 

type EvalResult int

EvalResult is the outcome of evaluating a library predicate on a literal argument expression. 

const (
	// EvalSkip: the predicate is not library-known, the argument
	// expression is not in the evaluator's recognized shape set, or
	// the combination is not applicable. The caller falls back to
	// normal discharge.
	EvalSkip EvalResult = iota
	// EvalHolds: the predicate evaluates to true on the literal.
	EvalHolds
	// EvalFails: the predicate evaluates to false on the literal.
	// The caller treats this as "cannot prove" (the literal cannot
	// satisfy the predicate on any call).
	EvalFails
)

type Event added in v0.0.23 

type Event struct {
	Kind  eventKind
	Pos   token.Pos
	Scope int
	Pred  Predicate
	Alts  []Predicate
	Var   string

	// DischargeIdx / ParamIdx stitch query events back into the
	// CallDischarge records the analyzer emits: each query's
	// resolution result updates the Missing / MissingOrs slices of
	// the corresponding parameter discharge.
	DischargeIdx int
	ParamIdx     int
}

Event is one entry in the recorded fact stream. The semantics of each field depend on kind: 

evSourceLeaf: Pred holds on Var at Pos inside Scope.
evSourceOr:   One of Alts holds on Var at Pos inside Scope.
evWrite:      Var was mutated at Pos inside Scope. Any Source
              event on Var in an ancestor-or-self scope preceding
              this Write is no longer visible to later queries.
evQueryLeaf:  A call-site obligation that Pred hold on Var at Pos.
              The resolver decides whether any reachable source
              discharges it.
evQueryOr:    Same, but the obligation is disjunctive over Alts.

Var in Phase 1 is always a bare identifier name; Phase 2 widens it to a canonical expression key that includes selector paths.

type Fact 

type Fact struct {
	Pred Predicate
	Var  string
}

Fact asserts that predicate Pred holds on the variable named Var at a given program point.

type FactSet 

type FactSet struct {
	// contains filtered or unexported fields
}

FactSet is a compact intermediate used only by collectGuardFacts and the emit-as-sources helpers. It carries the (predicate, var) pairs (and disjunctive equivalents) that a guard expression proves when true, so they can be emitted as Source events at the branch boundary. The previous full-featured implementation (Has, Clone, Forget, etc.) was retired with the FactSet-based resolver in Phase 3; only the accumulator surface remains.

func (*FactSet) Add 

func (fs *FactSet) Add(f Fact)

Add records a leaf fact in the set; duplicates are coalesced.

type FuncSummary 

type FuncSummary struct {
	Name        string
	Recv        string
	ParamPreds  map[int][]Predicate
	ParamOrs    map[int][][]Predicate
	ReturnPreds []Predicate
	ReturnOrs   [][]Predicate

	// DerivedReturnPreds / DerivedReturnOrs are postconditions the
	// analyzer inferred from the body — the intersection of fact sets
	// on the returned identifier across every ReturnStmt. Populated
	// after the flow-sensitive pass (AnalyzeFunc). Callers plant them
	// as facts at assignment sites the same way as the explicit
	// ReturnPreds / ReturnOrs above, so a function without an
	// explicit proven.Returns can still advertise the facts its body
	// actually proves. Keeping the explicit fields distinct preserves
	// the "this is the declared contract" marker for API-boundary
	// functions that opt into a claim the compiler verifies.
	DerivedReturnPreds []Predicate
	DerivedReturnOrs   [][]Predicate
}

FuncSummary collects the proven.That / proven.Returns facts declared in one function body.

ParamPreds: parameter position (0-based) to the AND-composed list of leaf-predicate obligations asserted on that parameter by every proven.That call in the body. proven.And(a, b) and its nested forms flatten into additional leaves here. An entry is present only if at least one such call exists; absent parameters carry no obligations.

ParamOrs: parameter position to the AND-composed list of disjunctive obligations, each inner []Predicate representing one proven.Or(a, b) call's OR-alternatives (the Or's arguments must be named leaves — nested combinators inside Or are rejected by strict mode). Any leaf holding, or an exact-match Or-fact, is enough to discharge one disjunction.

ReturnPreds / ReturnOrs: the postcondition counterparts, merged across every proven.Returns / trust.Returns call in the body. Phase 2 treats these as bags because tracking "which return value position is constrained" would require flow analysis over the body, which is Phase 3's job.

Recv is the receiver type identifier for methods (without the leading star), empty for free functions.

func (*FuncSummary) Key 

func (s *FuncSummary) Key() string

Key returns a stable identifier for looking up the summary from a call site: "Func" for free functions, "Recv.Method" for methods.

type InferRule 

type InferRule struct {
	From  []Predicate
	Given []Predicate
	To    []Predicate
}

InferRule is one declared package-scope implication rule harvested from `var _ = infer.From(premises...).[Given(contexts...).]To(conclusions...)`.

Every slot is variadic and AND-composed — the rule reads as "if every From predicate AND every Given predicate holds on the variable, then every To predicate holds on it". Given is empty when no .Given(...) step was present.

Rules are trusted — the scanner does not verify that the implication actually holds (docs/design.md). Unresolvable predicate arguments (combinator calls, function literals, etc.) cause the rule to be skipped rather than silently stored with an empty identity.

type PackageSummary 

type PackageSummary struct {
	ImportPath string
	Funcs      map[string]*FuncSummary
	Rules      []InferRule
}

PackageSummary is the scanner output for one compile unit. Only functions with at least one obligation are present in Funcs.

func ScanPackage 

func ScanPackage(importPath string, sources []string) (*PackageSummary, error)

ScanPackage parses each source file and returns the obligation summary for the package. importPath is the Go import path of the package being scanned (from `compile -p <importpath>`); it populates Predicate.Pkg for same-package predicate references.

ScanPackage is tolerant of source files that do not import pkg/proven: they produce no entries. A syntax error in any file aborts the scan with a wrapped error, matching the compile step's fail-fast behavior.

type ParamDischarge 

type ParamDischarge struct {
	ParamIdx    int
	ArgName     string
	ArgExpr     string
	Required    []Predicate
	Missing     []Predicate
	RequiredOrs [][]Predicate
	MissingOrs  [][]Predicate
}

ParamDischarge records per-parameter discharge: which predicates the callee required (from Phase 2's summary) and which remained missing from the caller's fact set at the call site.

RequiredOrs / MissingOrs carry the disjunctive-obligation side: each entry is one proven.Or(alts...) obligation on the parameter. An Or-obligation is discharged when any alt leaf holds or a matching Or-fact was planted. Surfaced separately from the leaf lists so diagnostics can render the whole Or at once instead of emitting one complaint per disjunct.

ArgName is the canonical fact-subject key used internally by the resolver (a bare identifier, a selector-path, or a synthetic "$argN" for virtually-planted literal / nested-call arguments). ArgExpr is the rendered source form of the actual call-site argument — used in diagnostics so users see "holder.Value" / "5" / "foo(x)" at the error line, not the internal key.

type Plan 

type Plan struct {
	NewArgs []string
	Cleanup func()
	Diags   []Diagnostic
}

Plan is the decision made for one toolexec compile invocation.

NewArgs is the argv to forward to the real compile tool, or nil to leave the incoming toolArgs unchanged.

Cleanup is deferred after the forwarded compile returns; may be nil.

Diags, if non-empty, is printed to stderr by the caller and the preprocessor exits non-zero without forwarding the compile. A Plan may carry both NewArgs and Diags only if a handler decides to emit diagnostics after partially rewriting — not a case the current implementation exercises.

type Predicate 

type Predicate struct {
	Pkg  string
	Name string
}

Predicate identifies a predicate function by its declaring package and identifier name. For predicates defined in the scanned package itself, Pkg is that package's own import path — giving every predicate a uniform qualified identity that Phase 3 can compare without special-casing same-package lookup.

type TrailingPreds added in v0.0.8 

type TrailingPreds struct {
	Leaves []Predicate
	Ors    [][]Predicate
}

TrailingPreds carries the result of resolving the trailing predicate list of a prove.That / prove.Must / trust.That call. Leaves are leaf / And-decomposed predicates; Ors are disjunctive facts (from inline proven.Or(...)) that should be planted on the same LHS variable.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.