diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-28 07:13:39 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-28 07:13:39 +0200 |
| commit | 0bd3d3c9cb1445a588ed4f254c5e036a213801c1 (patch) | |
| tree | 84af4dcde76f30fec3a1f77d2741e48c5444a338 /mppa_k1c/Asmblockdeps.v | |
| parent | e9e83f59ed2b1087ea974e7112abf71d8eb4195b (diff) | |
| download | compcert-kvx-0bd3d3c9cb1445a588ed4f254c5e036a213801c1.tar.gz compcert-kvx-0bd3d3c9cb1445a588ed4f254c5e036a213801c1.zip | |
simpler definition of reduce
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index e0aaee58..55a02633 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1579,20 +1579,31 @@ Definition is_constant (o: op): bool := | _ => false end. -Program Definition failsafe_reduce := Terms.failsafe_reduce is_constant. -Obligation 1. +Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None. +Proof. destruct o; simpl in * |- *; try congruence. destruct ao; simpl in * |- *; try congruence; destruct n; simpl in * |- *; try congruence; unfold arith_eval; destruct ge; simpl in * |- *; try congruence. Qed. +Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t). + +Local Hint Resolve is_constant_correct: wlp. + +Lemma main_reduce_correct t: + WHEN main_reduce t ~> pt THEN Terms.match_pt t pt. +Proof. + wlp_simplify. +Qed. + +Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}. Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then - IST.verb_bblock_simu_test failsafe_reduce string_of_name string_of_op (trans_block p1) (trans_block p2) + IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2) else - IST.bblock_simu_test failsafe_reduce (trans_block p1) (trans_block p2). + IST.bblock_simu_test reduce (trans_block p1) (trans_block p2). Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. |