From 47fae389c800034e002c9f8a398e9adc79a14b81 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 May 2021 18:07:02 +0200 Subject: Native support for bit fields (#400) This big PR adds support for bit fields in structs and unions to the verified part of CompCert, namely the CompCert C and Clight languages. The compilation of bit field accesses to normal integer accesses + shifts and masks is done and proved correct as part of the Cshmgen pass. The layout of bit fields in memory is done by the functions in module Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic soundness properties of the layout are shown, such as "two different bit fields do not overlap" or "a bit field and a regular field do not overlap". All this replaces the previous emulation of bit fields by source-to-source rewriting in the unverified front-end of CompCert (module cparse/Bitfield.ml). This emulation was prone to errors (see nonstandard layout instead. The core idea for the PR is that expressions in l-value position denote not just a block, a byte offset and a type, but also a bitfield designator saying whether all the bits of the type are accessed (designator Full) or only some of its bits (designator Bits). Designators of the Bits kind appear when the l-value is a bit field access; the bit width and bit offset in Bits are computed by the functions in Ctypes that implement the layout algorithm. Consequently, both in the semantics of CompCert C and Clight and in the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a type and a bitfield designator are used in a number of places where a single type was used before. The introduction of bit fields has a big impact on static initialization (module cfrontend/Initializers.v), which had to be rewritten in large part, along with its soundness proof (cfrontend/Initializersproof.v). Both static initialization and run-time manipulation of bit fields are tested in test/abi using differential testing against GCC and randomly-generated structs. This work exposed subtle interactions between bit fields and the volatile modifier. Currently, the volatile modifier is ignored when accessing a bit field (and a warning is printed at compile-time), just like it is ignored when accessing a struct or union as a r-value. Currently, the natural alignment of bit fields and their storage units cannot be modified with the aligned attribute. _Alignas on bit fields is rejected as per C11, and the packed modifier cannot be applied to a struct containing bit fields. --- test/abi/.gitignore | 3 + test/abi/Makefile | 40 ++++++++- test/abi/generator.ml | 2 +- test/abi/genlayout.ml | 158 ++++++++++++++++++++++++++++++++++++ test/abi/layout.c | 59 ++++++++++++++ test/abi/staticlayout.c | 76 +++++++++++++++++ test/regression/Makefile | 2 +- test/regression/Results/bitfields10 | 14 ++++ test/regression/Results/bitfields9 | 18 +--- test/regression/Runtest | 2 +- test/regression/bitfields10.c | 66 +++++++++++++++ test/regression/bitfields9.c | 21 ++--- test/regression/sizeof1.c | 4 +- 13 files changed, 431 insertions(+), 34 deletions(-) create mode 100644 test/abi/genlayout.ml create mode 100644 test/abi/layout.c create mode 100644 test/abi/staticlayout.c create mode 100644 test/regression/Results/bitfields10 create mode 100644 test/regression/bitfields10.c (limited to 'test') diff --git a/test/abi/.gitignore b/test/abi/.gitignore index c115947e..5aa03c7c 100644 --- a/test/abi/.gitignore +++ b/test/abi/.gitignore @@ -2,7 +2,10 @@ *.c *.h *.compcert +*.cc *.cc2compcert *.compcert2cc *.light.c *.s +!layout.c +!staticlayout.c diff --git a/test/abi/Makefile b/test/abi/Makefile index eb9ca292..ef354e06 100644 --- a/test/abi/Makefile +++ b/test/abi/Makefile @@ -8,7 +8,10 @@ TESTS=fixed.compcert fixed.cc2compcert fixed.compcert2cc \ vararg.compcert vararg.cc2compcert vararg.compcert2cc \ struct.compcert struct.cc2compcert struct.compcert2cc -all: $(TESTS) +DIFFTESTS=layout.compcert layout.cc \ + staticlayout.compcert staticlayout.cc + +all: $(TESTS) $(DIFFTESTS) all_s: fixed_def_compcert.s fixed_use_compcert.s \ vararg_def_compcert.s vararg_use_compcert.s \ @@ -18,12 +21,22 @@ test: @set -e; for t in $(TESTS); do \ SIMU='$(SIMU)' ARCH=$(ARCH) MODEL=$(MODEL) ABI=$(ABI) SYSTEM=$(SYSTEM) ./Runtest $$t; \ done + @set -e; for t in layout staticlayout; do \ + $(SIMU) ./$$t.compcert > _compcert.log; \ + $(SIMU) ./$$t.cc > _cc.log; \ + if diff -a -u _cc.log _compcert.log; \ + then echo "$$t: CompCert and $CC agree"; rm _*.log; \ + else echo "$$t: CompCert and $CC DISAGREE"; exit 2; fi; \ + done generator.exe: generator.ml ocamlopt -g -o $@ generator.ml +genlayout.exe: genlayout.ml + ocamlopt -g -o $@ genlayout.ml + clean:: - rm -f generator.exe *.cm[iox] + rm -f generator.exe genlayout.exe *.cm[iox] fixed_decl.h: generator.exe ./generator.exe -rnd 500 -o fixed @@ -49,6 +62,16 @@ struct_def.c struct_use.c: struct_decl.h clean:: rm -f struct_decl.h struct_def.c struct_use.c +ifeq ($(ARCH),arm) +GENLAYOUT_OPTIONS += -stable +endif +ifeq ($(ARCH),aarch64) +GENLAYOUT_OPTIONS += -stable +endif + +layout.h: genlayout.exe + ./genlayout.exe $(GENLAYOUT_OPTIONS) > layout.h + struct%.o: CCOMPFLAGS += -fstruct-passing -dclight %_compcert.o: %.c @@ -61,6 +84,19 @@ struct%.o: CCOMPFLAGS += -fstruct-passing -dclight %_cc.s: %.c $(CC) $(CFLAGS) -S -o $@ $*.c +layout.compcert: layout.c layout.h + $(CCOMP) $(CCOMPFLAGS) -o $@ layout.c +layout.cc: layout.c layout.h + $(CC) $(CFLAGS) -o $@ layout.c + +staticlayout.compcert: staticlayout.c layout.h + $(CCOMP) $(CCOMPFLAGS) -o $@ staticlayout.c +staticlayout.cc: staticlayout.c layout.h + $(CC) $(CFLAGS) -o $@ staticlayout.c + +%.compcert: %_def_compcert.o %_use_compcert.o + $(CCOMP) -o $@ $*_def_compcert.o $*_use_compcert.o + %.compcert: %_def_compcert.o %_use_compcert.o $(CCOMP) -o $@ $*_def_compcert.o $*_use_compcert.o diff --git a/test/abi/generator.ml b/test/abi/generator.ml index aecee7cf..529352e0 100644 --- a/test/abi/generator.ml +++ b/test/abi/generator.ml @@ -439,7 +439,7 @@ let _ = " use the given seed for randomization" ] (fun s -> raise (Arg.Bad ("don't know what to do with " ^ s))) - "Usage: gencalls [options]\n\nOptions are:"; + "Usage: generator [options]\n\nOptions are:"; let oc0 = open_out (!output_prefix ^ "_decl.h") and oc1 = open_out (!output_prefix ^ "_def.c") and oc2 = open_out (!output_prefix ^ "_use.c") in diff --git a/test/abi/genlayout.ml b/test/abi/genlayout.ml new file mode 100644 index 00000000..5c26ca35 --- /dev/null +++ b/test/abi/genlayout.ml @@ -0,0 +1,158 @@ +open Printf + +type typ = Bool | Char | Short | Int + +type field = + | Plain of typ + | Bitfield of typ * int + | Padding of typ * int + +type struct_ = field list + +(* Concise description of a struct *) + +let print_typ oc = function + | Bool -> fprintf oc "b" + | Char -> fprintf oc "c" + | Short -> fprintf oc "s" + | Int -> fprintf oc "i" + +let print_padding_typ oc = function + | Bool -> fprintf oc "B" + | Char -> fprintf oc "C" + | Short -> fprintf oc "S" + | Int -> fprintf oc "I" + +let print_field oc = function + | Plain t -> print_typ oc t + | Bitfield(t, w) -> fprintf oc "%a%d" print_typ t w + | Padding(t, w) -> fprintf oc "%a%d" print_padding_typ t w + +let rec print_struct oc = function + | [] -> () + | f :: s -> print_field oc f; print_struct oc s + +(* Printing a struct in C syntax *) + +let c_typ oc = function + | Bool -> fprintf oc "_Bool" + | Char -> fprintf oc "char" + | Short -> fprintf oc "short" + | Int -> fprintf oc "int" + +let c_name oc n = fprintf oc "%c" (Char.chr (Char.code 'a' + n)) + +let c_field oc n = function + | Plain t -> + fprintf oc " %a %a;\n" c_typ t c_name n; + n + 1 + | Bitfield(t, w) -> + fprintf oc " %a %a:%d;\n" c_typ t c_name n w; + n + 1 + | Padding(t, w) -> + fprintf oc " %a :%d;\n" c_typ t w; + n + +let c_struct oc s = + fprintf oc "struct %a {\n" print_struct s; + let rec c_str n = function + | [] -> () + | f :: s -> let n' = c_field oc n f in c_str n' s in + c_str 0 s; + fprintf oc "};\n" + +(* Random generation of structs *) + +let random_1_8 () = + let n1 = Random.bits() in + let n2 = n1 lsr 2 in + match n1 land 3 with + | 0 -> 1 + | 1 -> 2 + (n2 land 1) (* 2-3 *) + | 2 -> 4 + (n2 land 1) (* 4-5 *) + | 3 -> 6 + (n2 mod 3) (* 6-8 *) + | _ -> assert false + +let random_1_16 () = + let n1 = Random.bits() in + let n2 = n1 lsr 2 in + match n1 land 3 with + | 0 -> 1 + (n2 land 1) (* 1-2 *) + | 1 -> 3 + (n2 mod 3) (* 3-4-5 *) + | 2 -> 6 + (n2 land 3) (* 6-7-8-9 *) + | 3 -> 10 + (n2 mod 7) (* 10-16 *) + | _ -> assert false + +let random_1_32 () = + let n1 = Random.bits() in + let n2 = n1 lsr 2 in + match n1 land 3 with + | 0 -> 1 + (n2 land 1) (* 1-2 *) + | 1 -> 3 + (n2 mod 5) (* 3-4-5-6-7 *) + | 2 -> 8 + (n2 mod 8) (* 8-15 *) + | 3 -> 16 + (n2 mod 17) (* 16-32 *) + | _ -> assert false + +let random_field () = + let (t, w) = + match Random.int 9 with + | 0 -> (Bool, 1) + | 1|2 -> (Char, random_1_8()) + | 3|4 -> (Short, random_1_16()) + | _ -> (Int, random_1_32()) in + match Random.int 10 with + | 0 -> Padding(t, (if Random.int 3 = 0 then 0 else w)) + | 1 | 2 -> Plain t + | _ -> Bitfield(t, w) + +let rec random_struct len = + if len <= 0 then [] else begin + let f = random_field () in + f :: random_struct (match f with Padding _ -> len | _ -> len - 1) + end + +(* Optional filtering of structs where padding fields can increase alignment. + ELF says that padding fields are ignored to determine struct alignment, + but ARM does otherwise. *) + +let alignof = function Bool -> 1 | Char -> 1 | Short -> 2 | Int -> 4 + +let unstable_alignment str = + let rec alignments al_data al_padding = function + | [] -> + al_padding > al_data + | (Plain t | Bitfield(t, _)) :: l -> + alignments (max (alignof t) al_data) al_padding l + | Padding(t, _) :: l -> + alignments al_data (max (alignof t) al_padding) l + in + alignments 1 1 str + +(* Random testing *) + +let structsize = ref 4 +let ntests = ref 1000 +let stable = ref false + +let _ = + Arg.parse [ + "-size", Arg.Int (fun n -> structsize := n), + " produce structs with members (default: 4)"; + "-n", Arg.Int (fun n -> ntests := n), + " produce random structs"; + "-seed", Arg.Int Random.init, + " use the given seed for randomization"; + "-stable", Arg.Set stable, + " don't generate padding fields that could cause differences in alignment" + ] + (fun s -> raise (Arg.Bad ("don't know what to do with " ^ s))) + "Usage: genlayout [options]\n\nOptions are:"; + for _i = 1 to !ntests do + let s = random_struct !structsize in + if not (!stable && unstable_alignment s) then begin + printf "{\n"; + c_struct stdout s; + printf "TEST%d(%a)\n" !structsize print_struct s; + printf "}\n" + end + done diff --git a/test/abi/layout.c b/test/abi/layout.c new file mode 100644 index 00000000..ebc6a2b2 --- /dev/null +++ b/test/abi/layout.c @@ -0,0 +1,59 @@ +#include +#include +#include +#include +#include "../endian.h" + +static inline int bit(void * p, unsigned bitno) +{ + unsigned byteno = bitno / 8; +#ifdef ARCH_BIG_ENDIAN + unsigned bit_in_byte = 7 - (bitno & 7); +#else + unsigned bit_in_byte = bitno & 7; +#endif + return (((unsigned char *) p)[byteno] >> bit_in_byte) & 1; +} + +void print_prologue(char * name, size_t al, size_t sz) +{ + printf("%s: align %d, sizeof %d, layout", name, (int)al, (int)sz); +} + +void print_next_field(_Bool first, size_t sz, void * p) +{ + static unsigned pos; + + if (first) pos = 0; + /* Find first bit set, starting with [pos] */ + while (1) { + assert (pos < 8 * sz); + if (bit(p, pos)) break; + pos += 1; + } + /* Print this position */ + printf(" %u", pos); + /* Skip over one bits */ + while (pos < 8 * sz && bit(p, pos)) pos++; +} + +void print_epilogue(void) +{ + printf("\n"); +} + +#define TEST4(s) \ + struct s x; \ + memset(&x, 0, sizeof(x)); \ + print_prologue(#s, _Alignof(struct s), sizeof(x)); \ + x.a = -1; print_next_field(1, sizeof(x), &x); \ + x.b = -1; print_next_field(0, sizeof(x), &x); \ + x.c = -1; print_next_field(0, sizeof(x), &x); \ + x.d = -1; print_next_field(0, sizeof(x), &x); \ + print_epilogue(); + +int main() +{ +#include "layout.h" + return 0; +} diff --git a/test/abi/staticlayout.c b/test/abi/staticlayout.c new file mode 100644 index 00000000..8a655afc --- /dev/null +++ b/test/abi/staticlayout.c @@ -0,0 +1,76 @@ +#include +#include "../endian.h" + +static inline int bit(void * p, unsigned bitno) +{ + unsigned byteno = bitno / 8; +#ifdef ARCH_BIG_ENDIAN + unsigned bit_in_byte = 7 - (bitno & 7); +#else + unsigned bit_in_byte = bitno & 7; +#endif + return (((unsigned char *) p)[byteno] >> bit_in_byte) & 1; +} + +void print_prologue(char * name, size_t al, size_t sz) +{ + printf("%s: align %d, sizeof %d, layout", name, (int)al, (int)sz); +} + +#if 0 +void print_contents(size_t sz, void * p) +{ + int last, lastpos; + printf(" - "); + last = 0; lastpos = 0; + for (int i = 0; i < sz; i++) { + for (int b = 0; b < 8; b++) { + int curr = bit((char *) p + i, b); + int currpos = i * 8 + b; + if (curr != last) { + if (currpos > lastpos) { + printf("%d(%d)", last, currpos - lastpos); + } + last = curr; lastpos = currpos; + } + } + } + { int currpos = sz * 8; + if (currpos > lastpos) { + printf("%d(%d)", last, currpos - lastpos); + } + } +} +#else +void print_contents(size_t sz, void * p) +{ + printf(" - "); + for (int i = 0; i < sz; i++) { + printf("%02x", ((unsigned char *)p)[i]); + } +} +#endif + +void print_epilogue (void) +{ + printf("\n"); +} + + +#define TEST4(s) \ + static struct s x1 = {-1, 0, 0, 0}; \ + static struct s x2 = {-1, -1, 0, 0}; \ + static struct s x3 = {-1, 0, -1, 0}; \ + static struct s x4 = {-1, -1, -1, -1}; \ + print_prologue(#s, _Alignof(struct s), sizeof(x1)); \ + print_contents(sizeof(x1), &x1); \ + print_contents(sizeof(x2), &x2); \ + print_contents(sizeof(x3), &x3); \ + print_contents(sizeof(x4), &x4); \ + print_epilogue(); + +int main() +{ +#include "layout.h" + return 0; +} diff --git a/test/regression/Makefile b/test/regression/Makefile index 698c1392..33a9f993 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -21,7 +21,7 @@ TESTS=int32 int64 floats floats-basics floats-lit \ # Can run, but only in compiled mode, and have reference output in Results TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ - bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t \ + bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t bitfields10 \ builtins-common builtins-$(ARCH) packedstruct1 packedstruct2 alignas \ varargs1 varargs2 varargs3 sections alias aligned diff --git a/test/regression/Results/bitfields10 b/test/regression/Results/bitfields10 new file mode 100644 index 00000000..9dc00daf --- /dev/null +++ b/test/regression/Results/bitfields10 @@ -0,0 +1,14 @@ +loc_s = { a = 11, b = 2 } +loc_t = { c = 11, d = 1, e = 2 } +loc_u_u = { u = -5 } +loc_u_v = { v = 3 } +compound_s = { a = 2, b = 3 } +compound_t = { c = 2, d = 1, e = -11 } +compound_u = { u = 2 } +loc_s = { a = 7, b = 2 } +loc_t = { c = 7, d = 1, e = 50 } +loc_u_u = { u = 7 } +loc_u_v = { v = 2 } +compound_s = { a = -14, b = 3 } +compound_t = { c = 50, d = 1, e = -7 } +compound_u = { u = 2 } diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9 index e35c2414..ec35fc08 100644 --- a/test/regression/Results/bitfields9 +++ b/test/regression/Results/bitfields9 @@ -2,17 +2,7 @@ glob_s = { a = -12, b = 1 } glob_t = { c = 123, d = 1, e = -45 } glob_u_u = { u = -3 } glob_u_v = { v = 6 } -loc_s = { a = 11, b = 2 } -loc_t = { c = 11, d = 1, e = 2 } -loc_u_u = { u = -5 } -loc_u_v = { v = 3 } -compound_s = { a = 2, b = 3 } -compound_t = { c = 2, d = 1, e = -11 } -compound_u = { u = 2 } -loc_s = { a = 7, b = 2 } -loc_t = { c = 7, d = 1, e = 50 } -loc_u_u = { u = 7 } -loc_u_v = { v = 2 } -compound_s = { a = -14, b = 3 } -compound_t = { c = 50, d = 1, e = -7 } -compound_u = { u = 2 } +loc_s = { a = -12, b = 1 } +loc_t = { c = 123, d = 1, e = -45 } +loc_u_u = { u = -3 } +loc_u_v = { v = 6 } diff --git a/test/regression/Runtest b/test/regression/Runtest index f693219a..600ae045 100755 --- a/test/regression/Runtest +++ b/test/regression/Runtest @@ -51,7 +51,7 @@ then exit 0 else echo "$name: WRONG OUTPUT (diff follows)" - diff -u "$ref" "$out" + diff -a -u "$ref" "$out" exit 2 fi else diff --git a/test/regression/bitfields10.c b/test/regression/bitfields10.c new file mode 100644 index 00000000..0f022664 --- /dev/null +++ b/test/regression/bitfields10.c @@ -0,0 +1,66 @@ +#include + +/* Dynamic initialization of bit-fields */ +/* Known not to work with the reference interpreter */ + +struct s { + signed char a: 6; + unsigned int b: 2; +}; + +struct t { + unsigned int c: 16; + _Bool d: 1; + short e: 8; + int : 10; +}; + +union u { + int u: 4; + unsigned int v: 3; +}; + +void print_s(char * msg, struct s p) +{ + printf("%s = { a = %d, b = %d }\n", msg, p.a, p.b); +} + +void print_t(char * msg, struct t p) +{ + printf("%s = { c = %d, d = %d, e = %d }\n", msg, p.c, p.d, p.e); +} + +void print_u_u(char * msg, union u p) +{ + printf("%s = { u = %d }\n", msg, p.u); +} + +void print_u_v(char * msg, union u p) +{ + printf("%s = { v = %u }\n", msg, p.v); +} + +/* Local, non-static initialization */ +void f(int x, int y, int z) +{ + struct s loc_s = { x, y }; + struct t loc_t = { x, z, y }; + union u loc_u_u = { .u = x }; + union u loc_u_v = { .v = z }; + print_s("loc_s", loc_s); + print_t("loc_t", loc_t); + print_u_u("loc_u_u", loc_u_u); + print_u_v("loc_u_v", loc_u_v); + print_s("compound_s", (struct s) { y, x }); + print_t("compound_t", (struct t) { y, ~z, -x }); + print_u_u("compound_u", (union u) { y }); +} + +int main() +{ + f(11, 2, 3); + f(7, 50, 2); + return 0; +} + + diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c index eef20168..025216fa 100644 --- a/test/regression/bitfields9.c +++ b/test/regression/bitfields9.c @@ -1,6 +1,6 @@ #include -/* Initialization of bit-fields */ +/* Static initialization of bit-fields */ struct s { signed char a: 6; @@ -39,27 +39,23 @@ void print_u_v(char * msg, union u p) printf("%s = { v = %u }\n", msg, p.v); } - /* Global initialization */ struct s glob_s = { -12, 1 }; struct t glob_t = { 123, 2, -45 }; union u glob_u_u = { -3 }; union u glob_u_v = { .v = 6 }; -/* Local initialization */ -void f(int x, int y, int z) +/* Local, static initialization */ +void f(void) { - struct s loc_s = { x, y }; - struct t loc_t = { x, z, y }; - union u loc_u_u = { .u = x }; - union u loc_u_v = { .v = z }; + static struct s loc_s = { -12, 1 }; + static struct t loc_t = { 123, 2, -45 }; + static union u loc_u_u = { -3 }; + static union u loc_u_v = { .v = 6 }; print_s("loc_s", loc_s); print_t("loc_t", loc_t); print_u_u("loc_u_u", loc_u_u); print_u_v("loc_u_v", loc_u_v); - print_s("compound_s", (struct s) { y, x }); - print_t("compound_t", (struct t) { y, ~z, -x }); - print_u_u("compound_u", (union u) { y }); } int main() @@ -68,8 +64,7 @@ int main() print_t("glob_t", glob_t); print_u_u("glob_u_u", glob_u_u); print_u_v("glob_u_v", glob_u_v); - f(11, 2, 3); - f(7, 50, 2); + f(); return 0; } diff --git a/test/regression/sizeof1.c b/test/regression/sizeof1.c index ca494622..5bd4d739 100644 --- a/test/regression/sizeof1.c +++ b/test/regression/sizeof1.c @@ -17,8 +17,8 @@ char tbl[sizeof(struct s)]; */ struct bits1 { - unsigned a: 1; - unsigned b: 6; + unsigned char a: 1; + unsigned char b: 6; }; char b1[sizeof(struct bits1)]; /* should be 1 */ -- cgit From 8eaff6bf3933f2213ae85584009e05123c40fa65 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 10:47:14 +0200 Subject: clightgen: handle empty names given to padding bit fields In the Clight AST, padding bit fields (such as `int : 6;`) in composite declarations are given an ident that corresponds to the empty string. Previously, clightgen would give name `_` to this ident, but this is not valid Coq. This commit gives name `empty_ident` to the empty ident. This name does not start with an underscore, so it cannot conflict with the names for regular idents, which all start with `_`. --- test/clightgen/bitfields.c | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/clightgen/bitfields.c (limited to 'test') diff --git a/test/clightgen/bitfields.c b/test/clightgen/bitfields.c new file mode 100644 index 00000000..34f6a686 --- /dev/null +++ b/test/clightgen/bitfields.c @@ -0,0 +1,13 @@ +struct s { + int a: 10; + char : 6; + _Bool b : 1; + int : 0; + short c: 7; +}; + +int f(void) +{ + struct s x = { -1, 1, 2 }; + return x.a + x.b + x.c; +} -- cgit From d32955030937937706b71a96dc6584800f0b8722 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 16 Sep 2021 11:03:40 +0200 Subject: Refactor clightgen Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/ --- test/clightgen/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile index f0e9d961..83ba0fd3 100644 --- a/test/clightgen/Makefile +++ b/test/clightgen/Makefile @@ -5,7 +5,7 @@ ARCHDIRS=$(ARCH) else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -RECDIRS := lib common $(ARCHDIRS) cfrontend exportclight +RECDIRS := lib common $(ARCHDIRS) cfrontend export COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) ifeq ($(LIBRARY_FLOCQ),local) COQINCLUDES += -R ../../flocq Flocq -- cgit From dffc9885e54f9c68af23ec79023dfe8516a4cc32 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 16 Sep 2021 14:54:22 +0200 Subject: Add support to clightgen for generating Csyntax AST as .v files As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output. --- test/Makefile | 2 +- test/clightgen/Makefile | 56 --- test/clightgen/annotations.c | 8 - test/clightgen/bitfields.c | 13 - test/clightgen/empty.c | 1 - test/clightgen/issue196.c | 927 ------------------------------------------- test/clightgen/issue216.c | 5 - test/clightgen/issue319.c | 12 - test/export/Makefile | 68 ++++ test/export/annotations.c | 8 + test/export/bitfields.c | 13 + test/export/clight/.gitkeep | 0 test/export/csyntax/.gitkeep | 0 test/export/empty.c | 1 + test/export/issue196.c | 927 +++++++++++++++++++++++++++++++++++++++++++ test/export/issue216.c | 5 + test/export/issue319.c | 12 + 17 files changed, 1035 insertions(+), 1023 deletions(-) delete mode 100644 test/clightgen/Makefile delete mode 100644 test/clightgen/annotations.c delete mode 100644 test/clightgen/bitfields.c delete mode 100644 test/clightgen/empty.c delete mode 100644 test/clightgen/issue196.c delete mode 100644 test/clightgen/issue216.c delete mode 100644 test/clightgen/issue319.c create mode 100644 test/export/Makefile create mode 100644 test/export/annotations.c create mode 100644 test/export/bitfields.c create mode 100644 test/export/clight/.gitkeep create mode 100644 test/export/csyntax/.gitkeep create mode 100644 test/export/empty.c create mode 100644 test/export/issue196.c create mode 100644 test/export/issue216.c create mode 100644 test/export/issue319.c (limited to 'test') diff --git a/test/Makefile b/test/Makefile index fa1fef30..ccf8fcd7 100644 --- a/test/Makefile +++ b/test/Makefile @@ -2,7 +2,7 @@ include ../Makefile.config DIRS=c compression raytracer spass regression abi ifeq ($(CLIGHTGEN),true) -DIRS+=clightgen +DIRS+=export endif all: diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile deleted file mode 100644 index 83ba0fd3..00000000 --- a/test/clightgen/Makefile +++ /dev/null @@ -1,56 +0,0 @@ -include ../../Makefile.config - -ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),) -ARCHDIRS=$(ARCH) -else -ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) -endif -RECDIRS := lib common $(ARCHDIRS) cfrontend export -COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) -ifeq ($(LIBRARY_FLOCQ),local) -COQINCLUDES += -R ../../flocq Flocq -endif - - -CLIGHTGEN=../../clightgen -COQC=coqc - -# Regression tests in the current directory -SRC=$(wildcard *.c) -# From ../c -SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \ - fftsp.c fftw.c fib.c integr.c knucleotide.c lists.c mandelbrot.c \ - nbody.c nsievebits.c nsieve.c perlin.c qsort.c sha1.c sha3.c \ - siphash24.c spectral.c vmach.c -# From ../raytracer -SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \ - matrix.c memory.c object.c render.c simplify.c surface.c vector.c - -CFLAGS=-DSYSTEM_$(SYSTEM) - -aes.vo almabench.vo binarytrees.vo bisect.vo chomp.vo: CFLAGS += -short-idents - -fft.vo fftsp.vo fftw.vo fib.vo integr.vo knucleotide.vo: CFLAGS += -short-idents -normalize - -qsort.vo sha1.vo sha3.vo siphash24.vo spectral.vo vmach.vo: CFLAGS += -normalize - -all: $(SRC:.c=.vo) - -test: - -%.v: %.c - $(CLIGHTGEN) $(CFLAGS) -o $@ $< - -%.v: ../c/%.c - $(CLIGHTGEN) $(CFLAGS) -o $@ $< - -%.v: ../raytracer/%.c - $(CLIGHTGEN) -I../raytracer -fall $(CFLAGS) -o $@ $< - -%.vo: %.v - $(COQC) $(COQINCLUDES) -noglob $< - -.SECONDARY: $(SRC:.c=.v) - -clean: - rm -f *.v *.vo* .*.aux diff --git a/test/clightgen/annotations.c b/test/clightgen/annotations.c deleted file mode 100644 index 993fa7d0..00000000 --- a/test/clightgen/annotations.c +++ /dev/null @@ -1,8 +0,0 @@ -int f(int x, long y) -{ -#if !defined(SYSTEM_macos) && !defined(SYSTEM_cygwin) - __builtin_ais_annot("x is %e1, y is %e2", x, y); -#endif - __builtin_annot("x is %1, y is %2", x, y); - return __builtin_annot_intval("x was here: %1", x); -} diff --git a/test/clightgen/bitfields.c b/test/clightgen/bitfields.c deleted file mode 100644 index 34f6a686..00000000 --- a/test/clightgen/bitfields.c +++ /dev/null @@ -1,13 +0,0 @@ -struct s { - int a: 10; - char : 6; - _Bool b : 1; - int : 0; - short c: 7; -}; - -int f(void) -{ - struct s x = { -1, 1, 2 }; - return x.a + x.b + x.c; -} diff --git a/test/clightgen/empty.c b/test/clightgen/empty.c deleted file mode 100644 index 8f8871a7..00000000 --- a/test/clightgen/empty.c +++ /dev/null @@ -1 +0,0 @@ -/* The empty source file */ diff --git a/test/clightgen/issue196.c b/test/clightgen/issue196.c deleted file mode 100644 index 1821fd6d..00000000 --- a/test/clightgen/issue196.c +++ /dev/null @@ -1,927 +0,0 @@ -#include -#include -#include - - -typedef int ASN1_BOOLEAN; -typedef int ASN1_NULL; -typedef struct ASN1_ITEM_st ASN1_ITEM; -typedef struct asn1_object_st ASN1_OBJECT; -typedef struct asn1_pctx_st ASN1_PCTX; -typedef struct asn1_string_st ASN1_BIT_STRING; -typedef struct asn1_string_st ASN1_BMPSTRING; -typedef struct asn1_string_st ASN1_ENUMERATED; -typedef struct asn1_string_st ASN1_GENERALIZEDTIME; -typedef struct asn1_string_st ASN1_GENERALSTRING; -typedef struct asn1_string_st ASN1_IA5STRING; -typedef struct asn1_string_st ASN1_INTEGER; -typedef struct asn1_string_st ASN1_OCTET_STRING; -typedef struct asn1_string_st ASN1_PRINTABLESTRING; -typedef struct asn1_string_st ASN1_STRING; -typedef struct asn1_string_st ASN1_T61STRING; -typedef struct asn1_string_st ASN1_TIME; -typedef struct asn1_string_st ASN1_UNIVERSALSTRING; -typedef struct asn1_string_st ASN1_UTCTIME; -typedef struct asn1_string_st ASN1_UTF8STRING; -typedef struct asn1_string_st ASN1_VISIBLESTRING; - -typedef struct AUTHORITY_KEYID_st AUTHORITY_KEYID; -typedef struct DIST_POINT_st DIST_POINT; -typedef struct ISSUING_DIST_POINT_st ISSUING_DIST_POINT; -typedef struct NAME_CONSTRAINTS_st NAME_CONSTRAINTS; -typedef struct X509_POLICY_CACHE_st X509_POLICY_CACHE; -typedef struct X509_POLICY_LEVEL_st X509_POLICY_LEVEL; -typedef struct X509_POLICY_NODE_st X509_POLICY_NODE; -typedef struct X509_POLICY_TREE_st X509_POLICY_TREE; -typedef struct X509_algor_st X509_ALGOR; -typedef struct X509_crl_st X509_CRL; -typedef struct X509_pubkey_st X509_PUBKEY; -typedef struct bignum_ctx BN_CTX; -typedef struct bignum_st BIGNUM; -typedef struct bio_method_st BIO_METHOD; -typedef struct bio_st BIO; -typedef struct bn_gencb_st BN_GENCB; -typedef struct bn_mont_ctx_st BN_MONT_CTX; -typedef struct buf_mem_st BUF_MEM; -typedef struct cbb_st CBB; -typedef struct cbs_st CBS; -typedef struct conf_st CONF; -typedef struct dh_method DH_METHOD; -typedef struct dh_st DH; -typedef struct dsa_method DSA_METHOD; -typedef struct dsa_st DSA; -typedef struct ec_key_st EC_KEY; -typedef struct ecdsa_method_st ECDSA_METHOD; -typedef struct ecdsa_sig_st ECDSA_SIG; -typedef struct engine_st ENGINE; -typedef struct env_md_ctx_st EVP_MD_CTX; -typedef struct env_md_st EVP_MD; -typedef struct evp_aead_st EVP_AEAD; -typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX; -typedef struct evp_cipher_st EVP_CIPHER; -typedef struct evp_pkey_asn1_method_st EVP_PKEY_ASN1_METHOD; -typedef struct evp_pkey_ctx_st EVP_PKEY_CTX; -typedef struct evp_pkey_method_st EVP_PKEY_METHOD; -typedef struct evp_pkey_st EVP_PKEY; -typedef struct hmac_ctx_st HMAC_CTX; -typedef struct md4_state_st MD4_CTX; -typedef struct md5_state_st MD5_CTX; -typedef struct pkcs8_priv_key_info_st PKCS8_PRIV_KEY_INFO; -typedef struct pkcs12_st PKCS12; -typedef struct rand_meth_st RAND_METHOD; -typedef struct rc4_key_st RC4_KEY; -typedef struct rsa_meth_st RSA_METHOD; -typedef struct rsa_st RSA; -typedef struct sha256_state_st SHA256_CTX; -typedef struct sha512_state_st SHA512_CTX; -typedef struct sha_state_st SHA_CTX; -typedef struct ssl_ctx_st SSL_CTX; -typedef struct ssl_st SSL; -typedef struct st_ERR_FNS ERR_FNS; -typedef struct v3_ext_ctx X509V3_CTX; -typedef struct x509_crl_method_st X509_CRL_METHOD; -typedef struct x509_revoked_st X509_REVOKED; -typedef struct x509_st X509; -typedef struct x509_store_ctx_st X509_STORE_CTX; -typedef struct x509_store_st X509_STORE; -typedef void *OPENSSL_BLOCK; - const EVP_MD *EVP_md4(void); - const EVP_MD *EVP_md5(void); - const EVP_MD *EVP_sha1(void); - const EVP_MD *EVP_sha224(void); - const EVP_MD *EVP_sha256(void); - const EVP_MD *EVP_sha384(void); - const EVP_MD *EVP_sha512(void); - - - - const EVP_MD *EVP_md5_sha1(void); - - - - const EVP_MD *EVP_get_digestbynid(int nid); - - - - const EVP_MD *EVP_get_digestbyobj(const ASN1_OBJECT *obj); - void EVP_MD_CTX_init(EVP_MD_CTX *ctx); - - - - EVP_MD_CTX *EVP_MD_CTX_create(void); - - - - int EVP_MD_CTX_cleanup(EVP_MD_CTX *ctx); - - - void EVP_MD_CTX_destroy(EVP_MD_CTX *ctx); - - - - int EVP_MD_CTX_copy_ex(EVP_MD_CTX *out, const EVP_MD_CTX *in); - - - - - - - - int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type, - ENGINE *engine); - - - - int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type); - - - - int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *data, - size_t len); - int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, uint8_t *md_out, - unsigned int *out_size); - - - - int EVP_DigestFinal(EVP_MD_CTX *ctx, uint8_t *md_out, - unsigned int *out_size); - - - - - - - int EVP_Digest(const void *data, size_t len, uint8_t *md_out, - unsigned int *md_out_size, const EVP_MD *type, - ENGINE *impl); - int EVP_MD_type(const EVP_MD *md); - - - const char *EVP_MD_name(const EVP_MD *md); - - - - uint32_t EVP_MD_flags(const EVP_MD *md); - - - size_t EVP_MD_size(const EVP_MD *md); - - - size_t EVP_MD_block_size(const EVP_MD *md); - int EVP_MD_CTX_copy(EVP_MD_CTX *out, const EVP_MD_CTX *in); - - - - int EVP_add_digest(const EVP_MD *digest); - - - - - - - const EVP_MD *EVP_MD_CTX_md(const EVP_MD_CTX *ctx); - - - - unsigned EVP_MD_CTX_size(const EVP_MD_CTX *ctx); - - - - unsigned EVP_MD_CTX_block_size(const EVP_MD_CTX *ctx); - - - - - int EVP_MD_CTX_type(const EVP_MD_CTX *ctx); - - - void EVP_MD_CTX_set_flags(EVP_MD_CTX *ctx, uint32_t flags); - - - - void EVP_MD_CTX_clear_flags(EVP_MD_CTX *ctx, uint32_t flags); - - - - uint32_t EVP_MD_CTX_test_flags(const EVP_MD_CTX *ctx, - uint32_t flags); - - -struct evp_md_pctx_ops; - -struct env_md_ctx_st { - - const EVP_MD *digest; - - uint32_t flags; - - - void *md_data; - - - - int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); - - - - EVP_PKEY_CTX *pctx; - - - - const struct evp_md_pctx_ops *pctx_ops; -} ; - - int MD4_Init(MD4_CTX *md4); - - - int MD4_Update(MD4_CTX *md4, const void *data, size_t len); - - - - - int MD4_Final(uint8_t *md, MD4_CTX *md4); - - - - void MD4_Transform(MD4_CTX *md4, const uint8_t *block); - -struct md4_state_st { - uint32_t A, B, C, D; - uint32_t Nl, Nh; - uint32_t data[16]; - unsigned int num; -}; - int MD5_Init(MD5_CTX *md5); - - - int MD5_Update(MD5_CTX *md5, const void *data, size_t len); - - - - - int MD5_Final(uint8_t *md, MD5_CTX *md5); - - - - uint8_t *MD5(const uint8_t *data, size_t len, uint8_t *out); - - - - void MD5_Transform(MD5_CTX *md5, const uint8_t *block); - -struct md5_state_st { - uint32_t A, B, C, D; - uint32_t Nl, Nh; - uint32_t data[16]; - unsigned int num; -}; -struct cbs_st { - const uint8_t *data; - size_t len; -}; - - - - void CBS_init(CBS *cbs, const uint8_t *data, size_t len); - - - - int CBS_skip(CBS *cbs, size_t len); - - - const uint8_t *CBS_data(const CBS *cbs); - - - size_t CBS_len(const CBS *cbs); - - - - - - - int CBS_stow(const CBS *cbs, uint8_t **out_ptr, size_t *out_len); - int CBS_strdup(const CBS *cbs, char **out_ptr); - - - - int CBS_contains_zero_byte(const CBS *cbs); - - - - - int CBS_mem_equal(const CBS *cbs, const uint8_t *data, - size_t len); - - - - int CBS_get_u8(CBS *cbs, uint8_t *out); - - - - int CBS_get_u16(CBS *cbs, uint16_t *out); - - - - int CBS_get_u24(CBS *cbs, uint32_t *out); - - - - int CBS_get_u32(CBS *cbs, uint32_t *out); - - - - int CBS_get_bytes(CBS *cbs, CBS *out, size_t len); - - - - - int CBS_get_u8_length_prefixed(CBS *cbs, CBS *out); - - - - - int CBS_get_u16_length_prefixed(CBS *cbs, CBS *out); - - - - - int CBS_get_u24_length_prefixed(CBS *cbs, CBS *out); - int CBS_get_asn1(CBS *cbs, CBS *out, unsigned tag_value); - - - - int CBS_get_asn1_element(CBS *cbs, CBS *out, unsigned tag_value); - - - - - - - int CBS_peek_asn1_tag(const CBS *cbs, unsigned tag_value); - int CBS_get_any_asn1_element(CBS *cbs, CBS *out, - unsigned *out_tag, - size_t *out_header_len); - - - - - - int CBS_get_asn1_uint64(CBS *cbs, uint64_t *out); - - - - - - - int CBS_get_optional_asn1(CBS *cbs, CBS *out, int *out_present, - unsigned tag); - - - - - - - - int CBS_get_optional_asn1_octet_string(CBS *cbs, CBS *out, - int *out_present, - unsigned tag); - - - - - - - int CBS_get_optional_asn1_uint64(CBS *cbs, uint64_t *out, - unsigned tag, - uint64_t default_value); - - - - - - - int CBS_get_optional_asn1_bool(CBS *cbs, int *out, unsigned tag, - int default_value); -struct cbb_buffer_st { - uint8_t *buf; - size_t len; - size_t cap; - char can_resize; - -}; - -struct cbb_st { - struct cbb_buffer_st *base; - - - size_t offset; - - struct cbb_st *child; - - - uint8_t pending_len_len; - char pending_is_asn1; - - - char is_top_level; -}; - - - - - int CBB_init(CBB *cbb, size_t initial_capacity); - - - - - int CBB_init_fixed(CBB *cbb, uint8_t *buf, size_t len); - - - - - void CBB_cleanup(CBB *cbb); - int CBB_finish(CBB *cbb, uint8_t **out_data, size_t *out_len); - - - - - int CBB_flush(CBB *cbb); - - - - - int CBB_add_u8_length_prefixed(CBB *cbb, CBB *out_contents); - - - - - int CBB_add_u16_length_prefixed(CBB *cbb, CBB *out_contents); - - - - - int CBB_add_u24_length_prefixed(CBB *cbb, CBB *out_contents); - - - - - - - int CBB_add_asn1(CBB *cbb, CBB *out_contents, uint8_t tag); - - - - int CBB_add_bytes(CBB *cbb, const uint8_t *data, size_t len); - - - - - - int CBB_add_space(CBB *cbb, uint8_t **out_data, size_t len); - - - - int CBB_add_u8(CBB *cbb, uint8_t value); - - - - int CBB_add_u16(CBB *cbb, uint16_t value); - - - - int CBB_add_u24(CBB *cbb, uint32_t value); - - - - - int CBB_add_asn1_uint64(CBB *cbb, uint64_t value); - ASN1_OBJECT *OBJ_dup(const ASN1_OBJECT *obj); - - - - int OBJ_cmp(const ASN1_OBJECT *a, const ASN1_OBJECT *b); - - - - - - - int OBJ_obj2nid(const ASN1_OBJECT *obj); - - - - int OBJ_cbs2nid(const CBS *cbs); - - - - int OBJ_sn2nid(const char *short_name); - - - - int OBJ_ln2nid(const char *long_name); - - - - - int OBJ_txt2nid(const char *s); - - - - - - - const ASN1_OBJECT *OBJ_nid2obj(int nid); - - - const char *OBJ_nid2sn(int nid); - - - const char *OBJ_nid2ln(int nid); - - - - int OBJ_nid2cbb(CBB *out, int nid); - ASN1_OBJECT *OBJ_txt2obj(const char *s, int dont_search_names); - int OBJ_obj2txt(char *out, int out_len, const ASN1_OBJECT *obj, - int dont_return_name); - - - - - - - int OBJ_create(const char *oid, const char *short_name, - const char *long_name); - int OBJ_find_sigid_algs(int sign_nid, int *out_digest_nid, - int *out_pkey_nid); - - - - - - - int OBJ_find_sigid_by_algs(int *out_sign_nid, int digest_nid, - int pkey_nid); - int SHA1_Init(SHA_CTX *sha); - - - int SHA1_Update(SHA_CTX *sha, const void *data, size_t len); - - - - - int SHA1_Final(uint8_t *md, SHA_CTX *sha); - - - - - uint8_t *SHA1(const uint8_t *data, size_t len, uint8_t *out); - - - - void SHA1_Transform(SHA_CTX *sha, const uint8_t *block); - -struct sha_state_st { - uint32_t h0, h1, h2, h3, h4; - uint32_t Nl, Nh; - uint32_t data[16]; - unsigned int num; -}; - int SHA224_Init(SHA256_CTX *sha); - - - int SHA224_Update(SHA256_CTX *sha, const void *data, size_t len); - - - - int SHA224_Final(uint8_t *md, SHA256_CTX *sha); - - - - - uint8_t *SHA224(const uint8_t *data, size_t len, uint8_t *out); - int SHA256_Init(SHA256_CTX *sha); - - - int SHA256_Update(SHA256_CTX *sha, const void *data, size_t len); - - - - int SHA256_Final(uint8_t *md, SHA256_CTX *sha); - - - - - uint8_t *SHA256(const uint8_t *data, size_t len, uint8_t *out); - - - - void SHA256_Transform(SHA256_CTX *sha, const uint8_t *data); - -struct sha256_state_st { - uint32_t h[8]; - uint32_t Nl, Nh; - uint32_t data[16]; - unsigned int num, md_len; -}; - int SHA384_Init(SHA512_CTX *sha); - - - int SHA384_Update(SHA512_CTX *sha, const void *data, size_t len); - - - - int SHA384_Final(uint8_t *md, SHA512_CTX *sha); - - - - - uint8_t *SHA384(const uint8_t *data, size_t len, uint8_t *out); - - - - void SHA384_Transform(SHA512_CTX *sha, const uint8_t *data); - int SHA512_Init(SHA512_CTX *sha); - - - int SHA512_Update(SHA512_CTX *sha, const void *data, size_t len); - - - - int SHA512_Final(uint8_t *md, SHA512_CTX *sha); - - - - - uint8_t *SHA512(const uint8_t *data, size_t len, uint8_t *out); - - - - void SHA512_Transform(SHA512_CTX *sha, const uint8_t *data); - -struct sha512_state_st { - uint64_t h[8]; - uint64_t Nl, Nh; - union { - uint64_t d[16]; - uint8_t p[128]; - } u; - unsigned int num, md_len; -}; - -struct env_md_st { - - - int type; - - - unsigned md_size; - - - uint32_t flags; - - - - int (*init)(EVP_MD_CTX *ctx); - - - int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); - - - int (*final)(EVP_MD_CTX *ctx, uint8_t *out); - - - unsigned block_size; - - - unsigned ctx_size; -}; - - - - -struct evp_md_pctx_ops { - - - void (*free) (EVP_PKEY_CTX *pctx); - - - - EVP_PKEY_CTX* (*dup) (EVP_PKEY_CTX *pctx); - - - - int (*begin_digest) (EVP_MD_CTX *ctx); -}; - - -static int md4_init(EVP_MD_CTX *ctx) { return MD4_Init(ctx->md_data); } - -static int md4_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return MD4_Update(ctx->md_data, data, count); -} - -static int md4_final(EVP_MD_CTX *ctx, unsigned char *out) { - return MD4_Final(out, ctx->md_data); -} - -static const EVP_MD md4_md = { - 257, 16, 0 , md4_init, - md4_update, md4_final, 64 , sizeof(MD4_CTX), -}; - -const EVP_MD *EVP_md4(void) { return &md4_md; } - - -static int md5_init(EVP_MD_CTX *ctx) { return MD5_Init(ctx->md_data); } - -static int md5_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return MD5_Update(ctx->md_data, data, count); -} - -static int md5_final(EVP_MD_CTX *ctx, unsigned char *out) { - return MD5_Final(out, ctx->md_data); -} - -static const EVP_MD md5_md = { - 4, 16, 0 , md5_init, - md5_update, md5_final, 64 , sizeof(MD5_CTX), -}; - -const EVP_MD *EVP_md5(void) { return &md5_md; } - - -static int sha1_init(EVP_MD_CTX *ctx) { return SHA1_Init(ctx->md_data); } - -static int sha1_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return SHA1_Update(ctx->md_data, data, count); -} - -static int sha1_final(EVP_MD_CTX *ctx, unsigned char *md) { - return SHA1_Final(md, ctx->md_data); -} - -static const EVP_MD sha1_md = { - 64, 20, 0 , sha1_init, - sha1_update, sha1_final, 64 , sizeof(SHA_CTX), -}; - -const EVP_MD *EVP_sha1(void) { return &sha1_md; } - - -static int sha224_init(EVP_MD_CTX *ctx) { return SHA224_Init(ctx->md_data); } - -static int sha224_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return SHA224_Update(ctx->md_data, data, count); -} - -static int sha224_final(EVP_MD_CTX *ctx, unsigned char *md) { - return SHA224_Final(md, ctx->md_data); -} - -static const EVP_MD sha224_md = { - 675, 28, 0 , - sha224_init, sha224_update, sha224_final, - 64 , sizeof(SHA256_CTX), -}; - -const EVP_MD *EVP_sha224(void) { return &sha224_md; } - - -static int sha256_init(EVP_MD_CTX *ctx) { return SHA256_Init(ctx->md_data); } - -static int sha256_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return SHA256_Update(ctx->md_data, data, count); -} - -static int sha256_final(EVP_MD_CTX *ctx, unsigned char *md) { - return SHA256_Final(md, ctx->md_data); -} - -static const EVP_MD sha256_md = { - 672, 32, 0 , - sha256_init, sha256_update, sha256_final, - 64 , sizeof(SHA256_CTX), -}; - -const EVP_MD *EVP_sha256(void) { return &sha256_md; } - - -static int sha384_init(EVP_MD_CTX *ctx) { return SHA384_Init(ctx->md_data); } - -static int sha384_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return SHA384_Update(ctx->md_data, data, count); -} - -static int sha384_final(EVP_MD_CTX *ctx, unsigned char *md) { - return SHA384_Final(md, ctx->md_data); -} - -static const EVP_MD sha384_md = { - 673, 48, 0 , - sha384_init, sha384_update, sha384_final, - 128 , sizeof(SHA512_CTX), -}; - -const EVP_MD *EVP_sha384(void) { return &sha384_md; } - - -static int sha512_init(EVP_MD_CTX *ctx) { return SHA512_Init(ctx->md_data); } - -static int sha512_update(EVP_MD_CTX *ctx, const void *data, size_t count) { - return SHA512_Update(ctx->md_data, data, count); -} - -static int sha512_final(EVP_MD_CTX *ctx, unsigned char *md) { - return SHA512_Final(md, ctx->md_data); -} - -static const EVP_MD sha512_md = { - 674, 64, 0 , - sha512_init, sha512_update, sha512_final, - 128 , sizeof(SHA512_CTX), -}; - -const EVP_MD *EVP_sha512(void) { return &sha512_md; } - - -typedef struct { - MD5_CTX md5; - SHA_CTX sha1; -} MD5_SHA1_CTX; - -static int md5_sha1_init(EVP_MD_CTX *md_ctx) { - MD5_SHA1_CTX *ctx = md_ctx->md_data; - return MD5_Init(&ctx->md5) && SHA1_Init(&ctx->sha1); -} - -static int md5_sha1_update(EVP_MD_CTX *md_ctx, const void *data, size_t count) { - MD5_SHA1_CTX *ctx = md_ctx->md_data; - return MD5_Update(&ctx->md5, data, count) && SHA1_Update(&ctx->sha1, data, count); -} - -static int md5_sha1_final(EVP_MD_CTX *md_ctx, unsigned char *out) { - MD5_SHA1_CTX *ctx = md_ctx->md_data; - if (!MD5_Final(out, &ctx->md5) || - !SHA1_Final(out + 16, &ctx->sha1)) { - return 0; - } - return 1; -} - -static const EVP_MD md5_sha1_md = { - 114, - 16 + 20, - 0 , - md5_sha1_init, - md5_sha1_update, - md5_sha1_final, - 64 , - sizeof(MD5_SHA1_CTX), -}; - -const EVP_MD *EVP_md5_sha1(void) { return &md5_sha1_md; } - - -struct nid_to_digest { - int nid; - const EVP_MD* (*md_func)(void); -}; - -static const struct nid_to_digest nid_to_digest_mapping[] = { - { 4, EVP_md5 }, - { 64, EVP_sha1 }, - { 675, EVP_sha224 }, - { 672, EVP_sha256 }, - { 673, EVP_sha384 }, - { 674, EVP_sha512 }, - { 114, EVP_md5_sha1 }, - { 66, EVP_sha1 }, - { 113, EVP_sha1 }, - { 416, EVP_sha1 }, - { 8, EVP_md5 }, - { 65, EVP_sha1 }, - { 671, EVP_sha224 }, - { 668, EVP_sha256 }, - { 669, EVP_sha384 }, - { 670, EVP_sha512 }, -}; - -const EVP_MD* EVP_get_digestbynid(int nid) { - unsigned i; - - for (i = 0; i < sizeof(nid_to_digest_mapping) / sizeof(struct nid_to_digest); - i++) { - if (nid_to_digest_mapping[i].nid == nid) { - return nid_to_digest_mapping[i].md_func(); - } - } - - return - ((void *)0) - ; -} - -const EVP_MD* EVP_get_digestbyobj(const ASN1_OBJECT *obj) { - return EVP_get_digestbynid(OBJ_obj2nid(obj)); -} diff --git a/test/clightgen/issue216.c b/test/clightgen/issue216.c deleted file mode 100644 index 796b69b4..00000000 --- a/test/clightgen/issue216.c +++ /dev/null @@ -1,5 +0,0 @@ -#include - -struct list {unsigned head; struct list *tail;}; -struct list three[] = { {1, three+1}, {2, three+2}, {3, NULL} }; -int f(int x) { return x;} diff --git a/test/clightgen/issue319.c b/test/clightgen/issue319.c deleted file mode 100644 index be9f3f7e..00000000 --- a/test/clightgen/issue319.c +++ /dev/null @@ -1,12 +0,0 @@ -/* Dollar signs in identifiers */ - -int c$d = 42; - -int a$b(int x$$) { - return c$d + x$$; -} - -int main(int argc, const char *argv[]) -{ - return a$b(6); -} diff --git a/test/export/Makefile b/test/export/Makefile new file mode 100644 index 00000000..d1228bf9 --- /dev/null +++ b/test/export/Makefile @@ -0,0 +1,68 @@ +include ../../Makefile.config + +ifeq ($(wildcard ../../$(ARCH)_$(BITSIZE)),) +ARCHDIRS=$(ARCH) +else +ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) +endif +RECDIRS := lib common $(ARCHDIRS) cfrontend export +COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +COQINCLUDES += -R ../../flocq Flocq +endif +COQINCLUDES += -R ./clight compcert.test.clight +COQINCLUDES += -R ./csyntax compcert.test.csyntax + +CLIGHTGEN=../../clightgen +COQC=coqc + +# Regression tests in the current directory +SRC=$(wildcard *.c) +# From ../c +SRC+=aes.c almabench.c binarytrees.c bisect.c chomp.c fannkuch.c fft.c \ + fftsp.c fftw.c fib.c integr.c knucleotide.c lists.c mandelbrot.c \ + nbody.c nsievebits.c nsieve.c perlin.c qsort.c sha1.c sha3.c \ + siphash24.c spectral.c vmach.c +# From ../raytracer +SRC+=arrays.c eval.c gmllexer.c gmlparser.c intersect.c light.c main.c \ + matrix.c memory.c object.c render.c simplify.c surface.c vector.c + +GENERATED=$(SRC:%.c=clight/%.v) $(SRC:%.c=csyntax/%.v) + +CFLAGS=-DSYSTEM_$(SYSTEM) + +aes.vo almabench.vo binarytrees.vo bisect.vo chomp.vo: CFLAGS += -short-idents + +fft.vo fftsp.vo fftw.vo fib.vo integr.vo knucleotide.vo: CFLAGS += -short-idents -normalize + +qsort.vo sha1.vo sha3.vo siphash24.vo spectral.vo vmach.vo: CFLAGS += -normalize + +all: $(GENERATED:.v=.vo) + +test: + +clight/%.v: %.c + $(CLIGHTGEN) -clight $(CFLAGS) -o $@ $< + +clight/%.v: ../c/%.c + $(CLIGHTGEN) -clight $(CFLAGS) -o $@ $< + +clight/%.v: ../raytracer/%.c + $(CLIGHTGEN) -clight -I../raytracer -fall $(CFLAGS) -o $@ $< + +csyntax/%.v: %.c + $(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $< + +csyntax/%.v: ../c/%.c + $(CLIGHTGEN) -csyntax $(CFLAGS) -o $@ $< + +csyntax/%.v: ../raytracer/%.c + $(CLIGHTGEN) -csyntax -I../raytracer -fall $(CFLAGS) -o $@ $< + +%.vo: %.v + $(COQC) $(COQINCLUDES) -noglob $< + +.SECONDARY: $(GENERATED) + +clean: + for d in clight csyntax; do rm -f $$d/*.v $$d/*.vo $$d/.*.aux; done diff --git a/test/export/annotations.c b/test/export/annotations.c new file mode 100644 index 00000000..993fa7d0 --- /dev/null +++ b/test/export/annotations.c @@ -0,0 +1,8 @@ +int f(int x, long y) +{ +#if !defined(SYSTEM_macos) && !defined(SYSTEM_cygwin) + __builtin_ais_annot("x is %e1, y is %e2", x, y); +#endif + __builtin_annot("x is %1, y is %2", x, y); + return __builtin_annot_intval("x was here: %1", x); +} diff --git a/test/export/bitfields.c b/test/export/bitfields.c new file mode 100644 index 00000000..34f6a686 --- /dev/null +++ b/test/export/bitfields.c @@ -0,0 +1,13 @@ +struct s { + int a: 10; + char : 6; + _Bool b : 1; + int : 0; + short c: 7; +}; + +int f(void) +{ + struct s x = { -1, 1, 2 }; + return x.a + x.b + x.c; +} diff --git a/test/export/clight/.gitkeep b/test/export/clight/.gitkeep new file mode 100644 index 00000000..e69de29b diff --git a/test/export/csyntax/.gitkeep b/test/export/csyntax/.gitkeep new file mode 100644 index 00000000..e69de29b diff --git a/test/export/empty.c b/test/export/empty.c new file mode 100644 index 00000000..8f8871a7 --- /dev/null +++ b/test/export/empty.c @@ -0,0 +1 @@ +/* The empty source file */ diff --git a/test/export/issue196.c b/test/export/issue196.c new file mode 100644 index 00000000..1821fd6d --- /dev/null +++ b/test/export/issue196.c @@ -0,0 +1,927 @@ +#include +#include +#include + + +typedef int ASN1_BOOLEAN; +typedef int ASN1_NULL; +typedef struct ASN1_ITEM_st ASN1_ITEM; +typedef struct asn1_object_st ASN1_OBJECT; +typedef struct asn1_pctx_st ASN1_PCTX; +typedef struct asn1_string_st ASN1_BIT_STRING; +typedef struct asn1_string_st ASN1_BMPSTRING; +typedef struct asn1_string_st ASN1_ENUMERATED; +typedef struct asn1_string_st ASN1_GENERALIZEDTIME; +typedef struct asn1_string_st ASN1_GENERALSTRING; +typedef struct asn1_string_st ASN1_IA5STRING; +typedef struct asn1_string_st ASN1_INTEGER; +typedef struct asn1_string_st ASN1_OCTET_STRING; +typedef struct asn1_string_st ASN1_PRINTABLESTRING; +typedef struct asn1_string_st ASN1_STRING; +typedef struct asn1_string_st ASN1_T61STRING; +typedef struct asn1_string_st ASN1_TIME; +typedef struct asn1_string_st ASN1_UNIVERSALSTRING; +typedef struct asn1_string_st ASN1_UTCTIME; +typedef struct asn1_string_st ASN1_UTF8STRING; +typedef struct asn1_string_st ASN1_VISIBLESTRING; + +typedef struct AUTHORITY_KEYID_st AUTHORITY_KEYID; +typedef struct DIST_POINT_st DIST_POINT; +typedef struct ISSUING_DIST_POINT_st ISSUING_DIST_POINT; +typedef struct NAME_CONSTRAINTS_st NAME_CONSTRAINTS; +typedef struct X509_POLICY_CACHE_st X509_POLICY_CACHE; +typedef struct X509_POLICY_LEVEL_st X509_POLICY_LEVEL; +typedef struct X509_POLICY_NODE_st X509_POLICY_NODE; +typedef struct X509_POLICY_TREE_st X509_POLICY_TREE; +typedef struct X509_algor_st X509_ALGOR; +typedef struct X509_crl_st X509_CRL; +typedef struct X509_pubkey_st X509_PUBKEY; +typedef struct bignum_ctx BN_CTX; +typedef struct bignum_st BIGNUM; +typedef struct bio_method_st BIO_METHOD; +typedef struct bio_st BIO; +typedef struct bn_gencb_st BN_GENCB; +typedef struct bn_mont_ctx_st BN_MONT_CTX; +typedef struct buf_mem_st BUF_MEM; +typedef struct cbb_st CBB; +typedef struct cbs_st CBS; +typedef struct conf_st CONF; +typedef struct dh_method DH_METHOD; +typedef struct dh_st DH; +typedef struct dsa_method DSA_METHOD; +typedef struct dsa_st DSA; +typedef struct ec_key_st EC_KEY; +typedef struct ecdsa_method_st ECDSA_METHOD; +typedef struct ecdsa_sig_st ECDSA_SIG; +typedef struct engine_st ENGINE; +typedef struct env_md_ctx_st EVP_MD_CTX; +typedef struct env_md_st EVP_MD; +typedef struct evp_aead_st EVP_AEAD; +typedef struct evp_cipher_ctx_st EVP_CIPHER_CTX; +typedef struct evp_cipher_st EVP_CIPHER; +typedef struct evp_pkey_asn1_method_st EVP_PKEY_ASN1_METHOD; +typedef struct evp_pkey_ctx_st EVP_PKEY_CTX; +typedef struct evp_pkey_method_st EVP_PKEY_METHOD; +typedef struct evp_pkey_st EVP_PKEY; +typedef struct hmac_ctx_st HMAC_CTX; +typedef struct md4_state_st MD4_CTX; +typedef struct md5_state_st MD5_CTX; +typedef struct pkcs8_priv_key_info_st PKCS8_PRIV_KEY_INFO; +typedef struct pkcs12_st PKCS12; +typedef struct rand_meth_st RAND_METHOD; +typedef struct rc4_key_st RC4_KEY; +typedef struct rsa_meth_st RSA_METHOD; +typedef struct rsa_st RSA; +typedef struct sha256_state_st SHA256_CTX; +typedef struct sha512_state_st SHA512_CTX; +typedef struct sha_state_st SHA_CTX; +typedef struct ssl_ctx_st SSL_CTX; +typedef struct ssl_st SSL; +typedef struct st_ERR_FNS ERR_FNS; +typedef struct v3_ext_ctx X509V3_CTX; +typedef struct x509_crl_method_st X509_CRL_METHOD; +typedef struct x509_revoked_st X509_REVOKED; +typedef struct x509_st X509; +typedef struct x509_store_ctx_st X509_STORE_CTX; +typedef struct x509_store_st X509_STORE; +typedef void *OPENSSL_BLOCK; + const EVP_MD *EVP_md4(void); + const EVP_MD *EVP_md5(void); + const EVP_MD *EVP_sha1(void); + const EVP_MD *EVP_sha224(void); + const EVP_MD *EVP_sha256(void); + const EVP_MD *EVP_sha384(void); + const EVP_MD *EVP_sha512(void); + + + + const EVP_MD *EVP_md5_sha1(void); + + + + const EVP_MD *EVP_get_digestbynid(int nid); + + + + const EVP_MD *EVP_get_digestbyobj(const ASN1_OBJECT *obj); + void EVP_MD_CTX_init(EVP_MD_CTX *ctx); + + + + EVP_MD_CTX *EVP_MD_CTX_create(void); + + + + int EVP_MD_CTX_cleanup(EVP_MD_CTX *ctx); + + + void EVP_MD_CTX_destroy(EVP_MD_CTX *ctx); + + + + int EVP_MD_CTX_copy_ex(EVP_MD_CTX *out, const EVP_MD_CTX *in); + + + + + + + + int EVP_DigestInit_ex(EVP_MD_CTX *ctx, const EVP_MD *type, + ENGINE *engine); + + + + int EVP_DigestInit(EVP_MD_CTX *ctx, const EVP_MD *type); + + + + int EVP_DigestUpdate(EVP_MD_CTX *ctx, const void *data, + size_t len); + int EVP_DigestFinal_ex(EVP_MD_CTX *ctx, uint8_t *md_out, + unsigned int *out_size); + + + + int EVP_DigestFinal(EVP_MD_CTX *ctx, uint8_t *md_out, + unsigned int *out_size); + + + + + + + int EVP_Digest(const void *data, size_t len, uint8_t *md_out, + unsigned int *md_out_size, const EVP_MD *type, + ENGINE *impl); + int EVP_MD_type(const EVP_MD *md); + + + const char *EVP_MD_name(const EVP_MD *md); + + + + uint32_t EVP_MD_flags(const EVP_MD *md); + + + size_t EVP_MD_size(const EVP_MD *md); + + + size_t EVP_MD_block_size(const EVP_MD *md); + int EVP_MD_CTX_copy(EVP_MD_CTX *out, const EVP_MD_CTX *in); + + + + int EVP_add_digest(const EVP_MD *digest); + + + + + + + const EVP_MD *EVP_MD_CTX_md(const EVP_MD_CTX *ctx); + + + + unsigned EVP_MD_CTX_size(const EVP_MD_CTX *ctx); + + + + unsigned EVP_MD_CTX_block_size(const EVP_MD_CTX *ctx); + + + + + int EVP_MD_CTX_type(const EVP_MD_CTX *ctx); + + + void EVP_MD_CTX_set_flags(EVP_MD_CTX *ctx, uint32_t flags); + + + + void EVP_MD_CTX_clear_flags(EVP_MD_CTX *ctx, uint32_t flags); + + + + uint32_t EVP_MD_CTX_test_flags(const EVP_MD_CTX *ctx, + uint32_t flags); + + +struct evp_md_pctx_ops; + +struct env_md_ctx_st { + + const EVP_MD *digest; + + uint32_t flags; + + + void *md_data; + + + + int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); + + + + EVP_PKEY_CTX *pctx; + + + + const struct evp_md_pctx_ops *pctx_ops; +} ; + + int MD4_Init(MD4_CTX *md4); + + + int MD4_Update(MD4_CTX *md4, const void *data, size_t len); + + + + + int MD4_Final(uint8_t *md, MD4_CTX *md4); + + + + void MD4_Transform(MD4_CTX *md4, const uint8_t *block); + +struct md4_state_st { + uint32_t A, B, C, D; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; + int MD5_Init(MD5_CTX *md5); + + + int MD5_Update(MD5_CTX *md5, const void *data, size_t len); + + + + + int MD5_Final(uint8_t *md, MD5_CTX *md5); + + + + uint8_t *MD5(const uint8_t *data, size_t len, uint8_t *out); + + + + void MD5_Transform(MD5_CTX *md5, const uint8_t *block); + +struct md5_state_st { + uint32_t A, B, C, D; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; +struct cbs_st { + const uint8_t *data; + size_t len; +}; + + + + void CBS_init(CBS *cbs, const uint8_t *data, size_t len); + + + + int CBS_skip(CBS *cbs, size_t len); + + + const uint8_t *CBS_data(const CBS *cbs); + + + size_t CBS_len(const CBS *cbs); + + + + + + + int CBS_stow(const CBS *cbs, uint8_t **out_ptr, size_t *out_len); + int CBS_strdup(const CBS *cbs, char **out_ptr); + + + + int CBS_contains_zero_byte(const CBS *cbs); + + + + + int CBS_mem_equal(const CBS *cbs, const uint8_t *data, + size_t len); + + + + int CBS_get_u8(CBS *cbs, uint8_t *out); + + + + int CBS_get_u16(CBS *cbs, uint16_t *out); + + + + int CBS_get_u24(CBS *cbs, uint32_t *out); + + + + int CBS_get_u32(CBS *cbs, uint32_t *out); + + + + int CBS_get_bytes(CBS *cbs, CBS *out, size_t len); + + + + + int CBS_get_u8_length_prefixed(CBS *cbs, CBS *out); + + + + + int CBS_get_u16_length_prefixed(CBS *cbs, CBS *out); + + + + + int CBS_get_u24_length_prefixed(CBS *cbs, CBS *out); + int CBS_get_asn1(CBS *cbs, CBS *out, unsigned tag_value); + + + + int CBS_get_asn1_element(CBS *cbs, CBS *out, unsigned tag_value); + + + + + + + int CBS_peek_asn1_tag(const CBS *cbs, unsigned tag_value); + int CBS_get_any_asn1_element(CBS *cbs, CBS *out, + unsigned *out_tag, + size_t *out_header_len); + + + + + + int CBS_get_asn1_uint64(CBS *cbs, uint64_t *out); + + + + + + + int CBS_get_optional_asn1(CBS *cbs, CBS *out, int *out_present, + unsigned tag); + + + + + + + + int CBS_get_optional_asn1_octet_string(CBS *cbs, CBS *out, + int *out_present, + unsigned tag); + + + + + + + int CBS_get_optional_asn1_uint64(CBS *cbs, uint64_t *out, + unsigned tag, + uint64_t default_value); + + + + + + + int CBS_get_optional_asn1_bool(CBS *cbs, int *out, unsigned tag, + int default_value); +struct cbb_buffer_st { + uint8_t *buf; + size_t len; + size_t cap; + char can_resize; + +}; + +struct cbb_st { + struct cbb_buffer_st *base; + + + size_t offset; + + struct cbb_st *child; + + + uint8_t pending_len_len; + char pending_is_asn1; + + + char is_top_level; +}; + + + + + int CBB_init(CBB *cbb, size_t initial_capacity); + + + + + int CBB_init_fixed(CBB *cbb, uint8_t *buf, size_t len); + + + + + void CBB_cleanup(CBB *cbb); + int CBB_finish(CBB *cbb, uint8_t **out_data, size_t *out_len); + + + + + int CBB_flush(CBB *cbb); + + + + + int CBB_add_u8_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + int CBB_add_u16_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + int CBB_add_u24_length_prefixed(CBB *cbb, CBB *out_contents); + + + + + + + int CBB_add_asn1(CBB *cbb, CBB *out_contents, uint8_t tag); + + + + int CBB_add_bytes(CBB *cbb, const uint8_t *data, size_t len); + + + + + + int CBB_add_space(CBB *cbb, uint8_t **out_data, size_t len); + + + + int CBB_add_u8(CBB *cbb, uint8_t value); + + + + int CBB_add_u16(CBB *cbb, uint16_t value); + + + + int CBB_add_u24(CBB *cbb, uint32_t value); + + + + + int CBB_add_asn1_uint64(CBB *cbb, uint64_t value); + ASN1_OBJECT *OBJ_dup(const ASN1_OBJECT *obj); + + + + int OBJ_cmp(const ASN1_OBJECT *a, const ASN1_OBJECT *b); + + + + + + + int OBJ_obj2nid(const ASN1_OBJECT *obj); + + + + int OBJ_cbs2nid(const CBS *cbs); + + + + int OBJ_sn2nid(const char *short_name); + + + + int OBJ_ln2nid(const char *long_name); + + + + + int OBJ_txt2nid(const char *s); + + + + + + + const ASN1_OBJECT *OBJ_nid2obj(int nid); + + + const char *OBJ_nid2sn(int nid); + + + const char *OBJ_nid2ln(int nid); + + + + int OBJ_nid2cbb(CBB *out, int nid); + ASN1_OBJECT *OBJ_txt2obj(const char *s, int dont_search_names); + int OBJ_obj2txt(char *out, int out_len, const ASN1_OBJECT *obj, + int dont_return_name); + + + + + + + int OBJ_create(const char *oid, const char *short_name, + const char *long_name); + int OBJ_find_sigid_algs(int sign_nid, int *out_digest_nid, + int *out_pkey_nid); + + + + + + + int OBJ_find_sigid_by_algs(int *out_sign_nid, int digest_nid, + int pkey_nid); + int SHA1_Init(SHA_CTX *sha); + + + int SHA1_Update(SHA_CTX *sha, const void *data, size_t len); + + + + + int SHA1_Final(uint8_t *md, SHA_CTX *sha); + + + + + uint8_t *SHA1(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA1_Transform(SHA_CTX *sha, const uint8_t *block); + +struct sha_state_st { + uint32_t h0, h1, h2, h3, h4; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num; +}; + int SHA224_Init(SHA256_CTX *sha); + + + int SHA224_Update(SHA256_CTX *sha, const void *data, size_t len); + + + + int SHA224_Final(uint8_t *md, SHA256_CTX *sha); + + + + + uint8_t *SHA224(const uint8_t *data, size_t len, uint8_t *out); + int SHA256_Init(SHA256_CTX *sha); + + + int SHA256_Update(SHA256_CTX *sha, const void *data, size_t len); + + + + int SHA256_Final(uint8_t *md, SHA256_CTX *sha); + + + + + uint8_t *SHA256(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA256_Transform(SHA256_CTX *sha, const uint8_t *data); + +struct sha256_state_st { + uint32_t h[8]; + uint32_t Nl, Nh; + uint32_t data[16]; + unsigned int num, md_len; +}; + int SHA384_Init(SHA512_CTX *sha); + + + int SHA384_Update(SHA512_CTX *sha, const void *data, size_t len); + + + + int SHA384_Final(uint8_t *md, SHA512_CTX *sha); + + + + + uint8_t *SHA384(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA384_Transform(SHA512_CTX *sha, const uint8_t *data); + int SHA512_Init(SHA512_CTX *sha); + + + int SHA512_Update(SHA512_CTX *sha, const void *data, size_t len); + + + + int SHA512_Final(uint8_t *md, SHA512_CTX *sha); + + + + + uint8_t *SHA512(const uint8_t *data, size_t len, uint8_t *out); + + + + void SHA512_Transform(SHA512_CTX *sha, const uint8_t *data); + +struct sha512_state_st { + uint64_t h[8]; + uint64_t Nl, Nh; + union { + uint64_t d[16]; + uint8_t p[128]; + } u; + unsigned int num, md_len; +}; + +struct env_md_st { + + + int type; + + + unsigned md_size; + + + uint32_t flags; + + + + int (*init)(EVP_MD_CTX *ctx); + + + int (*update)(EVP_MD_CTX *ctx, const void *data, size_t count); + + + int (*final)(EVP_MD_CTX *ctx, uint8_t *out); + + + unsigned block_size; + + + unsigned ctx_size; +}; + + + + +struct evp_md_pctx_ops { + + + void (*free) (EVP_PKEY_CTX *pctx); + + + + EVP_PKEY_CTX* (*dup) (EVP_PKEY_CTX *pctx); + + + + int (*begin_digest) (EVP_MD_CTX *ctx); +}; + + +static int md4_init(EVP_MD_CTX *ctx) { return MD4_Init(ctx->md_data); } + +static int md4_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return MD4_Update(ctx->md_data, data, count); +} + +static int md4_final(EVP_MD_CTX *ctx, unsigned char *out) { + return MD4_Final(out, ctx->md_data); +} + +static const EVP_MD md4_md = { + 257, 16, 0 , md4_init, + md4_update, md4_final, 64 , sizeof(MD4_CTX), +}; + +const EVP_MD *EVP_md4(void) { return &md4_md; } + + +static int md5_init(EVP_MD_CTX *ctx) { return MD5_Init(ctx->md_data); } + +static int md5_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return MD5_Update(ctx->md_data, data, count); +} + +static int md5_final(EVP_MD_CTX *ctx, unsigned char *out) { + return MD5_Final(out, ctx->md_data); +} + +static const EVP_MD md5_md = { + 4, 16, 0 , md5_init, + md5_update, md5_final, 64 , sizeof(MD5_CTX), +}; + +const EVP_MD *EVP_md5(void) { return &md5_md; } + + +static int sha1_init(EVP_MD_CTX *ctx) { return SHA1_Init(ctx->md_data); } + +static int sha1_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA1_Update(ctx->md_data, data, count); +} + +static int sha1_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA1_Final(md, ctx->md_data); +} + +static const EVP_MD sha1_md = { + 64, 20, 0 , sha1_init, + sha1_update, sha1_final, 64 , sizeof(SHA_CTX), +}; + +const EVP_MD *EVP_sha1(void) { return &sha1_md; } + + +static int sha224_init(EVP_MD_CTX *ctx) { return SHA224_Init(ctx->md_data); } + +static int sha224_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA224_Update(ctx->md_data, data, count); +} + +static int sha224_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA224_Final(md, ctx->md_data); +} + +static const EVP_MD sha224_md = { + 675, 28, 0 , + sha224_init, sha224_update, sha224_final, + 64 , sizeof(SHA256_CTX), +}; + +const EVP_MD *EVP_sha224(void) { return &sha224_md; } + + +static int sha256_init(EVP_MD_CTX *ctx) { return SHA256_Init(ctx->md_data); } + +static int sha256_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA256_Update(ctx->md_data, data, count); +} + +static int sha256_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA256_Final(md, ctx->md_data); +} + +static const EVP_MD sha256_md = { + 672, 32, 0 , + sha256_init, sha256_update, sha256_final, + 64 , sizeof(SHA256_CTX), +}; + +const EVP_MD *EVP_sha256(void) { return &sha256_md; } + + +static int sha384_init(EVP_MD_CTX *ctx) { return SHA384_Init(ctx->md_data); } + +static int sha384_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA384_Update(ctx->md_data, data, count); +} + +static int sha384_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA384_Final(md, ctx->md_data); +} + +static const EVP_MD sha384_md = { + 673, 48, 0 , + sha384_init, sha384_update, sha384_final, + 128 , sizeof(SHA512_CTX), +}; + +const EVP_MD *EVP_sha384(void) { return &sha384_md; } + + +static int sha512_init(EVP_MD_CTX *ctx) { return SHA512_Init(ctx->md_data); } + +static int sha512_update(EVP_MD_CTX *ctx, const void *data, size_t count) { + return SHA512_Update(ctx->md_data, data, count); +} + +static int sha512_final(EVP_MD_CTX *ctx, unsigned char *md) { + return SHA512_Final(md, ctx->md_data); +} + +static const EVP_MD sha512_md = { + 674, 64, 0 , + sha512_init, sha512_update, sha512_final, + 128 , sizeof(SHA512_CTX), +}; + +const EVP_MD *EVP_sha512(void) { return &sha512_md; } + + +typedef struct { + MD5_CTX md5; + SHA_CTX sha1; +} MD5_SHA1_CTX; + +static int md5_sha1_init(EVP_MD_CTX *md_ctx) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + return MD5_Init(&ctx->md5) && SHA1_Init(&ctx->sha1); +} + +static int md5_sha1_update(EVP_MD_CTX *md_ctx, const void *data, size_t count) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + return MD5_Update(&ctx->md5, data, count) && SHA1_Update(&ctx->sha1, data, count); +} + +static int md5_sha1_final(EVP_MD_CTX *md_ctx, unsigned char *out) { + MD5_SHA1_CTX *ctx = md_ctx->md_data; + if (!MD5_Final(out, &ctx->md5) || + !SHA1_Final(out + 16, &ctx->sha1)) { + return 0; + } + return 1; +} + +static const EVP_MD md5_sha1_md = { + 114, + 16 + 20, + 0 , + md5_sha1_init, + md5_sha1_update, + md5_sha1_final, + 64 , + sizeof(MD5_SHA1_CTX), +}; + +const EVP_MD *EVP_md5_sha1(void) { return &md5_sha1_md; } + + +struct nid_to_digest { + int nid; + const EVP_MD* (*md_func)(void); +}; + +static const struct nid_to_digest nid_to_digest_mapping[] = { + { 4, EVP_md5 }, + { 64, EVP_sha1 }, + { 675, EVP_sha224 }, + { 672, EVP_sha256 }, + { 673, EVP_sha384 }, + { 674, EVP_sha512 }, + { 114, EVP_md5_sha1 }, + { 66, EVP_sha1 }, + { 113, EVP_sha1 }, + { 416, EVP_sha1 }, + { 8, EVP_md5 }, + { 65, EVP_sha1 }, + { 671, EVP_sha224 }, + { 668, EVP_sha256 }, + { 669, EVP_sha384 }, + { 670, EVP_sha512 }, +}; + +const EVP_MD* EVP_get_digestbynid(int nid) { + unsigned i; + + for (i = 0; i < sizeof(nid_to_digest_mapping) / sizeof(struct nid_to_digest); + i++) { + if (nid_to_digest_mapping[i].nid == nid) { + return nid_to_digest_mapping[i].md_func(); + } + } + + return + ((void *)0) + ; +} + +const EVP_MD* EVP_get_digestbyobj(const ASN1_OBJECT *obj) { + return EVP_get_digestbynid(OBJ_obj2nid(obj)); +} diff --git a/test/export/issue216.c b/test/export/issue216.c new file mode 100644 index 00000000..796b69b4 --- /dev/null +++ b/test/export/issue216.c @@ -0,0 +1,5 @@ +#include + +struct list {unsigned head; struct list *tail;}; +struct list three[] = { {1, three+1}, {2, three+2}, {3, NULL} }; +int f(int x) { return x;} diff --git a/test/export/issue319.c b/test/export/issue319.c new file mode 100644 index 00000000..be9f3f7e --- /dev/null +++ b/test/export/issue319.c @@ -0,0 +1,12 @@ +/* Dollar signs in identifiers */ + +int c$d = 42; + +int a$b(int x$$) { + return c$d + x$$; +} + +int main(int argc, const char *argv[]) +{ + return a$b(6); +} -- cgit From 9d1867bfa7814b3eb0a017638d79fc694289ba61 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Sep 2021 18:31:32 +0200 Subject: add union passing --- test/regression/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test') diff --git a/test/regression/Makefile b/test/regression/Makefile index 9661a99e..c56532ff 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -18,7 +18,7 @@ TESTS?=int32 int64 floats floats-basics floats-lit \ funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 for2 switch switch2 compound \ decl1 bitfields9 ptrs3 \ - parsing krfun ifconv + parsing krfun ifconv union_passing # Can run, but only in compiled mode, and have reference output in Results -- cgit From 2a0096bc0c6057577f10d6343063d9eca76cbdea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 23 Sep 2021 18:31:55 +0200 Subject: union passing --- test/regression/union_passing.c | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test/regression/union_passing.c (limited to 'test') diff --git a/test/regression/union_passing.c b/test/regression/union_passing.c new file mode 100644 index 00000000..b0ce6319 --- /dev/null +++ b/test/regression/union_passing.c @@ -0,0 +1,23 @@ +#include +#include +static int32_t bk; +union ba { + int64_t bb; +}; +static void dada(union ba); +void nothing(void); +void stuff(void) { + union ba f = {5}; + int32_t i[1000]; + nothing(); + dada(f); +} +static void dada(union ba k) { + bk = k.bb; +} +void nothing(void) { +} +int main() { + stuff(); + printf("result = %d\n", bk); +} -- cgit