aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Adding the new benches to benches.shCyril SIX2019-11-221-1/+1
|
* benchmarks += ocamlCyril SIX2019-11-221-30/+3
|
* Fixing zlibCyril SIX2019-11-193-0/+541
|
* Adding zlibCyril SIX2019-11-151-49/+57
|
* Adding jpeg-6b benchmarkCyril SIX2019-11-152-32/+50
|
* Correcting typo in rules.mkCyril SIX2019-11-131-1/+1
|
* Putting back the building rules for the paper (rules.mk)Cyril SIX2019-11-131-11/+11
|
* Removing clutter from building + running benchesCyril SIX2019-11-134-7/+21
|
* Scaling down forgotten tests -> test/c/ operationalCyril SIX2019-10-227-3/+27
|
* Adding MPPA endianess in test/endian.hCyril SIX2019-10-211-1/+1
|
* [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-1614-48/+658
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * 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
| |
* | genann addedCyril SIX2019-10-023-3/+5
| |
* | Adding picosat to the benchesCyril SIX2019-10-022-34/+8
| |
* | Updating test/monniaux/README.mdCyril SIX2019-10-021-1/+8
| |
* | (forgot to add glpk to benches.sh)Cyril SIX2019-10-021-1/+1
| |
* | Intégration de GLPKCyril SIX2019-10-022-37/+7
| |
* | Restored previous input sizes for other backendsCyril SIX2019-09-2553-60/+330
| |
* | Preferring the (ifeq) approach for removing testsCyril SIX2019-09-251-0/+4
| |
* | 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-204-24/+33
| | | | | | | | don't pass
* | __builtin_bswap16, 32 and 64Cyril SIX2019-09-201-2/+2
| |
* | Desactivating CompCert tests taking too longCyril SIX2019-09-191-1/+3
| |
* | Adding some function calls in interop testsCyril SIX2019-09-192-7/+15
| |
* | Adding back "exit 2" to the test target of test/c/MakefileCyril SIX2019-09-131-2/+2
| |
* | Scaling down compression testsCyril SIX2019-09-131-5/+11
| |
* | Reducing further the input size of the testsCyril SIX2019-09-1330-71/+68
| |
* | Scaling down most of c/ CompCert testsCyril SIX2019-09-1318-37/+56
| |
* | Starting to modify official CompCert tests to be passable with the simuCyril SIX2019-09-1018-89/+81
| |
* | Test for compd.geuCyril SIX2019-09-051-0/+6
| |
* | Removing unused .all, .any, .nall and .none conditionsCyril SIX2019-09-051-1/+1
| |
* | Adding tests for cmovedCyril SIX2019-09-052-0/+85
| |
* | aclrw testCyril SIX2019-09-031-0/+12
| |
* | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-workCyril SIX2019-09-0310-100/+75
|\ \ | | | | | | | | | | | | | | | | | | Conflicts: configure mppa_k1c/Archi.v mppa_k1c/Asmexpand.ml
| * | macros for fma() fmaf()David Monniaux2019-08-301-0/+1
| | |
| * | fma with first negated operandDavid Monniaux2019-08-301-0/+1
| | |
| * | fmaDavid Monniaux2019-08-301-0/+12
| | |
| * | merge upstream including fma fixesDavid Monniaux2019-08-283-72/+0
| | |
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-196-28/+61
| |\| | | | | | | | | | mppa-work-upstream-merge
| | * 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.
generated by cgit (git 2.34.1) at 2024-07-12 04:29:44 +0000