Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Copyright (C) 1999-2006, 2008 Henry Cejtin, Matthew Fluet, Suresh |
2 | * Jagannathan, and Stephen Weeks. | |
3 | * Copyright (C) 1997-2000 NEC Research Institute. | |
4 | * | |
5 | * MLton is released under a BSD-style license. | |
6 | * See the file MLton-LICENSE for details. | |
7 | *) | |
8 | ||
9 | functor x86JumpInfo(S: X86_JUMP_INFO_STRUCTS) : X86_JUMP_INFO = | |
10 | struct | |
11 | open S | |
12 | open x86 | |
13 | ||
14 | val tracer = x86.tracer | |
15 | ||
16 | datatype status = Count of int | None | |
17 | ||
18 | val status_eq | |
19 | = fn (None , None ) => true | |
20 | | (Count i1, Count i2) => i1 = i2 | |
21 | | _ => false | |
22 | ||
23 | val status_toString | |
24 | = fn None => "None" | |
25 | | Count i => concat ["Count ", Int.toString i] | |
26 | ||
27 | datatype t = T of {get: Label.t -> status ref} | |
28 | ||
29 | fun newJumpInfo () | |
30 | = let | |
31 | val {get : Label.t -> status ref, ...} | |
32 | = Property.get(Label.plist, | |
33 | Property.initFun (fn _ => ref (Count 0))) | |
34 | in | |
35 | T {get = get} | |
36 | end | |
37 | ||
38 | local | |
39 | fun doit (status_ref, maybe_fn) | |
40 | = case !status_ref | |
41 | of None => () | |
42 | | Count i => status_ref := (maybe_fn i) | |
43 | in | |
44 | fun incNear (T {get}, label) | |
45 | = doit (get label, fn i => Count (i+1)) | |
46 | fun decNear (T {get}, label) | |
47 | = doit (get label, fn i => Count (i-1)) | |
48 | fun forceNear (T {get}, label) | |
49 | = doit (get label, fn _ => None) | |
50 | end | |
51 | fun getNear (T {get}, label) = !(get label) | |
52 | ||
53 | fun completeJumpInfo {chunk = Chunk.T {blocks, ...}, | |
54 | jumpInfo: t} | |
55 | = List.foreach | |
56 | (blocks, | |
57 | fn Block.T {entry, transfer,...} | |
58 | => (case entry | |
59 | of Entry.Jump _ => () | |
60 | | Entry.Func {label, ...} => forceNear (jumpInfo, label) | |
61 | | Entry.Cont {label, ...} => forceNear (jumpInfo, label) | |
62 | | Entry.Handler {label, ...} => forceNear (jumpInfo, label) | |
63 | | Entry.CReturn {label, func, ...} | |
64 | => if CFunction.maySwitchThreads func | |
65 | then forceNear (jumpInfo, label) | |
66 | else (); | |
67 | List.foreach | |
68 | (Transfer.nearTargets transfer, | |
69 | fn label | |
70 | => incNear (jumpInfo, label)))) | |
71 | ||
72 | val (completeJumpInfo, completeJumpInfo_msg) | |
73 | = tracer | |
74 | "completeJumpInfo" | |
75 | completeJumpInfo | |
76 | ||
77 | fun verifyJumpInfo {chunk as Chunk.T {blocks, ...}, | |
78 | jumpInfo: t} | |
79 | = let | |
80 | local | |
81 | val {get : Label.t -> status ref, | |
82 | destroy} | |
83 | = Property.destGet(Label.plist, | |
84 | Property.initFun (fn _ => ref (Count 0))) | |
85 | in | |
86 | val jumpInfo' = T {get = get} | |
87 | val destroy = destroy | |
88 | end | |
89 | val _ = completeJumpInfo {chunk = chunk, | |
90 | jumpInfo = jumpInfo'} | |
91 | ||
92 | val verified | |
93 | = List.forall | |
94 | (blocks, | |
95 | fn Block.T {entry,...} | |
96 | => let | |
97 | val label = Entry.label entry | |
98 | in | |
99 | if status_eq(getNear(jumpInfo, label), | |
100 | getNear(jumpInfo', label)) | |
101 | then true | |
102 | else (print "verifyJumpInfo: "; | |
103 | print (Label.toString label); | |
104 | print "\n"; | |
105 | print "jumpInfo: "; | |
106 | print (status_toString (getNear(jumpInfo, label))); | |
107 | print "\n"; | |
108 | print "jumpInfo': "; | |
109 | print (status_toString (getNear(jumpInfo', label))); | |
110 | print "\n"; | |
111 | false) | |
112 | end) | |
113 | ||
114 | val _ = destroy () | |
115 | in | |
116 | verified | |
117 | end | |
118 | ||
119 | val (verifyJumpInfo, verifyJumpInfo_msg) | |
120 | = tracer | |
121 | "verifyJumpInfo" | |
122 | verifyJumpInfo | |
123 | end |