diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-30 14:48:33 +0000 |
commit | 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 (patch) | |
tree | f7adbc5ec8accc4bec3e38939bdf570a266f0e83 /backend/RTLgenaux.ml | |
parent | 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 (diff) | |
download | compcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.tar.gz compcert-6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9.zip |
Reorganized the development, modularizing away machine-dependent parts.
Started to merge the ARM code generator.
Started to add support for PowerPC/EABI.
Use ocamlbuild to construct executable from Caml files.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLgenaux.ml')
-rw-r--r-- | backend/RTLgenaux.ml | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml new file mode 100644 index 00000000..4c1fc05c --- /dev/null +++ b/backend/RTLgenaux.ml @@ -0,0 +1,72 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Camlcoq +open Switch +open CminorSel + +let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false + +module IntOrd = + struct + type t = Integers.int + let compare x y = + if Integers.Int.eq x y then 0 else + if Integers.Int.ltu x y then -1 else 1 + end + +module IntSet = Set.Make(IntOrd) + +let normalize_table tbl = + let rec norm seen = function + | [] -> [] + | Datatypes.Coq_pair(key, act) :: rem -> + if IntSet.mem key seen + then norm seen rem + else (key, act) :: norm (IntSet.add key seen) rem + in norm IntSet.empty tbl + +let compile_switch default table = + let sw = Array.of_list (normalize_table table) in + Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw; + let rec build lo hi minval maxval = + match hi - lo with + | 0 -> + CTaction default + | 1 -> + let (key, act) = sw.(lo) in + if Integers.Int.sub maxval minval = Integers.Int.zero + then CTaction act + else CTifeq(key, act, CTaction default) + | 2 -> + let (key1, act1) = sw.(lo) + and (key2, act2) = sw.(lo+1) in + CTifeq(key1, act1, + if Integers.Int.sub maxval minval = Integers.Int.one + then CTaction act2 + else CTifeq(key2, act2, CTaction default)) + | 3 -> + let (key1, act1) = sw.(lo) + and (key2, act2) = sw.(lo+1) + and (key3, act3) = sw.(lo+2) in + CTifeq(key1, act1, + CTifeq(key2, act2, + if Integers.Int.sub maxval minval = coqint_of_camlint 2l + then CTaction act3 + else CTifeq(key3, act3, CTaction default))) + | _ -> + let mid = (lo + hi) / 2 in + let (pivot, _) = sw.(mid) in + CTiflt(pivot, + build lo mid minval (Integers.Int.sub pivot Integers.Int.one), + build mid hi pivot maxval) + in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned |