From e72c8c4319e485d8e39c9ce085d21711fe781fed Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 31 Dec 2012 15:56:53 +0000 Subject: RTLgenaux: heuristic to orient if-then-else statements based on sizes. Makefile: coqchk notes git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2086 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenaux.ml | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 58 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 245b80cd..363bc2bd 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -10,11 +10,68 @@ (* *) (* *********************************************************************) +open Datatypes open Camlcoq open Switch open CminorSel -let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = false +(* Heuristic to orient if-then-else statements. + If "false" is returned generates a conditional branch to the "then" branch + and a fall-through to the "else" branch. + If "true" is returned generates a conditional branch to the "else" branch + and a fall-through to the "then" branch. + The fall-through behavior is generally slightly more efficient, + for average-case execution time as well as for worst-case. + The heuristic is based on an estimate of the sizes of the "then" and + "else" branches, in terms of rough number of instructions, and on + putting the bigger of the two branches in fall-through position. *) + +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) + | Elet(e1, e2) -> size_expr e1 + size_expr e2 + | Eletvar n -> 0 + +and size_exprs = function + | Enil -> 0 + | Econs(e1, el) -> size_expr e1 + size_exprs el + +let rec length_exprs = function + | Enil -> 0 + | Econs(e1, el) -> 1 + length_exprs el + +let size_eos = function + | Coq_inl e -> size_expr e + | Coq_inr id -> 0 + +let rec size_stmt = function + | Sskip -> 0 + | Sassign(id, a) -> size_expr a + | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src + | Scall(optid, sg, eos, args) -> + 3 + size_eos eos + size_exprs args + length_exprs args + | Stailcall(sg, eos, args) -> + 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) + | Sloop s -> 1 + 4 * size_stmt s + | Sblock s -> size_stmt s + | Sexit n -> 1 + | Sswitch(arg, tbl, dfl) -> 2 + size_expr arg + | Sreturn None -> 2 + | Sreturn (Some arg) -> 2 + size_expr arg + | Slabel(lbl, s) -> size_stmt s + | Sgoto lbl -> 1 + +let more_likely (c: Op.condition) (ifso: stmt) (ifnot: stmt) = + size_stmt ifso > size_stmt ifnot + +(* Compiling a switch table into a decision tree *) module IntOrd = struct -- cgit