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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
open Printf
open Camlcoq
open Datatypes
open Maps
open AST
open Gible
open Predicate
open PrintAST
let reg pp r =
fprintf pp "x%d" (P.to_int r)
let pred pp r =
fprintf pp "p%d" (P.to_int r)
let rec regs pp = function
| [] -> ()
| [r] -> reg pp r
| r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
let ros pp = function
| Coq_inl r -> reg pp r
| Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
let rec print_pred_op_gen f pp = function
| Plit p -> if fst p then f pp (snd p) else fprintf pp "~%a" f (snd p)
| Pand (p1, p2) -> fprintf pp "(%a ∧ %a)" (print_pred_op_gen f) p1 (print_pred_op_gen f) p2
| Por (p1, p2) -> fprintf pp "(%a ∨ %a)" (print_pred_op_gen f) p1 (print_pred_op_gen f) p2
| Ptrue -> fprintf pp "T"
| Pfalse -> fprintf pp "⟂"
let print_pred_option_gen f pp = function
| Some x -> fprintf pp "(%a)" (print_pred_op_gen f) x
| None -> ()
let print_pred_option = print_pred_option_gen pred
let print_bblock_exit pp i =
match i with
| RBcall(_, fn, args, res, _) ->
fprintf pp "%a = %a(%a)"
reg res ros fn regs args;
| RBtailcall(_, fn, args) ->
fprintf pp "tailcall %a(%a)"
ros fn regs args
| RBbuiltin(ef, args, res, _) ->
fprintf pp "%a = %s(%a)"
(print_builtin_res reg) res
(name_of_external ef)
(print_builtin_args reg) args
| RBcond(cond, args, s1, s2) ->
fprintf pp "if (%a) goto %d else goto %d"
(PrintOp.print_condition reg) (cond, args)
(P.to_int s1) (P.to_int s2)
| RBjumptable(arg, tbl) ->
let tbl = Array.of_list tbl in
fprintf pp "jumptable (%a)" reg arg;
for i = 0 to Array.length tbl - 1 do
fprintf pp "\tcase %d: goto %d" i (P.to_int tbl.(i))
done
| RBreturn None ->
fprintf pp "return"
| RBreturn (Some arg) ->
fprintf pp "return %a" reg arg
| RBgoto n ->
fprintf pp "goto %d" (P.to_int n)
let print_bblock_body pp i =
fprintf pp "\t\t";
match i with
| RBnop -> fprintf pp "nop\n"
| RBop(p, op, ls, dst) ->
fprintf pp "%a %a = %a\n"
print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls)
| RBload(p, chunk, addr, args, dst) ->
fprintf pp "%a %a = %s[%a]\n"
print_pred_option p reg dst (name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
| RBstore(p, chunk, addr, args, src) ->
fprintf pp "%a %s[%a] = %a\n"
print_pred_option p
(name_of_chunk chunk)
(PrintOp.print_addressing reg) (addr, args)
reg src
| RBsetpred (p', c, args, p) ->
fprintf pp "%a %a = %a\n"
print_pred_option p'
pred p
(PrintOp.print_condition reg) (c, args)
| RBexit (p, cf) ->
fprintf pp "%a %a\n" print_pred_option p print_bblock_exit cf
|