From 5c84fd4adbcd8a63cc29fb0286cb46f18abde55c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 17:11:47 +0000 Subject: Expand 64-bit integer comparisons into 32-bit integer comparisons. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 7964feb..edc63cd 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 -- cgit v1.2.3