Intermediate representation for sessions

[treiher]

Research

Concepts

• Three-Address Code (TAC)
• Static single assignment form (SSA)
• Continuation-Passing Style (CPS)

Languages

• C Intermediate Language

Design

Approach

Specification ⇾ Model ⤵
                     Intermediate Representation ⇾ SPARK Model ⇾ SPARK Code
          Integration ⤴

Objectives

• Represent actions of session states
• Enable static analysis / verification of session model
  • Take into account
    • Contracts of states
    • Contracts of functions
    • Type constraints
    • Buffer sizes defined in integration file
  • Prove absence of runtime errors (e.g., integer overflows)
  • Enable mapping of issues in the intermediate representation back to the specification
• Enable code generation for various languages (at least SPARK and C)
• Prevent unnecessary checks in generated code

Instructions

• Assignment (TAC, maybe also SSA?)
  • Variable
  • Literal
  • Mathematical expression (add, sub, mul, div, pow, mod)
  • Boolean expression (and, or)
  • Relation (lt, le, eq, ge, gt, ne)
  • Quantified expression (for all, for some)
  • Call expression
    • Variable
    • Constant
    • Literal
• Assertion
  • Boolean expression

Convertion from Model to IR

1. Transform state actions into TAC format
2. Transform model statements into IR instructions
3. Infer and add assertions (e.g., preconditions of calls, checks to prevent overflows)

Mapping from Model to IR

Statements

Model Statement	IR
VariableAssignment	Assignment
MessageFieldAssignment	Call?
Reset	Call?
Append	Call?
Extend	Call?
Read	Call?
Write	Call?

Expressions (in VariableAssignment)

Model (in TAC format)	IR
T := X	T:= X
T := not X	T := not X
T := X and Y	T := X and Y
(Other boolean expressions)	(Direct mapping)
(Mathematical expressions)	(Direct mapping)
(Relations)	(Direct mapping)
(Quantified expressions)	(Direct mapping)
T := X'Size	T := Type_Specific_Size_Func (X)
(Other attributes)	(Equivalent mapping to call)
T := M.F	T := Message_Type_Specific_Field_Func (M)
T := F (X, Y)	(Direct mapping)
T := (1, 2, 3)	(Direct mapping)
T := "FOO"	(Direct mapping)
T := [for I in S if C => I.X]	(Direct mapping or call)
T := M'(F1 => X, F2 => Y)	(Direct mapping or call)
(Binding)	(INVALID)

Implementation

• Create class hierarchy for IR
  • Separate session, statement, and expression classes
  • Comply with TAC
  • Generation of VCs for state actions #861
    • Enable determining preconditions for mathematical and boolean expressions (to enable detection and prevention of runtime errors)
    • Enable representation of preconditions and postconditions of function calls (e.g., for reading or setting message fields)
• Create transformation from existing session model to IR
• Adapt SPARK code generator to IR
• Create simple C code generator

[treiher]

Added in version 0.12.0.