diff options
Diffstat (limited to 'aarch64/Asmblockgen.v')
-rw-r--r-- | aarch64/Asmblockgen.v | 40 |
1 files changed, 28 insertions, 12 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index d68cd7ac..96e7db4b 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -1159,11 +1159,11 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := | _ => false end. -Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):= +Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := match il with - | nil => OK (k) + | nil => OK (nil) | i1 :: il' => - do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k; + do k1 <- transl_basic_code f il' (it1_is_parent it1p i1); transl_instr_basic f i1 it1p k1 end. @@ -1196,12 +1196,29 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio (* XXX: the simulation proof may be complex with this pattern. We may fix this later *) Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks := - match non_empty_bblockb bdy ex with - | true => {| header := ll; body:= bdy; exit := ex |} :: nil - | false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil + match ex with + | None => + match bdy with + | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil + | _ => {| header := ll; body:= bdy; exit := None |} :: nil + end + | _ => + match bdy with + | nil => {| header := ll; body:= nil; exit := ex |} :: nil + | _ => {| header := ll; body:= bdy; exit := ex |} :: nil + end end. -Obligation 1. - rewrite <- Heq_anonymous. constructor. +Next Obligation. + induction bdy. congruence. + simpl. auto. +Qed. +Next Obligation. + destruct ex. simpl. auto. + congruence. +Qed. +Next Obligation. + induction bdy. congruence. + simpl. auto. Qed. Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) := @@ -1227,10 +1244,9 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : end. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := - let stub := false in - do (bdy, ex) <- transl_exit f fb.(Machblock.exit); - do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy; - OK (cons_bblocks fb.(Machblock.header) bdy' ex) + do (bdy2, ex) <- transl_exit f fb.(Machblock.exit); + do bdy1 <- transl_basic_code f fb.(Machblock.body) ep; + OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) . Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) := |