Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | | select through bitwise operations | David Monniaux | 2021-01-30 | 1 | -0/+40 | |
| | | | | ||||||
* | | | | Try to save values in virtual registers during expansion | Léo Gourdin | 2021-03-01 | 2 | -94/+117 | |
| | | | | ||||||
* | | | | Proofs finished for expansion | Léo Gourdin | 2021-03-01 | 2 | -19/+62 | |
| | | | | ||||||
* | | | | Debugging fake values finished | Léo Gourdin | 2021-03-01 | 2 | -14/+20 | |
| | | | | ||||||
* | | | | some bugfix | Léo Gourdin | 2021-03-01 | 2 | -15/+20 | |
| | | | | ||||||
* | | | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 8 | -170/+527 | |
| | | | | ||||||
* | | | | [Admitted checker] Some more proof, version with buggy addirw0 | Léo Gourdin | 2021-02-25 | 1 | -5/+126 | |
| | | | | ||||||
* | | | | some more proof for fake hsval checker expansions | Léo Gourdin | 2021-02-25 | 2 | -46/+771 | |
| | | | | ||||||
* | | | | [Intermediate] Adding fake hsval for Ccomp expansion | Léo Gourdin | 2021-02-23 | 2 | -7/+112 | |
| | | | | ||||||
* | | | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work | Léo Gourdin | 2021-02-23 | 1 | -0/+19 | |
|\ \ \ \ | ||||||
| * | | | | Separate target_op_simplify for riscV | Léo Gourdin | 2021-02-23 | 1 | -0/+19 | |
| | |/ / | |/| | | ||||||
* | | | | Branch expansions activated and configured in the checker (but admitted) and ↵ | Léo Gourdin | 2021-02-19 | 1 | -5/+6 | |
| | | | | | | | | | | | | | | | | bugfix in the expansion liveness modification | |||||
* | | | | Proof of Ocmp expansions without immediate and some drafts in comment | Léo Gourdin | 2021-02-18 | 2 | -6/+6 | |
| | | | | ||||||
* | | | | fix bug in merge | Léo Gourdin | 2021-02-16 | 1 | -1/+1 | |
| | | | | ||||||
* | | | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof | Léo Gourdin | 2021-02-11 | 8 | -61/+248 | |
| | | | | ||||||
* | | | | [Admitted checker] Adding cbranch expansions (without scratch) to the checker | Léo Gourdin | 2021-02-10 | 2 | -5/+7 | |
| | | | | ||||||
* | | | | [Admitted checker] Checker expansion for reg Ocmp (without scratch) | Léo Gourdin | 2021-02-10 | 4 | -36/+36 | |
| | | | | ||||||
* | | | | Adding pathmap psize modification during expansion oracle | Léo Gourdin | 2021-02-08 | 1 | -9/+20 | |
| | | | | ||||||
* | | | | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work | Léo Gourdin | 2021-02-08 | 1 | -1/+1 | |
|\| | | | ||||||
| * | | | fix OpWeights | David Monniaux | 2021-01-30 | 1 | -1/+1 | |
| |/ / | ||||||
* | | | cond and branches expanded | Léo Gourdin | 2021-02-06 | 8 | -293/+691 | |
| | | | ||||||
* | | | All Ocmp expanded in RTL | Léo Gourdin | 2021-02-03 | 7 | -202/+417 | |
| | | | ||||||
* | | | Ccomp for long | Léo Gourdin | 2021-02-03 | 8 | -52/+408 | |
| | | | ||||||
* | | | Ccompu expansion | Léo Gourdin | 2021-02-02 | 8 | -178/+223 | |
| | | | ||||||
* | | | Expansion of Ccompimm in RTL [Admitted checker] | Léo Gourdin | 2021-02-02 | 8 | -4/+383 | |
|/ / | ||||||
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-08 | 5 | -26/+136 | |
|\ \ | ||||||
| * \ | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 11 | -242/+577 | |
| |\ \ | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile configure | |||||
| * \ \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 5 | -26/+136 | |
| |\ \ \ | | | |/ | | |/| | ||||||
| | * | | 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. | |||||
| | * | | RISC-V implementation of __builtin_clz* and __builtin_ctz* | Xavier Leroy | 2020-07-27 | 2 | -0/+134 | |
| | | | | | | | | | | | | | | | | Using binary search loops expanded at point of use. | |||||
| | * | | 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 . | |||||
| | * | | 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 | -3/+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. | |||||
* | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3 | David Monniaux | 2020-12-02 | 9 | -239/+553 | |
|\ \ \ \ | | |_|/ | |/| | | ||||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-24 | 2 | -3/+14 | |
| |\ \ \ | ||||||
| * | | | | allow changing the target core | David Monniaux | 2020-10-22 | 2 | -120/+160 | |
| | | | | | ||||||
| * | | | | attempt at modeling Rocket | David Monniaux | 2020-10-22 | 1 | -0/+83 | |
| | | | | | ||||||
| * | | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵ | Sylvain Boulmé | 2020-10-17 | 1 | -0/+10 | |
| | | | | | | | | | | | | | | | | | | | | scheduler) | |||||
| * | | | | so that all architectures compile | David Monniaux | 2020-10-02 | 2 | -8/+16 | |
| | | | | | ||||||
| * | | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepass | David Monniaux | 2020-09-21 | 6 | -239/+390 | |
| |\ \ \ \ | ||||||
| | * | | | | risc-V now without trapping instructions | David Monniaux | 2020-09-21 | 4 | -74/+90 | |
| | | | | | | ||||||
| | * | | | | moved Risc-V div ValueAOp to central location | David Monniaux | 2020-09-21 | 1 | -293/+0 | |
| | | | | | | ||||||
| | * | | | | maketotal mod & div | David Monniaux | 2020-09-21 | 6 | -165/+593 | |
| | | |/ / | | |/| | | ||||||
| * | | | | wrong resources | David Monniaux | 2020-09-18 | 1 | -1/+1 | |
| | | | | | ||||||
| * | | | | EH1 scheduling | David Monniaux | 2020-09-18 | 1 | -5/+18 | |
| | | | | | ||||||
| * | | | | bogus OpWeights for Risc-V | David Monniaux | 2020-09-18 | 1 | -0/+19 | |
| |/ / / | ||||||
* | | | | op_depends_on_memory_correct | David Monniaux | 2020-11-25 | 1 | -6/+24 | |
| | | | | ||||||
* | | | | cond_valid_pointer_eq | David Monniaux | 2020-11-25 | 1 | -0/+10 | |
| | | | |