Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | * | | | Implemented call, return, store and loop heuristics | Cyril SIX | 2019-12-11 | 1 | -2/+55 | |
| | | | | | ||||||
| | * | | | Function to look ahead unconditionally | Cyril SIX | 2019-12-11 | 1 | -0/+12 | |
| | | | | | ||||||
| | * | | | Loop headers detection works! | Cyril SIX | 2019-12-11 | 1 | -3/+17 | |
| | | | | | ||||||
| | * | | | Dominators approach not working well ==> opting for visit approach | Cyril SIX | 2019-12-10 | 1 | -23/+73 | |
| | | | | | ||||||
| | * | | | Calcul de dominateurs a l'air de marcher | Cyril SIX | 2019-12-10 | 1 | -88/+144 | |
| | | | | | ||||||
| | * | | | Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' ↵ | Cyril SIX | 2019-12-09 | 24 | -292/+162 | |
| | |\ \ \ | | | | | | | | | | | | | | | | | | | into mppa-duplicate-oracle | |||||
| | | * \ \ | Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into ↵ | David Monniaux | 2019-12-09 | 24 | -292/+162 | |
| | | |\ \ \ | | | | | | | | | | | | | | | | | | | | | | mppa-duplicate-oracle | |||||
| | * | | | | | Rajout du calcul de dominateurs - pas testé | Cyril SIX | 2019-12-09 | 1 | -16/+43 | |
| | |/ / / / | ||||||
| | * | | | | merge w/ non trapping loads | David Monniaux | 2019-12-06 | 1 | -3/+3 | |
| | | | | | | ||||||
| | * | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-duplicate-oracle | David Monniaux | 2019-12-06 | 199 | -3768/+22046 | |
| | |\ \ \ \ | ||||||
| | * | | | | | Adding breadth first search | Cyril SIX | 2019-12-06 | 1 | -3/+6 | |
| | | | | | | | ||||||
| | * | | | | | [BROKEN] Compiles, not tested | Cyril SIX | 2019-12-06 | 1 | -3/+3 | |
| | | | | | | | ||||||
| | * | | | | | [BROKEN] Started BFS - does not compile | Cyril SIX | 2019-12-05 | 1 | -0/+30 | |
| | | | | | | | ||||||
| | * | | | | | bfs --> dfs | Cyril SIX | 2019-12-05 | 1 | -24/+26 | |
| | | | | | | | ||||||
| | * | | | | | Traces now stop at Icall/Ibuiltin/Ijumptable | Cyril SIX | 2019-12-04 | 1 | -6/+11 | |
| | | | | | | | ||||||
| | * | | | | | Fixed trace selection - for now, it only prints them, and the chosen paths ↵ | Cyril SIX | 2019-12-02 | 1 | -17/+32 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | are random | |||||
| | * | | | | | [BROKEN] Implementing trace selection from Chang & Hwu 1988, to be debugged | Cyril SIX | 2019-10-09 | 1 | -2/+163 | |
| | | | | | | | ||||||
| * | | | | | | CSE2 with NOTRAP | David Monniaux | 2020-02-03 | 2 | -95/+186 | |
| | | | | | | | ||||||
| * | | | | | | NOTRAP in CSE2: progress | David Monniaux | 2020-02-03 | 2 | -33/+260 | |
| | | | | | | | ||||||
| * | | | | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2 | David Monniaux | 2020-02-03 | 1 | -18/+18 | |
| |\ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert/dm-cse2 into mppa-cse2 | David Monniaux | 2020-02-03 | 5 | -0/+33 | |
| |\ \ \ \ \ \ \ | ||||||
| * \ \ \ \ \ \ \ | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 8 | -11/+1865 | |
| |\ \ \ \ \ \ \ \ | | |_|_|_|_|_|/ / | |/| | | | | | | | ||||||
| * | | | | | | | | Added description for forward moves | Cyril SIX | 2020-01-17 | 1 | -0/+1 | |
| | | | | | | | | | ||||||
| * | | | | | | | | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 12 | -60/+419 | |
| |\ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | 2-instruction signed division by two on Aarch64 | David Monniaux | 2020-01-15 | 3 | -24/+54 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | ARM generation of 2-instruction signed division by 2 (as opposed to ↵ | David Monniaux | 2020-01-14 | 2 | -3/+24 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 3-instruction) | |||||
| | * | | | | | | | | 64-bit signed division by two code | David Monniaux | 2020-01-14 | 3 | -14/+26 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | shrxl_shrl_3 | David Monniaux | 2020-01-14 | 1 | -0/+52 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | shrx'1_shr' | David Monniaux | 2020-01-14 | 1 | -1/+127 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4) | David Monniaux | 2020-01-14 | 3 | -14/+25 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | shrx_shr_3 | David Monniaux | 2020-01-14 | 1 | -0/+54 | |
| | | | | | | | | | | ||||||
| | * | | | | | | | | shrx1_shr | David Monniaux | 2020-01-14 | 1 | -0/+51 | |
| | | | | | | | | | | ||||||
| * | | | | | | | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-forwardmoves | David Monniaux | 2020-01-09 | 2 | -6/+7 | |
| |\ \ \ \ \ \ \ \ \ | ||||||
| | * | | | | | | | | | Fixing issue with <math.h> and fabs | Cyril SIX | 2020-01-09 | 1 | -1/+2 | |
| | | | | | | | | | | | ||||||
| | * | | | | | | | | | Fixing issue with "destruct ... in ..." tactics with Coq 8.8 | Cyril SIX | 2020-01-09 | 1 | -5/+5 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | FINISHED the forward-moves pass | David Monniaux | 2020-01-09 | 1 | -2/+6 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | nearly done | David Monniaux | 2020-01-09 | 1 | -3/+5 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | fix move | David Monniaux | 2020-01-09 | 1 | -1/+3 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | fix move | David Monniaux | 2020-01-09 | 2 | -4/+120 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | return is ok | David Monniaux | 2020-01-09 | 1 | -14/+53 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | proof of return | David Monniaux | 2020-01-09 | 1 | -1/+59 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | we still have issues with call stacks | David Monniaux | 2020-01-09 | 2 | -15/+51 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | moving forward with proofs | David Monniaux | 2020-01-09 | 2 | -5/+20 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | proof for jumptable | David Monniaux | 2020-01-09 | 1 | -1/+17 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | more proofs | David Monniaux | 2020-01-09 | 1 | -1/+18 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | fix bug and forward in proofs | David Monniaux | 2020-01-09 | 2 | -2/+18 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | some more proof | David Monniaux | 2020-01-09 | 1 | -3/+53 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | moving forward with proofs | David Monniaux | 2020-01-09 | 1 | -1/+59 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | fix bug in xfer function | David Monniaux | 2020-01-09 | 1 | -1/+2 | |
| | | | | | | | | | | | ||||||
| * | | | | | | | | | | progressing in proofs | David Monniaux | 2020-01-08 | 2 | -12/+101 | |
| | | | | | | | | | | |