diff options
-rw-r--r-- | backend/Cminor.v | 4 | ||||
-rw-r--r-- | backend/CminorSel.v | 75 | ||||
-rw-r--r-- | backend/RTLgen.v | 41 | ||||
-rw-r--r-- | backend/RTLgenaux.ml | 17 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 160 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 91 | ||||
-rw-r--r-- | backend/SelectLong.vp | 46 | ||||
-rw-r--r-- | backend/SelectLongproof.v | 273 | ||||
-rw-r--r-- | backend/Selection.v | 16 | ||||
-rw-r--r-- | backend/Selectionproof.v | 32 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 6 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 9 | ||||
-rw-r--r-- | common/Values.v | 8 | ||||
-rw-r--r-- | ia32/SelectOp.vp | 4 | ||||
-rw-r--r-- | ia32/SelectOpproof.v | 9 | ||||
-rw-r--r-- | lib/Integers.v | 94 | ||||
-rw-r--r-- | runtime/Makefile | 4 | ||||
-rw-r--r-- | runtime/arm/i64_scmp.s | 56 | ||||
-rw-r--r-- | runtime/arm/i64_ucmp.s | 51 | ||||
-rw-r--r-- | runtime/ia32/i64_scmp.S | 58 | ||||
-rw-r--r-- | runtime/ia32/i64_ucmp.S | 52 | ||||
-rw-r--r-- | runtime/powerpc/i64_scmp.s | 72 | ||||
-rw-r--r-- | runtime/powerpc/i64_ucmp.s | 72 | ||||
-rw-r--r-- | runtime/test/test_int64.c | 29 |
25 files changed, 590 insertions, 691 deletions
diff --git a/backend/Cminor.v b/backend/Cminor.v index 3963e76c..6b36b4dc 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -309,8 +309,8 @@ Definition eval_binop | Ocmp c => Some (Val.cmp c arg1 arg2) | Ocmpu c => Some (Val.cmpu (Mem.valid_pointer m) c arg1 arg2) | Ocmpf c => Some (Val.cmpf c arg1 arg2) - | Ocmpl c => Some (Val.cmpl c arg1 arg2) - | Ocmplu c => Some (Val.cmplu c arg1 arg2) + | Ocmpl c => Val.cmpl c arg1 arg2 + | Ocmplu c => Val.cmplu c arg1 arg2 end. (** Evaluation of an expression: [eval_expr ge sp e m a v] diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 3538dda8..c80f424d 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -40,7 +40,7 @@ Inductive expr : Type := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr - | Econdition : condition -> exprlist -> expr -> expr -> expr + | Econdition : condexpr -> expr -> expr -> expr | Elet : expr -> expr -> expr | Eletvar : nat -> expr | Ebuiltin : external_function -> exprlist -> expr @@ -48,7 +48,12 @@ Inductive expr : Type := with exprlist : Type := | Enil: exprlist - | Econs: expr -> exprlist -> exprlist. + | Econs: expr -> exprlist -> exprlist + +with condexpr : Type := + | CEcond : condition -> exprlist -> condexpr + | CEcondition : condexpr -> condexpr -> condexpr -> condexpr + | CElet: expr -> condexpr -> condexpr. Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope. @@ -65,7 +70,7 @@ Inductive stmt : Type := | Stailcall: signature -> expr + ident -> exprlist -> stmt | Sbuiltin : option ident -> external_function -> exprlist -> stmt | Sseq: stmt -> stmt -> stmt - | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt + | Sifthenelse: condexpr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt @@ -161,11 +166,10 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_addressing ge sp addr vl = Some vaddr -> Mem.loadv chunk m vaddr = Some v -> eval_expr le (Eload chunk addr al) v - | eval_Econdition: forall le cond al b c vl vb v, - eval_exprlist le al vl -> - eval_condition cond vl m = Some vb -> - eval_expr le (if vb then b else c) v -> - eval_expr le (Econdition cond al b c) v + | eval_Econdition: forall le a b c va v, + eval_condexpr le a va -> + eval_expr le (if va then b else c) v -> + eval_expr le (Econdition a b c) v | eval_Elet: forall le a b v1 v2, eval_expr le a v1 -> eval_expr (v1 :: le) b v2 -> @@ -190,10 +194,25 @@ with eval_exprlist: letenv -> exprlist -> list val -> Prop := eval_exprlist le Enil nil | eval_Econs: forall le a1 al v1 vl, eval_expr le a1 v1 -> eval_exprlist le al vl -> - eval_exprlist le (Econs a1 al) (v1 :: vl). + eval_exprlist le (Econs a1 al) (v1 :: vl) + +with eval_condexpr: letenv -> condexpr -> bool -> Prop := + | eval_CEcond: forall le cond al vl vb, + eval_exprlist le al vl -> + eval_condition cond vl m = Some vb -> + eval_condexpr le (CEcond cond al) vb + | eval_CEcondition: forall le a b c va v, + eval_condexpr le a va -> + eval_condexpr le (if va then b else c) v -> + eval_condexpr le (CEcondition a b c) v + | eval_CElet: forall le a b v1 v2, + eval_expr le a v1 -> + eval_condexpr (v1 :: le) b v2 -> + eval_condexpr le (CElet a b) v2. -Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop - with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop. +Scheme eval_expr_ind3 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind3 := Minimality for eval_exprlist Sort Prop + with eval_condexpr_ind3 := Minimality for eval_condexpr Sort Prop. Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := | eval_eos_e: forall le e v, @@ -232,7 +251,7 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont) | Some sk => Some sk | None => find_label lbl s2 k end - | Sifthenelse cond al s1 s2 => + | Sifthenelse c s1 s2 => match find_label lbl s1 k with | Some sk => Some sk | None => find_label lbl s2 k @@ -302,10 +321,9 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sseq s1 s2) k sp e m) E0 (State f s1 (Kseq s2 k) sp e m) - | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b, - eval_exprlist sp e m nil al vl -> - eval_condition cond vl m = Some b -> - step (State f (Sifthenelse cond al s1 s2) k sp e m) + | step_ifthenelse: forall f c s1 s2 k sp e m b, + eval_condexpr sp e m nil c b -> + step (State f (Sifthenelse c s1 s2) k sp e m) E0 (State f (if b then s1 else s2) k sp e m) | step_loop: forall f s k sp e m, @@ -382,7 +400,7 @@ Inductive final_state: state -> int -> Prop := Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -Hint Constructors eval_expr eval_exprlist: evalexpr. +Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr. (** * Lifting of let-bound variables *) @@ -396,8 +414,8 @@ Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr := | Evar id => Evar id | Eop op bl => Eop op (lift_exprlist p bl) | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl) - | Econdition cond al b c => - Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c) + | Econdition a b c => + Econdition (lift_condexpr p a) (lift_expr p b) (lift_expr p c) | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c) | Eletvar n => if le_gt_dec p n then Eletvar (S n) else Eletvar n @@ -409,6 +427,13 @@ with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist := match a with | Enil => Enil | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl) + end + +with lift_condexpr (p: nat) (a: condexpr) {struct a}: condexpr := + match a with + | CEcond c al => CEcond c (lift_exprlist p al) + | CEcondition a b c => CEcondition (lift_condexpr p a) (lift_condexpr p b) (lift_condexpr p c) + | CElet a b => CElet (lift_expr p a) (lift_condexpr (S p) b) end. Definition lift (a: expr): expr := lift_expr O a. @@ -458,22 +483,28 @@ Lemma eval_lift_expr: eval_expr ge sp e m le' (lift_expr p a) v. Proof. intros until w. - apply (eval_expr_ind2 ge sp e m + apply (eval_expr_ind3 ge sp e m (fun le a v => forall p le', insert_lenv le p w le' -> eval_expr ge sp e m le' (lift_expr p a) v) (fun le al vl => forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); + eval_exprlist ge sp e m le' (lift_exprlist p al) vl) + (fun le a b => + forall p le', insert_lenv le p w le' -> + eval_condexpr ge sp e m le' (lift_condexpr p a) b)); simpl; intros; eauto with evalexpr. - eapply eval_Econdition; eauto. destruct vb; eauto. + eapply eval_Econdition; eauto. destruct va; eauto. eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. case (le_gt_dec p n); intro. apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. apply eval_Eletvar. eapply insert_lenv_lookup1; eauto. + + eapply eval_CEcondition; eauto. destruct va; eauto. + eapply eval_CElet; eauto. apply H2. constructor; auto. Qed. Lemma eval_lift: diff --git a/backend/RTLgen.v b/backend/RTLgen.v index f5e34e4b..193702e6 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -401,12 +401,10 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do rl <- alloc_regs map al; do no <- add_instr (Iload chunk addr rl rd nd); transl_exprlist map al rl no - | Econdition cond al b c => - do rl <- alloc_regs map al; + | Econdition a b c => do nfalse <- transl_expr map c rd nd; do ntrue <- transl_expr map b rd nd; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map a ntrue nfalse | Elet b c => do r <- new_reg; do nc <- transl_expr (add_letvar map r) c rd nd; @@ -435,6 +433,26 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) do no <- transl_exprlist map bs rs nd; transl_expr map b r no | _, _ => error (Errors.msg "RTLgen.transl_exprlist") + end + +(** Translation of a conditional expression. Branches to [ntrue] or + to [nfalse] depending on the truth value of the expression. *) + +with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) + {struct a} : mon node := + match a with + | CEcond c al => + do rl <- alloc_regs map al; + do nt <- add_instr (Icond c rl ntrue nfalse); + transl_exprlist map al rl nt + | CEcondition a b c => + do nc <- transl_condexpr map c ntrue nfalse; + do nb <- transl_condexpr map b ntrue nfalse; + transl_condexpr map a nb nc + | CElet b c => + do r <- new_reg; + do nc <- transl_condexpr (add_letvar map r) c ntrue nfalse; + transl_expr map b r nc end. (** Auxiliary for branch prediction. When compiling an if/then/else @@ -445,7 +463,7 @@ with transl_exprlist (map: mapping) (al: exprlist) (rl: list reg) (nd: node) no impact on program correctness. We delegate the choice to an external heuristic (written in OCaml), declared below. *) -Parameter more_likely: condition -> stmt -> stmt -> bool. +Parameter more_likely: condexpr -> stmt -> stmt -> bool. (** Auxiliary for translating [Sswitch] statements. *) @@ -545,18 +563,15 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; transl_stmt map s1 ns nexits ngoto nret rret - | Sifthenelse cond al strue sfalse => - do rl <- alloc_regs map al; - if more_likely cond strue sfalse then + | Sifthenelse c strue sfalse => + if more_likely c strue sfalse then do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map c ntrue nfalse else do ntrue <- transl_stmt map strue nd nexits ngoto nret rret; do nfalse <- transl_stmt map sfalse nd nexits ngoto nret rret; - do nt <- add_instr (Icond cond rl ntrue nfalse); - transl_exprlist map al rl nt + transl_condexpr map c ntrue nfalse | Sloop sbody => do n1 <- reserve_instr; do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret; @@ -611,7 +626,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state) {struct s} : labelmap * state := match s with | Sseq s1 s2 => reserve_labels s1 (reserve_labels s2 ms) - | Sifthenelse cond al s1 s2 => reserve_labels s1 (reserve_labels s2 ms) + | Sifthenelse c s1 s2 => reserve_labels s1 (reserve_labels s2 ms) | Sloop s1 => reserve_labels s1 ms | Sblock s1 => reserve_labels s1 ms | Slabel lbl s1 => alloc_label lbl (reserve_labels s1 ms) diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 150de5a2..75901027 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -30,8 +30,8 @@ let rec size_expr = function | Evar id -> 0 | Eop(op, args) -> 1 + size_exprs args | Eload(chunk, addr, args) -> 1 + size_exprs args - | Econdition(cond, args, e1, e2) -> - 1 + size_exprs args + max (size_expr e1) (size_expr e2) + | Econdition(ce, e1, e2) -> + 1 + size_condexpr ce + max (size_expr e1) (size_expr e2) | Elet(e1, e2) -> size_expr e1 + size_expr e2 | Eletvar n -> 0 | Ebuiltin(ef, el) -> 2 + size_exprs el @@ -41,6 +41,13 @@ and size_exprs = function | Enil -> 0 | Econs(e1, el) -> size_expr e1 + size_exprs el +and size_condexpr = function + | CEcond(c, args) -> size_exprs args + | CEcondition(c1, c2, c3) -> + 1 + size_condexpr c1 + size_condexpr c2 + size_condexpr c3 + | CElet(a, c) -> + size_expr a + size_condexpr c + let rec length_exprs = function | Enil -> 0 | Econs(e1, el) -> 1 + length_exprs el @@ -59,8 +66,8 @@ let rec size_stmt = function 3 + size_eos eos + size_exprs args + length_exprs args | Sbuiltin(optid, ef, args) -> 1 + size_exprs args | Sseq(s1, s2) -> size_stmt s1 + size_stmt s2 - | Sifthenelse(cond, args, s1, s2) -> - 1 + size_exprs args + max (size_stmt s1) (size_stmt s2) + | Sifthenelse(ce, s1, s2) -> + size_condexpr ce + max (size_stmt s1) (size_stmt s2) | Sloop s -> 1 + 4 * size_stmt s | Sblock s -> size_stmt s | Sexit n -> 1 @@ -70,7 +77,7 @@ let rec size_stmt = function | Slabel(lbl, s) -> size_stmt s | Sgoto lbl -> 1 -let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = +let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = size_stmt ifso > size_stmt ifnot (* Compiling a switch table into a decision tree *) diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index c3cae286..51f1f276 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -546,6 +546,19 @@ Definition transl_exprlist_prop /\ (forall r, In r pr -> rs'#r = rs#r) /\ Mem.extends m tm'. +Definition transl_condexpr_prop + (le: letenv) (a: condexpr) (v: bool) : Prop := + forall tm cs f map pr ns ntrue nfalse rs + (MWF: map_wf map) + (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) + (ME: match_env map e le rs) + (EXT: Mem.extends m tm), + exists rs', exists tm', + plus step tge (State cs f sp ns rs tm) E0 (State cs f sp (if v then ntrue else nfalse) rs' tm') + /\ match_env map e le rs' + /\ (forall r, In r pr -> rs'#r = rs#r) + /\ Mem.extends m tm'. + (** The correctness of the translation is a huge induction over the Cminor evaluation derivation for the source program. To keep the proof manageable, we put each case of the proof in a separate @@ -639,25 +652,22 @@ Proof. Qed. Lemma transl_expr_Econdition_correct: - forall (le : letenv) (cond : condition) (al: exprlist) (ifso ifnot : expr) - (vl: list val) (vcond : bool) (v : val), - eval_exprlist ge sp e m le al vl -> - transl_exprlist_prop le al vl -> - eval_condition cond vl m = Some vcond -> - eval_expr ge sp e m le (if vcond then ifso else ifnot) v -> - transl_expr_prop le (if vcond then ifso else ifnot) v -> - transl_expr_prop le (Econdition cond al ifso ifnot) v. + forall (le : letenv) (a: condexpr) (ifso ifnot : expr) + (va : bool) (v : val), + eval_condexpr ge sp e m le a va -> + transl_condexpr_prop le a va -> + eval_expr ge sp e m le (if va then ifso else ifnot) v -> + transl_expr_prop le (if va then ifso else ifnot) v -> + transl_expr_prop le (Econdition a ifso ifnot) v. Proof. - intros; red; intros; inv TE. inv H14. - exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. - assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst). - destruct vcond; auto. - exploit H3; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. + intros; red; intros; inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. + assert (tr_expr f.(fn_code) map pr (if va then ifso else ifnot) (if va then ntrue else nfalse) nd rd dst). + destruct va; auto. + exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. exists rs2; exists tm2. (* Exec *) - split. eapply star_trans. eexact EX1. - eapply star_left. eapply exec_Icond. eauto. eapply eval_condition_lessdef; eauto. reflexivity. - eexact EX2. reflexivity. traceEq. + split. eapply star_trans. apply plus_star. eexact EX1. eexact EX2. traceEq. (* Match-env *) split. assumption. (* Result value *) @@ -829,14 +839,85 @@ Proof. auto. Qed. +Lemma transl_condexpr_CEcond_correct: + forall le cond al vl vb, + eval_exprlist ge sp e m le al vl -> + transl_exprlist_prop le al vl -> + eval_condition cond vl m = Some vb -> + transl_condexpr_prop le (CEcond cond al) vb. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. + exists rs1; exists tm1. +(* Exec *) + split. eapply plus_right. eexact EX1. eapply exec_Icond. eauto. + eapply eval_condition_lessdef; eauto. auto. traceEq. +(* Match-env *) + split. assumption. +(* Other regs *) + split. assumption. +(* Mem *) + auto. +Qed. + +Lemma transl_condexpr_CEcondition_correct: + forall le a b c va v, + eval_condexpr ge sp e m le a va -> + transl_condexpr_prop le a va -> + eval_condexpr ge sp e m le (if va then b else c) v -> + transl_condexpr_prop le (if va then b else c) v -> + transl_condexpr_prop le (CEcondition a b c) v. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. + assert (tr_condition (fn_code f) map pr (if va then b else c) (if va then n2 else n3) ntrue nfalse). + destruct va; auto. + exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [OTHER2 EXT2]]]]]. + exists rs2; exists tm2. +(* Exec *) + split. eapply plus_trans. eexact EX1. eexact EX2. traceEq. +(* Match-env *) + split. assumption. +(* Other regs *) + split. intros. rewrite OTHER2; auto. +(* Mem *) + auto. +Qed. + +Lemma transl_condexpr_CElet_correct: + forall le a b v1 v2, + eval_expr ge sp e m le a v1 -> + transl_expr_prop le a v1 -> + eval_condexpr ge sp e m (v1 :: le) b v2 -> + transl_condexpr_prop (v1 :: le) b v2 -> + transl_condexpr_prop le (CElet a b) v2. +Proof. + intros; red; intros. inv TE. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. + assert (map_wf (add_letvar map r)). + eapply add_letvar_wf; eauto. + exploit H2; eauto. eapply match_env_bind_letvar; eauto. + intros [rs2 [tm2 [EX2 [ME3 [OTHER2 EXT2]]]]]. + exists rs2; exists tm2. +(* Exec *) + split. eapply star_plus_trans. eexact EX1. eexact EX2. traceEq. +(* Match-env *) + split. eapply match_env_unbind_letvar; eauto. +(* Other regs *) + split. intros. rewrite OTHER2; auto. +(* Mem *) + auto. +Qed. + Theorem transl_expr_correct: forall le a v, eval_expr ge sp e m le a v -> transl_expr_prop le a v. Proof - (eval_expr_ind2 ge sp e m + (eval_expr_ind3 ge sp e m transl_expr_prop transl_exprlist_prop + transl_condexpr_prop transl_expr_Evar_correct transl_expr_Eop_correct transl_expr_Eload_correct @@ -846,16 +927,20 @@ Proof transl_expr_Ebuiltin_correct transl_expr_Eexternal_correct transl_exprlist_Enil_correct - transl_exprlist_Econs_correct). + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). Theorem transl_exprlist_correct: forall le a v, eval_exprlist ge sp e m le a v -> transl_exprlist_prop le a v. Proof - (eval_exprlist_ind2 ge sp e m + (eval_exprlist_ind3 ge sp e m transl_expr_prop transl_exprlist_prop + transl_condexpr_prop transl_expr_Evar_correct transl_expr_Eop_correct transl_expr_Eload_correct @@ -865,7 +950,33 @@ Proof transl_expr_Ebuiltin_correct transl_expr_Eexternal_correct transl_exprlist_Enil_correct - transl_exprlist_Econs_correct). + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). + +Theorem transl_condexpr_correct: + forall le a v, + eval_condexpr ge sp e m le a v -> + transl_condexpr_prop le a v. +Proof + (eval_condexpr_ind3 ge sp e m + transl_expr_prop + transl_exprlist_prop + transl_condexpr_prop + transl_expr_Evar_correct + transl_expr_Eop_correct + transl_expr_Eload_correct + transl_expr_Econdition_correct + transl_expr_Elet_correct + transl_expr_Eletvar_correct + transl_expr_Ebuiltin_correct + transl_expr_Eexternal_correct + transl_exprlist_Enil_correct + transl_exprlist_Econs_correct + transl_condexpr_CEcond_correct + transl_condexpr_CEcondition_correct + transl_condexpr_CElet_correct). End CORRECTNESS_EXPR. @@ -877,7 +988,7 @@ Fixpoint size_stmt (s: stmt) : nat := match s with | Sskip => 0 | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1) - | Sifthenelse cond el s1 s2 => (size_stmt s1 + size_stmt s2 + 1) + | Sifthenelse c s1 s2 => (size_stmt s1 + size_stmt s2 + 1) | Sloop s1 => (size_stmt s1 + 1) | Sblock s1 => (size_stmt s1 + 1) | Sexit n => 0 @@ -1206,11 +1317,10 @@ Proof. econstructor; eauto. econstructor; eauto. (* ifthenelse *) - inv TS. inv H13. - exploit transl_exprlist_correct; eauto. intros [rs' [tm' [A [B [C [D E]]]]]]. + inv TS. + exploit transl_condexpr_correct; eauto. intros [rs' [tm' [A [B [C D]]]]]. econstructor; split. - left. eapply plus_right. eexact A. eapply exec_Icond; eauto. - eapply eval_condition_lessdef; eauto. traceEq. + left. eexact A. destruct b; econstructor; eauto. (* loop *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index d8d5dc8c..c82c0510 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -703,11 +703,11 @@ Inductive tr_expr (c: code): c!n1 = Some (Iload chunk addr rl rd nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Eload chunk addr al) ns nd rd dst - | tr_Econdition: forall map pr cond bl ifso ifnot ns nd rd ntrue nfalse dst, - tr_condition c map pr cond bl ns ntrue nfalse -> + | tr_Econdition: forall map pr a ifso ifnot ns nd rd ntrue nfalse dst, + tr_condition c map pr a ns ntrue nfalse -> tr_expr c map pr ifso ntrue nd rd dst -> tr_expr c map pr ifnot nfalse nd rd dst -> - tr_expr c map pr (Econdition cond bl ifso ifnot) ns nd rd dst + tr_expr c map pr (Econdition a ifso ifnot) ns nd rd dst | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> tr_expr c map pr b1 ns n1 r None -> @@ -730,17 +730,27 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eexternal id sg al) ns nd rd dst -(** [tr_condition c map pr cond al ns ntrue nfalse rd] holds if the graph [c], +(** [tr_condition c map pr a ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth - value of the Cminor conditional expression [cond] and terminate + value of the Cminor conditional expression [a] and terminate on node [ntrue] if the condition holds and on node [nfalse] otherwise. *) with tr_condition (c: code): - mapping -> list reg -> condition -> exprlist -> node -> node -> node -> Prop := + mapping -> list reg -> condexpr -> node -> node -> node -> Prop := | tr_CEcond: forall map pr cond bl ns ntrue nfalse n1 rl, tr_exprlist c map pr bl ns n1 rl -> c!n1 = Some (Icond cond rl ntrue nfalse) -> - tr_condition c map pr cond bl ns ntrue nfalse + tr_condition c map pr (CEcond cond bl) ns ntrue nfalse + | tr_CEcondition: forall map pr a1 a2 a3 ns ntrue nfalse n2 n3, + tr_condition c map pr a1 ns n2 n3 -> + tr_condition c map pr a2 n2 ntrue nfalse -> + tr_condition c map pr a3 n3 ntrue nfalse -> + tr_condition c map pr (CEcondition a1 a2 a3) ns ntrue nfalse + | tr_CElet: forall map pr a b ns ntrue nfalse r n1, + ~reg_in_map map r -> + tr_expr c map pr a ns n1 r None -> + tr_condition c (add_letvar map r) pr b n1 ntrue nfalse -> + tr_condition c map pr (CElet a b) ns ntrue nfalse (** [tr_exprlist c map pr exprs ns nd rds] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the values @@ -840,11 +850,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret - | tr_Sifthenelse: forall cond al strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, tr_stmt c map strue ntrue nd nexits ngoto nret rret -> tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> - tr_condition c map nil cond al ns ntrue nfalse -> - tr_stmt c map (Sifthenelse cond al strue sfalse) ns nd nexits ngoto nret rret + tr_condition c map nil a ns ntrue nfalse -> + tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend, tr_stmt c map sbody nloop nend nexits ngoto nret rret -> c!ns = Some(Inop nloop) -> @@ -914,9 +924,9 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> - forall map pr cond al ns ntrue nfalse, - tr_condition s1.(st_code) map pr cond al ns ntrue nfalse -> - tr_condition s2.(st_code) map pr cond al ns ntrue nfalse + forall map pr a ns ntrue nfalse, + tr_condition s1.(st_code) map pr a ns ntrue nfalse -> + tr_condition s2.(st_code) map pr a ns ntrue nfalse with tr_exprlist_incr: forall s1 s2, state_incr s1 s2 -> forall map pr al ns nd rl, @@ -962,7 +972,14 @@ with transl_exprlist_charact: (OK: target_regs_ok map pr al rl) (VALID1: regs_valid pr s) (VALID2: regs_valid rl s), - tr_exprlist s'.(st_code) map pr al ns nd rl. + tr_exprlist s'.(st_code) map pr al ns nd rl + +with transl_condexpr_charact: + forall a map ntrue nfalse s ns s' pr INCR + (TR: transl_condexpr map a ntrue nfalse s = OK ns s' INCR) + (WF: map_valid map s) + (VALID: regs_valid pr s), + tr_condition s'.(st_code) map pr a ns ntrue nfalse. Proof. induction a; intros; try (monadInv TR); saturateTrans. @@ -981,12 +998,12 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) inv OK. - econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + econstructor. + eauto with rtlg. apply tr_expr_incr with s1; auto. eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. + apply tr_expr_incr with s0; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1031,6 +1048,22 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. apply regs_valid_cons. apply VALID2. auto with coqlib. auto. red; intros; apply VALID2; auto with coqlib. + +(* Conditional expressions *) + induction a; intros; try (monadInv TR); saturateTrans. + + (* CEcond *) + econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. + (* CEcondition *) + econstructor; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + apply tr_condition_incr with s0; eauto with rtlg. + (* CElet *) + econstructor; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. + apply tr_condition_incr with s1; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + apply add_letvar_valid; eauto with rtlg. Qed. (** A variant of [transl_expr_charact], for use when the destination @@ -1056,10 +1089,10 @@ Proof. eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) econstructor; eauto with rtlg. - econstructor; eauto with rtlg. eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s2; auto. - eapply IHa1; eauto 2 with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. + eapply IHa1; eauto 2 with rtlg. + apply tr_expr_incr with s0; auto. eapply IHa2; eauto 2 with rtlg. (* Elet *) econstructor. eapply new_reg_not_in_map; eauto with rtlg. @@ -1227,21 +1260,19 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply IHstmt1; eauto with rtlg. (* Sifthenelse *) - destruct (more_likely c stmt1 stmt2); monadInv EQ0. + destruct (more_likely c stmt1 stmt2); monadInv TR. econstructor. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. econstructor. - apply tr_stmt_incr with s1; auto. + apply tr_stmt_incr with s0; auto. eapply IHstmt1; eauto with rtlg. - apply tr_stmt_incr with s2; auto. + apply tr_stmt_incr with s1; auto. eapply IHstmt2; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. (* Sloop *) econstructor. apply tr_stmt_incr with s1; auto. diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 8eb32c38..aad9d60e 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -41,9 +41,7 @@ Record helper_functions : Type := mk_helper_functions { i64_umod: ident; (**r unsigned remainder *) i64_shl: ident; (**r shift left *) i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_scmp: ident; (**r signed comparison *) - i64_ucmp: ident (**r unsigned comparison *) + i64_sar: ident (**r shift right signed *) }. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). @@ -51,7 +49,6 @@ Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). -Definition sig_ll_i := mksignature (Tlong :: Tlong :: nil) (Some Tint). Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). Section SELECT. @@ -291,6 +288,12 @@ Definition cmpl_eq_zero (e: expr) := Definition cmpl_ne_zero (e: expr) := splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)). +Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))). + Definition cmplu (c: comparison) (e1 e2: expr) := match c with | Ceq => @@ -301,15 +304,23 @@ Definition cmplu (c: comparison) (e1 e2: expr) := if is_longconst_zero e2 then cmpl_ne_zero e1 else cmpl_ne_zero (xorl e1 e2) - | _ => - comp c (Eexternal hf.(i64_ucmp) sig_ll_i (e1 ::: e2 ::: Enil)) - (Eop (Ointconst Int.zero) Enil) + | Clt => + cmplu_gen Clt Clt e1 e2 + | Cle => + cmplu_gen Clt Cle e1 e2 + | Cgt => + cmplu_gen Cgt Cgt e1 e2 + | Cge => + cmplu_gen Cgt Cge e1 e2 end. +Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := + splitlong2 e1 e2 (fun h1 l1 h2 l2 => + Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil)) + (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil)) + (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))). + Definition cmpl (c: comparison) (e1 e2: expr) := - let default := - comp c (Eexternal hf.(i64_scmp) sig_ll_i (e1 ::: e2 ::: Enil)) - (Eop (Ointconst Int.zero) Enil) in match c with | Ceq => if is_longconst_zero e2 @@ -322,13 +333,15 @@ Definition cmpl (c: comparison) (e1 e2: expr) := | Clt => if is_longconst_zero e2 then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) - else default + else cmpl_gen Clt Clt e1 e2 + | Cle => + cmpl_gen Clt Cle e1 e2 + | Cgt => + cmpl_gen Cgt Cgt e1 e2 | Cge => if is_longconst_zero e2 then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil) - else default - | _ => - default + else cmpl_gen Cgt Cge e1 e2 end. End SELECT. @@ -359,10 +372,7 @@ Definition get_helpers (ge: Cminor.genv): res helper_functions := do i64_shl <- get_helper ge "__i64_shl" sig_li_l ; do i64_shr <- get_helper ge "__i64_shr" sig_li_l ; do i64_sar <- get_helper ge "__i64_sar" sig_li_l ; - do i64_scmp <- get_helper ge "__i64_scmp" sig_ll_i ; - do i64_ucmp <- get_helper ge "__i64_ucmp" sig_ll_i ; OK (mk_helper_functions i64_dtos i64_dtou i64_stod i64_utod i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod - i64_shl i64_shr i64_sar - i64_scmp i64_ucmp). + i64_shl i64_shr i64_sar). diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index aca05bf2..3eeeeb5d 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -61,11 +61,7 @@ Definition i64_helpers_correct (hf: helper_functions) : Prop := /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z) /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y)) /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y)) - /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)) - /\(forall c x y, exists z, helper_implements hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - /\(forall c x y, exists z, helper_implements hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero). + /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)). End HELPERS. @@ -180,6 +176,22 @@ Proof. destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto. Qed. +Lemma eval_splitlong_strict: + forall le a f va v, + eval_expr ge sp e m le a (Vlong va) -> + (forall le a1 a2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le (f a1 a2) v) -> + eval_expr ge sp e m le (splitlong a f) v. +Proof. + intros until v. + unfold splitlong. case (splitlong_match a); intros. +- InvEval. destruct v1; simpl in H; try discriminate. destruct v0; inv H. + apply H0. rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto. +- EvalOp. apply H0; EvalOp. +Qed. + Lemma eval_splitlong2: forall le a b f va vb sem, (forall le a1 a2 b1 b2 x1 x2 y1 y2, @@ -198,7 +210,7 @@ Lemma eval_splitlong2: exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v. Proof. intros until sem; intros EXEC UNDEF. - unfold splitlong2. case (splitlong2_match a); intros. + unfold splitlong2. case (splitlong2_match a b); intros. - InvEval. subst va vb. exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]]. exists v; split; auto. @@ -240,6 +252,35 @@ Proof. erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto. Qed. +Lemma eval_splitlong2_strict: + forall le a b f va vb v, + eval_expr ge sp e m le a (Vlong va) -> + eval_expr ge sp e m le b (Vlong vb) -> + (forall le a1 a2 b1 b2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) -> + eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) -> + eval_expr ge sp e m le (f a1 a2 b1 b2) v) -> + eval_expr ge sp e m le (splitlong2 a b f) v. +Proof. + assert (INV: forall v1 v2 n, + Val.longofwords v1 v2 = Vlong n -> v1 = Vint(Int64.hiword n) /\ v2 = Vint(Int64.loword n)). + { + intros. destruct v1; simpl in H; try discriminate. destruct v2; inv H. + rewrite Int64.hi_ofwords; rewrite Int64.lo_ofwords; auto. + } + intros until v. + unfold splitlong2. case (splitlong2_match a b); intros. +- InvEval. exploit INV. eexact H. intros [EQ1 EQ2]. exploit INV. eexact H0. intros [EQ3 EQ4]. + subst. auto. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- EvalOp. apply H1; EvalOp. +Qed. + Lemma is_longconst_sound: forall le a x n, is_longconst a = Some n -> @@ -891,35 +932,49 @@ Proof. Qed. Lemma eval_cmpl_eq_zero: - unary_constructor_sound cmpl_eq_zero (fun v => Val.cmpl Ceq v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Ceq x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_eq_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Ceq). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Ceq). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (Int64.eq x Int64.zero); inv B2; auto. Qed. Lemma eval_cmpl_ne_zero: - unary_constructor_sound cmpl_ne_zero (fun v => Val.cmpl Cne v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Cne x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_ne_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Cne). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Cne). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (negb (Int64.eq x Int64.zero)); inv B2; auto. +Qed. + +Lemma eval_cmplu_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmplu_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmplu_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark int64_eq_xor: @@ -933,44 +988,57 @@ Proof. auto. Qed. -Theorem eval_cmplu: forall c, binary_constructor_sound (cmplu hf c) (Val.cmplu c). +Theorem eval_cmplu: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmplu c x y = Some v -> + eval_expr ge sp e m le (cmplu c a b) v. Proof. - intros; red; intros. unfold cmplu. - set (default := comp c (Eexternal (i64_ucmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmplu c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmplu in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. +- (* Clt *) + exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmplu_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. auto. +- (* Cgt *) + exploit (eval_cmplu_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cge *) + exploit (eval_cmplu_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. rewrite Int.eq_sym. auto. +Qed. + +Lemma eval_cmpl_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmpl_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmp ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmpl_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark decompose_cmpl_lt_zero: @@ -991,72 +1059,61 @@ Proof. vm_compute. intuition congruence. Qed. -Theorem eval_cmpl: forall c, binary_constructor_sound (cmpl hf c) (Val.cmpl c). +Theorem eval_cmpl: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmpl c x y = Some v -> + eval_expr ge sp e m le (cmpl c a b) v. Proof. - intros; red; intros. unfold cmpl. - set (default := comp c (Eexternal (i64_scmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmpl c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmpl in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. - (* Clt *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1. inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Clt). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2. simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (Int.lt (Int64.hiword x) Int.zero); inv B2; auto. ++ exploit (eval_cmpl_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmpl_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. auto. +- (* Cgt *) + exploit (eval_cmpl_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. - (* Cge *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Cge). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2; simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (negb (Int.lt (Int64.hiword x) Int.zero)); inv B2; auto. ++ exploit (eval_cmpl_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. rewrite Int.eq_sym. auto. Qed. End CMCONSTR. diff --git a/backend/Selection.v b/backend/Selection.v index 7964feb1..edc63cd4 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -37,10 +37,12 @@ Open Local Scope cminorsel_scope. (** Conversion of conditions *) -Function condition_of_expr (e: expr) : condition * exprlist := +Function condexpr_of_expr (e: expr) : condexpr := match e with - | Eop (Ocmp c) el => (c, el) - | _ => (Ccompuimm Cne Int.zero, e ::: Enil) + | Eop (Ocmp c) el => CEcond c el + | Econdition a b c => CEcondition a (condexpr_of_expr b) (condexpr_of_expr c) + | Elet a b => CElet a (condexpr_of_expr b) + | _ => CEcond (Ccompuimm Cne Int.zero) (e ::: Enil) end. (** Conversion of loads and stores *) @@ -133,8 +135,8 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr := | Cminor.Ocmp c => comp c arg1 arg2 | Cminor.Ocmpu c => compu c arg1 arg2 | Cminor.Ocmpf c => compf c arg1 arg2 - | Cminor.Ocmpl c => cmpl hf c arg1 arg2 - | Cminor.Ocmplu c => cmplu hf c arg1 arg2 + | Cminor.Ocmpl c => cmpl c arg1 arg2 + | Cminor.Ocmplu c => cmplu c arg1 arg2 end. (** Conversion from Cminor expression to Cminorsel expressions *) @@ -205,8 +207,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := end | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) | Cminor.Sifthenelse e ifso ifnot => - let (cond, args) := condition_of_expr (sel_expr e) in - Sifthenelse cond args (sel_stmt ge ifso) (sel_stmt ge ifnot) + Sifthenelse (condexpr_of_expr (sel_expr e)) + (sel_stmt ge ifso) (sel_stmt ge ifnot) | Cminor.Sloop body => Sloop (sel_stmt ge body) | Cminor.Sblock body => Sblock (sel_stmt ge body) | Cminor.Sexit n => Sexit n diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 525a29d4..93a5c513 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -117,8 +117,6 @@ Proof. repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end); intros; try (eapply helper_implements_preserved; eauto); try (eapply builtin_implements_preserved; eauto). - exploit H14; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto. - exploit H15; eauto. intros [z [A B]]. exists z; split; eauto. eapply helper_implements_preserved; eauto. Qed. Section CMCONSTR. @@ -127,22 +125,22 @@ Variable sp: val. Variable e: env. Variable m: mem. -Lemma eval_condition_of_expr: - forall le a v b, +Lemma eval_condexpr_of_expr: + forall a le v b, eval_expr tge sp e m le a v -> Val.bool_of_val v b -> - match condition_of_expr a with (cond, args) => - exists vl, - eval_exprlist tge sp e m le args vl /\ - eval_condition cond vl m = Some b - end. + eval_condexpr tge sp e m le (condexpr_of_expr a) b. Proof. - intros until a. functional induction (condition_of_expr a); intros. + intros until a. functional induction (condexpr_of_expr a); intros. (* compare *) - inv H. exists vl; split; auto. + inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. +(* condition *) + inv H. econstructor; eauto. destruct va; eauto. +(* let *) + inv H. econstructor; eauto. (* default *) - exists (v :: nil); split. constructor. auto. constructor. + econstructor. constructor. eauto. constructor. simpl. inv H0. auto. auto. Qed. @@ -248,8 +246,8 @@ Proof. apply eval_comp; auto. apply eval_compu; auto. apply eval_compf; auto. - apply eval_cmpl; auto. - apply eval_cmplu; auto. + exists v; split; auto. eapply eval_cmpl; eauto. + exists v; split; auto. eapply eval_cmplu; eauto. Qed. End CMCONSTR. @@ -495,7 +493,6 @@ Proof. destruct (find_label lbl (sel_stmt hf ge s1) (Kseq (sel_stmt hf ge s2) k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) - destruct (condition_of_expr (sel_expr hf e)) as [cond args]. simpl. exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; destruct (find_label lbl (sel_stmt hf ge s1) k') as [[sy ky] | ]; @@ -594,11 +591,8 @@ Proof. (* Sifthenelse *) exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. - exploit eval_condition_of_expr; eauto. - destruct (condition_of_expr (sel_expr hf a)) as [cond args]. - intros [vl' [C D]]. left; exists (State (sel_function hf ge f) (if b then sel_stmt hf ge s1 else sel_stmt hf ge s2) k' sp e' m'); split. - econstructor; eauto. + econstructor; eauto. eapply eval_condexpr_of_expr; eauto. constructor; auto. destruct b; auto. (* Sloop *) left; econstructor; split. constructor. constructor; auto. constructor; auto. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 9d3d2550..2df8b932 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1612,9 +1612,11 @@ Proof. (* cmpf *) inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. (* cmpl *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. + unfold Val.cmpl in *. inv H0; inv H1; simpl in H; inv H. + econstructor; split. simpl; eauto. apply val_inject_val_of_bool. (* cmplu *) - inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool. + unfold Val.cmplu in *. inv H0; inv H1; simpl in H; inv H. + econstructor; split. simpl; eauto. apply val_inject_val_of_bool. Qed. (** * Correctness of Cminor construction functions *) diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 3ab286e4..c45e0946 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -92,6 +92,8 @@ Definition make_cmp_ne_zero (e: expr) := | Ebinop (Ocmp c) e1 e2 => e | Ebinop (Ocmpu c) e1 e2 => e | Ebinop (Ocmpf c) e1 e2 => e + | Ebinop (Ocmpl c) e1 e2 => e + | Ebinop (Ocmplu c) e1 e2 => e | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 00ed1f64..de3b8df0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -220,6 +220,12 @@ Proof. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. unfold Val.cmp in H0. eauto. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. unfold Val.cmpl in H6. + destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. + inv H. econstructor; eauto. rewrite H6. decEq. decEq. + simpl in H6. unfold Val.cmplu in H6. + destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity. Qed. Lemma make_cast_int_correct: @@ -300,8 +306,7 @@ Proof. destruct (Int.eq i Int.zero); simpl; constructor. exists Vtrue; split. econstructor; eauto with cshm. constructor. (* long *) - econstructor; split. econstructor; eauto with cshm. simpl. eauto. - unfold Val.cmpl, Val.cmpl_bool. simpl. + econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. Qed. diff --git a/common/Values.v b/common/Values.v index f917e0b1..76fb2302 100644 --- a/common/Values.v +++ b/common/Values.v @@ -595,11 +595,11 @@ Definition cmpu (c: comparison) (v1 v2: val): val := Definition cmpf (c: comparison) (v1 v2: val): val := of_optbool (cmpf_bool c v1 v2). -Definition cmpl (c: comparison) (v1 v2: val): val := - of_optbool (cmpl_bool c v1 v2). +Definition cmpl (c: comparison) (v1 v2: val): option val := + option_map of_bool (cmpl_bool c v1 v2). -Definition cmplu (c: comparison) (v1 v2: val): val := - of_optbool (cmplu_bool c v1 v2). +Definition cmplu (c: comparison) (v1 v2: val): option val := + option_map of_bool (cmplu_bool c v1 v2). End COMPARISONS. diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 7f79a4f7..2d1ab483 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -423,14 +423,14 @@ Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := Elet e (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil) - (Econdition (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil) + (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil)) (intoffloat (Eletvar 1)) (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat. Definition floatofintu (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e - (Econdition (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil) + (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil)) (floatofint (Eletvar O)) (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)). diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 1569ad6f..8c9c7e64 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -735,8 +735,8 @@ Proof. constructor. auto. econstructor. eauto. econstructor. instantiate (1 := Vfloat fm). EvalOp. - eapply eval_Econdition with (vb := Float.cmp Clt f fm). - eauto with evalexpr. auto. + eapply eval_Econdition with (va := Float.cmp Clt f fm). + eauto with evalexpr. destruct (Float.cmp Clt f fm) eqn:?. exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ. EvalOp. simpl. rewrite EQ; auto. @@ -768,9 +768,8 @@ Proof. set (fm := Float.floatofintu Float.ox8000_0000). assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)). constructor. auto. - eapply eval_Econdition with (vb := Int.ltu i Float.ox8000_0000). - constructor. eauto. constructor. - simpl. auto. + eapply eval_Econdition with (va := Int.ltu i Float.ox8000_0000). + eauto with evalexpr. destruct (Int.ltu i Float.ox8000_0000) eqn:?. rewrite Float.floatofintu_floatofint_1; auto. unfold floatofint. EvalOp. diff --git a/lib/Integers.v b/lib/Integers.v index b2598bbf..5eb4c82d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -815,6 +815,15 @@ Proof. intros. generalize (eq_spec x y); case (eq x y); intros; congruence. Qed. +Theorem eq_signed: + forall x y, eq x y = if zeq (signed x) (signed y) then true else false. +Proof. + intros. predSpec eq eq_spec x y. + subst x. rewrite zeq_true; auto. + destruct (zeq (signed x) (signed y)); auto. + elim H. rewrite <- (repr_signed x). rewrite <- (repr_signed y). congruence. +Qed. + (** ** Properties of addition *) Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y). @@ -4121,47 +4130,62 @@ Qed. Lemma decompose_ltu: forall xh xl yh yl, - ltu (ofwords xh xl) (ofwords yh yl) = Int.ltu xh yh || Int.eq xh yh && Int.ltu xl yl. -Proof. - intros. unfold ltu. rewrite ! ofwords_add'. unfold Int.ltu. - destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). - simpl. apply zlt_true. - change (two_power_pos 32) with Int.modulus. + ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh. +Proof. + intros. unfold ltu. rewrite ! ofwords_add'. unfold Int.ltu, Int.eq. + destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). + rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). + apply zlt_true; omega. + apply zlt_false; omega. + change (two_p 32) with Int.modulus. generalize (Int.unsigned_range xl) (Int.unsigned_range yl). - change Int.modulus with 4294967296. omega. - unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)); simpl. - rewrite e. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). - apply zlt_true. omega. - apply zlt_false. omega. - apply zlt_false. - change (two_power_pos 32) with Int.modulus. - generalize (Int.unsigned_range xl) (Int.unsigned_range yl). - change Int.modulus with 4294967296. omega. + change Int.modulus with 4294967296. intros. + destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). + apply zlt_true; omega. + apply zlt_false; omega. Qed. -Lemma decompose_lt: +Lemma decompose_leu: forall xh xl yh yl, - lt (ofwords xh xl) (ofwords yh yl) = Int.lt xh yh || Int.eq xh yh && Int.ltu xl yl. + negb (ltu (ofwords yh yl) (ofwords xh xl)) = + if Int.eq xh yh then negb (Int.ltu yl xl) else Int.ltu xh yh. Proof. - intros. unfold lt. rewrite ! ofwords_add''. unfold Int.lt. - destruct (zlt (Int.signed xh) (Int.signed yh)). - simpl. apply zlt_true. - change (two_power_pos 32) with Int.modulus. - generalize (Int.unsigned_range xl) (Int.unsigned_range yl). - change Int.modulus with 4294967296. omega. - replace (Int.eq xh yh) with (proj_sumbool(zeq (Int.signed xh) (Int.signed yh))). - destruct (zeq (Int.signed xh) (Int.signed yh)); simpl. - rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). - apply zlt_true. omega. - apply zlt_false. omega. - apply zlt_false. - change (two_power_pos 32) with Int.modulus. + intros. rewrite decompose_ltu. rewrite Int.eq_sym. + unfold Int.eq. destruct (zeq (Int.unsigned xh) (Int.unsigned yh)). + auto. + unfold Int.ltu. destruct (zlt (Int.unsigned xh) (Int.unsigned yh)). + rewrite zlt_false by omega; auto. + rewrite zlt_true by omega; auto. +Qed. + +Lemma decompose_lt: + forall xh xl yh yl, + lt (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.lt xh yh. +Proof. + intros. unfold lt. rewrite ! ofwords_add''. rewrite Int.eq_signed. + destruct (zeq (Int.signed xh) (Int.signed yh)). + rewrite e. unfold Int.ltu. destruct (zlt (Int.unsigned xl) (Int.unsigned yl)). + apply zlt_true; omega. + apply zlt_false; omega. + change (two_p 32) with Int.modulus. generalize (Int.unsigned_range xl) (Int.unsigned_range yl). - change Int.modulus with 4294967296. omega. - predSpec Int.eq Int.eq_spec xh yh. - subst yh. unfold proj_sumbool; apply zeq_true. - destruct (zeq (Int.signed xh) (Int.signed yh)); auto. - elim H. rewrite <- (Int.repr_signed xh). rewrite <- (Int.repr_signed yh). congruence. + change Int.modulus with 4294967296. intros. + unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). + apply zlt_true; omega. + apply zlt_false; omega. +Qed. + +Lemma decompose_le: + forall xh xl yh yl, + negb (lt (ofwords yh yl) (ofwords xh xl)) = + if Int.eq xh yh then negb (Int.ltu yl xl) else Int.lt xh yh. +Proof. + intros. rewrite decompose_lt. rewrite Int.eq_sym. + rewrite Int.eq_signed. destruct (zeq (Int.signed xh) (Int.signed yh)). + auto. + unfold Int.lt. destruct (zlt (Int.signed xh) (Int.signed yh)). + rewrite zlt_false by omega; auto. + rewrite zlt_true by omega; auto. Qed. End Int64. diff --git a/runtime/Makefile b/runtime/Makefile index 3565fb18..a2af8d58 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -2,8 +2,8 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall INCLUDES= -OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_scmp.o i64_sdiv.o i64_shl.o \ - i64_shr.o i64_smod.o i64_stod.o i64_ucmp.o i64_udivmod.o i64_udiv.o \ +OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ + i64_shr.o i64_smod.o i64_stod.o i64_udivmod.o i64_udiv.o \ i64_umod.o i64_utod.o LIB=libcompcert.a diff --git a/runtime/arm/i64_scmp.s b/runtime/arm/i64_scmp.s deleted file mode 100644 index 144a13c9..00000000 --- a/runtime/arm/i64_scmp.s +++ /dev/null @@ -1,56 +0,0 @@ -@ ***************************************************************** -@ -@ The Compcert verified compiler -@ -@ Xavier Leroy, INRIA Paris-Rocquencourt -@ -@ Copyright (c) 2013 Institut National de Recherche en Informatique et -@ en Automatique. -@ -@ Redistribution and use in source and binary forms, with or without -@ modification, are permitted provided that the following conditions are met: -@ * Redistributions of source code must retain the above copyright -@ notice, this list of conditions and the following disclaimer. -@ * Redistributions in binary form must reproduce the above copyright -@ notice, this list of conditions and the following disclaimer in the -@ documentation and/or other materials provided with the distribution. -@ * Neither the name of the <organization> nor the -@ names of its contributors may be used to endorse or promote products -@ derived from this software without specific prior written permission. -@ -@ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -@ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -@ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -@ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -@ HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -@ EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -@ PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -@ PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -@ LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -@ NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -@ -@ ********************************************************************* - -@ Helper functions for 64-bit integer arithmetic. ARM version. - - .text - -@@@ Signed comparison - - .global __i64_scmp -__i64_scmp: - cmp r0, r2 @ compare low words (unsigned) - moveq r0, #0 @ res = 0 if eq - movhi r0, #1 @ res = 1 if unsigned higher - mvnlo r0, #0 @ res = -1 if unsigned lower - cmp r1, r3 @ compare high words (signed) - addgt r0, r0, #2 @ res += 2 if signed greater - sublt r0, r0, #2 @ res -= 2 if signed less - @ here, r0 = 0 if X == Y - @ r0 = -3, -2, -1 if X < Y - @ r0 = 1, 2, 3 if X > Y - bx lr - .type __i64_scmp, %function - .size __i64_scmp, . - __i64_scmp - diff --git a/runtime/arm/i64_ucmp.s b/runtime/arm/i64_ucmp.s deleted file mode 100644 index 51a5fdb0..00000000 --- a/runtime/arm/i64_ucmp.s +++ /dev/null @@ -1,51 +0,0 @@ -@ ***************************************************************** -@ -@ The Compcert verified compiler -@ -@ Xavier Leroy, INRIA Paris-Rocquencourt -@ -@ Copyright (c) 2013 Institut National de Recherche en Informatique et -@ en Automatique. -@ -@ Redistribution and use in source and binary forms, with or without -@ modification, are permitted provided that the following conditions are met: -@ * Redistributions of source code must retain the above copyright -@ notice, this list of conditions and the following disclaimer. -@ * Redistributions in binary form must reproduce the above copyright -@ notice, this list of conditions and the following disclaimer in the -@ documentation and/or other materials provided with the distribution. -@ * Neither the name of the <organization> nor the -@ names of its contributors may be used to endorse or promote products -@ derived from this software without specific prior written permission. -@ -@ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -@ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -@ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -@ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -@ HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -@ EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -@ PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -@ PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -@ LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -@ NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -@ -@ ********************************************************************* - -@ Helper functions for 64-bit integer arithmetic. ARM version. - - .text - -@@@ Unsigned comparison - - .global __i64_ucmp -__i64_ucmp: - cmp r1, r3 @ compare high words - cmpeq r0, r2 @ if equal, compare low words instead - moveq r0, #0 @ res = 0 if eq - movhi r0, #1 @ res = 1 if unsigned higher - mvnlo r0, #0 @ res = -1 if unsigned lower - bx lr - .type __i64_ucmp, %function - .size __i64_ucmp, . - __i64_ucmp - diff --git a/runtime/ia32/i64_scmp.S b/runtime/ia32/i64_scmp.S deleted file mode 100644 index 93ef2c28..00000000 --- a/runtime/ia32/i64_scmp.S +++ /dev/null @@ -1,58 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the <organization> nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Signed comparison - -FUNCTION(__i64_scmp) - movl 8(%esp), %eax // compare high words (signed) - cmpl 16(%esp), %eax - je 1f // if different, - setg %al // extract result - setl %dl - subb %dl, %al - movsbl %al, %eax - ret -1: movl 4(%esp), %eax // if high words equal, - cmpl 12(%esp), %eax // compare low words (unsigned) - seta %al // and extract result - setb %dl - subb %dl, %al - movsbl %al, %eax - ret -ENDFUNCTION(__i64_scmp) - diff --git a/runtime/ia32/i64_ucmp.S b/runtime/ia32/i64_ucmp.S deleted file mode 100644 index 34159866..00000000 --- a/runtime/ia32/i64_ucmp.S +++ /dev/null @@ -1,52 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the <organization> nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Unsigned comparison - -FUNCTION(__i64_ucmp) - movl 8(%esp), %eax // compare high words - cmpl 16(%esp), %eax - jne 1f // if high words equal, - movl 4(%esp), %eax // compare low words - cmpl 12(%esp), %eax -1: seta %al // AL = 1 if >, 0 if <= - setb %dl // DL = 1 if <, 0 if >= - subb %dl, %al // AL = 0 if same, 1 if >, -1 if < - movsbl %al, %eax - ret -ENDFUNCTION(__i64_ucmp) diff --git a/runtime/powerpc/i64_scmp.s b/runtime/powerpc/i64_scmp.s deleted file mode 100644 index 87811e03..00000000 --- a/runtime/powerpc/i64_scmp.s +++ /dev/null @@ -1,72 +0,0 @@ -# ***************************************************************** -# -# The Compcert verified compiler -# -# Xavier Leroy, INRIA Paris-Rocquencourt -# -# Copyright (c) 2013 Institut National de Recherche en Informatique et -# en Automatique. -# -# Redistribution and use in source and binary forms, with or without -# modification, are permitted provided that the following conditions are met: -# * Redistributions of source code must retain the above copyright -# notice, this list of conditions and the following disclaimer. -# * Redistributions in binary form must reproduce the above copyright -# notice, this list of conditions and the following disclaimer in the -# documentation and/or other materials provided with the distribution. -# * Neither the name of the <organization> nor the -# names of its contributors may be used to endorse or promote products -# derived from this software without specific prior written permission. -# -# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -# -# ********************************************************************* - -# Helper functions for 64-bit integer arithmetic. PowerPC version. - - .text - -### Signed comparison - - .balign 16 - .globl __i64_scmp -__i64_scmp: - cmpw cr0, r3, r5 # compare high words (signed) - cmplw cr1, r4, r6 # compare low words (unsigned) - mfcr r0 -# At this point, the bits of r0 are as follow: -# bit 31: XH < YH -# bit 30: XH > YH -# bit 27: XL > YL -# bit 26: XL < YL - rlwinm r3, r0, 0, 0, 1 # r3 = r0 & 0xC000_0000 - srawi r3, r3, 24 # r4 = r4 >>s 28 -# r3 = -0x80 if XH < YH -# = 0x40 if XH > YH -# = 0 if XH = YH - rlwinm r4, r0, 4, 0, 1 # r4 = (r0 << 4) & 0xC000_0000 - srawi r4, r4, 28 # r4 = r4 >>s 28 -# r4 = -8 if XL < YL -# = 4 if XL > YL -# = 0 if XL = YL - add r3, r3, r4 -# r3 = -0x80 or -0x80 - 8 or -0x80 + 4 or -8 if X < Y -# (in all cases, r3 < 0 if X < Y) -# = 0x40 or 0x40 - 8 or 0x40 + 4 or 4 if X > Y -# (in all cases, r3 > 0 if X > Y) -# = 0 if X = Y - blr - .type __i64_scmp, @function - .size __i64_scmp, .-__i64_scmp - -
\ No newline at end of file diff --git a/runtime/powerpc/i64_ucmp.s b/runtime/powerpc/i64_ucmp.s deleted file mode 100644 index 708bc74f..00000000 --- a/runtime/powerpc/i64_ucmp.s +++ /dev/null @@ -1,72 +0,0 @@ -# ***************************************************************** -# -# The Compcert verified compiler -# -# Xavier Leroy, INRIA Paris-Rocquencourt -# -# Copyright (c) 2013 Institut National de Recherche en Informatique et -# en Automatique. -# -# Redistribution and use in source and binary forms, with or without -# modification, are permitted provided that the following conditions are met: -# * Redistributions of source code must retain the above copyright -# notice, this list of conditions and the following disclaimer. -# * Redistributions in binary form must reproduce the above copyright -# notice, this list of conditions and the following disclaimer in the -# documentation and/or other materials provided with the distribution. -# * Neither the name of the <organization> nor the -# names of its contributors may be used to endorse or promote products -# derived from this software without specific prior written permission. -# -# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT -# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -# -# ********************************************************************* - -# Helper functions for 64-bit integer arithmetic. PowerPC version. - - .text - -### Unsigned comparison - - .balign 16 - .globl __i64_ucmp -__i64_ucmp: - cmplw cr0, r3, r5 # compare high words (unsigned) - cmplw cr1, r4, r6 # compare low words (unsigned) - mfcr r0 -# At this point, the bits of r0 are as follow: -# bit 31: XH < YH -# bit 30: XH > YH -# bit 27: XL > YL -# bit 26: XL < YL - rlwinm r3, r0, 0, 0, 1 # r3 = r0 & 0xC000_0000 - srawi r3, r3, 24 # r4 = r4 >>s 28 -# r3 = -0x80 if XH < YH -# = 0x40 if XH > YH -# = 0 if XH = YH - rlwinm r4, r0, 4, 0, 1 # r4 = (r0 << 4) & 0xC000_0000 - srawi r4, r4, 28 # r4 = r4 >>s 28 -# r4 = -8 if XL < YL -# = 4 if XL > YL -# = 0 if XL = YL - add r3, r3, r4 -# r3 = -0x80 or -0x80 - 8 or -0x80 + 4 or -8 if X < Y -# (in all cases, r3 < 0 if X < Y) -# = 0x40 or 0x40 - 8 or 0x40 + 4 or 4 if X > Y -# (in all cases, r3 > 0 if X > Y) -# = 0 if X = Y - blr - .type __i64_ucmp, @function - .size __i64_ucmp, .-__i64_ucmp - -
\ No newline at end of file diff --git a/runtime/test/test_int64.c b/runtime/test/test_int64.c index 49e732ad..0a7dfc45 100644 --- a/runtime/test/test_int64.c +++ b/runtime/test/test_int64.c @@ -50,9 +50,6 @@ extern u64 __i64_shl(u64 x, unsigned amount); extern u64 __i64_shr(u64 x, unsigned amount); extern s64 __i64_sar(s64 x, unsigned amount); -extern int __i64_ucmp(u64 x, u64 y); -extern int __i64_scmp(s64 x, s64 y); - extern double __i64_utod(u64 x); extern double __i64_stod(s64 x); extern u64 __i64_dtou(double d); @@ -140,32 +137,6 @@ static void test1(u64 x, u64 y) if (t != (s64) x >> i) error++, printf("%016llx >>s %d = %016llx, expected %016llx\n", x, i, t, (s64) x >> i); - i = __i64_ucmp(x, y); - if (x == y) { - if (! (i == 0)) - error++, printf("ucmp(%016llx, %016llx) = %d, expected 0\n", x, y, i); - } - else if (x < y) { - if (! (i < 0)) - error++, printf("ucmp(%016llx, %016llx) = %d, expected < 0\n", x, y, i); - } else { - if (! (i > 0)) - error++, printf("ucmp(%016llx, %016llx) = %d, expected > 0\n", x, y, i); - } - - i = __i64_scmp(x, y); - if (x == y) { - if (! (i == 0)) - error++, printf("scmp(%016llx, %016llx) = %d, expected 0\n", x, y, i); - } - else if ((s64)x < (s64)y) { - if (! (i < 0)) - error++, printf("scmp(%016llx, %016llx) = %d, expected < 0\n", x, y, i); - } else { - if (! (i > 0)) - error++, printf("scmp(%016llx, %016llx) = %d, expected > 0\n", x, y, i); - } - f = __i64_utod(x); g = (double) x; if (f != g) |