Lvc.Compiler
Require Import List CSet.
Require Import Util AllInRel IL EnvTy RenameApart Sim Status Annotation.
Require CMap.
Require Liveness TrueLiveness LivenessValidators ParallelMove ILN LivenessAnalysis.
Require Coherence Delocation DelocationAlgo DelocationValidator Allocation AllocationAlgo.
Require CopyPropagation DVE EAE Alpha.
Require ConstantPropagation ConstantPropagationAnalysis.
Require Import ExtrOcamlBasic.
Require Import ExtrOcamlZBigInt.
Require Import ExtrOcamlNatInt.
Require Import String ExtrOcamlString.
Set Implicit Arguments.
Section Compiler.
Hypothesis ssa_construction : stmt → ann (option (set var)) × ann (list var).
Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).
Hypothesis first : ∀ (A:Type), A → ( A → status (A × bool)) → status A.
Definition livenessAnalysis :=
Analysis.fixpoint LivenessAnalysis.liveness_analysis first.
Definition constantPropagationAnalysis :=
Analysis.fixpoint ConstantPropagationAnalysis.constant_propagation_analysis first.
Definition additionalArguments s lv :=
fst (DelocationAlgo.computeParameters nil nil nil s lv).
Class ToString (T:Type) := toString : T → string.
Hypothesis OutputStream : Type.
Hypothesis print_string : OutputStream → string → OutputStream.
Hypothesis toString_nstmt : ILN.nstmt → string.
Instance ToString_nstmt : ToString ILN.nstmt := toString_nstmt.
Hypothesis toString_stmt : stmt → string.
Instance ToString_stmt : ToString stmt := toString_stmt.
Hypothesis toString_ann : ∀ A, (A → string) → ann A → string.
Instance ToString_ann {A} `{ToString A} : ToString (ann A) :=
toString_ann (@toString A _).
Hypothesis toString_live : set var → string.
Instance ToString_live : ToString (set var) := toString_live.
Hypothesis toString_list : list var → string.
Instance ToString_list : ToString (list var) := toString_list.
Notation "S ´<<´ x ´<<´ y ´;´ s" := (let S := print_string S (x ++ "\n" ++ toString y ++ "\n\n") in s) (at level 1, left associativity).
Definition ensure_f P `{Computable P} (s: string) {A} (cont:status A) : status A :=
if [P] then cont else Error s.
Notation "´ensure´ P s ; cont " := (ensure_f P s cont)
(at level 20, P at level 0, s at level 0, cont at level 200, left associativity).
Definition toDeBruijn (ilin:ILN.nstmt) : status IL.stmt :=
ILN.labIndices ilin nil.
Definition toILF (ili:IL.stmt) : status IL.stmt :=
sdo lv <- livenessAnalysis ili;
ensure (TrueLiveness.true_live_sound Liveness.FunctionalAndImperative nil ili lv ∧ getAnn lv ⊆ freeVars ili) ("Liveness unsound (1)") ;
let ilid := DVE.compile nil ili lv in
let additional_params := additionalArguments ilid (DVE.compile_live ili lv ∅) in
ensure (Delocation.trs nil nil ilid (DVE.compile_live ili lv ∅) additional_params)
"Additional arguments insufficient";
Success (Delocation.compile nil ilid additional_params).
Definition optimize (s´:stmt) : status stmt :=
let s := rename_apart s´ in
sdo ALAE <- constantPropagationAnalysis s;
match ALAE with
| (AL, AEc) ⇒
let AE := (fun x ⇒ MapInterface.find x AEc) in
ensure (ConstantPropagation.cp_sound AE nil s)
"Constant propagation unsound";
ensure (∀ x, x ∈ freeVars s´ → AE x = None)
"Constant propagation makes no assumptions on free vars";
let s := ConstantPropagation.constantPropagate AE s in
sdo lv <- livenessAnalysis s;
ensure (TrueLiveness.true_live_sound Liveness.Functional nil s lv) "Liveness unsound (2)";
Success (DVE.compile nil s lv)
end.
Definition fromILF (s:stmt) : status stmt :=
let s_hoisted := EAE.compile s in
let s_renamed_apart := rename_apart s_hoisted in
let fv := freeVars s_renamed_apart in
sdo lv <- livenessAnalysis s_renamed_apart;
if [Liveness.live_sound Liveness.FunctionalAndImperative nil s_renamed_apart lv
∧ getAnn lv ⊆ freeVars s_hoisted] then
let fvl := to_list (getAnn lv) in
let ϱ := CMap.update_with_list fvl fvl (@MapInterface.empty var _ _ _) in
sdo ϱ´ <- AllocationAlgo.reg_assign Fresh.least_fresh s_renamed_apart lv ϱ;
let s_allocated := rename (CMap.findt ϱ´ 0) s_renamed_apart in
let s_lowered := ParallelMove.lower parallel_move
nil
s_allocated
(mapAnn (map (CMap.findt ϱ´ 0)) lv) in
s_lowered
else
Error "Liveness unsound.".
Opaque LivenessValidators.live_sound_dec.
Opaque DelocationValidator.trs_dec.
Lemma sim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: sim σ1 σ2 → sim σ2 σ3 → sim σ1 σ3.
Lemma bisim_sim {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2)
: Bisim.bisim σ1 σ2 → Sim.sim σ1 σ2.
Lemma toDeBruijn_correct (ilin:ILN.nstmt) s (E:onv val)
: toDeBruijn ilin = Success s
→ @sim _ ILN.statetype_I _ _
(ILN.I.labenv_empty, E, ilin)
(nil:list I.block, E, s).
Lemma labIndices_freeVars ilin s L
: ILN.labIndices ilin L = Success s
→ ILN.freeVars ilin = freeVars s.
Lemma toILF_correct (ili:IL.stmt) s (E:onv val)
: toILF ili = Success s
→ Delocation.defined_on (IL.freeVars ili) E
→ @sim _ statetype_I _ _ (nil, E, ili)
(nil:list F.block, E, s).
Lemma fromILF_correct (s s´:stmt) E
: fromILF s = Success s´
→ sim (nil:list F.block, E, s) (nil:list I.block, E, s´).
Lemma labelsDefined_rename_apart L s ϱ G
: LabelsDefined.labelsDefined s L
→ LabelsDefined.labelsDefined (snd (renameApart´ ϱ G s)) L.
Lemma optimize_correct (E:onv val) s s´
: optimize s = Success s´
→ LabelsDefined.labelsDefined s 0
→ sim (nil:list F.block, E, s) (nil:list F.block, E, s´).
End Compiler.
Print Assumptions toILF_correct.
Print Assumptions fromILF_correct.
Print Assumptions optimize_correct.
Extraction Inline bind Option.bind toString.
Extraction "extraction/lvc.ml" toILF fromILF AllocationAlgo.reg_assign optimize toDeBruijn.
Require Import Util AllInRel IL EnvTy RenameApart Sim Status Annotation.
Require CMap.
Require Liveness TrueLiveness LivenessValidators ParallelMove ILN LivenessAnalysis.
Require Coherence Delocation DelocationAlgo DelocationValidator Allocation AllocationAlgo.
Require CopyPropagation DVE EAE Alpha.
Require ConstantPropagation ConstantPropagationAnalysis.
Require Import ExtrOcamlBasic.
Require Import ExtrOcamlZBigInt.
Require Import ExtrOcamlNatInt.
Require Import String ExtrOcamlString.
Set Implicit Arguments.
Section Compiler.
Hypothesis ssa_construction : stmt → ann (option (set var)) × ann (list var).
Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).
Hypothesis first : ∀ (A:Type), A → ( A → status (A × bool)) → status A.
Definition livenessAnalysis :=
Analysis.fixpoint LivenessAnalysis.liveness_analysis first.
Definition constantPropagationAnalysis :=
Analysis.fixpoint ConstantPropagationAnalysis.constant_propagation_analysis first.
Definition additionalArguments s lv :=
fst (DelocationAlgo.computeParameters nil nil nil s lv).
Class ToString (T:Type) := toString : T → string.
Hypothesis OutputStream : Type.
Hypothesis print_string : OutputStream → string → OutputStream.
Hypothesis toString_nstmt : ILN.nstmt → string.
Instance ToString_nstmt : ToString ILN.nstmt := toString_nstmt.
Hypothesis toString_stmt : stmt → string.
Instance ToString_stmt : ToString stmt := toString_stmt.
Hypothesis toString_ann : ∀ A, (A → string) → ann A → string.
Instance ToString_ann {A} `{ToString A} : ToString (ann A) :=
toString_ann (@toString A _).
Hypothesis toString_live : set var → string.
Instance ToString_live : ToString (set var) := toString_live.
Hypothesis toString_list : list var → string.
Instance ToString_list : ToString (list var) := toString_list.
Notation "S ´<<´ x ´<<´ y ´;´ s" := (let S := print_string S (x ++ "\n" ++ toString y ++ "\n\n") in s) (at level 1, left associativity).
Definition ensure_f P `{Computable P} (s: string) {A} (cont:status A) : status A :=
if [P] then cont else Error s.
Notation "´ensure´ P s ; cont " := (ensure_f P s cont)
(at level 20, P at level 0, s at level 0, cont at level 200, left associativity).
Definition toDeBruijn (ilin:ILN.nstmt) : status IL.stmt :=
ILN.labIndices ilin nil.
Definition toILF (ili:IL.stmt) : status IL.stmt :=
sdo lv <- livenessAnalysis ili;
ensure (TrueLiveness.true_live_sound Liveness.FunctionalAndImperative nil ili lv ∧ getAnn lv ⊆ freeVars ili) ("Liveness unsound (1)") ;
let ilid := DVE.compile nil ili lv in
let additional_params := additionalArguments ilid (DVE.compile_live ili lv ∅) in
ensure (Delocation.trs nil nil ilid (DVE.compile_live ili lv ∅) additional_params)
"Additional arguments insufficient";
Success (Delocation.compile nil ilid additional_params).
Definition optimize (s´:stmt) : status stmt :=
let s := rename_apart s´ in
sdo ALAE <- constantPropagationAnalysis s;
match ALAE with
| (AL, AEc) ⇒
let AE := (fun x ⇒ MapInterface.find x AEc) in
ensure (ConstantPropagation.cp_sound AE nil s)
"Constant propagation unsound";
ensure (∀ x, x ∈ freeVars s´ → AE x = None)
"Constant propagation makes no assumptions on free vars";
let s := ConstantPropagation.constantPropagate AE s in
sdo lv <- livenessAnalysis s;
ensure (TrueLiveness.true_live_sound Liveness.Functional nil s lv) "Liveness unsound (2)";
Success (DVE.compile nil s lv)
end.
Definition fromILF (s:stmt) : status stmt :=
let s_hoisted := EAE.compile s in
let s_renamed_apart := rename_apart s_hoisted in
let fv := freeVars s_renamed_apart in
sdo lv <- livenessAnalysis s_renamed_apart;
if [Liveness.live_sound Liveness.FunctionalAndImperative nil s_renamed_apart lv
∧ getAnn lv ⊆ freeVars s_hoisted] then
let fvl := to_list (getAnn lv) in
let ϱ := CMap.update_with_list fvl fvl (@MapInterface.empty var _ _ _) in
sdo ϱ´ <- AllocationAlgo.reg_assign Fresh.least_fresh s_renamed_apart lv ϱ;
let s_allocated := rename (CMap.findt ϱ´ 0) s_renamed_apart in
let s_lowered := ParallelMove.lower parallel_move
nil
s_allocated
(mapAnn (map (CMap.findt ϱ´ 0)) lv) in
s_lowered
else
Error "Liveness unsound.".
Opaque LivenessValidators.live_sound_dec.
Opaque DelocationValidator.trs_dec.
Lemma sim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: sim σ1 σ2 → sim σ2 σ3 → sim σ1 σ3.
Lemma bisim_sim {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2)
: Bisim.bisim σ1 σ2 → Sim.sim σ1 σ2.
Lemma toDeBruijn_correct (ilin:ILN.nstmt) s (E:onv val)
: toDeBruijn ilin = Success s
→ @sim _ ILN.statetype_I _ _
(ILN.I.labenv_empty, E, ilin)
(nil:list I.block, E, s).
Lemma labIndices_freeVars ilin s L
: ILN.labIndices ilin L = Success s
→ ILN.freeVars ilin = freeVars s.
Lemma toILF_correct (ili:IL.stmt) s (E:onv val)
: toILF ili = Success s
→ Delocation.defined_on (IL.freeVars ili) E
→ @sim _ statetype_I _ _ (nil, E, ili)
(nil:list F.block, E, s).
Lemma fromILF_correct (s s´:stmt) E
: fromILF s = Success s´
→ sim (nil:list F.block, E, s) (nil:list I.block, E, s´).
Lemma labelsDefined_rename_apart L s ϱ G
: LabelsDefined.labelsDefined s L
→ LabelsDefined.labelsDefined (snd (renameApart´ ϱ G s)) L.
Lemma optimize_correct (E:onv val) s s´
: optimize s = Success s´
→ LabelsDefined.labelsDefined s 0
→ sim (nil:list F.block, E, s) (nil:list F.block, E, s´).
End Compiler.
Print Assumptions toILF_correct.
Print Assumptions fromILF_correct.
Print Assumptions optimize_correct.
Extraction Inline bind Option.bind toString.
Extraction "extraction/lvc.ml" toILF fromILF AllocationAlgo.reg_assign optimize toDeBruijn.