aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Wrong test for coroutined decompressorXavier Leroy2022-11-141-1/+1
| | | | | | | Use of `char` instead of `int` caused nontermination on platforms where `char` is unsigned. Fixes: #462
* Merge pull request #459 from AbsInt/full-switchXavier Leroy2022-11-093-1/+193
|\ | | | | Handle Duff's device and other unstructured `switch` statements
| * Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-293-1/+193
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - New elaboration pass: SwitchNorm - recognizes structured 'switch' statements and puts them in a normalized form; - if selected, transforms unstructured 'switch' statements into a structured switch with goto actions + the original switch body with appropriate labels and gotos. - C2C treatment of 'switch' statements is simplified accordingly. - New language support option `-funstructured-switch`. - Some tests were added (test/regression/switch3.c).
* | Add test for nested conditional, &&, || expressionsXavier Leroy2022-10-013-1/+55
|/
* test/export: use the standard headers from ../../runtime/includeXavier Leroy2022-09-231-1/+1
| | | | Just like in the other test/ directories.
* Temporary: don't run the regression/stringlit and regression/charlit testsXavier Leroy2022-09-191-1/+3
| | | | | Some versions of the glibc standard header `<uchar.h>` are not compatible with CompCert, causing the tests to fail on our CI.
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-195-1/+134
| | | | | | | | | | | | | | | | | * Support C11 Unicode string literals and character constants * Add tests for C11 string literals and character constants * Better error message for ill-formed universal character names E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits. * Add new warning `invalid-utf8` for byte sequences that are not valid UTF8. The warning is activated but not fatal by default. * Warn on uses of C11 Unicode character constants and string literals This uses the `c11-extensions` warning, which is off by default. * Support preprocessing option -finput-charset= for GNU toolchains
* In test/regression: Use `static inline` instead of `inline`Xavier Leroy2022-07-052-5/+5
| | | | Fixes: #441
* Some tests for _GenericXavier Leroy2022-05-133-1/+115
|
* Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-2210-11/+23
| | | | | | | | | 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.
* Refactor clightgenXavier Leroy2021-09-221-1/+1
| | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
* clightgen: handle empty names given to padding bit fieldsXavier Leroy2021-09-151-0/+13
| | | | | | | | | | | | 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 `_`.
* Native support for bit fields (#400)Xavier Leroy2021-08-2213-34/+431
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* 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.
generated by cgit (git 2.34.1) at 2024-06-02 15:19:15 +0000