driver: removed option -flonglong

test/c: added SHA3
cfrontend: support casts between long long and pointers, and comparisons between them.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2213 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 52 insertions, 25 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index c6e07b7..d085350 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -105,6 +105,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
   | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2
   | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2
+  | (Tpointer _ _ | Tcomp_ptr _ _), Tlong _ _ => cast_case_l2i I32 Unsigned
+  | Tlong si2 _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_i2l si2
   | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
   | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
   | Tvoid, _ => cast_case_void
@@ -805,6 +807,8 @@ Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
 
 Inductive classify_cmp_cases : Type :=
   | cmp_case_pp                       (**r pointer, pointer *)
+  | cmp_case_pl                       (**r pointer, long *)
+  | cmp_case_lp                       (**r long, pointer *)
   | cmp_default.                      (**r numerical, numerical *)
 
 Definition classify_cmp (ty1: type) (ty2: type) :=
@@ -812,6 +816,8 @@ Definition classify_cmp (ty1: type) (ty2: type) :=
   | Tpointer _ _ , Tpointer _ _ => cmp_case_pp
   | Tpointer _ _ , Tint _ _ _ => cmp_case_pp
   | Tint _ _ _, Tpointer _ _ => cmp_case_pp
+  | Tpointer _ _ , Tlong _ _ => cmp_case_pl
+  | Tlong _ _ , Tpointer _ _ => cmp_case_lp
   | _, _ => cmp_default
   end.
 
@@ -820,32 +826,21 @@ Definition sem_cmp (c:comparison)
                   (m: mem): option val :=
   match classify_cmp t1 t2 with
   | cmp_case_pp =>
-     option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
-(*
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
-      | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if zeq b1 b2 then
-            if Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)
-               && Mem.weak_valid_pointer m b2 (Int.unsigned ofs2)
-            then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
-            else None
-          else
-            if Mem.valid_pointer m b1 (Int.unsigned ofs1)
-               && Mem.valid_pointer m b2 (Int.unsigned ofs2)
-            then option_map Val.of_bool (Val.cmp_different_blocks c)
-            else None
-      | Vptr b ofs, Vint n =>
-          if Int.eq n Int.zero
-          then option_map Val.of_bool (Val.cmp_different_blocks c)
-          else None
-      | Vint n, Vptr b ofs =>
-          if Int.eq n Int.zero
-          then option_map Val.of_bool (Val.cmp_different_blocks c)
-          else None
-      | _,  _ => None
+      option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
+  | cmp_case_pl =>
+      match v2 with
+      | Vlong n2 => 
+          let n2 := Int.repr (Int64.unsigned n2) in
+          option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n2))
+      | _ => None
+      end
+  | cmp_case_lp =>
+      match v1 with
+      | Vlong n1 => 
+          let n1 := Int.repr (Int64.unsigned n1) in
+          option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c (Vint n1) v2)
+      | _ => None
       end
-*)
   | cmp_default =>
       sem_binarith
         (fun sg n1 n2 =>
@@ -1029,6 +1024,20 @@ Proof.
   replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b).
   simpl. TrivialInject. 
   symmetry. eapply val_cmpu_bool_inject; eauto. 
+- (* pointer - long *)
+  destruct v2; try discriminate. inv H1. 
+  set (v2 := Vint (Int.repr (Int64.unsigned i))) in *.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
+  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 v2) with (Some b).
+  simpl. TrivialInject. 
+  symmetry. eapply val_cmpu_bool_inject with (v2 := v2); eauto. constructor. 
+- (* long - pointer *)
+  destruct v1; try discriminate. inv H0. 
+  set (v1 := Vint (Int.repr (Int64.unsigned i))) in *.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
+  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp v1 tv2) with (Some b).
+  simpl. TrivialInject. 
+  symmetry. eapply val_cmpu_bool_inject with (v1 := v1); eauto. constructor. 
 - (* numerical - numerical *)
   assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))).
   {
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 2a27852..3ab286e 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -253,6 +253,8 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
   | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
+  | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2))
+  | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2)
   | cmp_default =>
       make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2
   end.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 7c24d0d..00ed1f6 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -563,6 +563,18 @@ Proof.
 - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
   simpl in SEM; inv SEM.
   econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto.
+- inv MAKE. destruct vb; try discriminate. 
+  set (vb := Vint (Int.repr (Int64.unsigned i))) in *.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
+  simpl in SEM; inv SEM.
+  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb. 
+  unfold Val.cmpu. rewrite E. auto.
+- inv MAKE. destruct va; try discriminate. 
+  set (va := Vint (Int.repr (Int64.unsigned i))) in *.
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
+  simpl in SEM; inv SEM.
+  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va. 
+  unfold Val.cmpu. rewrite E. auto.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 1dcf630..38660c6 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -280,6 +280,10 @@ Proof.
   destruct v; inv H. constructor.
   destruct v; inv H. constructor.
   destruct v; try discriminate. destruct (cast_float_long s f0); inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
 (* float *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H.
   constructor. apply cast_float_float_idem.