diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-08 14:01:06 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-08 14:01:06 +0100 |
commit | 8a57683e35e761389e0ca976d79f2a5a4c387733 (patch) | |
tree | 246ee8e50b13b9187c2e172d3a70f667d8e75290 | |
parent | 716687e12509a873e469e38250ffd57ba5d011f1 (diff) | |
download | compcert-kvx-8a57683e35e761389e0ca976d79f2a5a4c387733.tar.gz compcert-kvx-8a57683e35e761389e0ca976d79f2a5a4c387733.zip |
intro RTLpathWFcheck
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | scheduling/RTLpathScheduler.v | 8 | ||||
-rw-r--r-- | scheduling/RTLpathWFcheck.v | 28 |
3 files changed, 33 insertions, 5 deletions
@@ -140,7 +140,7 @@ SCHEDULING= \ RTLpathLivegen.v RTLpathSE_impl.v \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v + RTLpathScheduler.v RTLpathWFcheck.v # C front-end modules (in cfrontend/) diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v index beab405f..6f90b455 100644 --- a/scheduling/RTLpathScheduler.v +++ b/scheduling/RTLpathScheduler.v @@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof] Require Import AST Linking Values Maps Globalenvs Smallstep Registers. Require Import Coqlib Maps Events Errors Op. Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl. - +Require RTLpathWFcheck. Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG)) (at level 200, A at level 100, B at level 200) @@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler". Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} := - match RTLpathLivegen.function_checker tfr tpm with + match RTLpathWFcheck.function_checker tfr tpm with | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed") | true => OK {| fn_RTL := tfr; fn_path := tpm |} end. Next Obligation. - apply function_checker_path_entry. auto. + apply RTLpathWFcheck.function_checker_path_entry. auto. Defined. Next Obligation. - apply function_checker_wellformed_path_map. auto. + apply RTLpathWFcheck.function_checker_wellformed_path_map. auto. Defined. Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit := diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v new file mode 100644 index 00000000..eca5b24e --- /dev/null +++ b/scheduling/RTLpathWFcheck.v @@ -0,0 +1,28 @@ +Require Import Coqlib. +Require Import Maps. +Require Import Lattice. +Require Import AST. +Require Import Op. +Require Import Registers. +Require Import Globalenvs Smallstep RTL RTLpath. +Require Import Bool Errors. +Require Import Program. +Require RTLpathLivegen. + +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Definition function_checker (f: RTL.function) (pm: path_map): bool := + pm!(f.(fn_entrypoint)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *) + +Lemma function_checker_wellformed_path_map f pm: + function_checker f pm = true -> wellformed_path_map f.(fn_code) pm. +Admitted. + +Lemma function_checker_path_entry f pm: + function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)). +Proof. + unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true; + unfold path_entry. firstorder congruence. +Qed. |