1
2app load ["NormalTheory", "Normal", "basic"];
3open HolKernel Parse boolLib bossLib;
4open pairLib pairSyntax PairRules NormalTheory Normal basic;
5
6use "regAlloc.sml";
7open regAlloc;
8
9(*---------------------------------------------------------------------------*)
10(* Test case 1: The factorial function.                                      *)
11(*---------------------------------------------------------------------------*)
12
13val fact_def = Define
14   `fact i = if i = 0 then 1 else i * fact (i - 1)`;
15
16val def = (SSA_RULE o normalize) fact_def;
17
18(*
19 |- fact =
20       (\v1.
21          (if v1 = 0 then
22             1
23           else
24             (let v2 = v1 - 1 in
25              let v3 = fact v2 in
26              let v4 = v1 * v3 in
27                v4)))
28*)
29
30reg_alloc def;
31
32(*
33 |- fact =
34       (\r0.
35          (if r0 = 0 then
36             1
37           else
38             (let r1 = r0 - 1 in
39              let r1 = fact r1 in
40              let r0 = r0 * r1 in
41                r0))) : thm
42*)
43
44
45(*---------------------------------------------------------------------------*)
46(* Test case 2: Simple functions for testing spilling.                       *)
47(*---------------------------------------------------------------------------*)
48
49numRegs := 2;
50
51val def1 = Define
52   `f1 = \(v1:word32,v2:word32).
53     let (v3,v4,v5) = (v1,v2,v1) in (v1,v3,v5)`;
54
55val def2 = Define `
56    f2 = \(v1,v2,v3:word32).
57      let (v4,v5,v6) = f1(v1,v2) in
58      (v5,v3)`;
59
60val def3 = Define  `
61    f3 = \(v1:word32,v2:word32).
62     let v3 = v1 + v2 in
63     let v4 = v1 - v3 in
64     let v5 = v2 * v3 in
65     (v1,v2,v3,v4,v5)`;
66
67val def4 = Define  `
68    f4 = \(v1:word32,v2:word32,v3:word32,v4:word32).
69     let v5 = v3 + v4 in
70     (v1,v2,v3,v4,v5)`;
71
72val def5 = Define  `
73    f5 = \(v1:word32,v2:word32).
74     let v3 = v1 + v2 in
75     let v4 = v2 - v3 in
76     (v1,v2,v3,v4)`;
77
78val def6 = Define  `
79    f6 = \(v1:word32,v2:word32,v3:word32).
80     let (v3,v4) = f2 (v1,v2,v3) in
81     let (v5,v6,v7) = (v1,v3,v4) in
82     let (v8,v9,v10) = (v2,v2,v1) in
83     v5`;
84
85val def7 = Define  `
86    f7 = \(v1:word32).
87     let (v3,v4) = f2 (v1,v1,v1) in
88     let (v5,v6,v7) = (v1,v1,v3) in
89     let (v8,v9,v10) = (v1,v1,v1) in
90     v1`;
91
92(*
93reg_alloc def;
94*)
95