compilo/print_ltl.ml at master · ccompile/compilo · GitHub

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
92
93
94
open Format
open Register
open Print_rtl
open Ltl

let p_linstr f = function
  | Lmove(r1,r2,l) -> fprintf f "move %a %a -> %a"
    Print_rtl.p_pseudoreg r1 p_pseudoreg r2 p_label l
  | LLi(r,n,l) -> fprintf f "li %a %d -> %a"
    p_pseudoreg r (Int32.to_int n) p_label l
  | LLa(r,s,l) -> fprintf f "str %a %a -> %a"
    p_pseudoreg r p_address s p_label l
  | LLw(r,a,l) -> fprintf f "lw %a %a -> %a"
    p_pseudoreg r p_address a p_label l
  | LSw(r,a,l) -> fprintf f "sw %a %a -> %a"
    p_pseudoreg r p_address a p_label l
  | LLb(r,a,l) -> fprintf f "lb %a %a -> %a"
    p_pseudoreg r p_address a p_label l
  | LSb(r,a,l) -> fprintf f "sb %a %a -> %a"
    p_pseudoreg r p_address a p_label l
  | LArith(ar,r1,r2,op,l) -> fprintf f "%a %a %a %a -> %a"
    Mips.print_arith ar p_pseudoreg r1 p_pseudoreg r2 p_operand op p_label l
  | LSet(cond,r1,r2,op,l) -> fprintf f "%a %a %a %a -> %a"
    (Mips.print_condition (Rtl.is_oimm op))
     cond p_pseudoreg r1 p_pseudoreg r2 p_operand op p_label l
  | LNeg(r1,r2,l) -> fprintf f "neg %a %a -> %a"
    p_pseudoreg r1 p_pseudoreg r2 p_label l
  | Lgoto(l) -> fprintf f "goto -> %a"
    p_label l
  | LBeq(r1,r2,l1,l2) -> fprintf f "beq %a %a %a -> %a"
    p_pseudoreg r1 p_pseudoreg r2 p_label l1 p_label l2
  | LBne(r1,r2,l1,l2) -> fprintf f "bne %a %a %a -> %a"
    p_pseudoreg r1 p_pseudoreg r2 p_label l1 p_label l2
  | LBeqz(r,l1,l2) -> fprintf f "beqz %a %a -> %a"
    p_pseudoreg r p_label l1 p_label l2
  | LBnez(r,l1,l2) -> fprintf f "bnez %a %a -> %a"
    p_pseudoreg r p_label l1 p_label l2
  | LJr r -> fprintf f "jr %a" p_pseudoreg r
  | Lcall (name,lbl) -> fprintf f "call(%s) -> %a"
    name p_label lbl
  | Lsyscall l -> fprintf f "syscall -> %a"
    p_label l
  | Lget_stack(r,n,l) -> fprintf f "get_stack %a %ld -> %a"
    p_pseudoreg r n p_label l
  | Lset_stack(r,n,l) -> fprintf f "set_stack %a %ld -> %a"
    p_pseudoreg r n p_label l

let successeurs = function
  | Lmove(_,_,l)
  | LLi(_,_,l)
  | LLa(_,_,l)
  | LLw(_,_,l)
  | LSw(_,_,l)
  | LLb(_,_,l)
  | LSb(_,_,l)
  | LArith(_,_,_,_,l)
  | LSet(_,_,_,_,l)
  | LNeg (_,_,l)
  | Lgoto l
  | Lsyscall l
  | Lget_stack(_,_,l)
  | Lset_stack(_,_,l)
  | Lcall (_,l) -> [l]
  | LBeqz (_,l1,l2)
  | LBnez (_,l1,l2)
  | LBne (_,_,l1,l2)
  | LBeq (_,_,l1,l2) -> [l1;l2]
  | LJr _ -> []

let rec generic_dfs printer dejavu g f start =
  try
    if not (dejavu.(start)) then
      begin
        let instr = Ltl.find_instr g start in
        printer start instr;
        dejavu.(start) <- true;
        List.iter (generic_dfs printer dejavu g f) (successeurs instr)
    end
  with Not_found -> ()

let rec ltl_dfs dejavu g f =
  let printer start instr =
    fprintf f "%a : %a\n" p_label start p_linstr instr
  in
  generic_dfs printer dejavu g f

let p_ldecl f d =
  let dejavu = Array.make (Rtl.max_label ()) false in
  fprintf f "%s(...):\n%a\n\n"
    d.name
    (ltl_dfs dejavu d.g) d.entry

let print_ltl f =
  List.iter (p_ldecl f)