aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Update verilog back end with new x86 changesHEADmasterYann Herklotz2023-04-2721-165/+475
|
* Fix compilation of verilog back endYann Herklotz2023-04-272-102/+77
|
* Replace omega by liaYann Herklotz2023-04-277-52/+57
|
* Fix dune file as wellYann Herklotz2023-04-271-1/+1
|
* Add proof of splitlong_ptr32Yann Herklotz2023-04-271-0/+3
|
* Add Verilog backendYann Herklotz2023-04-2733-0/+16929
|
* Always try inlining functionsYann Herklotz2023-04-271-4/+1
|
* Ignore unnecessary foldersYann Herklotz2023-04-272-1/+1
|
* Fix a comment in Cstrategy.v (#485)Xuyang Li2023-04-051-2/+2
|
* Use a shorter insruction on x86 for loading unsigned 32-bit immediates into ↵Valoran2023-04-051-1/+3
| | | | | | | | | | | | | | | 64-bit registers.(#487) Writing into a 32-bit register erases the upper 32 bits of a 64-bit register. This is the shortest instruction for loading unsigned 32-bit immediates. The length of those instructions is: - movl: 5 bytes - movq: 7 bytes - movabsq: 10 bytes Some assemblers will choose the proper instruction by themselves; the GNU assembler does not, apparently. So it's better to make the choice of instruction explicit.
* Support Coq 8.16.0 and 8.16.1 in configure scriptXavier Leroy2023-03-101-2/+2
|
* Update warning flags used to compile Flocq and MenhirlibXavier Leroy2023-03-101-2/+5
| | | | | | | | We prefer not to change these two "vendored" libraries. Deprecation warnings can only be addressed upstream. So let's silence them. Flocq no longer triggers the `compatibility-notation` warning, so let's not silence it.
* Upgrade Flocq to 4.1.1Xavier Leroy2023-03-103-15/+15
|
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-105-13/+18
| | | | | | | | | | | | | | | * Define our own `Z_div_mod_eq` lemma The one in the Coq standard library is deprecated since 8.14, but its replacement changed type between 8.13 and 8.14. So the only way to remain compatible from 8.12 to 8.16 is to define our own lemma. Phew. * Do not use `Arith.Max`, deprecated. * Do not use `plus_lt_compat_r`, deprecated. * Do not use `beq_nat_refl` and `beq_nat_true`, deprecated.
* Include `+unix` and `+str` for OCaml 5 compatibilityXavier Leroy2023-03-061-1/+3
| | | | | | | In OCaml 5, the Unix and Str libraries are installed in subdirectories of the standard library directory. In OCaml 4, the `-I +str` and `-I +unix` options have no effect.
* Change preference for new register in allocatorBernhard Schommer2023-03-067-29/+129
| | | | | | | | | | | | Currently, the register allocator picks caller-save registers in preference to callee-save registers. But for ARM in Thumb mode, more compact code is obtained if we prefer integer registers R0...R3 rather than all integer caller-save registers. This commit introduces an `allocatable_registers` function in $ARCH/Conventions1.v that determines the preferred and remaining registers to be used for register allocation.
* configure: add -ignore-ocaml-version optionXavier Leroy2023-03-051-8/+11
| | | | | | Also: produce better "unsupported" message for OCaml 5. Fixes: #477
* Fix Thumb handling of `add reg, sp, #imm` and `sub reg, sp, #imm`Xavier Leroy2023-02-201-3/+4
| | | | | Don't add `s` suffix if source register is R13 (SP), so as to enable 16-bit instruction encodings.
* Move the old `offset_in_range` function inside `memcpy_small_arg`Bernhard Schommer2023-02-201-3/+2
| | | | It is no longer used elsewhere.
* For Thumb, use `movs` for loading immediate constantsBernhard Schommer2023-02-201-2/+2
| | | | It is supported and produces shorter code than `mov`.
* Use more functions from Asmgen in Asmexpand.Bernhard Schommer2023-02-201-17/+4
|
* Use the Asmgen offset check for volatile load/store.Bernhard Schommer2023-02-201-4/+20
| | | | | The old offset check is too conservative allowing only offsets that are allowed for all kinds of load/store instructions.
* ARM code generation: fix offset checks for loadsBernhard Schommer2023-02-201-3/+3
| | | | | | | | The check `Int.ltu x Int.zero` is always false, we replace this by using signed integer comparisons. We cannot use `Int.sign_ext` because the offsets are not signed integers but rather unsigned integers plus an additional sign bit.
* Remove unused definitionBernhard Schommer2023-02-201-4/+0
| | | | Closes: #467
* When installing the Coq development, also install coq-native generated filesXavier Leroy2023-02-201-1/+6
| | | | | | | | If the Coq version used supports native compilation, `.coq-native` directories are generated during the build, and they need to be installed along the `.vo` files. Fixes: #476
* Ignore self assign in if-conversionBernhard Schommer2023-02-202-4/+19
| | | | | | | | A self assign `x = x` can be classified as a skip in `classify_stmt`. This helps with the if-conversion of some code that the previous passes generates, e.g. for nested C conditional expressions. Closes: #466
* RISC-V: print flt.s, feq.s, fle.s with a tab after the mnemonic (#481)David Monniaux2023-02-071-3/+3
|
* wchar_t is unsigned int for arm_littleendian, arm_bigendian and aarch64Bernhard Schommer2023-02-011-2/+7
| | | | | | However, it is signed int for aarch64_apple. Fixes: #475
* Use define for wchar_t typeBernhard Schommer2023-02-012-6/+11
| | | | | | Since the wchar_t type depends on the architecture and the system we are compiling for we replace the typedef to a fixed type by a typedef to a define which is predefined by the compiler itself.
* Export `name_of_ikind` and `name_of_fkind`Xavier Leroy2023-02-011-0/+3
|
* Introduce `wchar_ikind` in machine descriptionsXavier Leroy2023-01-244-20/+12
| | | | | | This replaces `sizeof_wchar` and `wchar_signed`, and makes it possible to request that `wchar_t` is `long` instead of `int`, something that seems needed for PowerPC.
* Don't discard argument of `__builtin_va_end`Michael Schmidt2023-01-231-2/+2
| | | | | | Instead, evaluate it for the side effects it may contain. Fixes: #474
* Disable tail calls in variadic functionsMichael Schmidt2023-01-232-5/+6
| | | | | | | | | Variadic functions can use the stack frame to store values of registers. Hence, a pointer within the stack frame can be put in a va_list, and the stack frame should not be deallocated before a function call that may use this va_list. Fixes: #473
* Elaboration of compound initializers: reverse list of generated global variablesMichael Schmidt2023-01-231-1/+1
| | | | | | So as to respect dependency order when compound initializers are nested. Fixes: #471
* C2C: wrong handling of typedefs to enums in bit fieldsXavier Leroy2023-01-231-1/+1
| | | | Fixes: #472
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-225-7/+7
| | | | Adapt w.r.t. coq/coq#16904.
* Remove support for 32-bit CygwinXavier Leroy2022-12-082-23/+7
| | | | | Cygwin 32 bits has reached end of life, and Cygwin >= 3.4 will be 64-bit only. (https://cygwin.com/pipermail/cygwin-announce/2022-November/010777.html)
* Update doc commentXavier Leroy2022-12-081-2/+2
|
* Fix incomplete checking of unsolved holes (#465)Gaëtan Gilbert2022-11-281-1/+1
| | | | Adaptation to https://github.com/coq/coq/pull/16743
* Updates for release 3.12Xavier Leroy2022-11-213-3/+54
|
* Emit the Tag_ABI_VFP attribute appropriate to the calling conventions usedXavier Leroy2022-11-211-1/+6
| | | | Fixes: #461
* configure: add option -sharedir to specify where to put compcert.ini (#460)Xavier Leroy2022-11-141-5/+32
| | | | | | Make sure that it's one of the three locations where the ccomp executable looks for compcert.ini. Closes: #450
* 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-0913-142/+500
|\ | | | | Handle Duff's device and other unstructured `switch` statements
| * Ignore debug statements before the first case of a `switch`Xavier Leroy2022-11-031-1/+7
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This can occur in debug mode if there are declarations before the first case, as in ``` switch (x) { int x; case 0: ... } ``` Without this commit, the code above is a structured switch if -g is not given, and a non-structured switch if -g is given. Co-authored-by: Michael Schmidt <github@mschmidt.me>
| * Update man-page for `-funstructured-switch` (also for new `-std` option, ↵Michael Schmidt2022-11-031-4/+22
| | | | | | | | `-finput-charset` and other small fixes)
| * Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-2912-98/+439
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - 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).
| * Unblock: never put debug info before a labelXavier Leroy2022-10-291-11/+12
| | | | | | | | | | | | | | This ensures that normalized switch statements remain normalized. However, if the label and the labeled statement are on different lines, add an extra line directive corresponding to the label before the labeled statement.
| * Revised passing of options to `Parse.preprocessed_file`Xavier Leroy2022-09-273-41/+33
| | | | | | | | | | | | Instead of passing a string that encodes the optional source-to-source transformations to perform, just pass one optional, named argument for each transformation. It is clearer and easier to extend this way.
* | Replace CR, FF and VT with whitespace.Bernhard Schommer2022-11-051-3/+5
| | | | | | | | | | | | | | | | We use Printlines to copy C code fragments to assembly comments. While CR, FF and VT are treated like whitespace by C, they could possibly mess up the assembly comments if copied verbatim. Moreover, this avoids generating CR CR LF end-of-lines under Windows. Bug 34075
generated by cgit (git 2.34.1) at 2024-04-27 12:36:28 +0000