Lang.Crucible.Utils.CoreRewrite

Documentation

annotateCFGStmts

Arguments

:: TraverseExt ext

=> (forall cin cout. Some (BlockID blocks) -> Size cout -> Stmt ext cin cout -> Maybe (StmtSeq ext blocks UnitType cout))

This is the annotation function. The resulting StmtSeq gets spliced in after the statement so that they can inspect the result if desired. The terminal statement is ignored.

-> (forall ctx'. Some (BlockID blocks) -> Size ctx' -> TermStmt blocks ret ctx' -> Maybe (StmtSeq ext blocks UnitType ctx'))

As above but for the final term stmt, where the annotation will be _before_ the term stmt.

-> CFG ext blocks ctx ret

-> CFG ext blocks ctx ret

This function walks through all the blocks in the CFG calling fS on each Stmt and fT on each TermStmt. These functions return a possible annotaition statement (which has access to the result of the statement, if any) along with a context diff which describes any new variables.