diff options
Diffstat (limited to 'aarch64/Asmblockgen.v')
-rw-r--r-- | aarch64/Asmblockgen.v | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index e260bd69..325f238c 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -579,47 +579,47 @@ Definition cond_for_cond (cond: condition) := without setting then testing condition flags. *) Definition transl_cond_branch_default - (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) := + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := do ccode <- transl_cond c args k; - OK(ccode, PCtlFlow (Pbc (cond_for_cond c) lbl)). + OK(ccode, Pbc (cond_for_cond c) lbl). Definition transl_cond_branch - (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) := + (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*cf_instruction) := match args, c with | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) => if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz W r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbnz W r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) => if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz W r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbz W r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) => if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz X r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbnz X r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) => if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz X r1 lbl))) + then (do r1 <- ireg_of a1; OK (k, Pcbz X r1 lbl)) else transl_cond_branch_default c args lbl k | a1 :: nil, Cmaskzero n => match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz W r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz W r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasknotzero n => match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz W r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz W r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasklzero n => match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz X r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbz X r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | a1 :: nil, Cmasklnotzero n => match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz X r1 bit lbl)) + | Some bit => do r1 <- ireg_of a1; OK (k, Ptbnz X r1 bit lbl) | None => transl_cond_branch_default c args lbl k end | _, _ => @@ -1234,7 +1234,7 @@ Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res OK (make_epilogue f, PCtlFlow (Pbr r1 sig)) | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res)) | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl)) - | MBcond cond args lbl => transl_cond_branch cond args lbl nil + | MBcond cond args lbl => do (bc, c) <- transl_cond_branch cond args lbl nil; OK (bc, PCtlFlow c) | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA)) | MBjumptable arg tbl => do r <- ireg_of arg; OK (nil, PCtlFlow (Pbtbl r tbl)) @@ -1272,7 +1272,8 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: Program Definition make_prologue (f: Machblock.function) (k:bblocks) := {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi - storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; +(* storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; *) + ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil; exit := None |} :: k. (* Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b @@ -1290,7 +1291,7 @@ Definition transf_function (f: Machblock.function) : res Asmblock.function := else OK tf. Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) + transf_partial_fundef transf_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. |