blob: 4a1e710d7b83bcfd34da10355644765cae2fb07b (
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
26
27
28
29
30
31
32
33
34
35
36
|
+++
title = "Equations on SSA"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5c", "3a8g5b", "3a8d"]
forwardlinks = ["3a8f", "3a8e1"]
zettelid = "3a8e"
+++
There is also a notion of equations in CompCertSSA, which means that one
can mathematically express the value that are stored in some registers.
``` coq
Lemma equation_lemma :
forall prog d op args x succ f m rs sp pc s,
wf_ssa_program prog ->
reachable prog (State s f sp pc rs m) ->
fn_code f d = Some (Iop op args x succ) ->
sdom f d pc ->
eval_operation sp op (rs##args) m = Some (rs#x).
```
Using the above Lemma, it is therefore possible to show that if
operation at `d` is an assignment of an `Iop` instruction to `x`, then
one can show that the evaluation of the operation with the arguments at
the current register set will be equal to the value that is stored in
the register set at `x`.
**Question**: One question I have though, is can the args of the current
register set not be different to the register set that was initially
used to evaluate the initial `Iop` instruction?
**Answer**: Actually, one possible answer to this is that the register
already encode the index, so the args will actually be exactly the same
that were used in the original evaluation of the `Iop` intruction.
|
