aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
...
| * | 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-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 aarch64-p...Léo Gourdin2020-12-208-1288/+4260
|\ \ \ \ \ \
| * | | | | | 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
| * | | | | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-175/+1231
| |\ \ \ \ \ | | | |_|_|/ | | |/| | |
| * | | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-33/+34
| |\ \ \ \ \ | | | |/ / / | | |/| | |
| | * | | | Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| | * | | | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | * | | | Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | * | | | Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-8/+0
| | * | | | AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| | * | | | No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | * | | | Move shared code in new file.Bernhard Schommer2020-06-281-17/+0
| | * | | | Remove the `can_reserve_register` function.Bernhard Schommer2020-06-281-2/+0
| | * | | | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | * | | | Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
* | | | | | Allowing non-consec store, and cleaningLéo Gourdin2020-12-111-8/+41
* | | | | | Big improvment in peephole, changing LDP/STP semanticsLéo Gourdin2020-12-109-539/+551
| |_|_|/ / |/| | | |
* | | | | Peephole finished for nowLéo Gourdin2020-12-101-86/+211
* | | | | Non conseq storesLéo Gourdin2020-12-091-39/+87
* | | | | Non conseq loads in peepholeLéo Gourdin2020-12-091-82/+192
* | | | | Ocaml peephole oracle and array datastruct instead of listsLéo Gourdin2020-12-083-181/+246
* | | | | Some cleanup in todosLéo Gourdin2020-12-074-624/+13
* | | | | Simplifications in Peephole and size proof.Léo Gourdin2020-12-072-116/+48
* | | | | Simplification by merging fixpointsLéo Gourdin2020-12-071-21/+96
* | | | | peephole optLéo Gourdin2020-12-071-4/+3
* | | | | Asmgen proof completely proved with ldp/stpLéo Gourdin2020-12-066-133/+198
* | | | | a first working draft on ldp/stp peepholeLéo Gourdin2020-12-0413-205/+640
generated by cgit (git 2.34.1) at 2024-05-09 12:49:27 +0000