blob: c017128b6a0def617f624449bb729ff6cea5801b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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.
|
