aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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 proof of VLIWDavid Monniaux2019-03-288-24/+1074
|\ | | | | | | Merge branch 'mppa_postpass' into mppa-mul
| * Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-2810-75/+1072
| |\
| | * Merge branch 'mppa_vliw_essai_sylvain' of ↵Sylvain Boulmé2019-03-272-67/+80
| | |\ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_vliw_essai_sylvain
| | | * Proof of the entire forward simulation (still stuck to do + permutations)Cyril SIX2019-03-271-3/+10
| | | |
| | | * Preuve du forward_simu du parexec_wio_bblock_auxCyril SIX2019-03-272-60/+70
| | | |
| | * | dealing with permutationsSylvain Boulmé2019-03-272-29/+100
| | |/
| | * Avancement dans Asmblockdeps.vCyril SIX2019-03-272-91/+113
| | |
| | * 1 coup de pouce !Sylvain Boulmé2019-03-261-9/+29
| | |
| | * Un peu d'avancementCyril SIX2019-03-262-4/+287
| | |
| | * slight simplificationSylvain Boulmé2019-03-231-5/+4
| | |
| | * Avancement dans la preuve des bundlesCyril SIX2019-03-221-3/+51
| | |
| | * fix for Coq.8.8 ??Sylvain Boulmé2019-03-222-4/+3
| | |
| | * Décomposition de la preuve en une forward_simu_par_stuck et une ↵Cyril SIX2019-03-222-1/+72
| | | | | | | | | | | | forward_simu_par
| | * simplification of the proofSylvain Boulmé2019-03-212-29/+70
| | |
| | * yet another step backwardSylvain Boulmé2019-03-201-18/+39
| | |
| | * one step further...Sylvain Boulmé2019-03-201-6/+28
| | |
| | * premier decoupageSylvain Boulmé2019-03-201-2/+56
| | |
| | * Integrating Asmvliw.v in the proof chainCyril SIX2019-03-204-17/+30
| | |
| | * Idée de preuve VLIWCyril SIX2019-03-181-2/+21
| | |
| | * fix the step_internal of AsmvliwSylvain Boulmé2019-03-141-19/+23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Actually, we want to show that the outcome is the same for any order of "writes" in the parallel execution. (ie we ask that bundles have a deterministic semantics for parallel execution) - we relax the condition that the outcome should be given for sequential execution instead, we ask that the it is given for the "in order" writes. In theory, the semantics would also accept bundles like "R1 := R2 R2 := R1" which are deterministic for parallel execution But, of course, in practice, we will also prove the sequential execution.
| | * definition of VLIW semanticsSylvain Boulmé2019-03-143-14/+342
| | |
| * | 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
| | |
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| | |
* | | 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
| | |
* | | demo ternary opDavid Monniaux2019-03-242-0/+49
| | |
* | | mysteriously slow codeDavid Monniaux2019-03-242-0/+70
| | |
* | | encore un essai de creduceDavid Monniaux2019-03-233-0/+1561
| | |
* | | system for comparing speedsDavid Monniaux2019-03-231-0/+12
| | |
* | | bitsliced AES in one fileDavid Monniaux2019-03-231-10/+85
| | |
* | | Test in one file only.David Monniaux2019-03-231-0/+1467
| | |
* | | for testing with questDavid Monniaux2019-03-221-0/+24
| | |
* | | passage de structures en varargs (fonctionne avec une convention "passage ↵David Monniaux2019-03-221-0/+3
| | | | | | | | | | | | par référence" cohérente avec CompCert mais pas forcément avec gcc)
* | | Merge branch 'mppa-mul' of ↵David Monniaux2019-03-223-2/+54
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| * | | check that gcc and ccomp compiled k1c code return the sameDavid Monniaux2019-03-221-2/+6
| | | |
| * | | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| | | |
| * | | improved testingDavid Monniaux2019-03-221-5/+16
| | | |
| * | | some more testingDavid Monniaux2019-03-221-1/+1
| | | |
| * | | uses yarpgen random generatorDavid Monniaux2019-03-221-0/+37
| | | |
* | | | Merge branch 'mppa-mul' of ↵David Monniaux2019-03-22136-877/+595
|\| | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| * | | Merge branch 'mppa-mul' of ↵David Monniaux2019-03-2285-17/+259
| |\ \ \ | | | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
| | * | | Rajout de tests test/mppa pour division/moduloCyril SIX2019-03-226-0/+34
| | | | |
| | * | | Merge branch 'mppa_postpass' into mppa-mulCyril SIX2019-03-2282-30/+238
| | |\| |
| | | * | Reorganized the test/mppa/ tests to have fewer of themCyril SIX2019-03-2282-30/+238
| | | | |
generated by cgit (git 2.34.1) at 2024-07-11 23:47:48 +0000