aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-052-2/+2
|
* select cmpuDavid Monniaux2019-04-051-1/+1
|
* ternary ops for float/doubleDavid Monniaux2019-04-031-10/+6
|
* ternary ops in AES and TEADavid Monniaux2019-04-033-13/+5
|
* Merge branch 'mppa-ternary' of ↵David Monniaux2019-04-032-16/+10
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary
| * problem in ValueAOpDavid Monniaux2019-04-032-12/+7
| |
| * begin implementing ternary builtinDavid Monniaux2019-04-031-0/+7
| |
| * attempts at generating builtins, startDavid Monniaux2019-04-031-10/+2
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-0319-1151/+1412
| |\
* | \ Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-0219-1151/+1412
|\ \ \ | | |/ | |/|
| * | FIXME: Jumptables have linking issues.David Monniaux2019-03-293-0/+1241
| | |
| * | Merge branch 'mppa_k1c' of ↵David Monniaux2019-03-291-8/+8
| |\ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| | * \ Merge branch 'mppa-mul' into mppa_k0cDavid Monniaux2019-03-2921-1082/+1916
| | |\ \
| | * | | rm rules that conflictDavid Monniaux2019-03-291-8/+8
| | | | |
| * | | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mulDavid Monniaux2019-03-291-1/+1
| |\| | |
| | * | | use C99 modeDavid Monniaux2019-03-291-1/+1
| | | | |
| | * | | for testing with questDavid Monniaux2019-03-221-0/+24
| | | | |
| | * | | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| | | | |
| | * | | improved testingDavid Monniaux2019-03-221-5/+16
| | | | |
| | * | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| | | | |
| | * | | some more testingDavid Monniaux2019-03-221-1/+1
| | | | |
| * | | | missing config.hDavid Monniaux2019-03-291-0/+3
| | | | |
| * | | | Makefile for picosatDavid Monniaux2019-03-293-62/+0
| | |/ / | |/| |
| * | | ocaml benchmarkDavid Monniaux2019-03-283-8/+22
| | | |
| * | | MakefileDavid Monniaux2019-03-285-1025/+35
| | | |
| * | | NDEBUGDavid Monniaux2019-03-281-0/+6
| | | |
| * | | some more inlineDavid Monniaux2019-03-282-12/+13
| | | |
| * | | add some INLINE markersDavid Monniaux2019-03-281-36/+38
| | | |
| * | | picosat now uses the same Makefile system as the restDavid Monniaux2019-03-283-3/+49
| | | | | | | | | | | | | | | | we are 27% slower than gcc
* | | | Merge branch 'mppa-ternary' of ↵David Monniaux2019-04-025-1527/+39
|\ \ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary
| * | | merge VLIW proofsDavid Monniaux2019-03-285-1527/+39
| |\| | | | | | | | | | | | | | Merge branch 'mppa-mul' into mppa-ternary
| | * | some more ternaryDavid Monniaux2019-03-241-6/+6
| | | |
| | * | experiments with ternary operatorDavid Monniaux2019-03-241-1/+6
| | | |
| | * | experiments with ternaryDavid Monniaux2019-03-244-1526/+36
| | | |
| | * | another ternary implementationDavid Monniaux2019-03-241-1/+7
| | | |
* | | | script for creduceDavid Monniaux2019-03-291-0/+20
| | | |
* | | | bitsliced-tea slightly more efficient with ternaries at some placesDavid Monniaux2019-03-292-4/+18
|/ / /
* | | don't penalize x86 CompCertDavid Monniaux2019-03-271-1/+1
| | |
* | | put both compilers in their best moodDavid Monniaux2019-03-271-5/+18
| | |
* | | switch off ternary if not CompCertDavid Monniaux2019-03-271-14/+4
| | |
* | | improvements on cmoved etc.David Monniaux2019-03-271-4/+11
| | |
* | | work on ternaryDavid Monniaux2019-03-272-8/+21
| | |
* | | hand optimizedDavid Monniaux2019-03-272-0/+3271
| | |
* | | match some 'and'David Monniaux2019-03-272-4/+16
| | |
* | | essai du cmoveDavid Monniaux2019-03-273-3/+30
| | |