a more general way to manage special registers before introducing SP

1 files changed, 61 insertions, 60 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index c03e0d03..16f1ee4b 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -66,7 +66,7 @@ let find_or_addnmove op args rd succ map_consts not_final =
       if not_final then node := !node - 1;
       Sr (P.of_int r)
   | None ->
-      if not (List.exists (fun a -> a = rd) args) && not_final then
+      if (not (List.exists (fun a -> a = rd) args)) && not_final then
         Hashtbl.add map_consts sop (p2i rd);
       Si (Iop (op, args, rd, succ))
 
@@ -208,131 +208,132 @@ let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
 
 let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 
-let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None
+let make_optR is_x0 is_inv =
+  if is_x0 then if is_inv then Some X0_L else Some X0_R else None
 
 let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Ceq -> Icond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
 
 let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Icond (CEbequw optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Icond (CEbneuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Ceq -> Icond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k
 
 let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Ceq -> Icond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k
 
 let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> Icond (CEbequl optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cne -> Icond (CEbneul optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k
-  | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k
-  | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Ceq -> Icond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k
 
 let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ]
-  | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ]
-  | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ]
+  | Ceq -> [ Iop (OEseqw optR, [ a1; a2 ], dest, succ) ]
+  | Cne -> [ Iop (OEsnew optR, [ a1; a2 ], dest, succ) ]
+  | Clt -> [ Iop (OEsltw optR, [ a1; a2 ], dest, succ) ]
   | Cle ->
       let r = r2pi () in
-      let op = OEsltw optR0 in
+      let op = OEsltw optR in
       let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
-  | Cgt -> [ Iop (OEsltw optR0, [ a2; a1 ], dest, succ) ]
+  | Cgt -> [ Iop (OEsltw optR, [ a2; a1 ], dest, succ) ]
   | Cge ->
       let r = r2pi () in
-      let op = OEsltw optR0 in
+      let op = OEsltw optR in
       let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
 
 let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ]
-  | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ]
-  | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ]
+  | Ceq -> [ Iop (OEsequw optR, [ a1; a2 ], dest, succ) ]
+  | Cne -> [ Iop (OEsneuw optR, [ a1; a2 ], dest, succ) ]
+  | Clt -> [ Iop (OEsltuw optR, [ a1; a2 ], dest, succ) ]
   | Cle ->
       let r = r2pi () in
-      let op = OEsltuw optR0 in
+      let op = OEsltuw optR in
       let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
-  | Cgt -> [ Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) ]
+  | Cgt -> [ Iop (OEsltuw optR, [ a2; a1 ], dest, succ) ]
   | Cge ->
       let r = r2pi () in
-      let op = OEsltuw optR0 in
+      let op = OEsltuw optR in
       let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
 
 let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ]
-  | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ]
-  | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ]
+  | Ceq -> [ Iop (OEseql optR, [ a1; a2 ], dest, succ) ]
+  | Cne -> [ Iop (OEsnel optR, [ a1; a2 ], dest, succ) ]
+  | Clt -> [ Iop (OEsltl optR, [ a1; a2 ], dest, succ) ]
   | Cle ->
       let r = r2pi () in
-      let op = OEsltl optR0 in
+      let op = OEsltl optR in
       let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
-  | Cgt -> [ Iop (OEsltl optR0, [ a2; a1 ], dest, succ) ]
+  | Cgt -> [ Iop (OEsltl optR, [ a2; a1 ], dest, succ) ]
   | Cge ->
       let r = r2pi () in
-      let op = OEsltl optR0 in
+      let op = OEsltl optR in
       let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
 
 let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
-  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ]
-  | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ]
-  | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ]
+  | Ceq -> [ Iop (OEsequl optR, [ a1; a2 ], dest, succ) ]
+  | Cne -> [ Iop (OEsneul optR, [ a1; a2 ], dest, succ) ]
+  | Clt -> [ Iop (OEsltul optR, [ a1; a2 ], dest, succ) ]
   | Cle ->
       let r = r2pi () in
-      let op = OEsltul optR0 in
+      let op = OEsltul optR in
       let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
       fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
-  | Cgt -> [ Iop (OEsltul optR0, [ a2; a1 ], dest, succ) ]
+  | Cgt -> [ Iop (OEsltul optR, [ a2; a1 ], dest, succ) ]
   | Cge ->
       let r = r2pi () in
-      let op = OEsltul optR0 in
+      let op = OEsltul optR in
       let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
       let ht = build_head_tuple [] sv in
       let r' = unzip_head_tuple ht r in
@@ -481,8 +482,8 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts =
   let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in
   insn
   ::
-  (if normal' then [ Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) ]
-  else [ Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info) ])
+  (if normal' then [ Icond (CEbnew (Some X0_R), [ r; r ], succ1, succ2, info) ]
+  else [ Icond (CEbeqw (Some X0_R), [ r; r ], succ1, succ2, info) ])
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]