diff options
Diffstat (limited to 'riscV/ExpansionOracle.ml')
-rw-r--r-- | riscV/ExpansionOracle.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index dc7f4b82..fa05d318 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -118,8 +118,8 @@ let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = let optR0 = make_optR0 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 + | 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 @@ -138,8 +138,8 @@ let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = let optR0 = make_optR0 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 + | 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 @@ -164,8 +164,8 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k = let cond_int32u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ()) @@ -196,8 +196,8 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k = let cond_int64u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k | Cle -> Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ()) @@ -327,7 +327,7 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = insn :: (if normal' then Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO Maybe incorrect *) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] |