librarycode

cfamily.LibraryCode.node

def LibraryCode.node (n : String) : NodeId

A node of the library’s code.

cfamily.LibraryCode.variable

def LibraryCode.variable (n : String) (x : String) : Expr

A variable of the library’s code.

cfamily.LibraryCode.number

def LibraryCode.number (n : String) (v : Int) : Expr

An integer constant of the library’s code.

cfamily.LibraryCode.call

def LibraryCode.call (n : String) (f : String) (args : List Expr) : Expr

A call in the library’s code.

cfamily.LibraryCode.declare

def LibraryCode.declare (n : String) (x : String) (t : TypeSyntax) (e : Expr) : Stmt

A declaration with an initializer in the library’s code.

cfamily.LibraryCode.parameter

def LibraryCode.parameter (x : String) (t : TypeSyntax) : Param

A parameter of the library’s code.

cfamily.LibraryCode.comparator

def LibraryCode.comparator : TypeSyntax

The comparator’s type: int (*)(const void *, const void *).

cfamily.LibraryCode.checkArray

def LibraryCode.checkArray (n : String) (k : String) (base : String * String) (count : String * String) (size : String * String) : Stmt

The checks of qsort’s and bsearch’s array (C11 7.22.5p1), at node n with the base, count and size variables.

cfamily.LibraryCode.hold

def LibraryCode.hold (n : String) (base : String) (count : String) (size : String) : Stmt

Holding an array while the comparator runs (__qhold, C11 7.22.5p3: a write that alters it stops the run).

cfamily.LibraryCode.release

def LibraryCode.release (n : String) : Stmt

Letting go of the held array (__qrelease).

cfamily.LibraryCode.qsortOutOfOrder

def LibraryCode.qsortOutOfOrder : Expr

qsort’s test whether the j-th element is below the one before it.

cfamily.LibraryCode.qsortInner

def LibraryCode.qsortInner : Stmt

qsort’s inner loop: while j > 0 and the j-th is out of order, swap it with the one before.

cfamily.LibraryCode.qsortOuter

def LibraryCode.qsortOuter : Stmt

qsort’s outer loop over i from 1.

cfamily.LibraryCode.element

def LibraryCode.element (n : String) (base : String) (index : Expr) : Expr

The element of an array at an index.

cfamily.LibraryCode.compare

def LibraryCode.compare (n : String) (comparator : String) (a : Expr) (b : Expr) : Expr

A call of a comparator variable.

cfamily.LibraryCode.step

def LibraryCode.step (n : String) (op : BinaryOp) (x : String) : Expr

An index plus or minus 1.

cfamily.LibraryCode.isQuiet

def LibraryCode.isQuiet (n : String) (comparator : String) (quiet : List String) : Expr

Whether a comparator variable is one of the quiet functions: cmp == f || ..., 0 for none.

cfamily.LibraryCode.compareElements

def LibraryCode.compareElements (n : String) (comparator : String) (base : String) (a : Expr) (b : Expr) : Expr

A comparison of the elements of an array at two indices.

cfamily.LibraryCode.isZero

def LibraryCode.isZero (n : String) (e : Expr) : Expr

Whether an expression is 0.

cfamily.LibraryCode.upTo

def LibraryCode.upTo (n : String) (x : String) (start : Expr) (bound : String) (body : Stmt) : Stmt

for (unsigned long x = start; x < bound; x++) body.

cfamily.LibraryCode.when

def LibraryCode.when (n : String) (c : Expr) (body : Stmt) : Stmt

if (c) body.

cfamily.LibraryCode.qsortPair

def LibraryCode.qsortPair : Stmt

qsort’s check of the i-th and j-th elements of the sorted array (i before j, __qorder): the two comparisons, and whether every neighbour from the i-th to the j-th compares equal (qrun carries it along the row: for neighbours, whether they compare equal; further on, whether it held up to the one before the j-th and the one before equals the j-th). Three calls of the comparator for each pair.

cfamily.LibraryCode.qsortOrderCheck

def LibraryCode.qsortOrderCheck (quiet : List String) : Stmt

qsort’s check of the sorted array (C11 7.22.5p4), every pair once, when the comparator is quiet.

cfamily.LibraryCode.qsort

def LibraryCode.qsort (quiet : List String) : FunctionDefinition

qsort: an insertion sort through the comparator, after the checks of the array (C11 7.22.5.2), then the check of its results when the comparator is quiet; the array is held while it runs.

cfamily.LibraryCode.bsearchMiddle

def LibraryCode.bsearchMiddle : Stmt

bsearch’s middle index: lo + (hi - lo) / 2.

cfamily.LibraryCode.bsearchCompare

def LibraryCode.bsearchCompare : Stmt

bsearch’s comparison of the key with the middle element.

cfamily.LibraryCode.bsearchFound

def LibraryCode.bsearchFound : Stmt

bsearch’s return of the middle element when it equals the key, letting go of the held array first.

cfamily.LibraryCode.bsearchNarrow

def LibraryCode.bsearchNarrow : Stmt

bsearch’s halving: the lower half when the key is below the middle, else the upper.

cfamily.LibraryCode.bsearchSorted

def LibraryCode.bsearchSorted (quiet : List String) : Stmt

bsearch’s check that the array is sorted by the key (C11 7.22.5.1p2), each element with the one before, when the comparator is quiet (__qsorted).

cfamily.LibraryCode.bsearch

def LibraryCode.bsearch (quiet : List String) : FunctionDefinition

bsearch: a binary search through the comparator, after the checks of the array (C11 7.22.5.1) and, when the comparator is quiet, that the array is sorted; the array is held while it runs.

cfamily.LibraryCode.functions

def LibraryCode.functions (quiet : List String) : List FunctionDefinition

The library’s functions written in C, with the quiet comparators.

cfamily.TypeSyntax.isInt

def TypeSyntax.isInt (t : TypeSyntax) : Bool

Whether a type is int.

cfamily.TypeSyntax.isConstVoidPointer

def TypeSyntax.isConstVoidPointer (t : TypeSyntax) : Bool

Whether a type is const void *.

cfamily.Param.isConstVoidPointer

def Param.isConstVoidPointer (p : Param) : Bool

Whether a parameter is const void *.

cfamily.FunctionDefinition.isComparator

def FunctionDefinition.isComparator (f : FunctionDefinition) : Bool

Whether a function has the comparator’s type, int (const void *, const void *).

cfamily.Effects.isQuiet

def Effects.isQuiet (e : Effects) : Bool

Whether calling a function changes nothing a run shows: no input or output, no writes but to its own locals.

cfamily.LibraryCode.quietComparators

def LibraryCode.quietComparators (effects : EffectTable) (items : List Item) : List String

The program’s functions of the comparator’s type whose calls change nothing a run shows.

cfamily.FunctionDefinition.body

def FunctionDefinition.body (f : FunctionDefinition) : Stmt

A function’s body.

cfamily.Expr.names

def Expr.names (f : String) (e : Expr) : Bool

Whether an expression calls or names a function.

cfamily.Item.functions

def Item.functions (items : List Item) : List FunctionDefinition

The functions of the items, in order.

cfamily.Item.uses

def Item.uses (items : List Item) (f : String) : Bool

Whether the items’ functions call or name a function.

cfamily.LibraryCode.isNeeded

def LibraryCode.isNeeded (items : List Item) (d : FunctionDefinition) : Bool

Whether the program needs one of the library’s C functions: it uses the function and does not define it.

cfamily.LibraryCode.anyNeeded

def LibraryCode.anyNeeded (items : List Item) : Bool

Whether the program needs any of the library’s C functions.

cfamily.Item.withLibraryCode

def Item.withLibraryCode (quiet : List String) (items : List Item) : List Item

The items with the library’s C functions the program uses and does not define, checking the comparators named quiet.