Summary:
Show that the SSA restrictions imply that the blocks can be
topologically sorted so that any use of a variable follows its
definition in the list of blocks. This showed a slight flaw in my
definition of SSA form. It used to treat program counters up to
equality. However, PCs that point to a block header contain the location
that control came from (so that the Phi instructions can be executed),
but the SSA restrictions shouldn't pay attention to that, so now the
definition of SSA introduces a equivalence on PCs that ignores that
additional information.
Reviewed By: jberdine
Differential Revision: D21066873
fbshipit-source-id: 735575a1f
Summary:
Separate into separate files the theorems that are just about the
translation (mostly about the structure of the variable->expression
mapping that the translation builds) from theorems about the translation
and the semantics.
Also move the stuff about dominator_ordered into the SSA Theory, since
it only makes sense for SSA programs, but doesn't have anything to do
with the translation.
Reviewed By: jberdine
Differential Revision: D20673124
fbshipit-source-id: 9d8b08164
Summary:
The LLVM->LLAIR translation keeps a mapping of variables to expressions.
Previously, the invariants related to that mapping were kept in the
state relation, and so the proof needed show that they were preserved
along execution traces. This wasn't obvious as the state changes in
non-SSA ways during evaluation, but the correctness of the mappings is
heavily based on the program being in SSA form. This change separates
out the invariants, and the proof uses the final mapping that the
compiler builds, which contains all of the relevant bindings that might
be needed during execution.
Reviewed By: jberdine
Differential Revision: D20625109
fbshipit-source-id: d4c2dfe19
Summary:
Improve the invariants to show that phi instructions are correctly
translated. It remains to show that the invariants can be established
when jumping to the start of a block
Reviewed By: jberdine
Differential Revision: D18228272
fbshipit-source-id: 4330b4781
Summary:
This commit adds truncation, sign extension and zero extension to LLVM
and the Convert instruction to LLAIR.
The LLVM instructions use HOL's build-in word/int and word/num
conversions. Sanity-checking theorems prove that zero-extending leaves
the value of the word unchanged when considered as an unsigned value,
and that sign-extending leaves the value unchanged when considered as a
signed value.
The llair semantics for Convert uses the truncate_2comp function which
converts an integer to another integer as though they were represented
in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp
255 8 = -1, truncate_2comp -3 2 = 1
Reviewed By: jberdine
Differential Revision: D18058833
fbshipit-source-id: df9de480c
Summary:
Previously, the LLVM semantics could be stuck where the LLAIR semantics
was not yet stuck, but would become stuck (at the same place) after
taking a step. This was due to LLVM using the traditional definition of
stuck states: any state from which there are no transitions. However,
LLAIR cannot do that because it might get stuck in the middle of a block
that contains several visible stores. We don't want to consider the
whole block stuck, nor can we finish it. Thus, the LLAIR definition of
stuckness is when the state has the stuck flag set which happens when
stopping in the middle of a block after encountering a stuck
instruction. Now LLVM takes the same approach.
Reviewed By: jberdine
Differential Revision: D17855085
fbshipit-source-id: a094d25d5
Summary:
Add an argument to the Exit instruction. Update the LLVM semantics to
execute the Exit instruction and store the result in an "exited"
component of the state. (Previously it just noticed that it was stuck
about to do an Exit.)
With exiting treated uniformly, now in the proof that for every LLVM
trace, there is a llair trace that simulates it, all of the cheats
except for 1 are just cases that I haven't got to yet. However, the last
cheat is for the situation where the LLVM program gets stuck and the
llair program doesn't. For example, the following two line LLVM program
gets stuck because r2 is not assigned (ignoring for the moment the static
restriction that LLVM is in SSA form).
r1 := r2
Exit(0)
The compilation to llair omits the assignment and so we get a llair
program that doesn't get stuck:
Exit(0)
The key question is whether the static restrictions are sufficient to
ensure that no expression that might be omitted can get stuck.
Reviewed By: jberdine
Differential Revision: D17737589
fbshipit-source-id: bc6c01a1b
Summary:
If the LLVM to llair translation keeps a mapping from register r to
expression e, then for each register r' mentioned in e, there must be an
assignment to r' that dominates the entire live range of r. Thus, where
ever r might be replaced by e, the value of r' will be the same as it
was when the initial assignment to r occurred. Maintaining this
invariant relies on the LLVM being in SSA form.
Reviewed By: jberdine
Differential Revision: D17710288
fbshipit-source-id: fd3eaa57d
Summary:
Since the correcteness of the mapping from LLVM to llair depends on
LLVM being SSA, we need to formalise what that means. We also prove that
the domination relation is a strict partial order, which will probably
be helpful when reasoning about the translation.
Reviewed By: jberdine
Differential Revision: D17631456
fbshipit-source-id: a00eb3f87
Scott Owens