aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* better intermediate pointDavid Monniaux2019-04-081-5/+8
|
* Merge branch 'mppa-work' of ↵David Monniaux2019-04-081-17/+29
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * improving comments on AsmvliwSylvain Boulmé2019-04-081-17/+29
| |
* | powerwindow from tacle-benchDavid Monniaux2019-04-0842-0/+5165
|/
* Merge branch 'mppa-refactor' into mppa-workCyril SIX2019-04-0812-1946/+1667
|\
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-refactorCyril SIX2019-04-0880-125/+82525
| |\ | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
| * \ Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactorCyril SIX2019-04-088-465/+331
| |\ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v
| | * | relecture sylvainSylvain Boulmé2019-04-058-505/+353
| | | | | | | | | | | | | | | | avec TODOs pour refactoring #90
| * | | #91 Removed completely the duplicated semantics in AsmblockCyril SIX2019-04-056-257/+89
| |/ /
| * | #90 Asmvliw/Asmblock refactoring attemptCyril SIX2019-04-0511-1611/+1634
| | |
* | | from Tacle BenchDavid Monniaux2019-04-088-0/+618
| |/ |/|
* | predicated experimentsDavid Monniaux2019-04-072-0/+29
| |
* | uses the pattern matchingDavid Monniaux2019-04-061-2/+2
| |
* | keep the .s filesDavid Monniaux2019-04-061-9/+11
| |
* | Makefile for timing.David Monniaux2019-04-062-3/+13
| | | | | | | | We are 12% slower than gcc.
* | makefile for PCRE2David Monniaux2019-04-063-5/+12764
| |
* | tests with PCRE2 (regular expression library)David Monniaux2019-04-0639-0/+62943
| |
* | use ternary in fillDavid Monniaux2019-04-061-1/+1
| |
* | reoptimize the CDavid Monniaux2019-04-061-1/+2
| |
* | hand optimizationsDavid Monniaux2019-04-061-2/+4
| |
* | various hand optimizationsDavid Monniaux2019-04-065-0/+1525
| |
* | reoptimize by handDavid Monniaux2019-04-061-3/+2
| |
* | goto endDavid Monniaux2019-04-061-2/+25
| |
* | there seems to be some cache preload involved?David Monniaux2019-04-061-1/+2
| |
* | use of ternary operatorsDavid Monniaux2019-04-061-3/+28
| |
* | hand optimizationsDavid Monniaux2019-04-062-0/+407
| |
* | have one with specific positionDavid Monniaux2019-04-061-1/+1
| |
* | no need for this to be in two_address_opDavid Monniaux2019-04-062-2/+2
| |
* | binary search from Rosetta CodeDavid Monniaux2019-04-062-0/+78
| |
* | ternary op version of bitsliced TEADavid Monniaux2019-04-051-4/+9
| |
* | use cmove in bitsliced AESDavid Monniaux2019-04-051-5/+2
| |
* | move patterns to include fileDavid Monniaux2019-04-052-14/+25
| |
* | implement using our "pattern matching"David Monniaux2019-04-051-4/+11
| |
* | reinstated the orl selectl constructDavid Monniaux2019-04-052-10/+7
| |
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
| |
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
| |
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-054-74/+8
| |
* | Oselectf, Oselectfs with conditionDavid Monniaux2019-04-058-131/+325
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-051-1/+1
|\|
| * Possible fix pour l'issue #82 (mauvais calcul de taille de bundle pour les ↵Cyril SIX2019-04-051-1/+1
| | | | | | | | store)
* | selectl with conditionDavid Monniaux2019-04-058-68/+172
| |
* | Select cmpluDavid Monniaux2019-04-052-1/+32
| |
* | select cmpuDavid Monniaux2019-04-058-6/+61
| |
* | factor out some proofsDavid Monniaux2019-04-051-6/+3
| |
* | some more Oselect comparisonsDavid Monniaux2019-04-042-1/+14
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-042-352/+187
|\|
| * Refactorisation de forward_simu_basicCyril SIX2019-04-041-102/+55
| |
| * refactorized forward_simu_controlCyril SIX2019-04-041-107/+67
| |
| * Refactorisation de forward_simu_par_controlCyril SIX2019-04-041-141/+63
| |
| * Erreur idiote dans les latences ?Cyril SIX2019-04-041-2/+2
| |