1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3a8g2b.md b/content/zettel/3a8g2b.md
new file mode 100644
index 0000000..c017128
--- /dev/null
+++ b/content/zettel/3a8g2b.md
@@ -0,0 +1,25 @@
++++
+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.