diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 18:43:57 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 18:43:57 +0200 |
| commit | f37547880890ec7ff2acfba89848944d492ce9ad (patch) | |
| tree | 3ad09350b0315d6461e516ba4a8df41d08194bcc /scheduling | |
| parent | 9f252d9055ad16f9433caaf41f6490e45424e88a (diff) | |
| parent | 3d8775adf2e22c1e22cc45beaa97a25343c8d533 (diff) | |
| download | compcert-kvx-f37547880890ec7ff2acfba89848944d492ce9ad.tar.gz compcert-kvx-f37547880890ec7ff2acfba89848944d492ce9ad.zip | |
Merge branch 'BTL' into BTL-translation
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTLroadmap.md | 8 | ||||
| -rw-r--r-- | scheduling/RTLpath.v | 2 | ||||
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 7 | ||||
| -rw-r--r-- | scheduling/abstractbb/AbstractBasicBlocksDef.v | 2 |
4 files changed, 9 insertions, 10 deletions
diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md index dde2090c..bd70e273 100644 --- a/scheduling/BTLroadmap.md +++ b/scheduling/BTLroadmap.md @@ -54,8 +54,12 @@ Branch factorization should also be possible in BTL -> RTL pass. Example: revert **CURRENT STATUS** - verifier: implemented and proved w.r.t match_iblock specification. -- BTL -> RTL: done. -- RTL -> BTL: started. +- Proof: + - BTL -> RTL: done. + - RTL -> BTL: done. +- Oracles: + - BTL -> RTL: TODO. + - RTL -> BTL: started. **TODO** diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v index 5b34dc16..2f73f1fa 100644 --- a/scheduling/RTLpath.v +++ b/scheduling/RTLpath.v @@ -27,8 +27,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import Op Registers. Require Import RTL Linking. -Declare Scope option_monad_scope. - Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index c3266db9..4bb3e18e 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -105,13 +105,12 @@ with hsmem_proj hm := | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv) end. -Declare Scope hse. -Local Open Scope hse. - - (** We use a Notation instead a Definition, in order to get more automation "for free" *) Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv)) (only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse. + +Local Open Scope hse. + Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv)) (only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse. Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm)) diff --git a/scheduling/abstractbb/AbstractBasicBlocksDef.v b/scheduling/abstractbb/AbstractBasicBlocksDef.v index 34d72de1..fec716c4 100644 --- a/scheduling/abstractbb/AbstractBasicBlocksDef.v +++ b/scheduling/abstractbb/AbstractBasicBlocksDef.v @@ -273,8 +273,6 @@ with list_term := Scheme term_mut := Induction for term Sort Prop with list_term_mut := Induction for list_term Sort Prop. -Declare Scope pattern_scope. -Declare Scope term_scope. Bind Scope pattern_scope with term. Delimit Scope term_scope with term. Delimit Scope pattern_scope with pattern. |