Module ullbc_to_llbc

Module ullbc_to_llbc 

Source
Expand description

ULLBC to LLBC

We reconstruct the control-flow in the Unstructured LLBC.

The reconstruction algorithm is not written to be efficient (its complexity is probably very bad), but it was not written to be: this is still an early stage and we want the algorithm to generate the best reconstruction as possible. We still need to test the algorithm on more interesting examples, and will consider making it more efficient once it is a bit mature and well tested. Also note that we more importantly focus on making the algorithm sound: the reconstructed program must always be equivalent to the original MIR program, and the fact that the reconstruction preserves this property must be obvious.

Finally, we conjecture the execution time shouldn’t be too much a problem: we don’t expect the translation mechanism to be applied on super huge functions (which will be difficult to formally analyze), and the MIR graphs are actually not that big because statements are grouped into code blocks (a block is made of a list of statements, followed by a terminator - branchings and jumps can only be performed by terminators -, meaning that MIR graphs don’t have that many nodes and edges).

StructsΒ§

BlockData πŸ”’
BlockWithRank πŸ”’
CfgInfo πŸ”’
Information precomputed about a function’s CFG.
ExitInfo πŸ”’
ExitsInfo πŸ”’
The exits of a graph
FilteredLoopParents πŸ”’
Irreducible πŸ”’
Error indicating that the control-flow graph is not reducible. The contained block id is a block involved in an irreducible subgraph.
LoopExitCandidateInfo πŸ”’
ReconstructCtx πŸ”’
Transform

EnumsΒ§

GotoKind πŸ”’

FunctionsΒ§

translate_body πŸ”’

Type AliasesΒ§

BigRational πŸ”’
BigUint πŸ”’
Arbitrary-precision numbers
Cfg πŸ”’
Control-Flow Graph
OrdBlockId πŸ”’