Lvc.IL.Annotation

Lvc.IL.IL

• Intermediate Language IL
  • Syntax
  • Semantics
    • Functional Semantics
    • Imperative Semantics

Lvc.IL.Var

• Definitions related to variables
  • A class for counted types
  • Variables
  • Locations
  • Labels
    • equality of labels is decidable
    • labels are counted
  • lab

Lvc.Equiv.Bisim

• Simulation

Lvc.Equiv.TraceEquiv

• Divergence
• Three equivalent notions of program equivalence
  • Prefix Trace Equivalence (partial traces)
    • Closedness under silent reduction/expansion
    • Bisimilarity is sound for prefix inclusion
    • The only prefix is empty if and only if the state diverges
    • Prefix Equivalence is sound for divergence
    • Several closedness properties
  • Trace Equivalence (maximal traces)
    • Several closedness properties
    • Bisimilarity is sound for maximal traces
    • Prefix trace equivalence coincides with maximal trace equivalence.
  • Bisimilarity is complete for prefix trace equivalence.

Lvc.Alpha

• Alpha Equivalence
  • Morphisims
  • Properties
    • ϱ and ϱ´ are inverses of each other on the free variables of s
    • Reflexivity
    • Symmetry
    • Transitivity
  • Soundness wrt. equivalence

Lvc.Liveness

• Liveness
  • Inductive Definition of Liveness
  • Relation between different overapproximations
  • live_sound ensures that the annotation matches the program
  • Some monotonicity properties
  • Live variables always contain the free variables
  • Liveness is stable under renaming
  • For functional programs, only free variables are significant
  • Since live variables contain free variables, liveness contains all variables significant to an IL/F program
  • Live variables contain all variables significant to an IL/I program

Lvc.Isa.Val

• More or less abstract values
  • There must be an injection into the booleans

Lvc.Isa.MoreExp

Lvc.Isa.Exp

• Expressions

Lvc.RenamedApart

• Renamed-apart (formally)
  • Morphisms
  • Relation to freeVars and occurVars
  • The two annotated sets are disjoint.

Lvc.Coherence.AllocationAlgo

• SSA-based register assignment formulated for IL
  • the algorithm produces a locally injective renaming
  • Theorem 8 from the paper.
  • Bound on the number of registers used
  • Theorem 8 from the paper.

Lvc.Coherence.Allocation

• Local Injectivity
  • Inductive definition of local injectivity of a renaming rho
  • Some Properties
  • local injectivity is decidable
  • Renaming with a locally injective renaming yields a coherent program
  • Theorem 6 from the paper.
  • Renaming with a locally injective renaming yields an α-equivalent program
  • Theorem 7 from the paper
  • local injectivity only looks at variables occuring in the program

Lvc.Coherence.Coherence

• Definition of Coherence: srd
  • Coherence is decidable
  • Some monotonicity properties
    • Every renamed apart program is coherent
    • In a coherent program, the globals of every function that can eventually be called are live
    • On a coherent program a liveness analysis which is sound imperatively is also sound functionally.
  • Definition of invariance
  • Agreement Invariant
  • Context coherence for IL/F contexts: approxF
  • Preservation properties
  • Main Theorem about Coherence
  • Coherence implies invariance

Lvc.Coherence.Restrict

Lvc.Fresh

Lvc.RenameApart

Lvc.RenamedApart_Liveness

Lvc.Alpha_RenamedApart

• Properties of Alpha Equivalence and Renamed Apart Programs
  • Definition of combine
  • Given an renamedApart program, every alpha-equivalent program
  • Alpha Equivalent programs map to identical De-Bruijn terms