diff options
| -rw-r--r-- | cfrontend/Cop.v | 59 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 2 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 12 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 4 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 6 | ||||
| -rw-r--r-- | test/c/Makefile | 2 | ||||
| -rw-r--r-- | test/c/Results/sha3 | 4 | ||||
| -rw-r--r-- | test/c/sha3.c | 223 |
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; +} + |