aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Elab bitfields: check size of type <=32bit rather than checking rank (#387)Amos Robinson2021-04-193-1/+24
| | | | | | | | | | | | When desugaring a bitfield, allow any integral type that is 32 bits or smaller. Previously this was checking the rank of the type rather than the size. This rank check caused issues with standard headers that declare `uint32_t` to be an `unsigned long` rather than an `unsigned int`. Here, any bitfields declared as `uint32_t` were failing to compile even though they are still actually 32 bits. Co-authored-by: Amos Robinson <amos@gh.st>
* "macosx" is now called "macos"Xavier Leroy2021-01-181-1/+1
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* Remove regression/interop1 testXavier Leroy2021-01-184-417/+1
| | | | Now subsumed by the tests in abi/
* Testing calling conventions and interoperability with another C compilerXavier Leroy2021-01-185-1/+583
| | | | Using a combination of fixed and randomly-generated function signatures.
* RISC-V: fix FP calling conventionsXavier Leroy2021-01-142-5/+5
| | | | | | | | | | | | | | | | | | | | | | | This is a follow-up to e81d015e3. In the RISC-V ABI, FP arguments to functions are passed in integer registers (or pairs of integer registers) in two cases: 1- the FP argument is a variadic argument 2- the FP argument is a fixed argument but all 8 FP registers reserved for parameter passing have been used already. The previous implementation handled only case 1, with some problems. This commit implements both 1 and 2. To this end, 8 extra FP caller-save registers are used to hold the values of the FP arguments that must be passed in integer registers. Fixup code moves these FP registers to integer registers / register pairs. Symmetrically, at function entry, the integer registers / register pairs are moved back to the FP registers. 8 extra FP registers is enough because there are only 8 integer registers used for parameter passing, so at most 8 FP arguments may need to be moved to integer registers.
* RISC-V: wrong fixup code generated for vararg calls with fixed FP argsXavier Leroy2021-01-102-0/+17
| | | | | | | | | This is a follow-up to 2076a3bb3. Integer registers were wrongly reserved for fixed FP arguments, causing variadic FP arguments to end up in the wrong integer registers. Added regression test in test/regression/varargs2.c
* Better "make clean"Xavier Leroy2020-11-011-1/+1
|
* Test clightgen with -short-idents and -normalize optionsXavier Leroy2020-09-221-0/+6
| | | | Use different combination of options for different test files.
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+6
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Add test for __builtin_sqrt and __builtin_fabsfXavier Leroy2020-07-272-0/+7
|
* Refactor regression testing of built-in functionsXavier Leroy2020-07-2713-110/+447
| | | | | | Share the testing code for built-in functions that are available on all target platforms. Improve testing of __builtin_clz* and __builtin_ctz*
* Improve portability of the test for annotations inclightgenXavier Leroy2020-06-052-0/+4
| | | | __builtin_ais_annot is not supported for macOS nor for Cygwin.
* clightgen: fix the printing of annotationsXavier Leroy2020-06-051-0/+6
| | | | | | | | | | | | The printing of EF_annot and EF_annot_val was missing the extra "kind" parameter introduced in commit 6a010b4. Also: the automatic translation of annotations into Coq assertions was confusing and prevented other uses of __builtin_annot statements in conjunction with clightgen. I believe it was never used. This commit removes this translation. Closes: #360
* Add a test for int64 -> float32 conversionXavier Leroy2020-03-302-39/+838
| | | | | This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32.
* Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
|
* clightgen: sanitize names of functions and global variablesXavier Leroy2019-10-281-0/+12
| | | | | A "dollar" sign in a function name or a global variable name was producing incorrect Coq identifiers. (Issue #319.)
* Revise the "bench" entries of the test suiteXavier Leroy2019-09-174-12/+9
| | | | | | | | Initially, the "bench" entries of the test suite used a "xtime" utility developed in-house and not publically available. This commit adds a version of "xtime" written in OCaml (tools/xtime.ml) and updates the "bench" entries of the test/*/Makefile to use it.
* Test for the compilation of floating-point literalsXavier Leroy2019-08-083-1/+562
| | | | With special emphasis on the use of the AArch64 fmov #imm instruction.
* AArch64 portXavier Leroy2019-08-083-5/+70
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Factor out endianness determination between testsXavier Leroy2019-08-074-30/+14
|
* When testing builtin functions, prevent constant propagationXavier Leroy2019-07-174-28/+31
| | | | | | | | | | Now that some builtin functions have known semantics, constant propagation can happen in this test. This defeats the purpose, which is to check that the correct processor instructions are generated. To prevent this constant propagation, we move the initialized variables to global scope. Since they are not "const", their values are not known to the optimizer.
* Extended asm: print register names according to their typesXavier Leroy2019-06-171-0/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When printing an extended asm code fragment, placeholders %n are replaced by register names. Currently we ignore the fact that some assemblers use different register names depending on the width of the data that resides in the register. For example, x86_64 uses %rax for a 64-bit quantity and %eax for a 32-bit quantity, but CompCert always prints %rax in extended asm statements. This is problematic if we want to use 32-bit integer instructions in extended asm, e.g. int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); produces addl %rax, %rdx which is syntactically incorrect. Another example is ARM FP registers: D0 is a double-precision float, but S0 is a single-precision float. This commit partially solves this issue by taking into account the Cminor type of the asm parameter when printing the corresponding register. Continuing the previous example, int x, y; asm("addl %1, %0", "=r"(x), "r"(y)); now produces addl %eax, %edx This is not perfect yet: we use Cminor types, because this is all we have at hand, and not source C types, hence "char" and "short" parameters are still printed like "int" parameters, which is not good for x86. (I.e. we produce %eax where GCC might have produced %al or %ax.) We'll leave this issue open.
* Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-171-0/+20
| | | | | A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction.
* If-conversion optimizationXavier Leroy2019-06-063-1/+156
| | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches.
* Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-3/+3
| | | | | | This is a manual, partial merge of Github pull request #296 by @Fourchaux. flocq/, cparser/MenhirLib/ and parts of test/ have not been changed because these are local copies and the fixes should be performed upstream.
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-252-0/+8
| | | | | | | | | | | | | | | | | | Consider: ``` struct s { ... } __attribute((aligned(N))); struct t { ... } __attribute((aligned(N))) struct t x; ``` In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned. In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning. This commit changes the attachment rule so that it treats both cases right. Extend regression test for "aligned" attribute accordingly, by testing aligned attribute applied to a name of struct type.
* Add regression test for "aligned" attributeXavier Leroy2019-02-253-1/+120
| | | | Expected results were obtained with GCC 5.4 and Clang 8.0
* Test for NULL in variable argument listsXavier Leroy2019-02-042-1/+53
| | | | | Sometimes a vararg function receives a NULL-terminated list of pointers. This can fail if sizeof(NULL) < sizeof(void *), as this test illustrates.
* Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-102-6/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Refactor common code of alignas. Instead of working on attributes the function now works directly on the type since the check always performed an extraction of attributes from a type. Bug 23393 * Attach _Alignas to the name. Bug 23393 * Attach "aligned" attributes to names So that __attribute((aligned(N))) remains consistent with _Alignas(N). gcc and clang apply "aligned" attributes to names, with a special case for typedefs: typedef __attribute((aligned(16))) int int_al_16; int_al_16 * p; __attribute((aligned(16))) int * q; For gcc, p is naturally-aligned pointer to 16-aligned int and q is 16-aligned pointer to naturally-aligned int. For CompCert with this commit, both p and q are 16-aligned pointers to naturally-aligned int. * Resurrect the alignment test involving typedef The test was removed because it involved an _Alignas in a typedef, which is no longer supported. However the same effect can be achieved with an "aligned" attribute, which is still supported in typedef.
* Improve execution of regression testsXavier Leroy2018-08-244-16/+45
| | | | | | - Make it possible to skip tests on some platforms - Make it possible to expect a failure (typically: of the reference interpreter) - Stop on error
* Harden the extasm.c test, continuedXavier Leroy2018-08-202-5/+5
| | | | | Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2 ("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
* Harden the extasm.c testXavier Leroy2018-08-202-2/+7
| | | | | | | Pass more info from CompCert's configuration as #define on command line. Use this info to improve the "64 bit" detection in extasm.c. (Before it fails with powerpc-ppc64, which has 64-bit int regs but couldn't be detected with #ifdefs.)
* Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-173-6/+60
| | | | | | | | | | | | | | | | | | | | | | | | | | | CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field): - the reference implementation, in Coq, from cfrontend/Ctypes.v - the implementation used during elaboration, in OCaml, from cparser/Cutil.ml The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used. This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example: ``` struct __packed__(1) s { char c; short s; int i; }; assert (__builtin_offsetof(struct s, i) == 3); assert (sizeof(struct s) = sizeof(char[sizeof(struct s)])); ``` The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs. This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout. Related changes: * cparser/Cutil: add `packing_parameters` function to extract packing info from attributes * cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout * cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.) * cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)). * cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab * cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/. * test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
* Clean .foo.aux files created by coqcXavier Leroy2018-07-101-1/+1
|
* Remove the `_Alignas(expr)` construct (#125)Xavier Leroy2018-06-072-36/+32
| | | | The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
* Don't depend on ../../clightgenXavier Leroy2018-06-021-3/+3
| | | | | It's not really necessary, and under Windows it's really ../../clightgen.exe, which confuses make.
* Add tests for clightgenXavier Leroy2018-06-015-0/+985
| | | | Also: add "parallel" entry to test/Makefile for parallel execution of tests.
* Initialization of anonymous bit-fields in structsXavier Leroy2018-04-251-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | For anonymous bit-fields in structs, carrier fields may be introduced which are not initialized since no default initializer are generated earlier. This cause the translation in C2C to throw an error since too few initializers are available. Example: struct s2 { int : 10; int a; int : 10; char b; int : 10; short c; int : 10; } s2 = { 42, 'a', 43 }; To work around this issue we need to generate a default inializer for every new member that does not have a translated member. Based on P#80, with more efficient algorithms. Bug 23362
* Initialization of union bit fieldsXavier Leroy2018-04-252-0/+33
| | | | | | | | | | | Bit fields in unions were initialized like normal fields, causing mismatch on the name of the field. Also: added function Bitfields.carrier_field and refactored. Patch by Bernhard Schommer. Bug 23362
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-302-1/+6
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Consider: struct P { int x, y; } struct S { struct P p; } struct P p0 = { 1,2 }; struct S s1 = { .p = p0; .p.x = 3 }; ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e. the initialization of s1.p.y to p0.y implied by ".p = p0" is kept, even though the initialization of s1.p.x to p0.x is overwritten by ".p.x = 3". GCC, old versions of Clang, and previous versions of CompCert initialize s1.p.y to the default value 0. I.e. the initialization ".p = p0" is forgotten, leaving default values for the fields of .p before ".p.x = 3" takes effect. Implementing the proper ISO C99 semantics in CompCert is difficult, owing to a mismatch between the intended semantics and the C.init representation of initializers. This commit turns the delicate case of reinitialization above (re-initializing a member of a composite that has already been initialized as a whole) into a compile-time error. We will then see if the delicate case occurs in practice and needs further attention.
* Add regression test for issue #211Xavier Leroy2018-01-133-1/+17
|
* Typo in Makefile: "ia32" is now "x86"Xavier Leroy2017-09-191-1/+1
|
* test/*/Makefile: suppress dependencies on ../../ccompXavier Leroy2017-09-112-6/+6
| | | | | Not very useful in practice (make clean is generally done before make all) and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
* For running tests with the interpreter, use the correct -stdlib optionXavier Leroy2017-08-281-3/+2
| | | | Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
* test/compression: use unique temporary files for testingXavier Leroy2017-08-271-7/+7
|
* test/ : stop at first error in "make all"Xavier Leroy2017-08-261-1/+1
|
* test/: add a CCOMPOPTS make variable to pass additional compile-time flagsXavier Leroy2017-08-265-5/+5
| | | | E.g. "-Os" for testing in "optimize for size" mode, or "-mthumb" for testing ARM in Thumb2 mode.
* Reduce the running times of the tests in test/cXavier Leroy2017-08-2630-87/+75
| | | | Running times were too long when executed on low-end ARM or PowerPC hardware, or under QEMU emulation.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-062-2/+8
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-063-1/+35
| | | | | | This extension enables more addressing modes to be encoded as builtin arguments and used in conjunction with volatile memory accesses. Current status: x86 port only, the only new addressing mode handled is reg + offset.
generated by cgit (git 2.34.1) at 2024-06-29 01:09:09 +0000