Some progress in Asmblockgenproof

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.