lifting

cfamily.Lifted

record Lifted (L : Constructs)

An expression with the statements it needs first and the accesses it makes.

cfamily.LiftedList

record LiftedList (L : Constructs)

Expressions with the statements they need first and the accesses they make.

cfamily.Lifted.of

def Lifted.of {L : Constructs} (before : List (TypedStmt L)) (e : TypedExpr L) (writes : List (MemoryAccess L)) (reads : List (MemoryAccess L)) : Lifted L

An expression with its statements, writes and reads.

cfamily.Lifted.pure

def Lifted.pure {L : Constructs} (e : TypedExpr L) : Lifted L

An expression that needs nothing first and accesses nothing.

cfamily.LiftedList.empty

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

No expressions.

cfamily.TypedExpr.isLvalue

def TypedExpr.isLvalue {L : Constructs} (dialectLvalue : L.expr -> Bool) (e : TypedExpr L) : Bool

Whether an expression is an lvalue: a variable, a dereference, a string literal, a member of an lvalue (C11 6.5.2.3p3), or one of the dialect’s that it says is.

cfamily.TypedExpr.isConstLvalue

def TypedExpr.isConstLvalue {L : Constructs} (e : TypedExpr L) : Bool

Whether an lvalue designates a const object (its type, or a member of a const object).

cfamily.TypedExpr.lvalueType

def TypedExpr.lvalueType {L : Constructs} (p : Platform) (e : TypedExpr L) : Ty L

The type of an lvalue itself, const kept (taking its address points to it).

cfamily.TypedExpr.accessOf

def TypedExpr.accessOf {L : Constructs} (lv : TypedExpr L) : MemoryAccess L

The access an lvalue makes: a variable by name, anything else by its location.

cfamily.TypedExpr.readsOf

def TypedExpr.readsOf {L : Constructs} (dialectLvalue : L.expr -> Bool) (p : Platform) (lv : TypedExpr L) : List (MemoryAccess L)

The read of reading an lvalue’s value (an array is not read: it decays to its address).

cfamily.Lifted.both

def Lifted.both {L : Constructs} (n : NodeId) (a : Lifted L) (b : Lifted L) (combine : TypedExpr L -> TypedExpr L -> TypedExpr L) : Lifted L

Two unsequenced operands: both their statements (in order), the checks of their accesses after them, and the expression the results combine to.

cfamily.LiftedList.prepend

def LiftedList.prepend {L : Constructs} (n : NodeId) (a : Lifted L) (rest : LiftedList L) : LiftedList L

An operand followed by the rest, unsequenced: as Lifted.both, collecting the expressions.

cfamily.Lifted.map

def Lifted.map {L : Constructs} (f : TypedExpr L -> TypedExpr L) (a : Lifted L) : Lifted L

The expression changed, the rest kept.

cfamily.Lifted.after

def Lifted.after {L : Constructs} (ss : List (TypedStmt L)) (a : Lifted L) : Lifted L

Statements to run first, before what the expression already needs.