From 9c9d516ba5df536d15bc27bed0a84fd8170fcdc0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 18 Feb 2021 13:22:09 +0100 Subject: Proof of Ocmp expansions without immediate and some drafts in comment --- riscV/Asmgenproof1.v | 2 +- riscV/ExpansionOracle.ml | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 0b1abe2a..35c5b9d6 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -377,7 +377,7 @@ Proof. rewrite <- Float32.cmp_swap. auto. Qed. -(* TODO UNUSUED ? Remark branch_on_X31: +(* TODO gourdinl UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 1e40b492..32c8731f 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -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)) (* TODO Maybe incorrect *) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) (* TODO gourdinl Maybe incorrect *) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -392,14 +392,14 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccompu\n"; exp := cond_int32u false c a1 a2 dest succ []; was_exp := true - (*| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> + | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u c a1 imm dest succ []; - was_exp := true*) + was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompl\n"; exp := cond_int64s false c a1 a2 dest succ []; @@ -408,14 +408,14 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccomplu\n"; exp := cond_int64u false c a1 a2 dest succ []; was_exp := true - (*| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> + | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u c a1 imm dest succ []; - was_exp := true*) + was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompf\n"; exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; -- cgit