aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
* | Use open_in_bin instead of open_in.Bernhard Schommer2022-11-051-1/+1
| | | | | | | | | | | | | | On platforms that do distinguish between text mode and binary mode, seek_in cannot reliably be used on files opened in text mode (open_in). The input file must therefore be opened in binary mode (open_in_bin). Bug 34075
* | Merge pull request #458 from AbsInt/simpl-expr-destsXavier Leroy2022-10-246-99/+220
|\ \ | | | | | | SimplExpr: revised handling of nested conditional, `||`, `&&` expressions
| * | Add test for nested conditional, &&, || expressionsXavier Leroy2022-10-013-1/+55
| | |
| * | SimplExpr: revised handling of nested conditional, `||`, `&&` operatorsXavier Leroy2022-10-013-98/+165
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a `For_set` destination, a temporary can be reused only if it always used with the same type. Otherwise, typing of Cminor code fails later in the compilation pipeline. This commit implements temporary reuse if and only if the typing constraint is respected. - For `&&` and `||`, it avoids the possibility of wrong reuse (as reported in #453). - For nested conditional expressions, it improves a bit the generated code by reusing the temporary when possible. Fixes: #453
* / Use .data.rel.ro section for const data with relocatable inits on ELF ↵Xavier Leroy2022-10-244-4/+16
|/ | | | | | | | | | | | | targets (#457) Follow-up to ed89275cb. AArch64, ARM, RISC-V and x86 ELF targets are changed. PowerPC / ELF is unchanged because we use the EABI variant, which has no `.data.rel.ro` section as far as I can see in GCC's output. (The SVR4 variant has `.data.rel.ro` but does not have `.sdata2`, which CompCert uses.) Fixes: #454
* test/export: use the standard headers from ../../runtime/includeXavier Leroy2022-09-231-1/+1
| | | | Just like in the other test/ directories.
* No need to set -std=c99 on the GNU C preprocessor command lineXavier Leroy2022-09-231-12/+12
| | | | The correct -std option is now added by ccomp itself.
* Support the `-std=<standard>` option (#456)Xavier Leroy2022-09-233-4/+24
| | | | | | | | | | | | | | It has two effects: - With a GNU toolchain, it's passed down to the preprocessor. This influences the contents of standard includes. - It determines the default effect of the "C11 feature" warning: -std=c99: warn on the use of C11 features -std=c11 or -std=c18: don't warn For backward compatiblity, the default, if no `-std` option is given, is to not warn, but to pass `-std=c99` to the preprocessor. Co-authored-by: Bernhard Schommer <bschommer@users.noreply.github.com>
* Add `Commandline.longopt` function for options of the form `-<key>=<arg>`Xavier Leroy2022-09-232-20/+18
| | | | | Also: use `int_of_string_opt` instead of `int_of_string` for slightly cleaner code.
* Improved help messages for the -g<n> and -gdwarf-<n> optionsXavier Leroy2022-09-231-3/+5
|
* Export the functions that control warningsXavier Leroy2022-09-231-0/+13
| | | | | Activation and deactivation of a given warning, plus set-as-error and remove-as-error.
* Temporary: don't run the regression/stringlit and regression/charlit testsXavier Leroy2022-09-191-1/+3
| | | | | Some versions of the glibc standard header `<uchar.h>` are not compatible with CompCert, causing the tests to fail on our CI.
* Support C11 Unicode string literals and character constants (#452)Xavier Leroy2022-09-1919-214/+490
| | | | | | | | | | | | | | | | | * Support C11 Unicode string literals and character constants * Add tests for C11 string literals and character constants * Better error message for ill-formed universal character names E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits. * Add new warning `invalid-utf8` for byte sequences that are not valid UTF8. The warning is activated but not fatal by default. * Warn on uses of C11 Unicode character constants and string literals This uses the `c11-extensions` warning, which is off by default. * Support preprocessing option -finput-charset= for GNU toolchains
* Add `Declare Scope` where appropriate (#440)Xavier Leroy2022-09-1919-7/+31
| | | | | | And re-enable the `undeclared-scope` warning. `Declare Scope` has been available since Coq 8.12, which is now the minimal Coq version supported.
* RTLgen: use the state and error monad for reserve_labels (#371)Pierre Nigron2022-09-194-24/+24
|
* Improved auto goal selection (#443)Andrej Dudenhefner2022-09-085-7/+7
| | | | | | Improves robustness in case of stronger (e)auto. This is in preparation of a change in Coq that will make auto and eauto stronger (https://github.com/coq/coq/pull/16293).
* Recognize more if-then-else statements that can be if-convertedXavier Leroy2022-09-052-126/+138
| | | | | | | | Ignore debug statements that could have prevented the recognition of a simple assignment. Since debug statements can formally get stuck, revise the simulation diagram to use the "eventually" modality.
* Introducing the "eventually" closure and new simulation diagrams using itXavier Leroy2022-09-051-27/+229
| | | | | | These diagrams enable the source program to make a number of finite transitions before eventually reaching a state that restores the simulation relation.
* `_Generic` is a C11 feature, should trigger the corresponding warning if activeXavier Leroy2022-09-041-0/+1
|
* Remove unused functions.Bernhard Schommer2022-09-031-7/+0
| | | | | | | | | | The `reset_constants` was only used for ARM and there it was superfluous since the jumptables, which it additionally resets in contrast to `reset_literals`, are always empty since jumptables are handled directly in during printing of the instruction. The `exists_constants` function is now also unused since we test directly for the different sizes in `emit_constants`.
* More simplifications for literal printingBernhard Schommer2022-09-036-31/+16
| | | | | | | Use the same code to split 64 bit literals into two 32 bit halfs as is used for 64 bit initialization data and print them in PrintAsm. This removes the need for a target specific printing function for 64 bit literals.
* Refactor emitting of constants.Bernhard Schommer2022-09-037-76/+21
| | | | | | The function was the same for nearly all backends and also the way 32 bit literals are printed so we moved it to PrintAsm. The 64 bit literals however are still target specific.
generated by cgit (git 2.34.1) at 2024-06-28 01:41:27 +0000