Commit 8a57683e authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

intro RTLpathWFcheck

parent 716687e1
......@@ -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/)
......
......@@ -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 :=
......
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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment