Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | fix ci ? | Léo Gourdin | 2021-03-02 | 2 | -0/+2 |
| | |||||
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 7 | -46/+9 |
|\ | |||||
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixed | David Monniaux | 2020-12-08 | 2 | -4/+6 |
| |\ | |||||
| | * | ARM modeling of registers destroyed by pseudo-instructions | Xavier Leroy | 2020-12-06 | 2 | -4/+6 |
| | | | | | | | | | | | | | | | Pflid destroys IR14 Inlined built-in functions destroy IR14 | ||||
| * | | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 4 | -3/+91 |
| |\ \ | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * \ \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 6 | -42/+3 |
| |\ \ \ | | | |/ | | |/| | |||||
| | * | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 1 | -2/+1 |
| | | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib. | ||||
| | * | | Add __builtin_sqrt as synonymous for __builtin_fsqrt | Xavier Leroy | 2020-07-27 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang. | ||||
| | * | | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml | Xavier Leroy | 2020-07-27 | 1 | -13/+0 |
| | | | | | | | | | | | | | | | | These functions are now available on all targets. | ||||
| | * | | No need to process __builtin_fabs in $ARCH/Asmexpand.ml | Xavier Leroy | 2020-07-27 | 1 | -2/+0 |
| | | | | | | | | | | | | | | | | __builtin_fabs has already been expanded in backend/Selection.v . | ||||
| | * | | Added missing hint database name. | Bernhard Schommer | 2020-06-30 | 1 | -1/+1 |
| | | | | |||||
| | * | | Move shared code in new file. | Bernhard Schommer | 2020-06-28 | 2 | -18/+0 |
| | | | | | | | | | | | | | | | | | | | | The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file. | ||||
| | * | | Remove the `can_reserve_register` function. | Bernhard Schommer | 2020-06-28 | 2 | -5/+0 |
| | | | | | | | | | | | | | | | | | | | | The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`. | ||||
| | * | | Use Hashtbl.find_opt. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt. | ||||
* | | | | cond_depends_on | David Monniaux | 2020-12-02 | 1 | -7/+7 |
| | | | | |||||
* | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 1 | -0/+1 |
|\ \ \ \ | | |_|/ | |/| | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 1 | -1/+0 |
| |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/Op.v common/Values.v kvx/Op.v | ||||
| * \ \ \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 2 | -3/+76 |
| |\ \ \ \ | |||||
| * | | | | | op_valid_pointer_eq arm | David Monniaux | 2020-10-19 | 1 | -0/+15 |
| | | | | | | |||||
| * | | | | | so that all architectures compile | David Monniaux | 2020-10-02 | 1 | -0/+1 |
| | |_|/ / | |/| | | | |||||
* | | | | | cond_valid_pointer_eq | David Monniaux | 2020-11-25 | 1 | -0/+10 |
| |_|/ / |/| | | | |||||
* | | | | pointer_eq copied | David Monniaux | 2020-11-25 | 1 | -0/+14 |
| |/ / |/| | | |||||
* | | | bug #223 fix for ARM | David Monniaux | 2020-11-23 | 2 | -3/+76 |
|/ / | |||||
* | | Adding copyrights | Cyril SIX | 2020-05-04 | 3 | -0/+38 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 2 | -3/+10 |
|\ \ | |||||
| * | | test whether the instructions are allowed | David Monniaux | 2020-04-19 | 1 | -0/+2 |
| | | | |||||
| * | | adapting new stuff for ARM and AArch64 | David Monniaux | 2020-04-01 | 1 | -3/+8 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 5 | -2/+56 |
|\ \ \ | |||||
| * | | | seems like the ARM profiling perhaps works | David Monniaux | 2020-04-11 | 4 | -2/+55 |
| | | | | |||||
| * | | | missing cases preventing compilation | David Monniaux | 2020-04-08 | 1 | -0/+1 |
| |/ / | |||||
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-thread | David Monniaux | 2020-04-08 | 4 | -209/+171 |
|\| | | |||||
| * | | DuplicateOpcodeHeuristic for ARM | David Monniaux | 2020-03-17 | 1 | -3/+22 |
| | | | |||||
| * | | ported to arm | David Monniaux | 2020-03-03 | 1 | -9/+6 |
| | | | |||||
| * | | fixed CSE2 for mppa_k1c | David Monniaux | 2020-03-03 | 2 | -0/+152 |
| |\ \ | | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2 | ||||
| | * | | CSE2 with alias analysis | David Monniaux | 2020-03-03 | 1 | -0/+20 |
| | | | | |||||
| | * | | CSE2 for ARM | David Monniaux | 2020-03-03 | 1 | -0/+132 |
| | |/ | |||||
| * | | Merge branch 'mppa-cse2' of ↵ | David Monniaux | 2020-03-03 | 11 | -14/+157 |
| |\ \ | | |/ | |/| | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | | Platform-independent implementation of Conventions.size_arguments (#222) | Xavier Leroy | 2020-02-24 | 1 | -206/+0 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The "size_arguments" function and its properties can be systematically derived from the "loc_arguments" function and its properties. Before, the RISC-V port used this derivation, and all other ports used hand-written "size_arguments" functions and proofs. This commit moves the definition of "size_arguments" to the platform-independent file backend/Conventions.v, using the systematic derivation, and removes the platform-specific definitions. This reduces code and proof size, and makes it easier to change the calling conventions. | ||||
* | | | Merge branch 'mppa-work' into mppa-thread | Cyril SIX | 2020-02-25 | 2 | -15/+19 |
|\ \ \ | |||||
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2020-02-24 | 2 | -15/+19 |
| |\| | | | |/ | |/| | | | | mppa-work-upstream-merge | ||||
| | * | Support re-normalization of values returned by function calls | Xavier Leroy | 2020-02-21 | 1 | -0/+6 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some ABIs leave more flexibility concerning function return values than CompCert expects. For example, the x86 ABI says that a function result of type "char" is returned in register AL, leaving the top 24 bits of register EAX unspecified, while CompCert expects EAX to contain 32 valid bits, namely the zero- or sign-extension of the 8-bit result. This commits adds a general mechanism to insert "re-normalization" conversions on the results of function calls. Currently, it only deals with results of small integer types, and inserts zero- or sign-extensions if so instructed by a platform-dependent function, Convention1.return_value_needs_normalization. The conversions in question are inserted early in the front-end, so that they can be optimized away in the back-end. The semantic preservation proof is still conducted against the CompCert model, where the return values of functions are already normalized. What the proof shows is that the extra conversions have no effect in this case. In future work we could relax the CompCert model, allowing functions to return values that are not normalized. | ||||
| | * | Refine the type of function results in AST.signature | Xavier Leroy | 2020-02-21 | 2 | -15/+13 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions. | ||||
* | | | fixes for aarch64 arm ppc ppc64 | David Monniaux | 2020-02-24 | 1 | -1/+1 |
| | | | |||||
* | | | fix for x86+arm unsupported thread local | David Monniaux | 2020-02-24 | 1 | -1/+3 |
|/ / | |||||
* | | stubs to keep compiling on architectures not K1c | David Monniaux | 2020-02-07 | 1 | -0/+3 |
| | | |||||
* | | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 2 | -3/+24 |
|\ \ | |||||
| * | | ARM generation of 2-instruction signed division by 2 (as opposed to ↵ | David Monniaux | 2020-01-14 | 2 | -3/+24 |
| |/ | | | | | | | 3-instruction) | ||||
| * | Revert "Remove `__builtin_nop` for some architectures. (#208)" | Bernhard Schommer | 2020-01-03 | 4 | -1/+8 |
| | | | | | | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95. | ||||
| * | Remove `__builtin_nop` for some architectures. (#208) | Bernhard Schommer | 2019-12-21 | 4 | -8/+1 |
| | | | | | | | | | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC. | ||||
* | | add: non trapping ops | David Monniaux | 2019-09-23 | 1 | -0/+26 |
| | |