aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* MPPA - Oshrximm + Mgetparam + FP is GPR10 + bugCyril SIX2018-04-201-17/+17
| | | | | | | | | | | Added Oshrximm and Mgetparam -> mmult.c divide & conqueer generates FP is now GPR10 instead of being a mix of GPR30 and GPR32 Corrected a bug where Pgoto and Pj_l were given the same interpretation, where in fact there's a fundamental difference : Pgoto is supposed to have a function name (symbol), while Pj_l is supposed to have a label name (print_label). This led to having undefinite labels in the code.
* MPPA - Added divide & conqueer test matmulCyril SIX2018-04-182-2/+87
|
* MPPA - added Oaddrsymbol -> now able to run the matrix mult testCyril SIX2018-04-183-37/+42
|
* MPPA - added a Matrix Multiply testCyril SIX2018-04-183-0/+140
|
* MPPA - Added Pmull -> now able to run the sort testCyril SIX2018-04-173-3/+8
|
* MPPA - More shiftsCyril SIX2018-04-171-1/+3
|
* MPPA - Forgot to uncomment debugging section of prng testCyril SIX2018-04-171-4/+2
|
* MPPA - added all shiftsCyril SIX2018-04-174-0/+12
|
* MPPA - Added CompCert testsCyril SIX2018-04-171-1/+16
|
* MPPA - added merge sort + corrected bug in insertion + testing them togetherCyril SIX2018-04-1710-38/+205
|
* MPPA - tests - added insertion sort and selection sortCyril SIX2018-04-175-0/+159
|
* MPPA - changed UNIT_TEST namesCyril SIX2018-04-172-4/+4
|
* MPPA - Added uint64_t types to the tests + k1c testCyril SIX2018-04-174-11/+34
|
* MPPA - added PRNG generator in the testsCyril SIX2018-04-163-0/+66
|
* MPPA - Automatic generation of expected value for testsCyril SIX2018-04-1118-10/+32
|
* MPPA - reorganized the test directoryCyril SIX2018-04-112-13/+18
|
* MPPA - Onegl + PneglCyril SIX2018-04-102-7/+3
|
* MPPA - Running tests in parallelCyril SIX2018-04-102-26/+41
|
* MPPA - fixed wrong extension in test filesCyril SIX2018-04-102-0/+0
|
* MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-095-1/+27
|
* MPPA - forgot check.sh in last commitCyril SIX2018-04-051-0/+29
|
* MPPA - Added regression testsCyril SIX2018-04-0513-14/+27
|
* MPPA - added test forvarl.cCyril SIX2018-04-042-1/+12
|
* MPPA - Added non immediate comparisonCyril SIX2018-04-042-2/+14
|
* MPPA - Added signed immediate comparisonCyril SIX2018-04-042-1/+13
|
* MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-042-2/+14
|
* MPPA - Added Msetstack + bunch of store --> on a des call !Cyril SIX2018-04-042-1/+17
|
* MPPA - code cleaningCyril SIX2018-04-041-1/+1
|
* MPPA - The project compiles.Cyril SIX2018-04-042-0/+32
| | | | | | | | | | | | | Supports very simple programs that load integer immediates. It starts the main, loads integer in registers, and return correctly. Addition in Mach not yet supported, but should not be hard to add them. Function calls are not yet supported. The ABI for now is the same as the RiscV, with a small twist: $ra is first loaded in a user register, then this user register is pushed (instead of pushing $ra straight away).
* 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.
* RISC-V port and assorted changesXavier Leroy2017-04-2814-14/+66
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Remove tests involving Cminor concrete syntax. Update ChangelogXavier Leroy2017-02-1528-3336/+0
| | | | Follow-up to [29653ba]
* Revised elaboration of attributesXavier Leroy2017-01-311-1/+1
| | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-273-10/+4
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* Update the tests in test/regression, continuedXavier Leroy2016-10-242-13/+5
|
* Update the tests and test infrastructure in test/regressionXavier Leroy2016-10-2412-7/+132
| | | | | Tests updated to work with x86 64 bits. Infrastructure added: script "Runtest", with ability to have different reference outputs depending on platform or bit size.
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-042-0/+2172
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-5/+5
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-056-15/+15
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* test/raytracer: use our own strdup(), since this is not a standard functionXavier Leroy2016-07-241-1/+9
|
generated by cgit (git 2.34.1) at 2024-07-12 04:06:42 +0000