summaries

cfamily.Effects.none

def Effects.none : Effects

Nothing.

cfamily.Effects.any

def Effects.any : Effects

Everything (a call through a pointer).

cfamily.Effects.inputOutputOnly

def Effects.inputOutputOnly : Effects

Input or output only.

cfamily.Effects.readingElsewhere

def Effects.readingElsewhere : Effects

Reading memory elsewhere only.

cfamily.Effects.writingElsewhereOnly

def Effects.writingElsewhereOnly : Effects

Writing memory elsewhere only.

cfamily.Effects.writingElsewhere

def Effects.writingElsewhere : Effects

Writing (and reading) memory elsewhere.

cfamily.Effects.mentions

def Effects.mentions (xs : List DeclId) (x : DeclId) : Bool

Whether the name is among the names.

cfamily.Effects.absentFrom

def Effects.absentFrom (xs : List DeclId) (x : DeclId) : Bool

Whether the name is not among the names.

cfamily.Effects.unionIds

def Effects.unionIds (a : List DeclId) (b : List DeclId) : List DeclId

The names in a and those of b not in a.

cfamily.Effects.join

def Effects.join (a : Effects) (b : Effects) : Effects

Both effects.

cfamily.Effects.joinAll

def Effects.joinAll (es : List Effects) : Effects

All the effects.

cfamily.Effects.sameSize

def Effects.sameSize (a : Effects) (b : Effects) : Bool

Whether two summaries are equal; summaries only grow from round to round, so the sizes of the lists suffice.

cfamily.ChildEffects

record ChildEffects

A child expression’s effects: evaluating it, and writing it as an lvalue.

cfamily.ChildEffects.evaluatedAll

def ChildEffects.evaluatedAll (children : List ChildEffects) : Effects

The effects of evaluating the children, joined.

cfamily.ChildEffects.evaluatedOf

def ChildEffects.evaluatedOf (c : ChildEffects) : Effects

The effects of evaluating a child.

cfamily.EffectExtension

record EffectExtension

How a dialect summarizes its own syntax. expression and statement get the effects of the children (expressions in the order they are written; the statements inside); writesReceiver says whether an lvalue is rooted at the object a member function is called on; declaration gives the effects of declaring an object of a written type (its constructors and destructor); library the effects of a library function; writesThroughArguments the arguments (by position) a library function writes through when those are all it writes elsewhere (snprintf’s buffer), else none; indirect whether variables of a written type refer to memory elsewhere (beyond pointers); indirectDeclarations the variables a dialect’s statement declares that refer elsewhere, given those of the statements inside it; keys a function’s name and short name (by which calls name it: C++’s C::f(int) is called as C::f and f); asynchronous whether calling a function lets the environment’s own events happen (simulated time passing: timers, interrupts), which are not the caller’s effects.

cfamily.EffectTable.summaryAt

def EffectTable.summaryAt (t : EffectTable) (i : Nat) : Effects

The summary of the function at position i of the table t.

cfamily.EffectTable.functionsNamed

def EffectTable.functionsNamed (t : EffectTable) (f : String) : Option FunctionsNamed

The functions the key f names in the table t, if any.

cfamily.EffectTable.named

def EffectTable.named (t : EffectTable) (f : String) : Effects

The joined summaries of the functions of the table t whose name or short name is f, the first outermost: s1 joined with (s2 joined with … none).

cfamily.EffectTable.throughPointer

def EffectTable.throughPointer (t : EffectTable) : Effects

What a call through a pointer may do: what the functions whose address the program takes may (anything when the table t does not know them).

cfamily.EffectTable.defines

def EffectTable.defines (t : EffectTable) (f : String) : Bool

Whether the program of the table t defines a function named f (else it is a library function).

cfamily.EffectTable.isGlobal

def EffectTable.isGlobal (t : EffectTable) (x : DeclId) : Bool

Whether x is a global variable of the table t.

cfamily.EffectTable.isIndirect

def EffectTable.isIndirect (t : EffectTable) (x : DeclId) : Bool

Whether x is a variable of the table t whose elements are elsewhere (a pointer, a reference, an array parameter).

cfamily.EffectTable.isReferring

def EffectTable.isReferring (t : EffectTable) (x : DeclId) : Bool

Whether x is a variable of the table t that is itself elsewhere (a reference).

cfamily.EffectTable.isArray

def EffectTable.isArray (t : EffectTable) (x : DeclId) : Bool

Whether x is a variable of the table t declared as an array of a written length, its elements its own storage (and not, under the same name, a pointer or a reference).

cfamily.Expr.rootVariable

def Expr.rootVariable (e : Expr) : Option DeclId

The variable an lvalue is rooted at (a of a[i], s of s.f), if it is one.

cfamily.Expr.throughPointer

def Expr.throughPointer (t : EffectTable) (e : Expr) : Bool

Whether the lvalue e is reached through a pointer (or is a variable that refers elsewhere), by the variables of t. A pointer variable itself is not: assigning it (x = x->left) writes the variable, what it points to is elsewhere.

cfamily.Effects.reading

def Effects.reading (t : EffectTable) (x : DeclId) : Effects

Reading the variable x: a global is recorded, a local is not.

cfamily.Effects.writingAt

def Effects.writingAt (ext : EffectExtension) (t : EffectTable) (e : Expr) : Effects

Writing where an lvalue is: the receiver, memory elsewhere, a global, or a local (nothing).

cfamily.Expr.indexesElsewhere

def Expr.indexesElsewhere (t : EffectTable) (a : Expr) : Bool

Whether the elements of a, the subscripted expression, are elsewhere (by the variables of t): a pointer, a reference, an array parameter, or an array reached through one.

cfamily.Expr.indexed

def Expr.indexed (t : EffectTable) (a : Expr) : Effects

Reading memory elsewhere when a, subscripted, is indexed through a pointer (by the variables of t).

cfamily.Expr.callee

def Expr.callee (ext : EffectExtension) (t : EffectTable) (f : String) (args : List Expr) : Effects

The effects of calling f with the arguments args (by ext, the dialect, and t, the table): its summary if the program defines it, else the library’s.

cfamily.Expr.libraryCallEffects

def Expr.libraryCallEffects (ext : EffectExtension) (t : EffectTable) (f : String) (args : List Expr) : Effects

The effects of calling the library function f with the arguments args (by ext, the dialect, and t, the table): the library’s, and where it writes elsewhere only through some of its arguments (EffectExtension.writesThroughArguments, snprintf’s buffer), those writes where the arguments point (Expr.writtenThrough): into a local array the caller cannot see, a global’s, or elsewhere.

cfamily.Expr.ownStorage

def Expr.ownStorage (t : EffectTable) (e : Expr) : Option DeclId

The variable whose own storage the lvalue e certainly is in (by the variables of t): a variable that is not a reference, a member of one (.), an element of an array variable; none for what is reached through a pointer, a reference or the object a member function is called on (whose members’ types the summaries do not know).

cfamily.Effects.writingVariable

def Effects.writingVariable (t : EffectTable) (x : DeclId) : Effects

Writing the storage of the variable x (by the variables of t): a global’s is recorded, a local’s is not.

cfamily.Expr.writtenThrough

def Expr.writtenThrough (t : EffectTable) (a : Option Expr) : Effects

What a library function writes through the argument a, a pointer (by the variables of t): into the variable it certainly points into (an array variable, the address of a variable or its part), nothing for a null pointer constant, else memory elsewhere (also for a missing argument).

cfamily.Expr.extension

def Expr.extension (ext : EffectExtension) (t : EffectTable) (e : Expr) (children : List ChildEffects) : Effects

A dialect’s expression: the dialect’s effects, or (if it does not know it) its children’s.

cfamily.Expr.scanTarget

def Expr.scanTarget (ext : EffectExtension) (t : EffectTable) (e : Expr) : Effects

What scanf writes through a target: the lvalue of &lvalue, else memory elsewhere.

cfamily.Expr.effectsOfSome

def Expr.effectsOfSome (ext : EffectExtension) (t : EffectTable) (e : Option Expr) : Effects

The effects of an optional expression.

cfamily.Stmt.childOfSome

def Stmt.childOfSome (ext : EffectExtension) (t : EffectTable) (e : Option Expr) : List ChildEffects

An optional expression as a child (none is no children).

cfamily.Stmt.extension

def Stmt.extension (ext : EffectExtension) (t : EffectTable) (s : Stmt) (exprs : List ChildEffects) (stmts : List Effects) : Effects

A dialect’s statement: the dialect’s effects, or (if it does not know it) its children’s.

cfamily.TypeSyntax.indirect

def TypeSyntax.indirect (ext : EffectExtension) (c : TypeSyntax) : Bool

Whether variables of the written type c have their elements elsewhere: pointers, unsized arrays, a type the summaries cannot see is not a pointer (deduced, auto; a typedef’s name; a member type, C::iterator; a template’s parameter), and what ext, the dialect, says (a reference).

cfamily.TypeSyntax.indirectParameter

def TypeSyntax.indirectParameter (ext : EffectExtension) (c : TypeSyntax) : Bool

Whether a parameter of the written type c has its elements elsewhere (ext knows the dialect’s types): as any variable, and an array (adjusted to a pointer).

cfamily.TypeSyntax.itselfElsewhere

def TypeSyntax.itselfElsewhere (ext : EffectExtension) (c : TypeSyntax) : Bool

Whether a variable of the written type c is itself memory elsewhere (a reference: ext, the dialect, says).

cfamily.Stmt.indirectExtension

def Stmt.indirectExtension (ext : EffectExtension) (s : Stmt) (inner : List (List DeclId)) : List DeclId

A dialect’s statement: what the dialect says it declares, or (if it does not know it) what its statements do.

cfamily.Param.indirect

def Param.indirect (which : TypeSyntax -> Bool) (p : Param) : List DeclId

A parameter’s declaration, if its type is one of which.

cfamily.FunctionDefinition.indirect

def FunctionDefinition.indirect (ext : EffectExtension) (f : FunctionDefinition) : List DeclId

The parameters and variables of a function whose elements are elsewhere: pointers, references, and array parameters (a parameter of array type is a pointer, C11 6.7.6.3p7, [dcl.fct]p5).

cfamily.FunctionDefinition.itselfElsewhere

def FunctionDefinition.itselfElsewhere (ext : EffectExtension) (f : FunctionDefinition) : List DeclId

The parameters and variables of a function that are themselves elsewhere: references (a pointer is a variable of its own; what it points to is elsewhere).

cfamily.TypeSyntax.isArrayWithLength

def TypeSyntax.isArrayWithLength (c : TypeSyntax) : Bool

Whether the written type c is an array of a written length (its elements are the variable’s own storage; an array without a length may be a pointer parameter).

cfamily.FunctionDefinition.arrays

def FunctionDefinition.arrays (ext : EffectExtension) (f : FunctionDefinition) : List DeclId

The variables a function’s body declares as arrays of a written length (not its parameters: an array parameter is a pointer).

cfamily.FunctionDefinition.name

def FunctionDefinition.name (f : FunctionDefinition) : String

The name of a function.

cfamily.EffectTable.byShort

def EffectTable.byShort (t : EffectTable) (f : String) : Effects

What a call by the short name f alone may do (a member function’s, by its name), by the table t: the summaries of the functions of that short name joined in order, the first innermost ((s1 joined with s2) joined with …); none for a name the program does not define.

cfamily.EffectTable.withSummaries

def EffectTable.withSummaries (t : EffectTable) (summaries : List Effects) : EffectTable

The table t with the summaries of a round, in the functions’ order.

cfamily.FunctionDefinition.callees

def FunctionDefinition.callees (pointed : Option (List String)) (f : FunctionDefinition) : List String

The names a function’s body calls by (a call’s name, a member function call’s): its summary can change only when one of theirs did. A call through a pointer calls those the program takes the address of, or anything (*).

cfamily.SummaryWork

record SummaryWork

A function to summarize, whether it may call anything (through a pointer to any function), and the positions of the functions whose summaries its own is made of (those its calls name).

cfamily.EffectTable.work

def EffectTable.work (t : EffectTable) (f : FunctionDefinition) : SummaryWork

What summarizing the function f reads of the table t: the positions of the functions its calls name, found once for the table rather than by name in each round.

cfamily.EffectTable.changedPositions

def EffectTable.changedPositions (before : List Effects) (after : List Effects) : List Nat

The positions whose summaries differ between two rounds, before and after.

cfamily.EffectTable.affected

def EffectTable.affected (changed : SearchTree Nat Unit) (everything : Bool) (w : SummaryWork) : Bool

Whether the summary of the function of w may change: in the first round (everything), or when it may call anything or calls a function whose summary changed in the round before (its position is in changed).

cfamily.SummaryWork.effects

def SummaryWork.effects (ext : EffectExtension) (t : EffectTable) (w : SummaryWork) : Effects

The summary of the function of w from t, the table of the previous round (ext knows the dialect): the effects of its body.

cfamily.EffectTable.fixpointFrom

def EffectTable.fixpointFrom (ext : EffectExtension) (fuel : Nat) (work : List SummaryWork) (t : EffectTable) (changed : SearchTree Nat Unit) (everything : Bool) : EffectTable

Rounds from the table t until no summary changes, at most fuel of them (ext knows the dialect): each round recomputes only the summaries of the work whose callees changed in the round before (all of them in the first, when everything).

cfamily.EffectTable.fixpoint

def EffectTable.fixpoint (ext : EffectExtension) (fuel : Nat) (fs : List FunctionDefinition) (t : EffectTable) : EffectTable

Rounds from the table t until no summary of the functions fs changes, at most fuel of them (ext knows the dialect).

cfamily.EffectTable.indirectGlobal

def EffectTable.indirectGlobal (which : TypeSyntax -> Bool) (g : DeclId * TypeSyntax) : List DeclId

A global’s declaration, if its type is one of which.

cfamily.KeyMention

record KeyMention

A key’s mention of the function at a position: as its name, as its short name, or both.

cfamily.EffectTable.mentions

def EffectTable.mentions (keys : List (String * String)) : List KeyMention

The mentions of the functions’ keys (each function’s, in order).

cfamily.FunctionsNamed.ofMention

def FunctionsNamed.ofMention (m : KeyMention) : FunctionsNamed

The functions of a key mentioned once, by m.

cfamily.FunctionsNamed.withMention

def FunctionsNamed.withMention (m : KeyMention) (f : FunctionsNamed) : FunctionsNamed

The functions f of a key with one more mention m, of an earlier position.

cfamily.EffectTable.grouped

def EffectTable.grouped (sorted : List KeyMention) : List (String * FunctionsNamed)

The mentions, sorted by key (stably: a key’s in the order of their positions), each run of one key made one entry.

cfamily.EffectTable.functionsByKey

def EffectTable.functionsByKey (keys : List (String * String)) : SearchTree String FunctionsNamed

The functions of each of the keys (each function’s name and short name), by position.

cfamily.EffectTable.pointedAmong

def EffectTable.pointedAmong (functions : SearchTree String FunctionsNamed) (addressed : Option (List String)) : Option (List String)

The functions a call through a pointer may call, of the addressed ones (none: may call anything): all of them when the program defines each (one of the functions, by its name or short name).

cfamily.EffectTable.of

def EffectTable.of (ext : EffectExtension) (globals : List (DeclId * TypeSyntax)) (fs : List FunctionDefinition) (addressed : Option (List String)) : EffectTable

The effect table of a program: its globals (and their written types), its functions (with the bodies of function templates, in a dialect that has them), and the functions whose address it takes (none: unknown); at most one round per function plus one.