analysis

Documentation

Overview

Package analysis contains methods that check whether each datalog clause is valid, and whether a set of valid clauses forms a valid datalog program.

Index

• func CheckDecl(decl ast.Decl) []error
• func ExtractPackages(program []parse.SourceUnit) (map[string]*packages.Package, error)
• func RectifyAtom(atom ast.Atom, usedVars VarList) (ast.Atom, []ast.Term, []ast.Variable, []ast.Variable)
• func RewriteClause(decls map[ast.PredicateSym]*ast.Decl, clause ast.Clause) ast.Clause
• type Analyzer
  • func New(extraPredicates map[ast.PredicateSym]ast.Decl, decls []ast.Decl, ...) (*Analyzer, error)
  • func (a *Analyzer) Analyze(program []ast.Clause) (*ProgramInfo, error)
  • func (a *Analyzer) CheckRule(clause ast.Clause) error
  • func (a *Analyzer) EnsureDecl(clauses []ast.Clause) error
• type BoundsAnalyzer
  • func (bc *BoundsAnalyzer) BoundsCheck() error
• type BoundsCheckingMode
• type Nodeset
  • func Stratify(program Program) ([]Nodeset, map[ast.PredicateSym]int, error)
• type Program
• type ProgramInfo
  • func Analyze(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl) (*ProgramInfo, error)
  • func AnalyzeAndCheckBounds(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl, ...) (*ProgramInfo, error)
  • func AnalyzeOneUnit(unit parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl) (*ProgramInfo, error)
• type VarList
  • func NewVarList(m map[ast.Variable]bool) VarList
  • func (vs VarList) AsMap() map[ast.Variable]bool
  • func (vs VarList) Contains(v ast.Variable) bool
  • func (vs VarList) Extend(vars []ast.Variable) VarList
  • func (vs VarList) Find(v ast.Variable) int

Functions

func CheckDecl

func CheckDecl(decl ast.Decl) []error

CheckDecl performs context-free checks to see whether a decl is well-formed.

func ExtractPackages

func ExtractPackages(program []parse.SourceUnit) (map[string]*packages.Package, error)

ExtractPackages turns source units into merged source packages.

func RectifyAtom

func RectifyAtom(atom ast.Atom, usedVars VarList) (ast.Atom, []ast.Term, []ast.Variable, []ast.Variable)

RectifyAtom ensures all arguments of an atom are variables. It returns a tuple (rectified atom, extra terms, fresh variables, defined variables).

An atom p(t_1, ..., t_n) is rectified if each t_i is a variable and all are distinct.

We go a bit further and also ensure that t_i are distinct from a set variables that may have been defined previously ("used"). On the other hand, we do not generate fresh variables for wildcards "_". If the given atom is already rectified in this stronger sense, than extra terms and fresh variables will be empty and boundVars contains atom arguments in left-to-right order.

func RewriteClause

func RewriteClause(decls map[ast.PredicateSym]*ast.Decl, clause ast.Clause) ast.Clause

RewriteClause rewrites a clause using information from declarations.

Types

type Analyzer

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

Analyzer is a struct providing built-in predicates and functions for name analysis.

func New

func New(extraPredicates map[ast.PredicateSym]ast.Decl, decls []ast.Decl, boundsChecking BoundsCheckingMode) (*Analyzer, error)

New creates a new analyzer based on declarations and extra predicates.

func (*Analyzer) Analyze

func (a *Analyzer) Analyze(program []ast.Clause) (*ProgramInfo, error)

Analyze identifies the extensional and intensional predicates of a program, checks every rule and that all references to built-in predicates and functions used in transforms are valid.

func (*Analyzer) CheckRule

func (a *Analyzer) CheckRule(clause ast.Clause) error

CheckRule checks arity and that every variable appearing is bound. A variable is bound when: - it appears in a positive atom, or - is unified (via an equality) with a constant or bound variable. These form the basis for datalog safety (ensuring termination). We permit mode declaration that modify these conditions. A variable is therefore bound when: - a mode declaration forces it as input - it appears as a column in a positive atom that is not declared as input, or - is unified (via an equality) with a constant or bound variable. Also checks that every function application expression has the right number of arguments.

func (*Analyzer) EnsureDecl

func (a *Analyzer) EnsureDecl(clauses []ast.Clause) error

EnsureDecl will ensure there is a declaration for each head of a rule, creating one if necessary.

type BoundsAnalyzer

type BoundsAnalyzer struct {
	RulesMap map[ast.PredicateSym][]ast.Clause
	// contains filtered or unexported fields
}

BoundsAnalyzer to infer and check bounds.

func (*BoundsAnalyzer) BoundsCheck

func (bc *BoundsAnalyzer) BoundsCheck() error

BoundsCheck checks whether the rules respect the bounds.

type BoundsCheckingMode

type BoundsCheckingMode int

BoundsCheckingMode represents a mode for bounds checking.

const (
	// NoBoundsChecking means there is no bounds checking of any kind.
	NoBoundsChecking BoundsCheckingMode = iota
	// LogBoundsMismatch means we log mismatch.
	LogBoundsMismatch
	// ErrorForBoundsMismatch means bounds mismatch leads to error.
	ErrorForBoundsMismatch
)

type Nodeset

type Nodeset map[ast.PredicateSym]struct{}

Nodeset represents a set of nodes in the dependency graph.

func Stratify

func Stratify(program Program) ([]Nodeset, map[ast.PredicateSym]int, error)

Stratify checks whether a program can be stratified. It returns strongly-connected components and a map from predicate to stratum in the affirmative case, an error otherwise. The result list of strata is topologically sorted. Stratification means separating a list of intensional predicate symbols with rules into strata (layers) such that each layer only depends on the evaluation of negated atoms for idb predicates in lower layers.

type Program

type Program struct {
	// Extensional predicate symbols; those that do not appear in the head of a clause with a body.
	EdbPredicates map[ast.PredicateSym]struct{}
	// Intensional predicate symbols; those that do appear in the head of a clause with a body.
	IdbPredicates map[ast.PredicateSym]struct{}
	// Rules that have a body.
	Rules []ast.Clause
}

Program represents a set of rules that we may or may not be able to stratify.

type ProgramInfo

type ProgramInfo struct {
	// Extensional predicate symbols; those that do not appear in the head of a clause with a body.
	EdbPredicates map[ast.PredicateSym]struct{}
	// Intensional predicate symbols; those that do appear in the head of a clause with a body.
	IdbPredicates map[ast.PredicateSym]struct{}
	// Heads of rules without a body.
	InitialFacts []ast.Atom
	// Rules that have a body.
	Rules []ast.Clause
	// Desugared declarations for all predicates, possibly synthetic.
	Decls map[ast.PredicateSym]*ast.Decl
}

ProgramInfo represents the result of program analysis. EdbPredicates and IdbPredicates are disjoint.

func Analyze

func Analyze(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl) (*ProgramInfo, error)

Analyze identifies the extensional and intensional predicates of a program and checks every rule.

func AnalyzeAndCheckBounds

func AnalyzeAndCheckBounds(program []parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl, boundsChecking BoundsCheckingMode) (*ProgramInfo, error)

AnalyzeAndCheckBounds checks every rule, including bounds.

func AnalyzeOneUnit

func AnalyzeOneUnit(unit parse.SourceUnit, extraPredicates map[ast.PredicateSym]ast.Decl) (*ProgramInfo, error)

AnalyzeOneUnit is a convenience method to analyze a program consisting of a single source unit.

type VarList

type VarList struct {
	Vars []ast.Variable
}

VarList is an ordered list of variables.

func NewVarList

func NewVarList(m map[ast.Variable]bool) VarList

NewVarList converts a map representation to a varlist deterministically.

func (VarList) AsMap

func (vs VarList) AsMap() map[ast.Variable]bool

AsMap converts VarList to a map representation.

func (VarList) Contains

func (vs VarList) Contains(v ast.Variable) bool

Contains returns true if this VarList contains the given variable.

func (VarList) Extend

func (vs VarList) Extend(vars []ast.Variable) VarList

Extend returns a new VarList with appended list of variables.

func (VarList) Find

func (vs VarList) Find(v ast.Variable) int

Find returns the index of the given variable, or -1 if not found.