normalize xs
produces a normalized BIL program with the same^1
semantics but in the BIL normalized form. Precondition: xs
is well-typed.
The BIL Normalized Form (BNF) is a subset of the BIL language, where expressions have the following properties:
- No let expressions - new variable can be created only with a Move instruction.
- All memory operations have sizes equal to one byte. Thus the size and endiannes can be ignored in analysis. During the normalization, the following rewrites are performed
- Memory load expressions can be only applied to a memory. This effectively disallows creation of temporary memory regions, and requires all store operations to be commited via the assignemnt operation. Also, this provides a guarantee, that store expressions will not occur in integer assigments, jmp destinations, and conditional expressions, leaving them valid only in an assignment statment where the rhs has type mem_t.
let x = <expr> in ... x ... => ... <expr> ...
x[a,el]:n => x[a+n-1] @ ... @ x[a]
x[a,be]:n => x[a] @ ... @ x[a+n-1]
m[a,el]:n <- x => (...((m[a] <- x<0>)[a+1] <- x<1>)...)[a+n-1] <- x<n-1>
m[a,be]:n <- x => (...((m[a] <- x<n-1>)[a+1] <- x<n>)...)[a+n-1] <- x<0>
... ite c ? x : y ... => if c \{ ... x ... } \{ ... y ... }
(x[a] <- b)[c] => m := x[a] <- b; m[c]
^1
: The normalization procedure may duplicate expressions that might be considered non-generative. For example,
let x = m[a] in x + x
is rewritten to m[a] + m[a]
. Given a concrete semantics of a memory (for example, if memory is mapped to a device register that changes every times it is read) this expression may have different value. It will also have different effect (such as two memory accesses, page faults etc).
However, in the formal semantics of BAP we do not consider effects, and treat all expressions as side-effect free, thus the above transformation, as well as