Ir docs

[ailrst]

Adds a description of the IR to the documentation

\begin{align*}
Program ::=&~ Procedure* \\ 
Procedure ::=&~ (name: ProcID) (entryBlock: Block) (returnBlock: Block) (blocks: Block*) \\
               &~ \text{Where }entryBlock, returnBlock \in blocks \\
Block ::=&~ BlockID \; (Statement*)\; Jump \; (fallthrough: (GoTo | None))\\
         &~ \text{Where $fallthough$ may be $GoTo$ IF $Jump$ is $Call$} \\
Statement ::=&~ MemoryAssign ~|~ LocalAssign ~|~ Assume ~|~ Assert ~|~ NOP \\
ProcID ::=&~ String \\
BlockID ::=&~ String \\
\\
Jump ::=&~ Call ~|~ GoTo \\
GoTo ::=&~ \text{goto } BlockID* \\
Call ::=&~ DirectCall ~|~ IndirectCall  \\
DirectCall ::=&~ \text{call } ProcID \\
IndirectCall ::=&~ \text{call } Expr \\
\\
          &~ loads(e: Expr) = \{x |  x:MemoryLoad, x \in e \} \\
          &~ stores(e: Expr) = \{x |  x:MemoryStore, x \in e \} \\
\\
MemoryAssign ::=&~ Memory := MemoryStore \\
LocalAssign ::=&~ Variable := Expr \\
Assume ::=&~ \text{assume } body:Expr\\
          &\text {Such that } loads(body) = stores(body) = \emptyset \\
Assert ::=&~ \text{assert } body:Expr\\
          &\text {Such that } loads(body) = stores(body) = \emptyset \\
\\
Expr ::=&~ MemoryStore ~|~ MemoryLoad ~|~ Variable ~|~ Literal ~|~ Extract ~|~ Repeat \\
          &~ ~|~ ZeroExtend ~|~ SignExtend ~|~ UnaryExpr ~|~ BinaryExpr \\
Variable ::=&~ Global ~|~ LocalVar \\
MemoryStore ::=&~  (mem:Memory) (addr: Expr) (val: Expr) (Endian) (size: Int) \\
          &\text {Such that } loads(addr) = loads(val) = stores(addr) = stores(val) = \emptyset \\
MemoryLoad ::=&~  (mem:Memory)  (addr: Expr)  (Endian) (size: Int) \\
          &\text {Such that } loads(addr) = stores(addr) = stores(val) = \emptyset \\
Memory ::=&~ Stack ~|~ Mem \\
Endian ::=&~ BigEndian ~|~ LittleEndian \\
\end{align*}

[l-kent]

by definition Assumes and Asserts cannot contain MemoryStores so I don't think it is necessary to specify that stores(body) == null for them. There also isn't any reason that they can't contain loads and it is possible there may be some reason we use Assumes and Asserts in the future. Any loads in Assumes or Asserts would not count as such for the purposes of the information flow logic though.

Otherwise this seems fine

[ailrst]

Assumes and Asserts cannot contain MemoryStores so I don't think it is necessary to specify that stores(body) == null for them

stores(body) == \emptyset is the definition stating that assumes and asserts cannot contain stores.

I agree on loads, it should be okay for assumes and asserts to reference memory.

[l-kent]

Additionally, Global isn't a subclass of Variable, it's a separate trait.

The way it works is:

• Memory extends Expr with Global
• Variable extends Expr
• Register extends Variable with Global
• LocalVar extends Variable

Global means Memory or Register, which are the things that have a global scope from Boogie/the IR's perspective

Variable means Register or LocalVar, which are things that can be the LHS of a LocalAssign

[l-kent]

Maybe to make terminology consistent, we should use shared/non-shared in relation to concurrency, and local/global in relation to IR scoping?

[ailrst]

I agree that is the terminology I tend to use, although the new MMM also uses shared to denote variables that are pointed-to from multiple procedures.