aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
Commit message (Expand)AuthorAgeFilesLines
* progressing on selectDavid Monniaux2019-04-042-17/+11
* working on selectDavid Monniaux2019-04-041-3/+24
* working on selectDavid Monniaux2019-04-041-28/+58
* prepare for conditions in cmoveDavid Monniaux2019-04-044-19/+34
* ternary ops for float/doubleDavid Monniaux2019-04-033-2/+72
* for floats and doubles, asmgen supportDavid Monniaux2019-04-033-15/+92
* ternary ops in AES and TEADavid Monniaux2019-04-034-8/+9
* problem in ValueAOpDavid Monniaux2019-04-034-9/+12
* Merge remote-tracking branch 'origin/mppa-work' into mppa-ternaryDavid Monniaux2019-04-0330-2245/+1299
|\
| * Merge remote-tracking branch 'origin/mppa_k1c' into mppa-workCyril SIX2019-04-0314-1456/+421
| |\
| | * robustness of Asmblockdeps.*op_eqSylvain Boulmé2019-04-021-27/+38
| | * comment on Asmblockdeps.is_constantSylvain Boulmé2019-04-021-9/+12
| | * Impure: improved iandb + struct_eqSylvain Boulmé2019-04-013-34/+28
| | * renommage abstractbb: Name -> PRegSylvain Boulmé2019-04-015-32/+32
| | * renommages abstract_bbSylvain Boulmé2019-04-015-156/+156
| | * petite factorisation de preuveSylvain Boulmé2019-04-011-69/+59
| | * minor simplSylvain Boulmé2019-04-011-8/+14
| | * simpler parexec_wio_bblock_auxSylvain Boulmé2019-04-012-3/+2
| | * cleaning Asmvliw semanticsSylvain Boulmé2019-04-014-42/+73
| | * delete useless DepExample* filesSylvain Boulmé2019-04-014-1051/+0
| * | Load/Store reg-reg are now proven everywhereCyril SIX2019-04-032-92/+68
| * | Preuve des load/store registre registre. Reste des modifs mineures dans les p...Cyril SIX2019-04-036-77/+196
| * | Preuve du transl_load et transl_store registre offsetCyril SIX2019-04-032-30/+89
| * | We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admittedCyril SIX2019-04-033-494/+51
| * | Small refactoring and renaming of Stores and LoadsCyril SIX2019-04-033-70/+50
| * | Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yetCyril SIX2019-04-0210-205/+417
| * | Started to add addressing with register + register, Mach -> Asm not done yetCyril SIX2019-04-015-3/+12
| * | Using fixedd.rz in longofsingle instead of i64_dtosCyril SIX2019-04-012-8/+13
| |/
| * fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-301-14/+18
| * Merge remote-tracking branch 'origin/mppa-jumptable' into mppa-jumptableCyril SIX2019-03-291-2/+5
| |\
| | * Finition de la preuve de AsmblockgenproofCyril SIX2019-03-291-2/+5
| * | Preuve de Jumptable dans Asmblockdeps.vCyril SIX2019-03-292-1/+24
| * | Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptableCyril SIX2019-03-297-23/+1120
| |\ \ | | |/ | |/|
| | * No more AdmittedCyril SIX2019-03-291-55/+102
| * | Avancement dans la preuve du MBjumptableCyril SIX2019-03-291-1/+21
| * | FIX BUG in TargetPrinter (nandd immediate wrongly printed as andd)David Monniaux2019-03-221-1/+1
| * | Merge branch 'mppa-mul' into mppa-jumptableDavid Monniaux2019-03-2214-719/+123
| |\ \
| * | | Jump tables now work. There is still an "Admitted" subcase in a proof.David Monniaux2019-03-223-5/+15
| * | | on avance sur la jumptableDavid Monniaux2019-03-222-3/+3
| * | | jumptable avanceDavid Monniaux2019-03-221-1/+8
| * | | Fixed proof of Asmblockdeps wrt PjumptableCyril SIX2019-03-221-25/+28
| * | | begin jumptables (does not work)David Monniaux2019-03-214-3/+57
* | | | merge VLIW proofsDavid Monniaux2019-03-287-23/+1073
|\ \ \ \
| * \ \ \ merge proof of VLIWDavid Monniaux2019-03-287-23/+1073
| |\ \ \ \ | | | |_|/ | | |/| |
| | * | | Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpassDavid Monniaux2019-03-289-74/+1071
| | |\ \ \
| | | * \ \ Merge branch 'mppa_vliw_essai_sylvain' of gricad-gitlab.univ-grenoble-alpes.f...Sylvain Boulmé2019-03-272-67/+80
| | | |\ \ \
| | | | * | | 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
generated by cgit (git 2.34.1) at 2024-07-14 15:11:51 +0000