aboutsummaryrefslogtreecommitdiffstats
path: root/test/regression
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/csmith' into towards_3.10David Monniaux2021-09-242-1/+24
|\
| * Merge branch 'csmith' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵David Monniaux2021-09-234-1/+351
| |\ | | | | | | | | | into csmith
| * | union passingDavid Monniaux2021-09-231-0/+23
| | |
| * | add union passingDavid Monniaux2021-09-231-1/+1
| | |
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-247-31/+96
|\ \ \ | |_|/ |/| |
| * | Native support for bit fields (#400)Xavier Leroy2021-08-227-31/+96
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
* | | csmith | creduce breaks on RISC-V 64David Monniaux2021-09-221-0/+36
| | |
* | | test for many parametersDavid Monniaux2021-09-173-1/+315
| |/ |/|
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-013-1/+24
| | | | | | | | cfrontend/C2C.ml
* | Updating varargs2 results for kvxCyril SIX2021-06-011-0/+1
| |
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-236-417/+18
|\| | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Remove regression/interop1 testXavier Leroy2021-01-184-417/+1
| | | | | | | | Now subsumed by the tests in abi/
| * 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
* | Fixing test/regression for KVXv3.8_kvxCyril SIX2020-12-072-0/+393
| |
* | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-0/+2
|\ \ | | | | | | | | | | | | | | | Conflicts: Makefile configure
| * | trace quand le simulateur est appeleSylvain Boulmé2020-07-241-1/+1
| | |
| * | Temporary prepass flags in test/regressionCyril SIX2020-07-241-0/+2
| | |
* | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-1813-112/+455
|\ \ \ | |/ / |/| / | |/
| * 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*
* | rename result fileDavid Monniaux2020-05-291-0/+0
| |
* | tests for kvxDavid Monniaux2020-05-261-0/+0
| |
* | k1c -> kvx changesDavid Monniaux2020-05-263-5/+5
| |
* | Fixing packedstruct issuev3.7_mppa_2020-04-01Cyril SIX2020-04-012-15/+15
| |
* | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-012-39/+838
|\|
| * 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.
* | disable some testsDavid Monniaux2020-03-271-4/+4
| |
* | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-036-24/+131
|\ \ | |/ |/| | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-168-27/+638
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | Removing NaNs from TESTS_DIFF (float precision issues..)Cyril SIX2019-09-251-0/+3
| | |
| * | varargs2 now work correctly (bis)Cyril SIX2019-09-252-3/+15
| | |
| * | Stub for builtins-mppa_k1c.cCyril SIX2019-09-251-0/+72
| | |
| * | varargs2 now work correctlyCyril SIX2019-09-251-0/+11
| | |
| * | Removing packed structs tests (do not work for now)Cyril SIX2019-09-251-0/+2
| | |
| * | More work on test, regression/packedstruct1.c and regression/varargs2.c ↵Cyril SIX2019-09-203-23/+28
| | | | | | | | | | | | don't pass
| * | __builtin_bswap16, 32 and 64Cyril SIX2019-09-201-2/+2
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-196-28/+61
| |\ \ | | | | | | | | | | | | mppa-work-upstream-merge
| * \ \ Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-033-1/+156
| |\ \ \ | | | | | | | | | | | | | | | mppa-if-conversion
| | * | | If-conversion optimizationXavier Leroy2019-05-313-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.
| * | | | Disabling the packedstruct tests from test/regressionCyril SIX2019-04-091-1/+2
| | | | |
| * | | | All CompCert tests can be compiledCyril SIX2019-04-092-2/+2
| |/ / /
* | | / Add interoperability test for functions returning small integer typesXavier Leroy2020-02-212-0/+23
| |_|/ |/| |
* | | 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-072-21/+5
| |/ |/|
* | 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.
generated by cgit (git 2.34.1) at 2024-05-20 08:27:44 +0000