diff options
| -rw-r--r-- | src/hls/GiblePargen.v | 12 | ||||
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 9 |
2 files changed, 16 insertions, 5 deletions
diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 2c7bfc8..0462e28 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -238,7 +238,7 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest (f #r (Reg r)) (seq_app (pred_ret (Eop op)) (merge (list_translation rl f)))); Some (pred, f #r (Reg r) <- pruned) - | RBload p chunk addr rl r => + | RBload p chunk addr rl r => do pruned <- prune_predicated (app_predicated (dfltp p ∧ pred) @@ -277,6 +277,16 @@ Definition update (fop : pred_op * forest) (i : instr): option (pred_op * forest Some (new_p, f <-e pruned) end. +Definition remember_expr (f : forest) (lst: list pred_expr) (i : instr): list pred_expr := + match i with + | RBnop => lst + | RBop p op rl r => (f #r (Reg r)) :: lst + | RBload p chunk addr rl r => (f #r (Reg r)) :: lst + | RBstore p chunk addr rl r => (f #r Mem) :: lst + | RBsetpred p' c args p => lst + | RBexit p c => lst + end. + (*| Implementing which are necessary to show the correctness of the translation validation by showing that there aren't any more effects in the resultant RTLPar diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index ebb2744..93b1778 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -67,7 +67,7 @@ Context (prog: GibleSeq.program) (tprog : GiblePar.program). Let ge : GibleSeq.genv := Globalenvs.Genv.globalenv prog. Let tge : GiblePar.genv := Globalenvs.Genv.globalenv tprog. -Lemma sem_equiv_execution : +(*Lemma sem_equiv_execution : forall sp x i i' ti cf x' ti', abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> @@ -81,7 +81,7 @@ Lemma sem_exists_execution : abstract_sequence x = Some x' -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf). -Proof. Admitted. +Proof. Admitted. *) Lemma abstr_seq_reverse_correct : forall sp x i i' ti cf x', @@ -91,9 +91,10 @@ Lemma abstr_seq_reverse_correct : exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) /\ state_lessdef i' ti'. Proof. - intros. exploit sem_exists_execution; eauto; simplify. +(* intros. exploit sem_exists_execution; eauto; simplify. eauto using sem_equiv_execution. -Qed. +Qed. *) + intros. (*| Proof Sketch: |