diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-25 10:14:54 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-25 10:14:54 +0200 |
| commit | 5b1c4771836a246e75eec07ccb1b72c83841baab (patch) | |
| tree | 696938647e2ebbe712d20551e46f053c471b0471 /mppa_k1c | |
| parent | ffaf5a655456e045f116fcd6b52e4faae9c8a7d4 (diff) | |
| download | compcert-kvx-5b1c4771836a246e75eec07ccb1b72c83841baab.tar.gz compcert-kvx-5b1c4771836a246e75eec07ccb1b72c83841baab.zip | |
add an example on depfree
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmbundle.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/mppa_k1c/Asmbundle.v b/mppa_k1c/Asmbundle.v index b5f92c2a..bd531930 100644 --- a/mppa_k1c/Asmbundle.v +++ b/mppa_k1c/Asmbundle.v @@ -228,11 +228,29 @@ Inductive depfreex : list breg -> list instruction -> Prop := | depfreex_nil : forall lw, depfreex lw nil | depfreex_cons : forall i lri lwi lw l, lri = readregs i -> lwi = writeregs i -> - disjoint (lri++lwi) lw -> (* Checking for WAW + RAW *) + disjoint_x lri lw -> (* Checking for RAW *) + disjoint_x lwi lw -> (* Checking for WAW *) depfreex (lw++lwi) l -> depfreex lw (i::l) . +Import ListNotations. + +Open Scope list_scope. + +Local Hint Resolve depfreex_nil depfreex_cons. + +Example depfreex_2 i1 i2 lw1 lr2 lw2: + lw1 = writeregs i1 -> + lr2 = readregs i2 -> + lw2 = writeregs i2 -> + disjoint_x lr2 lw1 -> (* RAW *) + disjoint_x lw2 lw1 -> (* WAW *) + depfreex [] [i1;i2]. +Proof. + intros; eapply depfreex_cons; eauto; + unfold disjoint_x; simpl; intuition. +Qed. (* FIXME: STUB *) Definition is_bundle (b:bblock):=True. |