blob: 7d47f7649f04375aef43f5da1da690889d1e8d89 (
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
|
+++
title = "Needing flexible evaluation for symbolic execution"
date = "2023-05-01"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3m"]
forwardlinks = ["3c3m2"]
zettelid = "3c3m1"
+++
When performing symbolic execution, we want flexible predicate
semantics, because we will encounter various situations in which
predicates are actually not evaluable by design. For example, we will
conditionally assign a predicate based on the value of another
predicate. In that case, we can only deduce what the evaluation is if
the original predicate was true. Otherwise, we do not even know whether
the expression assigned to the predicate is even evaluable, and it is
likely that that is not the case.
Therefore, when we generate a predicate, we can use the flexible
evaluation semantics for a predicate to encode this information, and
still end up with a predicate that is evaluable, even though there are
parts of it that are not evaluable.
|
