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

9 files changed, 282 insertions, 31 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.
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 619be1e..ea8e884 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -15,7 +15,6 @@
 let prepro_options = ref ([]: string list)
 let linker_options = ref ([]: string list)
 let assembler_options = ref ([]: string list)
-let option_flonglong = ref true
 let option_flongdouble = ref false
 let option_fstruct_return = ref false
 let option_fbitfields = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index eb0e004..e029aa2 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -379,7 +379,6 @@ Preprocessing options:
   -Wp,<opt>      Pass option <opt> to the preprocessor
 Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fbitfields    Emulate bit fields in structs [off]
-  -flonglong     Partial emulation of 'long long' types [on]
   -flongdouble   Treat 'long double' as 'double' [off]
   -fstruct-return  Emulate returning structs and unions by value [off]
   -fvararg-calls Emulate calls to variable-argument functions [on]
@@ -416,7 +415,7 @@ Linking options:
   -L<dir>        Add <dir> to search path for libraries
   -Wl,<opt>      Pass option <opt> to the linker
 General options:
-  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
+  -stdlib <dir>  Set the path of the Compcert run-time library
   -v             Print external commands before invoking them
 Interpreter mode:
   -interp        Execute given .c files using the reference interpreter
@@ -427,7 +426,7 @@ Interpreter mode:
 "
 
 let language_support_options = [
-  option_fbitfields; option_flonglong; option_flongdouble;
+  option_fbitfields; option_flongdouble;
   option_fstruct_return; option_fvararg_calls; option_fpacked_structs;
   option_finline_asm
 ]
@@ -497,7 +496,6 @@ let cmdline_actions =
   "-fnone$", Self (fun _ ->
               List.iter (fun r -> r := false) language_support_options);
   ]
-  @ f_opt "longlong" option_flonglong
   @ f_opt "longdouble" option_flongdouble
   @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
diff --git a/test/c/Makefile b/test/c/Makefile
index dbf3975..d14cb23 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -10,7 +10,7 @@ LIBS=$(LIBMATH)
 TIME=xtime -o /dev/null -mintime 2.0     # Xavier's hack
 #TIME=time >/dev/null                    # Otherwise
 
-PROGS=fib integr qsort fft fftw sha1 aes almabench lists \
+PROGS=fib integr qsort fft fftw sha1 sha3 aes almabench lists \
   binarytrees fannkuch knucleotide mandelbrot nbody \
   nsieve nsievebits spectral vmach \
   bisect chomp perlin siphash24
diff --git a/test/c/Results/sha3 b/test/c/Results/sha3
new file mode 100644
index 0000000..0f589cc
--- /dev/null
+++ b/test/c/Results/sha3
@@ -0,0 +1,4 @@
+SHA-3 224 passed
+SHA-3 256 passed
+SHA-3 384 passed
+SHA-3 512 passed
diff --git a/test/c/sha3.c b/test/c/sha3.c
new file mode 100644
index 0000000..29b8769
--- /dev/null
+++ b/test/c/sha3.c
@@ -0,0 +1,223 @@
+/* SHA-3 (Keccak) cryptographic hash function */
+/* Code adapted from the "readable" implementation written by
+   Markku-Juhani O. Saarinen <mjos@iki.fi> */
+
+#include <stdio.h>
+#include <string.h>
+
+typedef unsigned long long uint64;
+typedef unsigned char uint8;
+
+#define KECCAK_ROUNDS 24
+
+#define ROTL64(x, y) (((x) << (y)) | ((x) >> (64 - (y))))
+
+const uint64 keccakf_rndc[24] = 
+{
+    0x0000000000000001, 0x0000000000008082, 0x800000000000808a,
+    0x8000000080008000, 0x000000000000808b, 0x0000000080000001,
+    0x8000000080008081, 0x8000000000008009, 0x000000000000008a,
+    0x0000000000000088, 0x0000000080008009, 0x000000008000000a,
+    0x000000008000808b, 0x800000000000008b, 0x8000000000008089,
+    0x8000000000008003, 0x8000000000008002, 0x8000000000000080, 
+    0x000000000000800a, 0x800000008000000a, 0x8000000080008081,
+    0x8000000000008080, 0x0000000080000001, 0x8000000080008008
+};
+
+const int keccakf_rotc[24] = 
+{
+    1,  3,  6,  10, 15, 21, 28, 36, 45, 55, 2,  14, 
+    27, 41, 56, 8,  25, 43, 62, 18, 39, 61, 20, 44
+};
+
+const int keccakf_piln[24] = 
+{
+    10, 7,  11, 17, 18, 3, 5,  16, 8,  21, 24, 4, 
+    15, 23, 19, 13, 12, 2, 20, 14, 22, 9,  6,  1 
+};
+
+// update the state with KECCAK_ROUND rounds
+
+void keccakf(uint64 st[25])
+{
+    int j, round;
+    uint64 t, bc[5];
+
+    for (round = 0; round < KECCAK_ROUNDS; round++) {
+
+        // Theta
+#define THETA1(i) \
+            bc[i] = st[i] ^ st[i + 5] ^ st[i + 10] ^ st[i + 15] ^ st[i + 20]
+
+      THETA1(0); THETA1(1); THETA1(2); THETA1(3); THETA1(4);
+
+#define THETA2(i) \
+            t = bc[(i + 4) % 5] ^ ROTL64(bc[(i + 1) % 5], 1); \
+            st[0 + i] ^= t; \
+            st[5 + i] ^= t; \
+            st[10 + i] ^= t; \
+            st[15 + i] ^= t; \
+            st[20 + i] ^= t
+
+      THETA2(0); THETA2(1); THETA2(2); THETA2(3); THETA2(4);
+
+
+        // Rho Pi
+
+#define RHOPI(i, rotc) \
+            j = keccakf_piln[i]; \
+            bc[0] = st[j]; \
+            st[j] = ROTL64(t, rotc); \
+            t = bc[0]
+
+        t = st[1];
+        RHOPI(0, 1); RHOPI(1, 3); RHOPI(2, 6); RHOPI(3, 10);
+        RHOPI(4, 15); RHOPI(5, 21); RHOPI(6, 28); RHOPI(7, 36);
+        RHOPI(8, 45); RHOPI(9, 55); RHOPI(10, 2); RHOPI(11, 14);
+        RHOPI(12, 27); RHOPI(13, 41); RHOPI(14, 56); RHOPI(15, 8);
+        RHOPI(16, 25); RHOPI(17, 43); RHOPI(18, 62); RHOPI(19, 18);
+        RHOPI(20, 39); RHOPI(21, 61); RHOPI(22, 20); RHOPI(23, 44);
+
+        //  Chi
+
+#define CHI1(i,j) \
+                bc[i] = st[j + i]
+#define CHI2(i,j) \
+                st[j + i] ^= (~bc[(i + 1) % 5]) & bc[(i + 2) % 5]
+
+        for (j = 0; j < 25; j += 5) {
+          CHI1(0,j); CHI1(1,j); CHI1(2,j); CHI1(3,j); CHI1(4,j);
+          CHI2(0,j); CHI2(1,j); CHI2(2,j); CHI2(3,j); CHI2(4,j);
+        }
+
+        //  Iota
+        st[0] ^= keccakf_rndc[round];
+    }
+}
+
+// read a 64-bit integer in little endian at the given address
+
+static inline uint64 get64le(const uint8 *p)
+{
+  unsigned int l = p[0] | (p[1] << 8) | (p[2] << 16) | (p[3] << 24);
+  unsigned int h = p[4] | (p[5] << 8) | (p[6] << 16) | (p[7] << 24);
+  return l | ((uint64) h << 32);
+}
+
+// write a 64-bit integer in little endian at the given address
+
+static inline void set64le(uint8 * p, uint64 x)
+{
+  p[0] = x;       p[1] = x >> 8;  p[2] = x >> 16; p[3] = x >> 24;
+  p[4] = x >> 32; p[5] = x >> 40; p[6] = x >> 48; p[7] = x >> 56;
+}
+
+// compute a keccak hash (md) of the given byte length from "in"
+
+void keccak(const uint8 *in, int inlen, uint8 *md, int mdlen)
+{
+    uint64 st[25];    
+    uint8 temp[144];
+    int i, rsiz, rsizw;
+
+    rsiz = 200 - 2 * mdlen;
+    rsizw = rsiz / 8;
+    
+    memset(st, 0, sizeof(st));
+
+    for ( ; inlen >= rsiz; inlen -= rsiz, in += rsiz) {
+        for (i = 0; i < rsizw; i++)
+          st[i] ^= get64le(in + i * 8);
+        keccakf(st);
+    }
+    
+    // last block and padding
+    memcpy(temp, in, inlen);
+    temp[inlen++] = 1;
+    memset(temp + inlen, 0, rsiz - inlen);
+    temp[rsiz - 1] |= 0x80;
+
+    for (i = 0; i < rsizw; i++)
+      st[i] ^= get64le(temp + i * 8);
+
+    keccakf(st);
+
+    for(i = 0; i < 8; i++)
+      set64le(temp + i * 8, st[i]);
+
+    memcpy (md, temp, mdlen);
+}
+
+// test vectors
+
+typedef struct {
+    int mdlen;
+    char *msgstr;
+    uint8 md[64];
+} test_triplet_t;
+
+test_triplet_t testvec[4] = {   
+  {
+    28, "Keccak-224 Test Hash", {
+      0x30, 0x04, 0x5B, 0x34, 0x94, 0x6E, 0x1B, 0x2E, 
+      0x09, 0x16, 0x13, 0x36, 0x2F, 0xD2, 0x2A, 0xA0, 
+      0x8E, 0x2B, 0xEA, 0xFE, 0xC5, 0xE8, 0xDA, 0xEE, 
+      0x42, 0xC2, 0xE6, 0x65 }
+  }, {
+    32, "Keccak-256 Test Hash", {
+      0xA8, 0xD7, 0x1B, 0x07, 0xF4, 0xAF, 0x26, 0xA4, 
+      0xFF, 0x21, 0x02, 0x7F, 0x62, 0xFF, 0x60, 0x26, 
+      0x7F, 0xF9, 0x55, 0xC9, 0x63, 0xF0, 0x42, 0xC4, 
+      0x6D, 0xA5, 0x2E, 0xE3, 0xCF, 0xAF, 0x3D, 0x3C }
+  }, {
+    48, "Keccak-384 Test Hash", {
+      0xE2, 0x13, 0xFD, 0x74, 0xAF, 0x0C, 0x5F, 0xF9, 
+      0x1B, 0x42, 0x3C, 0x8B, 0xCE, 0xEC, 0xD7, 0x01, 
+      0xF8, 0xDD, 0x64, 0xEC, 0x18, 0xFD, 0x6F, 0x92, 
+      0x60, 0xFC, 0x9E, 0xC1, 0xED, 0xBD, 0x22, 0x30, 
+      0xA6, 0x90, 0x86, 0x65, 0xBC, 0xD9, 0xFB, 0xF4, 
+      0x1A, 0x99, 0xA1, 0x8A, 0x7D, 0x9E, 0x44, 0x6E }
+  }, {
+    64, "Keccak-512 Test Hash", {
+      0x96, 0xEE, 0x47, 0x18, 0xDC, 0xBA, 0x3C, 0x74, 
+      0x61, 0x9B, 0xA1, 0xFA, 0x7F, 0x57, 0xDF, 0xE7, 
+      0x76, 0x9D, 0x3F, 0x66, 0x98, 0xA8, 0xB3, 0x3F, 
+      0xA1, 0x01, 0x83, 0x89, 0x70, 0xA1, 0x31, 0xE6, 
+      0x21, 0xCC, 0xFD, 0x05, 0xFE, 0xFF, 0xBC, 0x11, 
+      0x80, 0xF2, 0x63, 0xC2, 0x7F, 0x1A, 0xDA, 0xB4, 
+      0x60, 0x95, 0xD6, 0xF1, 0x25, 0x33, 0x14, 0x72, 
+      0x4B, 0x5C, 0xBF, 0x78, 0x28, 0x65, 0x8E, 0x6A }
+  }
+};
+
+#define DATALEN 100000
+#define NITER 1000
+
+int main()
+{
+  static uint8 data[DATALEN];
+  int i;
+  uint8 md[64];
+
+  // test
+
+  for (i = 0; i < 4; i++) {
+    
+    keccak((uint8 *) testvec[i].msgstr, 
+           strlen(testvec[i].msgstr),
+           md, testvec[i].mdlen);
+
+    printf("SHA-3 %d %s\n",
+           testvec[i].mdlen * 8,
+           memcmp(md, testvec[i].md, testvec[i].mdlen) == 0 ? "passed" : "FAILED");
+
+  }
+
+  // benchmark
+  for (i = 0; i < DATALEN; i++) data[i] = i;
+  for (i = 0; i < NITER; i++)
+    keccak(data, DATALEN, md, 64);
+
+  return 0;
+}
+