index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
aarch64
/
PostpassSchedulingOracle.ml
Commit message (
Expand
)
Author
Age
Files
Lines
*
Passing info of live regs to scheduler: beginning
nicolas.nardino
2021-06-04
1
-0
/
+1
*
Adding fp loads pair
Léo Gourdin
2021-01-20
1
-4
/
+4
*
Big improvment in peephole, changing LDP/STP semantics
Léo Gourdin
2020-12-10
1
-124
/
+69
*
a first working draft on ldp/stp peephole
Léo Gourdin
2020-12-04
1
-3
/
+25
*
Adding semantics for Pldp
Léo Gourdin
2020-12-02
1
-3
/
+16
*
add option in scheduler to record bb size
Léo Gourdin
2020-11-30
1
-0
/
+5
*
Changing weights system at asmblock level instead of asm
Léo Gourdin
2020-11-30
1
-240
/
+71
*
Main part of postpasssch proof now completed
Léo Gourdin
2020-11-24
1
-1
/
+5
*
Postpass scheduling OK
Léo Gourdin
2020-11-18
1
-146
/
+13
*
Builtin mem spec in scheduler and some needed proof in Postpasssch.v
Léo Gourdin
2020-11-17
1
-1
/
+1
*
Remaining ctl insts except Pbuiltin (maps to error)
Léo Gourdin
2020-11-16
1
-31
/
+45
*
Loads and stores op
Léo Gourdin
2020-11-13
1
-26
/
+35
*
Arith inst OK for the verifier
Léo Gourdin
2020-11-12
1
-6
/
+36
*
Preparing the repo for debugging postpass and executing tests
Léo Gourdin
2020-11-06
1
-4
/
+4
*
set debug to false in oracle
Léo Gourdin
2020-11-05
1
-1
/
+1
*
A first (not well-tuned) working version of postpass scheduling for A64
Léo Gourdin
2020-11-05
1
-714
/
+713
*
Smart scheduler build problem and flatten solution OK
Léo Gourdin
2020-11-04
1
-237
/
+245
*
Dumb (identity) scheduling working and integrated
Léo Gourdin
2020-11-03
1
-858
/
+753
*
Preparation for postpass in aarch64 and refactoring
Léo Gourdin
2020-11-02
1
-0
/
+1029