| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | fix aarch64 merge? | Léo Gourdin | 2021-03-29 | 1 | -0/+466 |
| | | |||||
| * | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -467/+0 |
| |\ | | | | | | | | | | | | | | | | | 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 | ||||
| | * | AArch64: macOS port | Xavier Leroy | 2020-12-26 | 1 | -2/+3 |
| | | | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. | ||||
| * | | Adding fp stores pair | Léo Gourdin | 2021-01-20 | 1 | -0/+6 |
| | | | |||||
| * | | Adding fp loads pair | Léo Gourdin | 2021-01-20 | 1 | -4/+10 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into ↵ | Léo Gourdin | 2020-12-20 | 1 | -3/+2 |
| |\ \ | | | | | | | | | | aarch64-peephole | ||||
| | * | | Removing the PseudoAsm IR | Léo Gourdin | 2020-12-13 | 1 | -3/+2 |
| | | | | |||||
| * | | | Big improvment in peephole, changing LDP/STP semantics | Léo Gourdin | 2020-12-10 | 1 | -8/+8 |
| |/ / | |||||
| * | | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -10/+18 |
| | | | |||||
| * | | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -14/+21 |
| | | | | | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
| * | | Removing OrigAsmgen by moving the necessary functions in Asmgen.v | Léo Gourdin | 2020-11-25 | 1 | -0/+77 |
| | | | |||||
| * | | Restoring asmgenproof on multiple labels issue | Léo Gourdin | 2020-11-24 | 1 | -4/+4 |
| | | | |||||
| * | | Dumb (identity) scheduling working and integrated | Léo Gourdin | 2020-11-03 | 1 | -2/+2 |
| | | | |||||
| * | | Author and stash single label Asmgenproof after merge | Léo Gourdin | 2020-11-02 | 1 | -0/+1 |
| | | | |||||
| * | | Merge branch 'aarch64_block_multiple_labels' into aarch64-postpass | Léo Gourdin | 2020-11-02 | 1 | -4/+4 |
| |\ \ | |||||
| | * | | Yarpgen C file to test multiple labels and corresponding code | Léo Gourdin | 2020-11-01 | 1 | -4/+4 |
| | | | | | | | | | | In this branch I remove the multiple label limitation to pass some tests but the proof is admitted ! | ||||
| * | | | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -6/+7 |
| |/ / | |||||
| * | | Bugfix in Asmgen | Léo Gourdin | 2020-10-29 | 1 | -1/+1 |
| | | | |||||
| * | | Found a bug in Asmgen about iregsp constructor | Léo Gourdin | 2020-10-29 | 1 | -9/+9 |
| | | | |||||
| * | | aarch64 compiles again (but ccomp generates incorrect assembly) | Sylvain Boulmé | 2020-10-23 | 1 | -5/+5 |
| | | | |||||
| * | | Adding buitin_args lemmas | Léo Gourdin | 2020-10-21 | 1 | -1/+1 |
| | | | | | | | | | There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC. This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg. | ||||
| * | | Prove exec_body_dont_move_PC | Justus Fasse | 2020-08-18 | 1 | -5/+5 |
| | | | | | | | | | | | | | Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like | ||||
| * | | Simplify unfold_bblock and complete unfold_body's case in find_instr_bblock | Justus Fasse | 2020-07-29 | 1 | -9/+2 |
| | | | | | | | | | | | | | | | The previous version of unfold_bblock was copied from kvx/Asm.v. kvx's version is slightly different in that for the (here removed) special case it does not put a semicolon to separate bundles. Since aarch64 does not have kvx's bundles the two versions should be equivalent. | ||||
| * | | backward decomposition of the proof | Sylvain Boulmé | 2020-07-22 | 1 | -1/+1 |
| | | | |||||
| * | | Add dynamically checked assumption to simplify Asmgenproof | Justus Fasse | 2020-07-21 | 1 | -9/+23 |
| | | | | | | | | | | | Previously Asmblock.label_pos and Asm.label_pos could point to different memory location for the same label. | ||||
| * | | "we must check that the generated code contains less than [2^32] ↵ | Justus Fasse | 2020-07-15 | 1 | -2/+3 |
| | | | | | | | | | | | | | instructions otherwise the offset part of the [PC] code pointer could wrap around, leading to incorrect executions" -- From the original aarch64/Asmgen.v | ||||
| * | | Generate both Pcsel and Pfsel | Justus Fasse | 2020-07-13 | 1 | -1/+12 |
| | | | | | | | | | | | | | | | In Asmblock, Pcsel is used for both integer and floating-point conditional selection. A previous commit (c764ff84) had incorrectly reverted the merging of Pfsel into Pcsel. | ||||
| * | | Finish proof of Lemma symbol_high_low | Justus Fasse | 2020-07-09 | 1 | -3/+3 |
| | | | |||||
| * | | Implement unfold function from Asmblock to Asm | Justus Fasse | 2020-07-09 | 1 | -2/+299 |
| | | | | | | | | | | | | | | | | | Largely semi-automatically generated with vim regexes and macros. Right now the only interesting case is Pmovk: here we ckeck that on the Asmblock level the source and target register are the same. Then, we can safely translate to Asm's Pmovk which takes a single register (mutating it in-place). | ||||
| * | | restauring Coq compilation with STUBS | Sylvain Boulmé | 2020-06-22 | 1 | -2/+15 |
| | | | |||||
| * | | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -1162/+23 |
| | | | |||||
| * | | disable leaf function removal of return address restoration due to memcpy ↵ | David Monniaux | 2020-03-27 | 1 | -2/+5 |
| | | | | | | | | | overwriting the return address register | ||||
| * | | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-03-27 | 1 | -2/+4 |
| |\ \ | |||||
| | * | | removed RA restoration | David Monniaux | 2020-03-25 | 1 | -2/+4 |
| | |/ | |||||
| * | | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -8/+14 |
| |\ \ | |||||
| | * | | 2-instruction signed division by two on Aarch64 | David Monniaux | 2020-01-15 | 1 | -8/+14 |
| | |/ | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-12-09 | 1 | -1/+6 |
| |\| | | | | | | | mppa-work-upstream-merge | ||||
| | * | Fix for AArch64 alignment problem (#206) | Bernhard Schommer | 2019-11-28 | 1 | -1/+6 |
| | | | | | | | | | | | | | | | | | | | In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time. This PR extends the check for a representable offset for the addressing of global variables to also check whether the variable is correctly aligned. Only if both conditions are met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic loadsymbol sequence. | ||||
| * | | Merge tag 'v3.6_mppa_2019-09-20' of ↵ | David Monniaux | 2019-09-20 | 1 | -3/+8 |
| |/ | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load | ||||
| * | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -0/+1151 |
| This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |