From 322f3c865341fdfd5d22ab885b2934a5213ddbaa Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 17 Sep 2016 15:11:48 +0200
Subject: Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpy

Inline directives in extraction.v make the Caml output efficient and almost nice.
---
 cfrontend/Cexec.v       | 35 ++++-------------------------------
 extraction/extraction.v |  7 +++++++
 lib/Decidableplus.v     | 28 ++++++++++++++++++++++++++++
 3 files changed, 39 insertions(+), 31 deletions(-)

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index bf88e033..b7329a4d 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -15,6 +15,7 @@
 Require Import String.
 Require Import Axioms.
 Require Import Classical.
+Require Import Decidableplus.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
@@ -473,39 +474,11 @@ Definition memcpy_args_ok
    /\ (sz > 0 -> (al | odst))
    /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
 
-Remark memcpy_check_args:
-  forall sz al bdst odst bsrc osrc,
-  {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
-Proof with try (right; intuition omega).
-  intros.
-  assert (X: {al = 1 \/ al = 2 \/ al = 4 \/ al = 8} + {~(al = 1 \/ al = 2 \/ al = 4 \/ al = 8)}).
-    destruct (zeq al 1); auto. destruct (zeq al 2); auto.
-    destruct (zeq al 4); auto. destruct (zeq al 8); auto...
-  unfold memcpy_args_ok. destruct X...
-  assert (al > 0) by (intuition omega).
-  destruct (zle 0 sz)...
-  destruct (Zdivide_dec al sz); auto...
-  assert(U: forall x, {sz > 0 -> (al | x)} + {~(sz > 0 -> (al | x))}).
-    intros. destruct (zeq sz 0).
-    left; intros; omegaContradiction.
-    destruct (Zdivide_dec al x); auto. right; red; intros. elim n0. apply H0. omega.
-  destruct (U osrc); auto...
-  destruct (U odst); auto...
-  assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
-           +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}).
-    destruct (eq_block bsrc bdst); auto.
-    destruct (zeq osrc odst); auto.
-    destruct (zle (osrc + sz) odst); auto.
-    destruct (zle (odst + sz) osrc); auto.
-    right; intuition omega.
-  destruct Y... left; intuition omega.
-Defined.
-
 Definition do_ef_memcpy (sz al: Z)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
   | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
-      if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then
+      if decide (memcpy_args_ok sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc)) then
         do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
         do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
         Some(w, E0, Vundef, m')
@@ -581,7 +554,7 @@ Proof with try congruence.
   split. econstructor; eauto. omega. constructor.
 (* EF_memcpy *)
   unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs...
-  destruct v... destruct vargs... mydestr. red in m0.
+  destruct v... destruct vargs... mydestr. apply Decidable_sound in Heqb1. red in Heqb1.
   split. econstructor; eauto; tauto. constructor.
 (* EF_annot *)
   unfold do_ef_annot. mydestr.
@@ -623,7 +596,7 @@ Proof.
   inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega.
 (* EF_memcpy *)
   inv H; unfold do_ef_memcpy.
-  inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto.
+  inv H0. rewrite Decidable_complete, H7, H8. auto.
   red. tauto.
 (* EF_annot *)
   inv H; unfold do_ef_annot. inv H0. inv H6. inv H4.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index aecc07a5..8e13264c 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -12,6 +12,7 @@
 
 Require Coqlib.
 Require Wfsimpl.
+Require DecidableClass Decidableplus.
 Require AST.
 Require Iteration.
 Require Floats.
@@ -39,6 +40,12 @@ Require Import ExtrOcamlString.
 (* Coqlib *)
 Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
 
+(* Decidable *)
+
+Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide
+   Decidableplus.Decidable_and Decidableplus.Decidable_or
+   Decidableplus.Decidable_not Decidableplus.Decidable_implies.
+
 (* Wfsimpl *)
 Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
 
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 7772e07b..3bb6eee7 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.v
@@ -122,6 +122,34 @@ Next Obligation.
   apply Z.ltb_lt. 
 Qed.
 
+Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
+  Decidable_witness := Z.geb x y
+}.
+Next Obligation.
+  rewrite Z.geb_le. intuition omega.
+Qed.
+
+Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
+  Decidable_witness := Z.gtb x y
+}.
+Next Obligation.
+  rewrite Z.gtb_lt. intuition omega.
+Qed.
+
+Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
+  Decidable_witness := Z.eqb y ((y / x) * x)%Z
+}.
+Next Obligation.
+  split.
+  intros. apply Z.eqb_eq in H. exists (y / x). auto.
+  intros [k EQ]. apply Z.eqb_eq. 
+  destruct (Z.eq_dec x 0). 
+  subst x. rewrite Z.mul_0_r in EQ. subst y. reflexivity.
+  assert (k = y / x).
+  { apply Zdiv_unique_full with 0. red; omega. rewrite EQ; ring. }
+  congruence.
+Qed.
+
 (** Deciding properties over lists *)
 
 Program Instance Decidable_forall_in_list : 
-- 
cgit