aboutsummaryrefslogtreecommitdiffstats
path: root/test/regression/Results
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-242-14/+18
|\
| * Native support for bit fields (#400)Xavier Leroy2021-08-222-14/+18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-191-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | 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>
* | test for many parametersDavid Monniaux2021-09-171-0/+1
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-0/+1
| | | | | | | | 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-232-98/+1
|\| | | | | | | | | | | | | | | | | 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-181-98/+0
| | | | | | | | Now subsumed by the tests in abi/
| * RISC-V: fix FP calling conventionsXavier Leroy2021-01-141-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-101-0/+1
| | | | | | | | | | | | | | | | | | 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-071-0/+391
| |
* | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-186-40/+393
|\|
| * Add test for __builtin_sqrt and __builtin_fabsfXavier Leroy2020-07-271-0/+3
| |
| * Refactor regression testing of built-in functionsXavier Leroy2020-07-276-40/+390
| | | | | | | | | | | | 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
| |
* | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-011-38/+836
|\|
| * Add a test for int64 -> float32 conversionXavier Leroy2020-03-301-38/+836
| | | | | | | | | | This is a special value that causes double rounding with the naive conversion schema int64 -> float64 -> float32.
* | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-031-0/+11
|\ \ | |/ |/| | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-0/+17
| |\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | varargs2 now work correctlyCyril SIX2019-09-251-0/+11
| | |
| * | If-conversion optimizationXavier Leroy2019-05-311-0/+26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Add interoperability test for functions returning small integer typesXavier Leroy2020-02-211-0/+8
| |/ |/|
* | Test for the compilation of floating-point literalsXavier Leroy2019-08-081-0/+2
| | | | | | | | With special emphasis on the use of the AArch64 fmov #imm instruction.
* | AArch64 portXavier Leroy2019-08-081-0/+15
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | If-conversion optimizationXavier Leroy2019-06-061-0/+26
|/ | | | | | | | | | | | | | | | | | | | 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.
* Revised attachment of name attributes to structs, unions, enumsXavier Leroy2019-02-251-0/+1
| | | | | | | | | | | | | | | | | | 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-251-0/+11
| | | | Expected results were obtained with GCC 5.4 and Clang 8.0
* Attach _Alignas to names and refactor _Alignas checks (#133)Bernhard Schommer2018-09-101-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * 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.
* Issue with packed structs and sizeof, alignof, offsetof in cparser/Xavier Leroy2018-08-172-0/+24
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Remove the `_Alignas(expr)` construct (#125)Xavier Leroy2018-06-071-9/+9
| | | | The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
* Initialization of union bit fieldsXavier Leroy2018-04-251-0/+8
| | | | | | | | | | | 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-301-1/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-131-0/+1
|
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+2
| | | | | | | | - 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-061-0/+5
| | | | | | 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-281-0/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-0/+0
| | | | | | | | | | | | -> 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-241-0/+1
|
* Update the tests and test infrastructure in test/regressionXavier Leroy2016-10-246-0/+58
| | | | | 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-041-0/+2160
| | | | | | 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.
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-083-0/+4
| | | | | | | | | | | | | | Here are two examples that cause an internal error in Asmexpand.ml: volatile long long x; void f(unsigned int i) { x = i; } unsigned g(unsigned i) { return __builtin_clzll(i); } The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle. The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot. Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
* Revised handling of old-style, K&R function definitionsXavier Leroy2016-06-241-0/+3
| | | | | | | | This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in float f (x) float x; { return x; } "x" is passed with type "double", and must be converted to "float" at the beginning of the function.
* Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-223-2/+10
| | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/
* Issue #71: incorrect initialization of wchar_t arrays from wide string literalXavier Leroy2015-11-131-0/+3
| | | | Regression test added in regression/initializers.c
* Merge remote-tracking branch 'origin/master' into parser_fixJacques-Henri Jourdan2015-11-042-0/+3
|\
| * Merge branch 'ppc64' of ssh://github.com/AbsInt/CompCert into ppc64Xavier Leroy2015-10-111-0/+2
| |\
| | * Test __builtin_isel.Xavier Leroy2015-09-131-0/+2
| | |
* | | Better handling of old-style K&R function declarations:Jacques-Henri Jourdan2015-11-011-0/+10
|/ / | | | | | | | | | | - Added a Cabs.PROTO_OLD constructor to Cabs.decl_type - Refactored the Parser.vy and pre_parser.mly grammars - Rewritten the conversion of old function definitions to new-style
* / Fixed a few bugs in the pre parser. In particular, the following codeJacques-Henri Jourdan2015-09-301-0/+0
|/ | | | | | | | | | | | | | | was not parsed correctly: typedef int a; int f() { for(int a; ;) if(1); a * x; } Additionnaly, I tried to add some comments in the pre-parser code, especially for the different hacks used to solve various conflicts.
* More tests for alias analysis.Xavier Leroy2015-07-201-0/+1
|
generated by cgit (git 2.34.1) at 2024-06-13 11:59:37 +0000