infer_clone

Commit Graph

Author	SHA1	Message	Date
Scott Owens	5b7931e71a	[sledge sem] Add a rudimentary theory of SSA 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	5 years ago

Author

SHA1

Message

Date

Scott Owens

5b7931e71a

[sledge sem] Add a rudimentary theory of SSA

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

1 Commits (d3dc73a96e21ba7745075e2d2c67818af0f3d3b8)