+++
title = "Simplifying predicates over paths"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g2a"]
forwardlinks = ["3a8g2c"]
zettelid = "3a8g2b"
+++

One way to achieve this is to talk about how predicates are simplified
symbolically when traversing a path from a dominator of the predicate to
the predecessor of the γ function that the predicate should choose.
Incidentally, it does not even make sense to really talk about a
predecessor belonging to a predicate, because technically a predicate
could execute to true for two independent predecessors or none at all.

However, in a version of GSA where the predicates should be structurally
correct, as is the case right after the construction of GSA, then one
can actually formulate a property about the predicates which should hold
for them when symbolically executed on the path. This could say that all
predicates should simplify to a true value when executed along any of
the paths in the control-flow graph. This might be quite a strong
property, but it allows for a simple reconstruction of the control-flow
paths that lead to each predicate.