summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--cfrontend/Cop.v59
-rw-r--r--cfrontend/Cshmgen.v2
-rw-r--r--cfrontend/Cshmgenproof.v12
-rw-r--r--cfrontend/SimplLocalsproof.v4
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml6
-rw-r--r--test/c/Makefile2
-rw-r--r--test/c/Results/sha34
-rw-r--r--test/c/sha3.c223
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;
+}
+