diff options
Diffstat (limited to 'scheduling/RTLpathSE_theory.v')
| -rw-r--r-- | scheduling/RTLpathSE_theory.v | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index 4c492ecd..eec0bc51 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -1627,13 +1627,9 @@ Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop := /\ eqlive_reg alive is1.(irs) is2.(irs) /\ is1.(imem) = is2.(imem). -Definition istate_simu f (srce: PTree.t node) is1 is2: Prop := +Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop := if is1.(icontinue) then - (* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à - ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David) - Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière - sur la dernière instruction du superblock. *) - istate_simulive (fun _ => True) srce is1 is2 + istate_simulive (fun r => Regset.In r outframe) srce is1 is2 else exists path, f.(fn_path)!(is1.(ipc)) = Some path /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2 @@ -1651,10 +1647,10 @@ Record simu_proof_context {f1: RTLpath.function} := { Arguments simu_proof_context: clear implicits. (* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *) -Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) (st1 st2: sistate) (ctx: simu_proof_context f): Prop := +Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop := forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 -> exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2 - /\ istate_simu f dm is1 is2. + /\ istate_simu f dm outframe is1 is2. Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop := | Sleft_simu sv1 sv2: @@ -1885,13 +1881,14 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) -> sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)). -Definition sstate_simu dm f (s1 s2: sstate) (ctx: simu_proof_context f): Prop := - sistate_simu dm f s1.(internal) s2.(internal) ctx - /\ forall is1, +Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop := + sistate_simu dm f outframe s1.(internal) s2.(internal) ctx + /\ forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 -> is1.(icontinue) = true -> sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final). Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop := forall st1, sexec f1 pc1 = Some st1 -> - exists st2, sexec f2 pc2 = Some st2 /\ forall ctx, sstate_simu dm f1 st1 st2 ctx. + exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2 + /\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx. |