diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-09 11:41:08 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-09 11:41:08 +0200 |
| commit | feb29b9cf4a051ce0df81df84bc5f3228074de20 (patch) | |
| tree | 214676b7a6704788065c058acc5f4dedbfacf13b /kvx | |
| parent | fb62d3b4d69a5bed5c7ef42266816caec59c6f17 (diff) | |
| download | compcert-kvx-feb29b9cf4a051ce0df81df84bc5f3228074de20.tar.gz compcert-kvx-feb29b9cf4a051ce0df81df84bc5f3228074de20.zip | |
Cleanup
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathScheduler.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kvx/lib/RTLpathScheduler.v b/kvx/lib/RTLpathScheduler.v index b70c1685..0f099ce8 100644 --- a/kvx/lib/RTLpathScheduler.v +++ b/kvx/lib/RTLpathScheduler.v @@ -159,7 +159,6 @@ Definition verified_scheduler (f: RTLpath.function) : res (RTLpath.function * (P let tfr := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in do tf <- proj1_sig (function_builder tfr tpm); do tt <- function_equiv_checker dm f tf; -(* do _ <- injective_checker dm; *) OK (tf, dm). Theorem verified_scheduler_correct f tf dm: @@ -171,13 +170,12 @@ Theorem verified_scheduler_correct f tf dm: /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path f) pc1) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> path_entry (fn_path tf) pc2) /\ (forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2) -(* /\ is_injective dm *) . Proof. intros VERIF. unfold verified_scheduler in VERIF. explore. Local Hint Resolve function_equiv_checker_entrypoint function_equiv_checker_pathentry1 function_equiv_checker_pathentry2 - function_equiv_checker_correct (* injective_checker_correct *): core. + function_equiv_checker_correct: core. destruct (function_builder _ _) as [res H]; simpl in * |- *; auto. apply H in EQ2. rewrite EQ2. simpl. repeat (constructor; eauto). @@ -192,7 +190,6 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1; dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2; dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sexec_simu dupmap f1 f2 pc1 pc2; -(* dupmap_injective: is_injective dupmap *) }. Program Definition transf_function (f: RTLpath.function): |