From 17f519651feb4a09aa90c89c949469e8a5ab0e88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Aug 2014 07:52:12 +0000 Subject: - Support "switch" statements over 64-bit integers (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 127 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 94 insertions(+), 33 deletions(-) (limited to 'backend/Selection.v') diff --git a/backend/Selection.v b/backend/Selection.v index 9bd37ef5..cd17b9fd 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -27,6 +27,7 @@ Require Import AST. Require Import Errors. Require Import Integers. Require Import Globalenvs. +Require Import Switch. Require Cminor. Require Import Op. Require Import CminorSel. @@ -34,7 +35,8 @@ Require Import SelectOp. Require Import SelectDiv. Require Import SelectLong. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. +Local Open Scope error_monad_scope. (** Conversion of conditions *) @@ -203,60 +205,119 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind := end end. +(** Conversion of Cminor [switch] statements to decision trees. *) + +Parameter compile_switch: Z -> nat -> table -> comptree. + +Section SEL_SWITCH. + +Variable make_cmp_eq: expr -> Z -> expr. +Variable make_cmp_ltu: expr -> Z -> expr. +Variable make_sub: expr -> Z -> expr. +Variable make_to_int: expr -> expr. + +Fixpoint sel_switch (arg: nat) (t: comptree): exitexpr := + match t with + | CTaction act => + XEexit act + | CTifeq key act t' => + XEcondition (condexpr_of_expr (make_cmp_eq (Eletvar arg) key)) + (XEexit act) + (sel_switch arg t') + | CTiflt key t1 t2 => + XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar arg) key)) + (sel_switch arg t1) + (sel_switch arg t2) + | CTjumptable ofs sz tbl t' => + XElet (make_sub (Eletvar arg) ofs) + (XEcondition (condexpr_of_expr (make_cmp_ltu (Eletvar O) sz)) + (XEjumptable (make_to_int (Eletvar O)) tbl) + (sel_switch (S arg) t')) + end. + +End SEL_SWITCH. + +Definition sel_switch_int := + sel_switch + (fun arg n => comp Ceq arg (Eop (Ointconst (Int.repr n)) Enil)) + (fun arg n => compu Clt arg (Eop (Ointconst (Int.repr n)) Enil)) + (fun arg ofs => sub arg (Eop (Ointconst (Int.repr ofs)) Enil)) + (fun arg => arg). + +Definition sel_switch_long := + sel_switch + (fun arg n => cmpl Ceq arg (longconst (Int64.repr n))) + (fun arg n => cmplu Clt arg (longconst (Int64.repr n))) + (fun arg ofs => subl hf arg (longconst (Int64.repr ofs))) + lowlong. + (** Conversion from Cminor statements to Cminorsel statements. *) -Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt := +Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt := match s with - | Cminor.Sskip => Sskip - | Cminor.Sassign id e => Sassign id (sel_expr e) - | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs) + | Cminor.Sskip => OK Sskip + | Cminor.Sassign id e => OK (Sassign id (sel_expr e)) + | Cminor.Sstore chunk addr rhs => OK (store chunk (sel_expr addr) (sel_expr rhs)) | Cminor.Scall optid sg fn args => - match classify_call ge fn with + OK (match classify_call ge fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args) - end + end) | Cminor.Sbuiltin optid ef args => - Sbuiltin optid ef (sel_exprlist args) + OK (Sbuiltin optid ef (sel_exprlist args)) | Cminor.Stailcall sg fn args => - match classify_call ge fn with + OK (match classify_call ge fn with | Call_imm id => Stailcall sg (inr _ id) (sel_exprlist args) | _ => Stailcall sg (inl _ (sel_expr fn)) (sel_exprlist args) - end - | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2) + end) + | Cminor.Sseq s1 s2 => + do s1' <- sel_stmt ge s1; do s2' <- sel_stmt ge s2; + OK (Sseq s1' s2') | Cminor.Sifthenelse e ifso 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 - | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl - | Cminor.Sreturn None => Sreturn None - | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e)) - | Cminor.Slabel lbl body => Slabel lbl (sel_stmt ge body) - | Cminor.Sgoto lbl => Sgoto lbl + do ifso' <- sel_stmt ge ifso; do ifnot' <- sel_stmt ge ifnot; + OK (Sifthenelse (condexpr_of_expr (sel_expr e)) ifso' ifnot') + | Cminor.Sloop body => + do body' <- sel_stmt ge body; OK (Sloop body') + | Cminor.Sblock body => + do body' <- sel_stmt ge body; OK (Sblock body') + | Cminor.Sexit n => OK (Sexit n) + | Cminor.Sswitch false e cases dfl => + let t := compile_switch Int.modulus dfl cases in + if validate_switch Int.modulus dfl cases t + then OK (Sswitch (XElet (sel_expr e) (sel_switch_int O t))) + else Error (msg "Selection: bad switch (int)") + | Cminor.Sswitch true e cases dfl => + let t := compile_switch Int64.modulus dfl cases in + if validate_switch Int64.modulus dfl cases t + then OK (Sswitch (XElet (sel_expr e) (sel_switch_long O t))) + else Error (msg "Selection: bad switch (long)") + | Cminor.Sreturn None => OK (Sreturn None) + | Cminor.Sreturn (Some e) => OK (Sreturn (Some (sel_expr e))) + | Cminor.Slabel lbl body => + do body' <- sel_stmt ge body; OK (Slabel lbl body') + | Cminor.Sgoto lbl => OK (Sgoto lbl) end. End SELECTION. (** Conversion of functions. *) -Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : function := - mkfunction - f.(Cminor.fn_sig) - f.(Cminor.fn_params) - f.(Cminor.fn_vars) - f.(Cminor.fn_stackspace) - (sel_stmt hf ge f.(Cminor.fn_body)). +Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function := + do body' <- sel_stmt hf ge f.(Cminor.fn_body); + OK (mkfunction + f.(Cminor.fn_sig) + f.(Cminor.fn_params) + f.(Cminor.fn_vars) + f.(Cminor.fn_stackspace) + body'). -Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : fundef := - transf_fundef (sel_function hf ge) f. +Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef := + transf_partial_fundef (sel_function hf ge) f. (** Conversion of programs. *) -Local Open Scope error_monad_scope. - Definition sel_program (p: Cminor.program) : res program := let ge := Genv.globalenv p in - do hf <- get_helpers ge; OK (transform_program (sel_fundef hf ge) p). + do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p. -- cgit