diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-01-31 15:01:01 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-01-31 15:01:01 +0100 |
| commit | 464da1ee7861e0d51f6c5dc786907a66b0f46e35 (patch) | |
| tree | b8bd63a6eca6c4d0c7e328683c69cecb6360666c /mppa_k1c | |
| parent | 0934d70a0c10185400e435dc8337525f31e85d0d (diff) | |
| download | compcert-kvx-464da1ee7861e0d51f6c5dc786907a66b0f46e35.tar.gz compcert-kvx-464da1ee7861e0d51f6c5dc786907a66b0f46e35.zip | |
idee de refactoring
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/PostpassScheduling.v | 78 |
1 files changed, 54 insertions, 24 deletions
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v index 1483a5d7..e8e6fcc5 100644 --- a/mppa_k1c/PostpassScheduling.v +++ b/mppa_k1c/PostpassScheduling.v @@ -21,30 +21,60 @@ Axiom schedule: bblock -> list bblock. Extract Constant schedule => "PostpassSchedulingOracle.schedule". -(* TODO - implement the verificator *) -Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb). +(* TODO: refactorisation. -Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) := - match lbb with - | nil => OK nil - | (cons bb lbb) => - do tlbb <- transf_blocks lbb; - do tbb <- verified_schedule bb; - OK (tbb ++ tlbb) - end. +... concat2 ... -Definition transl_function (f: function) : res function := - do lb <- transf_blocks (fn_blocks f); - OK (mkfunction (fn_sig f) lb). - -Definition transf_function (f: function) : res function := - do tf <- transl_function f; - if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks)) - then Error (msg "code size exceeded") - else OK tf. - -Definition transf_fundef (f: fundef) : res fundef := - transf_partial_fundef transf_function f. - -Definition transf_program (p: program) : res program := +Fixpoint concat_all (lbb: list bblock) : res bblock :=
+ match lbb with
+ | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list")
+ | bb::nil => OK bb
+ | bb::lbb =>
+ do bb' <- concat_all lbb;
+ concat2 bb bb'
+ end.
+
+Axiom test_equiv_bblock: bblock -> bblock -> bool.
+
+Axiom test_equiv_bblock_correct:
+ forall ge f bb tbb,
+ test_equiv bb tbb = true ->
+ bblock_equiv ge f bb tbb.
+
+Definition verified_schedule (bb : bblock) : res (list bblock) :=
+ DO lbb <- (schedule bb) ;
+ DO tbb <- (concat lbb) ;
+ DO res <- test_equiv_bblock bb tbb ;
+ if res
+ then OK lbb
+ else Error (msg "blah").
+
+*)
+
+(* TODO - implement the verificator *)
+Definition verified_schedule (bb : bblock) : res (list bblock) := OK (schedule bb).
+
+Fixpoint transf_blocks (lbb : list bblock) : res (list bblock) :=
+ match lbb with
+ | nil => OK nil
+ | (cons bb lbb) =>
+ do tlbb <- transf_blocks lbb;
+ do tbb <- verified_schedule bb;
+ OK (tbb ++ tlbb)
+ end.
+
+Definition transl_function (f: function) : res function :=
+ do lb <- transf_blocks (fn_blocks f);
+ OK (mkfunction (fn_sig f) lb).
+
+Definition transf_function (f: function) : res function :=
+ do tf <- transl_function f;
+ if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
+ then Error (msg "code size exceeded")
+ else OK tf.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+ transf_partial_fundef transf_function f.
+
+Definition transf_program (p: program) : res program :=
transform_partial_program transf_fundef p.
\ No newline at end of file |