evaluation

cfamily.Evaluator

record Evaluator (L : Constructs)

The core’s evaluating functions, for a dialect evaluating its own expressions: a value, an address, and values in order; and the target the run is on (a dialect’s statements write characters and indexes of its widths).

cfamily.EvaluationExtension

record EvaluationExtension (L : Constructs)

How a dialect evaluates its own expressions (node, type, tag, types, operands): their values, and the objects of those that are lvalues.

cfamily.EvaluationExtension.empty

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

The extension of a dialect without expressions of its own (nothing reaches it).

cfamily.EvaluationDialect

record EvaluationDialect (L : Constructs)

What evaluating needs of a dialect: the target, the rules, the extension, and how new objects are made.

cfamily.Address.literalCode

def Address.literalCode (text : String) (i : Nat) : Int

The code of the i-th byte of a string literal (past the characters, the terminating null).

cfamily.State.objectAt

def State.objectAt {L : Constructs} (n : NodeId) (s : State L) (b : Nat) (path : List Nat) : Evaluated L Object

The object at an address of an object in a block that is alive.

cfamily.Value.asCharacter

def Value.asCharacter {L : Constructs} (t : Ty L) (v : Value) : Value

A value read through an lvalue of a character type as that type’s: an object of another character type read through it is its byte as the lvalue’s type (C11 6.5p7, [basic.lval]p11). A value written through the same type is already in range.

cfamily.State.noValue

def State.noValue {L : Constructs} (s : State L) (b : Nat) (path : List Nat) : Behavior

Why a scalar at a path in a block has no value: indeterminate (J.2), or in a union written through another member, unspecified bytes (C11 6.2.6.1p7).

cfamily.State.punning

def State.punning {L : Constructs} (rules : Rules) (s : State L) (a : Address) : List String

The choice reading at an address assumes: a union’s member other than the one last written, where the rules make that the implementation’s (C++).

cfamily.Ty.isClass

def Ty.isClass {L : Constructs} (t : Ty L) : Bool

Whether a type is a class type (a struct or union, or one only named).

cfamily.Ty.constAlong

def Ty.constAlong {L : Constructs} (rules : Rules) (fromNew : Bool) (t : Ty L) (path : List Nat) : Bool

Whether the object at a path below a type was defined const: the type or a type on the way down is const. Under a class type it is not in an object new made, when the rules have delete write const objects of class type.

cfamily.State.definedConst

def State.definedConst {L : Constructs} (rules : Rules) (s : State L) (b : Nat) (path : List Nat) : Bool

Whether writing at a path in a block modifies an object defined const (C11 6.7.3p6): not while the object is being made or destroyed (reserved), and never in malloc’s memory, which has no declared type (its block’s type comes from the pointer it was assigned to, const char *t = malloc(4); 6.5p6).

cfamily.State.writesConst

def State.writesConst {L : Constructs} (rules : Rules) (s : State L) (p : Pointer) : Bool

Whether writing through a pointer modifies an object defined const: the object it points into, or the element.

cfamily.Pointer.blockPath

def Pointer.blockPath (p : Pointer) : Option (Nat * List Nat)

The block a pointer into a block is in, and the path to the object it points into.

cfamily.Placed.step

def Placed.step (whole : Bool) (x : Placed) : Nat

The bytes a step of a pointer into the object at a place covers: the whole object’s (a pointer to the whole object), or an array’s element’s.

cfamily.Pointer.offsetFrom

def Pointer.offsetFrom (p : Pointer) (here : Placed) : Int

A pointer’s byte offset in its block, given where the object it points into is: its steps from there, or a byte’s.

cfamily.Block.alignment

def Block.alignment {L : Constructs} (p : Platform) (c : Block L) (root : Placed) : Nat

How a block’s start is aligned: malloc’s for any type (the platform’s largest, C11 7.22.3p1), any other object’s for its own type.

cfamily.State.placement

def State.placement {L : Constructs} (d : EvaluationDialect L) (s : State L) (p : Pointer) : Option (Nat * Int)

Where a pointer is: its block’s alignment and its byte offset in the block; none for a pointer not into a block or into one whose type has no shape.

cfamily.State.misalignment

def State.misalignment {L : Constructs} (d : EvaluationDialect L) (s : State L) (target : Ty L) (p : Pointer) : Option Behavior

Whether a pointer converted to point to a type is aligned for it (C11 6.3.2.3p7): misaligned when its offset is not a multiple of the type’s alignment (or of its block’s, when that is smaller: then the block’s start does not help); when its block is less aligned than the type, aligned or not by where the implementation placed the block.

cfamily.State.reinterpretedAligned

def State.reinterpretedAligned {L : Constructs} (d : EvaluationDialect L) (n : NodeId) (s : State L) (t : Ty L) (v : Value) : Evaluated L Value

State.reinterpreted past the alignment.

cfamily.State.reinterpreted

def State.reinterpreted {L : Constructs} (d : EvaluationDialect L) (n : NodeId) (s : State L) (t : Ty L) (v : Value) : Evaluated L Value

A pointer cast to a pointer type, aligned for the type it points to (C11 6.3.2.3p7): to a character type, a pointer into a block whose elements are not characters points to its object’s bytes; from the bytes to another object type, the pointer they came from; either is unspecified where the type has no C layout or the byte is not where an object of the type begins.

cfamily.Value.integerOf

def Value.integerOf {L : Constructs} (n : NodeId) (t : IntegerType) (v : Value) : Evaluated L Value

A value converted to an integer type: an integer, a truth for bool; a pointer made from an integer gives the integer back, null is 0, any other pointer’s address is the implementation’s (C11 6.3.2.3p6).

cfamily.Value.asPointer

def Value.asPointer (v : Value) : Value

A value converted to a pointer type: an integer is the address it stands for (0 is null), a pointer stays.

cfamily.Ty.accessAgainst

def Ty.accessAgainst {L : Constructs} (o : Ty L) (t : Ty L) : Bool

Whether an object of type o is accessed through an lvalue of type t against the types (C11 6.5p7, C++ [basic.lval]p11): both arithmetic and of different kinds — integers of different ranks (a signed type and its unsigned counterpart are the same kind; an enumeration is its underlying type’s), an integer and a floating type, floating types of different formats. A character type reaches any object’s bytes; pointers, aggregates and a dialect’s own types are not judged here.

cfamily.State.accessAgainst

def State.accessAgainst {L : Constructs} (s : State L) (a : Address) (t : Ty L) : Bool

Whether the object at an address is accessed through an lvalue of a type against its own (Ty.accessAgainst; an address of a literal’s byte or of an object’s bytes is not judged here).

cfamily.State.read

def State.read {L : Constructs} (n : NodeId) (s : State L) (a : Address) : Evaluated L Value

The value read at an address: a byte of a literal, an initialized scalar, or a struct or union whole (C11 6.3.2.1p2; reading an indeterminate value is undefined, J.2).

cfamily.State.wholeAt

def State.wholeAt {L : Constructs} (n : NodeId) (s : State L) (a : Address) : Evaluated L Object

The whole object at an address (a literal’s array is not an object that can be copied).

cfamily.State.lengthAt

def State.lengthAt {L : Constructs} (n : NodeId) (s : State L) (a : Address) : Evaluated L Nat

The number of elements of the array at an address (a variable length array’s length at run time).

cfamily.State.keptAs

def State.keptAs (chosen : List Chosen) (fuel : Nat) (b : Nat) (seen : List String) : Nat * List String

The number a block the library kept went on to, and the choices that took it there (a block kept again goes on; at most fuel steps).

cfamily.State.normalized

def State.normalized {L : Constructs} (s : State L) (p : Pointer) : Pointer * List String

A pointer as the run reads it: one to a block the library kept under a new number (the old number is dead) moved to the new number, with the choices that assumes; any other as it is.

cfamily.State.releasedBy

def State.releasedBy {L : Constructs} (s : State L) (p : Pointer) : List String

The choices a stop at a pointer depends on: its block was released only because of one.

cfamily.State.deadValue

def State.deadValue {L : Constructs} (s : State L) (v : Value) : Bool

Whether a value is a pointer to an object whose lifetime has ended: indeterminate (C11 6.2.4p2), so using it, even as a condition, is undefined.

cfamily.State.deadUse

def State.deadUse {L : Constructs} {A : Type} (n : NodeId) (s : State L) (v : Value) : Evaluated L A

The stop for using a pointer to an object whose lifetime has ended, with the choices that ended it.

cfamily.Evaluated.assuming

def Evaluated.assuming {L : Constructs} {A : Type} (n : NodeId) (cs : List String) (x : Evaluated L A) : Evaluated L A

A result with the choices it assumes: noted at the node on a value, carried by a stop.

cfamily.Evaluated.stopAssuming

def Evaluated.stopAssuming {L : Constructs} {A : Type} (n : NodeId) (b : Behavior) (cs : List String) : Evaluated L A

A stop at a node for a behavior, depending on the choices.

cfamily.State.stopAt

def State.stopAt {L : Constructs} {A : Type} (n : NodeId) (s : State L) (p : Pointer) (b : Behavior) : Evaluated L A

A stop for a behavior at a pointer, with the choices it depends on.

cfamily.State.follow

def State.follow {L : Constructs} (n : NodeId) (s : State L) (p : Pointer) : Evaluated L Address

The address a pointer designates, or why it designates none.

cfamily.State.move

def State.move {L : Constructs} (rules : Rules) (n : NodeId) (s : State L) (p : Pointer) (k : Int) : Evaluated L Value

p + k, or why it leaves the array; a null pointer plus 0 is null where the dialect’s rules say so.

cfamily.State.bothLive

def State.bothLive {L : Constructs} (s : State L) (p : Pointer) (q : Pointer) : Bool

Whether both pointers’ blocks are alive (a pointer to a dead block is indeterminate, C11 6.2.4p2).

cfamily.State.bothNormalized

def State.bothNormalized {L : Constructs} {A : Type} (n : NodeId) (s : State L) (p : Pointer) (q : Pointer) (next : Pointer -> Pointer -> Evaluated L A) : Evaluated L A

Two pointers as the run reads them (State.normalized), going on with them; the choices assumed noted.

cfamily.State.difference

def State.difference {L : Constructs} (rules : Rules) (n : NodeId) (s : State L) (p0 : Pointer) (q0 : Pointer) : Evaluated L Value

p - q: both alive and in the same array (C11 6.5.6p9); two null pointers give 0 where the dialect’s rules say so.

cfamily.BinaryOp.equality

def BinaryOp.equality (op : BinaryOp) (same : Bool) : Int

The result of an equality: == as is, != negated.

cfamily.Value.samePointer

def Value.samePointer (a : Value) (b : Value) : Bool

Whether two pointer values are equal: the same function, or the same place (C11 6.5.9p6).

cfamily.Value.normalizedPointer

def Value.normalizedPointer (v : Value) (p : Pointer) : Value

A pointer value with its pointer as the run reads it (a function stays as it is).

cfamily.State.comparePointers

def State.comparePointers {L : Constructs} (rules : Rules) (n : NodeId) (s : State L) (op : BinaryOp) (a : Value) (b : Value) : Evaluated L Value

A comparison of pointers, both alive: equality for any, order only within one array (C11 6.5.8p5; unspecified in C++, [expr.rel]p4).

cfamily.Value.toFloat

def Value.toFloat (f : FloatFormat) (v : Value) : Value

A value converted to a floating format: a floating value rounded, an integer exactly or rounded.

cfamily.Address.member

def Address.member (a : Address) (k : Nat) : Address

The address of the k-th member of the object at an address.

cfamily.Evaluator.fuel

def Evaluator.fuel : Nat

The fuel for one expression: deeper than any expression the checker accepts.

cfamily.TypedExpr.value

def TypedExpr.value {L : Constructs} (d : EvaluationDialect L) (s : State L) (e : TypedExpr L) : Evaluated L Value

An expression’s value in a state.

cfamily.TypedExpr.address

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

The address an lvalue designates in a state.

cfamily.TypedExpr.values

def TypedExpr.values {L : Constructs} (d : EvaluationDialect L) (s : State L) (es : List (TypedExpr L)) : Evaluated L (List Value)

Values in order.