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
- type BoundsAnalyzer
- type BoundsCheckingMode
- type Nodeset
- 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
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ExtractPackages ¶
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 ¶
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 ¶
CheckRule checks that every variable is either "bound" or defined by a transform. A variable in a rule is bound when it appears in a positive atom, or is unified (via an equality) with a constant or another variable that is bound. Also checks that every function application expression has the right number of arguments.
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 ¶
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 ¶
VarList is an ordered list of variables.
func NewVarList ¶
NewVarList converts a map representation to a varlist deterministically.
Source Files