Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | there seems to be some cache preload involved? | David Monniaux | 2019-04-06 | 1 | -1/+2 |
| | |||||
* | use of ternary operators | David Monniaux | 2019-04-06 | 1 | -3/+28 |
| | |||||
* | hand optimizations | David Monniaux | 2019-04-06 | 2 | -0/+407 |
| | |||||
* | have one with specific position | David Monniaux | 2019-04-06 | 1 | -1/+1 |
| | |||||
* | no need for this to be in two_address_op | David Monniaux | 2019-04-06 | 1 | -1/+1 |
| | |||||
* | binary search from Rosetta Code | David Monniaux | 2019-04-06 | 2 | -0/+78 |
| | |||||
* | ternary op version of bitsliced TEA | David Monniaux | 2019-04-05 | 1 | -4/+9 |
| | |||||
* | use cmove in bitsliced AES | David Monniaux | 2019-04-05 | 1 | -5/+2 |
| | |||||
* | move patterns to include file | David Monniaux | 2019-04-05 | 2 | -14/+25 |
| | |||||
* | implement using our "pattern matching" | David Monniaux | 2019-04-05 | 1 | -4/+11 |
| | |||||
* | removed the unproved hack to get builtins, will be reinstated later | David Monniaux | 2019-04-05 | 2 | -2/+2 |
| | |||||
* | select cmpu | David Monniaux | 2019-04-05 | 1 | -1/+1 |
| | |||||
* | ternary ops for float/double | David Monniaux | 2019-04-03 | 1 | -10/+6 |
| | |||||
* | ternary ops in AES and TEA | David Monniaux | 2019-04-03 | 3 | -13/+5 |
| | |||||
* | Merge branch 'mppa-ternary' of ↵ | David Monniaux | 2019-04-03 | 2 | -16/+10 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary | ||||
| * | problem in ValueAOp | David Monniaux | 2019-04-03 | 2 | -12/+7 |
| | | |||||
| * | begin implementing ternary builtin | David Monniaux | 2019-04-03 | 1 | -0/+7 |
| | | |||||
| * | attempts at generating builtins, start | David Monniaux | 2019-04-03 | 1 | -10/+2 |
| | | |||||
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-03 | 19 | -1151/+1412 |
| |\ | |||||
* | \ | Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary | David Monniaux | 2019-04-02 | 19 | -1151/+1412 |
|\ \ \ | | |/ | |/| | |||||
| * | | FIXME: Jumptables have linking issues. | David Monniaux | 2019-03-29 | 3 | -0/+1241 |
| | | | |||||
| * | | Merge branch 'mppa_k1c' of ↵ | David Monniaux | 2019-03-29 | 1 | -8/+8 |
| |\ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul | ||||
| | * \ | Merge branch 'mppa-mul' into mppa_k0c | David Monniaux | 2019-03-29 | 21 | -1082/+1916 |
| | |\ \ | |||||
| | * | | | rm rules that conflict | David Monniaux | 2019-03-29 | 1 | -8/+8 |
| | | | | | |||||
| * | | | | Merge remote-tracking branch 'origin/mppa_k1c' into mppa-mul | David Monniaux | 2019-03-29 | 1 | -1/+1 |
| |\| | | | |||||
| | * | | | use C99 mode | David Monniaux | 2019-03-29 | 1 | -1/+1 |
| | | | | | |||||
| | * | | | for testing with quest | David Monniaux | 2019-03-22 | 1 | -0/+24 |
| | | | | | |||||
| | * | | | check that gcc and ccomp compiled k1c code return the same | David Monniaux | 2019-03-22 | 1 | -2/+6 |
| | | | | | |||||
| | * | | | improved testing | David Monniaux | 2019-03-22 | 1 | -5/+16 |
| | | | | | |||||
| | * | | | uses yarpgen random generator | David Monniaux | 2019-03-22 | 1 | -0/+37 |
| | | | | | |||||
| | * | | | some more testing | David Monniaux | 2019-03-22 | 1 | -1/+1 |
| | | | | | |||||
| * | | | | missing config.h | David Monniaux | 2019-03-29 | 1 | -0/+3 |
| | | | | | |||||
| * | | | | Makefile for picosat | David Monniaux | 2019-03-29 | 3 | -62/+0 |
| | |/ / | |/| | | |||||
| * | | | ocaml benchmark | David Monniaux | 2019-03-28 | 3 | -8/+22 |
| | | | | |||||
| * | | | Makefile | David Monniaux | 2019-03-28 | 5 | -1025/+35 |
| | | | | |||||
| * | | | NDEBUG | David Monniaux | 2019-03-28 | 1 | -0/+6 |
| | | | | |||||
| * | | | some more inline | David Monniaux | 2019-03-28 | 2 | -12/+13 |
| | | | | |||||
| * | | | add some INLINE markers | David Monniaux | 2019-03-28 | 1 | -36/+38 |
| | | | | |||||
| * | | | picosat now uses the same Makefile system as the rest | David Monniaux | 2019-03-28 | 3 | -3/+49 |
| | | | | | | | | | | | | | | | | we are 27% slower than gcc | ||||
* | | | | Merge branch 'mppa-ternary' of ↵ | David Monniaux | 2019-04-02 | 5 | -1527/+39 |
|\ \ \ \ | | |_|/ | |/| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-ternary | ||||
| * | | | merge VLIW proofs | David Monniaux | 2019-03-28 | 5 | -1527/+39 |
| |\| | | | | | | | | | | | | | | Merge branch 'mppa-mul' into mppa-ternary | ||||
| | * | | some more ternary | David Monniaux | 2019-03-24 | 1 | -6/+6 |
| | | | | |||||
| | * | | experiments with ternary operator | David Monniaux | 2019-03-24 | 1 | -1/+6 |
| | | | | |||||
| | * | | experiments with ternary | David Monniaux | 2019-03-24 | 4 | -1526/+36 |
| | | | | |||||
| | * | | another ternary implementation | David Monniaux | 2019-03-24 | 1 | -1/+7 |
| | | | | |||||
* | | | | script for creduce | David Monniaux | 2019-03-29 | 1 | -0/+20 |
| | | | | |||||
* | | | | bitsliced-tea slightly more efficient with ternaries at some places | David Monniaux | 2019-03-29 | 2 | -4/+18 |
|/ / / | |||||
* | | | don't penalize x86 CompCert | David Monniaux | 2019-03-27 | 1 | -1/+1 |
| | | | |||||
* | | | put both compilers in their best mood | David Monniaux | 2019-03-27 | 1 | -5/+18 |
| | | | |||||
* | | | switch off ternary if not CompCert | David Monniaux | 2019-03-27 | 1 | -14/+4 |
| | | |