From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- scheduling/BTL_Scheduler.v | 42 ++++++++++++++++++++---------------------- 1 file changed, 20 insertions(+), 22 deletions(-) (limited to 'scheduling/BTL_Scheduler.v') diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index e7d2b37f..a3053add 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -60,35 +60,33 @@ Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res uni end end. -Definition check_symbolic_simu (f1 f2: BTL.function): res unit := - check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). - -Lemma check_symbolic_simu_rec_input_equiv lpc: forall f1 f2 x, - check_symbolic_simu_rec f1 f2 lpc = OK x -> - lpc = (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))) -> - equiv_input_regs f1 f2. +Definition erase_input_regs f1 f2 := + let code := PTree.map (fun pc ibf => + let oibf := match (fn_code f1)!pc with + | None => ibf + | Some oibf => oibf + end in + let regs := oibf.(input_regs) in + {| entry:= ibf.(entry); input_regs := regs; binfo := ibf.(binfo) |}) (fn_code f2) in + BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2). + +Lemma erase_input_regs_correct f1 f2 f3: + erase_input_regs f1 f2 = f3 -> + equiv_input_regs f1 f3. Proof. + unfold erase_input_regs; destruct f3; simpl; intros. + unfold equiv_input_regs; intuition auto. simpl. Admitted. -(* - unfold equiv_input_regs; induction lpc; simpl; intros f1 f2 x X EQL1. - - destruct (map _ _) eqn:EQL2; inv X; intuition; - symmetry in EQL1; apply map_eq_nil in EQL1; apply map_eq_nil in EQL2. - + destruct (fn_code f1), (fn_code f2); simpl in *; auto. - inv EQL2. - unfold PTree.elements in EQL1. - + admit. - + - destruct ((fn_code f1) ! a), ((fn_code f2) ! a); monadInv X. - eapply IHlpc; eauto. -Qed. - *) + +Definition check_symbolic_simu (f1 f2: BTL.function): res unit := + (*let f3 := erase_input_regs f1 f2 in*) + check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). Lemma check_symbolic_simu_input_equiv x f1 f2: check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. Proof. unfold check_symbolic_simu; simpl; intros X. - eapply check_symbolic_simu_rec_input_equiv; eauto. -Qed. +Admitted. Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x, check_symbolic_simu_rec f1 f2 lpc = OK x -> -- cgit