blob: c0eab04fbae730f0808943537821e1525a90e066 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** Useful functions for pretty-printers *)
open Printf
open Camlcoq
open AST
let name_of_type = function
| Tint -> "int"
| Tfloat -> "float"
| Tlong -> "long"
| Tsingle -> "single"
| Tany32 -> "any32"
| Tany64 -> "any64"
let name_of_chunk = function
| Mint8signed -> "int8s"
| Mint8unsigned -> "int8u"
| Mint16signed -> "int16s"
| Mint16unsigned -> "int16u"
| Mint32 -> "int32"
| Mint64 -> "int64"
| Mfloat32 -> "float32"
| Mfloat64 -> "float64"
| Many32 -> "any32"
| Many64 -> "any64"
let name_of_external = function
| EF_external(name, sg) -> sprintf "extern %S" (extern_atom name)
| EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name)
| EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
| EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
| EF_vload_global(chunk, id, ofs) ->
sprintf "volatile load %s global %S %ld"
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| EF_vstore_global(chunk, id, ofs) ->
sprintf "volatile store %s global %S %ld"
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| EF_malloc -> "malloc"
| EF_free -> "free"
| EF_memcpy(sz, al) ->
sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al)
| EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
| EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text)
| EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
|
