execution

cfamily.Leaving

data Leaving

How the current statements are left: done, by return (with the value), break, continue, or goto to a label in a block.

cfamily.Frame

data Frame (L : Constructs)

What to do after the current statements.

cfamily.Outcome

data Outcome (L : Constructs)

How a run ended: with an exit code, stopped (undefined behavior, a dialect’s reason), out of fuel inside an expression, at a statement that did not check (the type query’s collect mode), or before it began at a construct not supported yet (not an error in the program).

cfamily.Configuration

data Configuration (L : Constructs)

A configuration: running statements, leaving, or finished; or a trial run first, then going on from how it ended (a dialect compares what a choice the implementation makes changes, as whether unwinding the stack before a termination changes the output); or a trial of at most steps moves, then going on from how it ended with the moves left, or with over if it did not end (the other order of calls, cfamily.orders).

cfamily.RunExtension

record RunExtension (L : Constructs)

How a dialect runs what the core does not know. Each defaults to nothing.

• statement: its own statements (node, tag, types, expressions, statements), with the core’s evaluator;
• frame: how leaving passes one of its frames;
• ending: what to run before an object of a declaration ends (C++’s destructor), none when nothing; it is given the program’s functions (whether the destructor is one) and whether the object ends because an exception leaves its scope (C++’s cleanup of a half-constructed object’s members runs only then);
• uncaught: how a run ends when an exception leaves main uncaught (a dialect with exceptions raises them by leaving with raising; the scopes it leaves end as for any leaving, the calls pass it to their callers);
• sameState: whether its part of two states is the same (the two orders of calls are compared, cfamily.orders; a dialect with no state of its own has nothing to compare).

cfamily.RunExtension.empty

def RunExtension.empty {L : Constructs} : RunExtension L

The extension of a dialect without statements or frames of its own.

cfamily.RunDialect

record RunDialect (L : Constructs)

What running needs: the dialect’s evaluation, library and extension, the program’s functions and the one a run starts at (main, or a board core’s own).

cfamily.RunDialect.evaluator

def RunDialect.evaluator {L : Constructs} (d : RunDialect L) : Evaluator L

The core’s evaluator for a dialect.

cfamily.State.addNotes

def State.addNotes {L : Constructs} (s : State L) (notes : List (Stopped L)) : State L

The state with notes added.

cfamily.Configuration.after

def Configuration.after {L : Constructs} {A : Type} (s : State L) (r : Evaluated L A) (next : State L -> A -> Configuration L) : Configuration L

Going on with an evaluated value (its notes added to the state), or finishing at a stop.

cfamily.Configuration.stop

def Configuration.stop {L : Constructs} (n : NodeId) (b : Behavior) (s : State L) : Configuration L

A stop at a node.

cfamily.Frame.push

def Frame.push {L : Constructs} (rest : List (TypedStmt L)) (k : List (Frame L)) : List (Frame L)

The frames with the rest of a sequence pushed (nothing when it is empty).

cfamily.Frame.either

def Frame.either {A : Type} (a : Option A) (b : Option A) : Option A

The first of two options that is some.

cfamily.TypedStmt.hasLabel

def TypedStmt.hasLabel {L : Constructs} (name : String) (x : TypedStmt L) : Bool

Whether a statement carries a label.

cfamily.TypedStmt.splitAt

def TypedStmt.splitAt {L : Constructs} (name : String) (xs : List (TypedStmt L)) : Option (List (TypedStmt L) * List (TypedStmt L))

The statements before a label and from it on.

cfamily.State.inInnermost

def State.inInnermost {L : Constructs} (s : State L) (x : DeclId) : Bool

Whether a declaration is in the innermost scope.

cfamily.State.skipped

def State.skipped {L : Constructs} (m : Making L) (s : State L) (xs : List (TypedStmt L)) : State L

The declarations a jump forward skips: their objects exist from the block’s start, uninitialized (C11 6.2.4p6).

cfamily.CheckedFunction.named

def CheckedFunction.named {L : Constructs} (functions : List (CheckedFunction L)) (f : String) : Option (CheckedFunction L)

The function with a name.

cfamily.CheckedFunction.bodyOf

def CheckedFunction.bodyOf {L : Constructs} (functions : List (CheckedFunction L)) (f : String) : Option (TypedStmt L)

The body of the function with a name.

cfamily.Frame.functionBody

def Frame.functionBody {L : Constructs} (entry : String) (functions : List (CheckedFunction L)) (k : List (Frame L)) : Option (TypedStmt L)

The body of the function the frames are in (the innermost call; none is the entry, of the name given).

cfamily.State.local

def State.local (scopes : List Scope) : List Scope

The scopes but the last (the global one).

cfamily.State.global

def State.global (scopes : List Scope) : List Scope

The last scope (the global one).

cfamily.State.withGlobal

def State.withGlobal (scopes : List Scope) (global : List Scope) : List Scope

Scopes with the outermost (global) one replaced.

cfamily.State.backTo

def State.backTo {L : Constructs} (s : State L) (saved : List Scope) (target : Option (DeclId * Ty L)) (v : Option Value) : State L

Back in the caller: the callee’s scopes released, the caller’s restored (and its calls), the result (if any) in the target, which is an object from then on.

cfamily.State.declareTarget

def State.declareTarget {L : Constructs} (m : Making L) (s : State L) (target : Option (DeclId * Ty L)) : State L

A temporary for a result declared in the current scope (uninitialized).

cfamily.State.bindParameters

def State.bindParameters {L : Constructs} (s : State L) (ps : List (DeclId * Ty L)) (vs : List Value) : State L

The parameters declared with the arguments’ values.

cfamily.State.reserveTarget

def State.reserveTarget {L : Constructs} (m : Making L) (s : State L) (target : Option (DeclId * Ty L)) : State L

A temporary for a function’s result reserved in the current scope: no object until the call returns (one that leaves by an exception leaves none to end, [except.ctor]p1).

cfamily.Configuration.call

def Configuration.call {L : Constructs} (d : RunDialect L) (n : NodeId) (target : Option (DeclId * Ty L)) (f : String) (vs : List Value) (k : List (Frame L)) (s : State L) : Configuration L

A call: the target reserved in the caller’s scope, the callee’s body in a scope of its own over the global one; the call’s node is the innermost of the calls the run is in.

cfamily.Leaving.isRaising

def Leaving.isRaising (u : Leaving) : Bool

Whether leaving is an exception on its way out.

cfamily.Ending

record Ending (L : Constructs)

What the dialect runs before an object ends: the object’s declaration and block, and the statements.

cfamily.State.firstEnding

def State.firstEnding {L : Constructs} (d : RunDialect L) (s : State L) (unwinding : Bool) (scope : Scope) : Option (Ending L)

The most recent object of a scope the dialect has something to run for before it ends (an object only reserved, not yet constructed, has nothing).

cfamily.State.toEnd

def State.toEnd {L : Constructs} (s : State L) (x : DeclId) (b : Nat) : State L

An object about to end, moved to a scope of its own (State.isolate) and marked as being destroyed: const does not apply while its ending runs (C++ [class.dtor]), as while it is constructed.

cfamily.Configuration.arrive

def Configuration.arrive {L : Constructs} (d : RunDialect L) (block : NodeId) (label : String) (k : List (Frame L)) (s : State L) : Configuration L

A goto arriving at its label’s block: the objects declared from the label on that exist end first, the latest first (a jump back past a declaration ends its object, C++ [stmt.dcl]p2; each ending runs as in leaving a scope, then the jump arrives again); then from the label on, with the declarations it skipped.

cfamily.Configuration.leaveScope

def Configuration.leaveScope {L : Constructs} (d : RunDialect L) (u : Leaving) (frame : Frame L) (k : List (Frame L)) (s : State L) (next : State L -> Configuration L) : Configuration L

Leaving a scope: an object’s cleanup first (the object moves to a scope of its own, the cleanup runs, that scope ends with the object’s block, then leaving resumes at the same frame), else the scope ends.

cfamily.Leaving.exitCode

def Leaving.exitCode (u : Leaving) : Int

The exit code of a program’s end: main’s result, or 0 when main’s body ends (C11 5.1.2.2.3).

cfamily.Leaving.result

def Leaving.result (u : Leaving) : Option Value

The value a call returns: the return’s, none when the body ends (using it reads an indeterminate value).

cfamily.Frame.nextRound

def Frame.nextRound {L : Constructs} (n : NodeId) (before : List (TypedStmt L)) (c : TypedExpr L) (body : TypedStmt L) (after : List (TypedStmt L)) : List (TypedStmt L)

A loop’s next round: the statements each round ends with, then the check.

cfamily.Outcome.normalState

def Outcome.normalState {L : Constructs} (o : Outcome L) : Option (State L)

The state the trial outcome o ended in when it ended normally (or by an exit: one inside a call leaves the callee’s scopes, which the comparison sees).

cfamily.Frame.callerScopes

def Frame.callerScopes {L : Constructs} (k : List (Frame L)) : List Scope

The callers’ own scopes, saved in the call frames of k (their blocks are older than any comparison inside the calls).

cfamily.State.freshTemporaries

def State.freshTemporaries {L : Constructs} (base : Nat) (s : State L) : List DeclId

The temporaries of the innermost scope of s bound to blocks made from base on, the most recent first.

cfamily.State.endsSomething

def State.endsSomething {L : Constructs} (d : RunDialect L) (s : State L) (ys : List DeclId) : Bool

Whether the dialect d runs something, in the state s, before the object of one of the declarations ys ends (a destructor; an object only reserved has nothing).

cfamily.State.withBudget

def State.withBudget {L : Constructs} (s : State L) (budget : Nat) : State L

The state s with the budget for comparing orders replaced by budget.

cfamily.State.asTrial

def State.asTrial {L : Constructs} (s : State L) : State L

The state s as a trial runs from it: the points where the order of calls matters run in the first order.

cfamily.State.withOrdersUncompared

def State.withOrdersUncompared {L : Constructs} (s : State L) (n : NodeId) : State L

The state s with the note that the orders of the calls at n were not compared, past the budget; no budget is left for others.

cfamily.OrderDifference.between

def OrderDifference.between {L : Constructs} (written : Nat) (a : State L) (b : State L) : OrderDifference

How the states a and b of two orders that ended normally differ: in their output (what each wrote after the first written bytes), or else in the state.

cfamily.Configuration.afterOrders

def Configuration.afterOrders {L : Constructs} (n : NodeId) (written : Nat) (k : List (Frame L)) (s : State L) (ours : State L) (theirs : State L) (r : Sameness) (alikeNext : Matching -> Configuration L) : Configuration L

Going on, with the frames k, after the states ours (the first order’s) and theirs of the orders at the node n compared as r: as alikeNext says when alike, else from the run’s state s with the divergence noted (the outputs after the first written bytes), or, past the budget, that the orders were not compared (no budget is left for others).

cfamily.Configuration.endingsCompared

def Configuration.endingsCompared {L : Constructs} (d : RunDialect L) (n : NodeId) (base : Nat) (written : Nat) (callers : List Scope) (other : State L) (k : List (Frame L)) (s : State L) : Configuration L

The temporaries of the calls at the node n end in the reverse order of their making, which differs between the two orders when their scopes bind them in other orders: the temporaries made from base on of other (the other order’s state) and of s ended (as trials, by the dialect d) and the states compared again (the callers’ scopes reached as well), then the run goes on with the frames k; a difference in the output is shown after the first written bytes.

cfamily.Configuration.ordersCompared

def Configuration.ordersCompared {L : Constructs} (d : RunDialect L) (n : NodeId) (base : Nat) (written : Nat) (other : State L) (k : List (Frame L)) (s : State L) : Configuration L

The first order’s state s at the node n compared with the other’s, other (State.sameAs, on the blocks made from base on; the callers’ scopes in the frames k are reached as well): alike goes on (the temporaries’ endings compared too, by the dialect d, when the orders bound them in other orders and something runs before one ends), else the divergence is noted (the outputs after the first written bytes).

cfamily.Frame.leave

def Frame.leave {L : Constructs} (d : RunDialect L) (u : Leaving) (frame : Frame L) (k : List (Frame L)) (s : State L) : Configuration L

Leaving passes one frame.

cfamily.Address.isPrefix

def Address.isPrefix (p : List Nat) (q : List Nat) : Bool

Whether one path is a prefix of another.

cfamily.Held.coversPath

def Held.coversPath (h : Held) (q : List Nat) : Bool

Whether a path is in what a held array covers: it contains the array, or it is in one of the held elements (in the object, for a held whole object); an empty range covers nothing.

cfamily.Held.covers

def Held.covers (h : Held) (a : Address) : Bool

Whether a held array covers an address.

cfamily.Value.sameScalar

def Value.sameScalar (a : Value) (b : Value) : Option Bool

Whether two scalar values are the same, when the model can tell: integers, pointers and functions.

cfamily.State.altersHeld

def State.altersHeld {L : Constructs} (s : State L) (a : Address) (v : Value) : Bool

Whether storing a value at an address alters an array qsort or bsearch holds (C11 7.22.5p3): the address is in it and the value there is a different one. Storing the same value alters nothing; a value the model cannot compare (a floating value, a whole struct, an indeterminate one) is let through, so this misses some writes but never rejects one that does not alter the array.

cfamily.TypedExpr.copiedFrom

def TypedExpr.copiedFrom {L : Constructs} (d : EvaluationDialect L) (s : State L) (e : TypedExpr L) : Evaluated L (Option Address)

Where a whole object being assigned is read from: the lvalue of a struct or union assignment’s right side (read whole, or a member or dereference of struct or union type); none for any other value.

cfamily.State.placesIn

def State.placesIn {L : Constructs} (d : EvaluationDialect L) (s : State L) (b : Nat) (p : List Nat) (q : List Nat) : Option (Placed * Placed)

The places of two subobjects of a block, by the layout of the block’s type (none when the type has no shape).

cfamily.Placed.overlapsPartly

def Placed.overlapsPartly (p : Placed) (q : Placed) : Bool

Whether two places share bits without being the same bits.

cfamily.State.overlapsPartly

def State.overlapsPartly {L : Constructs} (d : EvaluationDialect L) (s : State L) (a : Address) (source : Option Address) : Bool

Whether the object written and the object its value is read from overlap other than exactly (C11 6.5.16.1p3, C++17 [expr.ass]p8): in the same block, their bits by the block’s layout shared without being the same. Exact overlap with an incompatible type cannot be written (the assignment’s sides have compatible types); addresses of bytes, and blocks whose type has no shape, are let through.

cfamily.Address.overlap

def Address.overlap (a : Address) (b : Address) : Bool

Whether two addresses overlap: the same block with one path a prefix of the other (a struct and its member); a byte of an object overlaps the object and what is in it, another byte only when it is the same one.

cfamily.TypedClause.startingAt

def TypedClause.startingAt {L : Constructs} (v : Int) (cs : List (TypedClause L)) : Option (List (TypedStmt L))

The statements of a switch from the clause with the value (falling through the rest), or from default.

cfamily.Ty.cellLimit

def Ty.cellLimit : Nat

The most cells (scalars) an object the model makes may have: 2^20. A larger one would make the host run out of memory before the run ends (the elements are kept one by one).

cfamily.Object.repeated

def Object.repeated (count : Int) (o : Object) : Object

An array object of count copies of an element.

cfamily.Configuration.withinCells

def Configuration.withinCells {L : Constructs} (n : NodeId) (cells : Nat) (s : State L) (go : Unit -> Configuration L) : Configuration L

The run going on (go, called only after the check: making the object is what the limit prevents) unless an object of a count of cells is more than the model keeps.

cfamily.State.allocateArray

def State.allocateArray {L : Constructs} (d : RunDialect L) (s : State L) (x : DeclId) (element : Ty L) (elementSize : Nat) (size : Int) (zero : Bool) : State L

malloc and calloc: size bytes are size / elementSize whole elements (a remainder is never used), in a new block; the pointer to its first element goes into x.

cfamily.Memory.mallocStart

def Memory.mallocStart {L : Constructs} (m : Memory L) (p : Pointer) : Option Nat

The block a pointer starts if it is the start of a block malloc made that is alive (what free and realloc take, C11 7.22.3.3p2, 7.22.3.5p3).

cfamily.Configuration.free

def Configuration.free {L : Constructs} (n : NodeId) (p : Pointer) (k : List (Frame L)) (s : State L) : Configuration L

free: NULL does nothing; else it must be the start of a block malloc made that is alive (C11 7.22.3.3p2).

cfamily.Memory.elementsOf

def Memory.elementsOf {L : Constructs} (m : Memory L) (b : Nat) : List Object

A block’s elements (none for a block that is not an array).

cfamily.State.reallocated

def State.reallocated {L : Constructs} (d : RunDialect L) (s : State L) (x : DeclId) (element : Ty L) (elementSize : Nat) (size : Int) (b : Nat) : State L

realloc’s new block for a pointer into x: size bytes of element, the first objects moved from block b (the rest indeterminate), b released (C11 7.22.3.5p2).

cfamily.Configuration.reallocate

def Configuration.reallocate {L : Constructs} (d : RunDialect L) (n : NodeId) (x : DeclId) (element : Ty L) (elementSize : Nat) (p : Pointer) (size : Int) (k : List (Frame L)) (s : State L) : Configuration L

realloc: NULL is malloc; else the pointer must be the start of a block malloc made that is alive (C11 7.22.3.5p3); size zero is implementation-defined (C11 7.22.3p1); else the block moves to one of the new size.

cfamily.Configuration.returned

def Configuration.returned {L : Constructs} (target : Option (DeclId * Ty L)) (k : List (Frame L)) (r : Returned L) : Configuration L

The result of a library call delivered to its target.

cfamily.Configuration.stored

def Configuration.stored {L : Constructs} (k : List (Frame L)) (s : State L) (y : DeclId) (v : Value) : Configuration L

Going on with a value assigned to a declaration’s object.

cfamily.Configuration.returnWith

def Configuration.returnWith {L : Constructs} (k : List (Frame L)) (s : State L) (v : Value) : Configuration L

Leaving by returning a value.

cfamily.Configuration.declaration

def Configuration.declaration {L : Constructs} (d : RunDialect L) (x : TypedStmt L) (k : List (Frame L)) (s : State L) : Configuration L

Declarations, assignments and the objects’ lifetimes.

cfamily.Configuration.control

def Configuration.control {L : Constructs} (d : RunDialect L) (x : TypedStmt L) (k : List (Frame L)) (s : State L) : Configuration L

Control: branches, loops, blocks, switch, jumps.

cfamily.State.divergedAt

def State.divergedAt {L : Constructs} (s : State L) (n : NodeId) : Bool

Whether a divergence is noted in the state s at the node n already.

cfamily.Configuration.bothOrders

def Configuration.bothOrders {L : Constructs} (n : NodeId) (first : List (TypedStmt L)) (second : List (TypedStmt L)) (k : List (Frame L)) (s : State L) : Configuration L

Calls in an unspecified order whose effects could conflict (bothOrders at the node n): the second order first, as a trial from the state s (within the budget; the state is persistent, so it is simply kept), then the first order here, with the frames k, compared with the trial when it ends (comparedOrders). In a trial, at a point whose comparison is under way (a recursive call meets it again) and where a divergence is noted already, only the first order runs. Past the budget, that the orders were not compared is noted, and no budget is left for others.

cfamily.Configuration.effect

def Configuration.effect {L : Constructs} (d : RunDialect L) (x : TypedStmt L) (k : List (Frame L)) (s : State L) : Configuration L

Calls, the library, and the checks the checker placed.

cfamily.Configuration.step

def Configuration.step {L : Constructs} (d : RunDialect L) (x : Configuration L) : Configuration L

One move.

cfamily.CheckedFunction.entryBody

def CheckedFunction.entryBody {L : Constructs} (entry : String) (functions : List (CheckedFunction L)) (given : List String) : List (TypedStmt L)

The entry’s body (of the name given); with parameters (main’s argc and argv), inside a scope (no node: the debugger does not stop at it) that first gets them from the arguments.

cfamily.Configuration.start

def Configuration.start {L : Constructs} (d : RunDialect L) (globals : List (TypedStmt L)) (given : List String) (s : State L) : Configuration L

The start of a run on the program’s arguments: one block with the globals initialized in order (as one statement, so the first move runs them and a step stops next at main’s body), then main’s body; main’s return leaves the block, which ends the globals the last first (C++ [basic.start.term]p1: their destructors after main returns). The block’s scope is the global one (the outermost, which a called function sees): the run starts with no scope.

cfamily.State.argumentString

def State.argumentString {L : Constructs} (d : RunDialect L) (s : State L) (text : String) : State L * Nat

A string as a character array of its own (with the null), and its block.

cfamily.State.argumentStrings

def State.argumentStrings {L : Constructs} (d : RunDialect L) (s : State L) (texts : List String) : State L * List Nat

The strings as arrays of their own, and their blocks in order.

cfamily.State.arguments

def State.arguments {L : Constructs} (d : RunDialect L) (s : State L) (count : DeclId * Ty L) (vector : DeclId * Ty L) (given : List String) : State L

argc and argv declared: each argument a string of its own that the program may change, argv an array of pointers to them ending in NULL (C11 5.1.2.2.1p2).