+++
title = "Adding predicates to symbolic execution"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a7c"]
forwardlinks = ["1b8", "3c3f", "2e1b", "3a7e"]
zettelid = "3a7d"
+++

Adding predicates to the symbolic execution and abstract interpretation
lets us compare the executions of hyperblocks ([\#1b8]), and is linked
to the formal verification of HLS ([\#3c3f]). However, this seems to add
a lot of complexity, because predicates take exponential time to check.
My main argument is though that often you will not have that many
predicates that are active within a block, and that it should therefore
not take that long to check.

In general, the idea is that each instruction can be conditionally
executed, meaning the results of the registers should also contain
conditionals. When checking the equivalences, it is therefore necessary
to evaluate the predicates somehow, to be able to then evaluate the
equivalence of the expressions, I believe that one first has to reduce
the expressions to a form which does not include the predicates. Then
one can compare bare expressions again.

This is similar to how the comparison of predicates in gated-SSA
([\#2e1b]) is performed \[1\], where extra functions are added to SSA
which contain the predicate that the choice functions act upon.

<div id="refs" class="references csl-bib-body" markdown="1">

<div id="ref-tu95_gated_ssa_based_deman_driven" class="csl-entry"
markdown="1">

<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">P. Tu and D. Padua, “Gated
SSA-based demand-driven symbolic analysis for parallelizing compilers,”
in *Proceedings of the 9th international conference on supercomputing*,
in ICS ’95. Barcelona, Spain: Association for Computing Machinery, 1995,
pp. 414–423. doi: [10.1145/224538.224648].</span>

</div>

</div>

  [\#1b8]: /zettel/1b8
  [\#3c3f]: /zettel/3c3f
  [\#2e1b]: /zettel/2e1b
  [10.1145/224538.224648]: https://doi.org/10.1145/224538.224648