diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-11 20:03:49 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-11 20:03:49 +0100 |
| commit | adf1bbcd5c356a0cb75c412357a3b7af23795f47 (patch) | |
| tree | 2e6a75bbee70c0377868861fc85976fccf017547 /riscV/ExpansionOracle.ml | |
| parent | c40646559461154e5190a4c887f9992f35eedb9f (diff) | |
| download | compcert-kvx-adf1bbcd5c356a0cb75c412357a3b7af23795f47.tar.gz compcert-kvx-adf1bbcd5c356a0cb75c412357a3b7af23795f47.zip | |
[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof
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 ] |