aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-014-9/+25
|\
| * bugfix A64 peephole (cf Scade/Fighter example)Léo Gourdin2021-05-311-6/+5
| |
| * add auxfileDavid Monniaux2021-04-271-0/+17
| |
| * collision of registersDavid Monniaux2021-04-122-3/+3
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-015-16/+24
| | | | | | | | cfrontend/C2C.ml
* | fix aarch64 merge?Léo Gourdin2021-03-296-846/+17
| |
* | replacing omega with lia in some fileLéo Gourdin2021-03-294-30/+34
| |
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2317-216/+3156
|\ \ | |/ |/| | | | | | | | | | | | | 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
| * Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | Distinguish between: - uninitialized variables, which can go in COMM if supported - variables initialized with fixed, numeric quantities, which can go in a readonly section if "const" - variables initialized with symbol addresses which may need relocation, which cannot go in a readonly section even if "const", but can go in a special "const_data" section. Also: on macOS, use ".const" instead of ".literal8" for literals, as not all literals have size 8.
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-4/+4
| | | | | | | | | | | | | | This is a generalization of the previous PrintAsmaux.common_section function that - handles initialized variables in addition to uninitialized variables; - can be used for Section_const, not just for Section_data.
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-212-3/+3
| | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| * "macosx" is now called "macos"Xavier Leroy2021-01-183-3/+3
| | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
| * Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-6/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is complementary to 28f235806 Some ABIs leave more flexibility concerning function parameters than CompCert expects. For instance, the AArch64/ELF ABI allow the caller of a function to leave unspecified the "padding bits" of function parameters. As an example, a parameter of type "unsigned char" may not have zeros in bits 8 to 63, but may have any bits there. When the caller is compiled by CompCert, it normalizes argument values to the parameter types before the call, so padding bits are always correct w.r.t. the type of the argument. This is no longer guaranteed in interoperability scenarios, when the caller is not compiled by CompCert. This commit adds a general mechanism to insert "re-normalization" conversions on the parameters of a function, at function entry. This is controlled by the platform-dependent function Convention1.return_value_needs_normalization. The semantic preservation proof is still conducted against the CompCert model, where the argument 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 pass arguments that are not normalized.
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-133/+133
| | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| * AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)Xavier Leroy2020-12-261-1/+1
| | | | | | | | | | | | | | | | The .const section cannot contain absolute references to symbols, as these may need relocation and therefore must be writable. This should be fixed more generally by distinguishing between initialization data that contains absolute references to symbols and initialization data that does not.
| * AArch64: macOS portXavier Leroy2020-12-2612-215/+484
| | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
| * AArch64: clarify the printing of extending-register arithmetic operationsXavier Leroy2020-12-261-13/+13
| | | | | | | | | | The extended register is now printed as an X register if the extension mode is UXTX, and as a W register otherwise.
| * AArch64: wrong function alignmentXavier Leroy2020-12-261-1/+1
| | | | | | | | | | The alignment was 2 bytes (like for ARM) but should be 4 bytes. It was ignored by the GNU assembler, but the LLVM assembler warns.
* | fix ci ?Léo Gourdin2021-03-022-0/+59
| |
* | quick fixcommentsLéo Gourdin2021-02-161-1/+1
| |
* | Merge branch 'aarch64-peephole' into kvx-workLéo Gourdin2021-01-251-150/+110
|\ \
| * | Hashmap in peepholeLéo Gourdin2021-01-251-150/+110
| | |
* | | Merge remote-tracking branch 'origin/aarch64-peephole' into kvx-workDavid Monniaux2021-01-228-168/+297
|\| |
| * | printer and freg bugfixLéo Gourdin2021-01-211-57/+84
| | |
| * | fix str string in peepholeLéo Gourdin2021-01-201-1/+1
| | |
| * | Adding fp stores pairLéo Gourdin2021-01-207-27/+77
| | |
| * | Adding fp loads pairLéo Gourdin2021-01-208-134/+186
| | |
* | | Conditions now propagated by CSE3David Monniaux2021-01-201-5/+13
|\ \ \ | |/ / |/| | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-083-553/+241
| |\ \
| * \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-088-41/+45
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-029-171/+1141
| |\ \ \ \
| * | | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-5/+13
| | | | | |
* | | | | | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-076-230/+128
| | | | | |
* | | | | | cleaningSylvain Boulmé2021-01-071-2245/+0
| | | | | |
* | | | | | lia instead of omega in libLéo Gourdin2021-01-041-51/+51
| | | | | |
* | | | | | Fix Asmblockgenproof after mergeLéo Gourdin2020-12-201-8/+20
| | | | | |
* | | | | | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into ↵Léo Gourdin2020-12-208-1288/+4260
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | aarch64-peephole
| * | | | | | CleanupLéo Gourdin2020-12-195-1269/+919
| | | | | | |
| * | | | | | Asmblockgenproof finished !Léo Gourdin2020-12-192-215/+132
| | | | | | |
| * | | | | | Some progress in AsmblockgenproofLéo Gourdin2020-12-174-1494/+566
| | | | | | |
| * | | | | | intermediatet commit before builtinsLéo Gourdin2020-12-165-98/+3291
| | | | | | |
| * | | | | | Generals lemmas for asmblockgenproofLéo Gourdin2020-12-144-13/+896
| | | | | | |
| * | | | | | Removing the PseudoAsm IRLéo Gourdin2020-12-136-44/+301
| | | | | | |
* | | | | | | Fix the Asmblock/Asm proofLéo Gourdin2020-12-203-34/+26
| | | | | | |
* | | | | | | fix builtin_sqrtSylvain Boulmé2020-12-171-1/+1
| | | | | | |
* | | | | | | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-179-35/+52
|\ \ \ \ \ \ \ | | |_|_|_|/ / | |/| | | | |
| * | | | | | fix new register erasing scheme for AArch64David Monniaux2020-12-083-553/+241
| | |_|_|/ / | |/| | | |
| * | | | | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-082-8/+11
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
| | * | | | AArch64 modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-8/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
| * | | | | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-175/+1231
| |\ \ \ \ \ | | | |_|_|/ | | |/| | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure
generated by cgit (git 2.34.1) at 2024-07-04 02:04:32 +0000