diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 16:31:03 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-03 16:31:03 +0200 |
| commit | 6f05c86e614797b76d92bc3dbbd4c0ece683168e (patch) | |
| tree | 1a77f29d33ba74405281c8a4a2737c45d640599f /backend/Duplicate.v | |
| parent | b59eb881ad3fd72b8743fb48d90e2751dc996e77 (diff) | |
| download | compcert-kvx-6f05c86e614797b76d92bc3dbbd4c0ece683168e.tar.gz compcert-kvx-6f05c86e614797b76d92bc3dbbd4c0ece683168e.zip | |
Proof for Iop
Diffstat (limited to 'backend/Duplicate.v')
| -rw-r--r-- | backend/Duplicate.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index ce6c436f..a96d0826 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -2,7 +2,7 @@ structures *) Require Import AST RTL Maps Globalenvs. -Require Import Coqlib Errors. +Require Import Coqlib Errors Op. Local Open Scope error_monad_scope. Local Open Scope positive_scope. @@ -45,9 +45,21 @@ Definition verify_is_copy revmap n n' := | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end end. + Definition verify_match_inst revmap inst tinst := match inst with | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + | Iop op lr r n => match tinst with + Iop op' lr' r' n' => + do u <- verify_is_copy revmap n n'; + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK tt + else Error (msg "Different r in Iop") + else Error (msg "Different lr in Iop") + else Error(msg "Different operations in Iop") + | _ => Error(msg "verify_match_inst Inop") end | _ => Error(msg "not implemented") end. |