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